Ordinal Systems, Part 2: One Inaccessible

Anton Setzer

Department of Mathematics, Uppsala University, P.O. Box 480, S-751 06 Uppsala,

                      Sweden, email: setzer@math.uu.se

Abstract. We develop an alternative approach to well-ordering proofs beyond the Bachmann-Howard ordinal using transfinite sequences of ordinal notations and use it in order to carry out well-ordering proofs for σ-ordinal systems. We extend the approach of ordinal systems as an alternative way of presenting ordinal notation systems started in [18] and develop ordinal systems, which have in the limit exactly the strength of Kripke-Platek set theory with one recursivly inaccessible. The upper bound is determined by giving well-ordering proofs, which use the technique of transfinite sequences. We derive from the new approach the traditional approach to well-ordering proofs using distinguished sets. The lower bound is determined by extending the concept of ordinal function generators in [18] to inaccessibles.

1 Introduction

This article is a followup of [18]. In that article we introduced ordinal systems as an alternative way of describing ordinal notation systems which usually make use of collapsing functions. In the simplest case of one single ordinal system, ordinals were always denoted by referring to smaller ones, a principle, which is valid in the case of systems built from extensions of the Veblen function. In order to get beyond the Bachmann Howard ordinal, we used several ordinal systems in parallel, such that the ordinal systems refer to each other in a controlled way. We described, how the combination of ordinal systems was used in order to generate in a well-ordered way the ordinal notation systems in question. This showed that they are well-ordered. We considered and analyzed ordinal systems up to the proof theoretic strength of ID_{σ}. In the current article we proceed with this research and present I-ordinal systems: ordinal systems which reach in the limit the strength of KPI, Kripke Platek set theory with one recursively inaccessible I (more precisely, the class of ordinals in KPI has the properties of one recursively inaccessible; proof theoretic studies for variations of Kripke Platek set theory can be found in [9], a formalization of KPI can be found in [9] or looked up as well in [4]). We will then determine their strength as that of KPI. This presentation should help to understand ordinal notation systems of this strength in a better way.

The content of the article is as follows: I-ordinal systems will be introduced in Section 3. In Sections 4 and 5 we will then show that I-ordinal systems are well-ordered and that elementary I-ordinal systems, i.e. I-ordinal systems, the properties of which can be verified in PRA, have order type less than KPI. We are going to present two well-ordering proofs. One, using a new technique, namely transfinite sequences of ordinal notations, and a second in the more traditional way, which uses distinguished sets and can be used for well-ordering proofs in constructive theories. In order to motivate the new technique of using sequences, we introduce it in Section 2 in the context of σ-ordinal systems. In the last section of this article (Section 6), we will extend the notion of ordinal function generators and define ordinal function generators corresponding to I-OS. We will see there that we reach the strength of I-OS. Therefore the strength of elementary I-ordinal systems is determined as being precisely the strength of KPI.

2 A variation of the usual well-ordering proof techniques

The usual technique in proof theory for carrying out well-ordering proofs is the technique of distinguished sets, introduced by Buchholz in [1]. In our previous article [18] some (but not the full power of it) was used and it seems to be still the only technique available for carrying out well-ordering proofs of strength beyond ID_{ω} in constructive theories. However, we believe that for theories which have substantially stronger strength it is not so easy to understand what is going on in it, and found it very difficult to teach it. We have now developed a variation of it, which we hope is slightly more intuitive. The disadvantage of it is that it can in the current form not be carried out in constructive theories. However this is no harm since from it in a second step we can derive the technique of distinguished sets. We hope our presentation motivates distinguished sets in a better way. Instead of defining the sets in an abstract way we are going to define by recursion on set theoretic ordinals a transfinite sequence of ordinal notations a_{α}. Distinguished sets will occur as initial segments of the set of notations generated in such a way. In order to show the well-foundedness of the resulting system, apart from some verifications, which can be essentially be carried out in primitive recursive arithmetic, and the existence of such a sequence, which is clear in the case of Kripke Platek set theory — the use of classical logic is crucial here —, we will need that, when iterated over all ordinals, the resulting sequence is complete, i.e. this sequence can not be extended. In order to prove the consistency of the theories in question we will need therefore essentially that the class of ordinals is big enough. One can use principles which claim that the class of ordinals fulfills the properties of some recursively large ordinal. Or one can claim instead that the set of ordinals should be unbounded in the sense that we cannot exhaust it by any recursive process, and that therefore such an ordinal must exist. The latter point of view provides an alternative argument for the consistency of the theory in question, alternative to the use of constructive theories, the consistency of which can be philosophically shown or at least justified. At the moment, the new argument is not as well philosophically developed as the other approach, but we hope to be able to investigate it in the near future. In this article, we only mention the possibility of such an approach. Once we have found such a sequence and carried out the well-ordering proof using it, we can now find the constructive version of the well-ordering proof using distinguished sets by formalizing abstractly the principles according to which the sets A_{α} := {a_{β} | a_{β} ↓ ∧β < α} are defined. We will apply this in section 4 to I-ordinal systems. In a first step we want to look at σ-ordinal systems in order to introduce the technique. In the case of σ-ordinal systems, the benefits will not be very big, most readers will certainly prefer the old technique. However for stronger systems this technique will motivate wellordering proofs in a better way.

We need a theory of the strength of ID_{σ} in which we have ordinals available. Kripke Platek set theory without Δ_{0}-collection, but extended by natural numbers and the existence of a well-ordering Σ (as new urelemente) of order type σ and for every a ∈ Σ an admissible such that these admissibles are ordered as the corresponding elements of Σ and the collection of predecessors of an a ∈ Σ is a set, which is an element of the ath admissible, should be the correct theory. (The exact formulation of such a theory is not important here since this Section mainly serves to introduce and motivate the new technique). In this section, (set-theoretic) ordinal refers to the set of ordinals below some of the admissibles which were additionally introduced in this theory. Before defining such sequences we make our life easier by extending the order <_{ξ} to a global order:

Definition 2.1. (a) T := ⋃_{ξ∈Σ} T_{ξ}, T_{<ξ} := ⋃_{μ<ξ} T_{μ}, T_{≤ξ} := ⋃_{μ≤ξ} T_{μ}.

(b) If a ∈ T_{ξ}, b ∈ T_{μ}, then a ≺ b :⇔ (ξ < μ ∨ (ξ = μ ∧ a ≺_{ξ} b)).

(c) If a ∈ T_{ξ}, then k(a) := ⋃_{μ∈Σ} k_{ξ,μ}(a).

(d) If A ⊆ T, a ∈ T, A ∩ a := {b ∈ A | b ≺ a}

It seems, as if we are back to the traditional way of ordinal notation systems, in which small ordinals (e.g. a ∈ T_{0}) are denoted by referring to bigger ones (e.g. b ∈ k(a) ∩ T_{1}, therefore a ≺ b). But the real picture to keep in mind should be that of several ordinal systems, which refer to each other in a controlled way, i.e. smaller ordinal systems refer to bigger ordinal systems restricted to smaller levels only. The global order will be helpful in order to reduce the amount of syntax. In the well-ordering proof we defined by recursion on ξ ∈ Σ sets M_{ξ}, Acc_{ξ} ⊆ T_{ξ} by:

M_{ξ} := T_{ξ} ↾_{μ<ξ} Acc_{ν},
Acc_{ξ} := Acc_{≺}(M_{ξ}).

We can now use transfinite sequences of ordinal notations in order to obtain the same sets. We proceed as follows: we consider in increasing order all elements of Σ. For each ξ ∈ Σ we select, as long as possible, successively the least element of T_{ξ} which has smaller components in the set of ordinals already selected before, but has not been selected itself. Once we cannot find any more such a minimal element, we select the next element of Σ. Once we have finished, the elements of T chosen will be ⋃_{ξ∈Σ} Acc_{ξ}. In order to formalize this idea, we first define for sets A ⊆ T M[A] := {a ∈ T | k(a) ∩ a ⊆ A} and M_{ξ}[A] := M[A] ∩ T_{ξ}. Now we define by recursion on γ elements a_{γ} ∈ T together with i_{γ} ∈ Σ, A_{γ} ⊂ T_{γ} as follows:

A_{γ} := {a_{β} | β < γ ∧ a_{β} ↓},
i_{γ} :≃ min_{<}{ξ ∈ Σ | min_{≺}(M_{ξ}[A_{γ}] \ A_{γ}) ↓},
a_{γ} :≃ min_{≺}(M_{i_{γ}} [A_{γ}] \ A_{γ}).

Convention 2.2. A simultaneous definition of sequences like a_{γ}, i_{γ} above should in the following be understood as follows: both i_{γ}, a_{γ} (and possibly other sequences) are defined by recursion on the (set theoretic) ordinals γ and can have either value as indicated (above in Σ and T, respectively) or a symbol for undefined. a ↓ means that a is not a symbol for undefined, a ↑ means that a is (a symbol for) undefined. Similarly, for a set A min_{<}(A) ↓ (min_{<}(A) ↑) means that a minimum of A with respect to < exists (does not exists). For two possibly objects of a set with an undefined element a ≃ b :⇔ (a ↓ ∨b ↓) → a = b. In the above definition i_{γ} is defined iff ∀β < α(i_{β} ↓ ∧a_{β} ↓) and a minimum as in the definition above exists. If i_{γ} is defined, it has as value the corresponding minimal element. The definition of a_{γ} is similar, but presupposes that i_{γ} is defined. Similar future definitions are to be understood in the same way.

Therefore we start to define a_{γ}, i_{γ}, as long as possible. If this is no longer the case, both get the value undefined. Note that this can be defined in the classical set theory used, in which we can “decide” whether i_{γ}, a_{γ} are defined. Because of this definition, this proof is non-constructive.

Lemma 2.3. (Admissibles are Π_{2}-reflecting) Assume ϕ_{0}(x), ϕ_{1}(x, y) are Σ-formulas.

