Dmytro Taranovsky

Last Update: October 12, 2016

**Abstract:** We introduce a framework for ordinal notation systems, present a family of strong yet simple systems, and give many examples of ordinals in these systems. While much of the material is conjectural, we include well-foundness proof for an ordinal representation system with conjectured strength beyond Zermelo set theory.

**Outline:** We define strong yet simple ordinal notation systems as follows.

A Framework for Ordinal Notations — defines the general structure for the notations.

Definition of the General Notation

Basic Properties

Bachmann-Howard Ordinal

One Variable C

Goals of Ordinal Analysis

Degrees of Recursive Inaccessibility — presents a notation system for ATR_{0} plus "for every ordinal *a*, there is recursively *a*-inaccessible ordinal".

Definition of the Notation

Comparison Relation

Examples

Degrees of Reflection — presents a notation system that reaches substantially beyond KP + Π_{n} reflection and with the canonical setting of gaps.

Definition and Examples

Comparison Algorithm

Prior Work

Assignment of Degrees

A Step towards Second Order Arithmetic — an earlier attempt to reach second order arithmetic; retained for historical purposes.

Main Ordinal Notation System — introduces the main notation system, which was intended for second order arithmetic (Z_{2}), but the actual strength may be higher.

Definition and Basic Properties

Old Analysis and Examples

Beyond Second Order Arithmetic

Strength of the Main System — discusses strength of the main notation system.

Differences from Degrees of Reflection C

Intuitive Analysis of the Strength of C

Iteration of n-built from below — proposes a strengthening of the main system.

Built-from-below with Passthrough for Lower Levels — introduces and analyses a variation on a fragment of the main system, and proves well-foundness for a system with conjectured strength beyond Zermelo set theory.

Definition and Properties

Proof of Well-foundness

Multivariable Extensions

**Note:** Some of the results (but not theorems) here were reached by intuitive reasoning without formal proofs.

**Note:** A python module/program (OrdinalArithmetic.py) that implements comparison and ordinal arithmetic for the main ordinal notation system is available here (absolute link). See One Variable C subsection of the paper for a notational difference with the module. The reader is encouraged to try out 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 ("Degrees of Reflection") 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 main ordinal notation system, intended for second order arithmetic. Afterwards, in 2014 (Jan 9, 2014 revision), I discovered new structure in the main system and wrote an update (an initial version of Strength of the Main System). In 2015 (April 20, 2015 revision), I proposed a strengthening of the main system. August 24, 2016 revision added "Built-from-below with Passthrough for Lower Levels", and around that time, I made many improvements to the paper. Oct 9, 2016 revision extended the well-foundness proof for the passthrough system to a system with conjectured strength above Zermelo set theory. The paper was developed over time, and different sections can mostly be read independently of each other.

**Prerequisites:** The paper assumes basic understanding of ordinals, and parts of the paper assume more. A good introduction is in (Rathjen 2006).

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

- Every element
*a*has degree 0_{S}(the least element of S). 0_{S}only has degree 0_{S}. - For a limit b,
*a*has degree b iff it has every degree less than b. - 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).

**Definition:** Given a notion of degree, 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*. An alternative version of C is to require *a* to be maximal in C(a,b), making C a partial function strictly monotonic in *a*.

Intuitively, a degree indicates how closed the ordinal is. Degrees are fine-grained in that degree a+1 includes all limit points of the set of ordinals of degree *a*. For typical notions of degrees, the intuitive meaning of c having degree *a* depends not only on how large *a* is but also on the nature of the gap between c and *a*; this is necessary to preserve monotonicity. Given a typical ordinal notation system, the representation of *a* in terms of ordinals <c can be viewed as a reflection configuration with ordinals <c being parameters. Intuitively, if we increase c past certain subterms of *a*, the meaning of these subterms changes from being building blocks of the reflection configuration to that of parameters. Also, not all representations are valid as reflection configurations. Some increases in *a* correspond to diagonalization: We may have an increasing sequence of degrees a_{1},a_{2},...,a_{diag} with a_{diag} meaning c (if it is not too large relative to a_{diag}) having degree a_{c}. To preserve monotonicity; a_{i} may only be used when i<c. For i≥c, we skip a_{i} by making it equivalent to a_{diag} (and hence to a_{i}+1 and higher degrees <a_{diag}) for c.

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

- If an ordinal
*a*is in the domain of O, then represent*a*using O and the representations of ordinals in O(*a*). - Otherwise if
*a*= C(b, c) where b is maximal and c is minimal (that is b'>b ⇒ C(b', c) > C(b, c), and c' < c ⇒ C(b, c') < C(b, c)), then represent*a*through C(b, c).

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

If b < a, then having degree

If 0 < a ≤ b, then

C(a, b) = b+ω

C(a, b) is monotonic in

C(a, b) > b.

If b = C(c, d) where

In general, if

If

*Comparison*:

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.

Key to effective ordinal notation systems is managing complexity and distilling the strength into a simple form. Using C serves this goal by trivializing syntax (except which forms are standard) and comparison of standard forms while providing a general framework that one can use to achieve arbitrary strength.

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 Ω^{2}is 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 *a*th 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).

To allow more readable ordinal representations, given a definition of C, let us define C_{1} as

C_{1}(a) = C_{1}(a,0)

C_{1}(a,b) = C(a_{1},C(a_{2},... C(a_{n},b)..)) for the least ordinal ω^{an}+...+ω^{a2}+ω^{a1}≥a such that each a_{i} is maximal in C(a_{i},... C(a_{n},b)..).

(Note that the definition is unchanged by requiring a_{n}≥...≥a_{2}≥_{1}.)

Equivalent definition of C_{1}:

C_{1}(a) = C_{1}(a,0)

C_{1}(0,b) = b

if d < ω^{a+1} and *a* is maximal in C(a,b): C_{1}(ω^{a}+d,b) = C_{1}(d, C(a,b))

if d < ω^{a+1} and *a* is not maximal in C(a,b): C_{1}(ω^{a}+d,b) = C(a,b)

**Note:** The Python module uses "C" in place of 1-variable C_{1}, C(a, base=b) in place of C_{1}(a, b), and "C2" in place of the 2-variable C.

- C(a
_{1},C(a_{2},... C(a_{n},b)..)) (if each a_{i}is maximal) = C_{1}(ω^{an}+...+ω^{a2}+ω^{a1},b) - C(a, b) = C
_{1}(ω^{a}, b). - If b is fixed, C
_{1}is continuous and monotonic and onto ordinals ≥b. Also, C_{1}is monotonic in b. - If
*a*is not above the least fixpoint of exponentiation base ω above b, then C_{1}(a,b) = b+a. In all cases, C_{1}(a,b)≤b+a - If a
_{1}< a_{2}and a_{1}+b is maximal in C_{1}(a_{1}+b,c) and a_{2}is maximal in C_{1}(a_{2},c), then a_{2}+b is maximal C_{1}(a_{2}+b,c). - C
_{1}(a,b) = C_{1}(C_{1}inv(b)+a) where C_{1}inv(b) is the largest x such that C_{1}(x)=b provided that for ∃x b=C_{1}(x).

Formal definitions of ordinal notation systems tend to be simpler using C than C_{1} because C already takes care of addition and exponentiation, while with C_{1}, addition and exponentiation would have to be defined separately. However, use of C_{1} gives much more readable representations because a single C_{1} can combine a long chain of Cs, and because key properties C_{1}(a) can be read off CNF (for appropriate base) representation of *a*. Also, combining C_{1} with extended CNF (always using the maximum possible fix-point x→ω^{x} as the exponent base) has the benefit that the most significant terms are always to the left, which allows easy comparison.

For example (with C as defined in the Bachmann-Howard Ordinal subsection above):

ε_{ω2+ω+3} = φ(1, ω^{2}+ω+3) = C_{1}(Ω*(ω^{2}+ω+3)) = C(Ω,C(Ω,C(Ω,C(Ω+1,C(Ω+2,0)))))

φ(1,φ(φ(1, ω^{2}+ω+3),5)+6) = C_{1}(Ω^{C1(Ω*(ω2+ω+3))}*4+Ω*6)

As seen above, another key simplification for ordinal representations is that typically C_{1} can be just a one-argument function while two arguments are required for C.

Also, C_{1} allows using integers (including number of repetitions with the same *a*) in binary instead of unary; this shortcut can also be obtained using (for example) C_{n}(i,a,b) = C(a,...,C(a,b)..) (i *a*s).

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

Ordinal analysis of set theories gives us a qualitatively new understanding of the theories and of the infinite ordinals that appear in those theories. A good ordinal notation system captures all ordinals that have a canonical definition in the theory. If a theory is compared to a country, a good ordinal notation system can be viewed as a precise map of the country.

