[FOM] Friedman/Baez/Bauer

[Harvey Friedman]

>From https://johncarlosbaez.wordpress.com/2016/04/02/computing-the-uncomputable/#comment-79258

Baez:

Yes, mathematical logic is just a branch of mathematics: it doesn’t
actually “support” or “hold up” mathematics, as the term “foundations”
suggests. Mathematics would not collapse if everyone suddenly forgot
about ZFC. In fact, almost all mathematicians, forced at gunpoint to
recite the ZFC axioms, would wind up pleading for the lives. There’s a
reason: none of the grad students at the universities I’ve been to are
required to take any courses on logic or set theory. And yet they seem
to do pretty well.

(Personally I think they’d benefit from exposure to more logic. But
they should also learn more category theory, differential geometry,
complex analysis, real analysis, functional analysis, topology, group
theory, ring theory, homological algebra, algebraic geometry,
algebraic topology, number theory, probability theory, statistics,
game theory, computer science, physics, and other things.  Ars longa,
vita brevis.)

One thing mathematical logic really does is systematize mathematical
reasoning in a way that lets us study it using mathematical tools. So,
the term “metamathematics” seems more appropriate than “foundations of
mathematics”.

Friedman:

Mathematical logic is the branch of mathematics that arose out of the
mathematical tools that were used to make the great advances in the
foundations of mathematics. These basic tools that were so effective
for f.o.m. became investigated for their own sake, usually without any
clear foundational purpose. However, many of these tools and a
considerable amount of the ensuing mathematical logic needs to become
second nature if the subsequent challenges in f.o.m. are to be
properly met.

It is true that the standard “rulebook” for mathematical rigor –
standard f.o.m. – is almost always only in the background. This is
because anybody capable of being a professional (pure) mathematician
must absorb what must go into a rigorous proof as part of their second
nature blood, in order to function reasonably. For this, they do not
need to consult the “rulebook”. The “rulebook” has been implicitly
absorbed by their teachers and the general mathematical atmosphere,
since the “rulebook” is so so so intuitive and simple.

Nevertheless, the great importance of having this “rulebook” in the
archives cannot be underestimated. There were periods of great
confusion, reaching a head around 1800, before the great pieces of the
“rulebook” were starting to emerge and work together properly during
the 1800’s and early 1900’s.

Of course, the great David Hilbert needed a “rulebook” to even
formulate his doomed program, (more or less) destroyed by Goedel. And
the great further advances in Incompleteness depend on the “rulebook”.
If you want to prove that something or other cannot be proved by
rigorous mathematical argument, you are going to have to have a
“rulebook”, even if you and your friends are not personally consulting
it.

Of course, the great great great foundational issue is whether the
rulebook allows us to do the interesting math that we are interested
in. Experience shows that Incompleteness is most disturbing to people
when it involves mathematical statements that people are strongly
compelled to consider “matters of fact”. E.g., you can argue that the
continuum hypothesis is not, is not clearly, matter of fact. That what
sets of reals are is maybe subject to interpretation – i.e., relative
to what means you have for constructing arbitrary sets of reals.
Evidence for this kind of point of view might be that if you only
consider Borel measurable sets of reals, then the continuum hypothesis
is a theorem, with no foundational difficulties.

However, if the incompleteness involves only, say, finite sets of
rational numbers, which ultimately means through encodings, only
natural numbers, then it gets harder to question the matter of
factness, and incompleteness becomes more serious.

Even clearer still would be say, sets of 1000-tuples of rational
numbers of height at most 2^1000. There are only finitely many of
these, and it gets hard to deny the matter of factness.

Now an interesting mathematical statement, or any statement, in this
realm, is definitely going to be provable or refutable in ZFC by
enumeration of all of the possibilities.

However, such a proof by enumeration is not going to literally be
given in ZFC with any reasonable size. Reasonable size like the proof
of FLT.

So such a result would cast serious doubt about the adequacy of ZFC at
a new matter-of-factness level.

>From https://plus.google.com/110536551627130071099/posts/6TiKLxjSCnu

Friedman:

I am expecting something interesting to come out of
http://www.cs.nyu.edu/pipermail/fom/2016-April/019707.html
as discussed below.

I would like to add something to the below. To show just how open
minded I am, suppose e.g., that homotopy typists claim that there
stuff is going to make inroads or even solve P = NP. If this is the
case, I would not agree that this in any way shape or form makes
homotopy type theory any kind of serious alternative foundations for
mathematics. On that, I view myself as an expert AFTER I see some
serious attempt for the homotopy typists to make the case. On the
other hand, I do not view myself as an expert on the prospects for
homotopy type theory solving P = NP and related problems, even if I
saw some philosophically coherent presentation. For that, I would ask
people like Widgerson, Aronson, Valiant, etcetera, what they think of
such prospects.

Bauer:

The Foundations of mathematics (FOM) mailing list, which I left a
while ago due to unfair moderating practices, seems to have gone crazy
with infinite discussions of "Set theory versus Homotopy Type Theory".

Friedman:

On the contrary, FOM promises to get to the bottom of the important
foundational issues raised by people claiming to have a serious
alternative general purpose foundation for mathematics. Especially see
http://www.cs.nyu.edu/pipermail/fom/2016-April/019707.html

