Dmytro Taranovsky
Updated: October 5, 2022

Ordinal Notation

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 systems with conjectured strength beyond second order arithmetic (and plausibly beyond ZFC), and prove well-foundedness for some versions.

Contents:
1 Introduction
     1.1 Introduction
     1.2 Prior Work
     1.3 Goals of Ordinal Analysis
2 A Framework for Ordinal Notations — defines the general structure for the notations.
     2.1 Definition of the General Notation
     2.2 Basic Properties of C
     2.3 Bachmann-Howard Ordinal
     2.4 One Variable C
     2.5 Reflection Configurations
3 Degrees of Recursive Inaccessibility — presents a notation system for ATR₀ plus "for every ordinal a, there is recursively a-inaccessible ordinal".
     3.1 Definition of the Notation
     3.2 Comparison Relation
     3.3 Examples
4 Degrees of Reflection — presents a notation system at the level of Σ¹₁ reflecting ordinals, with the canonical assignment for nonrecursive ordinals.
     4.1 Definition of Degrees of Reflection
     4.2 Examples and Additional Properties
     4.3 Assignment of Degrees
     4.4 A Step towards Second Order Arithmetic
     4.5 Reflection Configuration Version
5 Main Ordinal Notation System — presents the main notation system, which plausibly reaches second order arithmetic (Z₂) or perhaps much higher.
     5.1 Definition and Basic Properties
     5.2 Strength of the Main System
     5.3 Old Analysis and Examples
6 Beyond Second Order Arithmetic — gives insights for going beyond second order arithmetic and ZFC.
     6.1 Old Analysis
     6.2 New Analysis
7 Iteration of n-built from below — proposes a strengthening of the main system.
8 Built-from-below with Passthrough — presents notation systems with some expected to be beyond Z₂ (and plausibly beyond ZFC), and proves well-foundedness of some versions.
     8.1 Definition and Properties
     8.2 Degrees of Reflection with Passthrough
     8.3 Proofs of Well-foundedness
     8.4 Using Canonical Definitions
     8.5 Well-foundedness with Reflection Configurations — proves well-foundedness of a system conjectured to correspond to Π¹₂-CA₀, and discusses related ordinal assignments.

Notes:
• Claims not marked as theorems or propositions should be treated as conjectures (see Introduction).
• OrdinalArithmetic.py (absolute link) is a python module/program that implements comparison and ordinal arithmetic for the main ordinal notation system. See 2.4 One Variable C subsection of the paper for a notational difference with the module. The reader is encouraged to try out the module.

1    Introduction

1.1    Introduction

What this Paper Accomplishes: We define and analyze several very strong ordinal notation systems presented as recursive relations between terms. The canonical assignment of ordinals to terms (see 1.3 Goals of Ordinal Analysis below for what that means) is fully given for some weaker systems, and many examples of conjectured canonical assignment are given beyond that. Well-foundedness is proved for some of the systems. Strength lower bounds are not proved.
    Formally, unless stated (or the reader is satisfied) otherwise, claims in this paper about the notation systems should be treated as conjectures. While some conjectures are speculative (with significant doubts always noted), in many cases our understanding is so detailed, coherent, and precise as to be very confident in its accuracy. This is not a substitute for proof, but is the best we have before the required bounds are proved.

1.2    Prior Work

Prior to the Degrees of Reflection system in this paper, the strongest reasonably simple ordinal notation system was the one for KP + Π₃ reflection (Rathjen 1994). (That system is referenced in the next paragraph, which the reader without requisite background is free to skip.) 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 Ψ^ξ_π(α) (for KP + Π₃ reflection) looks like C(a,b,c) (or C(ξ,α,π)) in "Degrees of Recursive Inaccessibility". In addition, Rathjen uses CNF (Cantor normal form), a constant K (corresponding to the least Π₃ reflecting cardinal), and Ξ(α) for the least α-recursively Mahlo ordinal below K, defined using diagonalization for α≥K. 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, Ψ⁰_π(α) 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 Ψ¹_Ξ(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). Ψ⁰_π(α) ranges over non-admissible limits of recursively hyper-hyper-Mahlo ordinals above Ξ(5), Ψ¹_π(α) ranges over admissible limits of such ordinals, and Ψ²_π(α) ranges over recursively Mahlo limits of such ordinals.

The downside of Rathjen's approach is the lack of the simple monotonicity that C has, as well as additional complexity when trying to extend it (especially beyond Π₃-reflection) where simple built-from-below does not suffice. Even more recent systems along these lines are fairly complex. For examples, see (Duchhardt 2008) for Π₄ reflection, (Arai 2015) for Π_n reflection, and (Stegert 2010) for stability.

For proving ordinal notation strength lower bounds, derivations in the target theory can be transformed into uniform (in an appropriate sense) infinitary cut-free derivations using terms in the notation system (with comprehension rules corresponding to operations on terms). An alternative possible proof mechanism is to construct a nonstandard model with all ordinals in the model being (possibly nonstandard) terms in the notation system.

History of this paper: 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 (January 24, 2006 revision), 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). In March 16, 2012 revision, I added the main ordinal notation system, intended for second order arithmetic. Afterwards, in 2014 (January 9, 2014 revision), I discovered new structure in the main system and wrote an initial version of a series of updates. In 2015 (April 20, 2015 revision), I proposed a strengthening of the main system (iterations of n-built from below). August 24, 2016 revision added "Built-from-below with Passthrough", including proof of well-foundedness, and around that time, I made many improvements to the paper. October 9, 2016 revision extended the well-foundedness proof for the passthrough system to a stronger system. August 2017 revision added "Using Canonical Definitions" and updated other parts of the paper. November 2018 revision (1) added the correct canonical assignment for Degrees of Reflection (including a correction at the level of Π_n reflection), (2) added reflection configurations, and (3) made expository, organizational and other changes. March 2020 revision added (presumably) optimal well-foundedness proof of the reflection configuration passthrough system conjectured to correspond to Π¹₂-CA₀.

1.3    Goals of Ordinal Analysis

We also want the system to be extensible, both generally, and also as a parameterized system of extensions achieving a form of completeness (see "Completeness and extensibility" above and also 4.3 Assignment of Degrees) or at least (to a certain extent) capturing the framework that T intuitively provides for its extensions.

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.

2    A Framework for Ordinal Notations

2.1    Definition of the General Notation

2.2    Basic Properties of C

2.3    Bachmann-Howard Ordinal

2.4    One Variable C

2.5    Reflection Configurations

While the use of degrees allows a simple formalization, it obscures a fundamental symmetry in our notation systems. Namely, every pair (b,a) of representable ordinals defines a special function r(a,b) (with r(a,b)(b) = a) describing how big is a relative to b, which can then be applied to other appropriate ordinals.

Definition: The reflection configuration of a term a above b is obtained by
- taking the standard representation of a in terms of ordinals/terms ≤b (so subterms ≤b are not parsed for subterms C(c,d)>b)
- in every subterm C(c,d)>b with d<b, replacing d with b
- replacing b with x, and adding λx to the front of the configuration. The variable name x is immaterial as long as x is not used otherwise.
The constants used are the outermost subterms <b in the configuration (i.e. a constant (<b) is not parsed for further constants).
The upper bound will typically be Ω or infinity, but formally the lesser of the least constant term >b used in the notation system and the term (if any) above all ordinary C-terms.
Note: a and b can be ordinals or terms in the notation system used. We are not restricting a and b provided that a has a standard representation in terms of ordinals ≤b.

The notation systems we will define will have the property that if A is a reflection configuration (of a above b), and d is an ordinal above the constants used and below the upper bound, then there is unique c such that A is the reflection configuration of c above d. In other words, given a and b and d, c is to d what a is to b. Furthermore, c is strictly monotonic in a and monotonic in d. In general, c will depend on the notation system used. However, if b and d have sufficiently strong reflection properties relative to the notation systems, c will be independent of the notation system, so the differences in notation systems are in how to handle reflection configurations above ordinals without sufficient reflection properties.

A single a has a finite set of reflection configurations, with configuration transitions (of the configuration of a above b) happening at subterms of a. The final reflection configuration of a will just use a as a constant (i.e. λx.a). In terms of the structure of the systems, reflection configurations can be said to be more important than degrees.

The comparison of configurations is simply the standard comparison with x treated as an ordinal above the constants but below the upper bound. In our systems using C,0,Ω, the lexicographical comparison (of postfix forms) works provided that we are given whether x<Ω (and similarly with other special constants for systems that use them). We will typically only care about configurations for x<Ω, but one can specify it explicitly using λx<Ω. Note that λx.x is the least nonconstant configuration.

Example: For the system for the Bachmann-Howard ordinal, the configuration for ε₀ above any lower ordinal is λx.C(Ω,x), and in line with this value, the least point in the range of ε above b<Ω equals λx.C(Ω,x)(b) = C(Ω,b).

The reflection configuration of a above <b is the reflection configuration of a above a sufficiently large term <b, except that for nonlimit b, we treat it as the configuration above an imaginary ordinal above all of b's predecessors. Thus, the only difference with using '<' is when b is a subterm of a.

Of particular importance is the reflection configuration of a above C(a,b) (standard term). If the configuration is λx.A(x), the configuration of C(a,b) above <C(a,b) is λx.C(A(x),x), which characterizes how big/reflective C(a,b) is relative to lower ordinals. Note that both configurations are also valid above every x<C(a,b) that is above all outermost subterms of C(a,b) that are <C(a,b).

Effect of reflection configurations on ordinal notation systems:
* Reflection configurations can be used to change certain notation systems by essentially requiring built-from-below reflection configurations rather than built-from-below ordinals. The impact is as follows.
* Reflection configurations add complexity to the systems. They also lead to an unconventional structure, for example turning what looks like ω admissibles into the strength of ω^ω admissibles. They also depend on symmetry.
* However, they pay it back by giving built-from-below a perfect form, especially for 'passthrough' systems. If we want to collapse a to get c, and a has a subterm d with c<d<a, then what a is to d might be smaller than what a is to c, which (in ordinary systems) cuts off the permitted degree of diagonalization a above d (unless each instance of d is inside an ordinal <c). Such cutoff might make the system much weaker, and also much less symmetric, as the relationship among ordinals a,c,d is somewhat arbitrary (and depends on the notation system). With reflection configurations, however, we can address this by translating a from c to d (for the appropriate d).

Elementary embeddings are central to large cardinal axioms and fine-structural models. Reflection configurations make embeddings appear everywhere, which aligns with translating large cardinal axioms into ordinal notation systems.

For creating subsystems of ordinal notation systems that use reflection configurations, one limits the strict supremum of the configurations used rather than just the largest ordinal used. If we have ordinals c₀, c₁, ... with c_i+1 above c_i being the analog of c₁ above c₀, a system cut off below say c₁₀₀ might be much weaker than the one below sup(c_i) because we might not have the syntactic space to move a configuration (using c_i above the ordinal) to a higher ordinal.

Handling of other notation systems:
* A large constant c can be handled by restricting the domain below c, or by turning c into a function with c(x) being the least c-like ordinal above x (with .. in c(..) handled like the second argument of C in constructing reflection configurations).
* Multivariable C(..,...,b) is treated as C((..,...),b).
* If for ordinals ≥Ω, we use a notation system O above a generic ordinal (as defined above), no special handling of O is necessary (for configurations above ordinals <Ω, except possibly for the configuration above 0). C(O(...),b) is essentially a generalization of multivariable C. If O uses ordinals <α as constants, we can still define configurations above ordinals ≥α (including above <α).
* For systems using other functions, there might be special rules for getting reflection configurations.
* In systems where symmetry is broken, but only locally, reflection configurations can be defined above sufficiently closed ordinals: In translating an ordinal a from b to c, both b and c (but not necessarily a) must be sufficiently closed. Thus, with special handling of the successor parts of ordinals below the upper bound for the configuration (including if the above O tests whether b<Ω is a successor rather than operating above a generic ordinal), b and c must be limit; and with special handling of CNF representations, they must be fixed points of ω^x.

Note on testing for standard forms: If a condition for standardness relies on the configuration of a above C(a,b), then in testing it, use standard comparison to determine which terms are <C(a,b). Then apply the condition to check for standardness. For example, C(C(Ω,0),0) is only standard if C(C(Ω,0),0) < C(Ω,0) (i.e. standard comparison gives this), so the configuration to check (for a=C(Ω,0) in the above) is λx.C(Ω,x) rather than λx.C(Ω,0).

Notations related to reflection configurations

To avoid repeating ourselves, here are some notations that make defining particular systems easier. The reader is free to skip this part and come back when encountering a definition that uses reflection configurations.

In testing C(a,b) for standardness with a and b standard and b minimal, the remaining condition is about a.