(a) (Provable in Kripke Platek set theory without Δ_{0}-collection but with natural numbers.) If κ is an admissible ordinal, then from

∃α < κ . ϕ_{0}(α) and
∀α < κ.∃β < κ . ϕ_{1}(α, β)

follows the existence of some δ < κ such that

∃α < δ . ϕ_{0}(α) and
∀α < δ.∃β < δ . ϕ_{1}(α, β).

(b) In the presence of Δ_{0}-collection (for the universe of sets) (a) holds for the class of ordinals, i.e.

∃α . ϕ_{0}(α) and

∀α.∃β . ϕ_{1}(α, β)

implies the existence of some δ such that the conclusion of (a) holds.

(c) (a), (b) hold as well with ϕ_{0}, ϕ_{1} replaced by several Σ-formulas.

Proof. (a): Define α_{n} for n ∈ ω inductively by: α_{0} = α + 1, where α minimal such that ϕ_{0}(α) holds. n → n + 1: ∀β < α_{n}.∃γ < κ.ϕ_{1}(β, γ). By Σ-collection there exists ρ < κ such that ∀β < α_{n}.∃γ < ρ.ϕ_{1}(β, γ). Choose α_{n+1} = max{ρ, α_{n}} for the minimal such ρ. With δ := sup_{n∈ω} α_{n} < α follows now the assertion.

(b) follows similarly and (c) by coding several Σ-formulas into one.

Definition 2.4. (a) A is T_{ξ}-complete iff

(∀μ ≤ ξ.∀a ∈ M_{μ}[A](M_{μ}[A] ∩ a ⊆ A) → a ∈ A) .

(b) A is complete iff A is T_{ξ}-complete for all ξ ∈ Σ.

Remark 2.5. (a) (γ < γ′ ∧ i_{γ′} ↓) ⇒ i_{γ} ≤ i′_{γ}.

(b) (α < β ∧ i_{β} ↓ ∧i_{α} = i_{β}) ⇒ a_{α} ≺ a_{β}

(c) A_{β} are ≺-well-ordered.

(d) A_{β} is T_{ξ}-complete iff i_{β} ↑ or ξ ≤ i_{β}.

A_{β} is complete iff a_{β} ↑.

(e) If A_{β} is T_{ξ}-complete (complete) and β < γ, then A_{γ} is T_{ξ}-complete (complete).

Proof. (a): easy induction on γ′. (b): Induction on β. a_{β} ≠ a_{α}. Let ξ := i_{α} and assume we had a_{β} ≺ a_{α}. By (a) A_{β} ∩ T_{≺ξ} = A_{α} ∩ T_{≺ξ}. By a_{β} ≺ a_{α} it follows a_{β} ∈ M_{ξ}[A_{β}] \ M_{ξ}[A_{α}], there exists c ∈ k(a_{β}) ∩ T_{ξ} such that c ∈ A_{β} \ A_{α}, c = a_{γ} for some α < γ < β, a_{γ} ≺ a_{β} ≺ a_{α}, contradicting the IH. (c): By (a), (b). (d) Immediate. (e) By (a), (d).

The following Lemma will not be needed for the well-ordering proof. We state it in order to show that we have defined exactly the sets Acc_{ξ} from the original well-ordering proof.

Lemma 2.6. (a) If we define i′_{γ}, a′_{γ}, A′_{γ} by

A′_{γ} := {a′_{β} | β < γ ∧ a′_{β} ↓},
i′_{γ} :≃ min_{<}{ξ ∈ Σ | min_{≺}{a ∈ T_{ξ} \ A′_{γ} | k(a) ∩ T_{<ξ} ⊆ A′_{γ}} ↓},
a′_{γ} :≃ min_{≺}{a ∈ T_{i′_{γ}} \ A′_{i′_{γ}} | k(a) ∩ T_{<i′_{γ}} ⊆ A′_{γ}},

then i′_{γ} ≃ i_{γ}, a′_{γ} ≃ a_{γ} for all γ.

(b) If A_{γ} is T_{ξ}-complete, then A_{γ} = Acc_{ξ}, where Acc_{ξ} is defined as in [18].

Proof. (a) Induction on γ. By IH A′_{γ} = A_{γ}. Let for ξ ∈ Σ, B_{ξ} := {a ∈ T_{ξ}\A_{γ} | k(a)∩T_{<ξ} ⊆ A_{γ}}. We show min_{≺}B_{ξ} ≃ min_{≺}(M_{ξ}[A_{γ}]\A_{γ}). Assume c := min_{≺}B_{ξ} ↓. If d ∈ k(c) ∩ T_{ξ}, then k(d) ∩ T_{<ξ} ⊆ k(c) ∩ T_{<ξ} ⊆ A_{γ}, by minimality and d ≺ c therefore d ∈ A_{γ}. It follows c ∈ M_{ξ}[A_{γ}], and by M_{ξ}[A_{γ}] ⊆ B_{ξ}, c = min(M_{ξ}[A_{γ}] \ A_{γ}). On the other hand, if c = min(M_{ξ}[A_{γ}] \ A_{γ}), d ≺ c, d ∈ B_{ξ}, follows by induction on the length of e ∀e ∈ k(d) ∩ T_{ξ}.e ∈ A_{γ} (using f ∈ k(e) ∩ T_{ξ} ⇒ k(f) ∩ T_{<ξ} ⊆ k(e)), therefore d ∈ M_{ξ}[A_{γ}] \ A_{γ}, a contradiction, again c = minB_{ξ}. Now it follows i_{γ} = i′_{γ}, a_{γ} = a′_{γ}.

(b) Induction on ξ. By (a) it follows A_{γ} ∩ T_{ξ} ⊑ M_{ξ}, by Remark 2.5 (c) A_{γ} ∩ T_{ξ} is well-ordered, and by completeness and (a) it follows A_{γ} = Acc_{ξ}.

Lemma 2.7. Let τ_{ξ} be the ξ-th admissible ordinal. If α ≥ τ_{ξ}, then A_{α} is T_{ξ}- complete. Especially, the union of all A_{α} is complete.

Proof. Induction on ξ. By Remark 2.5 (e) it suffices to show the assertion for κ = τ_{ξ}. By IH A_{κ} is T_{μ}-complete (μ < ξ), therefore, if i_{κ} is defined, then ξ ≤ i_{κ}. Assume c ∈ M_{ξ}[A_{κ}], M_{ξ}[A_{κ}] ∩ c ⊆ A_{κ}. Then by the finiteness of k(c) there exists α < κ such that c ∈ M_{ξ}[A_{α}] and by Σ-collection relativized to L_{κ} it follows ∀α < κ.∃β < κ(M_{ξ}[A_{α}] ∩ c ⊆ A_{β}). Further ∀α < κ∃β < κ.α < β and ∃α < κ.α = 0. Application of Lemma 2.3 to the last three formulas, ∃α < κ.c ∈ M_{ξ}[A_{α}] and ∀ξ′ < ξ.τ_{ξ′} < κ yields that there exists δ < κ such that the above conditions follow relativized to δ, i.e. δ is a limit ordinal such that ∃α < δ.c ∈ M_{ξ}[A_{α}], ∀α < δ.∃β < δ(M_{ξ}[A_{α}] ∩ c ⊆ A_{β}) and ∀ξ′ < ξ.τ_{ξ′} < δ. It follows ξ ≤ i_{δ}, c ∈ M_{ξ}[A_{δ}] and (M_{ξ}[A_{δ}] ∩ c ⊆ A_{δ}), therefore c ∈ A_{δ} ⊆ A_{κ} or c ∉ A_{δ}, i_{δ} = ξ, c = a_{δ} ∈ A_{κ}.

Now we can substitute in the proof of Theorem 4.3 (a) of [18] with A := ⋃_{α∈Ord} A_{α} Acc_{μ} by A ∩ T_{μ} and M_{μ} by M_{μ}[A] and replace in the equation which verifies that C^{ν}(s) is definable in ID_{σ} “∀ξ < μ(k_{ν,ξ}(r) ⊆ Acc_{ξ})” by ∀ξ ≤ μ(k_{ν,ξ}(r) ⊆ Acc_{ξ})”, and show that σ-OS are well-ordered, provable in our variant of Kripke-Platek set theory.

3 Ordinal Systems for one inaccessible

We are going to develop now ordinal systems for one inaccessible, in short I-OS, which will have in the limit order type |KPI| = |(Δ_{2}^{1} − CA) + (BI)| = ψ(ϵ_{I+1}). The step from σ-OS to I-OS is easy: instead of having one fixed order Σ, this order will now be generated by a further ordinal system. Therefore we have OS-structures (T_{a}, ≺_{a}, ≺′_{a}, k_{a,a}, length_{a}) depending on a ∈ T_{I}, where T_{I} is the underlying set of terms of an OS-structure (T_{I}, ≺_{I}, ≺_{I}, ≺′_{I}, k_{I,I}, length_{I}), functions k_{i,j} : T_{i} →_{ω} T_{j}, for i, j ∈ J := T_{I} ∪ {I}, an ordered set (L, ≺) together with functions level_{i} : T_{i} → L and k̃_{i} : L →_{ω} T_{i} for i ∈ J. As we did with σ-OS above we will simplify the definitions by replacing the individual component functions k_{i,j} by only one function k : T →_{ω} T, where T := ⋃_{i∈J} T_{i}, such that for a ∈ T_{i}, k_{i,j}(a) = k(a) ∩ T_{j}; similarly we define only one function k̃ : L →_{ω} T, level : T → L and length : T → ω, each. Further we will introduce global orders ≺, ≺′ on T. The resulting structure can now be visualized as follows:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} i  j  k  l (T_{i},≺′_{i})  (T_{j},≺′_{j})  (T_{k},≺′_{k})  (T_{l},≺′_{l}) (T_{i},≺_{i})  (T_{j},≺_{j})  (T_{k},≺_{k})  (T_{l},≺_{l}) (T_{I},≺′)  (T_{I},≺)

The conditions are now almost the same as for σ-OS, except for the following two changes:

