 # Notations for Ordinals, Si and O

Following Kleene , let first and (by App 10), let | | : N ^ Ordinals be the least partial function on N to ordinals which satisfies the following:

• (1) |1|= 0.
• (2) For every t, ^ | = | + 1.
• (3) For every e, if for every t, |et |^ and |et | < |et+i |, then |3 ? 5e|=limt^x|et |.

With S1 = {z : |z| ^}, the pair S1 = (Sb | |) is the first Church-Kleene notation system for ordinals and the only one we will use. Kleene  also introduced a smaller notation system S3 = (O, | |3) and a partial ordering <O of O such that and then used that in all his work on the topic—as did Spector and most researchers in the field. We will occasionally refer to O and <O when we want to quote early results exactly as they were stated, but we will not use them in any essential way and so we skip their precise definition.

A countable ordinal f is constructive if f = |z| for some z e S1. Note that directly from the definition, the constructive ordinals form an initial segment of the set of countable ordinals. Their supremum is a “constructive analog” of the first uncountable ordinal it is a fundamental constant of definability theory and it can be characterized in many natural ways, including the following early result:

Theorem 5.2.1 (Markwald , Spector ) An ordinal % is constructive if and only if it is finite or the order type of a recursive wellordering of N. 

•  Kleene’s obtuse coding (the 3 and 5 in the definition) is motivated by the plans he and Churchhad to develop a general “constructive theory of ordinals” beyond Cantor’s first and second numberclasses. They never got into this, but some (non-trivial and highly technical) results were provedby others, cf. Kreider and Rogers , Putnam , Enderton-Putnam . We will not cover thistopic here.
•  O and s^o are defined by a (simultaneous) inductive definition as in App 10 which (in Kleene’swords) “is regarded from the finitary point of view as a correction, in that it eliminates the presupposition of the classical (non-constructive) second number class”. There are problems with this view,partly because many results about constructive ordinals cannot be proved (or even stated) withoutreferring to ordinals. In any case, we will use S1 here.
•  A proof of this basic fact is included in §8 of Moschovakis .
•  For a discussion of the Spector Uniqueness Theorem and an outline of its proof for S1 see §9of Moschovakis .