[FOM] FOMUS/alternative foundations

[Harvey Friedman]

Response to Angere and Paulson.

Garde:

>>> But my impression is that the more radical proposals, particularly
>>> HOTT, philosophical coherence is proudly thrown away.

Friedman:

> That is my understanding, which may or may not be correct. (However,
> see below for a pointer to an internet manuscript ).This certainly
> prima facie precludes HOTT as any kind of reasonable "foundation for
> mathematics" in any standard sense.

Angere:

Caveat: I am not a member of the HoTT community, but just a
philosopher enthusiastic about the project. First of all, not everyone
agrees on ZFC's high "philosophical coherence". It was built
piece-by-piece, and while some parts can be given coherent
interpretations, it is not obvious that the whole can. I think a good
classic critique of ZFC's coherence is Hallett's "Cantorian Set Theory
and Limitation of Size".

Friedman:

Let's separate two issues concerning ZFC.

1. Does it reflect a philosophically coherent mental picture of a
fundamental reality or structure? Obviously one can try to say this
more carefully or more nuanced, but that would take us too far afield.
2. Here 1 does not address the issue as to whether it stops at a
natural or important place, or whether it really is a fragment of
something bigger.

Generally speaking, there is *general* agreement in the mathematical
community and the preponderance of the standard Western analytic
philosophy community that 1 is clearly true. And those in that
community who have serious reservations about ZFC with 1, normally
fully acknowledge a strong kind of coherence, maybe even calling it
philosophical coherence.

With regard to 2, we have a much more controversial situation. My own
view is that despite an historical case that ZFC came about "piece by
piece", ZFC or ZF is a demonstrably completely natural stopping point.
In fact, ZF(C) is the canonical transference of the hereditarily
finite set theory to infinite set theory. More specifically, ZF(C) is
logically equivalent to what you get when you take all statements of a
certain nice kind true in the hereditarily finite sets, and add the
axiom of infinity. I wrote about this on the FOM more than once some
years ago, and gave a talk on it at a set theory meeting in UPenn many
years ago. I didn't have a chance to complete this work because of
more urgent matters concerning Concrete Incompleteness. I would very
much like to get back to it.

Angere:

Second, HoTT has an extremely high degree of philosophical coherence.
Part of this is because Martin-Löf's original system was built with
just that purpose in mind; his Bibliopolis book

https://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf

gives lots of philosophical arguments for why the extensional version
of his system looks the way it does.

Friedman:

How does your first sentence compare with Garde:

>>> But my impression is that the more radical proposals, particularly
>>> HOTT, philosophical coherence is proudly thrown away.

Rather than refer to a book, it would be useful to actually COMPARE a
so called philosophically coherent presentation of ML and various
extensions, with a so called philosophically coherent presentation of
ZF(C) or Z(C) or other fragments. As indicated above, you would expect
me to start with the V(omega) construction. Actually, I think one of
the things I did is give a complete characterization of all statements
of a certain basic kind that are true in V(omega), showing that the
ones that are false are trivially refutable. And this complete
characterization is essentially ZF, if we merely add the axiom of
infinity. But regardless of any novel details, the main point is that
ZF(C) is supposed to be forced on you essentially from the actual
natural mathematical V(omega) construction.

If you or someone else takes up this challenge there is a danger that
you will be faced with the following situation. Before you even begin
to justify the meaning of a number of philosophically oriented items
that play absolutely no role for 99.99% of working mathematicians,
looking completely foreign to them, I on the other hand will be
finished entirely with my presentation. And that's before you even
really start to present any actual stuff.

I'm not saying that the situation is that bad. I'm just saying that
you want to be careful to avoid a situation like that.

And from what you say and my general impressions, the situation gets
MORE problematic when more modern ideas are layered on top of, or
incorporating forms of, ML.

Angere:

That book does not however treat the intensional version, which HoTT
is based on. But HoTT gets coherence from its geometric
interpretation: every rule of the system can be motivated by that.
When you are used to it, it is therefore a very intuitive system,
which is probably roughly the same as what can be said for ZFC. The
difference is that instead of visualizing in terms of collections of
things or Venn diagrams, you visualize in terms of spaces and paths.

Friedman:

Bringing in an intensional equality or identity is of course a huge
red flag for real foundations of mathematics. 99.99% of working
mathematicians will recoil in horror at even the suggestion that they
have to think consciously about equality, especially if there are
going to be more than one important kinds of equality. They know, and
well appreciate, that they are saved from this "nuisance" by the usual
set theoretic foundations.

