đŸ Archived View for flexibeast.space âș gemlog âș 2020-12-27.gmi captured on 2024-03-21 at 15:40:41. Gemini links have been rewritten to link to archived content
âŹ ïž Previous capture (2024-02-05)
âĄïž Next capture (2024-05-10)
-=-=-=-=-=-=-
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:
âIs set theory indispensable?â [abstract + link to PDF]
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
â
[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â