* T_a is the subterm/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 x is a proper subterm of y. Identical terms at different positions are distinguished (in the quantifiers and in ⊏).
Note: T_a will be useful in stating the conditions in first order logic.
* d=parent(c) means c⊏d ∧ ¬∃e c⊏e⊏d, but as a special case, parent(a) is C(a,b).
* d=parent_<Ω(c) means c⊏d ∧ d<Ω ∧ ∀e (c⊏e⊏d) e≥Ω, or if there is no such d, parent_<Ω(c) is C(a,b). In other words, if ordinals ≥Ω are merely syntactic constructs, d is the real parent of c.
* r(c,d) is the reflection configuration of c above d.
* r(c) is r(c,parent(c)), annotated with the position of c inside T_a; the standard comparison is used for C(a,b) even if it is nonstandard.
* r_<Ω(c) is as above using r(c,parent_<Ω(c)).
Note: r(c) or (as appropriate) r_<Ω(c) are the relevant configurations for extending built-from-below to reflection configurations.
* d∈r(c) iff d⊑c ∧ ∀z (d⊏z⊑c) z≥parent(c) (and similarly with r_<Ω(c) using parent_<Ω; also, the point is that r(c) uses d, possibly as a leaf term)
* r(e)⊆r(c) iff ∀z (z∈r(e)⇒z∈r(c))

For a reflection configuration a, the subterm tree T_a is defined as if it were an ordinal, except that the constants <x are not parsed further. r is defined as above (without fallback to C(a,b)) by replacing x with a fictitious (sufficiently large below the upper bound) ordinal x₀, computing the configuration, and replacing λx with λx λx₀. If a configuration already uses λx₀, then use x₁ (like x₀), and replace λx λx₀ with λx λx₁ λx₀; and so on. The comparison remains standard (lexicographical in postfix form with (if x<Ω) C < 0 < x₀ < x₁ < x₂ < ... < x < Ω). For x<Ω, r_<Ω is defined analogously.

Comparison between configurations for x<Ω and x≥Ω is by default undefined. However, in our systems using C,0,Ω it will be convenient to compare them as follows: For the configuration for x<Ω, replace Ω with Ω' (except in the constants below x) and then use the usual (lexicographical for postfix forms) comparison with C < 0 < Ω < x < Ω' (actually, any use of Ω' will make the configuration greater). For example, λx<Ω.5 = λx≥Ω.5 < λx>Ω2.Ω2 < λx<Ω.x < λx<Ω.Ω. See 4.4 A Step towards Second Order Arithmetic for an extension of this for certain systems.

3    Degrees of Recursive Inaccessibility

3.1    Definition of the Notation

3.2    Comparison Relation

3.3    Examples

4    Degrees of Reflection

4.1    Definition of Degrees of Reflection

Notes:
* For a more explicit phrasing, see Comparison Algorithm below.
* When C is used for O, the system is superficially similar to (but weaker than) the n=2 notation system in 5 Main Ordinal Notation System.
* A natural strengthening is 8.2 Degrees of Reflection with Passthrough.
* Intuitively, for constructing an ordinal α, built-from-below allows indirectly referring to appropriate ordinals <α⁺ (since built-from-below (from <α) ordinals can be collapsed to below α⁺), and O builds on top of that, so we can indirectly refer to appropriate ordinals <α⁺⁺ (but limited to O above α⁺) to describe the diagonalization pattern.
* Compared to using C, using CNF base Ω has the same strength but allows additional terms. For example, if a = Ω+d with d = d₁+...+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. However, if the representation of a using CNF base Ω does not use ordinals >C(a,b) that are not fix-points of x→ω^x, then C(a,b) is the same in both systems (but converting C(a,b) still requires conversion of a and b).
* We can also build the system above a generic ordinal (see above for "generic ordinal").
* An interesting question is whether over RCA₀, Σ¹₁-MI₀ is equivalent to: For every O (encoded by a real number, so not necessarily recursive) well-founded above a generic ordinal, the above system using O is also well-founded (equivalently, well-founded above a generic ordinal as we can code lower ordinals into O).

Comparison Algorithm

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

Syntax: Two constants (0, Ω) 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' < 'Ω': 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. ∀x∈T_a ∀y⊏x (x<y<Ω) ∃z⊒y (z<Ω) (z⊐x ∨ z < C(a, b)).

Here T_a is 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 x is a proper subterm of y; identical terms at different positions are distinguished (in the quantifiers and in ⊏).
Note that ∃z⊒y (z<Ω) z⊐x simply means that x is not in the representation of a in terms of ordinals <Ω (with z⊒y redundant).
Note: The '<' uses the above-described lexicographical order (including for z < C(a, b)).

When using an arbitrary O for ordinals >Ω: Condition (3) applies verbatim. (The term structure above Ω is irrelevant as long as the ordinals used <Ω are unaffected.) The other conditions are standard for C and can be handled accordingly. (In condition (2), exclude b=Ω. Use standard comparison for C. Comparison and standardness of O-terms is per the definition of O.)

Conversion of nonstandard forms: To convert 'C(a, b)' to the standard form (when C is used for O), 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 (condition 3 above). 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.

4.2    Examples and Additional Properties

4.3    Assignment of Degrees

Note the similarity with 2.5 Reflection Configurations since a degree gives a lower bound on the configuration of x above <x (if it exists).

x has degree d iff has x has <x-maximal degree d'≥d. (This holds because d does not use ordinals that are not representable from <x.) From now on, we mostly focus on <x-maximal degrees. In "x has <x-maximal d if ..", we assume that d is <x-maximal.

x has <x-maximal degree d+1 iff x is a limit of ordinals of degree d. This implies that 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 O-cofinality of d is <Ω, then x has degree d iff it has every degree <d.
Notes:
* The cofinality is required to be <Ω because our notation system has gaps.
* Weak theories typically will not prove that degrees <d are well-founded. However, the operative conditions for successor and O-cofinality Ω <x-maximal d' are phrased in terms of lower ordinals, which prevents infinite regress. An equivalent explicit definition for <x-maximal d (not of O-cofinality Ω) is that there are arbitrarily high d'<d such that x is a limit of ordinals of degree d'.

Cofinality Ω (using CNF base Ω)

If d has cofinality Ω in O (using CNF base Ω for O), separate out the rightmost 1 using CNF base Ω of d, and let n be its height (with the base being at height 1). Thus, n=2 for ..+Ω^..+1 (including ..+Ω¹), and n=3 for ..+Ω^..+Ω..+1, and so on.
x has degree d iff it has n-degree d or is a limit of such ordinals. n-degree is based on Π_n reflection (and 1-degree is just degree), with the numbering of degrees chosen to be consistent between different n.
An ordinal x has n-degree e+Ω^Ω^..^Ω (using n-1 Ω; using CNF; <x maximal degree) iff it is a Π_n reflecting limit of ordinals of degree e. (Also, this is a special case of the next sentence since "Π₁-reflecting on" is the same as "limit of", except that only here do we allow e=0.)
More generally, x has n-degree ..(e+Ω^Ω^..^1) (using CNF; <x maximal degree) where the 1 is at height n and the '+' is at height m iff x is Π_n reflecting and is Π_m reflecting onto ..(e).
If f = ..(e) has O-cofinality Ω, Π_m reflecting onto f means x is Π_m reflecting onto ordinals of n'-degree f, where n' is the height of the rightmost 1 in f.
Otherwise, it means there are arbitrarily large <x-maximal g<f with O-cofinality Ω such that x is Π_m reflecting onto g, with n' (the height of the rightmost 1 in g) is ≥m.

Levels of Stability

The above analysis also applies to a-stable x for a<x. We will use Veblen normal form base Ω, for convenience using φ_a(b) for Veblen φ_a(Ω+b) (a<Ω), and φ₀(b) for Ω^b.

The height of the rightmost '1' in d = ..+φ_a1(..+φ_a2(...+φ_an(..+1))..) (with a_i<Ω) is ω^a₁+ω^a₂+...+ω^a_n, but with 1 added if finite, and 1 subtracted (on the right) if the '1' is in a subterm of the form φ_a(Ω¹) or φ_a(..+Ω¹) (a>0 in both forms). (Note that ordinals like ε_Ω+1 do not have cofinality Ω.) The height of the rightmost '+' (above) is determined the same way, but without the subtraction.

Going further, the least κ-stable κ is C(φ_φΩ(1)(1)) (with φ as above). Diagonalization presents additional complications, but up to κ⁺, we can address them as follows. The height (of '1' and '+' above) will still use ω^a₁+ω^a₂+...+ω^a_n (adjusted as above), but a_i might be above x, in which case a_i is converted into the order type of {h<a_i: h is <x-maximal}. (Also, in a weak theory, if this is ill-founded, we give up setting this degree, except through higher degrees.) Further still, Π_Ω reflection corresponds to κ being κ⁺-stable (and to Π¹₁-reflection).

Notes on transfinite reflection levels:
* 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.
* Alternatively, transfinite Π_a reflection (for a<x) can be defined using infinitary formulas (with the set coding the formula in L_x). Note that every Π_a formula for limit a is Π_a' for some a'<a.
* If a is an x-recursive well-ordering (potentially ≥x), Π_a reflection can also be defined using almost self-referential formulas, with ψ(c,x) (c∈a), allowed to use ψ(c',y) with c'<c as a subformula (except that if c+ω>a, we have to count the quantifiers to confirm that the depth is ≤a).

Iterations of Π¹₁-reflection

Starting with Π¹₁-reflection, the picture changes qualitatively because Π¹₁-reflection for κ can be iterated up to (informally) κ⁺⁺ times as opposed to up to κ⁺ times for lower reflection levels, and iterations of the reflection capture the notation system. Essentially, ordinals <κ⁺ can be used freely, because if a and b are two different recursive representations of α above κ (using constants <λ), then above λ<κ, that a and b denote the same ordinal is Π¹₁ and can be added as a reflection condition, so it does not matter whether the reflection is iterated along a or b. Now given an ordinal notation system O above a generic ordinal, interpret O above κ⁺, and given an O-term A>0, Ath iteration of Π¹₁-reflection means being Π¹₁-reflecting onto Bth iteration for every B<A, with the 1st iteration simply means being Π¹₁-reflecting, or (as appropriate) Π¹₁-reflecting onto a given set.

Now, in the notation system (with x being Π¹₁-reflecting), parse the rightmost term of d until reaching either φ_Ω(a) (a>0) or a=φ_Ω(a)>Ω. Collapse the terms (<Ω) in O representation of a into ordinals below x⁺ using a_i → order type of {h<a_i: h is <x-maximal}, and convert a into a' using O above x⁺. Subtract 1 from a' (and store the result as a') if a' was b+n where n is finite and b is limit with O-cofinality <x⁺. Now, having <x-maximal degree d means being a'-Π¹₁-reflecting and also being Π_m reflecting onto ..(e) (or is a limit of such ordinals), where m and ..(e) are as above (see "Cofinality Ω (using CNF base Ω)" and its application to levels of stability; the rightmost '+' considered must be outside of a, so m<Ω).

Note that we do not require O to be well-founded, and d having O cofinality Ω is equivalent to every converging (to d) sequence having ordinals/terms unbounded in Ω. Assuming we have not missed anything, by plugging in appropriate O, we get the complete assignment below the least Σ¹₁-reflecting ordinal even in strong theories. For a sufficiently closed appropriate theory (such as Z₂), O would correspond to its proof-ordinal built above a generic ordinal, which might be available from other systems in the paper. Also, by using order-preserving bijections, the canonical assignment also applies to other appropriate ordinal notation systems.

A simple suboptimal assignment: There is also a relatively simple suboptimal assignment (that might not work in weak base theories) that should have the right limit when using Veblen normal form. As above, let e-Π¹₁ reflecting mean e-fold iteration of being Π¹₁-reflecting. C(0,x) will be the next admissible ordinal above x. x has <x maximal degree f iff x is f'-Π¹₁ reflecting (or even simpler, but with the wrong limit, f'-stable), or is a limit of such ordinals, where f' is roughly analogous to the old version below. Specifically, let f₁ be the order type of {h < f : h is <x maximal }. Let y be the order type of representable ordinals below C(Ω, x) (allowing x and ordinals <x as constants). Express f₁ using O base y and then change to O base x⁺ (the least admissible ordinal above x) to get f'.

Old Version

Notes:
* The text branches from the main text starting with "Cofinality Ω (using CNF base Ω)".
* The assignment below is retained for historical purposes but it misses some canonical ordinals starting with the least Π₃ reflecting ordinal that is Π₂ reflecting onto Π₃ reflecting ordinals, which leads it use higher ordinals (for given terms) than the canonical assignment. The canonical assignment only uses ordinals through Π_n reflection. I would like to thank a reviewer with alias Hyp cos for pointing out the issue (in a related system) and suggesting the right strengths, which was instrumental in getting the new version above.

Otherwise, the fundamental 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 fundamental 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₁ 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₁ = f if f≤x)
- Let y be the order type of representable ordinals below C(Ω, x). Express f₁ using CNF base y and then change CNF to base x⁺ (the least admissible ordinal above x) to get f' (so f' = f₁ if f<Ω).

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

4.4 A Step towards Second Order Arithmetic

