FOM: Re: Visual Proofs: Reply to Silver and Hayes

[Charles Silver]

On Mon, 1 Mar 1999, Joe Shipman wrote:

> Silver:
> > What do you mean by a "rigorous sentential proof"?

Joe shipman:
> Basically, a formal proof in the predicate calculus from some accepted
> set of axioms -- these proofs (the objects of proof theory) are
> "sentential" because they consist of sequences of sentences, each of
> which is either an axiom or derivable from earlier sentences by a
> logical rule.  

	I would bet that very few people in FOM have ever *seen* a
"rigorous sentential proof" in this sense.  Simple truths in set theory,
become monstrously long when reduced to sentences of first-order logic.
For example, I seem to remember first-order sentences expressing simple
properties of restrictions on functions that required several lines of
handwritten text. And derivations of these sentences go on for pages and
pages. I know this, because I once had to construct proofs of this kind a
long time ago in a set theory course I took.  I think the prof. didn't
realize what he was letting himself (and us) in for when he made these
assignments.  He didn't want to grade that junk, so he quickly changed his
requirements for what a proof was.  Another thing I remember: after a
simple set theoretic sentence is translated into a first-order sentence
that's say, four handwritten lines long, there's not much hope of
understanding its content.  It becomes technical gibberish; all meaning
seems to evaporate. So, I think a "rigorous proof" must stop short of
being a first-order derivation.  I don't know where one should stop,
though.  I think figuring out exactly what constitutes a "rigorous proof"
is not all that easy. 

Charlie Silver
Smith College