[FOM] Re: Lucas, Penrose, and the Church-Kleene ordinal

[Timothy Y. Chow]

A few weeks ago I suggested that the Lucas-Penrose argument could be
formulated as follows.  If S is "the set of first-order arithmetic truths
that are unassailably known by human mathematicians," then S satisfies

  RP: If T is a subset of S and T is a recursive CFA, then Con(T) is in S.

Recall that CFA = "consistent fragment of arithmetic."  Then I also 
suggested that candidates for S are related to iterated consistency
extensions of length w_1^CK.

The responses I got were very helpful, and clarified some misconceptions
that I had.  In particular, I found Torkel Franzen's book
"Inexhaustibility," which he modestly and inaccurately described as
"possibly tedious," extremely relevant and illuminating.  The book is not
yet published, but I'm sure he will provide electronic copies upon
request, and I highly recommend it to anyone interested in the issue.

With my improved understanding of the issues involved, I feel (even more
confidently than before) that RP is a good formulation of the argument.
Franzen and Solovay, if I understand them correctly, make the point
that RP, as I have formulated it, is vague.  Specifically, at the
beginning of the sentence, T is simply a set of sentences, but by the
end of the sentence we have subtly and implicitly made a shift (from
"extensional" to "intensional" perhaps?) to some *description* of T
in the language of arithmetic, since that is needed in order to write
down the sentence "Con(T)."  There are many ways to do this, and there
is no canonical choice that works in the utmost generality.  Moreover,
there are certain perverse choices that make RP highly implausible.

Nevertheless, this doesn't make me feel that RP fails to capture the
Penrose argument, because I think that that argument is vague to begin
with, and I believe that the vagueness of RP is actually a fairly
accurate representation of the original vagueness.  In particular,
I seem to recall that Penrose glosses over the issue of *recognizing*
that some particular formal system correctly represents some or all of
our mathematical knowledge, and this is analogous to glossing over the
issues involved in formulating Con(T) "correctly."

On the other hand, I believe that my earlier suggestions about w_1^CK
were misguided.  It's true that w_1^CK is a kind of "upper bound" on
how far an iterated consistency extension can go.  However, difficulties
can arise at much smaller countable ordinals; in order to write Con(T)
one needs to choose an *ordinal notation*, and we can run into the problem 
that in order to "know" Con(T) we need to know that the ordinal notation
expresses what it's supposed to, and this could require "knowing" 
arithmetical facts that we cannot justifiably claim to know.  (I hope I 
got that right.)

This is a pity, from my point of view, because I had been hoping for a
"clean" argument along the following lines: It is true that one can take
any recursive CFA and diagonalize out of it, but this does not mean that
humans are always one step ahead of Turing machines, because the 
diagonalization procedure is completely mechanical and can be done by
machines just as well as we can; if one tries to iterate this procedure
then it stalls when one hits a non-recursive axiom set, and at that point 
we're just as stymied as the machines are because Goedel's theorem doesn't
apply (since one of the hypotheses of the theorem---recursiveness---is
violated).

I wonder if there is a way to salvage this "clean" argument?  (I call
it "clean" because it doesn't have the "heap paradox" flavor that some
of the rebuttals to Lucas-Penrose have.)

Tim