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.
330 questions
157
votes
5
answers
28k
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 ...
- 1,667
74
votes
11
answers
12k
views
Why hasn't mereology succeeded as an alternative to set theory?
I have recently run into this Wikipedia article on mereology. I was surprised I had never heard of it before and indeed it seems to be seldom mentioned in the mathematical literature. Unlike set ...
- 5,902
74
votes
8
answers
14k
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 ...
- 6,917
63
votes
4
answers
7k
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,318
60
votes
7
answers
9k
views
In what respect are univalent foundations "better" than set theory?
It was an ambitious project of Vladimir Voevodsky's to provide new foundations for mathematics with univalent foundations (UF) to eventually replace set theory (ST).
Part of what makes ST so appealing ...
59
votes
8
answers
12k
views
How true are theorems proved by Coq?
Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...
- 35.4k
55
votes
10
answers
11k
views
How should a "working mathematician" think about sets? (ZFC, category theory, urelements)
Note that "a working mathematician" is probably not the best choice of words, it's supposed to mean "someone who needs the theory for applications rather than for its own sake". Think about it as a ...
- 1,115
50
votes
4
answers
6k
views
Do set-theorists use informal set theory as their meta-theory when talking about models of ZFC?
Here, Noah Schweber writes the following:
Most mathematics is not done in ZFC. Most mathematics, in fact, isn't done axiomatically at all: rather, we simply use propositions which seem "intuitively ...
- 509
47
votes
7
answers
7k
views
What is an explicit bijection in combinatorics?
A standard way of demonstrating that two collections of combinatorial objects have the same cardinality is to exhibit a bijection between them. Browsing through some examples (here, there, yonder) ...
- 48.8k
45
votes
5
answers
6k
views
Nonstandard analysis in probability theory
I am quite new at nonstandard analysis, and recently I became aware of its use in probability theory mainly through the following two books:
Nelson (1987). Radically Elementary Probability Theory
...
- 1,302
43
votes
4
answers
5k
views
Lists as a foundation of mathematics
I am wondering if there is a foundation of mathematics where not sets or "set-like objects" (such as objects of a suitable topos as in ETCS) are the primitive notion, but rather lists. These ...
- 63.1k
39
votes
8
answers
6k
views
Learning roadmap for Foundations of Mathematics (for the working mathematician)
(At the risk of being vapulated and downvoted, I'll ask this here.)
Suppose you work in a field that has nothing to do with the foundations of mathematics, but thanks to MO, you are becoming more and ...
39
votes
7
answers
6k
views
Is V, the Universe of Sets, a fixed object?
When I first read Set Theory by Jech, I came under the impression that the Universe of Sets, $V$ was a fixed, well defined object like $\pi$ or the Klein four group. However as I have read on, I am ...
- 750
39
votes
8
answers
14k
views
Good introductory book to type theory?
I don't know anything about type theory and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle ...
38
votes
4
answers
4k
views
Illustrating Edward Nelson's Worldview with Nonstandard Models of Arithmetic
Mathematician Edward Nelson is known for his extreme views on the foundations of mathematics, variously described as "ultrafintism" or "strict finitism" (Nelson's preferred term), which came into the ...
- 4,587
38
votes
4
answers
6k
views
Could groups be used instead of sets as a foundation of mathematics?
Sets are the only fundamental objects in the theory $\sf ZFC$. But we can use $\sf ZFC$ as a foundation for all of mathematics by encoding the various other objects we care about in terms of sets. The ...
- 3,137
37
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 ...
- 3,752
36
votes
6
answers
6k
views
Who needs Replacement anyway?
The set theory ETCS famously comes without the Replacement axiom schema (or an equivalent) that is part of ZFC. One (to me, not apparently useful) set that one cannot build in ETCS is $\coprod_{n\in \...
- 35.4k
36
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$-...
- 43.2k
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 ...
- 447
32
votes
11
answers
11k
views
Is PA consistent? do we know it?
1) (By Goedel's) One can not prove, in PA, a formula that can be interpreted to express the consistency of PA. (Hopefully I said it right. Specialists correct me, please).
2) There are proofs (...
30
votes
6
answers
3k
views
Mathematics without the principle of unique choice
The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ ...
- 66.7k
29
votes
3
answers
3k
views
Are there substantive differences between the different approaches to "size issues" in category theory?
In category theory, there are different ways to approach the "size issues" that crop up when we try to formalise the subject in axiomatic set theory. As far as I can tell, there are two main ...
- 961
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 ...
- 393
28
votes
0
answers
2k
views
Is Feferman's unlimited category theory dead?
In 2013 Solomon Feferman in Foundations of unlimited category theory: what remains to be done (The Review of Symbolic Logic, 6 (2013) pp 6-15, link) laid out three desirable axioms for "...
- 1,446
27
votes
4
answers
4k
views
Who introduced the terms "equivalence relation" and "equivalence class"?
Consider that the question does not concern the origin of the ideas of equivalence relation and equivalence class. It exactly concerns the origin of the terms "equivalence relation" and "equivalence ...
- 2,437
26
votes
1
answer
2k
views
Nontrivial circular arguments?
There is a famous circular argument for the Prime Number Theorem (PNT). It turns
out that there exists an infinite sequence of elementary-to-prove Chebyshev-type estimates
that taken together imply ...
- 17.6k
26
votes
4
answers
1k
views
Are there lightweight foundations for arbitrarily extendable objects?
My experience with foundations is rather scant, but I've run into some types of objects that seem to resist the sort of set-theoretic encoding schemes via Kurowski tuples that are rather common for ...
- 45.7k
25
votes
5
answers
4k
views
What is some current research going on in foundations about?
What is some current research going on in the foundations of mathematics about?
Are the foundations of mathematics still a research area, or is everything solved? When I think about foundations I'm ...
25
votes
1
answer
2k
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 ...
- 551
25
votes
1
answer
2k
views
On Joyal's completeness theorem for first order logic
In 1978, in a series of unpublished conferences in Montréal, A. Joyal announced a remarkable theorem that unified several completeness theorems for fragments of first order logic, as well as first ...
- 5,902
24
votes
2
answers
2k
views
Foundations and contradictions of Scholze's work: the category of presentable infinity categories contains itself
Preface: I am not an expert in the work of Scholze, or anything for that matter.
Question
Has Scholze stated what axioms he is using to develop his theory of motives and analytic geometry. In the ...
- 383
24
votes
1
answer
5k
views
What is the most transparent, rigorous definition of the Univalence Axiom?
I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers ...
- 469
23
votes
3
answers
2k
views
Why would the category of sets be intuitionistic?
This question is probably really naive. And, I hope the title doesn't come off as too combative. I think that topoi of $\mathbf{Set}$-valued sheaves provide an excellent motivation for higher-order ...
- 3,793
23
votes
5
answers
2k
views
Axiomatic construction of trigonometric functions
I am able to construct functions $\sin,\cos\colon \mathbb R \to \mathbb R$ satisfying the following properties:
$\sin^2 x + \cos^2 x = 1$,
$\sin(x+y)=\sin x \cos y + \sin y\cos x$, $\cos(x+y)=\cos x \...
- 702
23
votes
2
answers
1k
views
Statements in differential geometry independent from ZFC
It is well known that some problems in functional analysis and in general topology are independent from ZFC: to name a few, Kaplansky's conjecture, the existence of outer automorphisms of the Calkin ...
22
votes
4
answers
4k
views
How much of the axiom of choice do you need in mathematics?
Say we have DC-λ where λ is some inaccessible cardinal. Is that enough to develop all of ordinary mathematics? If not, is there a strengthening that is but that nevertheless does not assume full ...
- 419
22
votes
1
answer
4k
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 ...
- 711
21
votes
6
answers
3k
views
Where in ordinary math do we need unbounded separation and replacement?
[I have updated the question after initial comments in the hope of clarifying it.]
I do quite a bit of reasoning, typically about topology and metric spaces, in "non-standard" foundations, such as ...
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 (...
- 221
20
votes
5
answers
2k
views
Does formalizing math require search and creativity, or is it near-mechanical?
I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.
Is this type of conversion something that ...
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 ...
- 2,083
19
votes
3
answers
1k
views
Large categories vs. $\mathrm{U}$-categories: why is the loss of category-theoretic information inessential?
I've asked a related question about nine months ago here, however, apparently, I lacked expertise to ask the precise question I want to ask here, as I wish to revisit the matter of universes. I hope ...
- 1,115
19
votes
2
answers
2k
views
Which kind of foundation are mathematicians using when proving metatheorems?
Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. For every two objects/sets $a,b$ one can ask whether $a=b$ or not....
user103598
19
votes
1
answer
937
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 ...
- 21.1k
19
votes
0
answers
703
views
The cofinality of $(\mathbb{N}^\kappa,\le)$ for uncountable $\kappa$?
For a partially ordered set $P$, a set $A\subseteq P$ is cofinal if for each element of $P$ there is a larger element in $A$. The cofinality of $P$, ${\rm cof}(P)$, is the minimal cardinality of a ...
- 3,104
18
votes
3
answers
3k
views
What's the earliest result (outside of logic) that cannot be proven constructively?
Although mathematicians usually do not work in constructive mathematics per se, their results often are constructively valid (even if the original proof isn't).
An obvious counter-example is the law ...
- 6,353
18
votes
4
answers
2k
views
Does the existence of the von Neumann hierarchy in models of Zermelo set theory with foundation imply that every set has ordinal rank?
Let $T$ be the theory consisting of Zermelo's original set theoretic axioms (extensionality, empty set, pairing, union, powerset, infinity, separation, choice) together with foundation. Put more ...
- 2,240
17
votes
10
answers
7k
views
Set theory and alternative foundations
Every foundational system for mathematics I have ever read about has been a set theory, from ETCS to ZFC to NF. Are there any proposals for a foundational system which is not, in any sense, a set ...
- 555
17
votes
2
answers
2k
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 ...
- 141