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

[Harvey Friedman]

Reply to Mon, Apr 4, 2016 at 5:22 PM, Dimitris Tsementzis
<dtsement at princeton.edu>
http://www.cs.nyu.edu/pipermail/fom/2016-April/019656.html

Of course you can have a category SET of "all" sets in standard
f.o.m., as long as you do not demand that SET is a set.

I remember talking to some abstract mathematicians who like to simply
handle this with the usual set/class distinction, in the obvious
straightforward manner. this abstract mathematician was an algebraic
topologist with a categorical bent. He never mentioned a need for
something more than that.

Now there is an "issue" if you want the set of all sets, where
everything is a set. Then you have to give up any standard kind of
elementary separation axiom.

Of course, in standard f.o.m., this is closest to the situation with
untyped lambda calculus, where you move to functions, and give up
separation axiom ideas. There are really nice models, which I think go
back to Plotkin and Scott. I can imagine building on top of this work
in elaborate ways, preserving that the functions operate on absolutely
everything.

But as far as general purpose foundations for mathematics is
concerned, which is to be distinguished from other purposes, I do not
see how this is anywhere near worth what one has to give up.

I once played around with a simple type structure where you have a
type N (natural numbers) at the bottom, and the usual N,PN,PPN,...,
but also V,PV,PPV,... . You take some care in presenting the
appropriate comprehension axiom schemes. If I remember right, it is
fairly straightforward to do something demonstrably OK like this, but
nobody was interested. I could think about it again. Once again, I did
not see how, for general purpose foundations for mathematics, this is
anywhere near worth what one has to give up.

In particular, I just do not believe that this "issue" of a universal
object comes anywhere near close to any
kind of reason to overhaul the usual standard f.o.m. that has been so
firmly in place since around 1920.

Far far better to have a robust mental conception largely conceptually
grounded in the familiar
finite but extrapolated from it, where objects are rigidly grounded in
a pictured "reality", and the notions and ways of thinking are
incredibly simple and straightforward, and the logical part is the
universal language for general deductive thought (first order logic
with equality).

I'll change my mind on a dime if I see something comparatively simple, and there
is something specific and compelling that you gain that is far more
specific than what
Dmitiris is suggesting. Just the general idea that there is a
universal object is simply much too amorphous to be a reason. What do
you want to do with a universal object that is so terrific?

Once again, I want to come back to the observation that just about
everybody is on the same page with regard to having to having mutual
interpretations between seriously alternative foundations and standard
foundations. Apparently, these mutual interpretations are pretty much
known now. Such mutual interpretations invariable show the following:

*As far as reasonably concrete mathematical statements, especially
arithmetic statements, there is absolutely no different in provability
whether you use one foundation or another.*

So the serious issue is whether or not our foundations is adequate for
doing what we want to do in the realm of concrete mathematical
investigations. For this, all of the foundations being talked about
are more or less equivalent.

Harvey Friedman