[FOM] What is a proof?
williamtait@mac.com
williamtait at mac.com
Tue Oct 28 09:14:48 EST 2003
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
More information about the FOM
mailing list