[FOM] "Mere" correctness of a proof

[Franck Slama]

Following Timothy's interesting answer, I wanted to add the following on
explanatory versus non explanatory proof,
first versus second proof of a theorem, and a small digression on the
equality of such proofs :

Even if the only proof of a theorem T that we have is not very explanatory
(for example, the very computational proof
of the four colour theorem), we still get from this proof the motivating
guarantee that the theorem is *true*. This is the
big difference between a first proof, and any other proof that comes after
it : the first one might not explain very well why
things are this way, but it removes the doubt on T's veracity. The second,
third, and Nth proof of the same theorem T
can be more explanatory than the first, but we don't learn from them the
fact that T is a valid theorem, as we already
knew it from the first proof. This is why theorems are often named after
the first person that finds a proof of it (even
though there are exceptions).

With such a first proof of T, having this guarantee on the truth value of
T, we might be more tempted to spend more
time finding a more interesting/explanatory proof. However, when we don't
have this guarantee, we don't know if we
are simply losing our time, as the claimed theorem could simply be false...
In the case of the four colour theorem, it's even better as this first
proof is formally verified on a proof assistant, helping
us to believe even more on it (a very computational proof on the paper is
very likely to be wrong, as we're not computers
after all!).

If someone is only interested in the *truth* value of statements, he/she
can even consider different proofs of the same
theorem as equal, and be perfectly happy with the proof irrelevance
principle.
These proofs might be very different (they can be classical or
constructive, they can be explanatory or not, complicated
or simple, etc), if we're only interested in *truth*, they only exist to be
warrants on veracity.

However, if someone is also interested in the computational content of the
proofs (a constructivist), or in having a real
explanation on things (every mathematician I guess), or in having a simple
proof (a maths teacher for instance), then
he/she might not see such proofs as equal.

Please note that my comments are very much inspired from many explanations
given by Alain Prouté, and especially
from this presentation :
http://www.logique.jussieu.fr/~alp/luminy_05_2007.pdf

Kind regards,

Franck Slama

On Fri, Sep 7, 2018 at 8:30 AM Timothy Y. Chow <tchow at math.princeton.edu>
wrote:

> Harvey Friedman wrote:
> > A) the first digit of pi is 3.
> > B) the sixth digit of pi is 9.
> >
> > (recall pi ~ 3.14159)
> >
> > This is an interesting arena to test the idea of "explanation of proof".
>
> Another possible arena is computational complexity.  As longtime FOM
> participants know, I am fond of citing the theorem "Checkers is a draw."
> It is hard to imagine an "explanatory proof" of this theorem that does not
> involve brute-force calculation.  Assuming that there is some upper bound
> on how long a proof can be before it ceases to be "explanatory," any
> EXPTIME-complete problem furnishes a family of short theorems which cannot
> all have short proofs.
>
> "Checkers is a draw" could of course be criticized as an unnatural or
> uninteresting mathematical theorem.  But I see no reason why there could
> not exist a short and beautiful theorem for which there does not exist an
> explanatory proof.  (Of course it might be practically impossible to show
> that no explanatory proof exists, so we might be tempted to keep searching
> for one.)  In that event, would Weil have said that God exists because the
> theorem is true, but the Devil exists because we cannot explain why it is
> true?
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180907/90959803/attachment.html>