Q:

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.

A:

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.

