I just finished what I am confident is the final revision of my paper on the foundations of mathematics. I want to explain here what this is all about. Why do we need a new foundation of mathematics?
ZFC set theory has stood as a fixed eight-axiom foundation of mathematics since the early 1920s. ZFC does does an excellent job of capturing the notion of provability in mathematics. Things not provable in ZFC, such as the continuum hypothesis,the existence of inaccessible cardinals, or the consistency of ZFC, are forever out of the reach of mathematics. As a circumscription of the provable, ZFC suffices.
The problem is that ZFC is untyped. It is a kind of raw assembly language. Mathematics is about “concepts” — groups, fields, vector spaces, manifolds and so on. We want a type system where the types are in correspondence with the naturally occurring concepts. In mathematics every concept (every type) is associated with a notion of isomorphism. We immediately understand what it means for two graphs to be isomorphic. Similarly for groups, fields and topological spaces, and in fact, all mathematical concepts. We need to define what we mean by a concept (a type) in general and what we mean by “isomorphism” at each type. Furthermore, we must prove an abstraction theorem that isomorphic objects are inter-substitutable in well-typed contexts.
We also want to prove “Voldemort’s theorem”. Voldemort’s theorem states that certain objects exist but cannot be named. For example, it is impossible to name any particular point on a circle (unless coordinates are introduced) or any particular node in an abstract complete graph, any particular basis (coordinate system) for an abstract vector space, or any particular isomorphism between a finite dimensional vector space and its dual.
Consider Wigner’s famous statement on the unreasonable effectiveness of mathematics in physics. I feel comfortable paraphrasing this as stating the unreasonable effectiveness of mathematical concepts in physics – the effectiveness of concepts such as manifolds and group representations. Phrased this way, it can be seen as stating the unreasonable effectiveness of type theory in physics. Strange.
The abstraction theorem and Voldemort’s theorem are fundamentally about types and well-typed expressions. These theorems cannot be formulated in classical (untyped) set theory. The notion of canonicality or naturality (Voldemort’s theorem) is traditionally formulated in category theory. But category theory does not provide a grammar of types defining the mathematical concepts. Nor does it give a general definition of the category associated with an arbitrary mathematical concept. It reduces “objects” to “points” where the structure of the points is supposed to be somehow represented by the morphisms. I have always had a distinct dislike for category theory.
I started working on this project about six years ago. I found that defining the semantics of types in a way that the supports the abstraction theorem and Voldemort’s theorem was shockingly difficult (for me at least). About three years ago I became aware of homotopy type theory (HoTT) and Voevodsky’s univalence axiom which establishes a notion of isomorphism and an abstraction theorem within the framework of Martin-Löf type theory. Vladimir Voevodsky is a fields medalist and full professor at IAS who organized a special year at IAS in 2012 on HoTT.
After becoming aware of HoTT I continued to work on Morphoid type theory (MorTT) without studying HoTT. This was perhaps reckless but it is my nature to want to do it myself and then compare my results with other work. In this case it worked out, at least in the sense that MorTT is quite different from HoTT. I quite likely could not have constructed MorTT had I been distracted by HoTT. Those interested in details of MorTT and its relationship to HoTT should see my manuscript.