For simplicity, let us assume that the theory is naturally consistent with the existence of a definable function f such that ∀s∃n∈N s=f(n) (note that, for us, it suffices for s to range over ordinals). If not, we can use a conservative extension of the theory by, for example, a universal Skolem function: ∃tφ(s,t)⇒φ(s,F("φ",s)) (φ has two free variables and does not use F) (and an axiom to that effect); alternatively, for many theories, we can add proper classes or their analogues. We are also need a notion of the ordinals; for simplicity, if necessary, let us conservatively extend the theory with ordinals. Sometimes, the most natural extension is nontrivial. For example, for second order arithmetic (or ZF\P) with projective determinacy, we may want to consider Wadge ranks of projective sets instead of just countable ordinals.

In general, it is not clear what canonical means, or even, until we get a suitable ordinal notation system, that it is unambiguous. However, for recursive ordinals, canonical definitions are recursive. If the proof theoretical ordinal of a theory T (T includes Π^{1}_{1} induction) is sup(a_{n}), an example of a non-canonical definition is "sup(a_{n}) if each a_{n} exists, otherwise the largest a_{n} that exists". Intuitively, unlike provably recursive ordinals in T, this ordinal can be given a more direct definition in an extension of T.

It is often easier to skip some canonically definable ordinals, in which case we get only some of the benefit of a full ordinal analysis.

What we want from ordinal analysis of a theory T:

- A formula φ assigning notations to ordinals.

-- Ideal: Every canonically definable ordinal in T gets a notation.

- A comparison relation '≺' for the system such that provably in a weak base theory (PRA or weaker) '≺' is a polynomial-time computable linear ordering (with a polynomial-time computable domain).

-- Open ended: proof in a weak base system of various basic properties of '≺'.

-- Ideal: '≺' is as simple as possible given the strength of T (except that complexity is sometimes justified by convenience, extensibility, or other goals).

- Proof in a weak base system that ∀n∀m≺n T⊢"φ(m)<φ(n)" ('<' is the ordering of ordinals).

- Proof that the supremum of notations for recursive ordinals is the proof theoretical ordinal for T. There are several variations on this, but mainly:

-- Proof in a weak base theory that a Π^{1}_{1} statement is provable in T iff there is n≺Ω such that the statement is provable in a weak base theory plus transfinite induction on ≺ below n. Here, Ω is the notation for the least nonrecursive ordinal. This should be possible for natural T.

- (potentially open-ended) A proof theory for T that corresponds to the ordinal notation system.

- Open ended: A detailed correspondence between fragments of T (and their proof theoretical ordinals) and fragments of the notation system. Part of the assignment being canonical is existence of a natural correspondence between n and the proof theoretical ordinal of (essentially) "φ(n) exists". The correspondence is notation system dependent; φ(n) need not be recursive, but the proof ordinal is related to n.

The assignment of ordinals can be viewed not just as a formula but also as a story of the ordinals of T. Even without a proof, a detailed correspondence between the notation system and the canonical ordinals (and set-existence principles) of a theory is strong evidence that the system corresponds to the theory.

**What this Paper Accomplishes:** This paper presents and analyses several very strong ordinal notation systems presented as recursive relations. A canonical assignment is fully given for some weaker systems, and many examples of conjectured canonical assignment are given beyond that. Well-foundness is proved for some of the systems. Strength lower bounds are not proved.

In this section, we define an ordinal notation system for rudimentary set theory plus "for every ordinal *a*, there is recursively *a*-inaccessible ordinal". Rudimentary set theory consists of extensionality, foundation, empty set, and closure under rudimentary functions (as a schema, or using a selected set of rudimentary functions); assuming infinity, it is the set theoretical analog of ACA_{0}. Note that instead of rudimentary set theory, we can use a stronger theory like Π^{1}_{1}-CA_{0}.

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

- C(a, b, c) is the least ordinal
*e*of admissibility degree*a*that is above*c*and is not in H(b, e). - 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. - 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 Definition of the General Notation subsection.

A polynomial time comparison algorithm is obtained as follows:

- In C(a, b, c), treat (a, b) like an ordinal and use the comparison relation in the Definition of the General Notation subsection. 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) ∧ (a, b) < (c, d).

Note: (a, b) < (c, d) iff a < c, or a = c and b < d. *a*is always maximal in C(a, b, c).*b*is maximal in e = C(a, b, c) iff b is in H(b, e).*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.

C(0, x) = x+1,

C(b, c) = H(b, c+1) ∩ c

C(b, c) is the least ordinal not in H(b, c+1).

