[FOM] foundations meeting/FOMUS/discussion

[Harvey Friedman]

On Sat, Mar 19, 2016 at 12:18 PM, Louis Garde <louis.garde at free.fr> wrote:
> Le 18/03/2016 04:40, Harvey Friedman a écrit :
>>
>> Among the obvious merits of ZFC as a foundation for mathematics, there
>> is one that I often see not sufficiently emphasized. That is, its
>> PHILOSOPHICAL COHERENCE.
>>
>> ../..
>>
>> But my impression is that the more radical proposals, particularly
>> HOTT, philosophical coherence is proudly thrown away.

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.

However, there does remain the possibility that HOTT could have some
impact on the subject: foundations of mathematics. For instance, there
may be interesting metatheorems to the effect that if you take a HOTT
point of view in a certain kind of mathematical context, regardless of
its philosophical coherence, then you can always replace it with a
standard point of view - i.e., you still get a theorem of ZFC or
variant. I am under the impression that just this sort of thing is
being done.

Also it may well be the case that if you take a HOTT point of view in
a certain of mathematical context, then proof structure gets
simplified, and/or it gets easier to formally verify certain kind of
results.

Such developments promise to be relevant  to f.o.m. However, that it
not to say that it rises to the level of a new foundation for
mathematics. For that, the standards are rather high - and
philosophical coherence is absolutely essential.

> Could you clarify what you mean by "philosophical coherence"?
> Don't you think that constructiveness brings a very strong "philosophical
> coherence" ?

Philosophical coherence is a notion that has been in implicit use
since at least the great Greek philosophers. I am not really the best
one to try to clarify this notion. I think that the leading
philosophers can do a much better job of this.

Yes, constructiveness does have a sufficiently strong philosophical
coherence to offer an alternative foundation for mathematics that is
worthy of consideration. At the moment, it is doubtful if it is as
philosophically coherent as traditional non constructiveness, but it
is sufficiently philosophically coherence to be taken seriously as an
alternative foundation for mathematics.

However, the most readily digestible versions of constructive
foundations are trivially restrictions on classical foundations, and
so their value as an alternative is in terms of placing additional
demands.

But there are other versions of constructive foundations which cannot
be readily construed as obvious restrictions on classical foundations.
Here the philosophical coherence generally becomes much less clear.
>
> With my own understanding, the philosophical coherence of Martin Löf's
> intuitionistic type theory is at least as strong as ZFC's one.

It would be valuable for the FOM readers to give a brief simple
account of Martin Lof's intuitionistic type theory, here on the FOM.

E.g., what do you think of the account in
http://www.math.unipd.it/~silvio/papers/TypeTheory/InnIntro.pdf ?

There is nothing there that on a casual reading, has anything like the
philosophical coherence of the usual fragments of ZFC. Furthermore, on
a casual reading, there is one notion after another that is foreign to
the way working mathematicians think. This is already not a good sign.
On a casual reading, this appears to be incomparably more complicated
than the usual fragments of ZFC. Another not so good sign. Again, we
are talking about prima facie casual readings.

Philosophical coherence and complexity here can be nicely judged by
comparing descriptions and discussions side by side. In the case of
ZFC and its usual fragments, the philosophical coherence, complexity,
and descriptions are exceedingly well known and accepted, and so I am
not sure if there is any point in me displaying such things here on
the FOM. However, there does seem to be a point in trying to provide a
comparative treatment here on the FOM for the ITT side. Even before
one gets to the main event of HOTT.

I found the following on the Internet:
http://www.bristol.ac.uk/media-library/sites/arts/research/homotopy-type/documents/identity-in-hott-part-one.pdf
Unfortunately, I do not see any indication of who the authors are of
this internet manuscript, which is a bit strange and frustrating.
There they do claim that HOTT can be cast in a way that provides an
alternative foundation for mathematics. They appear to be quite
sensitive to the correct view that in order for HOTT to rise to the
level of a legitimate alternative foundation, it has to be cast in a
way that does not depend on specialized esoteric mathematics.

A quick read of this does not reveal any kind of clearly stated
philosophically coherent foundational proposal. It would of course be
very interesting to FOM readers to see such a proposal stated in
simple clear terms.

> And, to put it very briefly, HoTT is a natural extension of it: its
> definition of identity types makes it applicable to homotopy theory, but you
> do not need homotopy concepts to justify the rules defining identity types.
>
Mathematicians use one single robust notion of equality which is so
ingrained in their thinking that it does not require any conscious
thought. Identity sometimes becomes an issue, and that is normally
handled through equivalence relations and taking equivalence classes,
as taught in undergraduate math.

Having nuanced notions of equality of a nature that is generally
foreign to what is normally taught and used is prima facie rather
dubious, and the burden of proof is on the proposer if they wish to
maintain philosophical coherence. This is by no means impossible. It
just means that a high bar has to be met, with carefully constructed
and rather easily grasped accounts. One should be particularly
suspicious of rule based concepts.

Now ultimately, I doubt if anybody is going to convince the
mathematical or philosophical communities that alternatives like HOTT
are philosophically coherent unless they in some ways rely on an
interpretation of it into fragments of ZFC (or maybe standard
extensions of ZFC). Of course, once one does have such an
interpretation, there is the question of what has been gained by the
whole enterprise.

For instance, there is the extremely crucial perennial question of
whether the current foundations for mathematics is sufficient to
establish mathematically important results of a computational nature.
I mention computational here because those kinds of statements do not
have rival formulations. I.e., you have the same computational
statements independently of whether you are doing ZFC, ITT, HOTT, or
S:EOIAFHEIOEWAUOFN. Now if you develop mutually interpretations of the
usual kind that one expects and has done, then one gets as an
immediate Corollary, that computational statements are going to be
provable under one philosophically coherent foundational framework if
and only if it is provable under any other rival philosophically
coherent foundational framework.

So one thing that is NOT going to be gained by replacing the usual set
theoretic foundations with HOTT or SEOFINIOENFOWENFOIEN is any kind of
difference with regard to the derivability of mathematical results of
a computational nature (derivability in the usual sense).

So the argument for the value of having an alternative foundational
framework is likely going to have to rest on more focused practical
issues, rather than the classic foundational issues everybody is
familiar with.

One is of course that it is supposed to facilitate or even make
possible the creation of formal proofs. My impression is that, SO FAR,
the evidence for this is confined to a few examples from specialized
esoteric contexts, together with the "claim" that formal proofs cannot
be done with the usual set theoretic foundations in the pragmatic
sense. But how is such a "claim" justified? Merely saying that one has
failed to be able to come up with formal proofs under the usual
foundational framework is not remotely convincing. What is needed here
is an ATTRACTIVE challenge problem: can you get a formal proof of such
and such simple basic attractive theorem using the usual foundational
framework? One should be able to have some rather basic and intriguing
ATTRACtIVE challenge problems IF the aim is to go beyond specialized
esoteric mathematical contexts.

What other benefits are adherents envisioning for such alternative
foundational frameworks? (See the second and third paragraphs of this
posting).

Harvey Friedman