[FOM] What is a proof?

[John T. Baldwin]

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 .

>  
>