– If a ∈ T_{i}, i ∈ T_{I}, then k(i) ⊆ k(a). This guarantees that, if from ordinals generated before we can denote a, then we can already denote i. However, we can weaken this condition and will demand it only in case k_{i}(a) ≠ ∅ (since otherwise the information about i is already contained in the components of a).

– k_{j}(i) = ∅ for i ≺ j ∈ T_{I}. This guarantees that in the well-ordering proof using sequences, the sequence i_{γ} which corresponds to the sequence of i_{γ} in σ-ordinal systems is increasing, i.e. the elements of T_{I} are selected in increasing order.

Definition 3.1. (a) An Ordinal-System-structure of type I in short I-OS-structure is a 10-tuple

(T_{I}, (T_{i})_{i∈T_{I}}, (≺_{i})_{i∈T_{I}∪{I}}, (≺′_{i})_{i∈T_{I}∪{I}}, length, k, L, ≺_{L}, level, k̃)

such that, with

– J := T_{I} ∪ {I},

– T := ⋃_{i∈J} T_{i},

we have

– T_{I} and T_{i} (i ∈ T_{I}) are pairwise disjoint sets,

– ≺_{i}, ≺′_{i} are linear orders on T_{i} for i ∈ J,

– k : T →_{ω} T,

– length : T → ℕ,

– (L, ≺_{L}) is a linearly ordered set,

– level : T → L,

– k̃ : L →_{ω} T.

(b) For an I-OS-structure as above we define – k_{i}(a) := k(a) ∩ T_{i}; k̃_{i}(l) := k̃(l) ∩ T_{i} (i ∈ J, a ∈ T, l ∈ L);

– a binary relation ˜≺ on J defined for i, j ∈ J by

i˜≺j :⇔ ((i ∈ T_{I} ∧ j ∈ T_{I} ∧ i ≺_{I} j) ∨ (i ∈ T_{I} ∧ j = I)) ,

– a global order ≺ on T defined for i, j ∈ J, a ∈ T_{i}, b ∈ T_{j} by

a ≺ b ⇔ ((i = j ∧ a ≺_{i} b) ∨
(i ∈ T_{I} ∧ j ∈ T_{I} ∧ i ≺_{I} j) ∨
(i ∈ T_{I} ∧ j = I ∧ i ⪯_{I} b) ∨
(i = I ∧ j ∈ T_{I} ∧ a ≺_{I} j)).

– a ≺′ b :⇔ a ≺_{i} b for a, b ∈ T_{i}.

– If A ⊆ T, then k^{−1}(A) := {a ∈ T | k(a) ⊆ A}, k̃^{−1}(A) := {a ∈ L | k̃(a) ⊆ A}.

– If A ⊆ T, a ∈ T, then A ∩ a := {b ∈ A | b ≺ a}. (Note that as for σ-OS ≺ should be considered only as a technical simplification: the real intuition should be that several OS-structures are working in parallel; further note that on T_{i} (i ∈ J) ≺ coincides with ≺_{i}).

(c) An I-OS-structure as above is an I-times iterated Ordinal System in short I-OS, if for all i, j, l ∈ J, i′, j′ ∈ T_{I}, r, s ∈ T_{i}, r′, s′ ∈ T_{i′} the following holds: (I − OS 1) length[k(r)] < length(r); (I − OS 2) k_{i}(r) ≺ r; (I − OS 3) If r ≺ s, then r ⪯ k_{i}(s) ∨ r ≺′ s∨ level(r) ≺ level(s). (I − OS 4) If j ˜≺i, then k_{j} ∘ k_{i} ⊆ k_{j}. (I − OS 5) k̃(level(r)) ⊆ k(r) ∪ k̃[level[k_{i}(r)]]. (I − OS 6) If i′ ≺ j′, then level[k_{j′}(r′)] ≺ level(r′). (I − OS 7) If r ≺ s, then level(r) ⪯_{L} level(s). (I − OS 8) If k_{i′}(r′) = ∅, then k(i′) ⊆ k(r′). (I − OS 9) If i′ ⪯ j′, then k_{j′}(i′) = ∅. (I − OS 10) If A ⊆ T is ≺-well-ordered, then k^{−1}(A) is ≺′-well-ordered and

k̃^{−1}(A) is ≺_{L}-well-ordered.

(d) An I-OS as above is well-ordered if (T, ≺) is well-ordered, and its order type is that of (T_{a}, ≺_{a}), where a is the ≺-minimal element of T_{I} such that T_{a} ≠ ∅, (if no such a exists, the order type is 0). It is primitive recursive if the involved sets are primitive recursive subsets of the natural numbers (parameterized in T_{I}, i. e. t ∈ T_{u} is primitive recursive in t and u) all functions, relations (including ≺_{I}) are primitive recursive and all properties (including linearity of ≺_{I}, ≺′_{I}) except for (I − OS 10) can be shown in primitive recursive arithmetic. It is elementary if additionally the well-ordering condition follows in PRA in the sense of PRA-reducibility.

Remark 3.2. (I − OS 3), (I − OS 5) and (I − OS 8) could be replaced by the following conditions, which will be fulfilled in all the examples given in this article. We have chosen the weaker conditions above in order to be more general.

(I − OS 3′) If r ≺ s, then r ⪯ k_{i}(s) ∨ r ≺′ s. (I − OS 5′) k̃(level(r)) ⊆ k(r). (I − OS 8′) k(i′) ⊆ k(r′).

Remark 3.3. In an I-OS as above we have ∀a ∈ T_{I}.k(a) ≺ a.

4 Well-ordering proofs for I-OS using sequences

We are going to show Theorem 6.9 (a), (b): I-OS are well-ordered, and, if they are elementary, they have order type below the proof theoretic strength of KPI. We will show our assertion by giving a well-ordering proof for I-OS, which for elementary I-OS can be formalized in KPI. As mentioned in the introduction, we will carry out these proofs in two versions: In this section we will carry out a well-ordering proof using sequences. We regard this proof as more intuitive than the proof using distinguished sets, which is suitable for constructive theories and carried out in Section 5. The proof of the parts (a) and (b) of Theorem 6.9 will be almost identical. The latter one is achieved by carrying out the proof of (a) for elementary I-OS in KPI. The only difference between both proofs will be by choosing part (a) or (b) of the following assumption:

Assumption 4.1. In this and the next section assume an I-OS

O = (T_{I}, (T_{i})_{i∈J} , (≺_{i})_{i∈J} , (≺′_{i})_{i∈J} , length, k, L, ≺_{L}, level, k̃)

with the usual notations as above. Further assume one of the following:

(a) Our meta-theory is at least Kripke-Platek set theory with natural numbers and there exists an admissible ordinal κ_{0} such that ∀α < κ_{0}∃π < κ_{0}(α < π∧π is an admissible ordinal), where in the following admissible ordinal means “admissible ordinal > ω”. O ∈ L_{κ_{0}} and all conditions can be verified in our meta-theory, where condition (I − OS 10) should be provable for all sets A ∈ L_{κ}. Let in this case Ord := κ_{0} and Set := L_{κ_{0}}, and sets and ordinals range over Ord and Set. This condition is fulfilled if O is a set and we have as meta-theory ZFC.

(b) Our meta-theory is at least Kripke Platek set theory with natural numbers, ∀α∃κ.α < κ∧κ is an admissible ordinal, O is a set, all conditions of being an I-OS can be verified in our meta-theory, where condition (I − OS 10) should be provable for all classes A. Let in this case Ord := {α | α ordinal} and Set := {x | x = x}. This condition holds if we have KPI as meta-theory and O is elementary.

The well-ordering proof will be similar to the one given in Section 2. Instead of selecting the elements of Σ in increasing order, we will now select for each α the least element of T_{I} which has smaller components in the notations already defined before, but was not selected itself. For each such i we first select all elements of T_{i} as for σ-OS. Once we cannot find any more such an element, we select first i itself and then move on to the next i.

Definition 4.2. (a) M[A] := {a ∈ T | k(a) ∩ a ⊆ A}.

For i ∈ J M_{i}[A] := M[A] ∩ T_{i}.

(b) By recursion on the ordinals we define simultaneously i_{α} ∈ T_{I} and a_{α} ∈ T_{i_{α}} ∪ {i_{α}}. (Note Convention 2.2.)

A_{α} :≃ {a_{β} | β < α ∧ a_{β} ↓}
i_{α} :≃ min_{≺}(M_{I}[A_{α}] \ A_{α})
a_{α} :≃ \begin{cases}min_{≺}(M_{i_{α}}[A_{α}] \ A_{α}) & if such a minimum exists, \\ i_{α} & otherwise. \end{cases}

(c) W := {a_{α} | α ∈ Ord ∧ a_{α} ↓}.

W_{i} := W ∩ T_{i} (i ∈ J).

W_{I}^{+} := W_{I} ∪ {I}.

Remark 4.3. If A ⊆ M[A], a ∈ M_{i}[A], i ∈ T_{I}, then i ∈ M[A].

Proof. Induction on length(a). If k_{i}(a) = ∅, then k(i) ⊆ k(a) ∩ a and therefore the assertion follows. Otherwise c ∈ k_{i}(a) for some c, c ∈ A ⊆ M[A], by IH i ∈ M[A].

Lemma 4.4. (a) If α < β, i_{β} ↓, then i_{α} ⪯ i_{β}.

(b) If α < β, a_{β} ↓, then a_{α} ≺ a_{β}.

(c) A_{α} and W are ≺-well-ordered, i.e. we have the principle of transfinite induction over these sets and classes.

Proof. (a): Ind on β. Assume β according to the assumption. If i_{β} ≺ i_{α}, then i_{β} ∈ M[A_{β}]\M[A_{α}], there exists c ∈ k(i_{β})∩(A_{β} \A_{α}). Let c = a_{γ} with α ≤ γ < β. By IH i_{β} ≺ i_{α} ⪯ i_{γ}, c = i_{γ} or c ∈ T_{i_{γ}} contradicting (I − OS 2) and (I − OS 9). (b): If i_{α} ≺ i_{β}, this is clear. Otherwise i_{α} = i_{β}, i_{γ} = i_{α} for β ≤ γ ≤ α and the assertion follows similarly as in (a).

