Dmytro Taranovsky
Last Update: January 10, 2014

Ordinal Notation

Outline: We define strong yet simple ordinal notation systems. The first section defines the general structure for the notations. The notation system in the second section reaches ATR0 plus "for every ordinal a, there is recursively a-inaccessible ordinal." The third section reaches substantially beyond KP + Πn reflection. The fourth section (attempt to reach second order arithmetic) is retained for historical purposes. The final section proposes and analyzes an ordinal notation system for second order arithmetic.
Update (Jan 9, 2014): See update / correction at the end of the paper.
Note: Some of the results here were reached by intuitive reasoning without formal proofs.
Note: A python module/program that implements comparison and ordinal arithmetic for the ordinal notation system for second order arithmetic is available here. (See "One Variable C" subsection of the paper for a notational difference with the module.)

Historical Note: In 2005, I discovered the right general form of C, defined a notation system at the level of a-recursively inaccessible ordinals, and proposed a schema (a detailed idea) for reaching second order arithmetic (August 7, 2005 version of the paper). In 2006 (or possibly late 2005) (January 24, 2006 version), I defined the stronger (n=2) notation system, and (June 28, 2009 revision) added the comparison algorithm subsection (the algorithm was previously given implicitly). Finally, in March 16, 2012 revision, I added the ordinal notation system for second order arithmetic.

A Framework for Ordinal Notations

Definition of the General Notation

In this paper, we define several ordinal notation systems based on the general notion of degree and the corresponding collapsing function C.

Definition: A degree for a well-ordered set S is a binary relation on S such that

  1. Every element a has degree 0S (the least element of S). 0S only has degree 0S.
  2. For a limit b, 'a' has degree b iff it has every degree less than b.
  3. For a successor b'=b+1, either of the following holds
    • An element has degree b' iff it is a limit of elements of degree b
    • There is a limit element d ≤ b such that for every c in S, c has degree b' iff it has degree b and either c ≤ d or c is a limit of elements of degree b (or both).

The corresponding collapsing function C is defined such that:
C(a, b) is the least element above b that has degree a. C(a, b) is defined iff such an element exists.

C is called a collapsing function because typically, if a is much larger than b, then C(a, b) < a and acts as a collapse of a above b.

A partial ordinal notation system is a partial mapping O of ordinals into finite sequences of symbols and ordinals such that O(a) is undefined if a belongs to a sequence in the range of O. (Thus, ordinals are represented in terms of symbols and non-representable ordinals.)

For a partial ordinal notation system O and a collapsing function C corresponding to a degree, the standard combination of the notations is defined as follows: A well-behaved combined ordinal notation system should satisfy the following (this is not intended as a definition and can be skipped by the reader):
  1. Let Ω be the least ordinal that is above all ordinals that are represented by C-terms (a C-term is just C(…, …)). C(a, b) is defined whenever a and b are representable and min(a, b) < Ω (except possibly when b≥Ω and b+ωa is above all ordinals in the notation system).
  2. Let a be the least ordinal represented by a C-term and Ω as above. If a ≤ C(b,c) < Ω and b is maximal and c is minimal in C(b, c), then C(b, c) is represented by C-term except possibly when c=0 and b is not represented by a C-term.
    Note: In general, we can stack ordinal notation systems on top of each other. For example, we can use one system for ordinals below Ω, and another system for representing ordinals above Ω in terms of ordinals below Ω.
  3. The standard representation of an ordinal is the unique representation using (C and 0) with the least number of C-terms. This should hold even if all representable ordinals below a particular one were to be added to O as constant symbols.

An example is the notation system below ε0 generated using 0 as the least ordinal and C(a, b) = b+ωa. The standard representation is analogous to Cantor normal form. Another example is generated by 0, x→εx, and C with C(a, b) = b+ωa.
Each of the notation systems in this paper can also be built on top of an arbitrary ordinal by representing all ordinals below that one by a constant.

A notation system above a generic ordinal specifies standardness and comparison given syntactic form and comparison for inputs. For example, pairing gives a notation system for Ω2 given a system for Ω, and comparison of (a,b) with (c,d) depends only on how a,b,c,d compare with each other. (Note: While not necessary here, it may be convenient to relax the definition of ordinal notation system above a generic ordinal by allowing comparison with 0 and possibly other queries.) Notation systems in this paper can generally be defined above a generic ordinal. Furthermore, the general form of some constructs is a mapping that given an ordinal notation system above a generic ordinal, turns it into a stronger one.

Basic Properties

Using the general definition, we can prove a variety of properties of C. Without loss of generality, we will assume in the following that the well-ordered set S is an ordinal.
If b < a, then having degree a implies having degree b.
If 0 < a ≤ b, then b has degree a iff there are c and d with d ≥ a and b = c+ωd.
C(a, b) = b+ωa iff C(a, b) ≥ a.
C(a, b) is monotonic in a and b and is continuous in a.
C(a, b) > b.
If b = C(c, d) where c is maximal, then b is minimal in C(a, b) iff a≤c.
In general, if e is represented in the standard form as C(a1, C(a2,... C(am, b)...)) and f as C(c1, C(c2,... C(cn, b)...)), then e < f ⇔ (am, ... a2, a1) < (cn, ..., c2, c1) with the comparison done in lexicographical order. Also, am ≥... a2 ≥ a1.
If a is maximal in C(a, b) and b ≤ d, then a is maximal in C(a, d).

If a is maximal in C(a, b), then C(a, b) < C(c, d) iff C(a, b) ≤ d or (b < C(c, d) and a < c).
Since the standard form requires a to be maximal in C(a, b), the above equivalence leads to a polynomial time comparison algorithm for ordinals in the notation system assuming that we can compare a and b when "a" is a constant or is otherwise not a C-term.
Note that to evaluate C(a, b) < C(c, d), c need not be maximal in C(c, d). In fact, recursive definitions of maximality will often involve such comparisons.

Bachmann-Howard Ordinal

We illustrate the framework by defining a notation system at the level of the Bachmann-Howard ordinal. The notation system will consist of C (as above) and two constants: 0 (the least ordinal) and Ω with C(a, b) < Ω if b < Ω. At this point, the notation system is fully specified except for the definition of when a is maximal in C(a, b). On the other hand, at this point the system is fully general in that by choosing the maximality condition, we can reach arbitrarily high recursive ordinals. Note that the definition of maximality cannot affect comparison of ordinals in the standard representation. Instead, it determines which representations are standard. To reach the Bachmann-Howard ordinal, define a to be maximal in C(a, b) iff its standard representation (equivalently, some representation) in terms of ordinals not above b (equivalently, ordinals below C(a, b)) only uses ordinals below a.

