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.
312
questions
17
votes
0
answers
434
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 ...
12
votes
0
answers
531
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 ...
1
vote
0
answers
186
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$
...
3
votes
0
answers
175
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 ...
62
votes
4
answers
6k
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 ...
3
votes
1
answer
181
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 ...
7
votes
1
answer
402
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 ...
13
votes
0
answers
355
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 ...
6
votes
1
answer
441
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$ ...
4
votes
2
answers
515
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.
...
4
votes
0
answers
297
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 ...
6
votes
2
answers
363
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 $...
5
votes
1
answer
383
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 ...
35
votes
3
answers
2k
views
Defining $SU(n)$ in HoTT
From a recent answer by Mike Shulman, I read:
"HoTT is (among other things) a foundational theory, on roughly the same ontological level as ZFC, whose basic objects can be regarded as $\infty$-...
1
vote
1
answer
308
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 ...
9
votes
1
answer
769
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 ...
14
votes
4
answers
2k
views
Where is the end of universe?
In some sense the empty set ($\emptyset$) and the global set of all sets ($G$) are the ends of the universe of mathematical objects. The world which $ZFC$ describes has an end from the bottom and is ...
22
votes
1
answer
3k
views
Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?
Let the proof theoretic ordinal $\alpha$ of a theory $T$ be the least recursive ordinal such that $T$ does not prove that $\alpha$ is well-founded. This ordinal is intended to quantify in some sense ...
21
votes
2
answers
3k
views
Do set theorists work in T?
In the thread Set theories without "junk" theorems?, Blass describes the theory T in which mathematicians generally reason as follows:
Mathematicians generally reason in a theory T which (...
10
votes
1
answer
1k
views
Erroneous proof of recursion theorem examples
In his book Elements of Set Theory, Herbert Enderton defines (p. 70) a Peano system as a triple $(N, S, e)$ where $N$ is a set, $S$ is an $N$-valued function defined on $N$ and $e$ is a member of $N$ ...
20
votes
4
answers
4k
views
Is there a categorical proof of Gödel's incompleteness theorem?
A significant result in set theory was shown by Cohen when he showed that the continuum hypothesis was independent of ZFC using a new technique called forcing. In Topos theory, this result has a new ...
15
votes
1
answer
821
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 ...
12
votes
3
answers
1k
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, ...
33
votes
3
answers
5k
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 ...
10
votes
1
answer
433
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 ...
10
votes
1
answer
331
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$ ...
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 ...
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 ...
2
votes
1
answer
450
views
Is the statement "All numbers are counting numbers" independent of $PA$?
In his paper, "Completed versus Incomplete Infinity in Arithmetic" (which can be found here), the late Edward Nelson defines the notion of 'counting number' as follows:
0 is a counting ...
11
votes
7
answers
1k
views
(Non?)-linearity of the consistency strength ordering in ZF
Much of the research taking place in set theory, is related to the classification of sentences according to their consistency strength relative to ZF. In order to be more specific, we say that for all ...
1
vote
0
answers
488
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 ...
152
votes
5
answers
27k
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 ...
15
votes
2
answers
2k
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 ...
5
votes
0
answers
234
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 ...
7
votes
1
answer
302
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 ...
11
votes
5
answers
981
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 ...
6
votes
1
answer
293
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 ...
8
votes
4
answers
748
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 $...
5
votes
0
answers
259
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 ...
10
votes
4
answers
958
views
On a weak choice principle
[PLEASE SEE EDITS AT BOTTOM OF QUESTION]
Consider the following set-theoretic axiom:
For each set $X$ there exists a set-indexed collection $\{C_i \to X\}_{i\in I_X}$ of surjections such that for ...
16
votes
2
answers
796
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 ...
2
votes
1
answer
359
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 ...
12
votes
2
answers
832
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 ...
15
votes
2
answers
1k
views
Could Kronecker accept a proof of Goodstein's theorem?
A famous result of Goodstein asserts that the Goodstein sequence of integers terminates.
For a precise statement and a short proof, see https://en.wikipedia.org/wiki/Goodstein%27s_theorem.
A well ...
0
votes
0
answers
178
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 ...
8
votes
3
answers
1k
views
How much of concrete mathematics can be expressed in the language of category theory?
Question 1
How much of group/ring/lattice/... theory can be expressed in purely categorical terms (only using the notions object, morphism, identity morphism, and composition), that is, as properties ...
7
votes
1
answer
1k
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 ...
6
votes
1
answer
494
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 ...
8
votes
2
answers
743
views
weakening naive comprehension to avoid the paradoxes
Weakening the axiom of naive comprehension has not been a popular way of escaping from the set-theoretic paradoxes because no consistent weakenings seem to be particularly well motivated or even to ...
28
votes
2
answers
2k
views
Age of Stochasticity?
One user on MSE made an interesting question, which was unanswered so I suggested him to post it here but he refused for personal reasons and said I could ask it here.
The question is this:
Today ...