[FOM] Re: Proof "from the book"
Timothy Y. Chow
tchow at alum.mit.edu
Tue Aug 31 15:01:07 EDT 2004
"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
[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
(**) 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
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
> 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.
More information about the FOM