Consequently, for C(Ω*a+b, c) (a, b, c < Ω), we have either Ω*a+b or Ω*(a+1) or Ω2is maximal. C(Ω2, c) is the least ordinal in the range of Γ above c. If Ω*a+b is maximal and a > 0, then C(Ω*a+b, c) is point number ωb above c in the range if the ath fixpoint function (ε is the first fixpoint function).

If H(a, b) is the defined as the least set of ordinals including Ω and all ordinals below b and closed under x,y → C(x, y) where x<a, then
C(a, b) = H(a, b+1) ∩ Ω for b < Ω. (If Ω < b, then C(a, b) = b+ωa.)
Note: H would be unchanged if "closed under x,y → C(x, y)" is replaced by "closed under x,y → C(x, y) where x is maximal and y is minimal in C(x, y)".

To convert C(a, b) to the standard form, convert a and b to the standard form, maximize a and minimize b. b can be minimized using C(x, C(y, z)) = C(x, z) if y < x and y is maximal in C(y, z) (and if b = Ω (or 0), then it is already minimal). To maximize a, if a < Ω and not already maximal, then just replace a with Ω. If a ≥ Ω (and not already maximal), then look at the standard representation of a in terms of ordinals below Ω. Find the rightmost ordinal instance whose standard representation in terms of ordinals below b+1 uses an ordinal above a. Replace that instance with Ω and delete all ordinals (including Ω) to the left of it, removing extraneous Cs (by recursively replacing C(,x) with x and deleting C(,)).
For example, if b = 0 and a = Ω*ω+Γ0*2+1 = C(0, C(Γ0, C(Γ0, C(C(0, Ω), Ω)))), then out of (0, Γ0, Γ0, Γ0, 0), delete the first two and convert the third one to Ω: a → C(, C(, C(Ω, C(C(0, Ω), Ω)))) → C(Ω, C(C(0, Ω), Ω)) = Ω*(ω+1).

One Variable C

To allow more readable ordinal representations, given a definition of C, let us define C1 as
C1(a) = C1(a,0)
C1(0,b) = b
if d < ωa+1 and a is maximal in C(a,b): C1a+d,b) = C1(d, C(a,b))
if d < ωa+1 and a is not maximal in C(a,b): C1a+d,b) = C(a,b)
Note: The python module uses "C" in place of 1-variable C1, C(a, base=b) in place of C1(a, b), and "C2" in place of the 2-variable C.

Thus,

Formal definitions of ordinal notation systems tend to be simpler using C than C1 because C already takes care of addition and exponentiation, while with C1, addition and exponentiation would have to be defined separately. However, use of C1 gives much more readable representations because a single C1 can combine a long chain of Cs, and because key properties C1(a) can be read off CNF (for appropriate base) representation of a.
For example (with C as defined in the Bachmann-Howard ordinal subsection above):
εω2+ω+3 = φ(1, ω2+ω+3) = C1(Ω*(ω2+ω+3)) = C(Ω,C(Ω,C(Ω,C(Ω+1,C(Ω+2,0)))))
φ(1,φ(φ(1, ω2+ω+3),5)+6) = C1C1(Ω*(ω2+ω+3))*4+Ω*6)
As seen above, another key simplification for ordinal representations is that typically C1 can be just a one-argument function while two arguments are required for C.

The conversion between using C and using C1 is straightforward. Typically, in the standard form (and assuming that C1(a) is representable), "C1(a)" is used iff a is maximal and there is no other representation of C1(a); in particular, if "C1(a)" is standard, then C1(a) = ωC1(a). Typically, two-argument C1 is not used in standard representations. Comparison of standard forms is based on monotonicity of C1 and on C1(a) being a fix-point of exponentiation base ω. For typical C1, assuming that a is maximal in C1(a), C1(a+ωb) = ωC1(a+ωb) ⇔ ∃x≤b x=ωx > C1(a).

Degrees of Recursive Inaccessibility

In this section, we define an ordinal notation system for rudimentary set theory plus "for every ordinal a, there is recursively a-inaccessible ordinal". Note that instead of rudimentary set theory (a set theoretical analogue of ACA0), we can use a stronger theory like Π11-CA0.

Definition of the Notation

The notation is built from the constant 0 (the least ordinal) and a function C as follows:

  1. C(a, b, c) is the least ordinal e of admissibility degree a that is above c and is not in H(b, e).
  2. H(b, e) is the least set of ordinals that contains all members of e, and is closed under h, i, j → C(h, i, j) where i < b.
  3. If an ordinal e is of admissibility degree a, then C(h, i, j) < e whenever h < a and j < e. 0 is of admissibility degree 0.

A canonical notion of admissibility degrees is:
3'. Ordinals of admissibility degree a+1 are the recursively a-inaccessible ordinals and their limits.
For limit a, having admissibility degree a is the same as having every admissibility degree below a.
(An ordinal is recursively a-inaccessible iff it is admissible >ω and for every b < a is a limit of recursively b-inaccessible ordinals.).

1, 2, and 3 define the comparison relation for ordinals in the notation. 1, 2, and 3' uniquely fix C and imply 3.

Interpretation: C(a, b, c) is the least ordinal above c of degree a that is not reachable from below using "collapses" of ordinals less than b. If C(a, b, c) < b, then C(a, b, c) may be viewed as a collapse of b above c.
Note: The pair (a, b) may be viewed as a degree in a similar sense as degrees in the General Notation section.

Comparison Relation

