[FOM] Friedman/Baez

[Harvey Friedman]

More from https://plus.google.com/110536551627130071099/posts/6TiKLxjSCnu

BAEZ:

Friedman wrote:

"We are still, I think, largely talking about 'fundamental
psychological changes" in a tiny number of elite mathematicians in a
tiny number of esoteric mathematical specialities."

It's fun to see someone working on large cardinal axioms coming out
against "elite" mathematicians in "esoteric" specialities.  :-)

But it really goes to show, yet again, that we live in different
mathematical universes.   Not to engage you in your battle, but just
to explain where I'm coming from, let me say a bit about my world.

As a student, as soon as I'd learned the basics I wanted to understand
post-1950's work on topology, geometry, algebra and analysis.  I was a
mathematical physicist myself, and I did my PhD thesis on quantum
field theory - but still, I wanted to know what was going on in math.
I'm talking about in the 1980s and 1990s, when I was a grad student
and then a postdoc.

Naturally, I wanted to understand the work of the most visionary and
influential living mathematicians. These would include - but of course
not be limited to - Grothendieck, Serre, Quillen, Connes, Atiyah,
Singer, Segal and Witten.  I could keep listing names, but those were
some of my faves.

So, I spent a lot of time learning what these people did - not, of
course, mastering it all, but certainly trying to understand the basic
concepts, like schemes, sheaves, spectra, homotopy types, operads, Lie
algebras, Hopf algebras, von Neumann algebras, conformal field
theories, topological quantum field theories, and so on.   At school,
if you didn't know that these things were, you'd feel sort of "out of
it".

I eventually got a job at UC Riverside and left the hotbed of "elite,
esoteric" Ivy League mathematics.  This gave me time to ponder things
on my own.  It eventually became clear that n-categories connect and
explain whole lot of what's going on in the work I've just been
vaguely alluding to.   What at first seemed like a huge pile of
disparate topics started fitting together into something very nice!
Manin gives a nice explanation of the key idea, but there's more to
it.

I was lucky enough to realize this just a bit before a big crowd of
other people realized it and rushed in.  At that point things became
very competitive.  I left and started doing other things.

Some of this big crowd of "elite, esoteric" mathematicians are now
working on homotopy type theory.  But in fact most of them are
pursuing the vision Manin explained using other methodologies.

FRIEDMAN:

You are not being sensitize to a some major aspects of true
foundations. I discuss some of them below as 1-3. In fact, I believe
that you are deeply interested in all three of these, within 15
minutes of absorbing what they are.

1. Among the greatest mathematical events of all time (different than
greatest mathematics of all time) are results of the form

this or that mathematical question cannot be proved or refuted using
accepted mathematical standards for rigorous proofs

Now how are we going to establish such spectacular results?

We need a general purpose foundation for mathematics where
mathematicians readily see that ANYTHING that is done throughout the
whole of rigorous mathematics is OBVIOUSLY incorporated in that
general purpose foundation for mathematics.

So you talk of "entrances" rather than "foundations". But with a mere
entrance, you don't know that you can go everywhere.

In this message I will stick to only examples due to Goedel and Cohen.
But there are many others.

So you want to prove that CH cannot be proved or refuted in
mathematics. How are you going to even formulate this properly?

That some formal system does not prove or refute CH.

But what formal system? Are you going to pick some exotic type theory
or are you going to pick ZFC?

You simply cannot use exotic type theories for this purpose. It is
totally unconvincing for this purpose.

So you want to refute Hilbert's ambition, and show that the
consistency of mathematics cannot be proved within mathematics. How do
you formulate that result? If you use exotic type theories, you don't
get anywhere. The consistency statement does not correspond to
"mathematics is consistent". And the unprovability proof doesn't
correspond to unprovability in mathematics.

Your entrances are entirely worthless for these purposes.

Now you might say that if you have a statement in exotic topology, or
whatever, you might want to prove that it cannot be proved or refuted
in mathematics.

But then you can't say that in exotic type theory. Instead you need to
formulate this as a result over ZFC, and now you are having to
directly consider the set theoretic based formulation of the exotic
type theory statement.

So for a major purpose of general purpose foundations for mathematics,
your alternative "entrances" appear to be worthless.

2. Philosophical coherence and Consistency.

We want to feel secure that the general purpose foundations for
mathematics is free of contradiction. Otherwise, it is prima facie
completely worthless.

The only way we have to establish that a system is consistent is to
either give a web of philosophical coherence and robustness, or reduce
the consistency problem to that of another system which is regarded as
consistent on the basis of a web of philosophical coherence and
robustness.

At the moment, noone has presented such a web of philosophical
coherence and robustness for exotic types. For some of them, I gather,
one has reduced the consistency problem to ZFC. Otherwise, almost
noone would be confident of the consistency. I'm sure some strange
thinkers would differ with that, but they really have to make an
argument, and this has not been done. Furthermore, I suspect a lot of
brittleness in exotic type theories - if you do things slightly
differently - but conceptually pretty indistinguishable - then you
cannot tell in advance whether it collapses in inconsistency. So
that's why people like to reduce the consistency of exotic type
theories to that of ZFC.