Reflection configurations: (See 2.5 Reflection Configurations for definitions.) Let Ω_i(x) denote the least ordinal of correctness i above x. When defining a reflection configuration above b (or above <b), a reasonable notation is to replace Ω_i>b (or Ω_i≥b respectively) with Ω_i(x). This way, all reflection configurations are valid without an upper bound (unless we use a definition that breaks them), and we do not have to specify the domain explicitly. The comparison of configurations is lexicographical (in postfix form) after converting everything to the same Ω_i(0) and Ω_i(x) using Ω_j(x) = C(Ω_j+1(x),x). In this notation, λx.Ω₁(x) > λx.Ω₂(0), and the latter configuration is only valid for x>Ω₂ (and 0 serves to avoid confusion).

A Particular System

Using the above template, let us define a system analogously to Degrees of Reflection, but with an additional built-from-below condition to ensure well-foundedness.

Definition of the system: 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.

This leads to a polynomial time algorithm for checking whether a particular representation is standard, and I expect there is also a polynomial time algorithm for converting arbitrary C-terms to the standard form.

For the conjectured canonical assignment:
Every ordinal has correctness 0.
An ordinal a has correctness 1 if it is admissible >ω (or a limit of such ordinals).
An ordinal a has correctness of n+1 (n>0) if it is a Σ¹₁-reflecting limit of ordinals of correctness n (or a limit of such ordinals).
Note:
A more natural assignment of correctness (corresponding to second order arithmetic) is given in the next section.

The notation system is conjectured to reach 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 Π¹₁-CA₀ + lightface Π¹₂ comprehension. I have not ruled out that due to non-Gandy ordinals, the assignments should be lowered.

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

4.5    Reflection Configuration Version

The reflection configuration version of the Degrees of Reflection system is defined by changing the built-from-below condition to use reflection configurations (2.5 Reflection Configurations) in the standard manner. Formally, the condition using T_a is changed to:
∀x∈T_a ∀y⊏x (r_<Ω(x) < r_<Ω(y) ∧ y<Ω) ∃z⊒y (z<Ω) (z⊐x ∨ z < C(a, b)).

The use of reflection configurations does not give more strength assuming O is closed under ordinal exponentiation. It also loses a certain directness: If α is the least height of a transitive model of T, then in the base version, the proof ordinal of T is often around C(α,0), while with reflection configurations, C(α,0) is often much stronger. Nevertheless, the system is a good illustration of how ordinal notation systems with reflection configurations work.

Reflection configurations address the impact of delayed diagonalization in systems using passthrough (8 Built-from-below with Passthrough), where getting a recursively inaccessible ordinal already requires a Σ₁ correct ordinal. Here, however, their effect is simply to add a certain symmetry, which for proof ordinals corresponds to repeated replication of the structures even though they are not actually replicated at the transitive model level.

The canonical assignment of ordinals follows the same schema as before. Thus, C(Ω,0) is still ω₁^CK, and C(Ω*2,0) is the least recursively inaccessible and so on. However, reflection configurations in effect build structures above all ordinals, which has the effect of adding an extra level of reflection for the proof strength.

Every valid term in the base version is valid in the reflection configuration version.

The first difference from the base version is that the ordinal for KP is now C(εω1CK+1,0). More generally, for a typical theory T below Π11-CA0 that implies existence of ω1CK and without special strength <ω1CK, the proof ordinal is C(a,0) where a is the supremum of T-provable recursive-in-ω1CK ordinals. (Since T is effectively weaker for ordinals above ω1CK than ordinals above ω, this is below the supremum of T-provable recursive ordinals |T| translated (using reflection configurations) to ω1CK.) For example, the ordinal for KP + "1 admissible" is C(C(εω2CK+1,ω1CK),0), and the ordinal for KP + "2 admissibles" is C(C(C(εω3CK+1,ω2CK),ω1CK),0), and so on.
C(ω2CK,0) -- the proof ordinal for Π11-CA0
C(a+C(ω3CK,ω1CK),0) -- the proof ordinal for Π11-CA0 plus recursive ordinals are closed under the recursive function corresponding to "a" (for appropriate "a").
C(a+ω2CK,0) -- the proof ordinal for Π11-CA0 plus all ordinals are closed under the recursive function corresponding to "a" (for appropriate "a").
C(ω1+αCK,0) (for small α) -- the proof ordinal for <ωα admissibles (using a schema or the analog of Π11-CA0)
For a typical theory T strictly between ωα and ωα+1 admissibles, the proof ordinal is C(a,0) where a is the supremum of T-provable recursive-in-ωωαCK ordinals translated from ωωαCK to ω1+αCK.

To go further, suppose that C(a,0) (with a being sufficiently-closed and built-from-below) is the proof-ordinal for a natural theory corresponding to existence of certain recursively large ordinals S. Then C(f(a),0) corresponds to the proof ordinal of a certain limit of S as follows: In '.. - ...' (below), '..' means f(a) is the least ordinal above a satisfying '..', while '...' is the corresponding limit of S.
Note: In these correspondences, the theory of a recursively large universe is treated with minimal unbounded diagonalization, so the theory for "the universe is recursively Mahlo" corresponds to Π¹₁-CA₀ + "for every ordinal a, there is recursively a-inaccessible ordinal", and similarly with other hypotheses, and ω recursively Mahlo ordinals corresponds to Π¹₁-CA₀ + "for every ordinal, there is a recursively Mahlo ordinal above it".
Correspondences:
admissible - limit of S
α admissibles - ω^α examples of S
recursively inaccessible - admissible limit of S.
thus, by iterating, 2 recursive inaccessibles - admissible limit of admissible limits of S (and so on).
recursively 1+n-inaccessible (n>0) - recursively n-Mahlo limit of S.
recursively Mahlo - Π₃ reflecting limit of S
2 recursively Mahlos - Π₃ reflecting limit of Π₃ reflecting limits of S
admissible limit of recursively Mahlos - Π₂ reflecting onto Π₃ reflecting limits of S
recursively Mahlo limit of recursively Mahlos - Π₃ reflecting that is also Π₂ reflecting onto Π₃ reflecting limits of S
recursively n-Mahlo - n-Π₃ reflecting limit of S, where n is the number of iterations of Π₃ reflection
Π_n reflecting - Π_n+1 reflecting limit of S (and similarly with other levels of reflection).

The above can be combined, so for example, the least admissible above two recursively inaccessibles above a recursively Mahlo corresponds with a limit of admissible limits of admissible limits of Π₃ reflecting limits of S.

