FOM: NYC panel discussion/formalization

[Harvey Friedman]

Simpson 10:55PM 12/26/99 wrote:

>A special event at the conference was a lively and wide-ranging panel
>discussion on
>
>         The Role of Set Theory and its Alternatives
>            in the Foundations of Mathematics
>
>The moderator of the panel discussion was Rohit Parikh.  The panelists
>were Haim Gaifman, myself, Alex Heller, and Harvey Friedman.  The
>entire discussion was videotaped.  Perhaps Joel Hamkins can provide
>information about how to obtain the videotape.

>In his opening remarks, Gaifman set the tone by giving an overview of
>the subject.  One of Gaifman's memorable points was an analogy between
>the ZFC formalism and the gold in Fort Knox.  Gaifman's said that,
>even if nobody ever formalizes mathematical practice in ZFC, it is
>possible in principle to do so, and this is the currently accepted
>basis of mathematical rigor, just as gold backing is the basis of a
>sound currency.

In my opinion, there are a number of very interesting deep issues connected
with this common claim by logicians that ZFC is a formalization of
mathematical practice.

Ultimately, people may have sharply different views of what a formalization
of mathematical practice is, and whether ZFC provides it or not.

But there is extremely interesting basic knowledge lacking in connection
with ZFC and mathematical practice that  would definitely affect most in
depth discussions of the matter.

And taking a dogmatic view on the matter of ZFC and mathematical practice
is likely to inhibit certain important research and create missed
opportunities.

There is no question that many respected scholars feel that in some sense
essentially all of actual mathematics can be formalized in ZFC, and are
happy to leave it at that for a motivation for various research in
mathematical logic. But the really interesting issue is: what does it
really mean?

And again, no doubt many respected scholars don't really care what it
really means. What it means to them is that we have sufficient motivation
for studying formal systems such as ZFC.

Some of the issues surrounding ZFC have been discussed on the FOM in these
postings:

Trybulec, April 12, 1999
Friedman, April 12, 1999
Shipman April 12, 1999
Trybulec April 22, 1999
Trybulec April 26, 1999

Trybulec is a principal of the Mizar project and an FOM subscriber.

A principal application of the claim that "all mathematical proofs can be
done in ZFC" is that if one shows that ZFC cannot prove a sentence phi,
then mathematicians are never going to prove phi.

But of course, mathematicians may some day accept more than what is in ZFC
as a proof and then perhaps mathematicians might prove phi anyways.

But the obvious retort is: either this is never going to happen, or if it
does happen, it will be a monumental controversial event - or at least be
preceded by monumental controversial events.

In other words, some major change from the status quo must occur in order
for this to happen.

I believe in all this, even though I recognize the interest and
difficulties involved in making this more precise. However, I can tell you
something perhaps shocking to many:

A significant percentage of mathematicians do not relate to this at all. In
particular, they do not perceive the reasoning patterns that are so clear
to us as mathematical logicians. Reasoning patterns in some sense embedded
in ZFC.

In particular, they have never even seen a single example of a formal proof
of any nontriviality.

So it is natural to have some presentable examples of formal proofs of
nontrivialities. If one is actually going to present these, then, first of
all,

*they must be of some reasonable length (i.e., number of symbols). They
can't be of length, say, 2^50.*

But also,

*they must be readable.*

The latter has been a big bugaboo of mine in this area. I know that
mathematicians are very fussy about what they are willing to read. It must
conform to either very standard mathematical notation, or at least
mathematical notation that can be viewed as an improvement on very standard
mathematical notation.

For example, mathematicians generally are not totally wedded to the
sometimes vague dx notation, and are willing to consider operator notation,
even in relatively elementary contexts when dx notation is always used.

I definitely get the sense that this aspect of things is inadequately dealt
with by any work I have ever seen in this area. I worked on this problem of
the syntax and semantics of mathematical notation (which I looked at as
preliminary to any consideration of formalization of proofs), most recently
with Randy Dougherty. This is a doable problem.

But somewhat independently of this, is the crucial issue of length. This
can be profitably addressed without having a fully satisfactory notational
scheme.

In particular, I asked this question of Trybulec, and got this response:

>> E.g., how long is an appropriately formal proof of Fermat's Last Theorem?

>I have no idea.

In other words, the crucial issue regarding lengths of formalizations is
whether or not there is an impractical blowup that asserts itself when one
is dealing with a particularly involved mathematical proof. In particular,
a proof with a seriously nested structure. I.e., where the proof cleverly
combines several major results, each of which are proved by cleverly
combining several major results, etcetera, for quite a while down (up) a
tree. If there is in fact some nonlinearity going on in the formalization
in ZFC, then it just might assert itself in a situation like this where the
completely formalized proof is of unreasonable size.

And what does unreasonable size mean here? Well, certainly if the number of
symbols needed is, say, more than the total number in the currently
published mathematical literature. Or is it going to be even more than 2^50?

Well, I don't think so. But this is because I believe in the power of
formalization - if done right. I believe that we are talking about a linear
phenomena.

These issues have a lot in common with the analogous situation with regard
to formal verification of software (and hardware, of course). In this
context, the issues assume great practical importance - already of some
significant importance, but perhaps much greater potential importance. It
is still extremely expensive to create formally verified software for
various reasons. I want to discuss this matter in greater detail in a later
posting.

What do the results of Mizar so far indicate about the lengths of actual
formalizations of deep mathematical proofs? Of that I am not sure, but I
tend to think that Mizar is evidence that we are dealing with a linear
phenomenon with manageable constant factor.

Incidentally, I have been told the following:

a. That an investigator in the automated theorem proving project at SRI
wrote a formally verified proof of the Godel first incompleteness theorem
for his PhD.
b. That the Godel second incompleteness theorem is regarded as very
difficult to get a formally verified proof of - estimate of at least two
years of hard work needed.
c. That Constable at CS/Cornell is the man to talk about this project,
which has not yet been started.
d. Oh!! Constable is an FOM subscriber.