Set theory is generally accepted as a better foundation for mathematics than Principia's type theory, but if you wrote all those ZFC proofs with full formality

Set theory is generally accepted as a better foundation for mathematics than Principia's type theory, but if you wrote all those ZFC proofs with full formality they'd be pretty long too. This answer on Math Overflow is pretty indicative. http://mathoverflow.net/questions/14356/bourbakis-epsilon-calculus-notation/31778#31778 http://mathoverflow.net/questions/14356/bourbakis-epsilon-ca... Usually mathematical arguments are relatively informal; every time you use set comprehension notation, for example, you're skipping a few steps in your proof (and note, of course, that the impredicative definitions one can use with it are open to e.g. Russell's paradox, which is why we have axiomatic set theory in the first place).