# What does it mean to say that a particular mathematical theory is a foundation for mathematics?

We usually hear that set theory is a foundation for contemporary mathematics. Category theory is also another foundation of maths. There are other theories which deemed to be a foundation for maths.

Question 1: What does it mean to say a particular theory is a foundation of contemporary maths, "precisely"?

Question 2: In some cases people say, set theory is a foundation for almost all parts of modern mathematics. Why almost not all? Is there any mathematical concept or field that is not known to be expressible in terms of set theoretic axioms?

Question 3: Is it possible that a particular theory be a foundation of contemporary maths but not a foundation for mathematics in future? If yes, how is it possible?

Question 4: Is it meaningful to compare two foundations of maths and conclude that one of them is better, more useful or more fundamental than the other? If yes, how? and what can we say about the case of set theory and category theory?

• The main problem of set theory is ontology. That's why people want a more natural way of thinking about the objects treated in math (for instance, homotopy type theory). Furthermore, there is no universe in set theory. Nov 20, 2014 at 9:28
• @user40276, no universe in ZFC. Other set theories have universe. Nov 20, 2014 at 9:35
• @user40276 Regarding Martín's comment please see Quine's New Foundation set theory, NF.
– user180918
Nov 20, 2014 at 9:38
• I recently followed an interesting thread by the Univalent foundation program "developers", where they have some communication trouble over foundations being interpreted as tool with which we develop and implement other mathematical frameworks vs. framework which we use to judge other frameworks, demonstrate consistency etc.. I think the second question is technical in nature and the third and fourth crumble over the fuzziness which comes with the first. I'm going to be so bold and say that there will not be a best one - there's always place for improvement to this and that application. Nov 20, 2014 at 9:43
• @Martín-BlasPérezPinilla Yes, I know. I was assuming $text{ZF}$. Nov 20, 2014 at 9:48

That's an interesting question!

For sure there is not the answer, and I guess my opinion will also change (and hopefully, at some point, converge) during through forthcoming discussions and other answers, but here's a first try which fits with my experience.

Proposal for the definition of foundational system:

The underlying datum of a foundational system should include the following:

• A collection of syntactic entities (e.g. formulas, proof trees) and relations between them (e.g. well-formedness of formulas or proof trees).
• Translations from mathematical concepts (e.g. objects, statements, proofs) into syntactic objects and from judgements about them (e.g. "Proposition $A$ is provable" or "$P$ proves proposition $A$"") into statements about relations between the associated syntactic objects.

This datum should ideally be

• sufficiently expressive: All mathematical concepts, ideas and judgements should have a translation.

• sufficiently meaningful: 'Most' of what can be expressed through the system in terms of the syntactic entities and their relations should have an intuitive meaning, and translation should preserve that meaning.

The last part of the second conditions rules out trivial "foundational systems" with constant translations.

Examples

1) (ZFC) Set theory. This seems to mostly satisfy the expressiveness condition, but not the property of being sufficiently meaningful:

• Sufficiently expressive: To my knowledge, ZFC is sufficiently expressive to allow for the formalization of all mathematics which is in no need of treating classes as first-'class' objects. Category theory however can only be treated on the level of metatheorems, replacing statements like 'For every category ${\mathcal C}$ ...' by a meta-theoretical quantification over FOL formulas in one free variables satisfying the axioms of a category. This has a remedy by considering ZFC + U(niverses). I never encountered some idea or concept I would have liked to formalize but couldn't in ZFC + U.

This addresses also your second and third question. It is also conceivable that at some point it will become common to add even stronger set theoretic statements to the standard set of axioms. For example, there is Vopenka's principle having very pleasant categorical consequences (see http://ncatlab.org/nlab/show/Vop%C4%9Bnka%27s+principle).

• Sufficiently meaningful: In my opinion, not at all: For example, you can ask the ill-posed question as to what the intersection of two arbitrary sets is. For example: what is the intersection of $\text{sin}$ and $\pi$? Sure, intuitively this is nonsense, but nevertheless we can ask and even answer this, provided we settled on some explicit construction of the reals.

2) Category Theoretical foundations, for example Lawvere's [E]lementary [T]heory of the [C]ategory of [S]ets, corrects, in my opinion, the latter deficiency of set theory: For example, it is not imposed that any two sets have something to do with each other; instead we may only form their intersection ( in the form of a pullback) provided they both come equipped with a monomorphism into some common third object. I'm not sure but concerning the expressiveness I think ETCS + Universes is as expressive as ZFC.

However, as I'm writing this, I get aware that despite the above suggests that ETCS meets the proposed requirements of a foundational system better than ZFC does, I still tend to think in ZFC instead of ETCS. Apart from habit, that might be because translation of concepts into ETCS is sometimes not as straightforward as it is in ZFC, so maybe this should be a criterion as well?

Please don't get me wrong - I'm not at all meaning to downgrade ZFC with the above, but I only want to note that its expressive power and flexibility comes at the cost of the presence of meaningless statements as well.

• +1. I prefer working in ETCS instead of ZFC, even if not explicitly, since basically you may use the same language, but only that nonsense-stuff (intersections of two arbitrary sets, for example) disappears :). Nov 20, 2014 at 11:49
• Those statements aren’t meaningless; they just aren’t at all interesting. Nov 20, 2014 at 19:41
• I completely agree with the "Sufficiently meaningful" section. The exact same thought has always been at the back of my mind, thanks for allowing me to fully acknowledge it consciously :-) Nov 21, 2014 at 14:30
• If I recall correctly, $\sf ETCS$ is equivalent to $\sf ZC$, rather than $\sf ZFC$. So $\sf ETCS$ per se is weaker. I'm not 100% sure what happens when you add universes to $\sf ETCS$, though. Nov 21, 2014 at 15:45

There is probably not one definition of "foundation" that everybody will agree on. However, there is an answer to the question why set theory lies at the foundation of all of mathematics:

Set theory is an extension of propositional logic, the framework of strict reasoning implicitly underlying everything mathematicians do. Let $P$ and $Q$ be propositions, and let $A$ and $B$ be the sets of entities for which propositions $P$ and $Q$ hold. One can now put all boolean operations on $P,Q$ in direct correspondence with set operations on $A,B$, for example

$$P∨ Q\quad\leftrightarrow\quad A∪B$$

$$P∧ Q\quad\leftrightarrow\quad A∩B$$

$$¬ P\quad\leftrightarrow\quad \overline A$$

etc.

The key advantage of the set-theoretic formulation of logic is that its elements (sets) can be objects that are of mathematical interest anyway, such as numbers. Thus set theory blurs the distinction between object of study and method of study and provides a natural foundation for such branches of mathematics as algebra, probability theory and topology.

• It rains. What is the set underlying that proposition? Is set theory the framework underlying question of computational complexity of different sorting algorithms. Also, what is the action of a group element, really? Nov 20, 2014 at 9:54
• The semantics of a proposition, such as "It rains", are not subject to the methods of standard propositional logic either. You can of course take the set of all days where it rains, but this set will not tell you any more about whether a statement about rain is actually true than boolean algebra will, unless for example you have another set of "days with dry streets" and know their intersection is empty.
– user139000
Nov 20, 2014 at 10:06