FOM: mathematical certainty

[Vladimir Sazonov]

Anatoly Vorobey wrote:
>
> You, Stephen Cook, were spotted writing this on Fri, Nov 20, 1998 at 02:23:42PM -0500:
> > My point of view is that "mathematically certain" means that there exists a formal
> > proof in an appropriate formal system; say ZFC.  The authors of both theorems
> > are trying to convince us that such a proof exists.   I don't know which (group
> > of) author(s) has done the more convincing job, but the necessary use of computers
> > to check the four-color theorem proof does NOT make it less convincing.
>
> It would be fascinating to hear more responses on this, obviously foundational,
> issue. Rota's point is that mathematicians in general *do* feel very
> strongly that the necessary use of computers to check the 4CT makes the claim
> of its validity less convincing.
>
> > Both
> > computers and mathematicians can make mistakes:  to decide which argument is more
> > convincing one has to consider who checked each one and how it was checked.
>
> It seems to me that you're aiming for some kind of (however limited) equality
> of mathematicians and computers when validity of a theorem is to be
> considered - please correct me if I'm wrong! However, even the very statement
> "both computers and mathematicians can make mistakes" is very much
> "human-centered": a computer never makes a mistake from "its own" point of view,
> it just sits there and works. Mistakes "happen" when the results it produces
> don't match our, human, expectations.

I think that there were no aiming here of the "equality of 
mathematicians and computers".  In any case, it is a 
mathematician who checks whether a text satisfies all formal 
conditions of a correct proof. Computer only helps him as, say, 
airplane helps us to travel.  Both a mathematician (which 
himself also works here as a kind of computer) and electronic 
computer are not very reliable (may be by different reasons:  
some illness or crash, etc.).  The main point, as I understand 
it, is that only *formal* proof may be a genuine mathematical 
proof. Of course, what is "formal" was understood in mathematics 
somewhat differently (but quite coherently!) in different 
historical periods and even by different peoples in the same 
period.

However, being human beings, we do not like to write absolutely 
formal proofs and prefer to give only some convincing evidence 
that such a proof may be written (of course, together with some 
intuitive backgrounds behind this proof). We usually (and quite 
reasonably) evaluate this informal evidence much higher than the 
formal proof itself (as written symbol-by-symbol). Using such an 
informal evidence is the main difference between the ordinary 
"human-mathematical proof" vs. "computer proof".  But, 
nevertheless, this evidence concerns exactly to *existence of a 
formal proof*. Otherwise, this is everything, but not a *proper* 
mathematics. Say, it may be quite useful guess-work for a future 
proof or some philosophical remarks, etc. Only after fulfilling 
some sufficient(!) work towards formalization we get 
mathematical proof.

Another (actually self evident but often ignored) point which is 
worth and necessary to note and which I consider philosophically 
important consists in the "requirement" that any formal mathematical 
proof should have intuitively feasible length (i.e. the number of 
symbols). Say, (even feasible) rigorous proof in PA *of existence 
of a proof* of some theorem A is strictly speaking not a feasible 
proof of that theorem (however, it usually can be converted 
into a proper feasible proof of A).  On the other hand, by the 
evident vagueness of the intuitive notion of feasibility, we 
could consider more restrictively as *proper* only those proofs 
which have been checked by *human* beings ("human feasibility" 
vs.  "physical" or "computer feasibility").  Then 4CT may be 
considered as still unproved.  Moreover, it is possible in 
principle that its negation is formally consistent (in this more 
restricted sense of feasibility of proofs). 


Vladimir Sazonov