A polynomial time comparison algorithm is obtained as follows:

  1. In C(a, b, c), treat (a, b) like an ordinal and use the comparison relation in the General Notation section. Specifically, if a and b are maximal in C(a, b, c), then C(a, b, c) < C(d, e, f) iff C(a, b, c) ≤ f or (c < C(d, e, f) and (a, b) < (c, d)
    Note: (a, b) < (c, d) iff a < c, or a = c and b < d.
  2. a is always maximal in C(a, b, c).
  3. b is maximal in e = C(a, b, c) iff b is in H(b, e).
  4. k is in H(b, e) iff k < e,  or  k = C(g, h, i), h is maximal, i is minimal, each of g, h, i is in H(b, e), and h < b.

Instead of 3 and 4, we can use the following: b is maximal in C(a, b, c) iff it has a representation (equivalently, standard representation) in terms of ordinals below C(a, b, c) (used as constants) using only ordinals below b.

Examples

Here are some examples where C(a, b)=C(0, a, b), and x+=C(1, 0, x) (the next admissible ordinal above x):
C(0, x) = x+1,
C(b, c) = H(b, c+1) ∩ c+, so
C(b, c) is the least ordinal not in H(b, c+1).
However, C(1, 0+, 0) is greater than C(1, ε0, 0), the least ordinal of admissibility degree 1 that is not in H(0+, 1).
C(b, c) = min(c+ωb, C(c+, c)) if b < c+,
C(a+, a) is the least fixed point of x → ωx above a.
{x: c < x < C(a, b, c) and x has admissibility degree a} has order type 0 if b=0 and min(ωb, C(a, b, c)) otherwise.
C(a, C(a+1, 0, b), b) is the least ordinal c above b such that there are c ordinals <c of admissibility degree a.
C((0+)2, 0) = Γ0.
C((0+)ω, 0) is the small Veblen Ordinal, and C((0+)0+, 0) is the large Veblen ordinal.
C(0++, 0) is the Bachmann-Howard ordinal.
C(C(1, 1, 0), 0) is the proof-theoretical ordinal of Π11-CA0.
C(C(1, 1, 0)+, 0) is the ordinal for Π11-CA + TI.
C(C(2, 0, 0), 0) is the ordinal for Π11 Transfinite Recursion (with induction limited to sets).
C(C(2, 0, 0)+, 0) is the ordinal for KPi.
C(C(3, 0, 0)+, 0) is the ordinal for KP + a proper class of recursively inaccessible cardinals, which (in the absence of uncountable sets) is probably equivalent to KP + Σ11 Monotonic Induction.

Degrees of Reflection

Definition

We define a strong ordinal notation system as follows. Let Ω be a large ordinal and let O be a notation system for ordinals in terms of ordinals below Ω (ordinals below Ω are treated as given in O). For example (and for definiteness), let O be built using Ω and C with C(a, b) = b + ωa (b ≥ Ω; in the standard form b = Ω or b ≥ max(ωa, Ω)). Other canonical examples include Cantor and Veblen normal forms base Ω.
The notation uses C(a, b) for b < Ω (which for ordinals in the notation implies C(a, b) < Ω), and O for larger ordinals, and 0 for the least ordinal. a is maximal in C(a, b) iff for every ordinal d which is included in the O representation of a, the following holds. The standard representation of d does not use ordinals that are below Ω but greater than d, excluding instances in the scope of an ordinal less than C(a, b). (If d is …f…, and f < C(a, b), then do not parse f for ordinals larger than d. If a < Ω, then d is a.) (When C is used for O, this appears to be equivalent to the n=2 notation system in the
last section.)

Examples
Using a canonical O, and setting gaps in the canonical way, we have
C(Ω*a+b, c) = C(a, b, c) of the previous notation (for a, b, c representable in that notation).
Ordinals (below Ω and with a<Ω) of degree Ωa+1 are recursively a-Mahlo ordinals (and their limits)
C(C(Ω, C(Ω2, 0)), 0) is the ordinal for KPM (KP + the universe is recursively Mahlo).
In general, for many appropriate conditions F, the ordinal for KP + "the universe is F" is C(C(Ω, a), 0) (which equals C(εa+1, 0)) where a is the least ordinal such La satisfies or can be forced to satisfy F.
However, the ordinal for KP + "for every ordinal a, there is recursively a-inaccessible ordinal" is C(C(Ω2, 0) + εa+1, 0) since C(Ω2, 0) is needed to reach a = C(Ω*C(Ω2, 0) + Ω, 0), the least ordinal a that is recursively a-inaccessible.
Ordinals below Ω of degree ΩΩ are Π3 reflecting ordinals (and their limits).
Ordinals below Ω of degree ΩΩn (n < ω) are Πn+2 reflecting ordinals and their limits (Π2 reflecting is the same thing as admissible >ω).
C(C(Ω, C(ΩΩn, 0)), 0) is the proof theoretical ordinal of KP + Πn+2 reflection (n < ω).
C(C(ΩΩω, 0), 0) is the proof theoretical ordinal of KP + {Πn reflection}n, and also apparently of ACA0 + lightface Π12 comprehension.
Ordinals above a and below Ω of degree ΩΩω*a+1 are a-stable ordinals and their limits.
C(ΩΩC(ΩΩΩ,0)+1,0) is the least ordinal a that is a-stable.
C(ΩΩΩ, 0) is the least ordinal a that is a+-stable.
C(C(ΩΩΩ,0)++, 0) is the proof theoretical ordinal of KP + stable ordinal, but ATR + TI (or even just ATR0) + lightface Π12 comprehension appears strictly stronger because the later implies that there are sufficiently many ordinals above the stable ordinal.
C(ΩΩΩ*Ω+Ω, 0) is the least ordinal a that is a+*a++a+-stable, and analogously for other ordinals.
Note: a+ is C(Ω, a) (a<Ω)
a is b-stable iff LaΣ1 La+b.

Additional Properties

An ordinal that is a limit of ordinals of maximum degree a has degree a+b iff it is a "level" b limit of ordinals of degree a. For example, C(ΩΩ2+Ω+1, 0) is the least limit of admissible limits of recursively Mahlo limits of Π3 reflecting ordinals. An ordinal below Ω has degree a+Ω iff it is not above a certain ordinal and has degree a, or it is an admissible limit or a limit of admissible limits of ordinals of degree a. An ordinal above ω and below Ω in the notation is admissible iff its maximum degree has effective cofinality Ω using O (with effective cofinality of Ω being Ω); equivalently iff it is a limit ordinal and every increasing sequence of ordinals in the notation system having that ordinal as a limit uses arbitrarily high ordinals up to the limit of O in the representation of the ordinals.
An analogous property holds for ordinals of degree a*b. For example, C(ωΩ32*2+Ω, 0) is the least ordinal that is Π2 reflecting onto ordinals that are Π3 reflecting onto ordinals that are Π3 reflecting onto Π4 reflecting ordinals.
For the complete assignment of notations to ordinals (using C for O), see the assignment of degrees for the ordinal notation system for second order arithmetic.

In the case O is based on Ω and C, a natural construction order for representable ordinals is the following: Start with 0, and then iteratively add the least ordinal that equals C(a, b) for a and b already constructed, with Ω added at stage ε0. The following properties should hold. The construction order for representable ordinals below C(Ω, 0) agrees with their ordinal order. The construction order would remain unchanged if when adding C(a, b), we required that C(a, b) is in the standard form. The order-type of the construction order equals the order type of representable ordinals below C(Ω, 0). The construction order can also be relativized by starting with all ordinals (or all representable ordinals) below a particular one; such construction order should still satisfy analogues of the above properties.

Note that we are not defining C(a, b) when both a and C(a, b) are in a gap in the notation. One possibility is to allow ordinals not representable in the notation from below (that is using lesser ordinals as constants) to have the largest possible degrees. However, in that case some ordinals below C(Ω, 0) would have every degree below Ω (which contradicts the general definition of C). Another possibility is to use such a to fill in the gaps in the notation.

The notation system can just as well be defined above an arbitrary ordinal. Since O is a parameter, we can "stack" an ordinal notation on top of "itself" any finite number of times. However, stacking the notation system on top of itself an infinite number of times would lead to an ill-founded system.

As noted previously, using C1 rather than C can improve readability. Here is an example using C1:
C1ΩΩΩ2*3+ΩΩ*4+Ω2*5+Ω*6) is the 6th admissible ordinal after the 5th recursively inaccessible ordinal after the 4th recursively-Mahlo ordinal after the 3rd recursively hyper-Mahlo ordinal after the 1st Π3 reflecting ordinal.
In C1(...+Ωa*b+...), Ωa+b corresponds to going up by b (b is count) a-recursively inaccessible ordinals and their limits; if b is above the result, it encodes how much diagonalization to take (and similarly with other ordinals above the result). If a = ...+Ωc*d+..., c encodes degree of recursive Mahloness and d encodes the number of times to take a limit operation where at successor steps the limits must correspond to c (where c encodes degree of recursive Mahloness). For example, a=Ω2+Ω*2 corresponds to recursively Mahlo limit of recursively Mahlo limits of recursively hyper-Mahlo ordinals. If c=...+Ωe*f+..., then e encodes degree of reflection and f how many times to apply the reflection; for example Ω10*2 corresponds to Π8 reflecting ordinals onto Π8 reflecting ordinals. If e≥Ω, then the use of Ω in e corresponds to the next admissible ordinal above the result of C1. Limit values of a,b,c,d,e,f are handled using the limiting process; for example C1(ΩΩω) is the least limit of recursively n-Mahlo ordinals for all finite n (and hence is not admissible).

