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

[Timothy Y. Chow]

Torkel Franzen <torkel at sm.luth.se> wrote:
>   No, we're never "forced to stop" in a theoretical sense. Any
> effectively axiomatizable theory that we recognize as an iterated
> consistency extension of Q we can also extend by adding one more
> consistency statement.

O.K., so as usual I guess I need some remedial lessons here.

Suppose I start with Q.  I want to form a sentence Con(Q).  There are
several subtleties here; first of all, I have to fix a particular
recursive "presentation" of Q.  We can do this in pathological ways, e.g.,
by using a Turing machine that, after generating Q in some reasonable
fashion, starts generating one of the axioms of Q over and over again
while searching for a contradiction in "ZFC + measurable cardinals exist"
and then generating "0=1" if it finds one.  (In [off-list] email, Bob 
Solovay pointed out this example to me, although he was making a slightly
different point; I'll come back to this later.)  Assuming that no such
contradiction exists, the machine really just generates Q, but this
version of "Con(Q)" says a lot more than "Q is consistent."  Similarly,
even if we choose a reasonable presentation of Q, we can monkey around
with pathological consistency predicates.

Now, these problems are certainly solvable in the particular case of Q,
so suppose we do so.  But now I want to iterate, to get statements
Con(Q+Con(Q)), Con(Q+Con(Q)+Con(Q+Con(Q))), etc.  At each step I have
to be careful not to misbehave in the above fashion, but again this is
a solvable problem, and it's possible to devise an effective procedure
to generate each "level" from the previous one in a reasonable way.

If I now want to jump up another level, then the natural thing to do is to
take the union of the omega levels I've generated so far to form a new set
Q_omega of sentences, and then assert Con(Q_omega).  Once again some care
is needed because I need to figure out a recursive presentation of Q_omega
so that I can express its consistency.  But again, this is a solvable
problem.  And once I've solved it, I can move up the chain again to
Q_{omega+1}, Q_{omega+2}, and so forth.

Now what I presume is that this process can be iterated up to very high
countable ordinals, adding one statement at successor ordinals and taking
unions at limit ordinals.

So when does the process stop?  As Torkel Franzen remarks, it's not going 
to stop at a successor ordinal, so what must happen is that for some limit
ordinal alpha, Q_alpha (the union of all Q_beta with beta < alpha) is no
longer recursively presentable even though all the Q_beta are.  It would
seem to me that this would happen at alpha = w_1^CK.

But, I don't understand this process very well, so maybe I'm wrong about 
that...maybe the "solvable problems" I mentioned above (avoiding various
undesirable pathologies) stop being *uniformly* solvable at a much lower
ordinal and hence the ascent is blocked at an earlier stage?  Or maybe
I'm missing some other subtlety?

I'm sure this is all extremely well understood; perhaps by this point I've
irritated enough experts with my ignorance that one of you will be moved 
to educate me.  :-)

The upshot may be that assumption "RP" needs to be worded more carefully.  
I stated it as follows:

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

It might be that some riders need to be attached about exactly what kinds 
of statements "Con(T)" I'm allowing here.

By the way, I'm going on vacation tomorrow for about a week and will 
probably not have email contact, but of course I'll catch up on everything 
after I get back.

Tim