[FOM] What is a proof?
John T. Baldwin
jbaldwin at uic.edu
Sun Oct 26 18:19:13 EST 2003
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
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
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.
More information about the FOM