[FOM] Re: Proof "from the book"

[Timothy Y. Chow]

"Jeffrey Ketland" <ketland at ketland.fsnet.co.uk> wrote:
> Aren't "proofs from the book" meant to give the "true reason" for the
> proposition proved? The underlying explanation?

That's a good question, but I think you'll get different answers from 
different people.  From my personal observations of how people use the
term, one of the main criteria for deciding whether a proof is from the
book is elegance.  The proof should be slick, beautiful, having no 
extraneous detail or messy constructions.  It should have an air of
optimality or unimprovability.

"Giving the true reason" often involves developing additional machinery
or placing the result in a larger context.  If your proof derives a result
as a quick corollary of a more general result, then some people might not
feel that it's a book proof, because you're "cheating" by sweeping a large
amount of potentially messy detail under the rug.  For example, Martin 
Davis's suggestion for a book proof of Goedel's 1st theorem is short and
sweet, but is it really a book proof, since it cites theorems that may not 
have unimprovably mess-free proofs themselves?

In short, book proofs might not give the "underlying explanation."  As
another example, the "underlying explanation" of quadratic reciprocity
might be the Artin reciprocity law from class field theory (or even more
general reciprocity laws), but most people will reserve the term "book
proof" for a short, self-contained and elementary proof of quadratic
reciprocity.

[Re: Lucas-Penrose argument]
> I entirely agree with this reply. In order for their arguments to work at
> all we should need empirical evidence for the claim,
> 
>       (*) For any consistent S, the human mind can reliably come to see
>       that S is consistent.

I don't think they need such a strong assumption.  They just need 
something like,

(**) If S is an explicitly describable subset of reliable human 
     mathematical knowledge, then the consistency of S is also
     an explicitly describable piece of reliable human mathematical 
     knowledge.

In other words, they don't need to quantify over *all* consistent S.
There's a section in "Shadows of the Mind" that talks about large
cardinals, and Penrose doesn't claim that we're able to ascertain the
consistency of arbitrarily powerful systems.  It's just that according to
Penrose, *if* S is unassailably reliable then Con(S) is unassailably
reliable, so that the unassailably reliable truths can't be recursively
axiomatizable.

> Feferman defines a theory Ref(S) which he
> calls the "reflective closure" of S. This is meant to contain the sentences
> one "ought to accept", when one initially accepts a mathematical theory S.
> In a sense, Ref(S) is the result of iterating the construction from S to
> Tr(S). Feferman doesn't advocate iterating Ref(S), but I do not see why.

Torkel Franzen has an illuminating discussion of this and related matters 
in his book.

Tim