[FOM] Challenge addressed by HoTT/UF that is not addressed by ZFC

[Harvey Friedman]

On Fri, Apr 8, 2016 at 7:47 PM, Dimitris Tsementzis
<dtsement at princeton.edu> wrote:

> I never doubted that there are such work-arounds. My contention is that they are not as satisfactory as what you can do in HoTT (with respect to this issue). All of the methods above involve “large” and “small” sets in one form or another. So there will be sets that you are leaving out when defining SET. In HoTT this doesn’t happen. This is to be expected, because in HoTT not all its basic objects are sets. The basic objects are homotopy types. This allows you to easily talk about all sets, since not all homotopy types are sets.
>
> There is absolutely nothing complicated going on here other than the natural evolution of ideas. Set theory gave a foundation to mathematics. Mathematics also advanced because of set theory. Sets thus became objects of study of actual day-to-day mathematics, rather than just ways to formalize mathematics. So now we need natural foundations which can talk of *all* sets as if they were just one more among many (non-
primitive) mathematical structures. HoTT provides one such way.

I'm not sure that this is what you mean. In class theory, we can talk
of all sets, as if they were just one more among many mathematical
structures. Namely, in class theory, we have a thing called the class
of all sets. This is just one more among many mathematical structures
called classes.

The objection to what I am saying is that, yes, the class of all sets
is just one among a more general kind of object, namely classes. But
it is highly preferred. It is the largest one under inclusion.

So we fix this by having an even more general concept of mathematical
structure. Namely superclasses. Now the the sets altogether now form a
tiny special structure among the much greater and all encompassing
structures, namely the superclasses. The intended model reflected by
this is (V(lambda), V(kappa), epsilon), where lambda is much larger
than kappa. The sets are the elements of V(kappa), and the
superclasses are the elements of V(lambda).

Now you may complain that superclasses are behaving too much like
sets, even though there are transcendentally more of them.

So now we can do this easy thing. Instead of the universe consisting
of superclasses, the universe can consist of superrelations of several
variables. Then the usual (V,epsilon) from regular set theory just
becomes a tiny binary relation epsilon whose field is this tiny V, all
within the gigantic aggregate of superrelations.

>From what you say, I don't see any difference conceptually between the
above and many many variants of the above, and what you describe with
HoTT.

This is in addition to my objection of "so what?", that philosophical
coherence and interpretability is what really matters, and on either
count ZFC is just perfect as it is.

Friedman:

>> The natural question from the point of view of general purpose
>> foundations for mathematics, is just where in the Undergrad Math
>> Courses at Princeton,
>> https://www.math.princeton.edu/undergraduate/courses one should or
>> could naturally take advantage of this feature?
>
Tsementzis:

> Very few, of course. But I don’t see how that’s relevant. After all, both HoTT and ZFC will coincide for all practical purposes for the vast majority of these courses. As you have emphasized time and time again (and I agree): with respect to concrete mathematics (e.g. the kind taught in most of these courses) all that matters is bi-interpretability of foundations. In all other respects it is a virtue for foundations to remain invisible, to stay in the background.
>
> As such, foundations (whether HoTT or ZFC) will remain invisible for the vast majority of these courses, and that’s the way it should be. In some of these courses (e.g. Algebraic Geometry) foundations become visible when you have to consider, say, large categories. Instructors will usually say something like “We assume here that we are given a universe of small sets, there are several ways to do this etc.” and then carry on as usual. With HoTT, foundations would not need to become visible even in such cases, since we would rest assured that sets are merely one of many structures on our basic objects, and there is no reason to worry about “size". Thus, with respect to this ISSUE, HoTT provides an incremental improvement: increased invisibility.

Given what I wrote above, I am not sure that we have increased
invisibility. Also you would have increased visibility if you have to
present something really subtle like two kinds of equality. There is
nothing more visible to an undergraduate even at Princeton than
something subtle out of nowhere.

By the way, I should mention that Grothendieck universes, like
V(theta) where theta is a strongly inaccessible cardinal, is
technically speaking used in the proof of FLT. But insiders I talked
to laughed at the very idea that something like that was more than a
mere convenience, and in no way reflected what is really going on.
When I pressed insiders as to why the proof was not rewritten to
reflect what was really going on, they scoffed that this was silly
busywork because anybody who was anybody knew this. Well I think that
McLarty has cleared this up very well, and went further, going well
beyond mere busywork, with getting clear how this fits into the
cumulative hierarchy safely below V(omega + omega). So as an outsider,
I would like to question whether real top players really want to get
involved in any complicated abstract nonsense in the first place, let
alone introduce it into the Princeton Undergraduate Mathematics
Curriculum.

Let me put this differently. Isn't it advantageous to simply layer
some new kind of abstract nonsense on top of roughly ZFC? Do you
really want to claim that the abstract nonsense has some genuine
independent status?

Claiming that it has some genuine independent status is obviously
enticing, but the standards for making that remotely compelling
requires at the very minimum, a philosophically coherent presentation
that makes easy sense to everybody, like the standard f.o.m.

Now I am totally open to listening to a philosophically coherent
account of some new notions that are allegedly more fundamental than
sets. I try to do this all the time, e.g., with flat mental pictures
and conservative growth. I try to do this every day. But I know the
weaknesses, and am not ready to claim a new foundation that is more
fundamental than the usual. I know my humble place in the history of
great ideas (actually I don't). I respect the standards for doing
something like this.

Are you prepared to present a philosophically coherent account of some
genuinely new notions that are more fundamental than sets, and provide
a new foundation for mathematics? I try to do this, but I am not ready
to make grandiose claims that I have.

Let's see what you've got. Maybe it's closer to my flat mental
pictures and conservative growth than one would think.

Harvey Friedman