ZFC is _a_ foundation for maths, not _the_ foundation
A number of people seem to have the impression that ZFC, Zermelo-Fraenkel set theory with Choice, is the One True Foundation for all of mathematics.
Wikipedia: ‘Zermelo-Fraenkel set theory’
Nope. Although ZFC+FOL[a] is widely accepted as a framework in which much of mathematics can be encoded, it's by no means the only such framework available. In fact, setting aside the debates around the Axiom of Choice[b], ZFC is both vastly overpowered for many areas of mathematics, yet simultaneously underpowered for others:
- Nik Weaver's paper “Is set theory indispensable?” describes how much mathematics can be done in systems much weaker than ZFC, and indeed, might be better done in such systems.
“Is set theory indispensable?” [abstract + link to PDF]
- ‘Grothendieck universes’ are used in algebraic geometry; the existence of nontrivial Grothendieck universes is equivalent to the existence of strongly inaccessible cardinals[c]. The ZFC axioms alone can't prove the existence of inaccessible cardinals. On the other hand, if we use ZFC and assume that an inaccessible cardinal exists, we can prove that ZFC is consistent, i.e. that it does not prove contradictions.
More generally, of course, Gödel's first incompleteness theorem[d] means there are mathematical statements that can't be proved in ZFC, that are ‘independent’ of it - most famously, the Continuum Hypothesis[e], as demonstrated by the combined work of Gödel and Cohen.
ZFC isn't even the be-all-and-end-all of set theory. Apart from constructive variants like CZF and IZF, other set theories include von Neumann-Bernays-Gödel (NBG), Morse-Kelley (MK), New Foundations (NF) and Sets, Elements and Relations (SEAR)[f].
In addition to set theory, however, there are other possibilities for foundations, such as type theory[g]:
[T]ype theory is not built on top of first-order logic; it does not require the imposing superstructure of connectives, quantifiers, and inference to be built up before we start to state axioms. Of course, type theory has first-order logic, which is a necessity for doing mathematics. But first-order logic in type theory is just a special case of the type-forming rules. A proposition is merely a certain type; to prove it is to exhibit an element of that type. When applied to types that are propositions, the type-forming operations of cartesian product, disjoint union, and function types reduce to the logical connectives of conjunction, disjunction, and implication; the quantifiers arise similarly from dependent sums and products. Thus, type theory is not an alternative to set theory built on the same “sub-foundations”; instead it has re-excavated those sub-foundations and incorporated them into the foundational theory itself.[h]
One such type theory is Homotopy Type Theory (HoTT):
nLab: ‘homotopy type theory - advantages’
All that said, most mathematicians don't actually care much about foundations, since mathematical research often doesn't require them to - they just need to know that in theory, their work _could_ be derived from a reasonable collection of base concepts. Still, amongst those whose work and interests end up engaging with the issue of mathematical foundations, there is no shortage of vigorous discussion and debate on the topic, as demonstrated by this 2016 post to the n-Category Café blog:
“Foundations of Mathematics”
The final part of Baez' post appeals to me:
Personally I don’t think the metaphor of "foundations" is even appropriate for this approach. I prefer a word like "entrance". A building has one foundation, which holds up everything else. But mathematics doesn’t need anything to hold it up: there is no "gravity" that pulls mathematics down and makes it collapse. What mathematics needs is "entrances": ways to get in. And it would be very inconvenient to have just one entrance.
☙
🏷 maths
Glossary
Gemlog Home
☙
[a] ‘FOL’ is ‘First-Order Logic’. ZFC alone doesn't give us a way to make inferences from the axioms.
Wikipedia: ‘First-order logic’
[b] Although accepting AC leads to results that can feel counterintuitive, such as the Banach-Tarski paradox, its _negation_ leads to such results as well, such as “In some model [of ZF¬C], there is an infinite set of real numbers without a countably infinite subset.”
Wikipedia: ‘Banach-Tarski paradox’
Reddit: “Why is the Banach-Tarski paradox an argument against the Axiom of Choice?”
Wikipedia: ‘Axiom of Choice - Statements consistent with the negation of AC’
[c] Wikipedia: ‘inaccessible cardinal’
[d] Gödel's first incompleteness theorem shows that in _any_ sufficiently powerful formal system, there are certain true statements that the system can't _prove_ are true, i.e. the system is ‘incomplete’.
Wikipedia: ‘Gödel's incompleteness theorems’
Wikipedia: ‘complete theory’
An example of a _complete_ system is Presburger arithmetic, in which multiplication is not available:
Wikipedia: ‘Presburger arithmetic’
[e] Wikipedia: ‘continuum hypothesis’
[f] For further details, refer to e.g.:
Wikipedia: ‘constructive set theory’
Wikipedia: ‘von Neumann-Bernays-Gödel set theory’
Wikipedia: ‘Morse-Kelley set theory’
Wikipedia: ‘New Foundations’
nLab: ‘SEAR’
[g] nLab: ‘type theory - type-theoretical foundations’
[h] “From set theory to type theory”