Comparison Algorithm

In this subsection, we explicitly state the comparison algorithm and the conversion to the standard form.
For ordinals in the standard representation written in the postfix form, the comparison is done in the lexicographical order where 'C' < '0' < 'Ω': For example, C(C(0,0),0) < C(Ω, 0) because 000CC < 0ΩC. (This does not hold for non-standard representations of ordinals). The recursive test for being in the standard form is:

  1. '0' and 'Ω' are standard
  2. If 'C(a,b)' is standard, then so are 'a' and 'b'.
  3. If C('a', C('b', 'c')) is standard, then a≤b
  4. If the above tests succeeded for "C(a,b)", let Ta be the parse tree of 'a': Ta is the set of subterms of 'a', and for x and y in Ta, x<y means that y is a subterm of x and y≠x. Let Ord(x) be the ordinal coded by x. Parse 'a' into the set of terms below Ω. Formally,
    let X = {x ∈ Ta: Ord(x) < Ω ∧ ∀y<x Ord(y)≥Ω}
    The test for the standard form is:
    ∀x∈X ∀y>x (Ord(y)<Ord(x) ∨ Ord(y)≥Ω ∨ ∃z≤y Ord(z) < C(a, b))
    Note: All comparisons between ordinals here can be done in the above-described lexicographical order.

To convert 'C(a, b)' to the standard form, first convert 'a' and 'b'. Next, recursively minimize b by replacing it with d for as long as b is C(c, d) and c<a. If we are not done, then perform a right-to-left (with functions written in prefix form) preorder traversal of Ta until we find the first y that violates the above condition. Replace y with Ω, and delete everything in 'a' to the left of 'y' (except for the required number of 'C'). Convert 'a' to the standard form. 'C(a, b)' is now a standard representation.

A Step towards Second Order Arithmetic

Note: The section is retained for historical purposes, but the content is effectively superseded by the last section.

The notation system below is only slightly more powerful, yet by introducing the idea of "correctness", it brings us significantly closer to full second order arithmetic. Originally, the notation system was my attempt to reach the full second order arithmetic, yet the maximality condition used here gives a much weaker strength.

Here is the notion of correctness used in this section:
Every ordinal has correctness 0.
An ordinal a has correctness 1 if it is admissible >ω.
An ordinal a has correctness of n+1 (n>0) if it is a++-stable limit of ordinals of correctness n.
a++ is the second admissible ordinal above a.
Below, limits of ordinals of correctness n (with correctness n as defined above) will also be said to have correctness n.
A more natural notion of correctness is used in the next section.

The notation system reaches KP + {there is an ordinal of correctness n}n. This is weaker than even KP + there is a that is a+++1-stable, which is weaker than Π11-CA0 + lightface Π12 comprehension.

For every positive integer i, the constant Ωi is for the least ordinal of correctness i. (In the above, Ω corresponds to Ω2.) C(a, b) has correctness n>0 iff there is c with correctness n+1 and b < c ≤ a. Every ordinal has correctness 0, and if m < n, every ordinal of correctness n has correctness m.
Thus, if an ordinal a has a positive but not infinite correctness n, b < a, and d is less than the least ordinal above a of correctness n+1, then C(d, b) < a.

For Ω of correctness at least two, the maximality condition in the notation in the previous section is a necessary but not a sufficient one. We propose the following condition, which implies the previous one.

If C(a, b) has maximum correctness n>0, let Ω be the least ordinal above b of correctness n+1, and Ω' the least ordinal above b of correctness n+2. Thus, we have Ω ≤ a < Ω'. For maximality of a, we require that the standard representation of a does not use ordinals that are above a but below Ω' except in the scope of an ordinal less than Ω. In addition, as in the previous section, parse "a" from the root to branches until a constant or an ordinal below Ω is reached on every branch (at this stage, do not parse the ordinals below Ω). For every such ordinal d < Ω, we require that its standard form does not use ordinals strictly between d and Ω except in the scope of an ordinal less than C(a, b). If C(a, b) only has correctness 0, we simply require that the standard form of a does not use ordinals strictly between a and Ω except in the scope of an ordinal less than C(a, b), where Ω is the least ordinal above b of correctness 2.

