Questions tagged [foundations]

Mathematical logic, Set theory, Peano arithmetic, Model theory, Proof theory, Recursion theory, Computability theory, Univalent foundations, Reverse mathematics, Frege foundation of arithmetic, Goedel's incompleteness and Mathematics, Structural set theory, Category theory, Type theory.

Filter by
Sorted by
Tagged with
0 votes
0 answers
66 views

Can Frege's program be revived to serve foundations for mathematics?

To second order logic, add a primitive partial one place function symbol "$\epsilon$" from unary predicate symbols [upper cases] to object symbols [lower cases]. Define: $ x=y \equiv_{df} \...
user avatar
0 votes
0 answers
70 views

A formal definition of a useful theorem?

Sorry if this feels a bit squishy, but I'm wondering if there is any published work trying to give a fully formal definition of the notion of a useful theorem. I mean, in mathematics we all know that ...
user avatar
  • 1,525
1 vote
1 answer
216 views

An axiomatic approach to the multiverse of sets

Work in a theory where the primitives are classes $X,Y,Z,\dots$, and class membership $X\in Y$, and add an individual constant $\mathcal{M}$ called 'the multiverse'. Classes which are members of the ...
user avatar
  • 6,251
7 votes
1 answer
117 views

Is there a purely constructive presentation of the HK integral?

Treating the Riemann integral in a constructive setting is easy and straightforward. Treating the closely related but much more powerful Henstock-Kurzweil integral constructively is almost easy, ...
user avatar
  • 1,015
3 votes
0 answers
107 views

Consistency of Generalised Continuum Hypothesis and univalence in HoTT

In homotopy type theory, propositional excluded middle and the axiom of choice sets are both consistent with univalence, both of which yields type theoretic models for classical mathematics. However, ...
user avatar
0 votes
0 answers
64 views

'Maximising interpretative power entails maximising consistency strength'?

I'm hoping there is a clear mathematical answer to this question (hence asking it here) rather than anything more exegetical (in which case it's presumably not appropriate for this site). In his paper ...
user avatar
24 votes
1 answer
1k views

Coinduction for all?

Every undergraduate in mathematics learns about proofs by mathematical induction. Moreover, every undergraduate taking a course in theoretical computer science or logic learns about inductive ...
user avatar
3 votes
1 answer
313 views

Homotopical realizability

After a long story of dancing around the effective topos $ \mathcal{Eff}$, I finally resolved to get to the bottom of it. To this effect, working as it were backward, I ended up revisiting Kleene's ...
user avatar
13 votes
0 answers
333 views

The free complete lattice on three generators, beyond ZF

This was originally asked at MSE; although it is still under bounty it seems unlikely to be answered there. $\mathsf{ZF}$ proves that there is no free complete lattice on three generators since any ...
user avatar
10 votes
0 answers
378 views

Harvey Friedman's minimalist axioms for set theory

[This is a question on the FOM mailing list.] In 1997, Harvey Friedman introduced the following theory: Let $\in$ be a binary predicate and $U$ be a constant. Add the following axioms: Subworld ...
user avatar
  • 1,577
1 vote
0 answers
172 views

Does foundationless Ackermann set theory prove replacement?

From Ackermann's set theory equals ZF (1970) by William N. Reinhardt: Let A be the theory determined by the following axioms: Extensionality: $\forall z (z \in x \leftrightarrow z \in y) \to x = y$ ...
user avatar
  • 1,577
2 votes
0 answers
144 views

Can we interpret ZFC in GEM?

I have long held similar views as put forth here. As professor Hamkins points out though, $(M,\subseteq)$ is insufficient to model most of mathematics. However, this is unsatisfactory to me, as this ...
user avatar
  • 190
3 votes
1 answer
132 views

0-valued and 1-valued logics?

In addition to classic two-valued logic, there are many many-valued logics, including Łukasiewicz's and Kleene's three-valued logics, Gödel's many-valued logic $G_k$, and infinite-valued fuzzy logic ...
user avatar
  • 477
7 votes
1 answer
318 views

Does the small object argument need replacement?

Does one need the axiom of replacement in the small object argument and in the transfinite construction of free algebras? My motivation for the question is that I heard that the axiom of replacement ...
user avatar
13 votes
0 answers
348 views

Context of set theory in which one doesn't have to worry about size issues

In this beautiful talk by Colin McLarty, McLarty quotes Grothendieck: It would be nice to have a context where one doesn't add any real axioms to set theory, and yet one can work with categories ...
user avatar
6 votes
1 answer
421 views

What do you call the generalisation of the direct image?

This question was posted on Math Stack Exchange, but did not attract an answer. Here is the question: Informal Description Let me start with an example. Let $X$ be the set $\{a, b, c, d, e\}$ and $E$ ...
user avatar
  • 105