For completeness, here is one restriction of the reflection configuration version (that still includes all terms in the base version):
∀x∈T_a ∀x'⊑x ∀y⊏x' (r_<Ω(x) < r(x',y) ∧ x'<y<Ω) ∃z⊒y (z<Ω) (z⊐x ∨ z < C(a, b)).
The difference is that if a chain of reflection configurations is used to collapse y, the restriction adds up all the collapses (instead of considering them individually) in deciding whether y is too large. The restriction lacks the symmetry in terms of which collapses are permissible, and its behavior is unclear. Plausibly, the virtual replication (for computing proof ordinals) is limited to being twofold; it is also unclear whether its analogs for 8 Built-from-below with Passthrough are closer to the base version or the reflection configuration version.

5    Main Ordinal Notation System

5.1    Definition and Basic Properties

Notes:
* For basic properties, see 2 A Framework for Ordinal Notations above. For example, C(a,b) = b+ω^a for a below the least ε_x>b.
* For b < Ω_n, note that Ω_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(a,b) for a=Ω₂+C(Ω₂*2+C(C(Ω₂*3,0),0),0) and b=0 (the highlighted term is between b and C(a,b)).
* Formalization of n-built from below: As before, 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 x is a proper subterm of y; identical terms at different positions are distinguished (in the quantifiers and in ⊏). If a≺_nb means a is n-built from below from <b, then a≺₀b ⇔ a<b and a≺_n+1b ⇔ ∀x∈T_a (x>a) ∃y⊒x y≺_nb. For example, a≺₂b ⇔ ∀x∈T_a (x>a) ∃y⊒x ∀z⊏y (z>y) ∃t⊒z t<b.

For n=0, this system just reaches ε₁, for n=1, this is the notation system for 2.3 Bachmann-Howard ordinal given earlier, and for n=2, the notation system is superficially similar to (but perhaps much stronger than) the one in 4 Degrees of Reflection. A natural conjecture (see 5.2 Strength of the Main System) is that the strength of the n^th ordinal notation system is between Π¹_n-1-CA and Π¹_n-CA₀ (or higher), and thus the sum of the order types of these ordinal notation systems is the proof-theoretical ordinal of second order arithmetic (or higher).

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 a is not n-built from below from b, then perform an in-order right-to-left traversal of the term tree of a to find the first counterexample: a < a₁ < a₂ ... < a_n (a_i+1 is a subterm of a_i). This occurrence of a_n is part of C(a_n, d) with C(a_n, d) < Ω_n. Replace this C(a_n, d) with Ω_n, and delete everything to the left of this Ω_n, and add the right number of 'C(' to make the new 'a' a valid term, and convert the new 'a' to the standard form.
Note: By converting between different Ω_i, the conversion for the full notation system follows.

Proposition: In the nth system, given a standard term a (in prefix form), every nonempty suffix of a augmented with the corresponding number of 'C' on the left is standard.
Note: For example, for standard C(C(a,b),c), C(b,c) is standard. Also, in the combined system, the result is standard after a possibly repeated conversion C(Ω_i+1,0) → Ω_i.
Proof: By recursion, it suffices to check when a=C(c,d), c is modified into c', and c' is standard. Since c' has no subterms between c' and c (or between C(c',d) and C(c,d), and similarly for certain subterms of c') and since the subterm tree is sufficiently preserved, the n-built from below criterion will carry over to c'.

Variations using one-variable C: If the system is expressed using C₁ (one variable C), the maximality condition on a in C₁(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₁(a) (terms use 0, Ω_n,'+', x→ω^x, and C₁ 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 to be n-built from below.

Passthrough extension: It is natural to try to extend the system by combining it with ideas from 8 Built-from-below with Passthrough. For example, let a be 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(Ω₂+C(Ω₂*2+C(C(Ω₂*3,0),C(Ω₂*2,0)),0),0) (the term is C(a,0) and c is highlighted). In defining the extension, we have to be careful to prevent passthrough from wrapping terms into built-from-below terms, which could then be collapsed into ill-foundedness. To achieve this, in C(a,b) we require that a is a,n-built-from-below from <C(a,b), denoted a≺_a,nC(a,b).
a≺_a',0b ⇔ a<b
a≺_a',n+1b ⇔ ∀x∈T_a (x>a) ∃y⊒x (y≺_a',nb ∨ y⊐x ∧ d(y)<a' ∧ ∀z (x⊑z⊑y) z≥y)
where d(C(e,f))=e (for standard C(e,f)) and d(y)=∞ otherwise. The combined system can be defined as above. A natural restriction is to prevent entering n-built-from-below stage while we are in the passthrough. The passthrough might make the system much stronger (especially if delayed diagonalization is not a problem here), but given our lack of knowledge, also has a high risk of ill-foundedness. If full passthrough is a problem, a restricted version can still likely be used for iterating n-built-from-below, as described in 7 Iteration of n-built from below.

Reflection configurations: There is also a possible variation on the main system using 2.5 Reflection Configurations (see there for terminology); its strength and well-foundedness are unclear. The nth system will require that in C(a,b), r(a) is r(a),n-built-from-below, denoted by B_r(a),n(r(a)), or if we are not using passthrough, 0,n-built-from-below. The combined system is as above.
B_a,0(d) ⇔ d < λx.x (i.e. reflection configuration d is a constant (below x))
B_a,n+1(d) ⇔ ∀x∈T_d (x⊏d ∧ r(x)>d) ∃y⊏d (r(x)⊆r(y) ∧ (r(y)<a ∨ B_a,n(r(y))).
Notes:
* Explanation of B_a,n+1(d): For every proper subterm x of d (treating constant configurations below λx.x as leaf subterms), a violation of built-from-below "r(x)>d" is in the scope "r(x)⊆r(y)" of passthrough "r(y)<a" or n-built-from-below (with passthrough) "B_a,n(r(y))".
* An equivalent construction that avoids nested configurations is to require a≺_r(a),nC(a,b) (using standard comparison for C(a,b)), or ≺_0,n if not using passthrough, with:
e≺_a,0b ⇔ e<b (note that e is an ordinal, but after pruning with z below, T_e is closely related to the above T_d; 'a' is a reflection configuration)
e≺_a,n+1b ⇔ ∀x∈T_e (x⊏e ∧ r(x)>r(e,b) ∧ ∀z∈T_e (x⊏z) z≥b) ∃y⊏e (r(x)⊆r(y) ∧ (r(y)<a ∨ y≺_a,nparent(y))).
* The scope of reflection configurations (which is narrower than the scope for ordinals) already gives us a form of passthrough, but the passthrough condition becomes relevant after our parsing leads into a higher configuration. For example, in the final stage, rather than being built-from-below (and thus in a sense, recursive), we have built-from-below with passthrough, which might be much broader.
* Given the triple permissiveness (n-built-from-below, reflection configurations, passthrough), this is the place for the interested reader to look for ill-foundedness, but quite possibly this is also the only version that actually reaches second order arithmetic with projective determinacy.

5.2    Strength of the Main System

Without a proof or a clear understanding of its structure, we cannot rule out (1). At the moment, (2) represents a lower bound on our intuitive ability to embed descriptions of ordinals into the notation system (and even there, I did not properly analyze structure at non-Gandy ordinals, which start appearing before α⁺+1-stable; α⁺+1-stable already 'looks' like stable past a recursively inaccessible for systems that ignore that structure); we do not expect the strength to be that low, but we do not yet see beyond that with a sufficient clarity. (3) corresponds to the similarity between the nth system and around n alternating quantifiers, and to a rough similarity between C_i in the passthrough system (8 Built-from-below with Passthrough below) and the usage of Ω_i (though that also suggests Π¹₂-CA₀). Bounded Zermelo set theory is also possible. (4) often shows up in certain loosely similar problems (see Harvey Friedman's work and also (Taranovsky 2012)). Moreover, the relationship between the passthrough system and the main system at level of Π_n-reflection suggests a strength beyond (3). Going further, despite inclusion of small large cardinals, L has a Δ¹₂ well-ordering (of ordinals countable in L). If second order quantifiers are fully used (corresponding to a Δ¹_n well-ordering), the strength would correspond to (5). A number of different natural additions to second arithmetic, including (conjecturally) comparability of Wadge degrees lead to projective determinacy. Our guess for the main system is (3), but we expect that a reasonable modification can be used to get (5). Perhaps, some combination of passthrough and/or reflection configurations with n-built-from-below works (see above for example systems). See 6.2 New Analysis for additional details (and possibilities).

Also, an intuitive analysis by user Hyp cos of a fragment of the main system (unmodified version) with a long list of examples can be found at http://googology.wikia.com/wiki/User_blog:Hyp_cos/TON,_stable_ordinals,_and_my_array_notation ; I have not verified its correctness.

Differences from Degrees of Reflection C

The n=2 notation system in 5 Main Ordinal Notation System is not identical to the one in 4 Degrees of Reflection. The notation system for degrees of recursive inaccessibility corresponds to the one in "Degrees of Reflection", and the assignments of ordinals in "Degrees of Recursive Inaccessiblity" and "Degrees of Reflection" should not be used for the main system. 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(Ω₂+ε_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".

Conjectured Hierarchy

For standard C (with Ω=Ω₂), 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²,0) -- least recursively Mahlo, C(Ω+d^d,0) -- least Π₃ reflecting, and so on, analogously to the description from "Degrees of Reflection".

The hierarchy would suggest that C(Ω*2, 0) should be the least ordinal x such that L_x is a Σ₁ elementary substructure of L, and this hierarchy is formalized below in 8 Built-from-below with Passthrough, which is a variation on a fragment of the main system. However, while the passthrough system makes certain collapses free, 2-built-from-below (without passthrough) gives one free collapse, which might be insufficient as we approach an ordinal a that is a⁺⁺-stable (or just Σ¹₁-reflecting). Roughly speaking, getting an ordinal d corresponding to a large level <a⁺⁺ involves one collapse and arguments corresponding to <a⁺, with a second collapse to get those arguments.

The level at which the main system reaches a⁺⁺ stable ordinals is unclear. Essentially, the worst case scenario is that correctness n>1 corresponds to the closure of {α: α is α⁽⁺⁾ⁿ-stable} (or even less, with Ω₂ possibly being the least Σ¹₁ reflecting ordinal). Consider c = C(Ω₂+a,b), and let f be an appropriate recursive ordinal function (using parameters <c; f(x)>x), and consider how f can be placed in a. In constructing c, the final collapse in the definition of f is free, which allows using f in many but not all places inside a. If we can show that the permitted places are enough, then α = C(Ω₂*2,0) would already correspond to α⁺⁺-iterations (or more if there is some stronger other structure). Note however, that places inside a that will be collapsed further impose a limit on the ordinals used in f (if placed there), which would not work for getting the strength.

While the definition of the main system is perhaps simpler than the passthrough system, the relationship between the ordinals and the notations appears more direct in the passthrough system, especially if the main system does not reach beyond second arithmetic. Assuming it is strong enough, the passthrough system probably works better for proving the exact ordinal strength of Z₂.

Higher n: If the strength of the main system corresponds to second order arithmetic, some conjectured assignments are as follows.
Ω_n (n>1) - as in the next section
C(C(C(Ω₃+1,0),0),0) - the proof ordinal of Π¹₂-CA₀, and analogously for Π¹_n-CA₀.
C(C(C(Ω₃+ε₀,0),0),0) - the proof ordinal of Δ¹₃-CA, and analogously for Δ¹_n-CA.
C(C(C(Ω₃*2₀,0),0),0) - the proof ordinal of Π¹₂+TR₀, and analogously for Π¹_n+TR₀.

Levels of Correctness

For terms in the notation system, assign correctness levels as in 4.4 A Step towards Second Order Arithmetic above. (See above for basic properties, but for example, Ω_i (i>0) is the least ordinal of correctness i.) If the notation system corresponds to Z₂, then we expect the following under the conjectured canonical assignment:
* 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_ρ.
Note: Here, ρ is an ordinal such that L_ρ satisfies ZFC minus power set. For definiteness, let ρ be ω₁^L since second order arithmetic does not prove existence ρ with L_ρ satisfying ZFC\P, but it proves as a schema that L_ω1^L satisfies ZFC\P.

5.3    Old Analysis and Examples

6    Beyond Second Order Arithmetic

6.1    Old Analysis

Notes:
* This subsection is retained for both intuitive and historical value. A more precise analysis of how C might reach ZFC and beyond is in the next section. Also, the three variable C described here corresponds with 8 Built-from-below with Passthrough system.
* Both the old (and especially) the new analysis assume some understanding of set theory. Useful references include (Jech 2006) and (Kanamori 2008).

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 Ω²+ω 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 3 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 ≥ω_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 Ω₁, Ω₂, ..., (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.

Collapsing functions

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₁, g₂, ... 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 notation system

[Update: Retained for historical purposes, but 7 Iterations of n-built from below is (at present) a better candidate. Also, it is unclear whether the system is related to 8 Built-from-below with Passthrough, and the caveat of it being a guess (that possibly was not thought through) applies.]
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₁, a₂, ..., a_n, b) corresponds to 2-variable C((a₁, ..., a_n), b) if (a₁, ..., 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₁)=a₁, and standard form prohibits a₁=0. Thus (as written in 2.2 Basic Properties section for general C), it suffices to state the maximality condition.
(a₁, ..., a_n) is maximal in C(a₁, ..., a_n, b) iff for each i 1≤i≤n, a_i is <(a₁, ..., a_n) built from below from <C(a₁, ..., 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₁, ..., 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₁,...,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²,0), and so on.
Instead of n-tuples (as in (a₁, ..., 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)<Ω.)

6.2    New Analysis

Introduction and notes:
* This section provides insights about ordinals and cardinals (especially in L) and how a C-like system is likely to work there. The specific analysis is for a system behaving like 8.2 Degrees of Reflection with Passthrough but without delays in diagonalization. We refer to it as the n=2 system, though whether the main system for n=2 behaves like this is not clear. The system is (actually or hypothetically) extended to higher n analogously to the main notation system.
* If either the main system, or Degrees of Reflection with Passthrough, or a passthrough extension of the main system (or a system using reflection configurations) works like that, then most of the analysis should be (approximately) accurate for that system.
* The ordinal assignments may seem high, but keep in mind that in L, all reals are Δ¹₂ in a countable ordinal, and if the notation system has mastered Σ_α-elementary substructures in L (and transitive collapses), the constructible versions of (small) large cardinals start to resemble the recursive versions (but with additional structure).
* If Degrees of Reflection with Passthrough (or a fragment considered, and especially if not using reflection configurations) is too weak, we conjecture that the assignment can still be defined and formalized by relying on the extensibility of the system (while keeping the assignment unchanged), though it is unclear how the extensibility should be formalized. Such an assignment would still qualitatively enhance our understanding of ordinals and cardinals, but there are points where it would fade out. One possibility is that for a theory T, models of T at definability level α are only captured if T is not too strong relative to (and has an appropriate definition at) the next definability level above α. Thus, the least rank-initial model of ZFC (or V_δ^L⊨ZFC) would likely be captured, but because ZFC is too strong relative to the concept of transitive models, the least transitive model of ZFC would not. Or more precisely (if the system is parameterized by an ordinal notation system O built above all ordinary ordinals), the supremum of the heights of the least transitive models of finite fragments of ZFC would then likely equal C(1,δ,0) where δ corresponds to the O-term (or diagonalization level) corresponding to the proof ordinal of ZFC.

Note: We will work in L (where V=L).

Previous introduction: To inspire future research, here is an optimistic guess about the strength of C. 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 8 Built-from-below with Passthrough (and in particular Degrees of Reflection with Passthrough) and in effect analyze that system, and that section (below) will help the reader to understand the discussion here. However, whether the analogy holds is unclear, and should the main system be too weak, the comments below for the n=2 system might still work for Degrees of Reflection with Passthrough (though it could be too weak as well), with n=3 and higher systems not yet defined (but see passthrough extensions to the main system for a possibility).

C(Ω*a+b,c) for b<C(Ω*a+b,c) should be ordinal number ω^b of definability/reflection level a above c (here Ω is Ω₂). Otherwise (i.e. b>C(Ω*a+b,c)), b has a canonical definition "b" (using ordinals <C(Ω*a+b,c) as constants), and C(Ω*a+b,c) is roughly the least ordinal corresponding to definability level a model of "b" (above c). For example, if a=1 corresponds to transitive models, then (working in L and assuming we have enough strength and there is no acceleration or delay) 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 and insight, let us analyze the Σ₂ hull of L. Here, we can have large cardinals but every set will be Σ₂ definable, or Σ₁ with the cardinality predicate. Thus, the supremum of the hull is also (in a sense) the supremum of built-from-below ordinals with the L-cardinality predicate. When a is sufficiently definable, c having definability/reflection 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_κ≺_Σ1L is the least ordinal such that transitive models for arbitrary sufficiently satisfiable axioms exist below κ. Assuming the base theory T gets its strength from the large cardinals it asserts, these axioms correspond to large ordinals/cardinals, so C(Ω+b,0) (as b→∞) should cover transitive models for theories <T, so C(Ω*2,0)=κ.

Approximate definability level correspondence for c=C(Ω*a+a₁,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). (Update: Per 8.5 Well-foundedness with Reflection Configurations, we likely need some diagonalization on a to get there (if we get there at all), probably around ω₁^L*a for countable b. The systems do not have bounded-quantifier definability built-in, and with passthrough being a partial substitute, getting to Σ₁ correct α (above a given ordinal) corresponds to up to α iterations of the Σ₁ truth predicate, with each iteration increasing the level of definability.)
large a<Ω -- c is not Σ₁ definable in (L_κ+a, ∈, Card) (Card is predicate for cardinals (in L)) allowing ordinals <c as constants, where κ is the least cardinal above c.
a=Ω -- cardinals. C(Ω²+a,0) is ω_ω^a for a below the least fix-point of the aleph function.

Large cardinal structure below subtle cardinals is intertwined with indescribability. For every appropriate notion of indescribability, there is an indescribable cardinal below the first subtle cardinal (and ω₁ is the analog of this for indescribable ordinals), and since we are in a Σ₂ hull, an indescribability notion corresponds to an ordinal where the notion is Σ₁(card) definable, and related collapses will yield indescribable cardinals for the notion.

To start, 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 Σ₂ statements.
the least κ such that V_κ≺_Σ2V_λ. κ is also the least fix-point of f where f(a) is the least b such that V_b and V_λ satisfy the same Σ₂ statements with parameters in V_a.
the least κ such that V_κ≺_ΣaV_λ. For large 'a', one analog of this is the supremum of ordinals <λ that are Σ₁(Card) definable in L_a using parameters <κ.
Note the parallel between these notions and ordinals ≥λ that are below λ⁺ (the cardinal successor of λ), and our intuitive analysis suggests this analogy also applies to the notation system (hence the choice of the notation for the least inaccessible cardinal).

Let C(a,b,c,d) = C(Ω²*a+Ω*b+c,d) and C(b,c,d) = C(0,b,c,d), and x⁺ = C(1,0,0,x) (the cardinal successor of x), and let S=C(1,1,0,0).
C(1,0,S,0) -- the least fix-point of x→ω_x.
C(1,0,C(1,0,S),0) -- a lower bound on the least power-admissible ordinal. However, this treats C(1,0,S) as admissible, and just like the correction for Σ_a elementary substructures, the next admissible above S might be C(S+2,0,S) (or in any case, above C(1,0,S)), though C(1,0,C(S+1,0,S),0) might suffice for the least power-admissible ordinal. For simplicity, the below terms do not use this correction; the reader can treat C(a,b,c) as requiring some higher a, but with our use of S⁺ unaffected (so for example, the least inaccessible does not need a correction).
C(1,0,C(2,0,S),0) -- might be the least cardinal κ such that V_κ and V_λ satisfy the same Σ₂ statements, where λ is the least inaccessible cardinal.
C(1,0,C(2,0,S)*S,0) -- might be the least cardinal κ such that V_κ≺_Σ2V_λ, where λ is the least inaccessible cardinal.
C(C(ω,0,S),0) -- might be the proof theoretical ordinal of ZFC.
C(1,0,C(a,0,S),0) -- approximately the least cardinal κ that is not Σ₁(Card) definable in L_a (for appropriate large a ) using parameters <κ. Equivalently, it is the least κ that is inaccessible in the collapse of Σ₁(Card) Skolem hull of L_a where ordinals <κ are constants.
C(1,0,S⁺,0) -- the least inaccessible cardinal.
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(2,0,S)*S,0) -- might be the least cardinal κ such that V_κ≺_Σ2V_λ, where λ is the least Mahlo cardinal.
C(1,0,S⁺*C(a,0,S),0) -- approximately the least cardinal κ that is Mahlo in the collapse of Σ₁(Card) Skolem hull of L_a (for appropriate large a) where ordinals <κ are constants.
C(1,0,(S⁺)²,0) -- the least Mahlo cardinal.
C(1,0,(S⁺)³,0) -- the least hyper-Mahlo cardinal.
C(1,0,(S⁺)^S+,0) -- the least greatly Mahlo cardinal.
C(1,0,S⁺⁺,0) -- might be the least weakly compact cardinal κ (assuming representations for ordinals below κ⁺⁺ can be sufficiently robust, as otherwise the least weakly compact could be lower).
C(1,0,S⁺⁽ⁿ⁺¹⁾,0) -- might be the least Πⁿ₁ indescribable cardinal.
C(1,0,a,0) -- approximately the least a-indescribable cardinal (for appropriate large ordinal a).
C(1,n,0,0) -- might be the least n-subtle cardinal.

Other possibilities for n-subtle cardinals are C(n+1,0,0,0) (with C(1,a,0,0) being approximately a-indescribable) or C(Ωⁿ⁺¹,0). While we do not see which set theoretical structures would raise the assignments this way, much uncertainty remains.

More on cardinals after the first subtle cardinal:
S is also the least cardinal κ such that for every S⊆κ, there is an S-indescribable 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.

Beyond n-subtle cardinals, we have α-subtle cardinals where instead of an n-tuple of indiscernibles, we have a well-founded tree, with the indiscernity along each branch of the tree (but not necessarily between different branches). Formally, κ is α-subtle (α≤κ⁺) iff for every α'<2+α, club C⊆κ, and regressive f:κ^<ω→κ, there is a well-founded tree of rank α' of ordinals in C such that every branch is an increasing tuple homogeneous for f. Note that a completely ineffable cardinal is α-subtle for every α, and is below the least 1-iterable cardinal. Possible assignment (low confidence):
C(1,α,0,0) -- approximately the least α-subtle cardinal (if α is not too large).
C(1,C(2,0,α,0),0,0) -- approximately the least α-iterable cardinal (in a generic extension where α is countable, and assuming the cardinal is above α).
C(1,P,0,0) -- (where P corresponds to a large cardinal axiom) approximately the least possible for a transitive model M of P, with every M-cardinal being a cardinal in L, with the M existing in a generic extension of L (note that M can have measurable cardinals and more).
Going further, recall that the above is in the Σ₂ hull of L.
C(2,x,y,z) appears work similarly but with Σ₃ hull of L, and so on.
C(α,0,0,0) -- the height of the transitive collapse of (approximately) Σ_α hull of L (assuming α<C(α,0,0,0)).
Beyond that, using n ordinals of degree Ω₂³, we get hulls using about n Silver indiscernibles, allowing us to approach the true ω₁^L.
C(C(1,0,0,1,0),0,0,x) -- the least L-cardinal above x. At this point, we effectively have zero sharp, so successor infinite L-cardinals have effective cofinality ω (with the cofinality witnessed by the notation system).
C(C(1,0,0,1,0)*a,0,0,0) -- approximately the result of iterating the sharp operation a times.
Ω₂ -- ω₁^V. We do not use ω₁^HOD because we expect that (analogously to ω₁^L) in an appropriate extension of the language of set theory, there is a canonical sequence of length ω converging to ω₁^HOD.

For the full n=2 system (or more likely, for a proper restriction of it), if we are only just beyond 0^#, one possibility is that ordinals <Ω 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) then 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(Ωⁱ*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.

However, if (per above) C(C(1,0,0,1,0),0,0,x) allows us to use ω indiscernibles, we do not see why C(ε_{C(1,0,0,1,0)+1},0,0,x) (or similar) would not reach mice below ε_Ω+1, making the system much stronger. One possibility is measurable cardinals with o(κ)<ε_κ+1. In that case, C(Ω³α,..) may correspond to iterating measurable limit of measurables α times (or so), and C(Ω^α,..) may correspond to measurables of order around α (and their limits).

Beyond n=2

Beyond n=2, as of this writing, our understanding is very limited, so we present 3 options.

The low option assumes that we are missing something, and do not reach Woodin cardinals. For example, Σ¹_n+3 generic absoluteness is equiconsistent with n strong cardinals (with model also apparently having Σ¹_n+3 uniformization), and it could be that some of the systems are stuck there.

For the main option, we note that 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.

For the (aspirational) high option, we transcend Woodin cardinals, with C(Ω₃+α,0) (or some other term) corresponding to a countable mouse with roughly α (or ω^α) Woodin cardinals. A natural higher stopping point is supercompact cardinals, but perhaps we get to n-huge cardinals (if not higher). One optimistic possibility is that ordinals of correctness n>2 naturally correspond to (approximately) n-2-reflective cardinals (and their limits) (reflective cardinals are defined in (Taranovsky 2012)), and also that n-reflective cardinals agree with the critical sequence of an n-huge embedding. (Note that the first is about the level of expressiveness, while the second is about strength, and capturing n-reflective cardinals in V may or may not naturally correspond to reaching (approximately) n-huge cardinals analogously to how the expressiveness of second order arithmetic leads to the strength of Woodin cardinals.) The supremum of representable countable ordinals might then be ω₁^HOD (recall that reflective cardinals go beyond (V,∈) definability). Also, n-huge cardinals have a natural definition using a normal ultrafilter, and can also be characterized by M (with a nontrivial elementary j:V→M and crit(j)=κ) including a sufficient fragment of the embedding, j''(j⁽ⁿ⁾(κ))∈M.

7    Iteration of n-built from below

By iterating n-built from below, we get a candidate stronger notation system, but its strength and well-foundedness are unclear. The construction is similar to 8.2 Degrees of Reflection with Passthrough (especially for handling the limit stages of the iteration), but with additional complications. For relevant subterms we have to set the permissible n (for n-built-from-below) so as to prevent infinite regress, which we accomplish by reading off n from the portion of term that is sufficiently stable relative to the subterm.

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 the representation of a in terms of ordinals <Ω representation of a is a''-n-built from below from <C(a,b). See below for definitions.
Possible extension: Use a-n-built from below (but n will still be based on a'').

Definitions:
4. 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 proper subterm of C(c,d) with c<a'' that is not in the scope of a subterm of C(c,d) that is <C(c,d).

5. Testing for <C(a,b) can be done in the ordinary lexicographical order.
6. a'' is the part of a that is not affected by taking the limit a'→Ω. n is the integer part of the leftmost outermost subterm e of a'' that is not C(f,g) with f≥Ω. (The integer part of e is the maximum n such that e (as a string in the prefix form) begins with n-fold repetition of 'C0'.)
7. To get the limit in (6), 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; replacement order does not matter). a'' (as a string) will be the largest common suffix of a and a_lim, with enough 'C' added on the left to be well-formed, or if a'' is empty, replace it with 0.

Extensions: If for representing ordinals above Ω (in terms of ordinals <Ω), we use a given C (perhaps using Ω' to go beyond CNF), the above construction applies, with the limit in (6) obtained directly using nonstandard forms above Ω (it is unclear if the computation in (7) will work for typical C).

Variation using CNF base Ω:
(1)-(5) are as above, except as modified below.
8. 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 <Ω.)
9. 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).
10. n=max(m∈ℕ: ∃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').

Notes:
* In 4, 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).
* A convenient variation is to use n+1 instead of n; it has the same strength but especially for a<Ω, more closely resembles our other systems.
* As written, if Ω^c*d is deleted because d is deleted, subterms of c might still be used for setting n.
* 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.
* A variation (apparently permitting fewer terms) is not to consider ordinals inside passthrough (4(b)) as candidates for a''-n built from below (4a), thus making the structure of C(c,d) above <C(c,d) irrelevant.
* Reflection configurations: For the CNF version, given our special use of the integer part, reflection configurations are only (unconditionally) defined above limit ordinals (and they use CNF base Ω above Ω). For b+ω, configurations above <(b+ω) use a fictitious limit ordinal x with b<x<b+ω. This limitation does not apply to configurations that do not use Ω (except in constants below x). It also does not apply to the C version (except for configurations above 0, and even that would work if we extracted n in (6) using e=f+ω^g*n with f>0, or alternatively treated C(0,..) above Ω as a unary function).
* The well-foundness of the possible extension is unclear. We still need to be strict about n so as to prevent infinite descending sequences like Ω, C(Ω+1,0), C(C(Ω+1,0)+2,0),... (each lower ordinal gets a higher permissible n).

To understand the system (using CNF base Ω), consider the segment that uses only C(a,b,c) = C(Ω*a+b,c) (with a,b,c <Ω). 4 requires that b is a-n-built from below from <C(a,b,c) where n is the integer part of a. (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, 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. If the main notation system corresponds to Z₂+PD, for limit a, the level may correspond with J_a(ℝ), and then one repeats n-built from below construction but this time assuming that for lower levels definability has been completed, hence 4b. The sense of 4b is that C(c,d) is treated as representing C(c,d) in terms of ordinals <C(c,d), and which intermediate ordinals >C(c,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''.

Strength: For all we know, if the main system corresponds to second order arithmetic or lower, the strength here might be only slightly higher than second order arithmetic (or even lower, or if above Z₂, just slightly below existence of L_εω1+1). However, if the main notation system (that uses Ω_n) reaches Z₂+PD, 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 (of variable countable ordinal length) with a level n round (schema given n), where level m rounds consist of level m-1 subrounds, with the number of subrounds (or number of moves for level 1 rounds) 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.)

A question regarding this assignment of strengths is that if n-built-from-below leads to around n Woodin cardinals, what happens if the system were built using (say) 5-built-from-below throughout. On one hand, it is unclear what would prevent it from accumulating Woodin cardinals (at a slower rate, getting around kα (k<5) in place of ωα Woodin cardinals at similar points), but on the other hand, the construction appears weaker than (say) 7-built-from-below (in the main system). It is possible that our conjectured strengths are wrong, with a small chance that the main notation system already reaches n-huge cardinals.

Further extensions:
* While the strength can be increased slightly by going beyond ε_Ω+1, new construction principles are required to reach substantially further.
* One approach is to set n in some way that more closely approaches self-reference.
* Another approach is that 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 here is just an illustrative guess and might well be either ill-founded or failing to reach further. In 4 (above), for the variation using CNF base Ω, 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) Ω^ω, where the significance level of a' in Ωⁿa' is (essentially) n.)

Reflection configuration version: If iterations of n-built-from-below is weaker than expected, using 2.5 Reflection Configurations may allow the system to get the right strength. The definition combines the reflection configuration definitions for the main notation system and for Degrees of Reflection with Passthrough. Let r' denote r_<Ω. For comparing configurations, Ω stands for λx<Ω.Ω. The relevant condition will be that for every c<Ω in the representation of a in terms of ordinals <Ω, B_r'(a),n(r'(c)) holds (or B_r'(a''),n(r'(c)) for the unextended version).
B_a,n(d) means that d is a,n built-from-below.
B_a,0(d) holds iff d is a constant (below Ω = λx<Ω.Ω).
B_a,n+1(d) holds iff (with quantifiers ranging over T_d)
∀x⊏d (d < r'(x) < Ω) ∃y⊏d (r'(x)⊆r'(y)) (y<Ω ∧ B_a,n(r'(y)) ∨ parent(y)<Ω ∧ r'(y)<a).

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

8    Built-from-below with Passthrough

8.1    Definition and Properties

Here we present an ordinal notation system with conjectured strength beyond Π¹₂-CA₀, and below (8.2 Degrees of Reflection with Passthrough) we hope to reach beyond ZFC. The system comes in two versions:
* The basic version. It behaves very similarly to the extended version (which makes it exceptionally precise in imitating second order arithmetic), except that because of delayed diagonalization, we suspect that it is weak. In 8.3 Proofs of Well-foundedness, we prove its well-foundedness using large cardinals, with the proofs perhaps extendible to other systems.
* The extended version that uses reflection configurations and should have the right strength. Its well-foundedness up to level ω is proved in 8.5 Well-foundedness with Reflection Configurations, which can be read independently of the intermediate sections. The proof uses Π¹₁ soundness of Π¹₂-CA₀, which is presumably optimal.

Update (March 4, 2020): The strength up to level ω is limited to Π¹₂-CA₀ rather than Z₂ (see the detailed discussion after the proof for the adjustment in the canonical assignments of gaps). However, the previous suboptimal assignment of gaps simplifies and illuminates the structure of ordinals, and is a good starting point for making optimal assignments in the future (including assignments using a stronger system such as 8.2 Degrees of Reflection with Passthrough). Thus, we keep the assignments in the exposition below (especially in the "Levels of stability" paragraph). Ordinals below the least Σ¹₁ reflecting ordinal are unaffected.

Intuition: 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. The system can be described as built-from-below with passthrough for lower reflection levels.

Relation with the main system: C_i(a,b) superficially corresponds with the main system C(Ω₂*i+a,b) with a,b<Ω₂ and a and b representable without using ordinals ≥Ω₂². However, the 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₀(C₁(C₂(0,0),C₂(0,0)),0), and most likely, the main system misses too many terms for the above correspondence to approximately hold. In the other direction, not all valid main system terms that do not use ordinals ≥Ω₂² become valid C_i terms; an example is (courtesy of Hyp cos) C(Ω₂+C(C(Ω₂*2+C(Ω₂+C(Ω₂,C(Ω₂*2,0)),0),0),C(Ω₂*2,0)),0).

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 proper 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 <C_j(e,f). In other words, C_j(e,f) is treated as representing the ordinal C_j(e,f) in terms of ordinals <C_j(e,f), and which intermediate ordinals >C_j(e,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₂(0,0), and for readability allow ordinal addition.
C₁(M+C₁(M*2,0),0) is invalid because M+C₁(M*2,0) uses a higher ordinal (M*2).
C₁(C₀(C₃(0,0),M),0) is valid because of the passthrough for C₀. As far as C₁ is concerned, we are not using C₃(0,0) as an ordinal but merely as a notational shorthand to define C₀(C₃(0,0),M) in terms of M.
On the other hand, in the first example, M+C₁(M*2,0) = C₀(C₁(M*2,0),M) and C₁ "knows" what is C₀(C₁(M*2,0),M) in terms of C₁(M*2,0) and M but cannot handle C₁(M*2,0) because M*2 is larger than M+C₁(M*2,0).

Proposition: In the definition of C_i(a,b), it is sufficient to allow ordinals ≤b as constants. For the passthrough it does not matter whether we use ≤f or <C_j(e,f).
Note: Out of the four equivalent possibilities here, we chose the one with the best extensibility by emphasizing C(a,b) rather b. The second statement in the proposition also holds for the reflection configuration version since i<C_i(a,b).
Proof: Regarding passthrough, all terms strictly between f and C_j(e,f) have degree <(j,e), so passthrough applies to those terms as well. Regarding ≤b vs <C_i(a,b), 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-foundedness). 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 α.

Terms that are built-from-below typically correspond with recursive terms, or to ordinals below the proof ordinal of the theory represented. Since built-from-below terms are captured by C₀, a natural assignment is to set C₁(0,x) as the next admissible ordinal above x. Moreover such assignment is canonical in its ability to keep existing terms unchanged as one extends C₀ to a stronger recursive system. The relationship for higher C_i and C_i+1 is analogous. We conjecture that this extensibility (properly formulated) can be used to formally define the canonical assignment of ordinals (and that the strength of the system corresponds to (or is weaker than) the assignment).

Reflection Configuration Version: If (as it seems likely; see proof ordinals below) the delay in the ability to do diagonalization affects the strength, our remedy is to use 2.5 Reflection Configurations rather than degrees. In (for example) C_j(c,M) (j≥i) as part of C_i(a,b), the relevant test will be not whether c<a, but whether what c is to C_j(c,M) is less than what a is to C_i(a,b), which is expressed using reflection configurations.
Formalization: In the subterm tree (with terms in different positions distinguished) for C(a,b), let r(c) for c in C_j(c,d) be the reflection configuration of c above C_j(c,d); these are the only configurations we need. In the definition of the system, replace "a does not use ordinals above a" with "a does not use reflection configurations >r(a)".
Notes:
* Out of j,e,f, only e can be bigger than C_j(e,f). Thus, in the original version, it suffices to test e (for being >a), and in this form, the only difference (from using reflection configurations) is in how e is tested.
* All terms valid in the basic version are also valid here because in the relevant case, C_i(a,b) < C_j(e,f).

One variable C: We will use 2.4 One Variable C, with C'_i(ω^a_n+...+ω^a₁) = C_i(a₁,...,C₁(a_n,0)..)) (standard term). Note that C'_i(0) = 0 and C'_i(ω²) = C_i(ω2,0).

Conjectured Strength: Despite being formally weaker (for n>1), in many ways the C_n system (n>0, terms only use C_i for i≤n) corresponds to Π¹_n-TR₀. (TR stands for transfinite recursion and 0 indicates limited induction.) For a conjectured natural assignment of gaps, C_1+i returns ordinals κ such that L_κ≺_Σiω₁^L for i>0, allowing transfinite i, and C₁ returns admissible ordinals and their limits, and with ordinals below C₁(0,0) recursive. The proof theoretical ordinal of second order arithmetic would be C₀(C_ω(0,0),0) = C'₀(C'_ω(1)) — if the system were strengthened to match the assignment of gaps. The full system would 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₂(0,0) = C'₂(1), and let x⁺=C₁(0,x), and N = M⁺.
    C'₁(a) for a<M enumerates admissible ordinals <M and their limits, C'₁(M+a) enumerates fix-points of the above enumeration, C'₁(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'₁(N+a) (a<N=M⁺) enumerates recursively inaccessible ordinals <M and their limits, and so on with N being similar to Ω in 4 Degrees of Reflection. For example, C'₁(N^NN2+N*16+N^NN*15+N^N*N*14+N^N*13+N²*12+N*11+10) should be the 10th admissible above the 11th recursively inaccessible above the 12th recursively hyperinaccessible above the 13th recursively Mahlo above the 14th admissible limit of recursively Mahlo ordinals above the 15th Π₃ reflecting ordinal above the 16th Π₃ reflecting ordinal that is Π₂ reflecting onto Π₄-reflecting ordinals. Note that while diagonalization in "Degrees of Reflection" uses built-from-below ordinals <Ω, here we first collapse a built-from-below ordinal into an ordinal <M⁺ (or another appropriate ordinal), and then use it (using passthrough).

Levels of stability:
Going further, for appropriate f, C'₁(f(M)) is roughly the least ordinal c that is f(c) stable. However, this is approximate.
* Note: The treatment of ordinals here assigns C₁(0,κ) for admissible κ to the supremum of κ-recursive well-orderings, which while true up to the least Σ¹₁-reflecting κ (and slightly beyond), understates (as the above update notes) the complexity inside Σ₁ chains.
* C'₁(M⁺⁺) is the least Σ¹₁-reflecting c (and thus the least non-Gandy c) as opposed to the least c⁺⁺ stable c. Also, for non-Gandy κ, C₁(0,κ) appears to be the supremum of κ-recursive well-orderings of κ, with the next admissible above κ being C₁(0,(C₁(0,κ)) instead, or even higher for very strong reflection levels (or if we missed essential structure). (Also, since M is non-Gandy, N is not an admissible ordinal.) If L_a ≺_Σc L_b with a^+,CK<b, then the next admissible above a requires at least min(c,a)+1 iterations of C₁(0,..). If a has uncountable cofinality in L_a^+,CK+1 (this is relevant for stronger systems), then a^+,CK appears like a recursively inaccessible in the notation system (and we have not ruled out further complications).
* C'₁(φ_M⁺⁺(1)) (using Veblen φ) could be the least ordinal that is both Π¹₁ and Σ¹₁ reflecting.
* C'₁(φ_M⁺ⁿ(1)) (n>2) could be the least ordinal stable up to n-1 admissibles.
* C'₁(M^+ω) = C'₁(C₁(1,M)) is likely the least ordinal that for every n<ω is above an ordinal that is stable up to n admissibles.
* C'₁(φ_M⁺ (M^+ω+1)) is likely the least ordinal that for every n is Π¹₁-reflecting onto κ⁺ⁿ-stable κ . The use of φ appears analogous to the assignment of degrees for "Degrees of Reflection" above; different reflection levels can be combined and iterated similar to that assignment.
* C'₁(M^+(ω+1)) is likely the least κ^+ω-stable κ.
* For the basic version, the least ordinal stable up to a recursively inaccessible ordinal is likely C'₁(C'₂(2)⁺). This is the because C'₂(2)⁺ = C₂(0,M)⁺ is required to get the first recursively inaccessible ordinal above M, I = C₁(C'₂(2)⁺,M) (and I is the first relevant ordinal that requires C'₂(2)⁺). The least ordinal Π¹₁-reflecting onto ordinals stable up to a recursively inaccessible is likely C₁(C'₂(2)⁺+φ_M⁺(I+1),0), and similarly with other ordinals. However, for the reflection configuration version, built-from-below is more permissive, and the ordinals are C'₁(I) and C'₁(φ_M⁺(I+1)), respectively.
* For the basic version, the least ordinal above x<M stable up to a nonprojectible ordinal could be C₁(C'₂(ω)⁺,x), in which case the height of the least transitive model of Π¹₂-CA is C₁(C'₂(ω)⁺+1,0). For the reflection configuration version, use C'₂(2) in place of C'₂(ω).

Additional intuition: In c = C_i(a,b) (for the standard choice of a), let M = C_i+1(0,b). c is the least ordinal >b that satisfies (approximately) T, where T denotes the reflection properties of M up to a (using ordinals <c in C_i(a,b) as constants), and (as a description) T works at absoluteness level i. Now, C_i(a,b) is monotonic (including in a), and to achieve that, the standard a is built-from-below using functions that are sufficiently absolute between c and M. For example, C₀(a,b) gives a recursive-in-b ordinal, and the ability to use passthrough for C₀ corresponds to Π¹₁-absoluteness for appropriate transitive models. Now, Σ_i elementary substructures agree about Σ_i formulas, and each increase in i corresponds to an extra quantifier, or an extra definability level for the passthrough.

Proof ordinals in the reflection configuration version:
* Like in 4.5 Reflection Configuration Version, the use of reflection configurations can replicate the structure ω (or more) times.
C'₀(N) is likely the proof ordinal for Π¹₁-CA₀ + ω recursively inaccessible ordinals, and similarly with N² and recursively Mahlo ordinals, and so on.
* Also, for typical α<C_i+2'(0), C_i'(C_i+1'(1+α)) in the reflection configuration version corresponds to C_i'(C_i+1'(ω^α)) in the base version (using canonical gaps rather than proof ordinals even if the base version is too weak for those gaps). However, above C_i+2'(0), the replication (for C_i compared to C_i+1) from the use of reflection configurations is at most ω times (and sometimes C_i is slightly behind C_i+1) because of how rapidly C_i+1 grows.
* For a hypothetical strengthening that matches the assignment of gaps:
C'₀(C'_i(2)) would likely be the proof ordinal for Π¹_i-CA₀.
C'₀(C'_i+1(1)) would likely be the proof ordinal for Π¹_i-TR₀.

Layering and delayed proof ordinals:
    However, for the basic version, C'₀(C'₂(n)) for n≤ω is only the proof ordinal of Π¹₁-TR₀ + n recursively inaccessible ordinals. To see this, let T_i,c (for sufficiently definable c) be the notation system where (1) no term or subterm is ≥c, (2) the ith recursively inaccessible ordinal is assigned to C'₂(i), and (3) in place of terms <C'₂(i), all ordinals <C'₂(i) are used as constants. If T_i+1,c is well-founded, then so is T_i,c because recursiveness of T_i+1,c combined with the recursive inaccessibility allows us to carry out an ordinal assignment. Formulated in a different and more specific way, instead of setting C₁(0,x) as the next admissible ordinal, we can set it to the proof ordinal (built above x) of Π¹₁-TR₀ + (n-i) recursively inaccessible ordinals, where C'₂(i)≤x<C'₂(i+1). Similar layering for C'_i(n) also happens with higher i.
    We have not ruled out that (for appropriate a<C'₂(ω)) C₀(C'₂(ω)+a,x) "unlocks" the strength of a above x, but our expectation is low. C₀(C'₂(ω) + C'₁(n),0) (n>1) appears to be the proof ordinal of KP + there is a limit of recursively inaccessible ordinals and n-2 admissibles above it. A lower bound on C₀(C₂(ω)*α,0) is the proof ordinal for Π¹₁-CA₀ + ωα recursively inaccessible ordinals, using diagonalization to express α > C'₂(ω). This lower bound (and its generalization to other limits) is insufficient to rule out correspondence with 3 Degrees of Recursive Inaccessibility (with C₀(C_i+1(ω)) being the proof ordinal of Π¹₁-CA₀ + ω recursively i-inaccessible ordinals), or between 4 Degrees of Reflection and 8.2 Degrees of Reflection with Passthrough.
    Ordinal notation systems can be characterized by (1) the kind of diagonalization they permit, and (2) by how high up you have to go to carry out diagonalization. On the first point, we have enough structure for Π¹₂-CA₀. However, on the second point, the notation system (without reflection configurations) resembles 3 Degrees of Recursive Inaccessibility. To give an example, while getting a diagonalization of admissibles (in typical systems) can be done above the next recursively inaccessible ordinal, here we have to wait until C₂(0,0). Note that even if C₀ is too weak in the full system, the canonicity of the above (partially given) assignment remains (besides correspondence with the reflection configuration version) in the ability to keep the assignment unchanged as one extends C₀, including in 8.2 Degrees of Reflection with Passthrough.