(c) by (b).

Definition 4.5. (a) i ∈ T_{I} can be reached by A iff i ∈ M_{I}[A] and M_{I}[A]∩i ⊆ A.

(b) If i ∈ T_{I}, then a ∈ T_{i} can be reached by A iff i can be reached by A, a ∈ M_{i}[A] and M_{i}[A] ∩ a ⊆ A (equivalently: iff (M_{i}[A] ∪ M_{I}[A]) ∩ a ⊆ A and a, i ∈ M_{i}[A]).

(c) A ⊆ T is T_{I}-complete (T_{I} ∩ i-complete) iff, whenever i ∈ T_{I} (i ∈ T_{I} ∩ i) can be reached by A, then i ∈ A.

(d) Assume i ∈ T_{I}. A ⊆ T is T_{i}-complete iff it is T_{I} ∩ i-complete and whenever a ∈ T_{i} can be reached by A then a ∈ A.

(e) A is complete iff it is T_{I}-complete and T_{i}-complete for every i ∈ T_{I}.

Lemma 4.6. (a) A_{α} is T_{I}-complete iff i_{α} ↑ (and therefore as well a_{α} ↑).

(b) If i ∈ T_{I}, then A_{α} is T_{I} ∩ i-complete iff i_{α} ↑ ∨i ⪯ i_{α}.

(c) If i ∈ T_{I}, then A_{α} is T_{i}-complete iff i_{α} ↑ ∨i ≺ i_{α} ∨ a_{α} = i.

(d) If A_{α} is T_{I}-complete (T_{I} ∩ i-complete, T_{i}-complete, complete) and α < β, then A_{β} is T_{I} ∩ i-complete (T_{I} ∩ i-complete, T_{i}-complete, complete).

(e) If κ is an admissible ordinal, O ∈ L_{κ}, i_{κ} ↓, then A_{κ} is T_{i_{κ}}-complete and therefore a_{κ} = i_{κ}.

(f) If i ∈ T_{I}, a ∈ W_{i}, then k(i) ⊆ W.

(g) W is complete.

Proof. (a), (b), (c): easy. (d): by (a) - (c) and Lemma 4.4 (a). (e): Let i := i_{κ}. By (b) A_{κ} is T_{I} ∩ i-complete. Assume b ∈ T_{i}, b can be reached by A_{κ}. Then

i ∈ M_{I}[A_{κ}] ∧ M_{I}[A_{κ}] ∩ i ⊆ A_{κ},
b ∈ M_{i}[A_{κ}] ∧ M_{i}[A_{κ}] ∩ b ⊆ A_{κ}.

Similarly as in Lemma 2.7 it follows that for some α < κ

i ∈ M_{I}[A_{α}] ∧ M_{I}[A_{α}] ∩ i ⊆ A_{α},
b ∈ M_{i}[A_{α}] ∧ M_{i}[A_{α}] ∩ b ⊆ A_{α},

i_{α} ⪯ i therefore i_{α} = i, b ∈ A_{α} ⊆ A_{κ} or b = a_{α} ∈ A_{κ}.

(f) Induction on length(a). If k_{i}(a) = ∅, then k(i) ⊆ k(a) ∩ a ⊆ W. Otherwise there exists c ∈ k_{i}(a) ⊆ W, and by IH follows the assertion.

(g) Assume i ∈ M_{I}[W] ∧ M_{I}[W] ∩ i ⊆ W. As in (e) there exists some α such that

i ∈ M_{I}[A_{α}] ∧ M_{I}[A_{α}] ∩ i ⊆ A_{α} .

It follows A_{α} is T_{I} ∩ i-complete. There exists α < κ ∈ Ord, κ an admissible ordinal. By (d) A_{κ} is T_{I} ∩ i_{κ}-complete, i_{κ} ↑ ∨i ⪯ i_{κ}. If i_{κ} ↑ ∨i ≺ i_{κ}, it follows i ∈ A_{κ} ⊆ W, otherwise i_{κ} = i and by (e) i = a_{κ} ∈ W. If i can be reached by W, then by the argument just given i = a_{α} for some α, A_{α} and therefore as well W are T_{i}-complete.

Lemma 4.7. (a) If i ∈ T_{I} and a ∈ W_{i}, then i ∈ M[W] and M[W] ∩ i ⊆ W.

(b) If a ∈ W_{i}, then a ∈ M[W] and M_{i}[W] ∩ a ⊆ W.

Proof. (a) a = a_{γ} for some γ. i = i_{γ} = min_{≺}(M_{I}[A_{γ}] \ A_{γ}), i ∈ M_{I}[A_{γ}] ⊆ M_{I}[W], and by Lemma 4.4 (a), (I−OS 2) and (I−OS 9) it follows M_{I}[W]∩i = M_{I}[A_{γ}]∩i ⊆ A_{γ} ⊆ W. (b) follows in a similar way.

Definition 4.8. (a) W̃:= k^{−1}(W).

(b) L̃ := k̃^{−1}(W).

(c) For M ⊆ T, M^{⪯l} := {a ∈ M | a ∈ T_{I} ∨ level(a) ⪯ l}.

Lemma 4.9. W̃ ∩ T_{I} ⊆ W.

Proof. Note W̃ = M[W]. We show ∀a ∈ W̃.a ∈ W by main induction on level(a) ∈ k̃^{−1}(W) (with respect to the well-ordering (!) ≺_{L} on it), side-induction on a ∈ W̃ (with respect to the well-ordering (!) ≺′ on it) and assume a according to the assertion. a ∈ M[W]. We show ∀c ∈ M_{I}[W] ∩ a.c ∈ W and assume c ∈ M_{I}[W] ∩ a. If level(c) ≺ level(a), by main IH c ∈ W. Otherwise, if c ≺′ a, then level(c) = level(a), by side-IH c ∈ W. Otherwise c ⪯ k(a) ⊆ W, c ∈ M_{I}[W] ∩ max(k(a)) ⊆ W. Now a can be reached by W and by the completeness of W it follows a ∈ W.

Proof of Theorem 6.9 (a), (b) using sequences. First note that (W̃, ≺) and (L̃, ≺_{L}) are well-ordered. We show by induction on l ∈ L̃

∀l ∈ L̃.(M[W])^{⪯l} ⊆ W

and assume l according to induction. We show

∀a ∈ W̃^{⪯l}.a ∈ W

by (side-)induction on (W̃, ≺′): Assume i ∈ J, a ∈ M_{i}[W] according to the induction. We define for j ∈ J, C^{j}(a) ⊆ T_{j} and C(a) ⊆ T:

C^{j}(a) := \begin{cases}W_{j} ∩ a & if j ˜≺i, \\ M_{j}[W] ∩ a & if j = i, \\ \{b ∈ T_{j} | (j ≠ I → level(b) ≺_{L} level(a))∧ ∀l ˜≺i(k_{l}(b) ⊆ W_{l} ∩ a)∧ k_{i}(b) ⊆ M_{i}[W] ∩ a∧ ∀l ∈ J (i˜≺l ˜≺j → level[k_{l}(b)] ≺_{L} level(a))\} & if i˜≺j. \end{cases}

C(a) := ⋃_{j∈J} C^{j}(a).

Note that for i˜≺j,

C^{j}(a) = {b ∈ T_{j} | (j ≠ I → level(b) ≺_{L} level(a)) ∧ ∀l ˜≺j.k_{l}(b) ⊆ C^{l}(a)} .

We prove

∀j ∈ J .i˜⪯j → k[C^{j}(a)] ⊆ C(a) ,  (1)

and assume i˜⪯j, b ∈ C^{j}(a) and show ∀c ∈ k(b).c ∈ C(a) by induction on length(c). Assume c ∈ T_{l}. If l ˜≺j, then by b ∈ C^{j}(a) it follows c ∈ C^{l}(a). If l = j = i, then c ∈ W_{i} ∩ a ⊆ M_{i}[W] ∩ a = C(a). Otherwise i˜⪯j ˜⪯l ≠ i. If l ≠ I, level(c) ⪯_{L} level(b) ⪯_{L} level(a) and one of the ⪯_{L} in this chain is actually ≺_{L}, so level(c) ≺_{L} level(a). In both cases l ≠ I and l = I it follows for all k ˜≺l that k_{k}(c) ⊆ k_{k}(b) and by IH k_{k}(c) ⊆ C(a), c ∈ C^{l}(a).

∀j ∈ J .i˜⪯j → ∀b ∈ C^{j}(a).k̃(level(b)) ⊆ C(a)  (2)

follows now by induction on length(b).

M_{I}[W] ∩ a ⊆ C(a) .  (3)

If a ∈ T_{I}, this follows by definition of C^{I}(a). Assume a ∈ T_{i}, i ∈ T_{I}. We show ∀c ∈ M_{I}[W] ∩ a.c ∈ C(a) by induction on length(c). By Remark 3.3 k_{I}(c) ⊆ W ⊆ M[W] and by side-side-IH k_{I}(c) ⊆ C(a). Further, if j ∈ T_{I}, d ∈ k_{j}(c), then j ≺ c ≺ i, k_{j}(c) ⊆ W_{j} ∩ a = C^{j}(a). It follows c ∈ C(a). We show by (side-side-)induction on length(b) simultaneously for all j

∀j ∈ J .∀b ∈ C^{j}(a).(b ∈ W ∧ (i˜⪯j → level(b) ∈ L̃))  (4)