The least ordinal of correctness n>0 above b equals f(i-n)i) whenever n≤i and Ωi>b and f(x)=C(x, b).
0 < Ω1 < Ω2 < …
C(a, b) < Ωi iff b < Ωi and a < Ωi+1.
C(a, b) = Ωi iff b < Ωi and a = Ωi+1.
The maximum degree of C(a, b) can be found by relying on the Ω ≤ a < Ω' above.
Ωi is always maximal in C(Ωi, b) (and as always, 0 is maximal in C(0, b)). The leads to a polynomial time algorithm for checking whether a particular representation is standard, and for comparing ordinals in the standard form. I conjecture that there is also a polynomial time algorithm for converting arbitrary C-terms to the standard form.

Examples:
If a has correctness n>0 (but not infinite correctness) and b is the least ordinal above a of correctness n and c < a, then C(εa + 1, c) = C(b, c).
C(Ωn+1*2, 0) is the least admissible limit of ordinals of correctness n.
C(Ωn+12, 0) is the least recursively Mahlo limit of ordinals of correctness n.
If a is the least ordinal above b of correctness n+1, then C(a+a, b) is the least admissible limit of ordinals of correctness n above b, and analogously with other large ordinal properties.

Ordinal Notation System for Second Order Arithmetic

Definition and Basic Properties

Definition: An ordinal a is 0-built from below from b iff a≤b
a is n+1-built from below from b iff the standard representation of a does not use ordinals above a except in the scope of an ordinal n-built from below from b.
(Note: "in the scope of" means "as a subterm of".)

The nth (n is a positive integer) ordinal notation system is defined as follows.
Syntax: Two constants (0, Ωn) and a binary function C.
Comparison: For ordinals in the standard representation written in the postfix form, the comparison is done in the lexicographical order where 'C' < '0' < 'Ωn': For example, C(C(0,0),0) < C(Ωn, 0) because 000CC < 0ΩnC.
Standard Form:
0, Ωn are standard
"C(a, b)" is standard iff
1. "a" and "b" are standard,
2. b is 0 or Ωn or "C(c, d)" with a≤c, and
3. a in n-built from below from b.

Notes:
* For b < Ωn, clearly Ωn is 1-built from below from b but not 0 built from below from b.
* An equivalent form of 3 (see proof below) is that a is n-built from below from <C(a,b) where c<C(a,b) is checked in the usual lexicographical order.

For n=1, this is the notation system for Bachmann-Howard ordinal given in the introduction, and for n=2, the notation system appears to be equivalent to the one in Degrees of Reflection section. I conjecture that the strength of the nth ordinal notation system is between Π1n-1-CA and Π1n-CA0 (see the previous section for detailed correspondence), and thus the sum of the order types of these ordinal notation systems is the proof-theoretical ordinal of second order arithmetic.

The ordinal notation systems are best combined into one system as follows:
Constants 0 and Ωi (for every positive integer i), and binary function C.
Ωi = C(Ωi+1, 0) and the standard form always uses Ωi instead of C(Ωi+1, 0).
To check for standard form and compare ordinals use Ωi = C(Ωi+1, 0) to convert each Ω to Ωn for a single positive integer n (it does not matter which n) and then use the nth ordinal notation system.

To make C a total function for a and b in the notation system, let C(a, b) be the least ordinal of degree ≥a above b, where the degree of Ωi is Ωi+1 and the degree of C(c,d) is c if "C(c,d)" is the standard form. I believe that this is recursive with the comparison conversion as follows.

Conjectured conversion to the standard form for the nth notation system: To convert 'C(a, b)' to the standard form, first convert 'a' and 'b'. Next, recursively minimize b by replacing it with d for as long as b is C(c, d) and c<a. If a is not n-built from below from b, then perform an in-order right-to-left traversal of the term tree of a to find the first counterexample: a < a1 < a2 ... < an (ai+1 is a subterm of ai). This occurrence of an is part of C(an, d) with C(an, d) < Ωn. Replace this C(an, d) with Ωn, and delete everything to the left of this Ωn, and add the right number of 'C(' to make the new 'a' a valid term, and convert the new 'a' to the standard form.
Note: By converting between different Ωi, the conversion for the full notation system follows.

Proof that of the equivalence of the alternative form of 3 (a is n-built from below from <C(a,b)) in the definition of the standard form:
Let "C(a, b)" be a counterexample, and let c be the least ordinal such that a is n-built from below from c. c is a subterm of a (hence proving its existence does not require proving that the notation system is well-founded) and b<c<C(a, b), and c = C(d, e) (standard form) with d<a and e≥b. By the minimality of c, c must be a counterexample to a being n-built from below from <c, which contradicts d<a and d being n-built from below from <c.

Also, computer search shows (or strongly suggests) that in defining the system, without affecting the set of standard terms, n+1-built from below can be weakened as follows: a is n+1-built from below from b if the representation of a does not use ordinals above a except in the scope of an ordinal n-built from below from b, where in representing C(c,d) for c<a, one only counts C(c,d) and ordinals ≤d and their subterms.

Regarding C1, a natural condition (in the nth notation system) for a to be maximal in C1(a) might be that a is n-built from below, but that is not equivalent to the system defined above.

Analysis and Examples

Note: The ordinal assignments in this section might be wrong; see "Update" below.

To correctly set the gaps in the notation system, we introduce the notion of correctness. Let ρ be an ordinal such that Lρ satisfies ZFC minus power set. For definiteness, let ρ be ω1L since second order arithmetic does not prove existence ρ with Lρ satisfying ZFC\P, but it proves as a schema that Lω1L satisfies ZFC\P.

For every positive integer i, the constant Ωi should be assigned to the least ordinal of correctness i. (In Degrees of Reflection section, Ω corresponds to Ω2.) C(a, b) has correctness n>0 iff there is c with correctness n+1 and b < c ≤ a. Every ordinal has correctness 0, and if m < n, every ordinal of correctness n has correctness m.
Thus, if an ordinal a has a positive but not infinite correctness n, b < a, and d is less than the least ordinal above a of correctness n+1, then C(d, b) < a.
The least ordinal of correctness n>0 above b equals f(i-n)i) whenever n≤i and Ωi>b and f(x)=C(x, b).
0 < Ω1 < Ω2 < …
C(a, b) < Ωi iff b < Ωi and a < Ωi+1.
C(a, b) = Ωi iff b < Ωi and a = Ωi+1.