But note even on this reduction, which is actually an interpretation,
ZFC is the boss and exotic type theory is the slave. That is the way
it should and even must be until there is philosophical coherence that
has been presented, argued and digested. See
http://www.cs.nyu.edu/pipermail/fom/2016-April/019707.html

3. Spectacular findings

Standard f.o.m. has spectacular findings, many of which are in the
realm of so called conservative extension results. E.g.,

any first order statement in the ring of integers that can be proved
in mathematics using the continuum hypothesis can be proved in
mathematics

any first order statement in the ring of integers that can be proved
in mathematics can be proved without any use of the axiom of choice

How do you state such results with your "entrances"?

The above is true for sentences of much greater complexity than first
order statements in the ring of integers. In fact,

"any second order statement in the ring of integers that can be proved
in mathematics using the continuum hypothesis can be proved in
mathematics*

There are a whole series of such results that generally bring in
complexity considerations, again natural from the ZFC point of view,
but prima facie opaque from the exotic type theory point of view. 

FRIEDMAN

Baez:

It's fun to see someone working on large cardinal axioms coming out
against "elite" mathematicians in "esoteric" specialities.  :-)

Friedman:

I do not work on large cardinal axioms in anything like the sense that
you probably mean.

I work on Incompleteness from all of mathematics. It turns out that
for this work, in order to establish the results, I provably MUST
bring in large cardinal hypotheses. This is out of necessity.

CONJECTURE. No revolutionary progress can be made on Incompleteness
without bringing in large cardinal hypotheses.

AND, since I MUST bring these large cardinal hypotheses into the
picture, I then MUST confront the challenges that they create, both
mathematically and philosophically. That is, I MUST confront the issue
of whether they are consistent, or explore reasons to believe that
they are consistent.

Whenever I do anything, I do it for a well defined definite
philosophically coherent purpose. EXCEPTION: I eat food for other
reasons.

Baez:

What at first seemed like a huge pile of disparate topics started
fitting together into something very nice!

Friedman:

Sounds like a nice framework, not a general purpose foundation for
mathematics with features such as in my message of 5:45PM here. 

BAEZ:

+Harvey Friedman wrote: "Your entrances are entirely worthless for
these purposes."

It's the responsibility of anyone who wants to use a particular
entrance to make sure it connects, via passageways, to the places they
want to go.

So, anyone who wants to use the classical results of mathematical
logic will want to enter a door that connects to the well-trodden
paths in this subject... or build a new passage that connects to these
paths.

And indeed, the precise connection between ETCS and ZFC is
well-understood.   So, it's just a matter of taste which of those
entrances one uses.

HoTT is much newer, so I don't personally know its precise connection
to ZFC.  Earlier in this thread Mike Shulman described the state of
the art on that question.

But I'm not interested in using HoTT for what you call "these
purposes" - i.e., the things you  listed, that you  are interested in.
  I'm interested in it for wholly other reasons!  So, its relation to
ZFC doesn't matter much to me.  Someone will eventually figure that
out, or maybe someone already has.  And when they do, I'll eventually
hear about it. That's enough for me.

FRIEDMAN:

So there seems to be a path to reconciliation. "You" refrain from
referring to exotic type theory as a general purpose foundation. That
phrase has an historical meaning over many decades, if not longer,
that supports investigations 1-3 and the like that I presented above.

It seems to be a framework for certain kinds of mathematics.

As I said before, model theorists and descriptive set theorists have
very effective frameworks that take them where they want to go. But
they do not even consider thinking of their frameworks as any kind of
general purpose foundation for mathematics.

In the next message I plan to take up the Lawvere quote.

Baez:

Reconciliation is pretty easy.  You claim ownership of the term
"foundation" and battle anyone who tries to use it in ways you
dislike.  I only use that term when I'm feeling too lazy to explain
what I'm really interested in - namely, "entrances".   So, you just
have to forgive me for being lazy sometimes.: if you see me say
"foundations", know that I mean "entrances".

As for that Lawvere quote, can you remind me what it is?   Did I quote
him at some point?

By the way, if you want to battle someone over foundations, Lawvere
would have been a lot better than me.  He's getting pretty old, but he
used to relish a good fight.  In fact, I hear he punched out his
department chair.

FRIEDMAN:

I was a colleague of Lawvere's for five years many years ago. If I
recall properly, we both pretty much regarded each other as hopeless
intellectually.

This is what I will take up after I take a break:

Baez:

There's also a tendency to see the traditional foundation as
relatively trivial and not worth the attention it gets, and even as
suspect in some way.   For instance, in an interview not long  after
Godel's 100th birthday, Lawvere answered a question about the
"extra-mathematical publicity around his incompleteness theorem" by
saying:

"In Diagonal arguments and Cartesian closed categories we demystified
the incompleteness theorem of Godel and the truth-definition theory of
Tarski by showing that both are consequences of some very simple
algebra in the Cartesian-closed setting. It was always hard for many
to comprehend how Cantor’s mathematical theorem could be re-christened
as a “paradox” by Russell and how Godel’s theorem could be so often
declared to be the most significant result of the 20th century. There
was always the suspicion among scientists that such extra-mathematical
publicity movements concealed an agenda for re-establishing belief as
a substitute for science. Now, one hundred years after Godel’s birth,
the organized attempts to harness his great mathematical work to such
an agenda have become explicit."

Harvey Friedman