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

*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.

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:

- 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.

**Zermelo-Fraenkel Set Theory (with Choice, and Foundation)**

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$make sense. Consequently, there is no "Julius Caesar Problem", the issue that Frege once raised about abstraction principles. For example,

$x = y$

$\{\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!

Hi Jeff,

ReplyDeleteThanks for another in this series of enlightening and thought-provoking posts on foundations. I have only a niggling complaint about your NBGish formulation of ZFC. This formulation is indeed simple and rather intuitive for the aficianado, but I don't think this is so for non-specialists. This wouldn't matter so much if the post were only

foraficianados but, like a lot of your writing, it is quite accessible and a lot of non-specialists will read it with interest.There are two things in particular that such readers might find confusing: (1) "set" is ineliminable in your formulation of ZFC, (apparently) contradicting the claim that only ∈ and = are primitive (it also leaves the reader to wonder exactly what sorts of things the non-sets might be); and (2) the formulations of Separation and Replacement on this approach are non-schematic, which might frustrate readers who try to identify the two axiom

schemesyou point to.And a quick question: Why do you include identity among among ZFC's primitives when it is nearly always introduced as part of the underlying logical apparatus? (It is also definable in the context of pure ZFC, as you know.)

Looking forward to the next post in the series!

Thanks, Chris!

ReplyDeleteI agree, but didn't want to fuss over the details of the schematic formulation for Separation and Replacement. Of course, in that formulation, I can't use the second-order variables $A$ and $F$, and have to use schemes instead. I'll do a little update pointing to which of the axioms are really covering for schemes.

I agree on the $=$ point too, as we usually treat it as part of FOL, rather than some extra-logical superstructure. But I wanted to make the Austerity point clearer. Also, yes, it's true that $=$ is definable in ZFC, for we have a formula $\phi(x,y)$, lacking $=$, such that,

$ZFC \vdash \forall x \forall y(x = y \leftrightarrow \phi(x,y))$.

(i.e., $\phi(x,y)$ is the formula $\forall z(z \in x \leftrightarrow z \in y)$.)

But some mathematicians want to think of $ZFC$ as an implicit definition, and one needs to be careful; for if one eliminates $=$ from the language, and reformulates as the axioms using $\phi(x,y)$ instead of $x=y$, then the models come out wrong. This is because $=$ is semantically rigid, as it were.

Cheers,

Jeff

Yes, it's definitely tough to express the schematic forms of Separation and Replacement concisely, especially the latter. Perhaps you could preface the axioms by noting that the central lesson of naive comprehension is that the sets satisfying certain expressible conditions don't necessarily constitute a further set but that we can safely treat them as if they form a further sort of "collection". That would at least motivate your introduction of a (convenient but dispensable) special sort of variable for collections in general as well as your use of the apparent primitive

Deleteset. But all this would admittedly require a lot of stage setting not directly relevant to the heart of the post.I like your point about considering identity part of ZFC vis-á-vis Austerity, though, of course, that does require the addition of the usual first-order identity axioms (or their equivalent) to be considered part of ZFC over and above (or maybe under and beneath?) the world shakers.

Best,

-chris

Hi Chris,

DeleteRight - basically, yes. That's why I didn't want to open the whole can of worms here, and the issue of schemes vs. second-order version. One either gets what I've written (intuitively: there are these sets, blah-blah...) or not - but if not, it's all just water-muddying to get into the whole business of schemes, etc., and not really connected to the main issues (austerity, non-circularity, etc.). Also, the issue of naive comprehension scheme is something I want ed to avoid as well, because it doesn't get its "Justification" from Zermelo's conception of the cumulative hierarchy, but rather from the more Fregean/Russelian logical notion of class.

Yes, I admit - on =, I'm trying to have my cake and eat it! (By having = as one of the basic concepts, but not including the identity axioms.) So, strictly, I'd need to add the two identity axioms, then I'd get 12 axioms that shook the world!

Cheers,

Jeff