After Πn reflecting ordinals, the next set theoretical concept is that of stability. Here are ordinals corresponding to different levels of stability.
C(Ω2+,0) -- the least ordinal a that is stable up to εa++1 (note that Ω2+ equals C(C(Ω32),Ω2))
C(C(Ω32),0) -- the least ordinal stable up to 2 admissible ordinals
C(C(Ω32)*Ω2,0) -- the least ordinal that is Π2 reflecting onto ordinals that are stable up to two admissible ordinals, and similarly with other levels of reflection
C(C(Ω3,C(Ω32)),0) -- the least ordinal stable up to 3 admissible ordinals, and so on
C(C(Ω32,0),0) -- the least ordinal stable up to a recursively inaccessible ordinal
C(C(Ω322,0),0) -- the least ordinal stable up to a recursively Mahlo ordinal, and so on
C(C(Ω3+C(Ω32),0),0) -- the least ordinal that is stable up to a larger ordinal that is stable up to two admissible ordinals
C(C(C(Ω3*2,0),0),0) -- proof theoretical ordinal of Π12-CA0
C(C(Ω3*2,0)+1,0) -- the least ordinal a such that La models KP + Σ1 separation (which has the same strength as Π12-CA + TI), so its proof theoretical ordinal appears to be C(C(C(Ω3*2,0)+1,0)+, 0).
C(C(C(Ω30,0),0),0) may be the proof theoretical ordinal of Δ13-CA, which has the same strength as KP + {there is a Σ1 elementary chain of length a: a0}.

Possible Alternative

One issue with the notation system is that while C(Ωn+1+1, 0) (n>0) is the height of the least Σ1n-correct model of Π1n-CA, the collapse C(C(Ω3+1, 0), 0) corresponds to a weaker theory than Π12-CA0. The cause of this is our maximality condition for degrees which causes for example C(εΩ2+1, 0) to equal C(Ω2+, 0). If we could devise a corresponding notation system that distinguishes such terms, here are guesses for some of the proof theoretical ordinals:
For n>0, C(…C(Ωn+1+1, 0)…, 0) (with n+1 Cs) -- the ordinal for Π1n-CA0.
C(C(C(Ω3, C(Ω3+1, 0)), 0), 0) -- the ordinal for Π12-CA + TI.
C(Ω3*2, 0) -- the least ordinal κ of correctness 2 with Lκ satisfying KP + Δ2 separation.
C(C(C(Ω3*2, 0), 0), 0) -- the ordinal for Π12-TR0.
C(C(C(Ω3, C(Ω3*2, 0)), 0), 0) -- the ordinal for Δ13-CA + TI.

Assignment of Degrees

This section gives a partial definition of degrees for arbitrary ordinals, including those not in the notation system. In turn, the definition of degrees (to the extent that it is complete) allows us to define how to correctly set gaps in the notation system. For illustration purposes, we start with a relatively simple fragment.

Let a = C(b, c) (standard representation) be an ordinal >ω in the notation system and Ω the least ordinal above a of correctness 2 and assume b<εΩ+1. a is admissible iff the critical sequence of b using Cantor Normal Form base Ω has length Ω. a is recursively f-Mahlo iff it is admissible and b is of the form ...+Ωd*e (Cantor Normal Form base Ω) where d>f and f≤a. (Note: recursively 0-Mahlo means admissible >ω and recursively f-Mahlo (f>0) means Π2 reflecting onto g-Mahlo ordinals for every g<f.) If a < C(Ω2C(Ω2Ω2, 0)+2, 0), then a is assigned to the least ordinal consistent with its degree of Mahloness and assignment of notations below a.

Also, if h is an ordinal, then the notation system can be defined above h treating all ordinals ≤h as constants (and with representations for ordinals above h in terms of ordinals <h agreeing with the standard representations). If a < C(ΩC(ΩΩ, h)+2, h) (a>h and Ω is the least ordinal above a of correctness 2), then a is assigned to the least ordinal consistent with its degree of Mahloness and assignment of notations below a.

To go beyond this fragment, let x be an ordinal, and construct the ordinal notation system above x using ordinals <x as constant symbols. Because we have not completely defined the gaps in the notation, degrees will be terms denoting ordinals in the notation. Furthermore, not all degrees will necessarily be defined for all ordinals below x (for example, we can have y<x and a degree using an ordinal <x above y), but assuming that x is limit (otherwise, it only has degree 0), given a degree d, the property of having degree d can be defined for all sufficiently large ordinals below x, which suffices for our purposes.
Note: If x > ω1L, then for defining correctness above x, ρ can be the least L-cardinal >x.

Let Ω be the least ordinal above x of correctness 2, and assume that the maximum degree of x is below εΩ+1. Also assume that x is limit. Every ordinal has degree 0. Let us say that d is <x maximal if for all sufficiently large y<x, d is maximal in C(d, y) (equivalently if there is y<x such that y is above all ordinals <x included in d and d is maximal in C(d, y)). x has degree d+1 iff x has degree d and (1) x is a limit of ordinals of degree d or (2) d is not <x maximal. If d is a limit and the critical sequence of d using Cantor Normal Form base Ω has length <Ω, then x has degree d iff it has every degree below d. (The length is required to be <Ω because our notation system has gaps.) Otherwise, let d' be the least degree ≥d that is <x maximal. x has degree d iff it has degree d'. d' has the form e + Ωf (additive decomposition) where f is successor or is ≥Ω. x has degree d iff x has admissibility degree f' and is a limit of ordinals of degree e, or a limit of such ordinals (that is a limit of ordinals of admissibility degree f' that are limits of ordinals of degree e), where f' is such that fdeg(f')=Ωf (so f' is f or f-1; fdeg is defined below). This reduces assignment of degrees (below εΩ+1) to that of admissibility degrees. (Note: The notion of admissibility degrees used here corresponds to degrees of recursive Mahloness and beyond and not degrees of recursive inaccessibility.)

We do not have the full definition of admissibility degrees, but for a partial definition, assume that the admissibility degree d is <εΩ+1 (note that we do not prohibit x from having degree (as opposed to admissibility degree) ≥εΩ+1). Every ordinal has admissibility degree 0. Let fdeg be the function converting admissibility degrees to degrees: fdeg(d) = Ωd, except that if d is a limit with critical sequence (using CNF base Ω) shorter than Ω, or if d is such a limit plus a finite ordinal, then fdeg(d)=Ωd+1. d has the form (CNF base Ω) e + Ωf*g. x has admissibility degree d iff
Case A: g is limit or fdeg(d) is not <x maximal. x has admissibility degree e + Ωf*h for every representable h<g (equivalently, for cofinally many h<g).
Case B: g is successor and fdeg(d) is <x maximal. x is Π2+f' reflecting onto ordinals of admissibility degree e + Ωf*(g-1) (g-1 is the predecessor of g) where f' is derived from f as follows:
- Let f1 be the order type of {h: fdeg(e + Ωf*(g-1)+Ωh) is <x maximal and h is a representable ordinal <f} (so f' = f1 = f if f≤x)
- Let y be the order type of representable ordinals below C(Ω, x). Express f1 using CNF base y and then change CNF to base x+ (the least admissible ordinal above x) to get f' (so f' = f1 if f<Ω).

Notes:
* For a>0, Πω*a reflecting means a-stable, and Πω*a+n reflection of x is defined using reflection of Lx+a onto an ordinal below x for the appropriate set of formulas. The definition for reflection onto a class of ordinals is analogous.
* To clarify, the degrees are arbitrary terms involving ordinals <x, 'C', Ω, and Ωi (i>2) where Ωi is the least ordinal of correctness i above Ω. In our assignment, there is some indeterminacy about comparison, specifically about how to compare certain terms with x (and ordinals below x). However, given an ordinal y, we still have unique assignment of degrees to ordinals below C(εΩ+1, y) (Ω is the least ordinal above y of correctness 2) where C(a, b) is only used for b≥y and ordinals ≤y are represented as themselves.

Beyond Second Order Arithmetic

Note: The contents of this subsection are speculative.
Also, as described in the Update section below, the standard C above might already capture ZFC and beyond.

To go beyond second order arithmetic, we need transfinitely many degrees of correctness. Cardinals will be ordinals that cannot be reached from below no matter how large the degree of correctness is. Let Ω be the least uncountable cardinal and b a countable ordinal, as computed in the model (specifically, in L). If a < b, then b having correctness ω*(a+1) may be defined as Lb+a being elementarily embeddable LΩ+a. Correctness Ω+ω may correspond to Lb+b being elementarily embeddable in LΩ+Ω, and similarly for Ω2+ω and LΩ*Ω, and so on.

For a notation system, we can try to use a total ternary function C such that C(a, b, c) is the least ordinal above c of correctness a and for that correctness of degree b. If we treat (a, b) like an ordinal, then the function satisfies formal requirements of C (as described in the general notation), so the only issue is specifying when (a, b) is maximal. For a=0, the maximality of b is arguably like in the second section (that is the standard form of b uses only ordinals below b), but the general case is unclear.

I do not have the conditions for a and b in the presence of uncountable cardinals. However, roughly speaking, the condition for a is being definable from below from <C(a,b,c). If a'<a, then C(a',b,c) is definable in LΩ+a for every representable value of b provided that c < Ω and a' and c are definable in LΩ+a (Ω+a (in both instances) is not sharp here, but it communicates the idea).

