FOM: mathematical certainty
Vladimir Sazonov
sazonov at logic.botik.ru
Tue Nov 24 15:59:58 EST 1998
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
More information about the FOM
mailing list