FOM: certainty

[Randy Pollack]

First, a recent example of another long-open problem verified using
computer calculation of many and large cases: Thomas Hales announced a
proof of Kepler's conjecture about maximum density packing of speheres
(http://www.math.lsa.umich.edu/~hales/countdown).  See Nature (1 Oct
1998) for an informal overview.


Vladimir Sazonov said he is "a permanent opponent of those who assert
existence of absolute mathematical truth."  I don't know what
"absolute truth" means.  Issues of evidence and belief are more
interesting.  What follows is not a final answer to mathematical
meaning, but some sample thoughts meant to widen the FOM discussion.


I suggest seperating belief in a formal system from belief in proofs
in that formal system.  Belief in ZFC is informal in the sense that if
we disagree (say Steve Cook believes ZFC but I do not) there is no
formal argument to attain agreement.  We must talk about mathematical
principles and other philosophical stuff.

Belief in a formal proof in a given formal system, S, (here I'm vague
about what is a formal system; I'll return to that later) is attained
formally, not philosophically.  If A doesn't accept a proof in S, s/he
must say which step s/he doesn't accept.  Then B, who believes the
proof in S, can add more detail to the explanation of why the side
conditions and premises of Rule xxx are satisfied; or possibly A can
convince B the formal rule does not actually apply.  Under reasonable
meanings of "formal system", A and B can resolve the point purely
formally.

The distinction is not quite as simple as I just suggested.  We need
some base notion of representation of a formal system; i.e. we somehow
have to bridge the informal-formal gap.  We cannot have a formal
presentation of a formal system until we have, at bottom, some
informally presented formal system.  This is usually where we appeal
to PRA (informally presented), or to Fefermans FS0, or to some weak
dependent types system (Martin-Lof's or Plotkin's Logical Frameworks).
So it is possible to find disagreement about the encoding of our
object formal system in the meta-system PRA or FS0 or ....  The
"informal" framework may actually be a computer program in a
completely formal notation, but it ultimately is executed on a
physical device.


We haven't yet addressed the formal system itself; we must look, not
at extension (the judgements derived), but at presentation.  Cut-free
FOL is different from FOL with cut in terms of both feasible checking
and mathematical principles.  The admissibility of cut is
meta-theoretic, outside of FOL, depending on induction in the
meta-theory.  So if we want to use cut, and other admissible rules,
they should be explicitly part of the formal system.

In this way, we might have a formal proof of the 4CT in a formal
system that has rules explaining the computational behavior of the
computer programs that check the cases.  Those rules are shown to be
admissible by meta-theoretic proof, just as the cut rule is for FOL.
Accepting the meta-theoretic program correctness proof as a
mathematical principle is the main difficulty to calling this a proof,
but how is it different from accepting cut?

We can internalize this approach in a logic with internal computation,
such as Martin-Lof type theory or the Calculus of Constructions.  The
4CT programs can be written as typed lambda-terms that are proved
correct internal to the logic.  (Now there is no new mathematical
principle being accepted specifically for the 4CT, and Martin-Lof type
theory is based on weak principles for those who accept ZFC!)
However, we must execute the typed lambda-terms (i.e. check
definitional equality in the formal system) to have a truly formal
proof.  This is totally infeasible!

But we can play the same trick again.  Work on "program extraction"
from constructive proofs (e.g. Nakano and Hayashi, Paulin-Mohring,
Berardi, ...) suggests that we can make these internal proofs of the
4CT in Martin-Lof type theory into feasible programs.  (E.g. using
Paulin-Mohring's extraction, implemented in Coq, there is a running
proofchecker actually extracted from a proof that proof-checking is
decidable in the Calculus of Constructions.)

However, we will need a new mathematical principle to accept these
feasible programs as internal proofs in the logic.  This has not been
studied to my knowledge.  Again, this principle is seen
meta-theoretically to be admissible, and is not a special principle
adopted to prove a particular theorem.

Thus it is conceivable we can have a completely formal (feasible)
proof of the 4CT in a constructive and predicative logic.  Still, I
guess no mathematician will "read and understand it" in the ordinary
sense.  What should we make of that?

-- 
Randy Pollack                      <http://www.dcs.gla.ac.uk/~pollack/>
Computing Science Dept.                         <pollack at dcs.gla.ac.uk>
University of Glasgow, G12 8QQ, SCOTLAND          Tel: +44 141 330-6055