[FOM] foundations meeting/FOMUS/discussion

[Harvey Friedman]

An important and as of yet unrealized role of FOM is to discuss
various mathematical foundational topics being addressed at meetings
throughout the world. Some time ago I mentioned the ambitious idea of
discussing available materials surrounding such meetings.

It occurred to me that in many cases, it makes sense to start
discussions based on meeting announcements, even in advance of those
meetings.

An obvious opportunity for this is the recent announcement on the FOM
of the workshop/conference FOMUS

http://www.cs.nyu.edu/pipermail/fom/2016-February/019545.html

I asked the organizers what they thought of the idea of generating an
in depth discussion on their topic in advance of their meeting right
here on the FOM. Perhaps they can make use of the discussion in
various ways during the meeting. They enthusiastically encouraged me
to go ahead with this plan now on the FOM!

For reader's convenience, I quote the purely content part of their
announcement in
http://www.cs.nyu.edu/pipermail/fom/2016-February/019545.html

"FOMUS: Foundations of Mathematics: Univalent Foundations and Set
Theory - What are Suitable Criteria for the Foundations of
Mathematics?

... emphasis on HoTT/Univalent Foundations and set theory.

Zermelo-Fraenkel axioms are widely assumed to be the foundation of
mathematics within the mathematical practice of set theory. However,
an increasing number of researchers are currently working on the
Univalent Foundations as an alternative foundation of mathematics.
This relatively young approach is based on Homotopy Type Theory, which
is a link between Martin Löf's intuitionistic type theory and the
homotopy theory from topology.

... With regard to the philosophical discipline of mathematics, the
formal requirements of the foundations of mathematics, their
limitations and their naturality will be examined. Recently, it has
become increasingly important to formalise mathematics by
computer-aided formal proof systems, such as Coq. With this in mind,
it will be investigated which foundation is most suitable for the
changing needs of mathematical practice".

In some correspondence I had with the organizers, the following topic
was also mentioned:

"Criteria of an appropriate foundation of mathematics, especially
about set theory as a foundation of mathematics, and  its pros and
cons."

I also see roughly a dozen announcements of various meetings in recent
weeks on the FOM! Perhaps many of these meeting announcements also
strongly suggest the initiation of interesting discussions!

*SOME THOUGHTS*

I like to distinguish two items:

1. A foundation for mathematics.
2. Foundational issues concerning mathematics.

Of course, 1,2 are normally lumped together with the phrase
"foundations of mathematics" as a topic or field of investigation.

A FOUNDATION FOR MATHEMATICS

There is a standard classical meaning for this. Namely, to provide a
precise "workable" rule book for mathematical "activity", that
provides suitable criteria for "correctness" or "legitimacy".

The ZFC system is easily the simplest and most directly effective
vehicle that we have for this, under a range of standard classical
meanings normally assigned to these words in quote signs.

However, there has been increasing interest in developing alternatives
to ZFC, motivated by more refined interpretations of the words in
quotes (and related words), and other motivations.

As readers can see on the FOM, I am an extremely loud defender of ZFC
and an extremely loud attacker of ZFC. For the second, I am putting
together a manuscript that utterly demolishes the sufficiency of ZFC
for very standard, arguably vital, mathematical purposes, with no
possibility of circumvention. But that is not something I want to
pursue in this posting.

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. This philosophical coherence is yet more
pronounced in the case of its rather strong and effective fragment ZC.

The FOMUS meeting can be viewed as being sensitive to refined notions
of "workable". There are senses in which the ZFC rule book is entirely
workable, and there are refined senses in which it is entirely
unworkable.

The sense in which it is entirely unworkable is in the refined sense
of applying to actually constructed mathematical proofs. If this is
taken literally, I am worried that mathematicians would die from
exhaustion from adhering to ZFC. In this sense, ZFC is actually
dangerous.

So what I am talking about is a new perceived role in a foundation for
mathematics, which is the support for the construction of actual
proofs - i.e., the construction of proof assistants.

This "new" movement (not so new any more, of course) in no way
diminishes the obvious status of ZFC as one of the top few premier
intellectual structures in the entire history of ideas. It does what
it does remarkably well, far superior to any competitors. But now we
have some additional purposes that ZFC does so badly, that it can make
people ill.

I favor the approach of carefully adding a lot of sugar to ZFC, rather
than bringing in foreign elements or replacing aspects of ZFC. There
are proof assistants in existence that are basically sugared ZFC in
use today, namely Mizar and Metamath. http://www.mizar.org
http://us.metamath.org

For the former, there have been a lot of complaints, with people
insisting that they need to introduce the foreign element of serious
typing. I'm not sure that Metamath has been developed enough or long
enough to have enough visibility yet for people to complain much about
it.

I strongly doubt that the creative possibilities for adding sugar to
ZFC are even remotely exhausted. I am particularly skeptical of
statements made by mathematicians and computer scientists who are not
experts in mathematical logic that make strong declarations about the
limitations of sugared ZFC.

Of course, with sugared ZFC - like Mizar and Metamath, there is no
question of philosophical coherence. However, depending on how
elaborate one's typing is, the issue of philosophical coherence
naturally arises. My impression is that already with systems like Coq,
philosophical coherence starts to or almost starts to become an issue.

But my impression is that the more radical proposals, particularly
HOTT, philosophical coherence is proudly thrown away. If my impression
is correct, then that would make it rather unlikely that HOTT could
play a significant general purpose role in any kind of foundation for
mathematics addressing refined notions of "workable" as we are
discussing.

However, my impression is that HOTT ideas can be profitably viewed as
a normal kind of technical development that simplifies and synthesizes
complex ideas in certain special areas of esoteric pure mathematics.
This kind of thing of course is highly valued in esoteric mathematical
circles without people referring to it as any kind of "new foundations
for mathematics".

Now I am giving you my impressions, and they are not based on making
the effort to look into such things in detail. I have my own interests
in "workability motivated f.o.m." and they are general purpose and go
into rather different channels.

FOUNDATIONAL ISSUES CONCERNING MATHEMATICS

There are many standard classical issues concerning the nature of
mathematics, which are only tangentially related to giving a
foundation for mathematics.

For some of these issues, particularly some that I have spent a lot of
time thinking about, it is clear that it doesn't make any difference
whatsoever whether one is using ZFC or some other moderately standard
non set theoretic setup.

I am referring to the various incompleteness issues initiated by
Goedel in the 1930s.

In particular, is there an incompleteness in our foundations of
mathematics that cannot be naturally circumvented and therefore safely
ignored for normal mathematical purposes?

An incompleteness representing this level of unremovability is
inevitably going to have to be of a rather low logical level of
complexity that issues of formulation and meaning are not going to
naturally arise. I.e., the incompleteness is not going to be sensitive
to whether one is taking a set theoretic approach or not. TRANSLATION:
Immediately digested statements in the integers or rationals have
foundational immunity.

Now why is it that the choice of foundations has no bearing on such
incompleteness? The answer lies in the notion of interpretation. The
point is that all reasonable foundational schemes thus far presented
are interpretable in set theory and vice versa. More specifically, all
reasonable foundational schemes seem to be mutually interpretable with
a standard version of set theory. And the kind of strong relative
interpretability arising here is enough to make the various systems
entirely equivalent with regard to such concrete incompleteness.

Other foundational issues that are immune to set theory:yes/no are:

tameness
algorithmic decidability
constructivity
finiteness
ultrafiniteness

and many others. Let's continue the discussion.

Harvey Friedman