4 votes
2 answers
361 views

Applications of ZFA-Set Theory

The set theory with atoms (ZFA), is a modified version of set theory, and is characterized by the fact that it admits objects other than sets, atoms. Atoms are objects which do not have any elements. ...
user avatar
  • 105
4 votes
0 answers
220 views

Can this graph theory serve as a foundational theory of mathematics?

Working in mono-sorted first order logic, add primitives of equality and its axioms, set membership $\in$, a partial ternary relation $\to$ denoting is the direction from to, and at last a total unary ...
user avatar
6 votes
2 answers
354 views

Resource request on "$\in$-homomorphisms" in Set Theory

Very loosely put, this is the intuitive idea behind an $\in$-homomorphism: Let $\mathcal{U}$ and $\mathcal{W}$ be universes of sets. A function $f \colon \mathcal{U} \to \mathcal{W}$ is said to be an $...
user avatar
  • 61
4 votes
1 answer
361 views

What structure do all kinds of theories, models, interpretations, proofs and all that form?

This is a question about a structure that can be used to investigate all kind of structures that can be investigated. Many years ago with Joseph Gubeladze we discussed something similar but I only ...
user avatar
7 votes
1 answer
561 views

Practical Benefits of HTT/univalent foundations for assisted proofs

I'm trying to understand what the claimed practical benefits of HTT/univalent foundations are for doing computer assisted proofs and while I've seen a lot of claims of benefits they all seem to be ...
user avatar
  • 1,525
15 votes
1 answer
627 views

Can the opposite of an elementary topos be an elementary topos?

This question is not really about elementary topoi, it is much more about a category $(\mathcal{E}, \Omega)$ admitting a subobject classifier, or about a category with power objects, you can choose ...
user avatar
10 votes
1 answer
398 views

Is material set theory conservative over structural set theory?

Suppose a statement $\phi$ that doesn't use the global $\in$-relation or the global $=$-relation in an essential way is provable in some material set theory, say bounded Zermelo with choice. (So that ...
user avatar
32 votes
3 answers
4k views

Top-down mathematics, or "Where it all begins"

Sorry if this is off-topic. It was my attempt to take a top-down approach to mathematics. Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as ...
user avatar
  • 437
15 votes
2 answers
1k views

When the definition of a set starts to matter in category theory

In most introductory courses to category theory, the precise definition of a set is more-or-less ignored. The idea being that all basic results in the subject hold for any reasonable definition of a ...
user avatar
0 votes
2 answers
1k views

Has there been any serious attempt at a "circular" foundation of mathematics?

As far as I know, there is no published attempt at a "circular" foundations of mathematics though I'ave seen it noted by many category theorists and logicians without in-depth analysis, e.g ...
user avatar
11 votes
3 answers
870 views

Elementary theory of the category of groupoids?

One axiomatisation of set theory, the Elementary Theory of the Category of Sets, or ETCS for short, comes from category theory and states that sets and functions form a locally cartesian-closed, ...
user avatar
1 vote
0 answers
398 views

Is this a good way of conceptualising the current status of Foundation of Maths projects?

I have been reading 'A Very Short Introduction to Mathematics' by Timothy Gowers and at one point he mentions that most of the mathematical proofs can be finally resolved to a set of logical ...
user avatar
  • 11
35 votes
2 answers
3k views

Building algebraic geometry without prime ideals

$\DeclareMathOperator\Spec{Spec}\DeclareMathOperator\ev{ev}$Teaching algebraic geometry, in particular schemes, I am struggling to provide intuitive proofs. In particular, I find it counter-intuitive ...
user avatar
  • 3,472
138 votes
5 answers
23k views

What makes dependent type theory more suitable than set theory for proof assistants?

In his talk, The Future of Mathematics, Dr. Kevin Buzzard states that Lean is the only existing proof assistant suitable for formalizing all of math. In the Q&A part of the talk (at 1:00:00) he ...
user avatar
  • 1,457
15 votes
2 answers
1k views

Formal definition of homotopy type theory

The HoTT community is quite friendly, and produces many motivational introductions to HoTT. The blog and the HoTT book are quite helpful. However, I want to get my hands directly onto that, and am ...
user avatar
  • 4,005
7 votes
1 answer
282 views

What is difference between working with small and large category of spaces?

The following construction have always bugged me. This is p328, Remark 5.1.6.1 in Lurie's Higher Topos Theory. Lurie begins with the following: Construction: Let $C$ be a simplicial set. $S$ denote ...
user avatar
8 votes
4 answers
637 views

Self-contained formalization of random variables?

I have not been able to find any formalization of random variables that supports construction of new random variables dependent on previously constructed ones. In what I have found, a random variable $...
user avatar
  • 2,576
