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

[Torkel Franzen]

  Tim Chow says:

 >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.

  That all depends on how the sequences are defined. The union of a
short sequence of effectively axiomatizable theories need not be
effectively axiomatizable. If we consider sequences of iterated
extensions by reflection relevant to our mathematical knowledge, we
don't get such short sequences, but we don't get any family of
sequences with a union of length w_1^CK either.

  The latter subject (defining iterated reflection sequences relevant
to mathematical knowledge) is developed at possibly tedious length in
my "Inexhaustibility" volume (LNL 16). Feferman's proof of the
existence of short complete sequences is presented in my forthcoming
BSL paper, "Transfinite progressions: a second look at completeness."
These might be suitable sources if you want to get a grip on the
details of one way of going about the construction of iterated
consistency sequences or reflection sequences (by way of progressions).