However, C(1, 0

C(b, c) = min(c+ω

C(a

{x: c < x < C(a, b, c) and

C(a, C(a+1, 0, b), b) is the least ordinal

C((0

C((0

C(0

C(C(1, 1, 0), 0) is the proof-theoretical ordinal of Π

C(C(1, 1, 0)

C(C(2, 0, 0), 0) is the ordinal for Π

C(C(2, 0, 0)

C(C(3, 0, 0)

**Definition:**

**Syntax:** 0 (the least ordinal), C (binary function), Ω (large ordinal), **O**.

** Condition for O:** **O** is a notation system for ordinals >Ω in terms of ordinals below Ω (ordinals below Ω are treated as given in **O**).

**Definition of C:** 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. C is as given in "A Framework for Ordinal Notations". This fully specifies the system (if we do not use gaps) apart from maximality of *a*. *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.)

**Canonical choice of O:** For definiteness, let **O** be Cantor Normal Form base Ω. Other choices include C with C(a, b) = b + ω^{a} (b ≥ Ω; in the standard form b = Ω or b ≥ max(ω^{a}, Ω)), or for a stronger system, Veblen Normal Form.

**Note:** Compared to using C, using CNF base Ω has the same strength but allows additional terms. For example, if a = Ω+d with d = d_{1}+...+d_{n} <Ω (each d_{i} is additively indecomposable and (d_{i}:1≤i≤n) is nonincreasing), we only check d rather than checking the representation of each d_{i} for ordinals >d_{i}.

**Note:** When C is used for **O**, the system is superficially similar to (but probably much weaker than) the n=2 notation system in the Main Ordinal Notation System section.

**Examples**

Here are examples using a canonical **O**, and setting gaps in the canonical way.

C(Ω*a+b, c) = C(a, b, c) of the previous notation (for a, b, c representable in that notation; **O** uses CNF base Ω).

Ordinals (below Ω and with a<Ω) of degree Ω^{a+1} are recursively *a*-Mahlo ordinals (and their limits), except that if c=C(Ω^{a+1},b)≤a, c is recursively c-Mahlo.

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 L_{a} 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 ACA_{0} + lightface Π^{1}_{2} 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 ATR_{0}) + lightface Π^{1}_{2} 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 L_{a} ⊰_{Σ1} L_{a+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(ω^{Ω3+Ω2*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 or CNF base Ω for **O**), see the Assignment of Degrees below.

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 C_{1} rather than C can improve readability. Here is an example using C_{1}:

C_{1}(Ω^{ΩΩ}+Ω^{Ω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 C_{1}(...+Ω^{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 C_{1}. Limit values of a,b,c,d,e,f are handled using the limiting process; for example C_{1}(Ω^{Ωω}) is the least limit of recursively n-Mahlo ordinals for all finite n (and hence is not admissible).

A natural extension of the system with the same strength is to use C_{1} instead of C in representing ordinals <Ω that are fix-points of x→ω^{x}. For example, in testing for standard form, in C_{1}(Ω+d), d<Ω would be parsed for ordinals >d that are below Ω and not in the scope of an ordinal <C_{1}(Ω+d).

In this subsection, we explicitly state the comparison algorithm and the conversion to the standard form (when C is used for **O**).

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:

- '0' and 'Ω' are standard
- If 'C(a,b)' is standard, then so are 'a' and 'b'.
- If C('a', C('b', 'c')) is standard, then a≤b.
- If the above tests succeeded for "C(a,b)", let T
_{a}be the parse tree of 'a': T_{a}is the set of subterms of 'a', and for x and y in T_{a}, x<y means that y is a subterm of x and y≠x. Here, identical terms at different positions are distinguished. Let Ord(x) be the ordinal coded by x. Parse 'a' into the set of terms below Ω. Formally,

let X = {x ∈ T_{a}: 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 T_{a} 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.

Prior to this system, the strongest reasonably simple system was the system for KP + Π_{3} reflection (Rathjen 1994). Rathjen also proposed stronger systems, but they are so complex that the problem of finding a reasonable ordinal notation system for those systems would be best described as only partially solved.

Superficially, Rathjen's Ψ^{ξ}_{π}(α) looks like C(a,b,c) (or C(ξ,α,π)) in "Degrees of Recursive Inaccessibility". However, while Rathjen does not go beyond ordinary built-from-below construction, he uses a trick that allows ξ to correspond to degree of recursive Mahloness instead of inaccessibility. (Actually, for simplicity his paper uses large cardinals instead of their recursive analogues. Also, while the examples below illustrate his system, I did not verify that the examples hold for all parameters.) Instead of collapsing above c, he collapses below (admissible) π. In his system, π codes both an ordinal above which to do the collapse, as well as the degree to which the resulting ordinal will be a limit of admissibles. If π is a successor admissible, the collapse will be an ordinal above π's admissible predecessor. If π is a successor recursively inaccessible, Ψ^{0}_{π}(α) will be a limit of admissible ordinals and will be above π's recursively inaccessible predecessor, and so on. Admissible ordinals below the least recursively Mahlo ordinal Ξ(2) are obtained using Ψ^{1}_{Ξ(2)}(α), which works since below Ξ(2) the degree of recursive inaccessibility is in a sense recursive. Now, for another example, suppose that π is the least recursively hyper-Mahlo limit of recursively hyper-hyper-Mahlo ordinals above the least recursively hyper-hyper-hyper-Mahlo ordinal Ξ(5). Ψ^{0}_{π}(α) ranges over non-admissible limits of recursively hyper-hyper-Mahlo ordinals above Ξ(5), Ψ^{1}_{π}(α) ranges over admissible limits of such ordinals, and Ψ^{2}_{π}(α) ranges over recursively Mahlo limits of such ordinals.

The downside is the lack of the simple monotonicity that C has, as well additional complexity when trying to extend it where simple build-from-below does not suffice.

The assignment of ordinals assumes that the notation system has gaps; otherwise, all ordinals would be recursive. In this section, we will set the gaps in the notation system in the canonical way. Pick any sufficiently closed ordinal Ω; it suffices that Ω is ε_{Ω++1}-stable (and Ω^{++}-stable should suffice for reasonable O). Alternatively, treat Ω as a syntactic construct and treat an ordinal ≥Ω either syntactically or as a pair (Ω, ordinal using Ω). We will define C(a,b) when *a* is representable using ordinals <C(a,b) as constants. This suffices for the system and allows extensions; the least ordinal that is not representable in the system is C(C(ε_{Ω+1},0),0) (using a natural extension of the system). Also, note that if b≥Ω, C(a,b)=b+ω^{a}.

C(a,b) is the least ordinal above b that has degree *a*. Thus, it suffices to define degrees. A complication to recursively defining degrees is that notations can use higher ordinals for which degrees have not yet been constructed. We work around this by defining when:

x has degree d where d is a term that uses C,Ω, and ordinals <x as constants.

The recursion will assume that degrees for ordinals <x have been constructed. Therefore, (using standard comparison for C from "A Framework for Ordinal Notations" and the criterion for maximality of *a* in C(a,b)) we have comparison for terms that use C, Ω, and ordinals <x as constants. In turn, the degree of x lets us compute C(x,b) when it is defined. Also, note that degree d makes sense for all ordinals y<x where y is above all constants used in d.

Every ordinal has degree 0. Assume that x is limit; otherwise x only 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 <Ω or d is not <x maximal, 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, the critical sequence for d using CNF base Ω has length Ω and d is <x maximal. 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 f_{deg}(f')=Ω^{f} (so f' is f or f-1; f_{deg} 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 now define admissibility degrees when the admissibility degree d is <ε_{Ω+1}, which suffices for the notation system. Every ordinal has admissibility degree 0. Let f_{deg} be the function converting admissibility degrees to degrees: f_{deg}(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 f_{deg}(d)=Ω^{d+1}. d has the form (CNF base Ω) e + Ω^{f}*g. x has admissibility degree d iff

Case A: f_{deg}(d) is not <x maximal. x has admissibility degree d' for the least d'>d such that f_{deg}(d') is <x maximal.

Case B: g is limit and f_{deg}(d) is <x maximal. x has admissibility degree e + Ω^{f}*h for every representable h<g (equivalently, for cofinally many h<g).

Case C: g is successor and f_{deg}(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 f_{1} be the order type of {h: f_{deg}(e + Ω^{f}*(g-1)+Ω^{h}) is <x maximal and h is a representable ordinal <f} (so f' = f_{1} = f if f≤x)

- Let y be the order type of representable ordinals below C(Ω, x). Express f_{1} using CNF base y and then change CNF to base x^{+} (the least admissible ordinal above x) to get f' (so f' = f_{1} if f<Ω).

**Note:** For a>0, Π_{ω*a} reflecting means a-stable, and Π_{ω*a+n} reflection of x is defined using reflection of L_{x+a} onto an ordinal below x for the appropriate set of formulas. The definition for reflection onto a class of ordinals is analogous.

If the notation system is restricted to terms below Ω^{Ω}, the assignment of gaps simplifies as follows: c = C(a,b) is the least ordinal consistent with its degree of recursive Mahloness and assignment of notations below c (here, the system is simultaneously built above all ordinals; the least notation incorrectly assigned would be C(Ω^{C(ΩΩ, 0)+2}, 0)). For every ordinal c=C(a,b) representable using lower ordinals as constants (even without the restriction on terms), c is admissible iff CNF base Ω critical sequence of *a* has length Ω, and c is recursively f-Mahlo iff it is admissible and *a* is of the form ...+Ω^{d}*e (CNF base Ω) where d>f and f≤a; recursively 0-Mahlo means admissible.

**Note:** The section is retained for historical purposes, but the content is effectively superseded by the next 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 Π^{1}_{1}-CA_{0} + lightface Π^{1}_{2} 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+1}^{2}, 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.

** 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 n^{th} (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Ω_{n}C.

**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* is n-built from below from <C(a,b) (use standard comparison to check).

**Notes:**

* For b < Ω_{n}, clearly Ω_{n} is 1-built from below from b but not 0 built from below from b.

* A variation is to require *a* to be n-built from below from ≤b, which would simplify the definition a bit but lead to arbitrary restrictions like disallowing C(Ω_{2}+C(Ω_{2}*2+**C(C(Ω _{2}*3,0),0)**,0),0) (the highlighted term is between b and C(a,b)).

For n=1, this is the notation system for Bachmann-Howard ordinal given in the introduction, and for n=2, the notation system is superficially similar to (but perhaps much stronger than) the one in Degrees of Reflection section. I conjecture (or conjectured, see Strength of the Main System below) that the strength of the n^{th} ordinal notation system is between Π^{1}_{n-1}-CA and Π^{1}_{n}-CA_{0}, and thus the sum of the order types of these ordinal notation systems is the proof-theoretical ordinal of second order arithmetic.

**Combined System:** 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 n^{th} ordinal notation system.

**Nonstandard Forms: ** 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 conversion to standard form as follows.

**Conjectured conversion to the standard form for the n ^{th} 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

An interesting, perhaps illfounded, variation is to weaken n+1-built from below 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. This allows additional terms such as C(Ω_{2}+C(Ω_{2}*2+C(**C(Ω _{2}*3,0)**,C(Ω

If the system is expressed using C_{1} (one variable C), the maximality condition on *a* in C_{1}(a) may not be the simplest. A natural variation (for the n^{th} notation system) is to require *a* to be n-built from below from <C_{1}(a) (terms use 0, Ω_{n},'+', x→ω^{x}, and C_{1} for fix-points of x→ω^{x}) and another natural variation (though it is unclear whether it is too restrictive to get the strength) is to simply require for *a* is to be n-built from below.

**Note:** The ordinal assignments in this section are likely wrong; see Strength of the Main System below. This section is retained to illustrate how assignments might look like if the system (or a similar system) corresponded to second order arithmetic.

- An ordinal κ has correctness 1 iff it is admissible >ω or is a limit of admissible ordinals.
- An ordinal κ has correctness n+1 with n>0 iff L
_{κ}is a Σ_{n}elementary substructure of L_{ρ}.

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(Ω_{3},Ω_{2}),Ω_{2}))

C(C(Ω_{3},Ω_{2}),0) -- the least ordinal stable up to 2 admissible ordinals

C(C(Ω_{3},Ω_{2})*Ω_{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(Ω_{3},Ω_{2})),0) -- the least ordinal stable up to 3 admissible ordinals, and so on

C(C(Ω_{3}+Ω_{2},0),0) -- the least ordinal stable up to a recursively inaccessible ordinal

C(C(Ω_{3}+Ω_{2}^{2},0),0) -- the least ordinal stable up to a recursively Mahlo ordinal, and so on

C(C(Ω_{3}+C(Ω_{3},Ω_{2}),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 Π^{1}_{2}-CA_{0}

C(C(Ω_{3}*2,0)+1,0) -- the least ordinal *a* such that L_{a} models KP + Σ_{1} separation (which has the same strength as Π^{1}_{2}-CA + TI), so its proof theoretical ordinal appears to be C(C(C(Ω_{3}*2,0)+1,0)^{+}, 0).

C(C(C(Ω_{3}*ε_{0},0),0),0) may be the proof theoretical ordinal of Δ^{1}_{3}-CA, which has the same strength as KP + {there is a Σ_{1} elementary chain of length *a*: *a*<ε_{0}}.

**Possible Alternative**

One issue with the notation system is that while C(Ω_{n+1}+1, 0) (n>0) is the height of the least Σ^{1}_{n}-correct model of Π^{1}_{n}-CA, the collapse C(C(Ω_{3}+1, 0), 0) corresponds to a weaker theory than Π^{1}_{2}-CA_{0}. 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 Π^{1}_{n}-CA_{0}.

C(C(C(Ω_{3}, C(Ω_{3}+1, 0)), 0), 0) -- the ordinal for Π^{1}_{2}-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 Π^{1}_{2}-TR_{0}.

C(C(C(Ω_{3}, C(Ω_{3}*2, 0)), 0), 0) -- the ordinal for Δ^{1}_{3}-CA + TI.

**Note:** The contents of this subsection are speculative.

**Update:** As described in the Strength of the Main System section below, the standard C above might already capture ZFC and beyond rather than just second order arithmetic. Also, the three variable C described here corresponds with Built-from-below with Passthrough for Lower Levels system. This section is retained for both intuitive and historical value.

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 L_{b+a} being elementarily embeddable L_{Ω+a}. Correctness Ω+ω may correspond to L_{b+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 Degrees of Recursive Inaccessibility (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 ≥w_{n+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 L_{a} 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 L_{a} 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)(L_{e}) → L_{a} 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 (reflective cardinals are defined in (Taranovsky 2012)), and define g_{1}, g_{2}, ... that are like g except that Coll and j must also be elementary with respect to n-reflective cardinals (for n<i for g_{i}), 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**

[*Update:* Iterations of n-built from below is (at present) a better candidate. Also, it is unclear whether the system is related to Built-from-below with Passthrough for Lower Levels.] 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(a_{1}, a_{2}, ..., a_{n}, b) corresponds to 2-variable C((a_{1}, ..., a_{n}), b) if (a_{1}, ..., a_{n}) 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 (a_{1})=a_{1} and standard form prohibits a_{1}=0. Thus (as written in Basic Properties section for general C), it suffices to state the maximality condition.

(a_{1}, ..., a_{n}) is maximal in C(a_{1}, ..., a_{n}, b) iff for each i 1≤i≤n, a_{i} is <(a_{1}, ..., a_{n}) built from below from <C(a_{1}, ..., a_{n}, b).

*a* is <b built from below from <c if for every subterm e_{i} of *a* where e_{i} is is part of C(e_{1}, ..., e_{m}, f) (as an immediate subterm in the term tree of a) and e_{i}>a and on the path from *a* to e_{i} all ordinals are ≥c and ≤a, we have (e_{1},...,e_{m}) < b and e_{i} 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,d^{2},0), and so on.

Instead of n-tuples (as in (a_{1}, ..., a_{n})), 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)<Ω.)

**Note:** This section first appeared as Jan 9, 2014 update/correction and was further updated Sep 22, 2016.

The n=2 notation system in Main Ordinal Notation System 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 "Main Ordinal Notation System".

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(Ω_{2}+ε_{C(Ω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(Ω+d^{2},0) -- least recursively Mahlo, C(Ω+d^{d},0) -- 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 L_{x} is a Σ_{1} elementary substructure of L, but the structure beyond that is unclear.

Similar patterns repeat at different levels of the strength hierarchy, and there are at least four plausible possibilities about the strength of the notation system: (1) not well-founded, (2) second order arithmetic, (3) rudimentary set theory + {there is n-subtle cardinal: n is a natural number}, and (4) second order arithmetic with projective determinacy (with the notation system covering canonical projective ordinals).

Here is one guess, to inspire future research. We will work in L (where V=L). The assignments might be too low if I missed structure in the notation system or too high if I missed structure in L. I assume that the n=2 system is analogous to Built-from-below with Passthrough for Lower Levels (and in effect analyze that system), and that section (below) will help the reader to understand the discussion here.

C(Ω*a+b,c) should be ordinal number b' of definability/reflection level *a* above c (here Ω is Ω_{2}). If b<C(Ω*a+b,c), then b'=ω^{b}. Otherwise, b has a canonical definition "b" (using ordinals <C(Ω*a+b,c) as constants), and b' is roughly the least ordinal corresponding to definability level *a* model of "b". For example, a=1 corresponds to transitive models, and (working in L) C(Ω+ω_{ω}^{L},0) should be the least ordinal d such that for every finite n, there is a transitive model of ZFC\P+"ω_{n} exists" below d.

For simplicity, let us analyze Σ_{2} hull of L. Here, we can have large cardinals but every set will be Σ_{2} definable (or Σ_{1} with the cardinality predicate). When *a* is sufficiently definable, c having definability level *a* corresponds to existence of structures <c of arbitrary complexity for (sufficiently definable) definability levels a'<a, allowing ordinals <c as parameters. For example, the least ordinal *κ* with L_{κ}≺_{Σ1}L is the least ordinal such that transitive models for arbitrary sufficiently satisfiable axioms exist below *κ*. Assuming the base theory gets its strength from the large cardinals it asserts, these axioms correspond to ordinals: *a* → "*a* exists" (where *a* is canonically defined from below), and the models roughly correspond with C(Ω+a,0), so C(Ω*2,0)=κ.

Approximate definability level correspondence (c=C(Ω*a+a_{1},b)):

small 1+a -- L_{c} is a Σ_{a} elementary substructure of L_{ω1} (c is countable, *a* may be transfinite, a=0 corresponds with L_{c} being admissible or limit of admissibles).

large a<Ω -- c is not Σ_{1} definable in (L_{κ+a}, ∈, Card) (Card is predicate for cardinals (in L)) allowing ordinals <c as constants, κ is the least cardinal above c.

a=Ω -- cardinals. C(Ω^{Ω}+a,0) is ω_{ωa} for *a* below the least fix-point of the aleph function.

To go further, let us list some cardinals (in L) in the increasing order below the least inaccessible cardinal λ in L:

the least κ such that V_{κ} is a model of ZFC.

the least cardinal κ such that for some α, L_{α} satisfies "P holds and κ is inaccessible" where P is some large cardinal axiom that is compatible with L.

the least κ such that V_{κ} and V_{λ} satisfy the same Σ_{2} statements.

the least κ such that V_{κ}≺_{Σ2}V_{λ}. κ is also the least fix-point of f where f(a) is the least b such that V_{b} and V_{λ} satisfy the same Σ_{2} statements with parameters in V_{a}.

the least κ such that V_{κ}≺_{Σa}V_{λ}. For large 'a', one analog of this is the supremum of ordinals <λ that are Σ_{1}(Card) definable in L_{a} using parameters <κ.

Note the parallel between these notions and ordinals ≥λ that are below λ^{+}; we assume that this analogy also applies to the notation system.

Let C(a,b,c,d) = C(Ω^{2}*a+Ω*b+c,d) and C(b,c,d) = C(0,b,c,d), and let S=C(1,1,0,0).

C(1,0,S,0) the least fix-point of x→ω_{x}.

C(1,0,C(a,0,S),0) -- approximately the least cardinal κ that is not Σ_{1}(Card) definable in L_{a} (for appropriate large *a* ) using parameters <κ. Equivalently, it is the least κ that is inaccessible in the collapse of Σ_{1}(Card) Skolem hull of L_{a} where ordinals <κ are constants.

C(1,0,S^{+},0) -- the least inaccessible cardinal; S^{+} is ω_{S+1}.

C(1,0,S^{+}+S,0) -- the least κ that is a limit of κ inaccessible cardinals.

C(1,0,S^{+}*2,0) -- the least hyperinaccessible cardinal.

C(1,0,S^{+}*C(a,0,S),0) -- approximately the least cardinal κ that is Mahlo in the collapse of Σ_{1}(Card) Skolem hull of L_{a} (for appropriate large *a*) where ordinals <κ are constants.

C(1,0,(S^{+})^{2},0) -- the least Mahlo cardinal.

C(1,0,(S^{+})^{3},0) -- the least hyper-Mahlo cardinal.

C(1,0,(S^{+})^{S+},0) -- the least greatly Mahlo cardinal.

C(1,0,a,0) -- (approximate) the least *a*-indescribable cardinal (for appropriate large *a*) .

S is the least cardinal κ such that for every S⊂κ, there is an S-indescribable cardinal <κ, which I think implies that S is the least subtle cardinal.

Let T = C(1,2,0,0).

C(1,1,C(1,0,a,T),0) -- (for appropriate large *a*) approximately the least *a*-indescribable limit of subtle cardinals.

C(1,1,C(1,1,0,T),0) -- the least subtle limit of subtle cardinals.

C(1,1,C(1,1,0,T)*T^{+},0) -- the least κ such that subtle cardinals are stationary below κ.

C(1,1,C(1,1,0,T)*C(1,0,a,T),0) -- (for appropriate large *a*) approximately the least *a*-indescribable subtle cardinal.

Past a subtle cardinal, the structure of cardinals becomes more complex. Below n-subtle cardinals, once speaks of (in a certain sense) indescribable n-tuples of cardinals. One possibility (the lowest plausible one) for the least n-subtle cardinal is C(1,n,0,0), but other possibilities (such as C(Ω^{n+1},0)) cannot yet be ruled out.

Going further (beyond L), a semirandom guess is

C(Ω_{3}*a,0) - enough structure for (approximately) *a*-reflective cardinals (reflective cardinals are defined in (Taranovsky 2012)), especially for a>ω.

C(Ω_{3}^{a+1},0) - measurable of order *a*.

Alternatively, for the full n=2 system, ordinals <Ω may correspond to countable ordinals, and higher ordinals correspond to countable mice with mouse order <ε_{ω1+1} (or <ε_{Ord+1} among all mice). (A mouse is a generalization of L_{a} for canonical inner models.) C(a,b) roughly corresponds to ordinal height of the least mouse of order a' (a' depends on b), where a' is obtained from *a* by representing *a* in terms of ordinals <Ω and replacing each term a_{i} that is too large with a_{i}', where a_{i}' corresponds to a model of the description of a_{i} with the model having definability level corresponding to the position of a_{i} in *a*. For example, if C(Ω^{i}*a,0) corresponds to iterating some mouse operator M *a* times, then for large *a* it may correspond to the least model of "a" that is closed under M.

In the nth system, we permit n drops, which corresponds to mice having, in some sense, complexity level n. Moreover, if ordinals correspond to real numbers, a drop corresponds to a quantifier, and mice capturing Σ_{n} truth correspond to about n-2 Woodin cardinals.

By iterating n-built from below, one gets a candidate stronger notation system, but its strength and well-foundess are not clear.

**Notation System:**

**Syntax:** Two constants (0, Ω) and a binary function C.

**Comparison:** Standard. (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.)

**Standard Form:**

0, Ω are standard

"C(a, b)" is standard iff

**1.** "a" and "b" are standard

**2.** b is 0 or Ω or "C(c, d)" with a≤c, and

**3.** Every a' in CNF base Ω representation of *a* is a''-n-built from below from <C(a,b). See below for definitions.

**Definitions for 3:**

**1.** In constructing the subterm tree of *a* (used below), ordinals ≥Ω are represented in Cantor Normal Form base Ω, which can be accomplished using the equation C(a,b)=b+ω^{a} iff *a* is ≤ the least fix-point of x→ω^{x} above b (the inequality always holds if b≥Ω). (Also, C(a,b)<Ω iff b <Ω.)

**2.** a'' is obtained by representing *a* in CNF base Ω and deleting all terms with significance level less than or equal that of a', where Ω^{c}*d is deleted if c or d is deleted, and '+' is deleted if d is deleted in c+d. The significance level of a term d<Ω in *a* (using CNF base Ω) is obtained by deleting everything to the right of d (but if d is inside e in Ω^{e}*f; f is replaced by 1), changing d to Ω and subtracting *a* on the left (and converting to standard form for comparison).

**3.** n=1+max(m∈N: ∃d∈Ord c=d+m), where c is the rightmost ordinal <Ω in CNF base Ω representation of *a*, where c is to the left of a' and the significance level (as defined above) of c is higher than that of a' (and c is 0 if *a* has no terms of higher significance level than that of a').

**4.** Testing for <C(a,b) can be done in the ordinary lexicographical order.

**5.** *a* is a''-0 built from below from <b iff a<b.

*a* is a''-n+1 built from below from <b iff *a* does not use ordinals <Ω above *a* except

a. as a subterm of an ordinal a''-n built from below from <b or

b. as a subterm of C(c,d) with c<a'' that is not in the scope of a subterm of C(c,d) that is ≤d.

**Notes:**

* In 5, the same ordinal may occur in several places in the subterm tree, and each occurrence is treated separately.

* In practice, one would use CNF base Ω for ordinals ≥Ω (also, one would likely prefer 1-variable C).

* Nonstandard forms can be defined in the usual way: C(a,b) is the least ordinal >b that equals C(c,d) (standard form) for c≥a. (Or if we want to make C(a,b) total in b but partial in *a*, set C(a,C(b,c))=C(a,c) if a>b, and after all these simplifications are complete, require the form to be standard.)

* A variation is to use a different ordinal notation system (instead of C) for ordinals ≥Ω. One can use an arbitrarily strong system as long as it has an appropriate structure for the combined system to work.

**Variation that does not use CNF:** Replace (3) with: Every a'<Ω in the representation of *a* in terms of ordinals <Ω (so if a<Ω, a' is a) is a''-n-built from below from <C(a,b). a'' is the part of *a* that is not affected by taking the limit a'→Ω, and n is maximal such that a'' is C(c,C(c,...)) (n-1 *c*s, each *c* must be identical), n=1 if a<Ω.

In definitions for (3), replace 1-3 with: To get the limit, which will call a_{lim}, represent *a* in prefix form, delete everything to the left of a', replace a' with Ω, add the right number of Cs on the left to make the term well-formed (not necessarily standard), and then recursively replace C(d,C(e,f)) with C(d,f) where d>e (using standard comparison). a'' (as a string) will be the largest common suffix of a and a_{lim}.

To understand the system, consider the segment that uses only C(a,b,c) = C(Ω*a+b,c) (with a,b,c <Ω). 5 requires that b is a-n-built from below from <C(a,b,c) where n is the integer part of a+1. (I use a-n in place of Ω*a-n; also in this segment *a* is automatically built from below from <C(a,b,c).) For a=n-1, this approximately corresponds with n built from below from c, which allows embedding of the main system (the one using Ω_{n}) into this segment with finite *a*. For limit *a*, the level may correspond with J_{a}(R), and then one repeats n-built from below construction but this time assuming that for lower levels definability has been completed, hence 5b. The sense of 5b is that C(c,d) is treated as representing the ordinal in terms of ordinals ≤d, and which intermediate ordinals >d are used is irrelevant.

The full system is a transfinite iteration of the above. Beyond Ω^{e} for a fixed small ordinal e, CNF base Ω becomes more complex, but using significance level should be the right generalization. In requiring a' to a''-n built from below (from <C(a,b,c)), we avoid circularity by requiring that, in a certain sense, a'' is constructed prior to a', which can be used to explain the construction of a''.

If the main notation system (that uses Ω_{n}) reaches Z_{2}+PD (otherwise, the strength here might be much lower), a reasonable hypothesis for the strength of this system below Ω^{Ω*ω} is rudimentary set theory + for every ordinal κ there are κ Woodin cardinals (with ordinals <Ω corresponding to Wadge ranks (within determinacy) that have a canonical definition in the theory). This appears to have the same strength as rudimentary set theory plus schema (n a natural number): Games on integers of countable length and projective payoff are determined, where the game consists of n rounds, with the first round having length ω and each round coding (with coding having projective complexity) the length of the next one. Ω^{a+1} may correspond with (approximately) ω*a Woodin cardinals, and Ω^{Ω+a} with (approximately) the number of Woodin cardinals equaling the value of (ω*a)th Woodin cardinal. The full system may correspond to games with a level n round (schema given n), with level m rounds consisting of level m-1 subrounds, and the number of subrounds (or number of moves for level 1 rounds) is determined at the start of each round. (This strength can also be expressed using limits of Woodin cardinals, and is well below a regular limit of Woodin cardinals.)

**Further Extensions:** While the strength can be increased slightly by going beyond ε_{Ω+1}, new construction principles are required to reach substantially further. In C(*a*,b,c), one would want to allow *a* to have a richer structure than b. Here is how it may look like, although the particular extension below is just a guess and might well be either ill-founded or failing to reach further. In 5 (above), add clause

c. or the term f (a'<f<Ω) has lower significance level in e than that of a' in *a*, where e is the outermost (without intervening C) CNF base Ω superterm of f.

(Thus, it is more accurate to say (significance level of a' in a)-a''-n built from below. The significance level is for CNF base Ω and is as defined above. If f is e, the level is Ω. One can also consider the restriction below (for example) Ω^{ω}.)

**Future:** To get to n-huge cardinals, one would want to find how to place a corresponding embedding j in a simple framework.

Here we present a strong ordinal notation system (with conjectured strength above second order arithmetic) whose well-foundness we can prove (albeit, using large cardinals). C_{i}(a,b) will be the least ordinal of reflection level i and for that level of degree *a* above b. The sense of reflection level i is that definitions for reflection levels <i have been completed in a sense that will be formalized by the notation system.

*Relation with the main system:* C_{i}(a,b) corresponds with C(Ω_{2}*i+a,b) with a,b<Ω_{2} and *a* and b representable without using ordinals ≥Ω_{2}^{2}. However, while I conjecture the strength to be the same, C_{i} system permits additional terms, including apparently all terms with C(Ω*i+a,b) valid for the Degrees of Reflection system, such as C_{0}(C_{1}(C_{2}(0,0),C_{2}(0,0)),0). It is not clear whether all valid main system terms that do not use ordinals ≥Ω_{2}^{2} become valid C_{i} terms.

**Syntax:** Constant 0 (the least ordinal), and function C with 3 arguments.

**Standard form:**

C_{i}(a,b) is standard iff

- a and b are standard

- b is 0 or b is C_{j}(c,d) with (i,a)≤(j,c) (lexicographically). (This is needed for uniqueness of representations, but not needed for comparison.)

- a is built from below from <C_{i}(a,b) with passthrough for (C_{j}:j<i), that is *a* does not use ordinals above *a* except

-- as a subterm of an ordinal <C_{i}(a,b) (using standard comparison to check) or

-- as a subterm of C_{j}(e,f) where j<i that is not in the scope of a subterm of C_{j}(e,f) that is ≤f. In other words, C_{j}(e,f) is treated as representing the ordinal C_{j}(e,f) in terms of ordinals ≤f, and which intermediate ordinals >f are used is irrelevant.

**Comparison:** Standard where (i,a) is treated as an ordinal ((i,a)<(j,b) ⇔ i<j ∨ i=j∧a<b). That is (assuming standard form)

C_{i}(a,b) ≤ d ⇒ C_{i}(a,b) < C_{j}(c,d)

b ≥ C_{i}(c,d) ⇒ C_{i}(a,b) > C_{j}(c,d)

otherwise, C_{i}(a,b) < C_{j}(c,d) iff (i,a) < (j,c).

**Example:** Let M=C_{2}(0,0), and for readability allow ordinal addition.

C_{1}(M+C_{1}(M*2,0),0) is invalid because M+C_{1}(M*2,0) uses a higher ordinal (M*2).

C_{1}(C_{0}(C_{3}(0,0),M),0) is valid because of the passthrough for C_{0}. As far as C_{1} is concerned, we are not using C_{3}(0,0) as an ordinal but merely as a notational shorthand to define C_{0}(C_{3}(0,0),M) in terms of M.

On the other hand, in the first example, M+C_{1}(M*2,0) = C_{0}(C_{1}(M*2,0),M) and C_{1} "knows" what is C_{0}(C_{1}(M*2,0),M) in terms of C_{1}(M*2,0) and M but cannot handle C_{1}(M*2,0) because M*2 is larger than M+C_{1}(M*2,0).

**Proposition:** In the definition of C_{i}(a,b), it is sufficient to allow ordinals ≤b as constants.

**Proof:** Assume contrary, and let b'>b be minimal such that *a* is built from below (with the passthrough) from ≤b' (because b' is a subterm of *a*, minimality does not require proving well-foundness). b' is C_{j}(a',b'') with j<i or j=i ∧ a'<a, and in both cases *a* is built from below (with the passthrough) from <b', contradicting minimality.

**Building the system above an ordinal:** The system can also be built above any given ordinal α. One version is to add ordinals <α as constants and to have C_{i}(a,b)≥α. Another version with the same strength is to add ordinals ≤α and (for standard forms) only use C_{i}(a,b) for b≥α; its benefit is that C_{i} need not depend on α.

**Conjectured Strength:** A natural conjecture is that the C_{n} system (n>0, terms only use C_{i} for i≤n) corresponds to Π^{1}_{n}-TR_{0}. For the conjectured natural assignment of gaps, C_{1+i} returns ordinals κ such that L_{κ}≺_{Σi}ω_{1}^{L} for i>0, allowing transfinite i, and C_{1} returns admissible ordinals and their limits, and with ordinals below C_{1}(0,0) recursive. The proof theoretical ordinal of second order arithmetic is then C_{0}(C_{ω}(0,0),0). C_{2} system likely corresponds to Π^{1}_{2}-TR_{0}, and given the clarity it gives to the structure of canonical ordinals for Π^{1}_{2}-TR_{0}, is highly unlikely to be weaker. (TR stands for transfinite recursion and 0 indicates limited induction.) The full system may then correspond to (canonical countable ordinals in) rudimentary set theory plus for every countable α, L_{ω1+α} exists. This has the same strength (and the same canonical countable ordinals) as second order arithmetic with comprehension for infinitary formulas, axiomatized using the truth predicate or satisfaction relation for such formulas.

**Examples (conjectured canonical assignment):**

Let M=C_{2}(0,0), and let N = M^{+}=C_{1}(0,M).

Using one variable C (see One Variable C above but essentially using C_{1}(ω^{an}+...+ω^{a1}) in place of C_{1}(a_{1},...,C_{1}(a_{n},0)..)), C_{1}(a) for a<M enumerates admissible ordinals <M and their limits, C_{1}(M+a) enumerates fix-points of the above enumeration, C_{1}(M*a+b) corresponds to 2-variable enumeration of the fixpoints, and so on for ordinals recursive in M (that is for ordinals <M^{+}). C_{1}(N+a) (a<N=M^{+}) enumerates recursively inaccessible ordinals <M and their limits, and so on with N being similar to Ω in "Degrees of Reflection" section. For example, C_{1}(N^{NNN}*17+N^{NN2+N}*16+N^{NN}*15+N^{N}*N*14+N^{N}*13+N^{2}*12+N*11+10) should be the 10th admissible above the 11th recursively inaccessible above the 12th recursively hyperinacessible above the 13th recursively Mahlo above the 14th admissible limit of recursively Mahlo ordinals above the 15th Π_{3} reflecting ordinal above the 16th ordinal Π_{3} reflecting onto Π_{4}-reflecting ordinals above the 17th ordinal that is stable up to an admissible above it. Going further, for appropriate f, C_{1}(f(M)) is approximately the least ordinal c that is f(c) stable; for example C_{1}(M^{++}) is the least ordinal c that is c^{++} stable. Higher up, C_{1} converts large ordinal notions into (roughly) ordinals corresponding to transitive models of these notions.

We first present a proof in ZFC of well-foundness of C_{0},C_{1},C_{2} system, and then (using a different approach) a proof of well-foundness of the full C_{i} system using a measurable cardinal. In the next section, we will build on the proof to prove well-foundness of an extension.

**Theorem:** C_{0},C_{1},C_{2} system is well-founded, even if built above an arbitrary ordinal.

**Proof:**

Work in the constructible universe L.

Set C_{2}(a,b)=ω_{b'+ωa} where b' is the maximal ordinal such that ω_{b'}≤b (and b'=0 if b<ω_{1}).

(Note: Instead of C_{2}, we could have used a function f to enumerate uncountable cardinals (in L). For the notation system, if 'a' is standard, then so is 'f(a)'; f(a)<f(b)⇔a<b, f(a)<C_{0}(c,d)⇔f(a)≤d, f(a)<C_{1}(c,d)⇔f(a)≤d.)

Let C_{1}(a,b) be the least possible c>b that is not Σ_{1}(Card) definable in L_{κ+a}, allowing ordinals <c as constants, where κ is the least uncountable cardinal >b and Card is the predicate for cardinals (in L).

C_{0}(a,b), when defined, is the least ordinal c such that a'<a ∧ b'<c ∧ (C_{0}(a',b') is defined) ⇒ C_{0}(a',b')<c.

C_{0}(a,b) is defined iff *a* can be represented using C_{0}, C_{1}, C_{2} and ordinals <C_{0}(a,b) as constants such that

- all intermediate ordinals are below a.

- each use of C_{0} and C_{1} is standard in the following sense:

-- if C_{0}(c,d) is used as a subterm, then c does not use ordinals ≥c except in the scope of an ordinal <C_{0}(c,d)

-- if C_{1}(c,d) is used as a subterm, then c does not use ordinals ≥c except in the scope of an ordinal <C_{1}(c,d), or as a subterm of C_{0}(e,f) that is not in the scope of a subterm g≤f of C_{0}(e,f).

*Proposition:* If *a* is below the least fix-point of x→ω^{x}, then C_{0}(a,b)=b+ω^{a}.

*Proof:* Simple, by recursion on a.

*Proposition:* For every a, there is b' such that C_{0}(a,b) is defined iff b≥b'.

*Proof:* Choose the least b' such that *a* is representable (in the required sense) using ordinals <C_{0}(a,b').

*Proposition:* C_{0}(a,b) is monotonic in b, and for the class of *a* such that C_{0}(a,b) is defined, strictly monotonic and continuous in a. When defined, C_{0}(a,b) is the least point in the range of x→C_{0}(a,x) above b.

*Proof:* By construction of C_{0}.

*Proposition:* Standard comparison for C_{0}: C_{0}(a,b) < C_{0}(c,d) iff C_{0}(a,b) ≤ d or (b < C_{0}(c,d) and a<c) (assuming both are defined).

*Proof:* Follows from the above properties.

*Proposition:* In the definition of C_{0}, one could replace <C_{0}(a,b) with ≤b.

*Proof:* By recursion on a. An ordinal c with b<c<C_{0}(a,b) equals C_{0}(a_{1},C_{0}(a_{2},...C_{0}(a_{n},b)...)) with each a_{i}<a.

*Proposition:* C_{1}(a,b) is monotonic in *a* and b, and continuous in *a*.

*Proof:* By construction of C_{1}; monotonicity is the reason we used Σ_{1} definability. Continuity holds because for each *a* the class of ordinals that are not sufficiently definable is closed except at cardinals.

*Definition:* *a* is maximal in C_{1}(a,b) iff C_{1}(a+1,b)>C_{1}(a,b).

*Proposition:* *a* is maximal in C_{1}(a,b) iff *a* is Σ_{1} definable in L_{κ+a+1}, allowing ordinals <C(a,b) and cardinals as constants.

*Proof:* Given a Σ_{1}-definition of *a*, the definition of C_{1}(a,b) becomes Σ_{1} in L_{κ+a+1}, hence *a* is maximal. Conversely, if *a* is maximal, then C_{1}(a,b) is by definition Σ_{1} definable in L_{κ+a+1}, and this definition can be converted into a Σ_{1}-definition of a.

These properties lead to the standard comparison for the notation system provided that we can show two things:

* C_{1}(0,b)>C_{0}(a,b)

* *a* is maximal in C_{1}(a,b) when C_{1}(a,b) is standard.

Suppose that we can show that C_{0}(c,d) is recursive (or just Σ_{1}) in field(c:d) where field(c:d) consists of d and ordinals ≤d obtained by parsing term c into ordinals ≤d. Then the above conditions are met since C_{1}(a,b) is above all recursive-in-b ordinals, and *a* has a Σ_{1} definition obtained by parsing its notation and using the values of C_{0}(c,d).

*Proposition:* Standard comparison works in the system.

*Proof:* Suppose that standard comparison works below a, that is for every base ordinal b<a, when all subterms are <a, the comparison works. Allow terms using a. C_{0}(c,d) equals d plus the order type of the system between d and C_{0}(c,d). The built-from-below condition ensures that all ordinals <C_{0}(c,d) are representable in terms of ordinals ≤ d while using only ordinals <a, thus the comparison is standard and hence the system is recursive in field(c:d) as required.

**End of Proof**

**Theorem:** Assuming an inner model with a measurable cardinal, the C_{i} ordinal notation system is well-founded, even if built above an arbitrary ordinal.

**Proof:**

Let K be the core model below a measurable cardinal, and let I_{α} be the predicate for ω(α+1)-reflective cardinals for K. See (Taranovsky 2012) (including section Iterations of Reflectiveness) for background, but the properties we will use are the following:

* Elements (and finite increasing n-tuples of elements) of I_{α} are good indiscernibles in (K, ∈, α, (I_{β})_{β<α}): φ(x)⇔φ(y) provided that x and y are finite subsets of I_{α} of the same cardinality, where φ is expressible in the model, and allowing sets in V_{min(x∪y)}^{K} as parameters. Access to the restricted I is allowed as a two variable function (so one can quantify over β in I_{β}).

* α<β⇒I_{β}⊂I_{α}

* K satisfies separation and replacement for predicates that use I.

Let F_{α} consist of functions that are definable in (K, ∈, (I_{β})_{β<α}) (allowing ordinals ≤α as parameters, I is treated as a two variable function), with each element of F_{α} taking a tuple of ordinals as input and returning an ordinal at least as large as the supremum of tuple.

When defined, C_{i}(a,b) is the least ordinal c in I_{i} such that C_{i}(a',b')<c if a'<a and b'<c and C_{i}(a',b') is defined, and

C_{i}(a,b) is defined iff *a* is built from below from <C_{i}(a,b) in the ith extension of the notation system. That is *a* must be representable as a term in that system such that all subterms are ≤a but allowing ordinals <C_{i}(a,b) as constants. In representing *a*, the ith extension uses functions in F_{i} and C with j≥i in C_{j}(b,c) where b does not use ordinals >b except in a term inside C_{l}(g,h) (l<j) that is not in a subterm of C_{l}(g,h) that is ≤h, where a subterm includes its position in the term.

(By recursion on a, this definition is noncontradictory and complete, except that we have not proved that ith extension is a really an extension.)

*Proposition:*

1. C_{i}(a,b) is the least ordinal in the range of x→C_{i}(a,x) above b.

2. C_{i}(a,b) is strictly monotonic in *a* (when it is defined).

3. For every i and a, there is minimum b' such that C_{i}(a,b) is defined iff b≥b'

4. If i<j and b < C_{j}(c,d), then C_{i}(a,b) < C_{j}(c,d)

5. C_{i}(a,b) < C_{j}(c,d) iff C_{i}(a,b) ≤ d ∨ b≤C_{j}(c,d) ∧ (i,a)<(j,c)

*Proof:* 1-3 standard. For 4, the condition C_{i}(a',b')<c corresponds to a closed unbounded set of possible c, and elements of I_{i} are stationary below every element of I_{j}. Statement 5 follows from the above properties and the definition.

Thus, the C_{i} ordinal notation system is well-founded provided that we can show that standard terms are valid in the constructed system. The only problem is that C_{i}(a,b) may use C_{j}(c,d)<a where j<i and c uses ordinals >a in a restricted way. The solution is to compute C_{j}(c,d) without computing term c as an ordinal.

Let d'' be the maximal subterm of C_{j}(c,d) that is <C_{j}(c,d); d'' is expressible using ordinals ≤d and C_{j'} for j'≤j. Replace each C_{k}(e,f)>d'' with C_{k}(e,d'') where f<d'', and represent C(c,d) in terms of subterms ≤d'', so the representation will be a code in the standard form for the notation above d'', plus a list of ordinals ≤d''. We want to show that for some function in F_{i}, its application to the code and the list ordinals equals C_{j}(c,d) (which will complete the proof).

To test e = C_{j}(c,d), after ruling out lower values for C_{j}(c,d), for every c'<c and d≤d'<e, compare C_{j}(c',d') with e where c' uses jth extension of the system.

By recursion, this solves the problem provided that we can test whether c'<c and C_{j}(c',d') is valid, and we can be overstrict with validity provided that at least one representation passes the test.

Overstrict validity test of C_{j}(c',d') (ordinals ≤d' are constants):
For every subterm C_{k}(e,f):

- f≥d'

- if f<C_{j}(c',d'), f=d'

- e≤c'

- e does not use ordinals above e except in a term inside C_{l}(g,h) (l<k) that is not in a subterm of C_{l}(g,h) that is ≤h, where a subterm includes its position in the term.

Comparison when doing the validity test:

- two C terms - standard

- C term and an ordinal (ordinals ≤d' and their values after functions in F_{j}) -- C term is greater

- otherwise, represent both terms in terms of C terms (do not parse the C terms yet) and ordinals. Pairwise compare all the C-terms. Assign the C-terms to arbitrary ordinals in I_{j} >d' consistent with the comparison. Compute both ordinals and compare. This is the point where we use the indiscernability of I_{j}.

To compare c' with c (assuming C_{j}(c',d') and C_{j}(c,d) were tested valid and d≤d'<C(c,d)):

- Use the comparison above. Even though d' need not equal d, the comparison of C terms with ordinals works since c does not have C-terms >d that are ≤d'.

The procedure could fail in three ways:

- We got comparison of ordinals wrong -- not possible given the analysis above.

- We failed to include a valid ordinal -- not possible since (apart from a strictness in representations), we fully covered the definition of C_{j}.

- We included an invalid ordinal.

Suppose that the computation fails (is wrong) for C_{i}. Then there is invalid C_{i}(a,b) in the ith extension which we treated as valid. Let C_{j}(c,d) be an invalid subterm of C_{i}(a,b) with j,c,d valid. Then j>i, and c has a subterm C_{k}(e,f) (i≤k<j) for which our computation fails. This means that there is invalid C_{k}(e',f') that we treated as valid with e'≤e<a (and f'≥f). Iterating, we get an infinite descending sequence of ordinals (since e and, for each iteration, its analogue are valid), which completes the proof.

*Note:* If we can rule out overflows (where C_{i}(a,b)≥C_{i+1}(0,b)), the measurability assumption can be weakened to "starting at zero, the sharp operation can be iterated any ordinal number of times".

**Reducing the assumption:** Σ_{i} elementary substructures of L_{ω1L} lack indiscernability but it may be possible to restrict F_{i} to a class of functions that guarantee the invariance of comparison. To check validity and compare C_{i}(a,b) with C_{i}(a',b) (a and a' are given as codes, with each C_{j(c,d)} having d≥b and with ordinals ≤b used as constants), it is sufficient to know the codes and the relative ordering of the ordinals ≤b that we used, and it may be possible to restrict F_{i} to an analogous class of functions (though perhaps with special conditions on b or other ordinals). One would also need sufficient definability of C_{i} to prove C_{i}(a,b)<C_{i+1}(0,b). Intuitively, validity of C_{i}(a,b) implies that *a* has a canonical definition of a certain type, which we can then 'drop' in an order preserving way to get a similar structure at a lower level.

The system can be extended by adding more variables. One extension (not the one below) which might be too restrictive is as follows. With C_{a,b}(c,d), c may use passthrough for C_{a',b'} where (a',b')<(a,b) (lexicographically) and b may use passthrough for C_{a',b'} where a'<a. To go further, combine a, b, and c into an ordinal using a large ordinal Ω and naturally (using CNF base Ω) extend the combination up to ε_{Ω+1}. The result will be the "Iteration of n-built from below" notation system with "n-built from below" replaced with "built from below". However, perhaps the above is too restrictive, and in C_{a,b}(c,d) we should allow passthrough for b where (a',b')<(a,b). A natural extension up to ε_{Ω+1} (or another ordinal) is the following.

**Degrees of Reflection with Passthrough:**

*Syntax:* 0 (the least ordinal), C (partial binary function), Ω (a large ordinal), **O** (ordinal notation system for ordinals above Ω in terms of ordinals <Ω).

*Choice of O:* CNF base Ω; another choice is C; any system that is well-founded above a generic ordinal should work.

*Description:* C is standard with C(a,b)<Ω when b<Ω. In C(a,b), each d in the representation of *a* in terms of ordinals <Ω is built from below from <C(a,b) allowing passthrough for C(a',b') where a'<a. Passthrough means that C(a',b') is treated as representing C(a',b') in terms of ordinals ≤b', and the intermediate ordinals used are not checked for being <d.

**Notes:**

* The passthrough is the only difference from Degrees of Reflection system.

* Like in the C_{i}(a,b) system, in built-from-below from <C(a,b), we can replace "<C(a,b)" with "≤b".

* If the system is well-founded (which is not yet clear), a natural conjecture is that it is similar to and has the same strength as the main system for n=2. See Strength of the Main System (above) for analysis.

We only have a proof of well-foundness of (a variation on) a small fragment of the system.

**Theorem:** Assume that there is an inner model 1+α measurable cardinals, where α is an ordinal. The C_{i}(a,b) system is well-founded even if augmented with α constants with (1) there is no constant c (c>0) with b<c≤C_{i}(a,b) and (2) in C_{i}(a,b), i is built from below from <C_{i}(a,b) with passthrough for lower values of i.

**Corollary:** Suppose that for every κ<min(δ: L_{δ}≺_{Σ1}L) there is a transitive model of "ZFC + κ measurable cardinals". Then for every α, the C_{i}(a,b) system with α constants is well-founded.

**Proof of the Corollary:** This follows from Σ^{1}_{2} correctness of L_{δ}.

**Notes:**

* Under conjectured canonical assignment, each constant corresponds to an uncountable cardinal in L.

* Unlike in the countable case, the least ordinal c such that L_{c} and L_{ω2L} satisfy the same Σ_{1}(Card) statements is below the least Σ_{1}(Card) elementary substructure of L_{ω2L}, and we have not determined the exact canonical assignment.

* The theorem and the proof suggest that in the table of cardinals and their recursive analogous, regular uncountable cardinals in L are recursive analogs of measurable cardinals.

* By iterating the construction (α → order type of the system) ω times (starting at 0), the ordinal we get is probably the proof theoretical ordinal for rudimentary set theory plus ∀α<ω_{1}^{CK} ∃s=ω_{α}^{L}. This is stronger than Zermelo set theory but weaker than Borel determinacy. Iterating it another time (for a total of ω+1 times) is equivalent to using a function to enumerate all C_{1}(0,0) constants and should give us all canonical ordinals in the theory.

**Proof of the Theorem:**

The proof is analogous to the proof of well-foundness of ordinary C_{i}(a,b), but there are key differences which we will now cover in detail. Work in M, where M is the minimal inner model with 1+α measurable cardinals. The constants will be measurable cardinals and their limits, excluding the supremum of the measurable cardinals. Let κ_{m} be the second cardinal above the supremum of measurable cardinals. The exact fine structure is unimportant, but we can for example set M_{a} to L_{a}[U] where U codes the sequence of ultrafilters.

*Definition:* I_{i} (below the supremum of measurable cardinals) is defined as follows: λ∈I_{i} iff λ and κ satisfy the same Σ_{1}({j(M_{κm})}) predicates in j(M_{κm+i+1}) with parameters in M_{λ}, where κ is the least measurable cardinal (in M) above λ and j is the corresponding embedding.

We will use only the following properties of I_{i}.

*Definition:* getmin(i) is the least ordinal such that i is Σ_{1}({M_{κm}},getmin(i)) definable in M_{κm+i+1}.

*Proposition:*

* For all measurable κ, I_{i} has measure 1 below κ.

* I_{i} is uniformly-in-i Σ_{1}({M_{κm}},i) definable in M_{κm+i+2}.

* i<j ⇒ I_{j}\(getmin(i)+1) ⊂ I_{i}

* For all finite subsets s and t of I_{i} with ∀(measurable κ) |s∩κ|=|t∩κ| and Σ_{1}({M_{κm}}) φ with two free variables, ∀x∈M_{min(s∪t)} M_{κm+i+1} ⊨ (φ(x,s)⇔φ(x,t)).

*Proof:*

The indiscernity holds because for every λ∈I_{i} below measurable κ (κ is the least measurable above λ) for every finite increasing iterate M' of M with the first embedding using κ, (κ,s) agrees with (λ,s) for the relevant class of formulas where s is the set of critical points >κ used in the embeddings. Here, increasing means that the critical points are increasing. The agreement holds because the embeddings are sufficiently definable in M_{κm+i+1}.

*Notes:*

* Elements of I_{i} are effectively indiscernibles except as to the number of measurable cardinals below the element.

* Our setup ensures that above getmin(i) elements of I_{j} are indiscernibles even for predicates that use I_{i} for i<j.

The ith extension is defined analogously to the proof of the previous theorem. Both i and *a* need to be built from below from <C_{i}(a,b). Instead of j,a,b→C_{j}(a,b) for j<i, we will allow x→y=F(n,x) when:

x is a tuple of ordinals.

y is Σ_{1}({M_{κm}},x) definable in M_{κm+i+1}; n is a code for the definition.

y is an ordinal >max(x).

there is no measurable κ with max(x)<κ≤y.

An equivalent condition on i is that getmin(i)<C_{i}(a,b). This is easily seen equivalent to i being built from from below from <C_{i}(a,b), allowing F as above.

As before, to show that standard terms are valid in the system we constructed, we propose computation of C_{i}(a,b) where *a* is given as a term (in the ith extension) rather than ordinal. The comparison of terms is essentially as before. Since getmin(i)<C_{i}(a,b), comparison with i works. The comparison between a C or F term and one of the measurable constants is trivial. When assigning C-terms to indiscernibles, each indiscernible must have the right number of measurable cardinals below it.

Suppose that the computation fails (is wrong) for C_{i}. Then there is invalid C_{i}(a,b) in the ith extension which (in our computation) we treated as valid. Let C_{j}(c,d) be an invalid subterm of C_{i}(a,b) with j,c,d valid. Then, j or c has a subterm C_{k}(e,f) (i≤k<j) for which our computation fails. (Otherwise, C_{k}(e,f) would be sufficiently definable. Also, if k≥j, the use of C_{k}(e,f) would not prevent C_{j}(c,d) from being valid even if our computation of C_{k}(e,f) fails.) This means that there is invalid C_{k}(e',f') that we treated as valid with e'≤e<a (and f'≥f). Iterating, we get an infinite descending sequence of ordinals (since e and, for each iteration, its analogue are valid), which completes the proof.

REFERENCES

Rathjen, Michael (1994), "Proof theory of reflection". Annals of Pure and Applied Logic 68, pp. 181–224.

Rathjen, Michael (2006), "The art of ordinal analysis", International Congress of Mathematicians, II, Zürich, Eur. Math. Soc., pp. 45–69.

Taranovsky, Dmytro (2012), "Reflective Cardinals", available on arXiv.