8.2    Degrees of Reflection with Passthrough

Notes:
* Like in the C_i(a,b) system, in built-from-below from <C(a,b), we can replace "<C(a,b)" with "≤b". Similarly, for the passthrough, it does not matter whether we use ≤b' or <C(a',b').
* The passthrough is the only difference from 4 Degrees of Reflection. The only difference in Comparison Algorithm is that the condition using T_a is now:
∀x∈T_a ∀y⊏x (x<y<Ω) ∃z⊒y (z<Ω) (z⊐x ∨ z < C(a, b) ∨ z⊐y ∧ d(z)<a ∧ ∀t (y⊑t⊑z) t≥z)
where d(C(e,f))=e (for standard C(e,f)) and d(z)=∞ otherwise. "z⊐y ∧ d(z)<a ∧ ∀t (y⊑t⊑z) t≥z" is the passthrough condition. I did not verify conversion of nonstandard forms.
* Omitting z⊐y (thus permitting z=y in passthrough) would make the system ill-founded as z=y would not restrict how y is used (as opposed to built). An example infinite descending sequence is (courtesy of Hyp cos) a₁ = M = C(Ω*2,0) and a_n+1 = C(Ω+M*a_n,0).
* While it permits many additional terms, we have not ruled out that (for typical O), it has the same strength as Degrees of Reflection. If that is the case, see the reflection configuration version below for a much stronger system (whose well-foundedness is unclear).