So you have a very very tall mountain to climb to bring in any
delicate kind of talk of equality or identity and have any chance
whatsoever of this rising to the level of any kind of alternative
foundation for mathematics.

Also, all of the logical axioms and rules in ZF(C) come from the most
universal kind of common sense logical thinking that has evolved over
million of years of the evolution of the human mind. Another high bar
to meet.

Angere:

So the reason I (and I assume some other philosophers too) am excited
about HoTT is precisely because of its philosophical coherence rather
than, say, its computational properties. Those properties are
important, but it shares them with other systems too. HoTT, on the
other hand, is rare among challengers to ZFC in that provides not only
a formal system but also very useful intuitive interpretations. This
means that it can be used to give an alternate way of looking at or
thinking about mathematical structures, which I have often found very
enlightening.

Friedman:

We can get the discussion going by presenting just one or two
fundamental mathematical structures and carefully talking about this
"alternative way of looking and thinking about them". Best would of
course be if you had a new way of looking at the usual number systems,
integers, rationals, real numbers, complex numbers. Maybe too
elementary? How about the usual separable Banach spaces. Any new way
of looking at them? What about finitely presented groups? What about
algebraic number fields? What about C(X) where X is a compact
Hausdorff space? What about the semi algebraic subsets of R^n? What
about analytic functions from C into C? What about ordinary and
partial differential equations, particularly those arising from
mathematical modeling of physical phenomena? What about standard Borel
spaces? Etc. Give us some red meat right here in front of our faces on
the FOM.

Let's step back here. I am deliberately ignorant about most things int
he world, because the world is an unbelievably big place. For example,
I don't know anything much about the circuitry used in the latest crop
of dishwashers, nor about the best methods known for training future
professional weightlifters, nor the most recent advances made in
improving the chemical compositions of paints, nor details of how
Exxon refines oil.

And why am I so ignorant?

Because with so many interesting things around, I have to figure out
how to spend the remaining 10, 20, 30, 100, or 1000 years of my life
with some level of efficiency.

So I, like most everybody else, I'm sure including you, develop some
sort of FALLIBLE instinct as to what ideas are worth thinking about or
investigating. I have leaned that if you want to do something totally
revolutionary, you may well have to spend 50 years thinking hard. Of
course, it does get tiring to bang your head against a wall for 50
years - usually either that wall or your head will irreparably break.

So generally speaking, when confronted with a grandiose idea, I rather
quickly dismiss it as too minor for my aging brain to even consider.
This particular group of grandiose ideas has got a tiny bit of my
attention
because; Some suggest that it has something serious to do with the
foundations of mathematics. Even that it represents some sort of new
foundational idea or foundational construction.

Obviously, if it were merely presented as a budding new specialized
branch of, say algebraic topology, or category theory, given the size
of the world, I would spend less than 10^-100 seconds thinking about
it. But that is not the aspect that we are talking about here.

So I was curious enough to listen a tiny bit. I even made a several
day trip to IAS. On one or two occasions I managed not to fall asleep
too much during relevant talks.

I KNOW what it sounds like when you take something really substantive
from one area and talk to superstars in other areas in a way that is
totally comprehensible to them. And succeed in getting them to see
what the point is in their terms. I've done this kind of thing for
decades. If I presented superstars with books, or links to books, or
manuscripts, I would have been instantly dismissed as a nuisance who
specializes in some weirdo stuff. For superstars, that characterizes
the vast preponderance of people, so I would be in good company. But I
rise beyond this because I don't throw links and manuscripts at those
superstars. I must make the essential points as unimpeachably crystal
clear as possible, as BRIEF and POWERFULLY as possible, in THEIR
terms, if I want to have any impact whatsoever.

Now it should be emphasized that this is not so easy to do. It is much
easier to talk shop, and simply operate with a variety of hidden
assumptions that you and your close colleagues work with at a
subconscious level. That is generally fatal if you want to have any
impact at all. AND, above all, if you want to deliver the real thing,
you MUST have the goods. This exercise of forcing one to talk to
superstars in a variety of areas that have no concept of or natural
affinity for your particular specialities, can be very brutal.
Weaknesses in you ideas get exponentiated or double exponentiated.

SO: my first impressions are

