# [FOM] What is a proof?

John T. Baldwin jbaldwin at uic.edu
Mon Oct 27 21:49:46 EST 2003

```
Stephen G Simpson wrote:

>John T. Baldwin 27 Oct 2003 writes:
>
> > (Of course it would only be terminological if you wanted to reserve
> > proof for the weak notiion ;-) used by fom and `good' proof for the
> > stronger notions that I am suggesting.)
>
>Dear John,
>
>I imagine your ;-) is intended as an indication that we are not to
>take your statement too seriously.  And, you have ackowledged the
>usefulness of reverse mathematics.
>
My wink is just twitting you on terminology.  I am just giving a partial
formalization of what stands a good mathematical practice.

I am in the midst of trying to understand some work which is
burdened by proofs which are usually correct in the sense of fom; but
are not proofs in the sense I am
speaking of -- they contain at least 30 or 40 % correct statements which
are not used for the Lemma or Theorem at hand.
So the difference between a proof and a good proof is very real to me at
the moment.  I gave a formal
definition, not at all vague, of one requirement of relevance.

This is a perfectly good formal notion which would improve the
explanatory value of a proof while not affecting its verifability
(not psychologically but formally ) one whit.

Simpson writes

>
>  Definition.  Let T be a theorem of second order arithmetic, Z_2.
>  Let P be a formal proof of T within the formal system Z_2.  We say
>  that P is *explanatory* if the conjunction of the fintely many Z_2
>  axioms used in P is logically equivalent to T, over RCA_0.
>
>This rigorous notion of *explanatory proof* may not do everything you
>want it to do, but it is good enough to make some useful distinctions.
>
>
As I said before.

It makes some useful distinctions;   it does not come near to doing
everything I want it to do .

>
>

```