If the system is well-founded (which is not yet proved), a natural conjecture is that it is similar to and has the same strength as the main system for n=2, or a hypothetical passthrough variation of the main system for n=2. See 6 Beyond Second Arithmetic (above) for analysis.

An example is C(a,b,c,d) with (a,b,c) compared lexicographically. Note that allowing passthrough for b using (a,b') (b'<b) allows b to use large values of c' even when using a. While seemingly unrestricted, this only appears to be useful in the presence of large enough gaps that there is no sign of infinite regress. The passthrough for c using (a,b,c') (c'<c) is only relevant when b>c (note that a < C(a,b,c,d) here) given the built-from-below condition.

Proposition: The C_i(a,b) system above permits the same terms that are <Ω (and with the same comparison) as degrees of reflection with passthrough using pairing for O and identifying C_i(a,b) with C(Ω*i+a,b).
Proof: The only difference not addressed above is passthrough for (i',a') with i'=i and a'<a, but this is vacuous. Assume contrary, and consider a shortest length counterexample C(Ω*i+a,b) with a prohibited subterm c' = C_i(a',b') < a. Because c' is valid in the C_i(a,b) system and c'<a, the inability to use passthrough for c' does not invalidate the term, contradicting the assumption.
Note: The proposition relies on i < max(a,C(Ω*i+a,b)) and does not fully apply to extensions. A counterexample is C(Ω*i+C(Ω*i,j),0) with i = C(Ω²*2,0) and j = C(Ω²,0).

Restricted passthrough: To formalize a framework for restrictions, in addition to O, one specifies a restriction p on passthrough: Given a and a subterm (including position) d<Ω in the O representation of a, return p(a,d). The condition using ∀x∈T_a would use d(z)<p(a,x) in place of d(z)<a. For example, the multivariable built-from-below with passthrough for lower levels would use p(Ωⁱ*a_i+...+Ω*a₁+a₀, (j,a_j)) = Ωⁱ*a_i+...+Ω^j+1*a_j+1 (this is 0 if i=j; in p(..), j is used to indicate the position of a_j). If the unrestricted system (i.e. p(a,..)=a) were ill-founded (or just inconveniently strong), then between a safe choice (used above and in Iteration of n-built-from-below) and the ill-foundedness, there would be a spectrum of possibilities, with degrees of reflection with passthrough acting as a framework rather than a single system.

Equivalent definition of Degrees of Reflection with Passthrough:
* The subterm tree for a term d < Ω in terms of ordinals <c with passthrough for <a (and treating ordinals ≥Ω as syntactic constructs) is as follows.
d is the root node.
Given d' in the tree:
d'<c (or d'=0) -- d' is the leaf node.
Otherwise, d' = C(a',b') (standard form), and
- if a'<a, the immediate subterms are the terms <d' (equivalently, leaf terms <Ω) in the standard representation of d' in terms of ordinals <d'. This is the passthrough condition.
- else the immediate subterms are b' and the terms <Ω in the standard representation of a' in terms of ordinals <Ω (note that the representation is trivial if a'<Ω).
* C(a,b) is standard if the standard conditions are met (a and b are standard, and b is 0 or Ω (if using C above Ω) or C(c,d) with a≤c) and for every d<Ω in the representation of a in terms of ordinals <Ω, for every term f in the subterm tree for d in terms of ordinals <C(a,b) with passthrough for <a, f≤d.
Note: Restricted passthrough is defined analogously, using "... with passthrough for <p(a,d) ...". (Also, the use of <C(a,b) allows even a very restricted passthrough such as p(a,..)=0.)

Reflection Configuration Version: Using 2.5 Reflection Configurations, the reflection configuration version of the system is obtained (analogously to 4.5 Reflection Configuration Version) by replacing the condition using T_a with:
∀x∈T_a ∀y⊏x (r_<Ω(x) < r_<Ω(y) ∧ y<Ω) ∃z⊒y (z<Ω) (z⊐x ∨ z < C(a, b) ∨ z⊐y ∧ r_<Ω(d(z)) < r_<Ω(a) ∧ ∀t (y⊑t⊑z) t≥z)
(the only change is the use of r_<Ω)
(as before, d(C(e,f))=e (for standard C(e,f)) and d(z)=∞ otherwise) .
* Equivalently, the above definition using the passthrough subterm tree is modified as follows.
- Replace a'<a with r(a',d') < r(a,C(a,b)); the subterm tree is otherwise unchanged.
- Replace f≤d with r(f,parent(f)) ≤ r(d,C(a,b)), where parent(f) is the parent of f in the above passthrough subterm tree; the parent of d is C(a,b).
Note: Subterms in different positions are distinguished. Use standard comparison for C(a,b) (as if nonstandard C does not exist).

8.3    Proofs of Well-foundedness

8.4    Using Canonical Definitions

Here is a technique that may permit getting well-foundedness of C in the weakest system possible, though as of this writing, we do not know whether it works, and it is unclear whether the definitions give us the desired C. (For an actual presumably optimal proof using a different approach, see the next section 8.5 Well-foundedness with Reflection Configurations.) The key idea is that instead of defining C using complex ordinal recursion, we define C directly using canonical definitions of its arguments, with the twist that the arguments are interpreted not just in V but in other appropriate models. The systems can be built above an arbitrary ordinal. The assignments below leave more gaps than is canonical; the canonical assignment remains unclear.

Typical General Construction:
Ordinals ≥Ω are treated as syntactic constructs.
We will define C(a,b) with strict C, b an ordinal, a a term that may use ordinals ≤b as constants, all terms <C(a,b) are ordinal constants ≤b, and in all C(c,d) (inside a), d≥b. By recursion, this suffices to define C (for representable terms).
A valid term C(a,b)<Ω for above is evaluated as the least ordinal κ>b such that there is a structure M, and an ordinal (or well-ordering) a':
* M is based on κ (each notion makes this specific) and satisfies a correctness/closure condition based on a'.
* a' is the value of a, as computed in M. (If the computation fails, this M is ruled out.)

By induction on the complexity of terms, the definition (once specified) is complete. Note that applying the definition inside M may lead to a computation in M'∈M (with appropriate terms precomputed in M), and so on.

We start with the three-variable C, using C(i,a,b) in place of C_i(a,b). We can optionally require that C(0,a,b) = b+ω^a when 'a' is below the least fix-point x→ω^x above b, but this appears unnecessary to get the right strength. We allow the system to be built above an arbitrary ordinal (within bounds), and similarly for the four variable and other extensions.

Here is one choice of assignment (update: C(a,b,c) is presumably weaker than what is described here). For a valid term, C(a,b,c) will be the lowest ordinal κ>max(a,c) such that L_κ is a Σ_1+a elementary substructure of L_ω1^L and some level of L satisfies "κ is ω₁ and κ+a+b exists" where "b" is the canonical definition of b above c. The canonical definition is the one using C and ordinals ≤c as constants (see Typical General Construction above; M is the above level of L).

A more optimal choice that uses minimal assumptions for the fragment corresponding to Z₂ (update: the fragment below C_ω is weaker than Z₂, so the assumptions are not minimal) is the following: C(a,b,c) is the least a*κ+b'-stable κ>max(a,c) with L_κ a Σ_a elementary substructure of L_ω1^L where b' is b computed inside L_κ but with subterms ≤c replaced by constants (outside of L_κ). A further step to optimality is to use Σ_a-1 elementarity for finite a, using admissible ordinals for a=1, and using no gaps (if all ordinals ≤c are permitted) for C(0,b,c). To complete the optimality, one would apply a construction similar to 4.3 Assignment of Degrees, but it is unclear how to extend it to the high strength level here.

Degrees of reflection with passthrough: While the system is likely stronger than this (unless we use the version without reflection configurations, which is likely below Z₂), if it were defined more narrowly so as to correspond to L_εω1^L+1, the following construction might work: C(a,b) is the least κ with L_κ+a' elementarily embeddable into some L_ω1^L+a'' with critical point κ, where a' is obtained from a by representing a in terms of ordinals <Ω, replacing terms ≤b with constants, and then interpreting the resulting expression in L_κ (instead of L_ω1^L). Also, the assignment of individual ordinals can be optimized by separating a as a₁*Ω+b₁, using Σ_a1 elementary substructures (using diagonalization to get a₁≥ω₁), and using appropriate levels of stability for b₁. It is unclear whether this interpretation satisfies C(Ω*C(Ω²,0)+C(Ω³,0),0) < C(Ω*C(Ω²+1,0),0) (a typical example in Degrees of Reflection with Passthrough). If it does and there are no other issues, that would suggest that the strength of Degrees of Reflection with Passthrough is only rudimentary set theory + ∀α "L_ω1^α exists".

Four Variable C

For the four variable extension C(a,b,c,d) (based on Degrees of Reflection with Passthrough or a similar system if the former is too weak), the following might work. Roughly, a corresponds to the level of indiscernibles preserved, b to the correctness for that level, and c to the object being modeled. Let Ω be a sufficiently-closed ordinal, and let I_a be indiscernibles of level a<Ω for V_Ω; for each a, Ω is the maximum element of I_a. ∀b>a I_b⊆I_a. Furthermore, I_a are good indiscernibles for V_Ω augmented with (as a single symbol) (I_a':a'<a). Here, 'good' means that the indiscernibility holds even if allow parameters whose rank (as a set) is below the least indiscernible in a tuple. Regarding Ω, require that for every a<Ω such that V_Ω+a exists (this qualification is relevant for weak theories), Ω is a-I-indescribable: For every U⊆V_Ω, there is Ω'<Ω such that (V_Ω+a,∈,I,U) and (V_Ω'+a,∈,I,U) satisfy the same statements with parameters in V_Ω'. Since ∀b<Ω Ω∈I_b, I-indescribability (for a>0) ensures that ∀b<Ω' Ω'∈I_b.

