[FOM] FOM: What is a proof?

[Bill Taylor]

The key to clarifying debates about this, is the recognition that the word
"proof" has two closely related yet starkly distinct meanings, when used
in math, or more precisely in meta-mathematics.


Proof-1 is a very formal object; a sequences of lines in a strict formal
language, usually FOL(=) with a few extra symbols and a shortish list
of axioms (and schemas).  It must follow certain precise and simple rules.

A proof-1 is itself a mathematical object! - a sequence of strings of
a certain type.  It was this realization, long heralded, but finally
fully clarified by Godel, that enabled his breakthrough theorems,
(actually meta-theorems), and launched modern math logic on its current path.

Unfortunately, humans, being as lazy and imprecise as they are, find proof-1's
virtually unpresentable for all but the most baby classroom examples.
Thus, only an outline of these can usually be given.  Such is a...


Proof-2.  This is a somewhat more informal object, containing a lot of
ordinary natural language as well as a fair amount of proof-1 material,
though even this is usually in a highly modified and abbreviated form.
Proof-2's are what typically appear in math journals.

It is generally assumed, and is usually the case, that a proof-2 could
("in principle") be converted into a proof-1, by standard classroom means
that are culturally conventional, slightly subjective, and what are largely
the content of school and university math education.  The fact that there
is usually (at least a small) subjective element, can occasionally lead
to controversy, mistakes, and corrections; and, very rarely, a complete
abandonment of an alleged proof-2.     This subjective element, however,
is enormously less than the equivalent in most, even all, other subjects;
though that doesn't stop it being pounced on by silly folk who should know
better, (such as Penrose, Hersch, and many others), to back up claims that
math is philosophically contentious, irremediably error-ridden and hopelessly
mind-substance-ish in origin.   None of these last things are true.


Finally, though a proof-2 is a mere outline of a proof-1, there is also
a thing often referred to as a...

"Proof outline".  These are commonly seen in colloquia rather than journals,
though they can appear there too.   A proof-outline is an even more informal
argument, that the demonstrater hopes, and hopes that his audience will see,
can be turned into a proof-2 by filling in some (possibly substantive)
gaps in the argument.  There is always an implied admission that work
still needs to be done.


If we continue the debate with these distinctions in mind, much will
become clearer, I hope.

------------------------------------------------------------------------------
        Bill Taylor                     W.Taylor at math.canterbury.ac.nz
------------------------------------------------------------------------------
             Logic - used by mathematicians but not talked about,
                       talked about by philosophers but not used.
------------------------------------------------------------------------------