[FOM] New Umbrella?

[Jay Sulzberger]

On Sun, 26 Oct 2014, Harvey Friedman <hmflogic at gmail.com> wrote:

> I found the recent post of  Jay Sulzberger real progress for the
> discussion. http://www.cs.nyu.edu/pipermail/fom/2014-October/018302.html
>
> The following crucial one line response appearing in his long and
> interesting message is as follows:
>
>> A. Give a completely transparent account of a generally understandable
>> situation where the Standard Umbrella allegedly really breaks down. It
>> is easy to point to some math that few people have studied and simply
>> say "the Standard Umbrella is inadequate" and just leave it at that.
>> That is completely unconvincing. See the recent FOM postings of Freek
>> and Levy on this point. Radicals - please comment on Freek and Levy on
>> this point.I
>
> No.  We are asking different questions.
>
> ***********
>
> Now we are really getting somewhere. What questions are you asking?
> Are they of general intellectual interest?
>
> STRONG THESIS: Whatever questions you are asking are easily answered
> in classical f.o.m. with some finesse.
>
> WEAK THESIS. Whatever questions you are asking can be adequately
> answered in classical f.o.m. with some serious work.
>
> If I can get enough grip on your questions, and they are of general
> intellectual interest, then I likely will try my hand at these Theses.
>
> Harvey Friedman

Last month at the HoTT NYC Reading Group dinner, Gershom Bazerman
reminded me where Gian-Carlo Rota published his good line about
using random variables vs the old way of doing probability.  In
the old way various solid objects of probability theory are
difficult to see, and so, difficult to stand on - the old way,
one is always just swimming.  Thus some theorems and proofs are
hard even to state.  Rota's propaganda for "combinatorial
species" is available at

   http://bergeron.math.uqam.ca/files/2013/11/introductionrota.pdf

Here is the book's BiBTeX supplied by Google:

@book{bergeron1998combinatorial,
    title={Combinatorial Species and Tree-like Structures},
    author={Bergeron, F. and Labelle, G. and Leroux, P.},
    isbn={9780521573238},
    lccn={96046136},
    series={Encyclopedia of Mathematics and its Applications},
    url={http://books.google.com/books?id=83odtWY4eogC},
    year={1998},
    publisher={Cambridge University Press}
}

I think Rota's foreword is good propaganda for HoTT.  I think it
is part of an answer to your challenge.


I think Rota's foreword also, in part, answers Question 4 of
Joe Shipman's post

   http://www.cs.nyu.edu/pipermail/fom/2014-October/018312.html


Paul Levy's post

   http://www.cs.nyu.edu/pipermail/fom/2014-October/018314.html

suggests that one big objective of HoTT may be seen as a theorem
in, indeed, a theory of big species.  The hope is we can survey
all possible connections among Objects in a World, and, perhaps
by E. Beth's theorem on implicit vs explicit definability, show
that if two differently presented objects are cryptomorphic we
can apply a transform of their definitions so that we can see
that the objects are really the same object.  This transform must
be so strong that every statement about one object, presented one
way, with the statement using that object's formal definition, is
transformed into a statement about the other object, using that
second object's formal definition.  Of course everything in sight
must transform, ridiculous word, "naturally".  And everything
here includes arbitrarily high towers of sets upon
sets^W^W^Wtypes upon types.  So, slogan:

   Univalent Foundations seeks to show that every cryptomorphism is
   an identity.


Paul Levy also lays out a defense against one piece of New Crazy
Types propaganda.  The claim is that

   ZFC folk can ask the question "17 is a member of N, the natural
   numbers.  Is 17 the vertex algebra for the Monster group?".

Of course we do not, indeed cannot, ask this question.
Paul Levy's answer is:

   In traditional foundations, one can construct an endofunction
   on the universe of sets that is not functorial on bijections.  For
   example: the function that sends {{}} to itself and every other set to
   the empty set.  Such a function is sometimes described as "evil",
   in the sense that the two singleton sets {{}} and {{{}}}, differing only
   in their implementation, are treated in different ways.

   In ordinary mathematical practice, including category theory, we rarely
   (I hesitate to say "never") consider such functions.  The things that we
   do to sets are usually independent of their particular implementation.

   That means that mathematicians usually work in a special fragment of
   traditional set theory in which it's impossible to define functions such
   as the above function.  To date, this fragment has not been precisely
   defined (I think).

So we see that already, before we ever heard of HoTT, we operate
using a type theory which rules out the claimed possible question
about 17 vs the vertex algebra.  An example of this false pro
HoTT propaganda appears on page 30 of the HoTT book, where it is
said that in set theory when we say "17 is a member of N." we
really mean a specific set N in the ZFC World.  Of course we do
not.  We mean N, no "implementation" required.  Now, of course,
the fact that we immediately recognize the question about 17 vs
the vertex algebra as nonsense is a better argument for taking
types seriously that the strawman argument proffered.


And I see that in this post

   http://www.cs.nyu.edu/pipermail/fom/2014-October/018325.html

Joes Shipman has addressed some of the confusions behind the
false propaganda claim.

oo--JS.


PS. The version of the HoTT book referred to above is at
http://hottheory.files.wordpress.com/2013/03/hott-online-611-ga1a258c.pdf