[FOM] What is a proof?

[John T. Baldwin]

These thoughts were stimulated by some of the notes on Corfields book 
but are independent enough that I am not going to search for the 
inspiration.  An alternative title is Why do we prove?

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


Position B.  A proof is an explanation of why a proposition is true.


Position B requires more of a proof than does position A.
A proof in the sense of position B must be a proof in the sense of 
Postion A.  But not conversely.

  I take Position A to be a part of traditional fom.


To raise some hackles:  Principia Mathematica was an existence proof for 
being able to prove all mathematical  truths in Sense A; however, its 
method of establishing A, completely defeated any chance of B.
(I deliberately ignore Godel; this statement simply glosses in a 
provacative way the effect of PM on the Mathematical community at large 
at the time. )

But my goal today is to point out that there are technical tools - 
provided by ordinary logic to address Position B.

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.

2.  A theorem is any line in a proof.

(2 is a commonplace to logicians, a strange convention to other 
mathematicians.)

 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).

This problem could be addressed by
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 and each line is a premise of some later step.

(I came to this conceit by trying to read a published paper which 
contained a number of true but irrelevant statements making the actual 
proof much harder to comprehend.)


Informally, a proof explains the truth of a proposition if the 
hypotheses are adequate to imply the conclusion but not too strong.
(We can prove 2 + 2 =4 from 0 not equal 1;  a better explanation is to 
use appropriate axioms for arithmetic.)  So we could make a criteria for 
  a proof  that for A => B to be a step in the proof there should not
be an A' where A' is as well-established as A and we could equally well 
use A' => B (where A=> A' but not conversely.)


One might give the notion of Theorem its usual mathematical use by 
refining the notion of `proof' to include the actual practice of 
collecting substrings into
Lemma's and applying Lemmas in other instances. Thus `theorems' are used 
often, represent repeated submodules in the long proof.  (Sorry, just 
speculation here.)


The point of this note is that the idea of `proof as explanation' has 
content beyond `proof as establishing truth'.   Serious exploration of 
this distinction would require new ideas.  I list a couple of 
trivialities simply to show that formal notions can apply.