For a valid term, C(a,b,c,d) will be the least Ω'>d such that
- V_Ω'+b' and V_Ω+b' satisfy the same statements with parameters in V_Ω', allowing (I_a':a'≤a) as a (single) predicate symbol. Here b' is the least ordinal such that for some I' agreeing with I_a' for a'≤a, (Ω,I') satisfies the definition of (Ω,I) in V_Ω+b'+1, with b' obtained by taking the C-definition of b above d (that is using ordinals ≤d as constants), and replacing I with I'.
- For some I' agreeing with I_a' for a'≤a, (Ω',I') satisfies the definition of (Ω,I) in V_Ω'+b'+c'+1. Here, c' is given by the C-definition of c above d, using (Ω',I') in place of (Ω,I).

Thus, Ω' is in I_a. Also, (it appears that) b' is below the next element of I_a+1. The built-from-below requirement should ensure that comparison works correctly provided that we preserved enough structure for the passthrough ability. Here, that structure is the level of indiscernibility, and for the final level reached, the level of agreement with Ω. Beyond that, built-from-below should let us get away with simulated structures: I' for b and (a different) (Ω',I') for c.

Starting with the minimum inner model L[U] with a measurable cardinal, the required indiscernibles can be constructed (using U and the indiscernibles in the model obtained by iterating U away) in a standard way. Also, it appears that we only care about indiscernibility of 1-tuples (with ordinal parameters). Furthermore, there is likely a weakening by using indiscernibles from a's iteration of the sharp. In that weakening, simulated indiscernibles (such as I') can be constructed in L (and other weak models) using a generic extension that makes Ω countable; L[(I_a':a'≤a)] is used in place of V. To get optimality, Ω (or the starting Ω) can be chosen as the least element of I_a+1 above d; the extent of I' will depend on b and (for Ω') c. Assuming it works and is optimal (for some system, perhaps with additional terms), the strength is that of "rudimentary set theory plus the sharp operation can be iterated any ordinal number of times".

