What are the leading alternative foundations for mathematics?

I know that all of mathematics can be recast in terms of set theory. There are multiple choices for this set theory (some form of ZFC, NBG, NF, etc.), and so multiple possible set theoretic foundations for mathematics.

I am told (though I know so little about the subject that I cannot verify) that category theory also provides us with a foundation for mathematics.

What are the other well-known candidates for the foundations of mathematics, if any?

• I realize I am probably being a bit vague in my statements. If there are important qualifications needed, please point them out. – Dennis Nov 10 '14 at 4:33

There is much to be said about any of the foundational systems below, so the following is necessarily only a very rough sketch on their main ideas and differences.

The category theoretic foundation you where told about is probably Lawvere's Elementary Theory of the Category of Sets (ETCS). Like classical set theory, it is a first order theory, but the basic concepts/ideas it builds upon are those of an object/set and a morphism between such, instead of sets and elements of sets as in classical set theory.

For example, see http://ncatlab.org/nlab/show/ETCS and http://ncatlab.org/nlab/show/Trimble+on+ETCS+I A nice introduction to elementary toposes, of which ETCS is the first-order axiomatization, is given in Maclane-Moerdijk, Sheaves in Geometry and Logic

Note, however, that like in classical set theory, we have a clear separation between the underlying logic and the theory build upon of it.

In type theory, this distinction is blurred: you are dealing with syntactic entities of types and terms, which may either be thought of as the domains of discourse and their elements, or as propositions about these and their proofs. Together with decidability of judgements "This term belongs to that type" which can be (and has been) implemented on a computer, this gives rise to a proof-sensitive and machine-checkable (and even machine-assisted) foundational formal system suitable for the formalization of both classical and intuitionistic reasoning in both first-order and higher-order logic.

For example, see http://ncatlab.org/nlab/show/type+theory and the references therein. In particular, you might want to have a look at homotopy type theory http://ncatlab.org/nlab/show/homotopy+type+theory, a type theoretic foundation of mathematics under development building on the concepts of space and homotopy as the basic concepts.

Besides ZFC, I find the work of Brian Rotman interesting: A more behaviouristic, linguistic, physical approach:

"Mathematics as Sign"

Writing, Imagining, Counting http://www.sup.org/books/title/?id=415