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

Tue Apr 19 10:26:00 EDT 2016

Dear Dimitris,

Thanks for your response!

I think philosophically I would definitely regard this as a superior way of
> dealing with the problem, at least insofar as you can get a category of
> sets with all the usual properties. Indeed, in some sense I *have* to think
> this is a better option since my own claim that HoTT is able to talk about
> *all* sets in a better way than ZFC relies on assuming that in the larger
> universe U’, SET(U) is treated very differently than the types in the
> universe U.

Exactly. Also, if you allow superplural reference (which is highly
controversial, see [1] and [2]), you end up with something essentially
type-theoretic.

> But I really don’t know enough about what people find objectionable in the
> position that you sketch. Is it mainly that the actual set theory you end
> up using is MK, rather than something that is “natively” plural-logical?

I don't think that this is it. Especially as there are Henkin-style
interpretations of plurals now (see [3]), which would motivate the use of
NBG rather than MK, and to which I think many complaints would still apply.
I think its rather that people think either that there's a collapse of
pluralities to sets (see [4]), or that plural resources can bear a strong
technical similarity to set theory (see [5]). In conversation, some
logicians have said that they ``can't understand the ranges/semantics of
the plural variables without set theory'' or similar. For the reasons in my
previous mail, I find this line unconvincing, but it merits further
scrutiny.

This is a very interesting possibility, if I understand it correctly. But
> I’m not at all clear how one could adapt a plural logic in the MLTT
> setting, e.g. in a way analogous to how FOL is recovered inside MLTT. Is
> this anything that anyone has thought about? More importantly, is this what
> you have in mind?
>

Yes, something like this. As I (poorly) understand HoTT (it's on the to-do
list for stuff I don't understand well but wish I did), there are two
challenges when trying to move to the set-theoretic setting. First, we've
got the problem of how to interpret types (e.g. SET(U)). There's then the
issue of studying these types category-theoretically as particular kinds of
groupoid. Both are going to be difficult to interpret when we want SET(U)
to denote *all* sets. However, you can code *a lot* in MK because of the
impredicativity, and there's at least possibilities that MK can be
interpreted with a proper-class-nominalism with plurals (and lots more if
you allow superplurals, supersuperplurals, etc.). Thus, there are at least
possibilities for a nominalistically acceptable paraphrase of HoTT over the
sets, where it is construed as providing new ways for *talking about the
sets* rather than as about new kinds of non-set-theoretic object (e.g.
proper classes, hyperclasses, n-hyperclasses and so on).

To properly assess the prospects of such a proposal though (both
philosophically and technically), I'd need to understand HoTT well, and I'm
just not there yet. For emphasis: *I'm *not* suggesting that this is how
HoTT practitioners *should* interpret their results, just that it might
provide an option *in addition* to the use of Grothendieck universes,
allowing us to translate HoTT-insight to the set-theoretic setting (and
vice versa).*

Thanks for the intuitive description of HoTT! I'm following it with
interest.

Best Wishes,

Neil

[1] Ben-Yami, Hanoch (2013). Higher‐Level Plurals versus Articulated
Reference, and an Elaboration of Salva Veritate. _Dialectica_ 67 (1):81-102.

[2] Linnebo, Øystein & Nicolas, David (2008). Superplurals in English.
_Analysis_ 68 (299):186–197.

[3] Florio, Salvatore & Linnebo, Øystein (2015). On the Innocence and
Determinacy of Plural Quantification. _Noûs_ 49 (1):1-19.

[4] Linnebo, Øystein (2010). Pluralities and Sets. _Journal of Philosophy_
107 (3):144-164.

[5] Linnebo, Øystein & Rayo, Agustín (2012). Hierarchies Ontological and
Ideological. _Mind_ 121 (482):269 - 308.

On 15 April 2016 at 18:34, Dimitris Tsementzis <dtsement at princeton.edu>
wrote:

> Dear Neil,
>
> 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.
>
>
> I think philosophically I would definitely regard this as a superior way
> of dealing with the problem, at least insofar as you can get a category of
> sets with all the usual properties. Indeed, in some sense I *have* to think
> this is a better option since my own claim that HoTT is able to talk about
> *all* sets in a better way than ZFC relies on assuming that in the larger
> universe U’, SET(U) is treated very differently than the types in the
> universe U. But I really don’t know enough about what people find
> objectionable in the position that you sketch. Is it mainly that the actual
> set theory you end up using is MK, rather than something that is “natively”
> plural-logical?
>
> 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).
>
>
> This is a very interesting possibility, if I understand it correctly. But
> I’m not at all clear how one could adapt a plural logic in the MLTT
> setting, e.g. in a way analogous to how FOL is recovered inside MLTT. Is
> this anything that anyone has thought about? More importantly, is this what
> you have in mind?
>
> Best,
>
> Dimitris
>
>
> On Apr 13, 2016, at 07:34, Neil Barton <bartonna at gmail.com> wrote:
>
> 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
>>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
>
> _______________________________________________
> 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/20160419/2d310add/attachment-0001.html>