Dimitris Tsementzis is from the Philosophy community, and so he knows
quite well what philosophical coherence means, having been grown up
with it in action. So far, I have not been able to get anybody to take
up the challenge in any other forum, so the FOM email list is a rather
special precious place at the moment.

NOTE ADDED: There are no unfair moderating practices on the FOM. The
moderating has worked very well. The moderator is Martin Davis. E.g.,
I am not a moderator.

NOTE ADDED: I fully expect something to come out of
Friedman/Tsementzis. But I expect that anything that will be offered
up foundationally I will be able to do better with standard f.o.m.
hopefully in real time. For instance, there is the old purely
geometric idea going back to Aristotle that the continuum is NOT made
of points. That it can be broken into two pieces in various "places",
but when so doing, there is no such thing as the endpoints of the two
pieces. Things like this, without points, need a tremendous amount of
creative ideas to get anywhere close to a general purpose foundation
for mathematics. Mathematics is just too big and diverse to think of
such intuitive geometric ideas as being anywhere near general enough
to provide a serious alternative foundation for mathematics.
Frameworks for parts of mathematics? Sure.

Bauer:

I find the whole activity ridiculous and based on the false premise
that the two foundations are in opposition (as attested by the titles
of discussion threads), or that they cannot co-exist, or that all
foundations of mathematics need to be linearly ordered. These are all
childish and false motivations.

Friedman:

It is not ridiculous. It appears that there is a combination of

1. A misunderstanding of what a general purpose foundation for mathematics is.

2. A gross underestimation of what needs to be done in order to
establish a general purpose foundation for mathematics.

It appears that some of the promoters of alternative general purpose
foundations for mathematics have 1 and some may not have 1 but have 2.

NOTE ADDED: There are some basic criteria for a general purpose
foundation for mathematics. I will discuss this in a later message.

Bauer:

The discussions are further hampered by the fact that no expert in
homotopy type theory is taking part.

Friedman:

They are in some other venues run by John Baez which I participate in,
and I copy a lot of that on the FOM. So you can see some of it in the
FOM Archives.

I think that as Dimitris Tsementzis tries to seriously grapple with
the real issues by trying to present something philosophically
coherent, this may draw in some of the experts in homotopy type
theory.

Bauer:

This might partly be a consequence of the lessons learned in the
1990's when FOM was extremely hostile to category theorists, although
I suspect (and can affirm for myself personally) that the questions
asked and the issues raised by Harvey Friedman are simply not relevant
to the HoTT crowd. There seems to be a very fundamental difference in
perception of what foundations of mathematics are, ought to be, and
what purpose they serve.

Friedman:

Yes, and I am trying to get a dialog going on the FOM and in these
other forums as to "what foundations of mathematics are, ought to be,
and what purpose they serve". I have offered up the word "framework"
for what homotopy type people are offering in the way of alternative
foundations for mathematics.

NOTE ADDED: It does look like you are right: that the issues I raise
are "simply not relevant to the HoTT crowd". This is more evidence
that the homotopy typists are not interested in seriously alternative
foundations for mathematics in the normal established sense of the
phrase.

Bauer:

Should the FOM audience stop throwing stones at anyone who disagrees
with them, they might actually learn about the exciting progress in
foundations of mathematics that is being brought about with
convergence of theoretical computer science and homotopy theory.

Friedman:

The issue is whether there is any progress in foundations of
mathematics brought about what you are referring to, and to what
extent it is real. For example, I have a kind of collaboration going
with an icon in theoretical computer science at the moment, and I
would doubt if he would recognize any serious such convergence. If you
are serious about this, I will inquire And do you think that icons
like Donald Knuth and Avi Widgerson are moved by any such convergence?
What about Leslie Valiant? 

NOTE ADDED: If such icons seriously talk of such convergence, then
homotopy type theory will get through my sieve, and I will have to
find the time to take a serious look. But i am hoping that I can just
work with  am expecting something interesting to come out of
http://www.cs.nyu.edu/pipermail/fom/2016-April/019707.html Category
type people have been throwing stones at standard f.o.m. for many
decades, and a good example is the quote from Lawvere that Baez
offered up, trying (absurdly and foolishly) to diminish Goedel's
Incompleteness results. I will come to that in a later message. I also
mentioned earlier that it was essentially a freak accident that I was
able to make a living working in real f.o.m. 

Bauer:

Supplemental: I have deleted the extremely long comments that appeared
under this post without reading them and have disabled further
comments. I also deleted one paragraph of my post which was arguably
something that required a reply. I am simply not in the business of
prolonging discussions with titles like "HoTT vs. ZFC" that present
"challenges to HoTT" or "challenges to ZFC", etc. They are
counter-productive and do not serve any purpose that would warrant
them appearing on my posts. If anyone feels like producing yet more
discussions, they are welcome to do so under their own G+ account. It
is easy enough to reference this post. But do not expect me to
participate, I simply wanted to express publicly my disappointment
with the FOM contracting a very common Internet sickness.

Friedman:

The FOM exhibits great internet health. I expect that the issues will
finally start to get seriously joined with followup from
http://www.cs.nyu.edu/pipermail/fom/2016-April/019707.html

Harvey Friedman