and assume b according to induction, b ∈ C^{j}(a). If j ˜≺i, this is trivial. Otherwise we have k(b) ⊆ C(a) and by IH k(b) ⊆ W, b ∈ W̃. Further k̃(level(b)) ⊆ k(b) ∪ k̃[level[k_{j}(b)]] ⊆ W by IH, level(b) ∈ L̃. Proof of b ∈ W: Case i = j: b ≺ a, therefore b ⪯ k_{i}(a) or level(b) ≺ level(a) or b ≺′ a. If b ⪯ k_{i}(a), by k_{i}(a) ⊆ W and Lemma 4.7 (b) it follows b ∈ W. If level(b) ≺_{L} level(a), by main IH and level(b) ∈ L̃ it follows b ∈ W. Otherwise b ≺′ a, b ∈ W̃ and by side-IH b ∈ W. Case i ≺ j ≠ I: level(b) ≺ level(a) and as before b ∈ W. Case i ≺ j = I: b ∈ W̃, b ∈ W. By (3), (4), C^{i}(a) = M_{i}[W] ∩ a, a ∈ M[W], therefore i ∈ T_{I} → i ∈ M[W] and by the completeness of W it follows a ∈ W.

5 Well-ordering proofs using distinguished sets

In this section we are going to develop the technique for carrying out wellordering proofs using distinguished sets. This is the technique used for analyzing constructive theories and subsystems of analysis without ordinals. In the case of standard ordinal notation systems of the strength of |KPI| it has been for instance used by [8] for a well-ordering proof in Feferman’s theory T_{0} and in [17] for a well-ordering proof for Martin-Löf’s Type Theory (which is slightly stronger than |KPI|). It was developed by Buchholz (the first presentation of it can be found in [1]). A distinguished set is a set A which is built in the same way as the sets A_{γ} are defined. So A∩T_{I} must be constructed by successively selecting the least element in M_{I}[A] not selected before, i.e. A is the set of elements of Acc(M_{I}[A]) which are less than some a ∈ A. This can be formalized as A ∩ T_{I} = Acc(M_{I}[A])|A. (Acc(M) is the accessible part, i.e. largest well-ordered initial segment of the ordered set M). Further, A ∩ T_{i} is constructed in the same way and we get under the assumption that i can be reached, i.e. M_{I}[A] ∩ i ⊆ A, the condition A ∩ T_{i} = Acc(M_{i}[A])|A. We will need as well versions, where we relativize the set of ordinals needed in the definition of the accessible part and therefore get a Σ-definition of distinguished sets, which can be used in instances of Σ-collection.

Definition 5.1. (a) If A, B ⊆ T, A|B:= {a ∈ A | ∃b ∈ B.a ⪯ b}.

(b) If A ⊆ T, a ∈ T, then A|a:= A|{a}.

(c) Acc_{α}(A) := A_{α}, where a_{γ} together with A_{γ} are defined by recursion on γ as a_{γ} :≃ min_{≺}(A \ A_{γ}), A_{γ} := {a_{β} | β < γ ∧ a_{β} ↓}.

(d) Acc(A) := Acc_{κ}(A), where κ is the least admissible such that A ∈ L_{κ}. One easily verifies that Acc(A) is the largest well-ordered segment of A i.e. the least set M such that a ∈ M iff ∀b ∈ A(b ≺ a → b ∈ M).

(e) W_{I}[A] := Acc(M_{I}[A]). If i ∈ T_{I}, then W_{i}[A] := {a ∈ Acc(M_{i}[A]) | M_{I}[A] ∩ i ⊆ A}. W[A] := ⋃_{i∈J} W_{i}[A].

(f) W_{I}^{α}[A] := Acc_{α}(M_{I}[A]). If i ∈ T_{I}, then W_{i}^{α}[A] := {a ∈ Acc^{α}(M_{i}[A]) | M_{I}[A] ∩ i ⊆ A}. W^{α}[A] := ⋃_{i∈J} W_{i}^{α}[A].

(g) A ⊆ T is distinguished (written as Ag(A), where Ag stands for the original German word “ausgezeichnet” for “distinguished”) iff A = W[A]|A.

(h) Ag_{α}(A) :⇔ ∀a ∈ (W_{α+1}[A] \ W_{α}[A])(A ≺ a) ∧ A = W_{α}[A]|A.

(i) The class W is the union of all distinguished sets which are elements of Set. W^{A} is the union of all distinguished sets which are elements of A.

Remark 5.2. (a) If ∀a ∈ (W^{α+1}[A] \ W^{α}[A]).A ≺ a, then W^{α}[A]|A = W[A]|A.

(b) If A is distinguished, A ∈ L_{κ}, κ admissible, then there exists α ≺ κ such that ∀a ∈ (W^{α+1}[A] \ W^{α}[A]).A ≺ a.

(c) If A ∈ L_{κ}, κ admissible, then A is distinguished iff ∃α < κ.Ag_{α}(A) iff ∃α.Ag_{α}(A).

(d) If B is an admissible set, a ∈ B, ∀x ∈ a.∃y ∈ B.(Ag(y) ∧ ϕ(x, y)), ϕ(x, y) a Σ-formula, then there exists b ∈ B such that ∀x ∈ a.∃y ∈ b.(Ag(y)∧ϕ(x, y)). The same holds in case we have (b) of Assumption 4.1 with B replaced by the class of sets.

Proof. (a) It follows A ≺ a for all a ∈ W^{β}[A] \ W^{α}[A]) and all α ≺ β.

(b) ∀a ∈ A∃β < κ.a ∈ W^{β}[A]. By κ admissible and A ∈ L_{κ} there exists α < κ such that ∀a ∈ A.∃β < α.a ∈ W^{β}[A] and by A = W^{κ}[A]|A, ∀a ∈ (W^{α+1}[A] \ W^{α}[A]).A ≺ a. (c): By (a), (b). (d): Replace Ag(A) by the Σ-formula ∃α.Ag_{α}(A).

Lemma 5.3. If A is distinguished, then A is well-ordered.

Proof. Let B := {i ∈ T_{I} | i ∈ A ∨ T_{i} ∩ A ≠ ∅}. Assertion: ∀i ∈ B.B ∩ i ⊆ A. Proof: Assume j ≺ i ∈ B, j ∈ B and show j ∈ A. If by the definition of j ∈ B we have j ∈ A, we are done. Otherwise there exists some c ∈ T_{j} ∩ A. c ∈ M[A], j ∈ M[A], i ∈ W[A] or for some a ∈ T_{i}, a ∈ W[A], and with b = i or b = a, j ∈ M_{I}[A] ∩ b ⊆ A. B is well-ordered: Assume ∀y ∈ B.(∀z ∈ B ∩ y.ϕ(z)) → ϕ(y), y ∈ B. Then B ∩ y = A ∩ T_{I} ∩ y, which is well-ordered, therefore ∀z ∈ B ∩ y.ϕ(z), ϕ(y). Define now f : A ↪ {<i, a> | i ∈ B, a ∈ (A ∩ T_{i}) ∪ {∞}} =: C. T_{I} ∋ a ⟼ <a, ∞> and if i ∈ T_{I}, T_{i} ∋ a ⟼ <i, a>. If we take as order on (A ∩ T_{i}) ∪ {∞} the order (A∩T_{i}, ≺) ◯ ≺ {∞}, then C with the lexicographic order is well-ordered. f is order-preserving, therefore A is well-ordered.

Lemma 5.4. (a) Assume sets A, B, Ag(A), Ag(B), a ∈ A, a ⪯ B. then a ∈ B.

(b) If B is a set, ∀X ∈ B(X ⊆ T ∧ Ag(X)), then Ag(⋃ B).

(c) A set A is distinguished iff A is an initial segment of W, i.e. A = W|A.

(d) W is well-ordered.

Proof. (a): We show ∀a ∈ A.(a ⪯ B → A|a = B|a) by induction on a and assume a according to induction. We show ∀b ∈ B(b ≺ a → A|b = B|b) by induction on b and assume b according to induction. By main and side-IH it follows A∩b = B∩b, b ∈ W[B]|b = W[B ∩ b]|b = W[A ∩ b]|b = W[A]|b = A|b. Therefore the sideinduction is complete, together with main IH it follows A ∩ a = B ∩ a and the main induction step follows as the side induction step.

(b) If a ⪯ ⋃ B, a ⪯ C for some C ∈ B, by (a) ⋃ B|a = C|a = W[C]|a = W[⋃ B]|a, therefore ⋃ B = W[⋃ B]|(⋃ B).

(c) If A is distinguished, then A ⊆ W and if a ∈ W|A, a ∈ C for some distinguished set C, by (a) C|a = A|a, a ∈ A. Therefore W|A = A. If W|A = A, then ∀x ∈ A.∃C(Ag(C) ∧ x ∈ C), By Remark 5.2 (d) there exists D such that ∀x ∈ A.∃C ∈ D(Ag(C)∧x ∈ C). Let D := ⋃{C|x | C ∈ D∧Ag(C)∧x ∈ C ∩A}. Then D is distinguished, A ⊆ D, D ⊆ A because A is an initial segment of W, A = D.

(d) Assume ∀x ∈ W.(∀y ∈ W(y ≺ x → ϕ(y)) → ϕ(x)), a ∈ W. Then a ∈ A for some distinguished set A, A is an initial segment of W, therefore ∀x ∈ A.(∀y ∈ A(y ≺ x → ϕ(y)) → ϕ(x)), ∀x ∈ A.ϕ(x), ϕ(a).

Lemma 5.5. (a) W^{A} is distinguished.

(b) If A is distinguished, a ∈ T_{i}, i ∈ T_{I}, a can be reached by A, then (A∩a)∪{a} is distinguished.

(c) If A is distinguished, i ∈ T_{I}, i can be reached by A and A is T_{i}-complete, then (A ∩ i) ∪ {i} is distinguished.

Proof. (a) By Lemma 5.4 (b).

