Ten Axioms That Shook the World

(No prizes for guessing the political joke in the title!)

The central claim made in relation with HoTT is its comparison with ZFC set theory as an alternative foundation for mathematics. I'm interested in this comparison. A few days ago, I posted a quick suggestion of five adequacy criteria for comparing foundational systems for mathematics. These are:

• Austerity
• Non-Circularity
• Justification
• Interpretation Strength
• Structural Invariance

The axiom system ZFC scores highly on these, except the final one, Structural Invariance. How HoTT does is not clear to me at the moment, but I'm really interested to learn more. (There have been some useful comments on this by François Dorais below the post.)

But I'm not so interested in the whole "Set Theory vs. Category Theory" shouting match! (Cf.,  Einstein's comment on the row between Hilbert and Brouwer, calling it the Frog-Mouse battle.) I'd like to get an idea about how these foundational approaches compare, and fit with, say,

• mathematical practice
• philosophical questions (i.e., ontology & epistemology)
• mathematics education
• application of mathematics in science.

And it would be nice to invoke, if possible, mathematical notions for the comparison. For example, consistency/interpretability strength.

Let me explain why $ZFC$ does so well. A simplified (but hopefully not misleading) formulation of the "Ten Axioms That Shook the World" of the title:

Zermelo-Fraenkel Set Theory (with Choice, and Foundation)
• If $\forall z(z \in x \leftrightarrow z \in y)$, then $x = y$.
• $\varnothing$ is a set.
• If $x, y$ are sets, then $\{x,y\}$ is a set.
• If $x$ is a set, then $\bigcup x$ is a set.
• If $x$ is a set, then $\mathcal{P}(x)$ is a set.
• If $x$ is a set, then $A \cap x$ is a set.
• There is an inductive set.
• If $x$ is a set of non-empty sets, then there is a choice function $f$ on $x$.
• If $x$ is a non-empty set, then there is an element $y \in x$ disjoint from $x$.
• If $x$ is a set and $F : x \to y$, then $y$ is a set.

(As aficionados know, this is a kind of "second-order" formulation, resembling $NBG$, which is conservative over $ZFC$. But it makes the content more intuitive.)

This foundational theory contains 10 axioms (well, strictly speaking, 8, with 2 axiom schemes) and is conceptually Austere. It has $\in$ and $=$ as its basic concepts, and is formulated in classical first-order logic. There is no "typing" at all. There is a single variable sort, and statements of the form:

$x \in y$
$x = y$

make sense. Consequently, there is no "Julius Caesar Problem", the issue that Frege once raised about abstraction principles. For example,

$\{\varnothing\} \neq V_{\omega}$. 

etc.

This foundational theory is conceptually Non-Circular. We don't cheat by putting numbers, integers, rational, real numbers, cardinals, ordinals, etc., in by hand. We define these structures and prove their existence (well, the existence of an "implementation", typically non-unique: I come back to this below).

This foundational theory has an intuitive epistemic Justification. One can picture, perhaps even "grasp" the cumulative hierarchy, as growing transfinite tower of "ranks", starting with $\varnothing$ and iterating the application of $\mathcal{P}$. Of course, this might not convince you that there is such an intended universe of sets.

This foundational theory has very high Interpretability Strength. It interprets pretty much everything any mathematician has ever written down. And for stuff it doesn't, it can, by either going to impredicative second-order theory, or by adding large cardinals.

However, $ZFC$'s weakness concerns its "implementation" of all the various mathematical objects, thingies, patterns, structures, and beasties that mathematicians know and love. The pairs, relations, functions, numbers, groups, spaces, and so on. One can interpret, or model, pairs, relations, functions, numbers, etc., in $ZFC$. But the modelling is always non-unique. There are lots of extensionally different implementations, rather like gauge choices or co-ordinate systems in physics. And it offends the mathematician's Platonic sensibilities to have lots of different "implementations" of the natural numbers, when one would really like to identify one single system: the natural numbers.

In short, $ZFC$ violates Structural Invariance. People have begun to say (the term derives from remarks by Harvey Friedman) that $ZFC$ is a "material set theory", which is contrasted with "Structural Set Theory", which is what we have in the category version of set theory, Lawvere's Elementary Theory of the Category of Sets (ETCS: relatedly, see this post "Rethinking Set Theory", by Tom Leinster), and also, I assume, in HoTT too.

To be continued!