8.5    Well-foundedness with Reflection Configurations

In this section, we give a (presumably) optimal well-foundedness proof of the conjectured system for Π¹₂-CA₀. Here, the nth passthrough system is the system using C_i with i<n (8 Built-from-below with Passthrough), using reflection configurations. The proof ordinal of Π¹₂-CA₀ is expected to be C₀(C_ω(0,0),0).

Theorem: For every n, Π¹₂-CA₀ proves that the nth passthrough system is well-founded, even when built above an arbitrary ordinal.

Proof: For every ordinal α, we will consider the system built above α. Our convention for the systems is that in C_i(a,b), b≥α, with b=α treated as minimal. Note that if α<α', then by replacing α with α', we get an order preserving injection of the system into one built above α'.

Let us say that the C₀ in C₀(a,b) is good if the reflection configuration of C₀(a,b) above <C₀(a,b) is well-founded above every ordinal even after replacing the constants ≥α with arbitrarily large ordinals (preserving order). Note that the configuration is some λx f(x,c₁,c₂,...,d₁,d₂,...) with c_i<α and d_i≥α, with the test being that for every ordinal β, there are e_i>β (with the right order) such that for some (equivalently every) γ>max(e_i), in the system above γ, f(γ,c₁,c₂,...,e₁,e₂,...) is valid and well-founded. Because of the monotonicity of f, the test is Π¹₂, and the selection of e_i does not matter as long as we have the right ordering. Now, let λ be the least Σ₁ correct ordinal. Any ill-foundedness is witnessed below λ: If we replace c_i≥λ with arbitrarily large ordinals (with the right order), ill-foundness is Σ¹₂, and so the witnesses can be found below λ (and since they are lower than the c_i we replaced, we get the required ill-foundedness). Thus, a single instance of Π¹₂ comprehension (independent of α) identifies the good portion of C₀.

Define the first trim by requiring that all C₀ are good. Because of the goodness, for every well-founded b, every term below C₁(0,b) is well-founded. Moreover, changing the base α to α'>α does not change which terms are good (not counting new good terms that use ordinals in α'\α). The analogous properties also hold for the nth system below. To see the well-foundedness, note that all reflection configurations used for builting ordinals above b in terms of ordinals ≤b (even for systems built above a lower ordinal) are relative to ordinals above b, so well-foundedness is not lost by having structures below b instead of building above b. Also note that for large enough α, all configurations that are not good are ill-founded in the system above α.

Analogously, in the first trim, define goodness for C₁ in C₁(a,b). Define the second trim by requiring that all C₁ are good, except for those inside a C₀ passthrough. Continue for all C_n (protecting C_i passthrough for i<n). The nth trim is well-founded since C_n(a,b)>a.

Our goal is to prove that if the (m+1)th trim is the same as the final trim for all α, then so is the m-th trim. Assume contrary. Pick a large enough limit α. Let a₀ in the (m+1)th trim be minimal such that c=C_m(a₀,α) is excluded, and hence ill-founded. But then c is the least term that is excluded from the system, and thus well-founded. For if a term is ill-founded and is not of the type C_m(a,α) with 'a' in the (m+1)th system, then it must use a smaller ill-founded reflection configuration through a subterm:
- If C_m(a,b) is ill-founded for well-founded b, we can move it down to get ill-founded C_m(a',α).
- In C_m(a,α), 'a' can only use lower configurations outside of passthrough.
Proof complete.

Notes:
* Well-foundedness of h = λx f(x,c₁,c₂,...,e₁,e₂,...) in the proof is equivalent to well-foundedness of a single reflection configuration. It appears that we can syntactically obtain the least reflection configuration ≥h whose constants are limited to c₁,c₂,... ; in any case, we can have x<min(e_i)+ω and consider the configuration above min(e_i).
* Instead of varying α, we could have built the system above any sufficiently large ordinal.
* In Π¹₂-CA₀, in place of C₀, we could apparently have used an arbitrary ordinal notation system (coded by a real number) above a generic ordinal. (Recall that for a system above a generic ordinal, comparison and validity of terms depends only on the comparison of variables.)
* The C₀,C₁,...,C_n system ((n+1)th system above) appears to correspond to Π¹₁-TR₀ + n-1 iterations (starting at 0) of Π¹₂ comprehension.
* While the proof does not immediately extend further, the full C_i(a,b) system likely corresponds to Π¹₂-TR₀.

The ωth system

For the ωth system, we can do the construction in the proof as a schema in Π¹₂-CA₀. An interesting question is whether in some model of Π¹₂-CA₀, perhaps even one satisfying all true Σ¹₁ statements, every ordinal gets a (possibly nonstandard) notation in this system (and if not, then how to expand the construction to make it happen).

In any case, for every standard term, Π¹₂-CA₀ proves that the term is included in the construction (note that correctness of comparison of included terms is automatic). For if not, consider the shortest counterexample C_i(a,b). Just like in the theorem, for standard i and m, we have well-foundedness of the portion of the ωth system (even above an arbitrary ordinal) using C₀,...,C_i-1 from the ith trim (as in the proof) and no C_m' with m'>m outside of the passthrough for C₀,...,C_i-1. Therefore, as required, the reflection configuration to test for C_i(a,b) is also well-founded because for large enough m, it and all lower relevant configurations are in the above portion of the ωth system.

We can get a single statement instead of a schema by using a cut I consisting of n<ω such that above every real, we can iterate Π¹₂ comprehension n times. Let the final trim of the ωth system allow C_i with i∈I for the ith trim, and other C_j when protected by passthrough in C_i. Provably in the theory, above every countable ordinal, every term that does not use C_i for i∉I is included in the final trim.

We can also 'cram' the system (or at least its terms of standard length) below ω₁^CK by cutting off the first trim, if it is nontrivial, below the largest included λx C₀(C_n(0,x),x), and similarly with other trims. Thus, in the partial well-ordering of formulas that provably denote an ordinal Π¹₂-CA₀, the rank of the formula denoting ω₁^CK is at least the order type of the ωth system. (Recall that this ranking overshoots the canonical assignment by using nonrecursive formulas for recursive ordinals; in a sense, the rank is not internal to the theory.) To go further, we can consider the rank of Ord in this partial well-ordering, or even further, we can consider formulas (or formulas of limited complexity that are properly handled by the theory) that provably in Π¹₂-CA₀ define a prewellordering of real numbers, with the formulas partially ordered under provable embeddability into a proper initial segment.

Assuming the strength is as expected, we completed one part of the ordinal analysis of Π¹₂-CA₀. The other two parts are the canonical assignment of the gaps and the proof of the lower bounds on the strength.

An adjustment in canonical ordinal assignments

Some of the intuitive correspondences (including in this paper) suggested that the above system should correspond to second order arithmetic Z₂. These relied on C₁(0,b) being the next admissible, which it apparently is (even if we do not want to simplify the assignment through suboptimal gaps) when b is the least countable ordinal that satisfies some Σ¹₁ property (Σ¹₁ over L_b, but without parameters), including for example (in stronger systems) the least b that is inaccessible in L_b^+,CK. There is a recursive linear order above a generic ordinal such that for all such b, the well-founded portion equals b^+CK — and in some models of the theory corresponding to the notation system, C₁(0,b) likely acts as such an order.

Specifically, there is a recursive order-invariant linear order f on ℚ^<ω such that for all such b, the initial well-founded portion of f restricted to b^<ω has length b^+CK. (By order invariance, it does not matter how b is embedded (preserving order) into ℚ, and f also makes sense for uncountable ordinals.) We can construct such f by maximizing the initial well-founded portion across all f and b (for all ordinals b). Enumerate bounded-time computable orders, and encode a tree (and use its Kleene-Brouwer order) that searches for ill-foundedness as follows. Each tree node tracks some orders, and for each tracked order includes a strictly descending sequence. Extending a node requires finding a lower element (separately for each order) for all tracked orders, and at depth i, we can get to a lower branch by also tracking the i-th order. Now, for each c.e. theory T with a distinguished symbol c, there is a well-behaved tree trying to construct an ω model of T all of whose ordinals <c are below b. The tree can be linearized using Kleene-Brouwer order or we can set up f directly to work on partial orders.

However, the above equality masks that C₁(0,b) tries to construct an ordinal above b almost blindly, while b-recursive well-orderings have access to real numbers in L_b. Use of elements of L_b can increase the well-ordering length, but only when we have sufficient reflection:
Consider the minimal Σ₁ elementary chain (for corresponding levels of L) κ₁ < κ₂ < ... < ω₁^L. For α≥κ_i, a (relativized) f in the above paragraph would need an oracle outside of L_κi (or the well-founded portion of f(α) would be below α^+CK), and in a sense existence of i levels of oracles once we cross κ_i makes α^+CK ≥ C_i+1(0,α). This also appears to hold for transfinite i, so for example the proof ordinal for Δ¹₃-CA should be C₀(C_ε0(0,0),0).

For L_λ ≺_Σ1 L_δ with minimal λ (given δ) and maximal δ (given λ; so δ<κ₁) and λ<α<α^+CK<δ, the next admissible above α (i.e. α^+CK) looks like recursively inaccessible in the notation system, with further reflection properties resembling the structure of the transitive model L_δ above α. For example, existence of a Σ₁ elementary chain of length n (or so) above α and below δ corresponds with α^+CK being above C₁(C_n(0,α),α). We have not worked out the exact correspondence, but note that for a system above a generic ordinal, unlike well-foundness for L_κ1, well-foundedness for L_λ is "flawed", which appears to limit the degrees of C₁(..,α) that are below α^+CK. For the least Σ¹₁-reflecting α, α^+CK should be just C₁(0,C₁(0,α)).

For sufficiently closed b (b=κ_n=n in the above (with transfinite n)), C_b(0,b) might be the supremum of b-recursive well-orderings. And since C_i(0,b) for i≥b can in a sense effectively use parameters in L_b, the strength above b might increase quickly. If α<b is maximal such that L_b is correct about which Σ_α (with parameters) orderings are well-orderings, the next admissible appears to correspond to iterating C_b+1(0,..) approximately α times, with C_b+2(0,b) (if not lower) likely the next admissible for b=ω₁^L and for other admissible b that have uncountable cofinality in L_b^+CK+1.

Beyond C_i(a,b), diagonalization is qualitatively enhanced. Consider the extension using 4-variable C with C_i(a,b)=C(0,i,a,b), and let K=C(1,0,0,0). We have not ruled out that Σ_n+1 correct ordinals (about L_ω1^L) correspond to C(n,..,..,..), but a more likely hypothesis is to use C_K*n+d(a,b) for b<K and 0<d≤K. If e=C_K(a,b)<K, then e is a limit of e Σ₁-correct ordinals, and a indicates the degree of diagonalization. a<C₁(0,K) corresponds to recursive diagonalization that is not strengthened through Σ₁-correct ordinals, and incidentally, the proof ordinal of Δ¹₃-CA + TI is likely C₀(C₁(0,K),0). a=C_f(0,K) for f<e corresponds to about f strengthenings of what is recursive. f=K catches up to what is recursive around e, and f=K+2 might correspond to e being Σ₁-reflecting onto Σ₁-correct ordinals, which (for checking that we have the right strength) is a key milestone in the amount of reflection required.

REFERENCES

Arai, Toshiyasu (2015), "A simplified ordinal analysis of first-order reflection", arXiv:1506.05280.
Duchhardt, Christoph (2008), "Thinning Operators and Π₄-Reflection", thesis, http://d-nb.info/98.3428.3/34.
Freund, Anton (2019), "Π¹₁-comprehension as a well-ordering principle", Advances in Mathematics, vol 355, arXiv:1809.06759.
Freund, Anton, and Rathen, Michael (2021), "Well ordering principles for iterated Π¹₁-comprehension", arXiv:2112.08005.
Jech, Thomas (2006). Set Theory (3rd edition). Springer.
Kanamori, Akihiro (2008). The Higher Infinite: Large Cardinals in Set Theory from Their Beginnings (2nd edition). Springer.
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.
Rathjen, Michael (2014), "Omega-models and well-ordering principles", Foundational Adventures: Essays in Honor of Harvey M. Friedman (Neil Tennant (ed.)). (College Publications, London, 2014) 179-212.
Stegert, Jan-Carl (2010), "Ordinal proof theory of Kripke-Platek set theory augmented by strong reflection principles", thesis, https://nbn-resolving.org/urn:nbn:de:hbz:6-44449504436.
Taranovsky, Dmytro (2012), "Reflective Cardinals", arXiv:1203.2270.