[FOM] What is a proof?

[williamtait@mac.com]

On Oct 26, 2003, at 5:19 PM, John T. Baldwin wrote:

> Position A.  A proof is a means of establishing the truth of a 
> proposition.

I would argue for ``the means'' in place of ``a means''.

> Position B.  A proof is an explanation of why a proposition is true.
> ..............
> 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.
> ............
> From the standpoint of Position B, the defect of Definition 1, is that 
> there is no criteria of relevance of the steps of the proof to the 
> result.  If we interpolate a sequence of tautologies in a proof (maybe 
> many times the length of the original proof) it is still a proof by 
> the (inadequate) definition 1).

There is a notion of equality of proofs (obtained by translating the 
proofs into natural deduction). Each equality class contains a unique 
proof in normal form, effectively determined from any member of the 
class.

The redundancies that you mention do not occur in normal proofs.

Natural deduction proofs do explain truth in one sense: e.g. a proof of 
B= forall x F(x) is the construction of a function yielding for each x 
a proof of F(x) and a proof of B = exists x F(x) is a pair consisting 
of a witness x and a proof of F(x).  There is, of course, an exception 
(in classical logic): the proof of B may be obtained from a proof of 
not not B by double negation elimination. TIn this case the sense in 
which the proof gives an explanation of truth is less straightforward.

Yet, there is a psychological notion of `explanation', to which at 
least in part  John is referring, to which normality is irrelevant.

Bill Tait