[FoM] What is a proof?

[John T. Baldwin]

A.P. Hazen wrote:

>    Baldwin and Simpson have been talking about the notion of an 
> *explanatory* proof.  Baldwin's proposed account of this notion is 
> that it is a proof in which every statement deduced contributes to the 
> final result: no obiter dicta.  (I hope my paraphrase of his 
> suggestion is recognizable!)  I'm afraid this sounds to me more like a 
> condition (of efficiency?) on the <i>presentation</i> of proofs than a 
> characterization of a quality -- explanatoriness -- of the proofs 
> themselves. 

This reply also partly addresses Tait's remarks concerning normal forms 
of proofs.  To avoid terminological confusion (partly engendered by my
contentious phrasing of `what is a proof')  I repeat my defintion

Standard Definition. 1. A proof is a sequence of propositions each of 
which is either an axiom or follows from those earlier in the list by a 
rule of inference.

A proof is a given such sequence; if you give me a different sequence it 
is a different proof.  We are trying to give some formal 
characterization of whether this
is a `good' or explanatory proof.   I provide only what seems to me a 
relatively straighforward condition which we could take as necessary. 
 My goal
explicitly to make this formal not psychological.

The condition I proposed  (which Hazen nicely phrases as `no obiter 
dicta' )  is fairly trivial , but I suggests it relevance on two grounds.

On the banal side, take a 20 line derivation in your favorite system of 
propostional calculus and random place add a tautology in every otherline..

On the practical side consider trying to read an extremeely complicated 
manuscript which contains the following sentence:  

"We divide the proof into cases, according to set-theoretic 
possibilities; in fact, not all cases are necessary but as our aim is 
also to exemplify
techniques, we do not economize."

Of course, `explanatory' is  psychological.  This doesn't mean that 
there can't be (less trivial than this example)  ways to formalize the 
explanatory
value.  Adding a modal relevance operator has been suggested.  

Simpson's reverse mathematics certainly gives some information.  But,  
it seems more to tell me more about the underlying theory in which two 
interesting propostitons have been reduced to different names for true 
than about the content and connections of the propositions.
In paticular, it is still an analysis of the relations between the 
results, not of the specific argument used to establish  the results



>
>