(b) Let A′ := (A ∩ a) ∪ {a}. We have W[A′] ∩ a = A′ ∩ a: If b ∈ W[A′] ∩ a, in case b ∈ T_{i}, b ∈ M_{i}[A′] ∩ a = M_{i}[A] ∩ a ⊆ A ∩ a ⊆ A′, in case b ∈ T_{I} again b ∈ A′, and in case b ∈ T_{j}, j ≠ i, I, then j ∈ M_{I}[A] ∩ a ⊆ A ∩ a and by A distinguished and b ∈ W[A] ∩ j, b ∈ A ∩ a ⊆ A′. Further A′ ∩ a = A ∩ a ⊆ W[A] ∩ a = W[A′] ∩ a. a ∈ W[A′], a ∈ A′, W[A′]|A′ = W[A′]|a = A′.

(c) Let A′ := (A∩i)∪{i}. As in (b) it follows W_{I}[A′]|A′ = A′, W_{j}[A′]|A′ = A′ for j ∈ T_{I} \ {i}. Further by the T_{i}-completeness of A W_{i}[A′] = W_{i}[A] ⊆ A ∩ i ⊆ A′ therefore W_{i}[A′]|A′ = A′, A′ is distinguished.

Lemma 5.6. If A, B are distinguished sets, A ⊆ B, a ∈ T, a can be reached by A, then a can be reached by B as well.

Proof. Case a = i ∈ T_{I}: Let C := (T_{I} ∩i)∪⋃_{j∈T_{I}∩i} T_{J}. We show A∩C = B ∩C: “⊆” follows by A ⊆ B. “⊇”: We show ∀b ∈ B ∩ C.b ∈ A by induction on b. Subcase b ∈ T_{I}: b ∈ M[B]|b = M[B ∩ b]|b = M[A ∩ b]|b ⊆ M[A] ∩ a ⊆ A. Subcase b ∈ T_{j}, j ∈ T_{I} ∩ C: b ∈ M[B], therefore j ∈ M[B] ∩ C, and as before j ∈ A, b ≺ j ∈ A, b ∈ B and by Lemma 5.4 (a) it follows b ∈ A. Now i ∈ M[A] ⊆ M[B], and M_{I}[B] ∩ i = M_{I}[B ∩ C] ∩ i = M_{I}[A ∩ C] ∩ i ⊆ M[A] ∩ i ⊆ A ⊆ B. Case a ∈ T_{i}, i ∈ T_{I}: We show A ∩ a = B ∩ a. “⊆” is clear. “⊇”: We show ∀b ∈ B ∩ a.b ∈ A by induction on b. If b ∈ T_{I} or b ∈ T_{j}, j ∈ T_{j}, j ≠ i, then the assertion follows by the case a ∈ T_{I} and since i can be reached by A. If b ∈ T_{i}, follows the assertion as in the case a ∈ T_{I}, b ∈ T_{I}. As before follows now the assertion.

Lemma 5.7. (a) If A is an admissible set, i can be reached by W^{A}, then W^{A}

is T_{i}-complete.

(b) W is complete.

Proof. (a) Assume b ∈ T_{i} can be reached by W^{A}. Show b ∈ W^{A}. i and b can be reached, i.e.

i ∈ M_{I}[W^{A}] ∧ M_{I}[W^{A}] ∩ i ⊆ W^{A}
b ∈ M_{i}[W^{A}] ∧ M_{i}[W^{A}] ∩ b ⊆ W^{A}

By k(i)∪k(b) finite, closure of distinguished sets under union and the assumption there exists B_{0} distinguished, B_{0} ∈ A such that i, b ∈ M[B_{0}]. Further we can, using Remark 5.2 (d), inductively define distinguished sets B_{n+1} ∈ A (n ∈ ℕ) such that B_{n} ⊆ B_{n+1}, M_{I}[B_{n}]∩i ⊆ B_{n+1}, M_{i}[B_{n}]∩b ⊆ B_{n+1}. Let B := ⋃_{n∈ω} B_{n}. B is distinguished, B ∈ A,

i ∈ M_{I}[B] ∧ M_{I}[B] ∩ i ⊆ B
b ∈ M_{i}[B] ∧ M_{i}[B] ∩ b ⊆ B

By Lemma 5.5 (b) it follows that (B ∩ b) ∪ {b} is distinguished and b ∈ W_{A}.

(b) W is T_{I}-complete: Assume i can be reached by W. As in (a) it follows that i can be reached by some distinguished set B. Let A be an admissible set such that B ∈ A. Then B ⊆ W_{A}, by Lemma 5.6 i can be reached by W_{A}, by (a) W_{A} is T_{i}-complete and by Lemma 5.5(c) it follows (W_{A} ∩ i) ∪ {i} is distinguished, i ∈ W. If i ∈ T_{I}, i can be reached by W, then as in (a) it follows that W is T_{i}-complete, and the assertion follows.

Lemma 5.8. (a) If i ∈ T_{I} and a ∈ W_{i}, then i ∈ M[W] and M[W] ∩ i ⊆ W.

(b) If a ∈ W_{i}, then a ∈ M[W] and M_{i}[W] ∩ a ⊆ W.

Proof. Trivial

Proof of Theorem 6.9 (a), (b) using distinguished sets: As before, using W as defined in this section.

6 I-Ordinal Function Generators

We are going to show that the bound derived before is sharp, i.e. the supremum of the order types of elementary I-OS is |KPI|. As for the systems considered in [18] we will introduce I-ordinal function generators (I-OFGs), which provide a more general framework for defining I-OS. Using these we will define directly a sequence of OS, which could be regarded as “the standard I-OS”, in which we use essentially the n-times nested Schütte-Klammersymbole plus Cantor normal form, and which exhaust, although we will not prove that, the strength of |KPI|. We will then interpret directly the system used in [4] as an OFG and this will show the desired lower bound. Note that the use of ordinals is not really necessary in order to develop the ordinal systems, it only simplifies the description of the ordinal systems slightly, and makes the relationship with the more traditional approach to ordinal notation systems more precise.

Definition 6.1. (a) An I-ordinal function generator, in short I-OFG is a qua-

druple

O := (C, L, A, k̃′)

such that

– C is a set of ordinals,

– L = (L′, ≺_{L′}) is a well-ordering,

– A = (Arg_{κ}, ≺′_{κ}, k′_{κ}, l′_{κ}, level′_{κ})_{κ∈C∪{I}} (I a special symbol),

– k̃′ : L′ →_{ω} Ord,

– for κ ∈ C ∪ {I} we have • (Arg_{κ}, ≺′_{κ}) is a well-ordering,

• k′_{κ}, l′_{κ} : Arg_{κ} →_{ω} Ord,

• level′_{κ} : Arg_{κ} → L′,

• ∀a ∈ Arg_{κ}.l′_{κ}(a) ⊆ k′_{κ}(a),

• ∀a, b ∈ Arg_{κ}(a ≺′_{κ} b → level′_{κ}(a) ⪯_{L′} level′_{κ}(b)),

• ∀a ∈ Arg_{κ}.k̃′[level′_{κ}(a)] ⊆ k′_{κ}(a),

– Arg_{κ} (κ ∈ C ∪ {I}) are pairwise disjoint, We assume in the following that L′ and A_{κ} are disjoint and omit therefore the index κ in k′, l′, ≺′, level′ and the index L′ in ≺_{L′}. Further let κ, μ, ν be, unless mentioned differently, elements of I := C ∪ {I}, and let O always be as above.

(b) For κ ∈ C κ^{−} := ⋃_{π∈C∩κ} π and O_{κ} := κ \ (κ^{−} + 1).

I^{−} := 0, O_{I} := C. Define the relation ˜≺ on I by κ˜≺μ ⇔ (κ, μ ∈ C ∧ κ < μ) ∨ (κ ∈ C ∧ μ = I). Let Λ be minimal such that C < Λ. (In order to avoid the existence of large cardinals, one can assume that C is a class instead of a set and treat Λ as a symbol for undefined). Arg := ⋃_{κ∈I} Arg_{κ}.

(c) An I-OFG is cardinality based iff

– C is a set of cardinals which has as order type a regular cardinal π such that ω < π ∧ ∀κ ∈ C.κ < π (if we have treated Λ as undefined above, we demand that C is a proper class),

– for all κ such that κ is not a regular cardinal > ω we have Arg_{κ} = ∅,

– for all B ⊆ Ord countable k′_{κ}^{−1}(B) is countable,

– for a ∈ Arg_{κ}, l′_{κ}(a) ⊆ k′_{κ}(a) ∩ O_{κ}. In this case we define for a ∈ Arg_{κ}, k′_{κ,ν}(a) := k′_{κ}(a) ∩ O_{ν}.

(d) If O as above is a cardinality based I-OFG, we define simultaneously for all κ ∈ I for a ∈ Arg_{κ} by recursion on level′_{κ}(a) ∈ L′, side-recursion on (Arg_{κ}, ≺′_{κ}), eval_{κ}(a) ∈ Ord, subsets C_{κ}(a), C_{κ}^{n}(a) ⊆ Ord (n ∈ ω) and, whether NF_{κ}(a) holds, by: Case κ ∈ C:

– C_{κ}^{0}(a) := (κ^{−} + 1) ∪ (⋃(k′_{κ}(a) ∩ O_{κ})) ∪ l′_{κ}(a),

– C_{κ}^{l+1}(a) := C_{κ}^{l}(a)∪

{eval_{ν}(b) | ν = I∨(ν = eval_{I}(c) ∈ C_{κ}^{l}(a)∧NF(c)∧c ∈ Arg_{I})∧

κ˜⪯ν ∧ b ∈ Arg_{ν}∧
((ν = κ ∧ b ≺′ a) ∨ level′(b) ≺_{L′} level′(a))∧
k′(b) ⊆ C_{κ}^{l}(a) ∧ NF_{ν}(b)},

– eval_{κ}(a) := min({α | α ∉ C_{κ}(a)} ∪ {κ}). Case κ = I:

– C_{I}^{0}(a) := (⋃(k′_{I}(a) ∩ O_{I})) ∪ l′_{I}(a),

– C_{I}^{l+1}(a) := C_{I}^{l}(a)∪

⋃{eval_{I}(b) + 1 | b ∈ Arg_{I} ∧ b ≺′ a∧

∧k′(b) ⊆ C_{I}^{l}(a) ∧ NF_{I}(b)},

