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

Wed Apr 13 07:34:54 EDT 2016

Dear Dimitris,

Thanks for your very nice comments on HoTT; I'm learning a lot just by
sitting in on the conversation.

As a non-expert in HoTT, I can't really comment on what's been said
regarding intuitive justifications. However, an issue that has repeatedly
popped up is the philosophical implications of providing an interpretation
of SET(U) within set theory by adding a Grothendieck universe.

In response to Ben, you proposed the following dilemma that you hold HoTT
threads but set-theoretic foundations do not:

 In HoTT one can collect all sets together (in a suitable sense) in such a
> way that one is neither (1) collecting *all* one's basic objects together,
> nor (2) defining a “larger” set.

I have little to say on (1). However, Harvey, I believe, raised the point
that we could be using proper classes to `collect together' all sets. You
rightly pointed out that these proper classes are just `collections'
`larger' than any sets, and that's pretty philosophically puzzling.

There is a different method. Instead of defining a new kind of collection,
we could be talking about sets in a different way. Uzquiano, building on
work of Boolos, showed that you can provide an interpretation of MK in
plural logic, where we refer to sets in the plural to mimic class talk.

Some people don't like this interpretation, as they feel that it is
parasitic on set theory (I do not find this objection compelling; plural
locutions were part of natural language a long time before set theory was
even discovered). However, we should bear in mind that just because one can
*use a theory* or *provide an interpretation*, one does not have to
countenance that the terms of the theory are ontologically transparent, in
that any use of first-order quantifiers (as in MK) corresponds to the
existence of singular objects.

How this fits in to the discussion of HoTT I don't know. But it seems open
to me that, when using the language of HoTT [footnote 1], we might construe
the use of the term SET(U) through plural reference to all the sets (as
well as to Grothendieck universes of the required kind).

[footnote 1] I'm very sympathetic to the claim that we should adopt a
pluralism towards the foundational language we use. Something that this
discussion seems to have brought out (for example, in Lasse's clear mail),
is that different foundational languages are appropriate for different
purposes. The challenge then is to find the best way for the foundations to
talk to one another, and what each tells us about the other.

Very Best,

Neil

On 12 April 2016 at 04:21, Dimitris Tsementzis <dtsement at princeton.edu>
wrote:

> > 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?
>
> For me, the two questions are independent. Pragmatically, it is definitely
> advantageous to layer HoTT on top of ZFC if only to have some assurance of
> its consistency. But philosophically, the basic notions of HoTT in my
> opinion also have genuine independence from the Cantorial notions
> associated with ZFC.
>
> > 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 think these two sentences give me a lot more insight into your position.
> You seem to regard alternative f.o.m. as a challenge to standard f.o.m.
> only if it can prove that it is based on *more* fundamental notions than
> those associated with standard f.o.m. (sets, membership etc.)
>
> After hundreds of comments on all these forums, I don’t think I’ve seen
> you make this position explicit or, if you have, I have not seen your
> interlocutors acknowledge it — assuming that it is indeed the position you
> hold. Perhaps doing so would help the discussion? Let me ask the question
> clearly: Do you consider alternative f.o.m. worthy of consideration only if
> it can prove that it is based on *more* fundamental (and philosophically
> coherent) notions than standard f.o.m.?
>
> I am almost certain that no-one will claim that the notions on which HoTT
> is based are *more* fundamental than those on which set theory is based,
> insofar as it is even intelligible what “more fundamental" would mean.
> Arguably, HoTT is based on notions that are equally (or “comparably”)
> fundamental than those of standard f.o.m. I take it that you are not
> convinced of this either — or at least that you are not convinced that they
> are philosophically coherent. But it presents at least prima facie a more
> plausible thesis.
>
> So the question is: Are you willing to consider alternative f.o.m based on
> notions of comparable fundamentality to those of standard f.o.m. if they
> can be argued to be philosophically coherent?
>
> > 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?
>
>
> As I’ve just written: More fundamental, no. Philosophically coherent and
> possibly just as fundamental as sets, yes.
>
> To be more precise, I can give you an account of the new foundations using
> seven basic notions: shape, point, symmetry, observation, juxtaposition,
> amalgamation, path. These are the notions I used to convince myself that I
> could justify the rules of HoTT without resorting to to set-theoretic
> topology. (Resorting to set-theoretic topology seems to me clearly the
> wrong way to go for an *intuitive* justification of the rules of HoTT.
> Rather, it is the way to go for a *formal* justification, i.e. for relative
> consistency results.) Anyway I am prepared to do that — and in any case, as
> I have mentioned to you, I believe such an account is possible, even if I
> have not found the clearest way to do it.
>
> Dimitris
>
>
>
> > On Apr 8, 2016, at 23:53, Harvey Friedman <hmflogic at gmail.com> wrote:
> >
> > 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
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160413/14a5af28/attachment-0001.html>