6 votes
1 answer
276 views

Set Theoretic Geology II: The structure of the directed partial order of grounds

In my previous question Set-theoretic geology: controlled erosion? and the great answer by Jonas Reitz, I have learned a few things, starting from the awareness that I understand the fine-grain ...
user avatar
5 votes
0 answers
186 views

Higher order arithmetic, hierarchies and proof theoretic ordinals

I asked this question on MSE some days ago but I have not received any answer so I have decided to post it here. I would like to consider a generalization of the notation $\Pi$ and $\Sigma$ used for ...
user avatar
5 votes
0 answers
232 views

Class theory of ZF-minus-Powerset as classical predicative system?

I've been thinking about some mathematics in weaker foundational systems a little bit, largely from a structural viewpoint, and with particular attention to classes. Some categories I've been keeping ...
user avatar
7 votes
1 answer
395 views

Iterated Gentzen: or, a Sith objection to the proof of consistency of PA

$\DeclareMathOperator\PRA{PRA}\DeclareMathOperator\WF{WF}\DeclareMathOperator\Con{Con}\DeclareMathOperator\PA{PA}$Preamble: In the year … in a galaxy far far away, a nasty Sith named Darth Dubious (...
user avatar
11 votes
5 answers
771 views

Emergence of the discrete from the continuum

An almost eternal theme in Mathematics is the approximation of the Continuum by the Discrete. This core idea goes back at least to Archimedes, and remains active to these very days (and quite likely ...
user avatar
9 votes
1 answer
290 views

An internalized version of Tennenbaum's Theorem

Tennenbaum's celebrated 1959 theorem (see here for a reference) is certainly one of the key theorems in mathematical logic. Not so much for its proof, but because it helps "isolating" $N$ ...
user avatar
1 vote
1 answer
218 views

Complete and consistent first-order theories that contain interesting phenomena

Gödel has shown that a consistent recursively axiomatizable first-order theory that can interpret Robinson arithmetic is incomplete. I think there is some sentimental value in working with a theory ...
user avatar
14 votes
2 answers
683 views

Appearance of proof relevance in "ordinary mathematics?"

I've been wondering recently what—if any—applications proof theory has to ordinary mathematics (by which I mean algebra, analysis, topology, and so on). In particular, I'd be fascinated to see a proof ...
user avatar
  • 157
1 vote
1 answer
287 views

Reference request on Gentzen's proof of the consistency of PA

I've always been interested in having a good understanding of Gentzen's proof of the consistency of arithmetic. Being more precise, he showed that $PRA + WF(\epsilon_0) \vdash Con(PA)$. I am ...
user avatar
  • 1,713
58 votes
4 answers
5k views

When size matters in category theory for the working mathematician

I think a related question might be this (Set-Theoretic Issues/Categories). There are many ways in which you can avoid set theoretical paradoxes in dealing with category theory (see for instance ...
user avatar
  • 1,713
1 vote
0 answers
159 views

A syntax independent theory of categories

The classic way to encounter the theory of categories is via Set Theory via the typical definition we see for categories. We see all kinds of categories that are equivalent to the category of small ...
user avatar
  • 1,435
12 votes
2 answers
742 views

The inconsistency of Graham Arithmetics plus $ \forall n, n < g_{64}$

As you all know, Ronald Graham just passed away. He is famous for many fabulous contributions to finite combinatorics, and much much more, but perhaps none of them is as popular as the infamous ...
user avatar
8 votes
1 answer
955 views

Are categories special, foundationally?

Some folks over at nLab want to use categories as a foundation for all of mathematics, I'm guessing as an alternative to sets. Sets work fine, and so do categories, so I have started wondering what ...
user avatar
  • 199
5 votes
1 answer
398 views

Historical origin of the empty set

The question is in the title: Who first claimed the existence / necessity of the empty set ? When did this happen ? Of course I know that the notation $\emptyset$ goes back to André Weil, and that ...
user avatar
  • 47.1k
4 votes
2 answers
581 views

What is a good definition of a mathematical structure?

At the moment I am writing a textbook in Foundations of Mathematics for students and trying to give a precise definition of a mathematical structure, which is the principal notion of structuralist ...
user avatar
  • 32.9k
70 votes
8 answers
8k views

Category theory and set theory: just a different language, or different foundation of mathematics?

This is a question to research mathematicians, as well as to those concerned with the history and philosophy of mathematics. I am asking for a reference. In order to make the reference request as ...
user avatar
  • 6,495
16 votes
1 answer
673 views

Positive set theory and the "co-Russell" set

This is a more focused version of a question which was asked at MSE a couple years ago, but is still unanswered there. That question asks about a broad range of theories, whereas this version focuses ...
user avatar

1
2 3 4 5 6