I also note that, for every finite n, to get an ordinal notation system for ZFC\P + "ωn exists", it is sufficient to describe an ordinal notation system for ordinals between ωn and ωn+1 where ordinals ≤ωn are given as constants and ordinals ≥wn+1 are represented in terms of ordinals <ωn+1 using a given notation system O. One can then stack the resulting systems on top of each other any finite (but fixed) number of times to get the full system for a particular n.

If the definition of C(a,b,c) is worked out, one can extend the system by adding a function that enumerates L-cardinals (or just cardinals). To get inaccessible cardinals, one can use constant 0 and a 4-variable C(a,b,c,d) where a indicates degree of inaccessibility. One guess is that going beyond 4-variables corresponds to higher order set theory, and that the strength for finite variable C corresponds to ZFC + {n-ineffable: n<ω} (plus a conservative higher order set theory extension to extend Ord to match the notation system). One can go further by adding ordinal Ω and using higher ordinals in place of n-tuples. To go still further, one would use Ω1, Ω2, ..., (analogously to the notation system for second order arithmetic) with the hope/ideal to capture second order arithmetic plus projective determinacy. However, we are still far from that.

One approach to find ordinal notation systems for ZFC and beyond is to find a set of functions that is rich enough to capture the set-existence principles but tame enough for comparison to be recursive. Let us start with 0, ordinal addition, ordinal exponentiation base ω, and add aleph function that enumerates infinite cardinals as computed in L. A key property of uncountable cardinals is unreachability from below; for example, every infinite model has a countable submodel. So to capture the unreachability, let us add function f: f(a, b) → the least ordinal c such that c is not definable in La using parameters ≤b.

Two questions to ask are:
Is the resulting ordinal representation system recursive? (That is, is there an algorithm for comparing terms?)
If yes, how strong is the resulting system? Does it capture the full strength of the underlying set theory or does it correspond to recursive analogue (of cardinals) or something in between?

If f is not sufficient, one can try a full collapsing mapping and instead of just its critical point:
Coll(a, b) → the collapsing mapping for least elementary submodel of La that contains all ordinals ≤b (and in that case, include terms like Coll(a,b)(c) in the notation system)

To try to reach ZFC and beyond, we can add a 3-variable function
f: f(a, b, c) → the least a-inaccessible (in L) L-cardinal k > c that that is not definable in L_b using parameters <k
and ask whether the resulting representation system is still recursive, and if so, what is its strength.

To (try to) go to levels of indescribability, one can add function
g: g(a, b, c) → the least cardinal d > c such that for some cardinal e>d, there is elementary embedding j:Coll(e, d)(Le) → La with crit(j) = d and j(d) = b. To (try to) get to n-ineffable cardinals for all n<ω, one can use a predicate for n-reflective cardinals as computed in L (see "Higher Order Set Theory with Reflective Cardinals" by the same author), and define g1, g2, ... that are like g except that Coll and j must also be elementary with respect to n-reflective cardinals (for n<i for gi), but allowing Coll and j to "move" the predicates for reflective cardinals by application.
To go beyond that, one would use mice and the associated embeddings.

An Example

