>>53In all honesty, there's no "one" theory of mathematics. There's all kinds.
ZFC is the standard. All mathematicians are taught it.
My interest is in type theory. It is a formulation of constructive mathematical logic using a typed lambda calculus..... in other words, it's a functional programming language (like ML or Haskell) in which it becomes possible to do most of mathematics.
The Curry Howard Correspondence tells us that there are deep connections between typed functional programming and logic. The types of objects are propositions. The objects themselves are proofs. A function type is a logical implication. A function is a computable transformation whose inputs and outputs are proofs.
Universal quantification corresponds to polymorphism (generics in C#/Java). Existential quantification corresponds to modularity and abstract types.
Since the logic is constructive, if you say "there exists a Foo such that Bar", it means you actually have an object of type Foo and a proof that that object has property Bar.
Recursion in such languages is restricted to primitive recursion. Primitive recursion corresponds to logical induction.
My favorite correspondence is this one, though: a program that gets stuck in an infinite loop is an indication that the corresponding logic is inconsistent.
Paradoxes don't seem so deep and mysterious. The liar's paradox is just a fast way to get your brain stuck in a loop thinking about it :)
Most programming languages, include ML and Haskell, ARE inconsistent.... It's more practical. Any Turing-complete language is inconsistent. But non-turing-complete languages can still be very powerful.
Above, I linked to homotopy type theory. This is a new development in the last few years of type theory that suggests that there's a deep connection between type theory and homotopy theory.
The most exciting development is Voevodsky's univalence axiom. This axiom essentially means isomorphic types are equal to each other. This would allow mathematicians, for the first time, to formalize a subtle but very common practice: the equating isomorphic objects when it is convenient. (For instance, freely translating between R2 and C when talking about points in the plane).
The other advantage of type theories is that they are much SIMPLER than ZFC. It is an unpopular truth, but the reality is most working mathematicians don't understand ZFC. They pay lipservice to it, but unless it's their area of concentration, no one thinks about writing proofs via the ZFC axioms.
To give some justification, ZFC has 9 axioms. It also (subtly) relies on First-Order logic (whose axioms are many more). The 9 axioms do not seem to have any rhyme or reason to them. They are just a collection of rules that were found out to be enough to do most of what mathematicians wanted to do at the time. It is hard to describe what they are all for in words.
Type Theory, on the other hand, is incredibly simple conceptually. You start off with syntactic terms (basically, a lambda calculus). Then, every kind of object has two axioms: an introduction rule and an elimination rule.
To create a Π type (a universal quantifier or a function), you use a lambda expression (you abstract a term by pulling out a common subexpression). To eliminate it, you use function application (you provide a new value for that subexpression).
To create a Σ type (an existential quantifier or a tuple), you just provide both items in the tuple. To eliminate it, you can project either item.
To create an inductive type (the natural numbers, integers, finite list types, and inductively-defined theorems), you construct a W type. To eliminate it, you use the primitive recursion operator.
To create a coinductive type (the extended naturals with a point at infinity, infinite sequences, the real numbers, the type of a webserver application), you create an M type. To use it, you can unfold it. These correspond to non-well-founded types found in set theories that have an Anti-Foundational Axiom.
To prove two things are equal, you use an equality type. Equality types are introduced through reflexivity (any two definitionally equal things are equal). They can be eliminated through the "J" operator in type theory. The J operator allows you to prove that equality is a congruence, and that it is a symmetric and transitive relation.
Lastly, many type theories have a so-called "tower of universes". As is well-known to anyone who has studied set theory, the notion of a "set of sets" is dangerous. ZFC refuses to let you talk about such a set. But in type theory, it is common to include a type of types, called Type_0, and a type of Type_0 called Type_1, and so on. There are no known paradoxes from this practice as long as you never have any type directly containing itself.
The tower of universes is extremely useful in practice. To a programmer, it theoretically allows for the same kind of metaprogramming found in dynamically-typed langauges in a strongly-typed setting. It is also useful to mathematics, as it is a necessity when formalizing category theory (which is arguably the most important breakthrough in mathematics since Cantor first proposed set theory). Category theory, in case you haven't heard the term, is a very general kind of algebraic structure that can model set theory, logic, and geometric spaces of all kinds. But foundational issues arise, because unlike other algebraic structures (like groups) whose underlying collections are sets, categories often work with collections such as proper classes (which are not actually admissible by ZFC), and even bigger collections.
Type Theory is pretty nifty. It's also really fun to play with. Check out Coq and Agda, two modern proof assistants slash programming languages based on type theory. #agda on irc.freenode.net is especially helpful if you want help with the latter.
