[FOM] Re: Consistency of Formal Theories

[Richard Zach]

>  Also, a yes answer would appear to contradict the information that
> was tacit in Richard Zach's response to my original query, for he
> seems to indicate that the Church-Kleene ordinal is countable, as if
> this is well-known.

You can find an exposition of constructive ordinals in Ch 11 of Rogers'
Theory of recursive functions and effective computability.  Kleene's O
is a particular system of ordinal notations, and an ordinal is
constructive if it is the order type of a notation in O. The least
ordinal that does not receive a notation in O is \omega_1^CK.  Since
each constructive ordinal is countable, and there are only countably
many constructive ordinals (they are enumerated by Kleene's ordinal
notation system S_1), \omega_1^CK is countable.

But to go back to your original question: You wanted to do something
like this: You start with S(0) (= PA) and add A(0) (= the Goedel-Rosser
sentence for S(0), which is neither provable nor refuatble in S(0)). 
This gives S(1).  Add the Goedel-Rosser sentence A(1) for S(1) to get
S(2), etc.  But to write down A(omega) you need a formula Prov(omega)[x,
y] which represents provability in S(omega).  For that you need a
formula that represents "is the code of an axiom of some S(n) for n <
omega".  Probably right here, but at the latest when you "continue this
procedure transfinite inductively" you need some kind of uniform way to
talk about "all ordinals less than \alpha" when you want to define
Prov(\alpha)[x, y].  You can do this if you, e.g., use recursive
ordinals (because these are all definable by primitive recursive
predicates), but it's not at all clear what to do if you want \alpha to
run through all the countable ordinals.  You'd need, for each countable
ordinal \alpha, a formula Prov(\alpha)[x, y] in order to define
S(\alpha+1); but there are only countably many formulas yet uncountably
many countable ordinals.

Yours, Richard

-- 
Richard Zach ...... http://www.ucalgary.ca/~rzach/
Assistant  Professor,   Department  of  Philosophy
University of Calgary, Calgary, AB T2N 1N4, Canada