– eval_{I}(a) := min({α ∈ C | α ∉ C_{κ}(a)} ∪ {Λ}). In both cases

– C_{κ}(a) := ⋃_{n∈ω} C_{κ}^{n}(a),

– NF_{κ}(a) :⇔ k′(a) ⊆ C_{κ}(a).

(e) eval(a) := eval_{κ}(a) for a ∈ Arg_{κ}, κ ∈ I. NF_{κ} := {a ∈ Arg_{κ} | NF_{κ}(b)}, NF := ⋃_{κ∈I} NF_{κ}. For a, b ∈ Arg a ≺ b :⇔ eval(a) < eval(b).

(f) Let O be a cardinality based I-OFG. We define T ⊆ NF inductively by: If κ = I ∨ (c ∈ T ∩ Arg_{I} ∧ κ = eval(c)), b ∈ NF_{κ}, k′(b) ⊆ eval[T], then b ∈ T. T_{I} := T ∩ Arg_{I}. T_{a} := T ∩ Arg_{eval_{I}(a)} for a ∈ T_{I}. Arg[T] := {a ∈ Arg | k′(a) ⊆ eval[T]}, Arg_{κ}[T] := Arg[T] ∩ Arg_{κ}. Note T ⊆ Arg[T]. Assuming that eval ↾ NF is injective and n ⊆ eval(T_{I}), which will be shown below, we define k^{0}, k^{1}, k : Arg[T] →_{ω} T, length : Arg[T] → ℕ, level : Arg[T] → L′ simultaneously by induction on a ∈ Arg[T] as follows: Assume a ∈ Arg_{κ}[T].

– κ ∈ C ⇒ k^{0}(a) := (eval^{−1}(k′(a)) ∩ T) ∪ k(eval^{−1}(κ)).

– κ = I ⇒ k^{0}(a) := eval^{−1}[k′(a)] ∩ T.

– k^{1}(a) := k^{0}(a) ∪ {d ∈ k(c) | c ∈ k^{0}(a) ∧ d ≺ c}.

– k(a) := k^{1}(a) ∪ k[k^{1}(a) ∩ Arg_{κ}].

– length(a) := max(length[k′(a)] ∪ {−1}) + 1.

– level(a) := max({level′(a)} ∪ level[k_{κ,κ}(a)]).

(g) J := T_{I} ∪ {I}. In the following let always k, l ∈ J. Let ≺_{k}, ≺′_{k} be the restriction of ≺, ≺′ to T_{k}. l(a) := eval^{−1}(l′(a)). k_{k}(a) := k(a) ∩ T_{k}, l_{k}(a) := l(a) ∩ T_{k} (k ∈ J). C′_{I}(a) := eval^{−1}(C_{I}(a)), and for k ∈ T_{I}, C′_{k}(a) := eval^{−1}(C_{eval(k)}(a)). L := k̃^{−1}(eval[T]). ≺_{L} be the restriction of ≺_{L′} to L. Define k̃ : L →_{ω} T, k̃(a) := eval^{−1}(k̃′(a)) ∩ T. If eval(k)^{−} exists, k^{−} := eval^{−1}(eval(k)^{−}).

Lemma 6.2. Let O be a cardinality based I-OFG.

(a) C_{κ}(a) is the least set M such that C_{κ}^{0}(a) ⊆ M and such that, if ν = I ∨ (ν = eval_{I}(c) ∈ C_{κ}^{l}(a) ∧ NF(c) ∧ c ∈ Arg_{I}), κ˜⪯ν, b ∈ Arg_{ν}, NF_{ν}(b), k′(b) ⊆ M, (ν = κ ∧ b ≺′ a) ∨ level′(b) ≺ level′(a), then eval_{ν}(b) ∈ M.

(b) If κ ∈ C, a ∈ Arg_{κ}, then C_{κ}(a) ∩ O_{κ} is an initial segment of O_{κ}. Especially eval_{κ}(a) = C_{κ}(a) ∩ κ. If a ∈ Arg_{I}, then C_{I}(a) is an initial segment of Ord.

(c) If a ∈ Arg_{κ}, then eval_{κ}(a) ∈ O_{κ} (κ ∈ I).

(d) If a, b ∈ NF_{κ}, then eval(a) < eval(b) ⇔ (a ≺′ b∧k′_{κ,κ}(a) < eval(b))∨eval(a) ≤ k′_{κ,κ}(b). Especially eval ↾ NF_{κ} is injective and therefore k, k^{0}, k^{1}, length and level are well-defined.

(e) F := (T_{I}, (T_{k})_{k∈T_{I}}, (≺_{k})_{k∈J} , (≺′_{k})_{k∈J} , length, k, L, ≺_{L}, level, k̃) is an I-OS-structure.

(f) In F, the relation ≺ derived from F being an I-OS-structure coincides with the original relation ≺.

Proof. (a) follows, since k′(a) is finite. (b): Main induction on level(a), ≺′-side induction on a. Assume the assertion for level(b) ≺ level(a) or b ≺′ a. We show ∀α ∈ C_{κ}^{n}(a) ∩ κ.α ⊆ C_{κ}(a) by side-side-induction on n: n = 0: clear, since l′(a) ⊆ k′_{κ,κ}(a). n → n + 1: Case κ = I: clear. Otherwise: If α ∈ (C_{κ}^{n+1}(a) \ C_{κ}^{n}(a)) ∩ O_{κ}, then α = eval_{κ}(b) with k′(b) ⊆ C_{κ}^{n}(a) and b ≺′ a, by side-side-IH and, since l′(b) ⊆ k′(b), ⋃(k′(b)∩O_{κ})∪l′(b) ⊆ C_{κ}(a), and by an immediate induction C_{κ}^{l}(b) ⊆ C_{κ}(a) for all l ∈ ω, C_{κ}(b) ⊆ C_{κ}(a), therefore α = min{γ | γ ∉ C_{κ}(b)} ⊆ C_{κ}(a).

(c) κ ≠ I. By an induction and the regularity of κ it follows that the cardinality of C_{κ}^{n}(a) and therefore as well that of C_{κ}(a) is < κ. We conclude that there exists an α < κ such that α ∉ C_{κ}(a). κ = I: Similarly it follows that there the cardinality of C_{I}(a) is < Λ. Therefore there exists α < Λ such that α ∉ C_{I}(a). For some α < π ∈ C it follows π ∉ C_{I}(a) ∩ C.

(d) “⇐” If a ≺′ b, k′_{κ,κ}(a) < eval(b), NF(a), it follows easily k′(a) ⊆ C_{κ}(a) ⊆ C_{κ}(b), eval(a) ∈ C_{κ}(b) ∩ κ = eval(b). If eval(a) ≤ k′_{κ,κ}(b), the assertion follows by k′_{κ,κ}(b) < eval(b). “⇒” If the right side is false, the right side holds for b ≺ a or a = b, so the left side is false.

(e) Trivial. (f) Easy.

Convention 6.3. In the following we will use all the definitions introduced for general I-OS-structures for the I-OS-structure of Lemma 6.2 (e).

Lemma 6.4. Assume k ∈ J, a ∈ T_{k}.

(a) b ∈ k(a) ⇒ k(b) ∩ b ⊆ k(a).

(b) b ∈ k_{k}(a) ⇒ k(b) ⊆ k(a).

(c) k = I ⇒ k(a) ≺ a.

(d) (k ∈ T_{I} ∧ b ∈ C′_{k}(a) \ (k^{−} ∪ {k^{−}})) ⇒ k(b) ⊆ C′_{k}(a).

(e) (k ∈ J ∧ a ∈ T_{k}) ⇒ k(a) ⊆ C′_{k}(a).

(f) If l ∈ T_{I}, k ˜≺l, b ∈ T_{l} ∩ C′_{k}(a), then level(b) ≺ level(a).

(g) length[k(a)] < length(a).

(h) k_{k}(a) ≺ a.

(i) (b ∈ T_{k} ∧ a ≺ b) ⇒ (a ≺′ b ∨ a ⪯ k_{k}(b)).

(j) If k, l ∈ J, l ˜≺k, then k_{l}[k_{k}(a)] ⊆ k(a).

(k) k̃(level(a)) ⊆ k(a).

(l) k ˜≺l ∈ T_{I} ⇒ level[k_{l}(a)] ≺ level(a).

(m) (a, b ∈ T_{k} ∧ a ≺ b) ⇒ level(a) ⪯ level(b).

(n) (k ∈ T_{I} ∧ a ∈ T_{k}) ⇒ k(k) ⊆ k(a).

(o) (k, l ∈ T_{I} ∧ k ≺ l) ⇒ k_{l}(k) = ∅.

(p) F is an I-OS. We call any I-OS isomorphic to F an I-OS based on O.

Proof. (a), (b): Induction on length(b). (c): Induction on length(a). k^{1}(a) ⪯ k^{0}(a) ⊆ C′_{I}(a), therefore k^{1}(a) ⊆ C′_{I}(a). By IH k[k^{1}(a) ∩ Arg_{κ}] ≺ k^{1}(a) ≺ a.

(d) Induction on length(b): k^{0}(b) ⊆ C′_{k}(a) and by IH it follows the assertion.

(e) In case k = I this follows by k(a) ≺ a and otherwise it follows similarly as (d), but using (d) instead of the IH.

(f) Induction on length(b). By (c), (d), k_{l}(b) ⊆ C_{k}(a) and by IH therefore level[k_{l}(b)] ≺ level(a). Further level′(b) ≺ level′(a) ⪯ level(a), and therefore level(b) ≺ level(a).

(g) Trivial. (h) By k(a) ⊆ C′_{k}(a). (i) Lemma 6.2 (d).

(j) If l ≺ k ∈ T_{I}, b ∈ k_{k}(a), then k_{l}(b) ⊆ k(b) ∩ b ⊆ k(a) by (a). If l ∈ T_{I}, k = I, b ∈ k_{k}(a), then by (c) k(b) ≺ b, k(b) = k(b) ∩ b ⊆ k(a).

