[FoM] What is a proof?
John T. Baldwin
jbaldwin at uic.edu
Tue Oct 28 12:42:23 EST 2003
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
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.
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
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
More information about the FOM