i. I do NOT see any "foundational red meat", and so prima facie, there
is no point in spending more than 10^-100 seconds thinking about it.
2. BUT: just enough people see something in this and are committing
time to writing about it, that I should take a second look.
3. I would be rather shocked if it rose to the level of any kind of
really alternative foundation, but I find it very likely that I could
benefit from knowing more about it.
4. To the extent that it has any general purpose merits, I expect that
brief, simple, clear, convincing, well constructed, totally
transparent, accounts of at least something impressive can be and will
be presented that fits nicely on a moderate length FOM posting, so
that it can be readily contemplated, absorbed, and discussed.
5. I personally have NEVER had a good idea that I could not readily
put in form 4. And when I have trouble putting it in form 4, I suspect
that the idea is no good.

Paulson:

I am very familiar with Martin Löf's intuitionistic type theory as it
was in 1982, and his explanation of the rules makes perfect sense from
the point of view of Heyting’s explanation of intuitionism. His system
can be regarded as a straight formalisation of Heyting’s philosophy,
and I believe it is also backed by some proof-theoretic results. I
don’t know how easily it could be interpreted in ZF, because you can
write things such as \lambda x. x (the unrestricted identity
function), which is a proper class rather than a set. I am much less
familiar with the type theory or theories underlying Coq and with the
question of set-theoretic models there.

Friedman:

Heyting's explanation of intuitionism is rather borderline
philosophically coherent, involving lots of extra mathematical
concepts. Computationalism is taking seriously in the math community,
but intuitionism is not. (By the way, I wrote a lot of papers on
intuitionism, and have been sitting on some advance in completeness
that I want to return to in the near future, improving seriously on
Lauchli).

Generally speaking, I am highly suspicious of any formalism which
doesn't have a completely straightforward interpretation into standard
set theory. I don't mean that it isn't interesting to find an
interpretation - it almost always is interesting. I mean that it is
dubious that it provides any kind of alternative foundational
framework - with a very high bar to meet. Typical red flags are the
use of notions not recognized or used by the working mathematician,
and the level of complications involved. Set theory suffers from
neither, although it packs far more generality than is used, but it
packs this extra generality as a byproduct of its great simplicity.
This is rather singular.

Paulson:

Heyting’s explanation of the logical connectives involves a certain
idea of evidence, where for example evidence for a conjunction is an
ordered pair, evidence for a disjunction is an element of a disjoint
sum and evidence for an implication is a (computable) function. This
may not have much to do with traditional mathematical practice, but it
has strong connections to computer science, and this explains the
considerable interest in constructive mathematics on the part of
theoretical computer scientists. My impression is that mainstream
mathematicians are much less interested in intuitionism.

Friedman:

"Evidence" in this sense is something totally missing from
mathematical practice. So it is a primitive notion not even in use. Is
it philosophically coherent in this context? Maybe marginally. "Strong
connections with computer science" of course is very much different
than "being an alternative foundation for mathematics".

Paulson:

In Martin Löf's 1982 type theory, evidence for a proof of equality was
effectively vacuous. This made equality extensional. I remember
reading Martin Löf's justification of this apparently controversial
decision. In a nutshell, the point was that once we know that a=b we
no longer need to know the reason. From my point of view, one
advantage of this choice was that it kept the “evidence” relatively
small even when it was based on a long and complicated proof. I did a
lot of work connected with this type theory in the early 1980s. But
sometime in 1984 or 1985, an intensional of equality was announced and
the previous system was dismissed as flawed. Interest in the earlier
system vanished not because of some paradox but because one man
changed his mind, and all of my own work was rendered useless because
it relied on extensional equality. That marked the end of my interest
in constructive type theory.

The Coq type theory is somewhat different but also has intensional
equality. That means for examples that n+0 = n and 0+n = n  (where n
is a natural number) are quite different statements, one holding by
definition and the other proved by induction. One of the claimed
advantages of HTT is that it simplifies the treatment of equality.
There is an obvious rejoinder to this.

Friedman:

Interesting, and the only comment I have is the following. Very early
on, the set theory situation became totally engraved in stone, with
one story holding up incredibly well. There was essentially only one
trial balloon, and it was Russell's type theories. In this classical
set theoretic line, only rather simple Russellian type theories
remain, the most common being object, sets of objects, sets of sets of
objects, ... . There is also the functional one: objects, functions
from objects to objects, functions from functions from objects to
objects to functions from objects to objects, etcetera, and obvious
variants. As is well known, this was all flattened out by Zermelo with
the system Z(C). Then Replacement came in for ZF(C). As I said
earlier, this is very far from piece by piece, as people who are not
happy with ZF(C) like to say.

Harvey Friedman