Foundational theories, their uses, interactions and comparisons?

Until now, I heard that there are some theories for building mathematical objects (or at least it is what it seems to my poor knowledge). Some of these are:

• Set theory;

• Logic;

• Category theory;

• Type Theory;

• Homotopy Type Theory;

• (Perhaps) Lambda calculus;

• Etc.

Until now I know that these seems to be different trials of foundations for mathematical objects, both with it's strong and weak points: I've heard - for example - that type theory allows the computional implementation of mathematical objects, while set theory makes it a little harder.

I've seen some books, for example Goldblatt's Topoi: A categorical analysis of logic - It seems that some of these theories, as in this case Logic and Category theory do interact somehow. I believe that there may be more interaction between them.

I'm looking for some resource about foundational theories, their uses, interactions and comparisons.

• nLab seems like a good place to start. But they have a strong bias towards category theory, type theory and homotopy type theory. Don't be misguided, set theory is the way to go! ;-) – Asaf Karagila Dec 1 '13 at 23:58
• Don't be misguided, set theory is dying and cannot express what is really going on in mathematics (outside set-theory working groups) - category theory is the way to go. ;-) – Martin Brandenburg Dec 2 '13 at 0:28
• *Gets popcorn*. – Git Gud Dec 2 '13 at 0:31
• – Billy Rubina Dec 2 '13 at 3:12
• @Trismegistos That might be a different question that the OP's, because in most cases what set theorists are currently trying to achieve is not closely related to the role of set theory as a possible foundation for "ordinary" mathematics (I would guess that the analogous statement is true for many category theorists as well, but I'm not sure.) – Trevor Wilson Dec 3 '13 at 1:08

1 Answer

This is more like a long comment. The only two major approaches to the foundations that you list are type theory and set theory. Let me explain.

First, make note of a naming convention:

1. the axioms of group theory tell us what it looks like inside a group
2. the axioms of category theory us what it looks like inside a category

etc.

Following this convention, you might think that set theories tell us what it looks like "inside" a set. But they don't (life is awfully boring inside a mere set!). Rather, they tell us something about what the universe of sets looks like. A similar statement can be made in regards to type theory; type theories describe universes of types.

Another important observation is the following. Using [insert your favourite set theory here], we can prove statements about the natural numbers. For example, $\mathrm{ZFC}$ proves that a variety of other formal systems are consistent; or in other words, that there does not exist a natural number $n$ such that so-and-so formal system proves a contradiction in $n$ or fewer steps. Type theories like Martin Lof type theory also have this ability.

On the other hand, neither the group theory axioms nor the category theory axioms tell us very much about the natural numbers. They just have no "foundational power." So I guess I would say that category theory is "ubiquitous" without really being "foundational." Don't be misguided; set theory and category theory solve very different problems. Set theories (and type theories) attempt to discern truth from falsehood, whereas category theory is a conceptual tool; the point is to conceptualize mathematics in a unified way. There's essentially no conflict between the two.

For these reasons and others, the only two major approaches to the foundations that you list are type theory and set theory. (That's not an exhaustive list; another example would be Lawvere's axiomatization of the "category of all categories.") I hope this comment has clarified a few things.

• Maybe you should also mention Mereology as an alternative to conceptualize mathematics in a unified way. See this. – user 170039 Nov 5 '16 at 6:38
• @user170039, I don't know anything about mereology. Perhaps you can write something? – goblin Nov 6 '16 at 2:50