To inspire future work, here is how a notation system (for ZFC+{n-ineffable}n<ω) might look like, though it would be lucky if this particular system is well-founded and has the right strength. The system uses constant 0 and multivariable C. C(a1, a2, ..., an, b) corresponds to 2-variable C((a1, ..., an), b) if (a1, ..., an) is treated as an ordinal with lexicographical comparison, where after all leading 0s are removed a longer sequence is larger than a shorter one and (a1)=a1 and standard form prohibits a1=0. Thus (as written in Basic Properties section for general C), it suffices to state the maximality condition.
(a1, ..., an) is maximal in C(a1, ..., an, b) iff for each i 1≤i≤n, ai is <(a1, ..., an) built from below from <C(a1, ..., an, b).
a is <b built from below from <c if for every subterm ei of a where ei is is part of C(e1, ..., em, f) (as an immediate subterm in the term tree of a) and ei>a and on the path from a to ei all ordinals are ≥c and ≤a, we have (e1,...,em) < b and ei is <b built from below from <c.
The hierarchy is a bit different from the notation systems in previous sections. If d=C(1,0,C(2,0,0)), the least recursively inaccessible ordinal should be C(1,d,0), least admissible limit of recursively inaccessibles should be C(1,d*2,0), least recursively Mahlo C(1,d2,0), and so on.
Instead of n-tuples (as in (a1, ..., an)), we can use a stronger notation system — the construction can be formally generalized into a mapping that turns ordinal notation systems above generic ordinals (notation system above a generic ordinal is defined earlier in the paper) into stronger ones. As a particular example, we can use 2-variable C (in place of multivariable C), 0, and a large ordinal Ω, and treat ordinals ≥Ω as syntactic constructs. (Formally, given a, let variables range over subterms of a, including their position in a, and let '⊏' denote subterm (not necessarily a proper subterm, but different positions in a are distinguished), and '<' compare variables as ordinals. The maximality condition for a in C(a,b) is ∀s,t (s<t<Ω ∧ t⊏s ∧ ¬∃u⊐s s<u<Ω ∧ ¬∃u⊐t t<u<Ω ∧ ¬∃u⊐t u<C(a,b) ⇒ ∀v⊐t (¬∃w<Ω (t⊏w⊏v ∧ w≠t ∧ w≠v) ⇒ v<a)). Also, b<Ω⇒C(a,b)<Ω.)

Remaining Work

To complete ordinal analysis of second order arithmetic, one would need:
* A canonical assignment of notations to formulas that provably in second order arithmetic denote an ordinal, and such that for every two ordinals/formulas, comparison is provable in second order arithmetic. The idea is that the notation system captures not only provably recursive ordinals of second order arithmetic but all ordinals that have a provable canonical definition in second order arithmetic. Currently, we have a complete assignment for a large fragment, including all representable ordinals below the least ordinal a that is a+ stable. A desired property (assuming that it is canonically achievable) is maximality: One cannot add an extra ordinal to the notation system, and still have provable (in second order arithmetic) comparison.
* Proof that the system is well-founded and that it has the right strength, etc. Specifically, we want:
- Proof in a weak base system of various basic properties of the recursive comparison relation.
- Proof in a weak base system that the assignment of notations to formulas (as requested in the paragraph above) satisfies the requested properties.
- (Strengthening of the previous item) A constructive proof in a weak base system and with feasible polynomial time witness that for every n, second order arithmetic proves (as a statement rather than a schema) the following statement: The assignment (as in the assignment above) of ordinal notations in the nth notation system to formulas is well-defined and order-preserving.
- Proof in a weak base system that the well-foundness of the notation system up to Ω1 is equivalent to Π11 soundness of second order arithmetic and that a slightly stronger assumption (like in ATR0 plus existence of a transitive model of second order arithmetic) suffices to prove well-foundness of the full system.
- A proof analysis of second order arithmetic that relates proofs to ordinal notations, and similarly for fragments of second order arithmetic.
- Proofs of various correspondences between fragments of the notation system and fragments of second order arithmetic.

To go beyond second order arithmetic, one would need to work out how to develop ordinal notations beyond the first ω levels of correctness, and eventually how to incorporate large cardinal properties in a tractable way.

Update

The n=2 notation system in "Ordinal Notation System for Second Order Arithmetic" is not identical to the one in "Degrees of Reflection". The notation system for degrees of inaccessibility corresponds to the one in "Degrees of Reflection". Let the standard C denote denote the notation system in "Ordinal Notation System for Second Order Arithmetic".

C(C(Ω+C(Ω*2,0),C(Ω*2,0)),0) appears to be the "least" term valid for "Degrees of reflection" C but not for the standard C. However, this does not appear to adversely affect the strength of the standard C since enough ordinals remain available for the collapse. For example, in n=2 system, for every a built from below, for every b that uses only ordinals <a, C(C(a+b,0),0) is standard (after converting a+b to the standard form).

C(Ω2C(Ω2*2,0)+1,0) appears to be the "least" term valid for the standard C but not "Degrees of Reflection" C, and the difference appears to make the standard C for n=2 much stronger than C in "Degrees of reflection". The assignment of ordinals in this paper is for the "Degrees of Reflection" system. Applying this assignment to the standard C, while valid as a formal definition, misses the full strength of the notation system.

For standard C (with Ω=Ω2), if d=C(Ω,C(Ω*2,0)), then C(Ω+d,0) should be the least recursively inaccessible ordinal. (Intuitively, since d is admissible but not limit of admissibles and for cofinally many representable e<d, C(1,e,0) is standard, C(1,d,0) should also be admissible.)
Continuing upward, C(Ω+d*2,0) should be the least recursively hyperinaccessible ordinal; C(Ω+d2) -- least recursively Mahlo, C(Ω+dd) -- least Π3 reflecting, and so on, completely analogously to the description from "Degrees of Reflection". The hierarchy suggests that C(Ω*2, 0) should be the least ordinal x such that Lx is a Σ1 elementary substructure of L, but the structure beyond that is unclear.

Here is one guess, which I include to inspire future research. C(Ω*a+b,c) corresponds with C(a,b,c) from "Beyond Second Order Arithmetic". For appropriate large a, C(ω*a+ω,0,0) is fa1L) where fa is the collapse of the Skolem hull of La. Going further, working in L (or other suitable model if L is insufficient) C(Ω2,0) corresponds to ω1. In C(Ω2+Ω*a,0), a is roughly related to the largest α such that C(Ω2+Ω*a,0) is inaccessible in LC(Ω2+Ω*a,0)+α, and for very large a, the condition might instead roughly be a-indescribable. C(Ω2+C(Ω2,C(Ω2*2,0)),0) might be the least inaccessible cardinal (compare with recursive inaccessibility). If a cardinal is subtle, then for every P there is P-indescribable cardinal below it, so C(Ω2*2,0) may be the least subtle cardinal. The least n-subtle might be C(Ω2*(n+2),0) (though C(Ωn+1,0) is also tempting). Going further, the hierarchy of ordinals above Ω possibly resembles a hierarchy of mice (in inner model theory), which (assuming zero sharp) also extends beyond Ord.

The strength of the full system for the standard C is unclear. The most optimistic plausible hypothesis is that the strength of the full system is that of second order arithmetic with projective determinacy. Allowing an ordinal to be defined from higher ordinals n-times might be analogous to mice being able to capture arbitrary reals (through genericity over iterates) n (or so) times. However, there are many plausible lower stopping points, one of which is ZFC+{n-reflective: n<ω} (same Π11 (and even ΣV2) strength as ZFC+{n-ineffable: n<ω} but with ordinals extending further), and the lowest plausible guess (assuming well-foundness) is still second order arithmetic.