# What theorems are most important for the foundation of mathematics?

What are the mathematical theorems which are considered as the most important for the mathematics themselves?

By importance I mean foundational to mathematics as a whole or foundational to a good chunk of mathematics.

By "foundational", I don't mean historical founding but crucial to the current foundations of the edifice of mathematics.

I'm thinking of Gödel's incompleteness theorem for example, which is perhaps the most talked about, but I don't really understand the importance of it in practical terms and I would expect a few less well known theorems to be equally or even more important.

• Define important. Mar 11 '19 at 11:21
• @Richard Can you elaborate? I know Pythagoras and his theorem, and I can see the historical importance of it. What I don't see is how it would be foundational to mathematics today. Perhaps, I need to specify that by "foundational", I don't mean historical founding but current foundation of the edifice. Mar 11 '19 at 12:24
• @Richard: Could you please explain how e.g. group theory, which is essentially the mathematical study of symmetries, is fundamentally built upon "the axioms of right triangles"? Mar 11 '19 at 13:28
• @Richard That's just not true. I'd love to hear, for example, how group theory (or computability theory, or algebraic topology, or ...) is ultimately founded on right triangles. Mar 11 '19 at 14:09
• The sense of "foundational" you have in mind does not exist anymore, one can "build" mathematics on multiple alternative basic notions (sets, categories, types), or none, and switch bases at will, see Azzouni Is there still a Sense in which Mathematics can have Foundations? (the answer is no). So you will have to come up with a different interpretation of "most important" to make this answerable. Perhaps, most talked about, or having most versatile applications/connections to different fields. Mar 11 '19 at 18:50

One person's foundations are another person's pointless pedantics. What follows is my own view of the foundational side of mathematics. Many of these results are not widely known among mathematicians, and so their foundational significance is definitely up for debate - is it really important if nobody needs it? - but to my mind these are results which tell us something important about the character of mathematics: they're not necessarily what makes it tick, but they say something about the sound that ticking makes.

Gödel's incompleteness theorem is definitely fundamental - it tells us what we can hope for from a "foundation for mathematics." A lot of this is taken for granted, but pre-Gödel the idea of a "nice" axiom system which would suffice to (at least in principle) resolve all mathematical questions was a reasonable dream. Post-Gödel, I think the theorem suffers from its in-retrospect-obviousness, but even if we just think of it as the confirmation of a perfectly reasonable intuition about the limits of mathematical reasoning (which some people at the time certainly had) it's still important in that respect. Tarski's undefinability theorem also deserves mention here, since it emphasizes the fact that representation in the language of arithmetic is the real issue here as opposed to the more-obviously-intriguing self-reference (which per the Diagonal Lemma isn't really much of an issue).

So as to some other foundational theorems, let's start with the "classical" ones - gauging how first-order logic behaves:

• Gödel's Completeness Theorem. Roughly speaking, there are two natural notions of "entailment" in logic: semantic entailment (= "p is true in every structure satisfying the axioms G," LaTeX code "\$G\models p\$") and syntactic entailment (= "there is a formal deduction of p from G," - LaTeX code "\$G\vdash p\$"). In general there's no a priori reason for the two notions to coincide; while it's easy to make sure that G syntactically entails p only if G semantically entails p (just make sure that your proof rules "make sense"), there's no reason to believe a priori that a given proof system fully captures the semantics. Keep in mind that a formal proof is a finite object, but even a finite theory G might not have any computable models. However, Gödel showed that we can in fact find a completely satisfying proof system. This is hugely foundational, as it justifies the value of formal proofs in the first place; to my mind it is also quite surprising - much more so than the incompleteness theorem - especially in light of the difficulty of telling whether a specific structure satisfies a given sentence.

• The (Downward) Löwenheim-Skolem Theorem. Continuing our analysis of first-order logic, the Löwenheim-Skolem theorem gauges the role of set theory in pure logic. There are other more technical results continuing this theme - e.g. the Mostowski and Shoenfield absoluteness theorems, especially in light of the Levy collapse - but this one is where it all starts.

• The Compactness Theorem. This says quite simply that the semantic entailment relation - see above - is "finitary:" if G semantically entails p then H semantically entails p for some finite subset H of G. This is an immediate corollary of the completeness theorem (since proofs can only use finitely many axioms), but doesn't need to be proved this way, and is really important on its own so in my opinion worth mentioning separately.

• Now a lesser-known one. We frequently talk about justifying our axiom system, but we should also care about what distinguishes our underlying logic from other logical systems we could (at least in principle) employ. Lindström's theorem gives a characterization of first-order logic: it is a maximal logic (with respect to expressive power) with the compactness and Löwenheim-Skolem properties. So in some sense first-order logic gives an upper bound for how strong a logical system can be without bringing infinities into the picture in one way or another.

• And finally, another lesser-known one (or pair): the characterization of satisfaction of a sentence in a structure via Skolem functions and of elementary equivalence between structures via the Ehrenfeucht-Fraïsse Theorem. These set the stage for the "game semantics" approach to understanding logic(s). I personally consider this a fundamental aspect of what logic is - structures, proofs, and games - but I recognize this is fairly personal opinion; that said, here's a neat application of proofs-as-games language to algebraic geometry.

OK, what if we look further afield - e.g. from what logic is/can be to sets, computations, ...?

