What are the other foundations of math?

Question

I know there are at least three foundations of math:

1. Zermelo-Frankel set theory. (Sp?)
2. ECTS
3. Category theory

Are there any others? Experimental foundations are welcome.

Answer 1

NF(U). We don't know yet, but Randall Holmes claims, that NF is consistent relative to ZFC. NFU is consistent relative to ZFC (and even BZC). But the category of NF sets is not a topos, so it's weird.

There are all sorts of variants of material set theory, some with non-classical logics, some permitting proper classes:

• BZ(C)
• IZF
• CZF
• NBG(C)
• MK
• IST
• ...

There is also the structural set theory SEAR, devised by Mike Shulman as an example of structural sets not axiomatised by properties of the category they define.

One could also just take a dependent type theory, such as Martin-Löf Type Theory (MLTT, but properly there are historical variants).

CCAF (Category of Categories As Foundation) was proposed by Lawvere, but didn't really take off. See discussion at this MathOverflow question as to how it could be improved.

Answer 2

Univalent Foundations, using Homotopy Type Theory, is another.

(More generally, I like this quote by John Baez: "[M]y opinion is mainly that people should try all sorts of foundations and see what happens.")