FOM: certainty/belief

[Harvey Friedman]

We start with the extremely crude question: is mathematics certain?

I claim that a careful systematic investigation of this question leads to a
recasting of a number of developments of f.o.m. as well as the opening up
of a number of new issues for f.o.m. and f.o.c.s. In particular, one is
compelled to make a large variety of distinctions - some of them quite
subtle.

I have no doubt that the discussion of this matter on the FOM could become
sufficiently sophisticated and systematic to as to form the beginnings of a
new subject. I would like to play a role in this.

Let me make an obvious point that says something about contemporary
academic culture. The question "is mathematics certain?" is of far greater
interest to almost anybody outside of mathematics than any topic in normal
mathematics. And of far greater interest to almost anybody outside of
matheamtical logic than any topic in mathematical logic. Yet how many
people make a living in academia on the basis of their work on this
question?

Now that doesn't mean that what people have said about this question - or
what people will say about this question - necessarily measures up to its
interest. That's the challenge.

The first point about "is matheamtics certain?" is that it would appear
that some mathematics may be certain and other mathematics not certain. Or
even that some mathematics is more certain than other mathematics. Without
biasing the discussion, we should rephrase the question as:

What is the nature of the belief in mathematical assertions? Is there a
highest level of belief appropriately associated with at least some
mathematical assertions? Is the nature of the belief in mathematical
assertions of a different character than it is in other subjects? If so,
then what is the nature of that difference?

I now want to describe a view about these matters that I find most
attractive. However, let me say that I am fully aware that there are all
kinds of subtle vulnerable spots and missing componenents in what I am
going to say. I like this. Because I have thought about this just enough to
see that defending what I am about to say will inevaitably require some
serious new science of permanent value. So this is fertile territory for a
good whore like me (5:20PM 9/11/98).

I want to first focus on "standard mathematical proof." By this, I mean the
kind of thing that is published as a theorem in, say, the Annals of
Mathematics, which explicitly does not rely on the action of a computer or
any physical processes. This is almost all of what has appeared in the
Annals as Theorems.

There are quite a number of deep and subtle issues surrounding proofs that
do rely on computer or physical processes, but want to defer discussion of
them.

When a Theorem is published in the Annals, there is a complex underlying
structure which lies in the background of the decision to accept the
Theorems as having been sufficiently documented. Thus the following would
not be publishable without modification in the Annals:

THEOREM. All B's are Q's.

Proof: At the 35th Annual meeting on GIBBELEYDOCK, this was extensively and
exhaustively discussed. Many objections were raised. The participants were
from all walks of life, who put their reputations on the line. Finally, a
vote was taken. It was unanimously agreed that this was definitely true. QED

On the other hand, we do see the following:

THEOREM. All B's are Q's.

Proof: From "The resolution of bad points in cones and spheres" by Joe
Blow, 2050, page 365. QED

THEOREM. All B's are Q's.

Proof: Immediate by Lemmas 8 and 23. QED

THEOREM. All B's are Q's.

Proof: Obvious. QED

THEOREM. All B's are Q's.

Proof: Left to the reader. QED

***

Thus, for the Annals, it is not enough to cite that "everybody agrees that
this is true". One must reference it as being claimed as a Theorem
elsewhere. This distinction is important to the Annals.

So the distinction between "A is proved" and "A is universally believed" is
a crucial one for the Annals.

Thus there is an adherence at the Annals in some sort of underlying
structure that is very different from opinion. We want to get at the exact
nature of this underlying structure.

Now the standard vehicle for delineating this underlying structure is in
terms of formal systems that lie at the heart of f.o.m. One constructs a
formalism - and without biasing matters yet, let's call it T. Here T
consists of a system of axioms and rules. Then one defines what a formal
proof in T is. Broadly speaking, this is a finite sequence of assertions
that adheres to the system of axioms and rules of T.

Conventional discussions surrounding this in f.o.m. stop here. Namely, one
says that a Theorem is accepted if and only if it has been given a proof in
T.

It is now very fashionable to question this assertion. This is actually
quite a reasonable thing to question. And it leads to some very interesting
new science.

It's quite reasonable to question it because, for one thing, it is
obviously false. In fact:

1. Let T be any standard version of ZFC - say, from textbooks for the basic
papers of f.o.m. Then only trivialities have ever been given actual formal
proofs within T. In fact, such systems must be augmented with lots of
abbreviational devices in order to make it humanly palatable to construct
formal proofs.

However,

2. There are now some automated theorem proving projects - particularly the
Mizar project - where serious theorems (still miniatures) are accepted by
the computer system as being proved, as the result of man/machine
interaction. The output is a proof in a suitable formal system.

Thus it seems reasonable to make the following separation, when addressing
the issue of "belief in mathematical theorems."

I. Should we believe in the formal system used by these systems, which is
invariably a variant of the standard ZFC system of axioms and rules? I.e.,
believe in theorems of that formal system? And how do we test our belief?

II. Should we believe that the output of this man/machine interaction -
which the machine says must be a proof in the formal system - is in fact a
proof in the formal system? And how do we test our belief?

Finally, there is a further issue for "real" and "critical" mathematical
situations. The Annals of Mathematics published a proof of A. Wiles of
Fermat's Last Theorem in 1996.

III. What procedure could or should be followed to maximize the degree of
belief in FLT? Can or will a proof of FLT be entered successfully in a
system like Mizar? Are the editors of the Annals, Wiles' himself, or the
number theory community explicitly or implicitly saying that they could
enter it in a system like Mizar?

These are some of the questions I want to address in the future.

Finally, I want to say something about: what is the point of developing a
system like ZFC?

First of all, you can probably already tell that I claim that ZFC is
important in connection with the issues addressed above, in that it has
suitable modifications for use in the construction of actual formal proofs.

But there is another point which was first illustrated by the classical
situation with regard to the continuum hypothesis. Once upon a time, people
like Hilbert actually worked on proving (or refuting) the continuum
hypothesis. ZFC appears to be easily a good enough model of what these
people had tried to do that the independence results about the continuum
hypothesis and ZFC are considered more than good enough to provide a
convincing and celebrated impossibility result. Does anybody question this?
Of course, some serious new science may need to be done in order to
seriously attack this, and/or to seriously defend this against attack.