Well, ultimately we run into a question of what "foundational" means. For example, what about results which impact how we think about mathematics in a deep way? The idea of Galois connections, for example, is absolutely fundamental to modern mathematics; is the fundamental theorem of Galois theory therefore fundamental, since it firmly establishes a place for these?

I'll tentatively say "no." With that in mind, here are a couple other theorems I consider foundational, organized by subject:

• Set Theory: Cantor's work established that we can in fact talk about infinite sets in a mathematically coherent way. That's huge in my opinion. Meanwhile, I don't consider hugely important topics like forcing or inner model theory to be truly foundational (although some will disagree with me on this), and I'm not really sold on ZFC as anything more than a convenient historical choice. The only other theorem in set theory I'd consider truly foundational is Russell's paradox: Gödel's incompleteness theorem puts limits on what we can expect from a foundational theory, but Russell established a limit on what mathematical language can treat appropriately. With the example of "naive properties" (and see my comments below this answer for a bit more comment on that), Russell's paradox raises the general question of whether fundamentally self-contradictory ideas can also be meaningful mathematical ideas, and I think that's fascinating.

• Computability Theory: Similarly to the situation with the Completeness Theorem, the existence of a satisfactory (in the general opinion, anyways) formalization of the intuitive notion of computation should be wildly surprising - in the modern world it's not, in light of computers, but that's a shame. Cantor's diagonal argument establishes the existence of non-computable sets, but the unsolvability of the halting problem establishes the existence of interesting ones. Kleene's identification of the T-predicate connects computability with definability in arithmetic - unsurprisingly in light of Gödel's representation of primitive recursive functions, but still important - and while it's not a theorem I think the formal definition of oracle computation (or rather, the existence of such) is also foundational.

• Category theory: I do in fact consider the notion of category (and the attendant concepts - functor, natural transformation, adjunction, universal property, ...) to be truly foundational: they tell us more about what mathematics, as we do it at least, is. That said, I don't know of many theorems that I'd consider foundational (I suspect this is more a "me" problem). The Yoneda lemma is an obvious candidate, but I'm not sure I really consider it "foundational" (see my comments above). Instead I'll go for the non-concreteness of homotopy; I'm not really overwhelmed by the result itself, but the idea that there are limitations to how the universe of sets can capture other mathematical "universes" - however technical - is one which thrills me.

The above surely reveals many biases on my part - but hopefully I've succeeded in painting a "foundational picture" which is, if nothing else, nontrivially interesting.

• The following expands on a now-removed part of this answer, which I've decided wasn't of central importance but still deserves mention: It's worth pointing out just how lethal Russell's paradox was to naive set theory. It's a reasonable instinct to think that we can save naive set theory by passing to a paraconsistent logic (where contradictions are allowed without necessarily trivializing everything). However, this won't actually save us here! This is essentially because we can blend Russell's paradox with Curry's paradox. (cont'd) Mar 12 '19 at 1:51
• Reasoning in naive set theory, let p be any proposition we want to prove. Let X be the set {a: if a is an element of a, then p}. We have "if X is in X, then if X is in X then p" - and this in turn gives "if X is in X, then p." But that implies X is in X, which therefore gives us p. Unwinding this, we get that it's very hard indeed to formulate a version of naive set theory that doesn't explode immediately: contradiction has nothing to do with it, we're getting into trouble at the level of modus ponens itself! So that's why I said "fundamentally self-contradictory" above - it really is! Mar 12 '19 at 1:55
• There are paraconsistent logics that block the Curry paradox explosion, see Meyer-Routley-Dunn, 1979. Your version will be blocked by any relevant logic, since p has nothing to do with X. The trouble is not so much with modus ponens but with its use on the material conditional. "Naive" reasoning does not use it, perhaps explaining why Frege and Cantor overlooked the paradoxes. Mar 13 '19 at 8:05
• @Conifold Sorry, just saw this. Of course you're right, and I was unclear. I didn't mean to say that no paraconsistent logic gets around it, only that the most naive retreat to paraconsistent logic isn't enough. That said, re: "The trouble is not so much with modus ponens but with its use on the material conditional," I would consider trouble with the use of modus ponens on the material conditional to be trouble with modus ponens, but of course that's an aesthetic claim. Apr 8 '19 at 19:31
• We intuitively trust modus ponens based on experience with natural reasoning, which is highly compartmentalized. The material conditional erases the restrictions and universalizes consequence, which is technically handy, but then we do not really have a reason to expect that modus ponens should still work. It is less of a paradox and more of a bait and switch at the heart of many logical paradoxes. I guess you are right about aesthetics, but the blame is usually placed on the contrivance, and not on that which it spoils. Apr 8 '19 at 20:55

One theorem I find to be particularly important is

Topos theory = Set theory = Type theory = Higher order logic

I'm phrasing this a little glibly, of course; each of these have various precise statements and various generalizations.

The reason I find these equivalences to be important, because it tells us vast swaths of different approaches to mathematics that superficially seem profoundly different are, in fact, all basically the same underlying ideas dressed up in different language. Among the consequences are:

• Having different language and perspectives is very useful: each perspective on the foundations clarifies different aspects of mathematics and has its own advantages and disadvantages.
• It unifies a number of things that have been historically divisive, freeing us collectively from having to dwell on them. For example, it demonstrates there is no essential difference between the set-theoretic "completed infinity" of natural numbers isolated from the mathematical universe by the principle of comprehension and the type-theoretic "potential infinity" of natural numbers constructed inductively by starting from zero and applying the successor operations