(k) Note first that for all a k̃(level′(a)) ⊆ k(a). We show by induction on length(a) the assertion: k̃(level(a)) ⊆ k̃(level′(a)) ∪ k̃[level[k_{k}(a)]] ⊆ k(a) ∪ k[k_{k}(a)] ⊆ k(a). (l): By (c), (e), (f).

(m) Induction on length(a) + length(b). If a ⪯ k_{k}(b), then by IH level(a) ⪯ level[k_{k}(b)] ⪯ level(b). Otherwise a ≺′ b, level′(a) ⪯ level′(b) ⪯ level(b). Further by IH level[k_{k}(a)] ⪯ level(b) and therefore level(a) ⪯ level(b).

(n) Trivial. (o) By (d). (p) By the above.

Definition 6.5. (a) Ω_{0} := 0, Ω_{α} := ℵ_{α} for α ≠ 0.

(b) Let I be the least strongly inaccessible cardinal. (One can easily replace this by demanding that the class of ordinals has the properties of a strongly inaccessible cardinal).

(c) Define 0_{k} ∈ S_{k} by 0_{0} := 0, 0_{k+1} := ( ) (the empty Klammersymbol), where

S_{k} is as in Example 2.7. (i) of [18].

Example 6.6. (a) Let l ∈ ω, l > 0 be fixed. We define an OFG as follows: – C := {Ω_{α} | 0 < α < I}, (where Ω_{α} := ℵ_{α} for α > 0),

(Arg_{Ω_{α}}, ≺′_{Ω_{α}}) := ∅ if α is not a successor ordinal,

(Arg′_{Ω_{α+1}}, ≺′′_{Ω_{α+1}}) := \begin{cases}CNF_{Ω_{1}}([0, Ω_{1}[,]0, ω[), & if α = 0, \\ CNF_{Ω_{α+1}}([0, Ω_{α+1}[,]0, Ω_{α}[)\ \\ (CNF_{Ω_{α+1}}(\{0\},]0, Ω_{α}[)∪ \\ \{CNF_{Ω_{α+1}}(1, 1)\}) & otherwise, \end{cases}

(Arg_{Ω_{α+1}}, ≺′_{Ω_{α+1}}) := (Arg′_{Ω_{α+1}}, ≺′′_{Ω_{α+1}}) ◯ ≺ ψ_{Ω_{α+1}}(S_{l}),

where S_{l} is defined as in Example 2.7. (i) of [18], but restricted to ordinals < I.

– (Arg′_{I}, ≺′_{I}) := Ω_{[0,I[} ◯ ≺ ψ_{I}(S_{l}).

– k′_{Ω_{α+1}}(a), l′_{Ω_{α+1}} are defined as k_{i}, l_{i} in Example 3.7. (b) of [18], for α = 0 as i = 0 and for α > 0 as i > 0, l′_{I}(Ω_{1}) := k′_{I}(Ω_{1}) := ∅, for α > 0, k′_{I}(Ω_{α}) := {α}, l′_{I}(Ω_{α}) := ∅, k′_{I}(ψ_{I}(A)) := k_{0}^{l}(A), where k_{0}^{l} is as in Example 2.7. (i) of [18], l′_{I}(ψ_{I}(A)) := ∅.

– (L′, ≺_{L′}) := S_{l} (with its order).

– level_{Ω_{α+1}}(CNF′_{Ω_{α+1}}(a⃗)) := 0_{l}, level_{Ω_{α+1}}(ψ_{Ω_{α+1}}(A)) := A, level_{I}(Ω_{α}) := 0_{l}, level_{I}(ψ_{I}(A)) := A.

– k̃(A) := k_{0}^{l}(A). Then one easily sees that the above definitions yield a cardinality based I-OFG (κ_{0} = I). It follows eval_{I}(Ω_{α}) = Ω_{α} (α > 0), eval_{Ω_{1}}(CNF_{Ω_{1}}(α_{1}, m_{1}, …, α_{n}, m_{n})) = ω^{α_{1}}m_{1} + ⋯ + ω^{α_{n}}m_{n}, eval_{Ω_{α+1}}(CNF_{Ω_{α+1}}(α_{1}, β_{1}, …, α_{n}, β_{n})) = Ω_{α}^{α_{1}}β_{1} + ⋯ + Ω_{α}^{α_{n}}β_{n}.

(b) We can obtain the system of [4] from (a) by making the following changes:

– Let f_{i} : S_{i} → Ord be defined as f_{i} in Example 2.7. (i) of [18], but with basis I.

– Restrict ψ_{Ω_{α+1}}(A) to A such that f_{l}(A) ∈ C_{Ω_{α+1}}(f_{l}(A)), where C_{Ω_{α+1}} is defined as in [4] (or equivalently such that k̃(A) ⊆ C_{Ω_{α+1}}(f_{l}(A))).

– Restrict ψ_{I}(A) to A such that f_{l}(A) ∈ C_{I}(f_{l}(A)).

– Insert in (Arg_{Ω_{α+1}}, ≺′_{Ω_{α+1}}) between Arg′_{Ω_{α+1}} and the “ψ_{Ω_{α+1}}-terms” φ_{]0,Ω_{α+1}[}([0, Ω_{α+1}[), define k′_{Ω_{α+1}}, l′_{Ω_{α+1}} for these new terms as k, l in Example 2.7. (f) of [18] and level(φ_{a}b) := 0_{l}. (Note that we have already the ω-function, which corresponds to λγ.φ_{0}γ in the system of [4]).

Then one can easily see that we obtain again a cardinality based I-OFG (κ_{0} = I), eval_{Ω_{α+1}} on CNF_{Ω_{α+1}}(α⃗), and eval_{I} on Ω_{α} have the same values as in (a), eval_{Ω_{α+1}}(φ_{α}β) = φ_{α}β, eval_{Ω_{α+1}}(ψ_{Ω_{α+1}}(A)) = ψ_{Ω_{α+1}}(f_{l}(A)), eval_{I}(ψ_{I}(A)) = ψ_{I}(f_{l}(A)), where ψ_{Ω_{α+1}}, ψ_{I} are as in [4], and the term set of the underlying ordinal system together with its order is isomorphic to the set of terms in [4] which make use of terms ≺ ω_{l}(I + 1) only (where ω_{0}(a) := a, ω_{l+1}(a) := ω^{ω_{l}(a)}). Therefore in the limit the order types of these I-OS reach |KPI|.

Remark 6.7. The (straightforward) generalization of Remark 4.7. in [18] to I-OFG holds.

Lemma 6.8. (a) For every OFG in the Example 6.6 there exists an elementary

OS based on it.

(b) The supremum of the strength of I-OS is |KPI|.

Proof. (a) as for Lemma 2.9. of [18]. (b) The elementary OS based on the sequence of OFG of Example 6.6 (b) (as well those of 6.6 (a)) have in the limit the strength of |KPI|.

Theorem 6.9. (a) Every I-OS is well-ordered.

(b) Every elementary I-OS has order type below |KPI| = |(Δ_{2}^{1} − CA) + (BI)| = ψ(ϵ_{I+1}).

(c) The bound in (a) is sharp.

References

1. W. Buchholz. Normalfunktionen und konstruktive Systeme von Ordinalzahlen. In J. Diller and G.H. Müller, editors, Proof Theory Symposion, Kiel 1974, volume 500 of Springer Lecture Notes in Mathematics, pages 4 – 25, Berlin, Heidelberg, New York, 1975. Springer.

2. W. Buchholz. A new system of proof-theoretic ordinal functions. Ann. Pure a. Appl. Logic, 32:195 – 207, 1986.

3. W. Buchholz. Wellordering proofs for systems of fundamental sequences. Draft, München, 1990.

4. W. Buchholz. A simplified version of local predicativity. In P. Aczel, H. Simmons, and S. S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 115 – 147, Cambridge, 1992. Cambridge University Press.

5. W. Buchholz and K. Schütte. Proof Theory of Impredicative Subsystems of Analysis. Bibliopolis, Naples, 1988.

6. J.-Y. Girard. Proof theory and logical complexity. Handwritten notes, 1135 pp.

7. J.-Y. Girard. Π_{2}^{1}-Logic, part 1: Dilators. Ann. Pure a. Appl. Logic, 21:75 – 219, 1981.

8. G. Jäger. A well-ordering proof for Feferman’s theory T_{0}. Arch. math. Logic, 23:65 – 77, 1983.

9. G. Jäger. Theories for Admissible Sets: A Unifying Approach to Proof Theory. Bibliopolis, Naples, 1986.

10. P. Martin-Löf. Intuitionistic type theory. Bibliopolis, Naples, 1984.

11. W. Pohlers. Proof Theory. An introduction, volume 1407 of Springer Lecture Notes in Mathematics. Springer, Berlin, Heidelberg, New York, 1989.

12. M. Rathjen. How to develop proof–theoretic ordinal functions on the basis of admissible ordinals. Mathematical Logic Quarterly, 39(1):47 – 54, 1993.

13. M. Rathjen and A. Weiermann. Proof–theoretic investigations on Kruskal’s theorem. Annals of Pure and Applied Logic, 60:49–88, 1993.

14. K. Schütte. Kennzeichnung von Ordinalzahlen durch rekursiv definierte Funktionen. Math. Ann., 127:16–32, 1954.

15. A. Setzer. Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe. PhD thesis, Universität München, 1993.

16. A. Setzer. An introduction to well-ordering proofs in Martin-Löf’s type theory. In G. Sambin and J. Smith, editors, Twenty-five years of constructive type theory, pages 245 – 263, Oxford, 1998. Clarendon Press.

17. A. Setzer. Well-ordering proofs for Martin-Löf type theory. Annals of Pure and Applied Logic, 92:113 – 159, 1998.

18. A. Setzer. Ordinal systems. To appear in: B. Cooper, J. Truss, editors, Sets and Proofs, Cambridge University Press, 1999.