Ordinal Systems

Anton Setzer ^{∗}

January 26, 2001

Abstract

Ordinal systems are structures for describing ordinal notation systems, which extend the more predicative approaches to ordinal notation systems, like the Cantor normal form, the Veblen function and the Schütte Klammer symbols, up to the Bachmann-Howard ordinal. σ-ordinal systems, which are natural extensions of this approach, reach without the use of cardinals the strength of the theories for transfinitely iterated inductive definitions ID_{σ} in an essentially predicative way. We explore the relationship with the traditional approach to ordinal notation systems via cardinals and determine, using “extended Schütte Klammer symbols”, the exact strength of σ-ordinal systems.

1 Introduction

1.1 Motivation

The original problem, which motivated the research in this article, seemed to be a pedagogical one. We have been trying to teach ordinal notation systems above the Bachmann-Howard ordinal several times. The impression we had was that we were able to teach the technical development of these ordinal notation systems, but there always remained some doubts in the audience. It remained unclear, why one could get a well-ordered notation system by denoting small ordinals by big cardinals.

The situation was completely different with typical ordinal notation systems below the Bachmann-Howard ordinal. We had the impression we always succeeded in teaching it after the audience had overcome some technical problems. And this included the Schütte Klammer symbols (an ordinal notation system extending the Veblen hierarchy — they will essentially be defined in this article): Although they are technically more complicated than the systems using one uncountable cardinal, they seem to be far more acceptable. Therefore the reason behind our pedagogical problems was not a technical one. The real problem was about foundations.

The original task of proof theory as understood by Hilbert was to show the consistency of systems in which mathematical reasoning can be formalized. After the proof of Gödel’s incompleteness theorem, one had to modify this and demand the reduction of the consistency of a theory to some principles, for which we have good reasons to believe that they are correct. One reason, why Gentzen’s result was so much appreciated, when it was presented, was that he reduced the consistency of Peano Arithmetic to the principle of well-ordering up to ϵ_{0}, of which we believe intuitively that it is correct. The argument presented in Lemma 2.2 is an attempt to formalize what we believe is the reason for our confidence with this principle: the usual notation system for ϵ_{0} is built from below and has therefore an intuitive well-ordering proof.

∗Department of Mathematics, Uppsala University, P.O. Box 480, S-751 06 Uppsala, Sweden, email:

setzer@math.uu.se

For the Veblen function and for the Schütte Klammer symbols the same holds. So, when analyzing a theory using these systems we have really gained more than only the reduction of the consistency of theory to a primitive recursive well-ordering: the reduction to the well-foundedness of an ordering, of which we intuitively believe that it is correct.

This leads to another aspect: the relationship to the notion of “natural well-ordering”. There exists a trivial ordinal analysis for any consistent theory. Take as elements of a wellordering essentially pairs consisting of a well-ordering proof in the theory and elements of the corresponding well-ordering and order them lexicographically by the Gödel-number of the proof and the ordering we are referring to. (A slight refinement is necessary in order to make it primitive recursive: replace the elements of the well-ordering by triples <a, b, c> where a is an element of the well-ordering, b a calculation that determines that a is an element of this ordering and c is a calculation that determines for all x < a, where < is the ordering on the natural numbers, whether x belongs to the well-ordering and, if yes, the order relation between x and a. Order triples <a, b, c> by the ordering of a). The corresponding ordering has as order type the proof theoretic ordinal of the theory.^{1} In order to make clear that what one was doing is not trivial, one usually states that one determines the proof theoretic strength not in some arbitrary primitive recursive notation system, but in a natural one. However, nobody succeeded up to now in defining precisely, what a natural well-ordering is. But there might be some systematic reason, why we will never be able to formalize, what a natural well-ordering is: if one has a precise notion, one will probably find a system diagonalizing over it, and this system can no longer be natural, although it will be in an intuitive sense.

After the considerations before, we suggest that one should replace “natural wellordering” by “ordering with an intuitive well-ordering proof”. We believe that the reduction to such well-orderings is in fact the real motivation for designing stronger and stronger ordinal notation systems. We will see in the following that the usual systems as developed by the Schütte school (we have not studied ordinal diagrams sufficiently yet) fulfill essentially this requirement. With a little bit more structure it is easy to see intuitively, why the system is consistent.

In the following we are going to explore three types of (iterated) ordinal systems: (noniterated) ordinal systems, n-ordinal systems and σ-ordinal systems. For each of these systems we will proceed as follows: First we motivate and introduce the structure. We will motivate that each of the steps taken is very natural — it is not the only natural way of proceeding but one possible one. We will then present, what we hope is an intuitive wellordering proof, which will be formalized rigorously in a theory of the appropriate strength and provides therefore as well upper bounds for the order types of the structure. In the case of σ-ordinal systems the rigorous formalization is not completed yet and we will omit the argument. After this intuitive well-ordering proof we will give constructive well-ordering proofs, which will be far shorter than the intuitive argument. However, although they have the advantage that they can be formalized in constructive theories, which does not hold for the intuitive well-ordering proofs, we personally believe in the well-ordering of the system essentially because of the intuitive well-ordering proof, not the constructive ones. We do not understand yet why this is the case, an analysis of this needs still to be done. It will become clear however that both proofs will be closely related.

Next we are going to introduce a sequence of ordinal notation systems, which exhausts the strength of the structure. It is no problem to develop it in a mere syntactical way. However, we want as well to develop functions acting on ordinals and not only on notations, and, when developing first the functions, we get the notation system almost for free. So we will take the detour via ordinal functions, which might not be as convincing for those, who like to cut out any ideal concepts like ordinals, but might be quite satisfactory for those, who want to compare the approach taken here with the traditional approach. We will succeed in recovering the functions used in the traditional approach in our setting. From the development taken, it will be very clear that we can introduce the notation system without referring to ordinals, not even for heuristic purposes, and it would be a boring task to rewrite these subsections so that no ordinals are used.

1We have heard this example from Richard Sommer, but do not know of its origins.

Technical advantages: This approach separates properties of ordinal notation systems, which do not have an influence on the whole strength of it, from structural properties, which are crucial for achieving the strength. The well-ordering proofs itself will become easier (for instance it works in one step, one does not have first to verify that the accessible part is closed under +, then under ω^{·}, then under ψ etc.) and focuses on, what is actually needed from the ordinal system, whereas the specific ordinal notation system plays only a role when verifying that it is an instance of a (non-iterated or n- or σ-) ordinal system. As a side-result we get simultaneously well-ordering proofs in the formal theories considered for a complete family of notation systems, not only for one specific system.

Background needed: We will in this article work quite lot with ordinals. However, we believe that one can understand quite a lot of it, even without having a deep insight. Without the knowledge of ordinal notation systems up to ϵ_{0} it will be probably difficult to understand anything. Knowledge of the Veblen function will be useful, but not necessary. We will consider Schütte Klammer symbols as examples. But, who does not know the Veblen function or the Klammer symbols, can take the equation we state between those functions and the corresponding ordinal function generators as the definition. In this case we recommend to skip the versions with fixed points and just consider the fixed-point free versions of φ and the Klammer symbols, which are in our setting more natural than the usual ones. The comparison with the ϑ- and ψ-function is only relevant for those, who know those systems. It will be useful — but not necessary — to read the first four sections of [Set98a], especially of the motivation given there.

Future developments: With σ-ordinal system we have not exhausted the power of combinations of ordinal systems, in the meantime we have developed ordinal systems which cover the strength of one recursive inaccessible and one recursive Mahlo ordinal, and this is certainly no the end of what can be done with our approach. For the author, this was quite satisfactory, since one can see, that even up to Mahlo we can work with extensions of Schütte’s Klammer symbols in a way which is still from below. Before carrying out this research, we could work with and calculate with the strong ordinal notation systems, but always had some feeling that what we were doing, was dubious. The only real argument for the well-foundedness of the systems was the well-ordering proof in a corresponding constructive theory and the main justification for carrying out ordinal analysis seemed to be to provide good tools for reducing the consistency of one theory to another where a direct way was impossible. But now we are really convinced that one gains something more: the reduction of the consistency to the well-ordering of a structure, for which we have an intuitive well-ordering proof, and which is — in an extended sense — built from below.

1.2 Notations

Definition 1.1 (a) As in [Set98a], A^{∗} will be the set of finite sequences of elements of A, coded, if A ⊆ ℕ as natural numbers, (a⃗)_{i} will be the ith element of the sequence a⃗ and (a slight change relative to [Set98a]) seqlength(a⃗) will be the length of the sequence a⃗. A class is an object {x | φ}, where φ is a formula. In this case, after some possibly necessary α-conversion, a ∈ {x | φ} := φ[x := a]. We identify unary predicates Q with the class {x | Q(x)}. A binary relation ≺ is a class. For binary relations ≺ we define r ≺ s := π(r, s) ∈≺, where π is a standard primitive recursive pairing function on the natural numbers having the usual properties. An ordering is a pair (A, ≺) where A is a class and ≺ is a binary relation on A. It is primitive recursive, if A is a primitive recursive subset of ℕ and ≺ is primitive recursive, and linear, if ≺ is a linear ordering on A. If A = (B, ≺), then |A|:= B, ≺_{A}:=≺. If C ⊆ |A|, we will write (C, ≺) instead of (C, ≺ ∩(B × B)). Transfinite induction over (A, ≺) with respect to the class B, in short TI_{(A,≺)}(B), is defined as ∀x ∈ A(∀y ∈ A(y ≺ x → y ∈ B) → x ∈ B) → ∀x ∈ A.x ∈ B. As in [Set98a], we define PRA^{+} as the extension of PRA by additional predicates (called free predicates) without having induction over formulas containing these predicates. Let A be a class, ≺ be a binary relation, both depending on unary free predicates A_{i} and binary free predicates ≺_{i} (i = 1, …, n). Transfinite induction over (A, ≺) is in PRA reducible to transfinite induction over (A_{i}, ≺_{i}) (i = 1, …, n), in short TI_{(A,≺)} is PRA-reducible to TI_{(A_{i},≺_{i})}, if there exist n_{i} ∈ ℕ, variables z_{i,j,k}, classes B_{i,j} with free variables ⊂ {z_{i,j,1}, …, z_{i,j,m_{i,j}}}, such that PRA^{+} ⊢ (⋀_{i=1}^{n} ⋀_{j=1}^{n_{i}}(∀z_{ij1}, …, z_{ijm_{i,j}}.TI_{(A_{i},≺_{i})}(B_{ij})) → TI_{(A,≺)}(Q) for some free unary predicate Q.

(b) Assume B is a class and ≺ is a binary relation, both depending on unary free predicates A_{i} and binary free predicates ≺_{i} (i = 1, …, m). (B, ≺) is an elementary construction from (A_{1}, ≺_{1}), …, (A_{m}, ≺_{m}), if the following holds: the formulas defining B, ≺ are formulas of the language of PRA with bounded quantifiers only (ie. quantifiers of the form ∀x < t, ∃x < t); PRA^{+} proves that, if (A_{i}, ≺_{i}) are linear orderings (i = 1, …, m), so is (B, ≺); transfinite induction over (B, ≺) is PRA-reducible to transfinite induction over (A_{i}, ≺_{i}).

(c) If f : A → B, M ⊆ A, then f[M]:= {f(x) | x ∈ M}. P^{fin}(A) is the set of finite sets of elements of A coded, if A ⊆ ℕ, as natural numbers, such that the usual properties, especially primitive recursiveness and decidable subset-relation hold. In case B ∈ P^{fin}(A), we write t ∈ B for the statement expressing t is an element of B expressed in the language of PRA. If B ∈ P^{fin}(A), a ∈ A, ≺ is a binary relation of A, then B ≺ a:⇔ ∀x ∈ B.x ≺ a, a ≺ B:⇔ ∃x ∈ B.a ≺ x. This definitions extends to arbitrary classes B as well. If ≺ is a binary relation on A, a ⪯ b:⇔ a ≺ b ∨ a = b, similarly we define ≺′ from ≺, ≤ from < etc. If k : A → P^{fin}(B) and C ⊆ B, then k^{−1}(C):= {x ∈ A | k(x) ⊆ C}. We write f : A →_{ω} B for f : A → P^{fin}(B). If f : A →_{ω} B, f′ : A →_{ω} B, g : B →_{ω} C, then g ∘ f: A →_{ω} C, (g ∘ f)(a) := g[f(a)], and f ⊆ f′ :⇔ ∀x ∈ A.f(x) ⊆ f′(x).

(d) If A_{1}, …, A_{m} are orderings, f : (|A_{1}|×⋯×|A_{m}|) → M injective, then f[A_{1}, …, A_{m}] denotes the ordering (f[|A_{1}| × ⋯ × |A_{m}|], ≺) where f(a_{1}, …, a_{m}) ≺ f(b_{1}, …, b_{m}) if (a_{1}, …, a_{m}) lexicographically less then (b_{1}, …, b_{m}) with respect to the orderings A_{1}, …, A_{m}. We will use this definition only in case where f(a_{1}, …, a_{n}) is the result of substituting in a term t (such as φ_{x_{1}}x_{2}, ψ(x_{1}), (x_{1}, x_{2}, x_{3}), x_{1} + x_{2}, \binom{x_{1}}{x_{2}}) variables x_{i} by a_{i}, i. e. f = λx_{1}, …, x_{n}.t, and will write in this case the result of replacing in t the variable x_{i} by A_{i} instead of f[A_{1}, …, A_{m}] (i.e. φ_{A_{1}}A_{2}, ψ(A_{1}), … instead of (λx, y.φ_{x}y)[A_{1}, A_{2}], (λx.ψ(x))[A_{1}]). The convention is here that the variables x_{i} are ordered from left to right and in case of \binom{x}{y} from bottom to top (i.e. φ_{A_{1}}A_{2} is ordered by lexicographic ordering on (A_{1}, A_{2}), \binom{A_{1}}{A_{2}} by lexicographic ordering on (A_{2}, A_{1})). Note that, after some standard Gödelization of terms, the new ordering in the examples with f = λx⃗.t is an elementary construction from the orderings A_{i}.

(e) If A is an ordering, A_{des}^{∗} (A_{weakdes}^{∗}) is the set/class of — possibly empty — strictly descending (weakly descending) sequences ordered lexicographically, which is an elementary construction from A. We omit double brackets for the elements of A_{des}^{∗} and A_{weakdes}^{∗}, writing for instance (a_{1}, b_{1}, …, a_{m}, b_{m}) instead of ((a_{1}, b_{1}), …, (a_{m}, b_{m})) for an element of (A, B)_{des} and \binom{a_{1}···a_{m}}{b_{1}···b_{m}} instead of (\binom{a_{1}}{b_{1}} ⋯ \binom{a_{m}}{b_{m}}) for an element of

\binom{A}{B}_{des}^{∗}. Obviously A_{des}^{∗} is an elementary construction from A.

(f) (Generalization of Schütte’s Klammer symbols [Sch54]). If A, B are orderings, let Schütte\binom{A}{B} := \binom{A}{B}_{des} ∩ \{\binom{a_{1}···a_{m}}{b_{1}···b_{m}} | m ∈ ω, a_{i} ∈ A, b_{i} ∈ B, b_{1} >_{B} ⋯ >_{B} b_{m}\}. Note that we have reversed the order relative to [Sch54]. Further we define Schütte(A, B) := ((A, B))_{des} ∩ {(a_{1}, b_{1}, …, a_{m}, b_{m}) | m ∈ ω, a_{i} ∈ A, b_{i} ∈ B, a_{1} >_{A} ⋯ >_{A} a_{m}}. Both are elementary constructions from A, B.

(g) If A_{1}, …, A_{m} are orderings and |A_{i}| are disjoint, then B :=A_{1} ◯ ≺ A_{2} ◯ ≺ ⋯ ◯ ≺ A_{m} is the ordering with |B| being the union of the A_{i} and ≺_{B} being the union of the ≺_{A_{i}} together with the pairs (a, b) for a ∈ |A_{i}|, b ∈ |A_{j}|, 1 ≤ i < j ≤ n. This is an elementary construction from the orderings A_{i}.

(h) We identify the one element set A with the ordering (A, ∅).

(i) If A is an ordering, B a set, let A ∩ B := (|A| ∩ B, ≺_{A} ∩((|A| ∩ B) × (|A| ∩ B))) and A \ B := A ∩ (|A| \ B). Note that this is an elementary construction from A, if B is primitive recursive.

(j) If A is an ordering, let Acc(A) be the accessible part of |A| with respect to ≺_{A}, i.e. the largest well-founded part of A, ⋃{X ⊆ |A| | (X, ≺) well-ordered }. Acc_{≺}(B) := Acc(B, ≺).

(k) If A is an ordering, a, b ∈ |A|, B ⊆ |A|, let B ∩ a := {c ∈ B | c ≺_{A} a}, and [a, b] := {c ∈ |A| | a ⪯_{A} c ⪯_{A} b}. The half open and open intervals [a, b[, ]a, b] and ]a, b[ are defined similarly. Again we obtain elementary constructions from A, if B is primitive recursive.

(l) If A is an ordering, B, C ⊆ |A|, then B ⊑ C (B is an initial segment of C) :⇔ B ⊆ C ∧ ∀x ∈ B.B ∩ x = C ∩ x.

(m) Ord is the class of ordinals, 𝔸 the class of additive principal numbers > 0. We identify classes of ordinals A with the ordering (A, <), where < is the usual ordering on Ord.

2 Elementary Ordinal Systems

2.1 Definition of Ordinal Systems

We will in the following develop first the notation of ordinal systems from that of ordinal notation systems from below as defined in the first four chapters of [Set98a]. However, it is not necessary to read this article, since for the reader who doesn’t know the previous approach we will then repeat the motivation given there, adapted to the new setting.

In [Set98a], the underlying structure of ordinal notation systems from below consisted of the set of notations T, a subset NF of T^{∗}, linear orderings ≺ on T and ≺′ on NF and a function f : NF → T. In order to deal with stronger systems, which extend the notion of ordinal notation system from below and allow to define ordinals beyond the Bachmann-Howard ordinal, one needs to deal with arguments that have more structure. Even in the case of ordinals below the Bachmann-Howard ordinal some more structure on the argument is needed. For instance in case of extended Schütte Klammer symbols (in English: “parenthesis symbols” or better “matrix symbols”), which will be defined in Example 2.7 (i) below, we need the information about the size of each of the sub-matrices and which ordinal notations belong to which sub-matrix. We could handle this by using some coding (see Subsection 2.2). However, the more elegant approach is to replace the set NF ⊆ T^{∗} by an arbitrary set Arg together with a function k : Arg →_{ω} T. The intuition is, that a ∈ Arg is an argument for the function f which is built from ordinal notations k(a), but has some additional structural information. An ordinal notation system from below can be translated into the new structure by defining Arg := NF and k(a_{1}, …, a_{m}) := {a_{1}, …, a_{m}}.

Now f was always a bijection, and therefore we can identify Arg with T, define f := λx.x and omit f completely. We have therefore two orderings on T, ≺ and ≺′, ≺ being the ordering on the ordinal notation system and ≺′ being the ordering which determines the order, in which new ordinal notations are introduced.

In order to express that T is the closure under the above process, we add a function length : T → ℕ and require length(a) < length(b) for a ∈ k(b). We replace the long name “ordinal notation system from below” by “ordinal system”.

The motivation for the resulting structure is now as follows: Ordinal notations t are built from a finite set of notations k(t). We want that the system is built from below: First, an ordinal should be denoted using smaller ones, i.e. k(t) ≺ t. Second, whenever we introduce a new notation t, we want to have constructed all smaller notations s before t. Either s could be below one of the components of t, i. e. s ⪯ k(t), since, whenever we introduce an ordinal, we assume that we have constructed its components and therefore all ordinals below them as well. Or s must have been introduced before t with respect to the termination ordering ≺′, i. e. s ≺′ t. In [Set98a] we showed that in case of simple systems like the standard system up to Γ_{0} or the Schütte Klammer symbols, we can construct ≺′ from ≺ by using the lexicographic ordering on pairs and on strictly descending sequences together with some simple operations. For instance we ordered terms for the Cantor normal form by the lexicographic ordering on strictly descending sequences and terms φ_{a}b by the lexicographic ordering on pairs (a, b). Orderings ≺′ constructed like this have the property that, whenever a set of notations is ≺-well-ordered, the set of notations built from it is ≺′-well-ordered, and in the definition of ordinal systems we will demand this condition. However, in the above examples it is possible to show this reduction in PRA, i.e. essentially in logic, and we define elementary ordinal systems by demanding additionally this stronger requirement. Elementary ordinal systems will have strength below the Bachmann-Howard ordinal, whereas with ordinal systems we will have no upper bound (choose for an arbitrary well-ordering (T, ≺), k(a) := ∅, length(a) := 0, ≺′:=≺).

Definition 2.1 (a) An Ordinal System Structure, in short OS-structure, is a quintuple F = (T, ≺, ≺′, k, length) where T is a set, ≺′, ≺ are linear orderings on T, k : T →_{ω} T and length : T → ℕ. We will sometimes regard the first two or three elements of this quintuple as a unity, so when writing F is an OS-structure of the form F = (A, ≺′, k, length) or (G, k, length) we mean that A is of the form (T, ≺) and G is of the form (T, ≺, ≺′) with T, ≺ and

≺′ as above.

(b) In the following, if not mentioned otherwise, let F be as in (a), and for any index i F_{i} = (T_{i}, ≺_{i}, ≺′_{i}, k_{i}, length_{i}).

(c) If F is an ordinal system structure as above, A, B ⊆ T, then B ↾ A := B ∩ k^{−1}(A), the restriction of B to arguments built from A or shorter restriction of B to A.

(d) An Ordinal System, in short OS, is an OS-structure F, such that the following holds: (OS 1) ∀t ∈ T.k(t) ≺ t. (OS 2) length[k(t)] < length(t). (OS 3) ∀t ∈ T.∀s ∈ T(s ≺ t → (s ⪯ k(t) ∨ s ≺′ t)). (OS 4) If A ⊆ T, A is ≺-well-ordered, then T ↾ A is ≺′-well-ordered.

(e) An OS F is primitive recursively represented, if T is a primitive recursive subset of ℕ, ≺, ≺′, k, length are primitive recursive, and all the properties of an OS, including linearity of ≺, ≺′, but except of (OS 4), can be shown in PRA.

(f) A primitive recursively represented OS F is elementary, if additionally (OS 4) can be shown in PRA, i.e. for a free predicate R TI_{(T↾R,≺′)} is PRA-reducible to TI_{(T∩R,≺)}.

(g) An OS-structure is well-ordered, if T is well-ordered. The order type of a well-ordered OS-structure F is the order type of T.

(h) Two OS-structures are isomorphic, if there exists a bijection between the underlying sets, which respects ≺, ≺′, k, length.

We illustrate an ordinal system by the following picture:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} t  r s  t k k(t) = {r, s} (T, ≺′)  (T, ≺)

(The arrow from t in (T, ≺′) to t in (T, ≺) represents the function f in the original definition, which is now the identity).

2.2 Equivalence of Elementary Ordinal Systems and Ordinal Notation Systems from below.

Let ≺′′ be the ordering on NF in an ordinal notation system from below, f the function used there, define ≺′ on f[NF] by f(a⃗) ≺′ f(b⃗) :⇔ a⃗ ≺′′ b⃗, k(f(a⃗)) := {a_{1}, …, a_{n}} and length in the obvious way. Then, if we started with an ordinal notation system from below in which ≺′′ is linear, provably in PRA, we obtain an elementary OS.

In the other direction, assume an elementary OS, together with an explicit enumeration of the natural numbers, i. e. there exists a primitive recursive function g : ω → T, where we write \underline{n} for g(n), such that ∀n.n ≤ \underline{n} and ∀n ∈ ℕ.\underline{n} = nth element of T provable in PRA (more precisely the formula ∀n ∈ ℕ(n ≤ \underline{n} ∧ ∀x ∈ T(x ≺ \underline{n} ↔ ∃l < n.x = \underline{l})) is provable in PRA). Note that therefore g[ω] and g^{−1} : g[ω] → ω are primitive recursive. Define T′ := T, NF′ ⊆ T′^{∗}, NF := \{()\} ∪ \{(\underline{0}, \underline{n}) | n ∈ ω\}∪

\{(\underline{1}, \underline{t}, s_{1}, …, s_{m}) | t ∈ T \ g[ω] ∧ m ∈ ω ∧ s_{1} ≺ ⋯ ≺ s_{m} ∧ k(t) = \{s_{1}, …, s_{m}\}\};

f′ : NF′ → T′, f′() := \underline{0}, f′(\underline{0}, \underline{n}) := \underline{n+1}, f′(\underline{1}, \underline{t}, s_{1}, …, s_{m}) := t; ≺′′ on NF by () ≺′′ (\underline{0}, \underline{0}) ≺′′ (\underline{0}, \underline{1}) ≺′′ (\underline{0}, \underline{2}) ≺′′ ⋯ ≺′′ (\underline{1}, \underline{t}, s_{1}, …, s_{m}) for all t and (\underline{1}, \underline{t}, s_{1}, …, s_{m}) ≺′′ (\underline{1}, \underline{t}′, s′_{1}, …, s′_{l}) iff t ≺′ t′. Then one sees easily that (T, ≺, NF, ≺′′, f′) is an ordinal notation system from below, which has the same order type as the original ordinal system and has essentially “the same form”, therefore under the above mentioned weak conditions, elementary OS can be seen as ordinal notation systems from below.

2.3 Intuitive Argument why OS are Well-ordered.

We will first illustrate, what we regard as an intuitive argument for the well-ordering of ordinal system, by taking a standard example.

Take the notation system built from the Cantor Normal form and the Veblen-function, based on φ_{0}α = ϵ_{α}. More precisely, it is defined as follows: Let ℕ̂ be the set of terms {0, S(0), S(S(0)), … }. 1 := S(0). The set of ordinal notations T together with the ordering ≺ on T are simultaneously defined by: ℕ̂ ⊆ T, if a_{1}, …, a_{m} ∈ T, n_{i} ∈ ℕ̂ \ {0}, m > 0, then φ_{a_{1}}a_{2} ∈ T provided m = 2 and a_{2} is not of the form φ_{b_{1}}b_{2} with a_{1} ≺ b_{1}, and ω^{a_{1}} · n_{1} + ⋯ + ω^{a_{m}} · n_{m} ∈ T provided a_{m} ≺ ⋯ ≺ a_{1} and if m = 1, then a_{1} ≠ 0 and a_{1} is not of the form φ_{b_{1}}b_{2}. S^{k}(0) ≺ S^{l}(0) :⇔ k < l, S^{k}(0) ≺ ω^{a_{1}} · n_{1} + ⋯ + ω^{a_{m}} · n_{m}, S^{k}(0) ≺ φ_{a}b, ω^{a_{1}} · n_{1} + ⋯ + ω^{a_{m}} · n_{m} ≺ ω^{b_{1}} · l_{1} + ⋯ + ω^{b_{k}} · l_{k} :⇔ (a_{1}, n_{1}, …, a_{m}, n_{m}) is lexicographically smaller than (b_{1}, l_{1}, …, b_{k}, l_{k}), c := ω^{a_{1}} · n_{1} + ⋯ + ω^{a_{m}} · n_{m} ≺ φ_{a}b :⇔ a_{1}, …, a_{m}, n_{1}, …, n_{m} ≺ φ_{a}b and, if this condition does not hold, then φ_{a}b ≺ c, and φ_{a}b ≺ φ_{a′}b′ :⇔ (a ≺ a′ ∧b ≺ φ_{a′}b′)∨(a = a′ ∧b ≺ b′)∨(a′ ≺ a∧φ_{a}b ≺ b′). The termination ordering ≺′ on T is now defined by S^{k}(0) ≺′ ω^{a_{1}} · n_{1} + ⋯ + ω^{a_{m}} · n_{m} ≺′ φ_{a}b, S^{k}(0) ≺′ S^{l}(0) iff k < l, ≺′ on terms ω^{a_{1}} ·n_{1} +⋯+ω^{a_{m}} ·n_{m} is the lexicographic ordering, and ≺′ on terms φ_{a}b is the lexicographic ordering on pairs (a, b) (the last two with respect to ≺). Further define k(0) = ∅, k(S(t)) := {t}, k(ω^{a_{1}} · n_{1} + ⋯ + ω^{a_{m}} · n_{m}) := {a_{1}, …, a_{m}, n_{1}, …, n_{m}} and k(φ_{a}b) := {a, b}.

It is easy to see that with the obvious definition of length we get an ordinal system (T, ≺, ≺′, k, length), especially we have: If A ⊆ T is ≺-well-ordered, the set of notations “built from A” or “with components in A”, namely k^{−1}(A), is ≺′-well-ordered. Now we proceed by selecting ordinal notations as follows: At the beginning we have no notation at all. The only notation which has components in the empty set is 0 and we select it. Now, if we take the the ordinals with components in the set of notations selected, namely in {0}, we choose the ≺′-least one not selected before, namely S(0). Again, we take all notations with components in {0, S(0)}, select the ≺′-least one not chosen before, S(S(0)), etc. Once we have selected all the natural numbers, the least one will be ω^{1} · 1. The ≺′ least one in T ↾ {0, S(0), S(S(0)), … } ∪ {ω^{1} · 1} not selected before will be ω^{1} · 1 + ω^{0} · 1 and one sees easily that we will proceed selecting systematically all ordinals built by the Cantor normal form, i. e. all notations below φ_{0}0.

The next ordinal will selected will be φ_{0}0. And here we will make for the first time a jump in the ≺′-ordering: there are notations ≺′ φ_{0}0 we have not chosen yet, but they are built from notations which we have not constructed before. After φ_{0}0 we will choose ω^{φ_{0}0} · 1 + ω^{0} · 1 — we will therefore move downwards with respect to ≺′ — and then we will exhaust again the Cantor normal form and choose all ordinals below φ_{0}1. Now φ_{0}1 will be selected and we will then proceed selecting (with the steps for building the Cantor normal form in between) φ_{0}2, φ_{0}3, …, φ_{0}(φ_{0}0), …, φ_{0}(φ_{0}(φ_{0}0)), …, then φ_{1}0. etc.

In order to be able to select the ≺′-least element of the sets considered, we need that the set of notations with components in the notations previously selected is ≺′-well-ordered. Now by (OS 4) this will be the case, if we have that the sequence of ordinals previously selected is ≺-increasing and therefore ≺-well-ordered. Now we can easily see by induction over the process above that, whenever we select an ordinal, we select in fact the ≺-least one not chosen before and therefore the set of ordinals previously chosen will be a ≺-segment of T:

Assume A is the ordinals previously selected, which is by IH a segment of the ordinals and let a be the new notation chosen. a will be bigger than A, since A is a segment. We need to show, which we will do by induction over the length of b, that, if b ≺ a, b ∈ A. If b ≺ a, then b ⪯ k(a) ⊆ A, so b ∈ A by A being a segment, or b ≺′ a. b is built from smaller components, they must be by side-IH all in A, therefore b has components in A, a was the ≺′-least such not selected before, so b must have been selected before, b ∈ A.

Now we assume that “we do not run out of ordinals”. Therefore we must reach a point, where we cannot select an ordinal any more. But then one sees easily that all notations must be selected, so the set of notations must be well-ordered (since we have selected them in increasing order) and we are done.

The argument “we do not run out of ordinals”, can now be formalized in set theory for elementary ordinal systems by using ω_{1}^{ck}: if we could select as above ω_{1}^{ck} ordinals, we would have a primitive recursive well-ordering of order type ω_{1}^{ck}, a contradiction. For this argument we need the big ordinal ω_{1}^{ck}. However it is only needed to provide an ordinal “big enough”. In fact, the process of selecting ordinals will terminate after α steps for some α which is below ω_{1}^{ck}. Something similar will be the case for all recursively large ordinals needed for stronger ordinal notation systems: they always play only the role of ordinals “big enough”, in fact, all processes involved will terminate after α steps for some ordinal < ω_{1}^{ck}.

We are now going to formalize the well-ordering argument above rigorously, in order to get absolute precision. We will then show that for elementary ordinal systems, it can be formalized in Kripke-Platek set theory (with natural numbers as urelemente). Therefore we will get an upper bound for the strength of elementary ordinal systems.

Lemma 2.2 (a) Let F be an ordinal system, and assume ⊥ ∉ T. By recursion on ordinals γ we define a_{γ} ∈ T ∪ {⊥} as follows: Let A_{<γ} := {a_{α} | α < γ}. Define “A_{<γ} is increasing” iff A_{<γ} ⊆ T and ∀α, β < γ(α < β → a_{α} ≺ a_{β}).

a_{γ} := \begin{cases}min_{≺′}((T ↾ A_{<γ}) \ A_{<γ}) & if A_{<γ} is increasing and T ↾ A_{<γ} ⊈ A_{<γ}, \\ ⊥ & otherwise. \end{cases}

Then there exists a γ such that A_{<γ} is increasing and A_{<γ} = T. Therefore (T, ≺) is well-ordered.

(b) γ as in (a) is < ω^{ck}, if F is primitive recursively represented.

(c) If F is elementary, (a) can be formulated in KPω.

Proof: (a): The definition is well-defined, since, if A_{<γ} is increasing, T ↾ A_{<γ} is well-ordered with respect to ≺′, therefore as well (T ↾ A_{<γ}) \ A_{<γ} and a_{γ} can be defined. We show: If A_{<γ} is increasing, then A_{<γ} is an initial segment of T w.r.t. ≺ by recursion on γ: The cases γ = 0 or γ limit ordinal follow trivially or by IH. Let now γ = δ + 1. We need to show a_{δ} is the <-least element in T \ A_{<δ}: a_{δ} ∉ A_{<δ}, which is an initial segment of T, therefore A_{<δ} ≺ a_{δ}. We show by induction on length(b) ∀b ≺ a_{δ}.b ∈ A_{<δ}, from which the assertion follows. b ≺ a_{δ}, therefore b ⪯ k(a_{δ}) ⊆ A_{<δ} ⊑ T and therefore b ∈ A_{<δ} or b ≺′ a_{δ}. In the last case, by IH, since k(b) ≺ b ≺ a_{δ}, k(b) ⊆ A_{<δ}, b ∈ T ↾ A_{<δ}, by ≺′-minimality of a_{δ} b ∉ (T ↾ A_{<δ}) \ A_{<δ}, b ∈ A_{<δ}. Let κ be an admissible ordinal such that F ∈ L_{κ} (if F is primitive recursively represented, κ can be chosen as ω_{1}^{ck}). If A_{<κ} were now increasing, then A_{<κ} = {a ∈ T | a ≺ a_{κ+1}} would be a well-ordering, which is an element of L_{κ} and has order type κ, a contradiction. Therefore there exists a least γ < κ such that A_{<γ} is not increasing. γ = γ_{0} + 1, A_{<γ_{0}} is increasing, therefore a well-ordered subset of T. T ↾ A_{<γ_{0}} ⊆ A_{<γ_{0}}, therefore by induction on length(a) follows for all a ∈ T a ∈ A_{<γ_{0}}, A_{<γ_{0}} = T and the assertion. (b): by the proof of (a). (c): The formalization is straight-forward, the only difficulty is the argument referring to κ, which we replace by the following: Let C := {γ ∈ Ord | A_{<γ} increasing }, C ⊑ Ord, f : C → T, f(α) := a_{α}. f[C] is a well-ordered initial segment of T. Assume f[C] ≠ T. Then (T ↾ f[C]) ⊈ f[C], let a ∈ (T ↾ f[C]) \ f[C] be ≺′ minimal. (Here we use reducibility of transfinite induction). As in the argument before follows a is the least element of T not in f[C], therefore f[C] = {b ∈ T | b ≺ a}, a set, f : Ord → f[C] bijective, f^{−1} : f[C] → Ord bijective, therefore Ord = f^{−1}[f[C]] is a set, a contradiction. Therefore f[C] = T is well-ordered. ⊓ ⊔

Theorem 2.3 The order type of elementary ordinal systems is less than the Bachmann-Howard ordinal.

Proof: by Lemma 2.2 (c) and since |KPω| is the Bachmann-Howard ordinal. ⊓ ⊔

2.4 Constructive Well-ordering Proof

We regard the above well-ordering proof as rather intuitive. However, for treating intuitionistic theories we will need a constructive argument as well. This argument will as well be shorter and can be formulated for instance in intuitionistic ID_{1} or type theory having the accessible part or one unnested W-type, which yields again the upper bound Bachmann-Howard for the order type of elementary OS.

Constructive well-ordering proof: Let Acc := Acc_{≺}(T) and Acc′ := k^{−1}(Acc), which is well-ordered w.r.t. ≺′. We show ∀t ∈ Acc′.t ∈ Acc by induction on t ∈ Acc′. It suffices to show ∀s ≺ t.s ∈ Acc by side-induction on length(s). If s ⪯ k(t), then s ∈ Acc since k(t) ⊆ Acc. Otherwise s ≺′ t, k(s) ≺ s ≺ t. By side-IH k(s) ⊆ Acc and by main-IH therefore s ∈ Acc and we are done. Now follows by induction on length(s) ∀s ∈ T.s ∈ Acc, T is well-ordered.

2.5 Ordinal Function Generators.

We are going to define elementary ordinal systems, which exhaust the strength of this concept. As in the introduction, we want to get functions, which act on ordinals as well. This does not require much extra work. As we said there, one can easily develop this without any reference to ordinals. The advantage of our approach is that we will get definitions for the usual ordinal functions like +, λα.ω^{α}, φ and the Schütte Klammer symbols and further new definitions for extensions of the Klammer symbols without much extra work.

There are typically two kinds of ordinal functions usually used: Versions having fixed points and fixed point free versions. One example is the Veblen function versus its fixed point free version (see for instance the function ψ in [Sch77], p. 84). When using versions with fixed points, we will usually not have the property, that the arguments of an ordinal functions are strictly smaller than the value of it. This is no harm, since in a next step one selects normal forms. The following definition allows to introduce both fixed point versions and fixed point free versions:

Definition 2.4 (a) An ordinal function generator, in short OFG is a quadruple O := (Arg, k, l, <′), where Arg is a class (in set theory), k, l : Arg →_{ω} Ord such that ∀a ∈ Arg.l(a) ⊆ k(a) and <′ is a well-ordered relation on Arg. We define <′_{O}:=<′.

(b) If O is as above, we define by recursion on a ∈ Arg simultaneously sets C_{O}(a) := C(a) ⊆ Ord and eval_{O}(a) := eval(a) ∈ Ord: C(a) := ⋃_{n<ω} C^{n}(a), where C^{0}(a) := (⋃ k(a)) ∪ l(a), C^{n+1}(a) := C^{n}(a) ∪ {eval(b) | b ∈ Arg, b <′ a, k(b) ⊆ C^{n}(a)}. eval(a) := min{α ∈ Ord | α ∉ C(a)}.

(c) Define for O as above, NF := {a ∈ Arg | k(a) < eval(a)}.

(d) Define for O as above Cl ⊆ NF inductively by: If a ∈ NF, k(a) ⊆ eval[Cl], then a ∈ Cl. Arg[Cl] := {a ∈ Arg | k(a) ⊆ eval[Cl]}. Note that Cl ⊆ Arg[Cl]. Assuming eval ↾ NF is injective, which will be shown later, we define k^{0} : Arg[Cl] →_{ω} Cl and length : Arg[Cl] → ℕ by k^{0}(a) := eval^{−1}[k(a)] ∩ Cl, length(a) := max(length[k^{0}(a)] ∪ {−1}) + 1 for a ∈ Arg[Cl] with −1 < n for n ∈ ℕ, −1 + 1 := 0. Further let for a, b ∈ Arg[Cl] a ≺ b :⇔ eval(a) < eval(b).

Note that the definition of eval(a) expresses something similar as for OS: When defining eval(a), we know all α < eval(a), since α < k(a), α ≤ l(a), or α was introduced before a, i.e. α = eval(b) for some b <′ a. Further, if a is in normal form, then a is a notation for eval(a) referring to smaller ordinals only, namely k(a).

Lemma and Definition 2.5 Let O be as above.

(a) C(a) is the least set such that (⋃ k(a)) ∪ l(a) ⊆ C(a) and, if b ∈ NF, b <′ a, k(b) ⊆ C(a), then eval(b) ∈ C(a).

(b) ∀a ∈ Arg(k(a) ≤ eval(a) ∧ l(a) < eval(a)).

(c) C(a) is an initial segment of Ord.

(d) eval restricted to NF is injective.

(e) eval[Cl] is an initial segment of Ord.

(f) For a, b ∈ Arg[Cl] it follows

eval(a) < eval(b) ⇔ (a <′ b ∧ k(a) < eval(b)) ∨ eval(a) < k(b) ∨ eval(a) ≤ l(b)
eval(a) = eval(b) ⇔ (a <′ b ∧ eval(b) = max(k(a)) ∧ eval(b) ∉ l(a)) ∨
(b <′ a ∧ eval(a) = max(k(b)) ∧ eval(a) ∉ l(b)) ∨
a = b

(g) For a, b ∈ NF we have eval(a) < eval(b) ⇔ (a <′ b ∧ k(a) < eval(b)) ∨ eval(a) ≤ k(b).

(h) F := (Cl, ≺, <′, k^{0}, length) is an ordinal system. We will call any OS-structure isomorphic to F an ordinal system based on O.

Proof: (a), (b): easy.

(c) Note that, if C(a) is an initial segment, eval(a) = C(a). Proof of the assertion by induction on a. We show ∀α ∈ C(a).α ⊆ C(a) by induction on the definition of C(a). If α ∈ ⋃ k(a), then α ⊆ C(a). If α ∈ l(a) ⊆ k(a), α ⊆ ⋃ k(a) ⊆ C(a). If α = eval(b), b <′ a, k(b) ⊆ C(a), by side-IH ⋃ k(b) ⊆ C(a), and by transitivity of <′ and l(a) ⊆ k(a) follows easily C(b) ⊆ C(a) and by main IH α = C(b) ⊆ C(a).

(d) Assume a ≠ b, a, b ∈ NF, eval(a) = eval(b). By linearity of <′, a <′ b or b <′ a, so w.l.o.g. a <′ b. k(a) < eval(a) = eval(b), therefore k(a) ⊆ C(b), a <′ b, therefore eval(a) ∈ C(b) = eval(b), a contradiction.

(e) We show ∀a ∈ Cl.eval(a) ⊆ eval[Cl] by induction on a ∈ Cl: Using IH, (a) and ¬NF(b) → eval(b) ∈ k(b) it follows C(a) ⊆ eval[Cl], eval(a) ⊆ eval[Cl].

(f) First formula “⇐”: eval(a) ∈ C(b) = eval(b). Second formula “⇐” consider only the case (a <′ b ∧ eval(b) = max(k(a)) ∧ eval(b) ∉ l(a)). eval(b) ∈ k(a) ≤ eval(a). Assume eval(b) < eval(a). Then, since eval(b) ≮ k(a), eval(b) ≰ l(a), by eval(b) ∈ C(a) it follows eval(b) = eval(b′) for some b′ <′ a, k(b′) ⊆ C(a). By the definition of C(a) and eval(b) ∈ C(a) \ C^{0}(a) there exists b′ <′ a and n such that k(b′) ⊆ C^{n}(a), eval(b′) ∈ C^{n+1}(a) \ C^{n}(a) and eval(b′) = eval(b). b′ <′ b, eval(b′) = eval(b), so k(b′) ≮ eval(b) = eval(b′), eval(b′) ∈ k(b′), contradicting the choice of b′. Therefore eval(b) = eval(a). “⇒” first formula: if the right hand side is false the right hand holds for eval(a) = eval(b) or eval(b) < eval(a), therefore the left hand side is false. For the second formula “⇒” follows in the same way.

(g) “⇐” is immediate, and “⇒” follows as before.

(h) (OS 1), (OS 2), (OS 4) are clear. (OS 3): If s ≺ t, s, t ∈ NF, then eval(s) ∈ C(t), eval(s) ≤ k(t) or s <′ t and the assertion. ⊓ ⊔

Definition 2.6 If O_{i} = (Arg_{i}, <′_{i}, k^{i}, l^{i}) are OFG (i = 0, 1), Arg_{0} ∩ Arg_{1} = ∅, Let O_{0} ◯ ≺ O_{1} := (Arg, <′, k, l), be defined by (Arg, <′) := (Arg_{0}, <′_{0}) ◯ ≺ (Arg_{1}, <′_{1}) and k(r) := k^{i}(r), l(r) := l^{i}(r) for r ∈ Arg_{i}. O_{0} ◯ ≺ O_{1} is obviously an OFG and eval_{O}(a) = eval_{O_{0}}(a) for a ∈ Arg_{O_{0}}.

Example 2.7 (a) Let α ∈ Ord be fixed, (Arg_{α}, <′_{α}) := α\underline{+}Ord (i.e. expanding Definition 1.1 (d), Arg_{α} = \{α\underline{+}β | β ∈ Ord\}, α\underline{+}β <′_{α} α\underline{+}γ ⇔ β < γ; here and in the following α\underline{+}β, \underline{φ}_{α}β etc. are formal terms defined from ordinals α, β, etc. coded

in set theory in some way). Let k(α\underline{+}β) := \{α, β\}, l(α\underline{+}β) := \begin{cases}∅ & if β = 0, \\ \{α\} & otherwise, \end{cases}

O_{α} := (Arg_{α}, <′_{α}, k, l). Then eval(α\underline{+}β) = α + β. Note that Cl = ∅.

(We could change the definition of OFGs by omitting the condition “<′ linear”. Then Lemma 2.5 (a) - (c) and (e) go through as well and one could define (Arg, <′) as the union of (Arg_{α}, <′_{α}) with α\underline{+}β and γ\underline{+}ρ incomparable for α ≠ γ. eval(α\underline{+}β) = α+β, so this way we would get a definition of the full function +.)

(b) Let (Arg, <) := \underline{Σ}(𝔸_{weakdes}), k(\underline{Σ}(α_{1}, …, α_{m})) := \{α_{1}, …, α_{m}\}, l(\underline{Σ}(α_{1}, …, α_{m}))

:= \begin{cases}\{α_{1}\} & if m > 1, \\ ∅ & otherwise. \end{cases} Let O_{+,w} be the resulting OFG. Then one easily verifies

eval(\underline{Σ}()) = 0 (similar cases occurring in future examples will not be mentioned below) eval(\underline{Σ}(α_{1}, …, α_{m})) = α_{1} + ⋯ + α_{m} for m > 0. The fixed point free version of it, i.e. l(t) := k(t) yields the same result, except eval(\underline{Σ}(α, \underbrace{1, …, 1}_{l})) = α + l + 1

(c) Let (Arg, <) := \underline{Σ}′(Schütte(𝔸, ω \ \{0\})), k(\underline{Σ}′(α_{1}, n_{1}, …, α_{m}, n_{m})) := \{α_{1}, …, α_{m}, n_{1}, …, n_{m−1}, n_{m} − 1\},

l(\underline{Σ}′(α_{1}, n_{1}, …, α_{m}, n_{m})) := \begin{cases}\{α_{1}, n_{m} − 1\} & if m > 1 or n_{m} > 1, \\ ∅ & otherwise. \end{cases}

Let O_{+} be the resulting OFG. eval_{O_{+}}(\underline{Σ}′(α_{1}, n_{1}, …, α_{m}, n_{m})) = (α_{1} · n_{1}) + ⋯ + (α_{m} · n_{m}).

(d) If we replace in (b), (c) 𝔸 by Ord and \underline{Σ} by CNF, we obtain ordinal function generators O_{CNF,w}, O_{CNF} for the Cantor normal form, i.e. eval_{O_{CNF,w}}(CNF(α_{1}, …, α_{m})) = ω^{α_{1}} + ⋯ + ω^{α_{m}} and eval_{O_{CNF}}(CNF′(α_{1}, n_{1}, …, α_{m}, n_{m})) = ω^{α_{1}} · n_{1} + ⋯ + ω^{α_{m}} · n_{m}

(e) Let O_{0} be O_{+,w} or O_{+}, O_{1} := (\underline{ω}^{Ord}, k, l) with k(\underline{ω}^{α}) := \{α\}, l(\underline{ω}^{α}) := ∅, O := O_{0} ◯ ≺ O_{1}, then eval(\underline{ω}^{α}) = ω^{α}. The fixed point free version (l(\underline{ω}^{α}) := \{α\}) yields the same result, except eval(\underline{ω}^{α+n}) = ω^{α+n+1} for epsilon numbers α.

(f) Let O_{0} be O_{+,w} or O_{+}, O_{1} := (\underline{φ}_{Ord}Ord, k, l), k(\underline{φ}_{α}β) := \{α, β\},

l(\underline{φ}_{α}β) := \begin{cases}\{α\} & if β > 0, \\ ∅ & otherwise, \end{cases} O := O_{0} ◯ ≺ O_{1}. Then eval(\underline{φ}_{α}β) = φ_{α}β, where φ is the

Veblen function with φ_{0}β := ω^{β}. If we use the OFG from (d) or (e) instead for O_{0} we obtain the φ-function starting with φ_{0}α := ϵ_{α}, and defining l(t) := k(t) yields the fixed point free version of the Veblen function.

(g) Let O_{0} be O_{+,w} or O_{+}, O_{1} := \underline{φ}(Schütte\binom{Ord\\{0\}}{Ord}). If A = \binom{β_{1}···β_{m}}{α_{1}···α_{m}}, define k(\underline{φ}(A)) := \{β_{1}, …, β_{m}, α_{1}, …, α_{m}\} and

l(\underline{φ}(A)) := \{β_{1}, …, β_{m−1}, α_{1}, …, α_{m−1}\} ∪ \begin{cases}\{α_{m}\} & if β_{m} > 1, \\ ∅ & otherwise, \end{cases}

O := O_{0} ◯ ≺ O_{1}. As in [Sch54] we allow addition of columns \binom{0}{α} and identify matrices which differ in such columns only. If A = \binom{β_{1}···β_{m}}{α_{1}···α_{m}}, (A, β_{m+1}, α_{m+1}) := \binom{β_{1}···β_{m}β_{m+1}}{α_{1}···α_{m}α_{m+1}}, (A, β_{m+1}, α_{m+1}, β_{m+2}, α_{m+2}) etc. are defined similarly. Then eval(\underline{φ}(A)) = φ(A), where φ(A) is defined as in [Sch54], based on φ(α) := ω^{α}, but with reversed order of the columns. We prove this by induction on <′_{O}: If A = \underline{φ}(α, 0), then we can easily show eval(A) = ω^{α} = φ(α, 0). If A = \underline{φ}(B, α, β, γ, 0), then it follows that C(\underline{φ}(A)) is closed under +, λδ.eval(\underline{φ}(B, α^{∗}, β, δ, β^{∗})) for α^{∗} < α, β^{∗} < β and contains further eval(\underline{φ}(B, α, β, γ^{∗}, 0)) for γ^{∗} < γ, therefore using the IH eval(\underline{φ}(B, α, β, γ, 0)) ≥ φ(B, α, β, γ, 0). On the other hand, φ(A) ≥ k(\underline{φ}(A)), φ(A) > l(\underline{φ}(A)), and, if B <′ A, k(\underline{φ}(B)) < φ(A), by the calculations in [Sch54] φ(B) < φ(A), therefore using the IH ∀γ ∈ C(\underline{φ}(A))(γ < φ(A)), φ(A) ≥ eval(\underline{φ}(A)).

(h) If we define in (g) l(\underline{φ}(A)) := k(\underline{φ}(A)), we obtain a fixed point free version of the Klammer symbols or equivalently eval(\underline{φ}\binom{β_{1}···β_{m}}{α_{1}···α_{m}}) = ϑ(Ω^{α_{1}}β_{1} + ⋯ + Ω^{α_{m}}β_{m}), where ϑ is defined as in [RW93], but without closing C(α, β) under λγ.ω^{γ}. (We obtain the original ϑ function, if we take as O_{0} the OFG for CNF). See [Sei94] for details. If we restricting the definition to those α_{i}, β_{i} such that for γ := Ω^{α_{1}}β_{1} + ⋯ + Ω^{α_{m}}β_{m} γ ∈ C(γ), where C(γ) is defined as for the ordinary ψ-function, then we will get the same result, but with ϑ replaced by the ψ-function (ψ = ψ_{0} as in [Buc86] or ψ = ψ_{Ω_{1}} as in [Buc92], however with C(α, β) not closed under φ). Note that this restriction has the effect that ≺′ and ≺ coincide in the corresponding OS for terms of the form \underline{φ}(a).

(i) Let S_{0} := Ord, S_{n+1} := Schütte\binom{Ord\\{0\}}{S_{n}}, k_{0}^{i} : S_{i} →_{ω} Ord, k_{0}^{0}(α) := \{α\}, k_{0}^{i+1}\binom{β_{1}···β_{m}}{A_{1}···A_{m}} := \{β_{1}, …, β_{m}\} ∪ ⋃_{j=1}^{m} k_{0}^{i}(A_{j}). Let k^{i}(\underline{φ}(A)) := k_{0}^{i}(A), O_{1}^{i} := (\underline{φ}(S_{i}), k^{i}, k^{i}), O^{i} := O_{0} ◯ ≺ O_{1} (O_{0} as before). We obtain, what we can call the “fixed point free version of extended Schütte Klammer symbols”. Let f_{i} : S_{i} → Ord, f_{0}(α) := α, f_{i+1}\binom{β_{1}···β_{m}}{A_{1}···A_{m}} := Ω^{f_{i}(A_{1})}β_{1} + ⋯ + Ω^{f_{i}(A_{m})}β_{m}, then one can easily see eval_{O^{i}}(\underline{φ}(A)) = ϑ(f_{i}(A)), ϑ as in (h). Applying a similar restriction as in (h) yields

the ψ-function restricted to ordinals < \underbrace{Ω^{Ω^{^{···}^{Ω}}}}_{i times}.

(j) As in (g) and (h), we can define a version of the extended Schütte Klammer symbols with fixed points. The verifications takes more space than is available here. In some sense we believe however that in the context of OS, the fixed point free versions are at least as natural or even more natural than the versions with fixed points.

(k) Let O^{i} be as in (i). The union of O^{i} can be described as follows: Let S′_{−1} := {0}, S′_{0} := Ord, S′_{n+1} := S′_{n} ◯ ≺ (Schütte\binom{Ord\\{0\}}{S′_{n}} \ |Schütte\binom{Ord\\{0\}}{S′_{n−1}}|), k_{0}^{i} : S′_{i} →_{ω} Ord,

k_{0}^{0}(α) := {α}, k_{0}^{i+1}(A) = k_{0}^{i}(A) for A ∈ S′_{i}, k_{0}^{i+1}(A) is defined as in (i) for A ∈ S′_{i+1} \ S′_{i}. Let |S′| := ⋃_{i<ω} |S′_{i}|, ≺_{S′}:= ⋃_{i<ω} ≺_{S′_{i}}, k^{i}(\underline{φ}(A)) := k_{0}^{i}(A), k := ⋃ k^{i}, O := O_{0} ◯ ≺ (\underline{φ}(S′), k, k), which is an OFG. Define ι_{i} : |\underline{φ}(S_{i})| → |\underline{φ}(S′_{i})| by ι_{0}(\underline{φ}(α)) := α, ι_{1}(\underline{φ}()) := \underline{φ}(0), ι_{1}(\underline{φ}\binom{α}{0}) := \underline{φ}(α), ι_{1}(a) := a otherwise, ι_{i+2}(a) := ι_{i+1}(a) for a ∈ \underline{φ}(S_{i+1}), ι_{i+2}(\underline{φ}\binom{β_{1}···β_{m}}{A_{1}···A_{m}}) := \underline{φ}\binom{β_{1}···β_{m}}{ι_{i+1}(A_{1})···ι_{i+1}(A_{m})} otherwise. Then ι_{i} is an isomorphism from \underline{φ}(S_{i}) to \underline{φ}(S′_{i}), \underline{φ}(S′_{0}) ⊑ \underline{φ}(S′_{1}) ⊑ ⋯, the isomorphism can be extended to an isomorphism from Arg_{O^{i}} to an initial segment of Arg_{O} which preserves the component sets k_{i}. In this sense O is the union of the O_{i}.

The following lemma, which will be used in the proof of 2.9, helps to derive from an OFG an OS based on it, which is primitive recursive: One introduces a set of terms T′′, which have the syntactical form of being arguments, if we replace its components by ordinals. From these terms we select now a set T of terms and T′ of arguments based on T such that T represents all elements of Cl and T′ all elements of Arg[Cl]. Whether an element belongs to T′ or T depends now on the ordering of its components, which need to be in T and then one can show that under the assumptions formulated in the next lemma, T, T′, ≺ and ≺′ will be primitive recursive. Especially condition (e) will have some flavor of Π_{1}^{2}-logic, however, the ordering of the elements of T and whether and element of T′′ belongs to T will depend not only on the order of its components, which allows some more generality.

Lemma 2.8 Let O be an OFG as usual, and let T′′ be a primitive recursive set, T ⊆ T′ ⊆ T′′, f : T′ → Arg, k̂ : T′′ →_{ω} T′′, l̂ : T′′ →_{ω} T′′, length′ : T′′ → ℕ, all primitive recursive. Let for a, b ∈ T′, a ≺′ b :⇔ f(a) <′ f(b), a ≺ b :⇔ eval(f(a)) < eval(f(b)). Assume the following conditions:

(a) ∀a ∈ T′.l̂(a) ⊆ k̂(a) ⊆ T.

(b) ∀a ∈ T′(f[k̂(a)] = k^{0}(f(a)) ∧ f[l̂(a)] = l(f(a))).

∀a ∈ T′′.length′[k̂(a)] < length′(a).

(c) For every subset A of T f[{t ∈ T′ | k̂(t) ⊆ A}] = {a ∈ Arg | k(a) ⊆ eval[f[A]]}.

(d) If A ⊆ T′, f ↾ A is injective, then f ↾ {t ∈ T′ | k̂(t) ⊆ A} is injective.

(e) For a, b ∈ T′′ such that k̂(a) ∪ k̂(b) ⊆ T we can determine from ≺ restricted to k̂(a) ∪ k̂(b) (coded as a finite list which is coded as a natural number) in a primitive recursive way, whether a, b ∈ T′ and, if this is the case, whether a ≺′ b.

(f) a ∈ T ⇔ a ∈ T′ ∧ f(a) ∈ NF ∧ k̂(a) ⊆ T.

Then T, T′, ≺′, ≺, are primitive recursive, we can define { \atop length} : T′ →_{ω} T such that { \atop length}(a) = length(f(a)) for a ∈ T′, and (T, ≺, ≺′, k̂, { \atop length}) is an OS based on O.

Proof: We determine for t ∈ T′′ whether t ∈ T′, t ∈ T and for r, s ∈ T′ such that length′(r), length′(s) ≤ length′(t) whether r ≺′ s and whether r ≺ s holds by recursion on length′(t) and side-recursion on length′(r) + length′(s): If k̂(t) ⊈ T, t ∉ T′. Otherwise we can decide whether t ∈ T′. Assume now r, s as above. Whether r ≺′ s follows from the induction hypothesis and then using Lemma 2.5 (f) we can determine whether r ≺ s holds. Now t ∈ T :⇔ t ∈ T′ ∧ k̂(t) ≺ t. f : T → Arg is injective by condition (d). f[T] ⊆ NF, f[T] ⊆ Cl. We show f[T] = Cl. It suffices to show ∀a ∈ Cl.∃b ∈ T.f(b) = a. Induction on a. k̂(a) ⊆ f[T]. Therefore there exists a t ∈ T′, k̂(t) ⊆ T, such that f(t) = a. Since NF(a), follows t ∈ T. { \atop length}(t) is defined now by { \atop length}(t) := max({ \atop length}[k̂(t)] ∪ \{−1\}) + 1. ⊓ ⊔

Lemma 2.9 For all the OFG in the Example 2.7 (a) - (i), except for those examples involving the lexicographic ordering on weakly descending sequences ((b) and the examples referring to it) there exists an elementary OS represented by them.

Remark 2.10 Note that the development of the OS can be done without having to refer to ordinals.

Proof of Lemma 2.9: First, using Lemma 2.8 we can define a primitive recursively represented OS based on the OFG. We look only at the example (g) in detail: Let \underline{0} := \underline{Σ}′(), \underline{l + 1} := \underline{Σ}′(\underline{0}, \underline{l}\underline{+}1), \underline{ℕ} := \{\underline{l} | l ∈ ω\}. Define T′′ together with k̂ : T′′ →_{ω} T′′, l̂ : T′′ →_{ω} T′′, length(T′′) → ℕ recursively by: If m ∈ ω, a_{i} ∈ T′′, b_{i} ∈ \underline{ℕ}, b_{i} ≠ \underline{0} for i < m, then t_{0} := \underline{Σ}′(a_{1}, b_{1}, …, a_{m−1}, b_{m−1}, a_{m}, b_{m}\underline{+}1) ∈ T′′,

k̂(t_{0}) := \{a_{1}, b_{1}, …, a_{m}, b_{m}\}, l̂(t_{0}) := \begin{cases}\{a_{1}, b_{m}\} & if m > 1 or b_{m} ≠ \underline{0}, \\ ∅ & otherwise, \end{cases}

length(t_{0}) := max{length(a_{1}), …, length(a_{m}), length(b_{1}), …, length(b_{m})} + 1. If a_{1}, …, a_{m}, b_{1}, …, b_{m} ∈ T′′, a_{1}, …, a_{m} ≠ \underline{0}, t_{1} := \underline{φ}\binom{a_{1}···a_{m}}{b_{1}···b_{m}} ∈ T′′, and we define k̂(t_{1}), l̂(t_{1}) by translating the conditions from Example 2.7 (g) and length(t_{1}) as before. T′′, length, k̂, l̂ are primitive recursive. Define T ⊆ T′′, T′ ⊆ T′′, together with f : T′ → Arg inductively by: If t_{0} is as above, k̂(t_{0}) ⊆ T, eval(f(a_{1})) > ⋯ > eval(f(a_{m})), then t_{0} ∈ T′, f(t_{0}) := \underline{Σ}′(eval(f(a_{1})), eval(f(b_{1})), …, eval(f(a_{m−1})), eval(f(b_{m−1})),

eval(f(a_{m})), eval(f(b_{m})) + 1).

If t_{1} is as above, eval(f(b_{1})) > ⋯ > eval(f(b_{m})), then t_{1} ∈ T′, f(t_{1}) := \underline{φ}\binom{eval(f(a_{1}))···eval(f(a_{m}))}{eval(f(b_{1}))···eval(f(b_{m}))}. Further t ∈ T :⇔ t ∈ T′ ∧ NF(f(t)). The conditions of Lemma 2.8 are now fulfilled and therefore most conditions of a primitive recursively represented OS are fulfilled, what is missing is verified easily.

The other OS are treated similarly. The constructions of new orderings considered in [Set98a] Lemma 3.5 (especially the lexicographic ordering on pairs and and strictly descending sequences) yield orderings such that transfinite induction over it reduces to transfinite induction over the underlying orderings in PRA and therefore we get actually get in all cases elementary OS. ⊓ ⊔

However, transfinite induction over weakly descending sequences reduces only in HA to the underlying ordering, so the examples where we used weakly descending sequences do not yield elementary OS.

Theorem 2.11 (a) The bound in Theorem 2.3 is sharp: The supremum of the order types of elementary OS is exactly the Bachmann-Howard ordinal.

(b) The limit of the order type of ordinal systems from below as introduced in [Set98a] is the Bachmann-Howard ordinal.

Proof: (a): Example 2.7 (i) yields OS of strength ϑ(\underbrace{Ω^{Ω^{^{···}^{Ω}}}}_{i times}), which in the limit reaches the

Bachmann-Howard ordinal. (b): by subsection 2.2, (a) and the upper bound developed in the last two sections of [Set98a]. ⊓ ⊔

Note that the construction in the example used in (a) really exhausts the full strength of elementary OS: In the OS related to O_{i} ≺′ is built from ≺ using i-times nested lexicographic ordering on descending sequences, TI over which reduces to the underlying ordering by using formulas of increasing length. The union of the O_{i}, O′ yields an OFG, such that in the OS belonging to it TI over ≺′ does no longer reduce to TI over ≺ in PRA, so it is no longer elementary. What is required are twice iterated ordinal systems.

3 n-times Iterated Ordinal Systems

3.1 Introduction

The usual way of getting beyond the Bachmann-Howard ordinal is to violate condition (OS 1), which was the basis for our analysis in the last two sections of [Set98a]. However, the foundationally more interesting approach seems to keep the condition that the ordinals are built from below and instead weaken the requirement that TI over ≺′ reduces to TI over ≺ in an elementary way, namely in PRA.

If we look at the OS corresponding to Example 2.7 (k) we can see that we generated by meta recursion a sequence of matrices of increasing complexity. We can replace this meta recursion by using a second OS: Let F_{0} := (T_{0}, ≺, ≺′, k, length) be the primitive recursive (but non-elementary) OS based on O, defined by the method used in Lemma 2.9. Let T_{1} := \{A | \underline{φ}(A) ∈ T_{0}\} with the ordering A ≺_{1} A′ :⇔ \underline{φ}(A) ≺′ \underline{φ}(A′). Define k_{0,j} : T_{0} →_{ω} T_{j} for i, j = 0, 1 by: k_{0,0} := k, k_{0,1}(\underline{Σ}′(a⃗)) := ∅, k_{0,1}(\underline{φ}(A)) := \{A\} and let for D ⊆ T_{0}, E ⊆ T_{i}, D ↾_{0,j} E := k_{0,j}^{−1}(E). Then if B ⊆ T_{0}, C ⊆ T_{1} are wellordered w.r.t. ≺, ≺_{1}, then (T_{0} ↾_{0,0} B) ↾_{0,1} C is well-ordered. If we take as C the set of matrices built from notations in B only and, if we know that C is well-ordered, then T_{0} ↾_{0,0} B = (T_{0} ↾_{0,0} B) ↾_{0,1} C is well-ordered, and we have shown that F_{0} is an OS.

Now in order to show that C is an well-ordered we use a second OS: Define k_{1,i} : T_{1} →_{ω} T_{i} by: if a ∈ T_{0}, k_{1,0}(a) := \{a\}, k_{1,1}(a) := ∅, and if A = \binom{a_{1}···a_{m}}{A_{1}···A_{n}}, then k_{1,0}(A) := {a_{1}, …, a_{n}} ∪ ⋃_{j=1}^{m} k_{1,0}(A_{j}), k_{1,1}(A) := {A_{1}, …, A_{m}} and define C ↾_{1,j} D as before. Let F_{1} := (T_{1}, k_{1,1}, ≺′, ≺′, length). and for B ⊆ T_{0} F_{1}[B] := (T_{1} ↾_{1,0} B, ≺_{1}, ≺_{1}, k_{1,1}, length). If B is ≺-well-ordered, then F_{1}[B] is now an ordinal system, and therefore C := T_{1} ↾_{1,0} B is well-ordered and with this C the above holds.

F_{1} is a system which internalizes what was before meta-induction. It is a relatively weak OS which is the relativized extension of the OS for the Cantor normal form. Expanding the OS we introduced in the last section we can get now more complex “matrices”, which can be used by the first OS. As before, we will exhaust the strength of this concept (which will be called 2-OS) by using the hierarchy of extended Klammer symbols. In order to go beyond this, we can iterate the step from OS to 2-OS once more and yield 3-OS, 4-OS etc. We are going to formalize in the following n-OS for arbitrary natural numbers n.

3.2 n-Ordinal Systems

In the example before we had as basic structures two ordinal structures F_{j} := (T_{j}, ≺_{j}, ≺′_{j}, k_{j,j}, length_{j}) (j = 0, 1) together with functions k_{i,1−i} : T_{i} →_{ω} T_{1−i}. It can be visualized as follows:

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (T_{1}, <′_{1})  (T_{2}, <′_{2}) (T_{1}, <_{1})  (T_{2}, <_{2}) t  r s t  u v k_{1,1}  k_{1,2} k_{1,1}(t) = {r, s} k_{1,2}(t) = {u, v}

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} (T_{1}, <′_{1})  (T_{2}, <′_{2}) (T_{1}, <_{1}) k_{2,1}(w) = {r, s} k_{2,2}(w) = {u, v}  (T_{2}, <_{2}) w r  s  u v  w k_{2,2} k_{2,1}

For simplicity assume T_{0} ∩ T_{1} = ∅ and write ≺, ≺′, length instead of ≺_{j}, ≺′_{j}, length_{j} and write ↾_{j} instead of ↾_{i,j} as defined before.

In the example F_{j} fulfilled all conditions of an OS except (OS 4). We used that, if A ⊆ T_{0}, B ⊆ T_{1} are well-ordered, then (T_{0} ↾_{0} A) ↾_{1} B is ≺′-well-ordered. In order to have that F_{1}[A] is an OS, we need as well that under the same conditions for A, B (T_{1} ↾_{0} A) ↾_{1} B is well-ordered. Further we needed that (T_{0} ↾_{0} A) ↾_{1} (T_{1} ↾_{0} A) = T_{0} ↾_{0} A for all A ⊆ T_{0}. Only ⊇ needs to be fulfilled, which is equivalent to k_{1,0}[k_{0,1}(a)] ⊆ k_{0,0}(a).

In order to get that F_{1}[A] is an OS-structure, we need k_{1,1} : T_{1} ↾_{0} A →_{ω} T_{1} ↾_{0} A for all A ⊆ T_{0}, i. e. k_{1,0}[k_{1,1}(a)] ⊆ k_{1,0}(a). The generalization to n-ordinal systems is now straight-forward and we get the following definition:

Definition 3.1 (a) An n-times iterated Ordinal-System-structure, in short n-OS-struc-

ture is a triple F = ((G_{i})_{i<n}, (k_{i,j})_{i,j<n}, (length_{i})_{i<n}) such that F_{i} :=

(G_{i}, k_{i,i}, length_{i}) are OS-structures and k_{i,j} : T_{i} →_{ω} T_{j} (i, j < n).

In the following, when introduced as an n-OS, F will be always as above (where n

can be replaced by any natural number), F_{i} = (G_{i}, k_{i,i}), G_{i} = (T_{i}, ≺_{i}, ≺′_{i}) and and

we will usually write ((G_{i}), (k_{i,j}), length_{i}) instead of ((G_{i})_{i<n}, (k_{i,j})_{i,j<n}). Further we

assume T_{i} are always disjoint and write ≺, ≺′, length instead of ≺_{i}, ≺′_{i}, length_{i}.

(b) If F is an n-OS-structure as above, A ⊆ T_{i}, B ⊆ T_{j}, A ↾_{j} B := A ∩ k_{i,j}^{−1}[B].

If B_{j} ⊆ T_{j}, then A ↾_{j=l}^{m} B_{j} := A ∩ ⋂_{j=l}^{m} k_{i,j}^{−1}[B_{j}]. We write ↾_{i<j}, ↾_{i≤j} for ↾_{i=0}^{j−1}

and ↾_{i=0}^{j}. If F is an n + 1-OS-structure and A ⊆ T_{0}, then F[A] := ((T_{i+1} ↾_{0} A,

≺_{i+1}, ≺′_{i+1})_{i<n−1}, (k_{i+1,j′+1})_{i,j′<n−1}, (length_{i+1})_{i<n−1})). (More precisely we have

to restrict ≺_{i+1}, ≺′_{i+1}, k_{i+1,j′+1} and length_{i+1} to T_{i+1} ↾_{0} A.)

(c) An n-OS-structure F is an n-times iterated Ordinal System, in short n-OS, if for all i, j, l < n the following holds (n − OS 1) F_{i} fulfill (OS 1), (OS 2) and (OS 3); (n − OS 2) if l < j, i, j < n, then k_{j,l} ∘ k_{i,j} ⊆ k_{i,l}; (n − OS 3) if A_{i} ⊆ T_{i} are ≺-well-ordered (i < n), l < n, then T_{l} ↾_{i<n} A_{i} is ≺′-well-

ordered.

(d) An n-OS F is well-ordered, if (T_{0}, ≺) is, and its order type is that of (T_{0}, ≺). It is primitive recursive, if the involved sets are primitive recursive subsets of the natural numbers, all functions, relations are primitive recursive and all properties except of the well-ordering condition can be shown in primitive recursive arithmetic. It is elementary, if additionally the well-ordering condition follows in PRA in the sense of reducibility of transfinite induction in PRA.

(e) Two n-OS are isomorphic, if there is are bijections between the underlying sets, which respect k_{i,j}, length_{i}, ≺_{i}, ≺′_{i} for all i, j < n.

We will need the following auxiliary definition:

Definition 3.2 (a) A relativized n-OS is a triple (F, T_{−1}, ≺, (k_{i,−1})_{0≤i<n}) such that F is an n-OS structure, (T_{−1}, ≺) is a linearly ordered set, k_{i,−1} : T_{i} →_{ω} T_{−1}, for j > −1 k_{j,−1} ∘ k_{i,j} ⊆ k_{i,−1} and such that F fulfills the conditions of an n-OS except for condition(n − OS 3), which is replaced by: if A_{i} ⊆ T_{i} are ≺-well-ordered (−1 ≤ i < n), then T_{l} ↾_{i=−1}^{n−1} A_{i} is ≺′-well-ordered (0 ≤ l < n).

(b) If (F, T_{−1}, k_{i,−1}) is a relativized n-OS, A ⊆ T_{−1}, then F[A]_{−1} is the relativization of F to A defined in a straightforward way.

Well-ordering of a n + 1-OS reduces to the well-ordering of an n-OS as follows:

Lemma 3.3 Assume F is an n + 1-OS-structure.

(a) If A ⊆ T_{0} and F fulfills ((n + 1) − OS 2), then F[A] is an n-OS-structure which fulfills (n − OS 2).

(b) If F is an n + 1-OS and A ⊆ T_{0} is ≺-well-ordered, then F[A] is an n-OS.

(c) If F is an 1-OS, then F is an OS.

(d) n-OS are well-ordered.

(e) For elementary n-OS, (d) can be shown in KPω extended by the existence of n − 1 admissible sets x_{1}, …, x_{n−1} such that x_{1} ∈ x_{2} ∈ ⋯ ∈ x_{n−1}.

Proof: (a) We need only to show that k_{i+1,j+1} : T_{i+1} ↾_{0} A → T_{j+1} ↾_{0} A, which follows by k_{j+1,0}(k_{i+1,j+1}(a)) ⊆ k_{i+1,0}(a). (b) easy. (c): trivial.

(d) We show by induction on n ≥ 1: If F is an n-OS, then (T_{i}, ≺) are well-ordered for i < n. n = 1: (c) and Theorem 2.2 (a). n → n + 1: We show first F_{0} is an OS. We have only to show (OS 4). Assume A ⊆ T is ≺-well-ordered. Then F[A] is an n-OS, by IH it follows that T_{i} ↾_{0} A are well-ordered (i = 1, …, n + 1). Therefore (T_{0} ↾_{0} A) ↾_{i=1}^{n} (T_{i} ↾_{0} A) is ≺′-well-ordered. But (T_{0} ↾_{0} A) ↾_{i=1}^{n} (T_{i} ↾_{0} A) = T_{0} ↾_{0} A, since k_{i,0}(k_{0,i}(a)) ⊆ k_{0,0}(a).

(e) We show by Meta-induction on n in KPω: If (F, T_{−1}, ≺, k_{i,−1}) is a relativized n-OS, A ⊆ T_{−1} is well-ordered, and there are n−1 admissibles above {A, F, k_{i,−1}}, then T_{i} ↾_{−1} A are ≺-well-ordered. The case n = 1 follows as in Theorem 2.2 (b). In the step n → n + 1 let κ be the least admissible ordinal such that {A, F, k_{i,−1}} ∈ L_{κ}. Define a_{α} as in Lemma 2.2 (c) for α ≤ κ. This can be done, by the same argument as in (d), using that F[A]_{−1}[B] is an n-OS for B ⊆ T_{0} ≺-well-ordered and that therefore, if B ∈ L_{κ^{+}}, (T_{i} ↾_{−1} A) ↾_{0} B are well-ordered (i = 1, …, n), where κ^{+} is the next admissible ordinal above κ. If we replace now in the proof of 2.2 (c) C by {α ∈ κ | A_{<α} increasing}, and the argument that there is no bijection between a set and Ord by that there is no (Δ_{0}-definable) bijection between an element of a and κ, we conclude that {a_{α} | α ∈ C} = T_{0} ↾_{−1} A, T_{0} ↾_{−1} A is well-ordered and therefore as well T_{i} ↾_{−1} A are well-ordered. ⊓ ⊔

Theorem 3.4 The strength of an n-OS (n > 0) is less than |ID_{n}| = ψ_{Ω_{1}}(ϵ_{Ω_{i}+1}) (ψ as in [Buc92]).

Proof: By Lemma 3.3 (e) and, since the strength of KPω extended by the existence of n − 1 admissibles is |ID_{n}|. ⊓ ⊔

3.3 Constructive Well-ordering Proof.

We will give now a proof of Lemma 3.3 (e) which can be formalized even in constructive theories like Martin-Löf’s type theory extended by an at most n times nested W-type or intuitionistic ID_{n}: Define inductively M_{i}, Acc_{i} ⊆ T_{i}: M_{i} := T_{i} ↾_{j<i} Acc_{j}, Acc_{i} := Acc_{≺}(M_{i}). Let Acc′_{i} := T_{i} ↾_{j<n} Acc_{j}. (Acc_{i}, ≺), (Acc′_{i}, ≺′) are well-ordered. We show by induction on n − i Acc_{i} = M_{i}. Assume i according to induction. We show ∀s ∈ Acc′_{i}.s ∈ Acc_{i} by sideinduction on (Acc′_{i}, ≺′): s ∈ M_{i}. Further ∀r ∈ M_{i}(r ≺ s → r ∈ Acc_{i}) by (side-side-)induction on length(r): Assume r according to induction, r ∈ M_{i} ∧ r ≺ s. If r ⪯ k_{i,i}(s) ⊆ Acc_{i}, it follows r ∈ Acc_{i}. Otherwise r ≺′ s. We show r ∈ Acc′_{i}. If j < i, k_{i,j}(r) ⊆ Acc_{j}. k_{i,i}(r) ≺ r ≺ s, if j < i, k_{i,j}[k_{i,i}(r)] ⊆ k_{i,j}(r) ⊆ Acc_{j}, therefore k_{i,i}(r) ⊆ M_{i} and by side-side-IH k_{i,i}(r) ⊆ Acc_{i}. For i < j < n we show by side^{3}-induction on j k_{i,j}(r) ⊆ Acc_{j}. If l < j, k_{j,l}[k_{i,j}(r)] ⊆ k_{i,l}(r) ⊆ Acc_{l} by IH, k_{i,j}(r) ⊆ M_{j}, by main-IH k_{i,j}(r) ⊆ Acc_{j}. Therefore r ∈ Acc′_{i}, r ≺′ s, by side-IH r ∈ Acc_{i}, and the side-side-induction and therefore as well the side-induction are complete. Now follows by induction on length(s) ∀s ∈ M_{i}.s ∈ Acc_{i}, Acc_{i} = M_{i} and the main induction is finished. Now it follows T_{0} = M_{0} = Acc_{0} and we are done.

3.4 n-Ordinal Function Generators

As before we are going to define the ordinal systems which exhaust the strength of elementary n-ordinal systems. As there, we want as a side result as well to get functions defined on arbitrary ordinals. Again of course this detour via ordinals is not necessary, one could define easily the n-ordinal systems purely syntactically.

We need to represent the higher ordinal systems we used as ordinals and will do it in the usual way by taking ordinals of higher number classes: Let Ω_{0} := 0, Ω_{n} := ℵ_{n}. Ordinals in [Ω_{n}, Ω_{n+1}[ can be regarded as objects referring to ordinals in [0, Ω_{n}[ and therefore be considered as representatives of the higher OS. In a refined approach one could replace Ω_{n} by the n-th admissible ordinal Ω_{n}^{rec} (starting with Ω_{1}^{rec} := ω_{1}^{ck}).

In the definition of (non-iterated) OFG we closed the sets C(a) under (k(b) ⊆ C(a)∧b <′ a) → eval(b) ∈ C(a) with no restriction on b being in normal form. But one could easily show that having the restriction of b being in normal form yields the same result, since, if b is not in normal form, eval(b) ∈ k(b). In the case of n-OFG, normal form will again mean that k(b) ⊆ C_{i}(b). However, this condition can be violated by having eval_{j}(c) ∈ k(b) such that j > i and k(c)∩[Ω_{i}, Ω_{i+1}[> eval(a). So we do no longer have a ∉ NF → eval(a) ∈ k(a) and the above argument does no longer go through. We will use the easiest way of dealing with these problems: we add only eval(c) to C(a), if NF(c) holds.

Definition 3.5 (a) An n-ordinal function generator, in short n-OFG is a quadruple O := (Arg_{i}, k_{i}, l_{i}, <′_{i})_{i<n} such that Arg_{i} are classes (in set theory), k_{i}, l_{i} : Arg_{i} →_{ω} Ord, ∀a ∈ Arg_{i}.l_{i}(a) ⊆ k_{i}(a), and <′_{i} is a well-ordered relation on Arg_{i} (i < n). We assume in the following that Arg_{i} are disjoint and omit therefore the index i in k, l, <′. Let in the following O be as above.

(b) Ω_{0} := 0, Ω_{n+1} := ℵ_{n+1},

(c) An n-OFG is cardinality based, if for all B ⊆ Ord countable k_{i}^{−1}(B) is countable and for a ∈ Arg_{i}, l_{i}(a) ⊆ k_{i}(a) ∩ [Ω_{i}, Ω_{i+1}[. In this case we define k_{i,j}(a) := k_{i}(a) ∩ [Ω_{j}, Ω_{j+1}[.

(d) If O as above is a cardinality based n-OFG, we define by main recursion on n − i (i = 1, …, n) by side-recursion on <′ ordinals for a ∈ Arg_{i} eval_{i}(a) ∈ Ord and subsets C_{i}(a) ⊆ Ord by: C_{i}(a) := ⋃_{l=0}^{ω} C_{i}^{l}(a), where C_{i}^{0}(a) := [0, Ω_{i}[∪(⋃(k_{i}(a)∩Ω_{i+1}))∪l(a), C_{i}^{l+1}(a) := C_{i}^{l}(a)∪

⋃_{i≤j<n}{eval_{j}(b) | (j = i → b <′ a), b ∈ Arg_{j}, NF_{j}(b), k(b) ⊆ C_{i}^{l}(a)} and

NF(b) :⇔ NF_{j}(b) :⇔ eval_{j}(b) ∈ C_{j}(b). eval_{i}(a) := min{α | α ∉ C_{i}(a)}, eval(a) := eval_{i}(a) if a ∈ Arg_{i}, and NF_{i} := {a ∈ Arg_{i} | NF(a)}.

(e) For cardinality based n-OFG O we define Cl_{i} ⊆ NF_{i} simultaneously for all i < n inductively defined by: if b ∈ NF_{i}, k(b) ⊆ ⋃_{i<n} eval_{i}[Cl_{i}], then b ∈ Cl_{i}. Cl := ⋃_{i<n} Cl_{i}, Arg[Cl]_{i} := {a ∈ Arg_{i} | k(a) ⊆ eval[Cl]}, Arg[Cl] := ⋃_{i<n} Arg[Cl]_{i}. Note Cl_{i} ⊆ Arg[Cl]_{i}. Assuming, that eval_{i} ↾ NF_{i} is injective, which will be shown later, we define length : Arg[Cl] → ℕ, k_{i,j}^{0}, k′_{i,j} : Arg[Cl]_{i} →_{ω} Cl_{j} simultaneously inductively by: k_{i,j}^{0}(b) := eval_{j}^{−1}[k_{i,j}(b)] ∩ Cl_{j}. k′_{i,j}(b) := k_{i,j}^{0}(b) ∪ ⋃_{j<l<n} k′_{l,j}[k_{i,l}^{0}(b)]. length(b) := max(length[⋃ k′_{i,i}(b)] ∪ {−1}) + 1.

(f) Define for a, b ∈ Arg_{i} a ≺ b :⇔ a ≺_{i} b :⇔ eval_{i}(a) < eval_{i}(b).

Lemma 3.6 Let O be a cardinality based n-OFG.

(a) C_{i}(a) is the least set M such that C_{i}^{0}(a) ⊆ M and such that, if b ∈ Arg_{j}, j = i∧b <′ a or j > i, and, if NF(b) and k(b) ⊆ M, then eval_{j}(b) ∈ M.

(b) C_{i}(a) ∩ Ω_{i+1} ⊑ Ord.

Therefore especially eval_{i}(a) = C_{i}(a) ∩ Ω_{i+1}

(c) If a ∈ Arg_{i}, then eval_{i}(a) ∈ [Ω_{i}, Ω_{i+1}[.

(d) If a, b ∈ NF_{i}, then eval(a) < eval(b) ⇔ (a <′ b ∧ k_{i,i}(a) < eval(b)) ∨ eval(a) ≤ k_{i,i}(b). Especially eval ↾ NF_{i} is injective and therefore length and k′_{i,j} are well-defined.

(e) If a ∈ Arg[Cl]_{i}, l < j, then k′_{l,j}[k′_{i,l}(a)] ⊆ k′_{i,j}(a).

(f) If a ∈ Arg_{i}, b ∈ Cl_{j} ∩ C_{i}(a), i, j, l < n, i ≤ j, then eval[k′_{j,l}(b)] ⊆ C_{i}(a). If a ∈ Cl_{i}, then eval[k′_{i,j}(a)] ⊆ C_{i}(a).

(g) F := ((Cl_{i}, ≺_{i})_{i<n}, (k′_{i,j})_{i,j<n}, (length_{i})_{i<n}) is an n-ordinal system. We will call any n-OS structure isomorphic to F an n-OS based on O.

Proof: (a) is clear, since k(a) is finite. (b): Main induction on n − i, Side Induction on a ∈ Arg_{i}: Assume assertion for b <′ a. We show ∀α ∈ C_{i}^{n}(a) ∩ Ω_{i+1}.α ⊆ C_{i}(a) by side-side-induction on n: n = 0: clear, since l_{i}(a) ⊆ k_{i}(a). n → n + 1: If α ∈ (C_{i}^{n+1}(a) \ C_{i}^{n}(a)) ∩ Ω_{i+1}, then α = eval_{i}(b) with k(b) ⊆ C_{i}^{n}(a), by side-side-IH and, since l(b) ⊆ k(b), ⋃(k(b) ∩ Ω_{n+1}) ∪ l(b) ⊆ C_{i}(a), and by an immediate induction C_{i}^{l}(b) ⊆ C_{i}(a) for all l ∈ ω, C_{i}(b) ⊆ C_{i}(a), therefore α = min{γ | γ ∉ C_{i}(b)} ⊆ C_{i}(a).

(c) By an induction using the condition “cardinality based OFG” it follows that the cardinality of C_{i}^{n}(a) and therefore as well that of C_{i}(a) is < Ω_{i+1}. We conclude that there exists an α < Ω_{i+1} such that α ∉ C_{i}(a).

(d) “⇐” If a <′ b, k_{i,i}(a) < eval(b), NF(a), it follows easily k(a) ⊆ C(a) ⊆ C(b), eval_{i}(a) ∈ C(b) ∩ Ω_{i+1} = eval_{i}(b). If eval(a) ≤ k_{i,i}(b), follows by k_{i,i}(b) < eval(b) the assertion. “⇒” If the right side is false, the right side holds for eval_{i}(b) < eval_{i}(a) or a = b, so the left side is false. (e): easy induction on length(a). (f): First assertion by induction on length(a), side-induction on length(b). Second assertion: by k(a) ⊆ C_{i}(a). (g): by the above (in order to show k′_{i,i}(a) < eval(a) use k′_{i,i}(a) ⊆ C_{i}(a)). ⊓ ⊔

Example 3.7 (a) Let Arg′_{0} := CNF′_{0}([0, Ω_{1}[,]0, ω[), Arg′_{i+1} := CNF′_{i+1}([0, Ω_{i+2}[,]0, Ω_{i+1}[) \ CNF′_{i+1}({0},]0, Ω_{i+1}[), k′_{0}, l′_{0} as k, l in Example 2.7 (d) (with CNF′ replaced by CNF′_{0}), k′_{i+1}(CNF′_{i+1}(α_{1}, β_{1}, …, α_{m}, β_{m})) := {α_{1}, …, α_{m}, β_{1}, …, β_{m}},

l′_{i+1}(CNF′_{i+1}(α_{1}, β_{1}, …, α_{m}, β_{m})) := \begin{cases}\{α_{1}\} & if m > 1 or β_{m} > 1, \\ ∅ & otherwise. \end{cases}

(|Arg′_{i}|, k′_{i}, l′_{i}, <_{Arg}′_{i}) is a cardinality based n-OFG such that eval_{0}(CNF′_{0}(α_{1}, n_{1} …, α_{m}, n_{m})) = ω^{α_{1}}n_{1} + ⋯ + ω^{α_{m}}n_{m}, eval_{i+1}(CNF′_{i+1}(α_{1}, β_{1} …, α_{m}, β_{m})) = Ω_{i+1}^{α_{1}}β_{1} + ⋯ + Ω_{i+1}^{α_{m}}β_{m}.

(b) Let S_{l}, k^{l} be defined as in Example 2.7 (i), but with the restriction to ordinals < Ω_{n+1} always. Let Arg′_{i}, k′_{i}, l′_{i} be as before, F_{i} := Arg′_{i} ◯ ≺ \underline{ψ}_{i}(S_{l}), k_{i} ↾ Arg′_{i} := k′_{i}, l_{i} ↾ Arg′_{i} := l′_{i}, k_{i}(\underline{ψ}_{i}(a)) := k^{l}(a), l_{i}(\underline{ψ}_{i}(a)) := k^{l}(a) ∩ [Ω_{i}, Ω_{i+1}[ for a ∈ |S_{l}|. The resulting cardinality based n-OFG can be seen as a generalization of the extended Schütte Klammer symbols.

(c) Let f_{l}^{n} : S_{l} → Ord, f_{0}^{n}(α) := α, f_{l+1}^{n}\binom{β_{1}···β_{m}}{A_{1}···A_{m}} := Ω_{n}^{f_{l}^{n}(A_{1})}β_{1} + ⋯ + Ω_{n}^{f_{l}^{n}(A_{m})}β_{m}. If we restrict now \underline{ψ}_{i}(S^{l}) to \underline{ψ}_{i}(A) such that f_{l}^{n}(A) ∈ C′_{Ω_{i+1}}(f_{l}^{n}(A)), where C′_{Ω_{i+1}}(a) is the C-set for the function ψ_{Ω_{i+1}} as in [Buc92], but with 0, +, ω^{·} as basic function, we get eval_{i}(\underline{ψ}_{i}(A)) = ψ_{Ω_{i+1}}(f_{l}^{n}(A)). Again, with this last modification we get that in the resulting ordinal notation system ≺_{i} and ≺′_{i} coincide for terms of the form \underline{ψ}_{i}(A).

Remark 3.8 (a) The straightforward generalization of Lemma 2.8 holds as well for cardinality based n-OFG with the exception that we can conclude that a ≺ b is primitive recursive only for a ∈ T, b ∈ T′. Further under the assumptions of this generalized lemma the function corresponding to k′_{i,j}, which takes the place of k_{i,j} in the resulting n-OS, is primitive recursive.

(b) In order to replace Ω_{i} by Ω_{i}^{rec} (the i th admissible, starting with Ω_{0} = 0, Ω_{1} = ω_{1}^{ck}) we need some additional conditions, which essentially express that we have terms as in (a) for the higher number classes and arguments, but based on ordinals in [0, Ω_{i}^{rec}[.

They can be developed in a similar way as the conditions in (a), but because of lack of space, we omit them here.

Proof of (a): As in Lemma 2.8. Only the primitive recursive determination of r ≺ s follows as follows: Note that k̂_{i,j} corresponds to k_{i,j}^{0}. Let for s ∈ T′_{i} C^{j}(s) := {r ∈ T_{j} | eval(f(r)) ∈ C_{i}(f(s))}. We determine for s ∈ T′_{i}, r ∈ T_{j} such that length(r), length(s) ≤ length(t) by recursion on length(r) primitive recursively whether r ∈ C^{j}(s): If j < i, r ∈ C^{j}(s). If j = i, r ∈ C^{j}(s) ⇔ r ⪯ k̂_{i,i}(s) ∨ (r ⪯′ s ∧ ∀l < n(k̂_{i,l}(r) ⊆ C^{l}(s))) and, if i < j, r ∈ C^{j}(s) ⇔ ∀l < n.k̂_{i,j}(r) ⊆ C^{l}(s). Then in case i = j follows r ≺ s ⇔ r ∈ C^{i}(s) and t ∈ T′_{i} ⇔ NF(f(t)) ⇔ ∀j < n.k̂_{i,j}(t) ⊆ C^{j}(t). ⊓ ⊔

Lemma 3.9 (a) For the OFG in the Examples 3.7, there exists an elementary OS represented by them.

(b) The supremum of the strength of n-OS is |ID_{n}|.

Proof: (a) as for Lemma 2.9, (b) as for Theorem 2.11. ⊓ ⊔

4 Transfinitely Iterated Ordinal Systems

4.1 Definition of σ-OS

The naïve way of extending the approach used in the last section to the transfinite does not work. In the proof of well-ordering of n-OS we always reduced well-ordering of an n-OS F_{n} to F_{n}[A] for well-ordered sets A ⊆ T_{0}. If we try this with n replaced by ω, we will reduce the well-ordering of an ω-OS to the well-ordering of an ω-OS, which does not work. In the proof using the accessibility predicate we had to use induction by n − i instead of i, and this induction does not work if n is replaced by ω.

Proof theoretically, when moving to at least ω-iterated OS, we go beyond the strength of Π_{1}^{1} − CA, so Π_{1}^{1}-arguments, which we used in the intuitive well-ordering proofs there, do no longer work.

Our proof proceeded in some sense by induction on the lexicographic ordering of (T_{0}, T_{1}, …, T_{n−1}). Whereas the lexicographic ordering on tuples of fixed length is wellordered, if the underlying orderings are, this does no longer hold for tuples of arbitrary length. However, for sequences descending along some well-ordering this holds. The solution for our problem is now the following: Introduce a function level : T_{μ} → L, where (L, ≺_{L}) is an ordering. Let T_{μ}^{≤l} (T_{μ}^{≺l}) be the restriction of T_{μ} to those a such that level_{μ}(a) ≤ l (level_{μ}(a) ≺_{L} l). Now let T_{μ}^{≤l} refer to T_{ν}^{≺l} only (if μ < ν), i.e. level_{ν}[k_{μ,ν}(t)] ≺_{L} level_{μ}(t) for μ < ν, and assume T_{μ}^{≤l} ⊑ T_{μ}, i.e. r ≺_{μ} s → level_{μ}(r) ⪯_{L} level_{μ}(s). Then we will proceed by working on sequences T_{μ_{1}}^{≤l_{1}}, T_{μ_{2}}^{≤l_{2}}, … such that l_{1} ≻_{L} l_{2} ≻_{L} · · ·.

We need now that (L, ≺_{L}) is a well-ordering. But to demand this directly would be a too strong requirement. What suffices is, to have functions k̃_{μ} : L → T_{μ} such that, if we define L ↾_{ν<σ} B_{ν} as usual, but referring to k̃_{μ}, well-ordering of L ↾_{ν<σ} B_{ν} reduces to well-ordering of B_{ν}. We only need additionally to demand that, if we relativize the sets of terms and the levels to some set B, the levels of the terms in the relativized sets are in the relativized set of levels, i.e. ∀a ∈ T_{ν}.k̃_{μ}(level(a)) ⊆ k_{ν,μ}(a).

A last necessary modification is that, since we are no longer introducing first the nth OS completely, then the (n − 1)th OS completely, etc., we need to demand that there is a descend in length when moving to higher components, i.e. ν > μ → length[k_{μ,ν}(r)] < length(r).

Apart from the conditions stated before we need the (naïve) generalization of the conditions for n-OS, which will include that for every a only for finitely many ν k_{μ,ν}(a) ≠ ∅. We can now (although for the concrete examples this is not necessary, but it might be useful in the future) weaken the condition (OS 2) in the sense that if r ≺_{μ} s, then one new alternative is that level_{μ}(r) ≺_{L} level_{μ}(s).

Assumption 4.1 In the following we assume that some well-ordering (Σ, <) of order type σ > 0, where σ is an ordinal below the Bachmann-Howard ordinal, is given. Let 0 = min_{<} Σ We will identify (Σ, <) with σ, writing μ < σ for μ ∈ Σ, Ω_{μ} for Ω_{f(μ)}, where f : Σ → σ is the order isomorphism, etc.. In the following we assume μ, ν, ξ < σ. (Note that we use the same symbol < as for the ordering on ordinals).

Definition 4.2 (a) A σ-times iterated Ordinal-System-structure relative to (Σ, <), in short σ-OS-structure is a quadruple F = ((G_{μ}), (k_{μ,ν}), (L, ≺_{L}, (level_{μ}), (k̃_{μ})), length_{μ})

= ((G_{μ})_{μ<σ}, (k_{μ,ν})_{μ,ν<σ}, (L, ≺_{L}, (level_{μ})_{μ<σ}, (k̃_{μ})_{μ<σ}), (length_{μ})_{μ<σ}) such that, with G_{μ} = (T_{μ}, ≺_{μ}, ≺′_{μ}) and F_{μ} := (G_{μ}, k_{μ,μ}, length_{μ}), it holds that F_{μ} are OS-structures, k_{μ,ν} : T_{μ} →_{ω} T_{ν}, (L, ≺_{L}) is an ordering, k̃_{μ} : L →_{ω} T_{μ} and level_{μ} : T_{μ} → L (μ, ν ∈ Σ). We will always assume that T_{μ} are disjoint and L is disjoint from T_{μ} and write therefore ≺, ≺′, length, level instead of ≺_{μ}, ≺′_{μ}, length_{μ}, level_{μ} and ≺ instead of ≺_{L}. Let in the following F be as above.

(b) If F is a σ-OS-structure as above, A ⊆ T_{μ}, B ⊆ T_{ν}, A ↾_{ν} B := A ∩ k_{μ,ν}^{−1}[B]. If B_{ν} ⊆ T_{ν} for all ν < ξ, then A ↾_{ν<ξ} B_{ν} := A ∩ ⋂_{ν<ξ} k_{μ,ν}^{−1}[B_{ν}]. In the same way we define for A ⊆ L A ↾_{ν} B, A ↾_{ν<ξ} B_{ν}, referring to k̃_{ν} instead of k_{μ,ν}.

(c) A σ-OS-structure as above is a σ-times iterated Ordinal System relative to Σ, in short σ-OS, if for all μ, ν, ξ < σ and r, s ∈ T_{μ} the following holds (σ − OS 1) k_{μ,μ}(r) ≺ r; (σ − OS 2) μ ≤ ν → length[k_{μ,ν}(r)] < length(r); (σ − OS 3) if r ≺ s, then r ⪯ k_{μ,μ}(s) ∨ r ≺′ s ∨ level(r) ≺ level(s); (σ − OS 4) if ξ < ν, then k_{ν,ξ} ∘ k_{μ,ν} ⊆ k_{μ,ξ}; (σ − OS 5) k_{μ,ξ′}(r) = ∅ for almost all ξ′ < σ; (σ − OS 6) if μ < ν, then level[k_{μ,ν}(r)] ≺ level(r); (σ − OS 7) if r ≺ s, then level(r) ⪯ level(s); (σ − OS 8) k̃_{ν}(level(r)) ⊆ k_{μ,ν}(r); (σ − OS 9) if A_{ξ} ⊆ T_{ξ} are ≺-well-ordered (ξ < σ), then (T_{ν} ↾_{μ<σ} A_{μ}, ≺′) and

(L ↾_{μ<σ} A_{μ}, ≺) are well-ordered, too.

(d) A σ-OS F is well-ordered, if (T_{0}, ≺) is (where 0 = min_{<} Σ), and its order type is that of (T_{0}, ≺). It is primitive recursive, if the involved sets (including Σ) are primitive recursive subsets of the natural numbers (parameterized in Σ, i. e. t ∈ T_{μ} is primitive recursive in t and μ), all functions, relations (including <) are primitive recursive, the finitely many ν such that k_{μ,ν}(a) ≠ ∅ can be computed primitive recursively from μ, ν, a, and all properties (including linearity of < and that the chosen ν such that k_{μ,ν}(a) ≠ ∅ are the only ones) except of the well-ordering condition can be shown in primitive recursive arithmetic. It is elementary, if additionally the well-ordering condition follows in PRA in the sense of reducibility of transfinite induction in PRA to transfinite induction on {(μ, a) | μ < σ ∧ a ∈ T_{μ}} with the lexicographic ordering (μ, a) < (ν, b) ⇔ μ < ν ∨ (μ = ν ∧ a <_{μ} b).

(e) “Two σ-OS are isomorphic” is defined as for n-OS.

Comparison with n-OS. n-OS have now been defined twice, since σ can be finite. So more precisely we have to distinguish between “finite n-OS” and “transfinite n-OS”. However, one can see easily that a finite n-OS F can be considered as a special cases of a transfinite n-OS. Let Σ := {0, …, n−1}, < be the usual ordering on Σ, L := {n−1, n−2, …, 0}, k̃_{i}(j) := ∅, i ≺ j :⇔ j < i, level(r) := i for r ∈ T_{i}. Replace length_{i}(r) by length′_{i}(r) := max{length_{i}(r)} ∪ ⋃_{j≥i} length′_{j}[k_{i,j}(r)] (defined by recursion on n − i side-recursion on length(r)). One can easily see, that, if we extend the structure by the above and replace length by length′, we get a transfinite n-OS. This illustrates again why a naïve generalization of n-OS to ω-OS does not work: We get the reverse ordering of the natural numbers, which is not well-ordered.

4.2 Constructive Well-ordering Proof.

Theorem 4.3 (a) Every σ-OS is well-ordered.

(b) Every elementary σ-OS has order type below |ID_{σ}| = ψ(ϵ_{Ω_{σ}+1}).

Proof: (a): Define by recursion on μ ∈ Σ inductively M_{μ}, Acc_{μ} ⊆ T_{μ}: M_{μ} := T_{μ} ↾_{ν<μ} Acc_{ν}, Acc_{μ} := Acc_{≺}(M_{μ}). Acc′_{μ} := T_{μ} ↾_{ν<σ} Acc_{ν}, Acc′_{L} := L ↾_{ν<σAcc_{ν}}. Further, if l ∈ L, A ⊆ T_{μ} A^{⪯l} := {x ∈ A | level(x) ⪯ l}, similarly we define A^{≺l}. (Acc_{μ}, ≺), (Acc′_{μ}, ≺′) and (Acc′_{L}, ≺) are well-ordered. We show by induction on l ∈ Acc′_{L}

∀l ∈ Acc′_{L}.∀μ < σ.M_{μ}^{⪯l} ⊆ Acc_{μ} ,

and assume l according to induction. We show

∀s ∈ Acc′_{μ}^{⪯l}.s ∈ Acc_{μ}

by (side-)induction on (Acc′_{μ}, ≺′) and assume s according to induction: s ∈ M_{μ}. We define C^{ν}(s) ⊆ T_{ν} (ν < σ): For ν < μ, C^{ν}(s) := Acc_{ν}. C^{μ}(s) := {r ∈ M_{μ} | r ≺ s}. If μ < ν, C^{ν}(s) := {r ∈ T_{ν} | level(r) ≺ level(s) ∧ ∀ξ < ν.k_{ν,ξ}(r) ⊆ C^{ξ}(s)}. Note that by (σ-OS 4) for ν > μ C^{ν}(s) = {r ∈ T_{ν} | level(r) ≺ level(s) ∧ ∀ξ < μ(k_{ν,ξ}(r) ⊆ Acc_{ξ}) ∧ k_{ν,μ}(r) ≺ s∧

∀ξ(μ < ξ < ν → level[k_{ν,ξ}(r)] ≺ level(s))}.

The last equation allows to define C^{ν}(s) in |ID_{σ}| as needed in (b). We prove

∀ν(μ ≤ ν → ∀ξ < σ.k_{ν,ξ}[C^{ν}(s)] ⊆ C^{ξ}(s))  (∗)

by induction on ξ: For ξ < ν this follows by the definition of C^{ν}(s). Otherwise for ξ′ < ξ, k_{ξ,ξ′}[k_{ν,ξ}[C^{ν}(s)]] ⊆ k_{ν,ξ′}[C^{ν}(s)] ⊆ C^{ξ′}(s) by IH. Let r ∈ C^{ν}(s). In case μ = ν = ξ we have k_{ν,ξ}(r) ≺ r ≺ s and, if μ < ξ, it follows level[k_{ν,ξ}(r)] ⪯ level(r) ⪯ level(s), and one of the ⪯ is actually ≺, so in both cases we get the assertion. We show by (side-side-)induction on length(r) simultaneously for all ν

∀ν.∀r ∈ C^{ν}(s).r ∈ Acc_{ν}

and assume r according to induction, r ∈ C^{ν}(s). If ν < μ, r ∈ Acc_{ν}. Assume μ ≤ ν. By side-side-IH and (∗) follows for all ξ, k_{ν,ξ}(r) ⊆ Acc_{ξ} and k̃_{ξ}(level(r)) ⊆ k_{ν,ξ}(r) ⊆ Acc_{ξ}, r ∈ Acc′_{ν}, level(r) ∈ Acc′_{L}. If μ = ν, r ≺ s, r ⪯ k_{μ,μ}(s) ⊆ Acc_{μ}, r ∈ M_{μ}, r ∈ Acc_{μ} or r ≺′ s, r ∈ Acc′_{μ}, level(r) ⪯ level(s) ⪯ l, and by side-IH r ∈ Acc_{μ}, or level(r) ≺ level(s) and as in the next case “μ < ν” follows the assertion. If μ < ν, level(r) ≺ level(s) ⪯ l, level(r) ∈ Acc′_{L}, r ∈ M_{ν}, by main IH r ∈ Acc_{ν}. Now follows ∀r ∈ M_{μ}(r ≺ s → r ∈ Acc_{μ}), and, since s ∈ M_{μ}, s ∈ Acc(M_{μ}) = Acc_{μ}, and the side-induction is complete. Now by induction on length(s) it follows ∀s ∈ M_{μ}^{⪯l}.s ∈ Acc_{μ}: If s ∈ M_{μ}^{⪯l} we first show ∀ν.k_{μ,ν}(s) ⊆ Acc_{μ}. For ν < μ this follows by assumption. For μ ≤ ν we show this by induction on ν. With the usual argument we get using the IH k_{μ,ν}(s) ⊆ M_{ν}^{⪯l}, and therefore by IH k_{μ,ν}(s) ⊆ Acc_{ν}. Therefore s ∈ Acc′_{μ} and by the proven statement of the side-induction it follows s ∈ Acc_{μ}. Therefore the main-IH is completed. Now follows by induction on length(r), simultaneously for all μ, ∀r ∈ T_{μ}(r ∈ Acc_{μ} ∧ level(r) ∈ Acc′_{L}): By IH k_{μ,ν}(r) ⊆ Acc_{ν}, k̃_{ν}(level(r)) ⊆ Acc_{ν}, level(r) ∈ Acc′_{L}, r ∈ M_{μ}^{⪯level(r)}, r ∈ Acc_{μ}. Therefore it follows T_{μ} is well-ordered and we are done.

(b) The proof of (a) can be carried out in ID_{σ}. (Note, that transfinite induction over σ is one of the axioms of ID_{σ}). ⊓ ⊔

4.3 σ-Ordinal Function Generators

The ordinal function generators referring to σ-OS are now defined similarly as for n-OFG. The only difference is that in the definition of C_{μ}(a) we will refer only to b ∈ Arg_{ν} (ν > μ) such that level_{ν}(b) < level_{μ}(a), which is the obvious adaption of the principles for σ-OS to OFG.

Definition 4.4 (a) A σ-ordinal function generator, in short σ-OFG is a triple O := (A, L, k̃), where A = (Arg_{μ}, k_{μ}, l_{μ}, <′_{μ}, level_{μ})_{μ<σ}, L = (L, <_{L}), Arg_{μ} are classes (in set theory), k_{μ}, l_{μ} : Arg_{μ} →_{ω} Ord, level_{μ} : Arg_{μ} → L, ∀a ∈ Arg_{μ}.l_{μ}(a) ⊆ k_{μ}(a), <′_{μ} is a well-ordered relation on Arg_{μ}, ∀a, b ∈ Arg_{μ}(a <′_{μ} b → level_{μ}(a) ≤′_{μ} level_{μ}(b)), L is a well-ordering, k̃ : L →_{ω} Ord, ∀a ∈ Arg_{μ}.k̃[level_{μ}(a)] ⊆ k_{μ}(a). We assume in the following that Arg_{μ} and L are disjoint and omit therefore the index μ in k, l, <′, level and the index L in <′. Let O always be as above.

(b) Ω_{0} := 0, Ω_{μ} := ℵ_{μ} otherwise.

(c) A σ-OFG is cardinality based, if for all B ⊆ Ord countable k_{μ}^{−1}(B) is countable, l_{μ}(a) ⊆ k_{μ}(a)∩[Ω_{μ}, Ω_{μ+1}[ and ∀a ∈ Arg_{μ}.∀ν > μ.level_{ν}[k(a)∩[Ω_{ν}, Ω_{ν+1}[] < level_{μ}(a). In this case we define for a ∈ Arg_{μ}, k_{μ,ν}(a) := k(a) ∩ [Ω_{ν}, Ω_{ν+1}[ and for a ∈ L k̃_{ν}(a) := k(a) ∩ [Ω_{ν}, Ω_{ν+1}[.

(d) If O as above is a cardinality based σ-OFG, we define for a ∈ Arg_{μ} simultaneously for all μ < σ by recursion on level_{μ}(a) ∈ L, side-recursion on (<′, Arg_{μ}), eval_{μ}(a) ∈ Ord and subsets C_{μ}(a) ⊆ Ord by: C_{μ}(a) := ⋃_{n=0}^{ω} C_{μ}^{n}(a) where C_{μ}^{0}(a) := [0, Ω_{μ}[∪(⋃(k_{μ}(a) ∩ Ω_{μ+1})) ∪ l_{μ}(a), C_{μ}^{l+1}(a) := C_{μ}^{l}(a)∪

⋃_{ν≥μ}{eval_{μ}(b) | b ∈ Arg_{ν}, ((ν = μ ∧ b <′ a ∧ level(b) = level(a))∨
(level(b) < level(a))) ∧ k(b) ⊆ C_{μ}^{l}(a) ∧ NF_{ν}(b)},

where NF_{ν}(b) :⇔ k(b) ⊆ C_{ν}(b). eval_{μ}(a) := min{α | α ∉ C_{μ}(a)}.

(e) Let O be a cardinality based σ-OFG. Referring to the definition of NF(b) as above and assuming that eval ↾ NF_{μ} is injective, which will be shown later, NF_{μ}, Cl_{μ}, Cl, Arg[Cl]_{μ} and Arg[Cl] are defined as in Definition 3.5. Further we define k_{μ,ν}^{0}, k′_{μ,ν} : Arg[Cl]_{μ} →_{ω} Cl_{ν} by k_{μ,ν}^{0}(b) := eval_{ν}^{−1}[k_{μ,ν}(b)] ∩ Cl_{ν}, k′_{μ,ν}(b) := k_{μ,ν}^{0}(b) ∪ ⋃_{ν≤ξ<σ} k′_{ξ,ν}[k_{μ,ξ}^{0}(b)], length as in Definition 3.5 and level′_{μ} : Cl_{μ} → L by level′_{μ}(r) := max{level_{μ}(r)} ∪ level′_{μ}[k_{μ,μ}(r)].

(f) For r, s ∈ Arg_{μ} we define r ≺ s :⇔ r ≺_{μ} s :⇔ eval_{μ}(r) < eval_{μ}(s).

Lemma 4.5 Let O be a cardinality based σ-OFG.

(a) Lemma 3.6 (a) - (f) holds mutatis mutandis.

(b) F := ((Cl_{μ}, ≺_{μ})_{μ<σ}, (k′_{μ,ν})_{μ,ν<σ}, (length_{i})_{i<n}, (L, <_{L}), (level′_{μ})_{μ<σ}, (length_{μ})_{μ}) is a σ-ordinal system. We will call any σ-OS-structure isomorphic to F a σ-ordinal system based on O.

Proof: (a): We write (a).(x) for the assertion corresponding to Lemma 3.6(x). (a).(a): clear. (a).(b): Similarly as in Lemma 3.6 (b). In the argument, which showed there C_{i}^{l}(b) ⊆ C_{i}(a) and in the new context now shows C_{μ}^{l}(b) ⊆ C_{μ}(a), we use that b <′ a, therefore level(b) ≤ level(a). (a).(c): as before; (a).(d): as before, using a <′ b → level(a) ≤ level(b); (a).(e): as before easy induction on length(a); (a).(f): as before. (b): The only problem are (σ-OS 6), (σ-OS 7): We show for r, s ∈ Cl, that if eval_{ν}(r) ∈ C_{μ}(s), then, in case ν = μ, level′_{ν}(r) ≤ level′_{μ}(s), and, in case ν > μ, level′_{ν}(r) < level′_{μ}(s), by main induction on length(s), side-induction on length(r), which is immediate. ⊓ ⊔

Example 4.6 (a) The straight forward generalization of Example 3.7 (a) together with L := {0}, k̃_{μ}(0) := ∅, level_{μ}(a) := 0 yields a cardinality based σ-OFG for the Cantor normal form with basis ω (μ = 0) and Ω_{μ} (μ > 0).

(b) Example 3.7 (b) generalizes again to a cardinality based σ-OFG with L := S_{l} as in Example 2.7 (i), k̃(a) := k^{l}(a), level(Σ′_{μ}(t⃗)) := 0 (where 0 := () ∈ L), level(\underline{ψ}_{μ}(A)) := (A) (only in case l = 0 we have to modify L in order to make it disjoint from T_{μ}). The resulting system can be seen as a further generalization of the extended Schütte Klammer symbols. Note that, whereas for n-OS for all terms t = \underline{ψ}(A) ∈ T′ it holds t ∈ T (in the fixed point free version), this is no longer the case here.

(c) If f_{σ}^{l} is defined similarly and we apply a similar restriction as in Example 3.7 (c), then we get eval_{μ}(\underline{ψ}_{μ}(a)) = ψ_{Ω_{μ+1}}(f_{σ}^{l}(a)) with ψ_{Ω_{μ+1}} the usual ψ-function based on 0, +, ω^{·}.

Remark 4.7 Assume the assumptions of the straight forward generalization of Lemma 2.8 to cardinality based σ-OFG. Additionally assume sets L̂ ⊆ L̂′ ⊆ L̂′′ corresponding to L such that L̂′′ is primitive recursive, a function f : L̂ → L and primitive recursive

functions ˆ k̃_{μ} : L̂′′ →_{ω} T′′_{μ}, l̂evel_{μ} : T′′_{μ} → L̂ corresponding to k̃_{μ}, level_{μ}. Define for l, l′ ∈ L, l ≺_{L} l′ :⇔ f(l) <_{L} f(l′). Assume the adaption of condition (b) of Lemma 2.8 for the

new structure and (a), (c) - (f) for L̂, ˆ k̃ instead of T, k̂, where appropriate, and omitting NF. E.g. the adaption of condition (d) to L reads: If A_{μ} ⊆ T′_{μ}, f ↾ A_{μ} is injective (μ < σ), then f ↾ {t ∈ L′ | ∀μ < σ.ˆk̃_{μ}(t) ⊆ A_{μ}} is injective. Then the conclusion of this lemma generalized to our setting holds as well in the weakened version of Remark 3.8, and additionally L̂, L̂′, ≺_{L} are primitive recursive.

Proof: As before. ⊓ ⊔

Theorem 4.8 (a) For every OFG in the Example 4.6 there exists an elementary OS based on it.

(b) The supremum of the strength of σ-OS is |ID_{σ}|.

Proof: As for Theorem 3.9. ⊓ ⊔

References

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

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

[Buc92] 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.

[Gir] J.-Y. Girard. Proof theory and logical complexity. Handwritten notes, 1135 pp.

[Gir80] J.-Y. Girard. Proof theoretic investigations of inductive definitions I. In E. Engeler, H. Laeuchli, and V. Strassen, editors, Logic & Algorithms. An international symposium held in honour of Ernst Specker, pages 201 – 236, Zurich, Switzerland, 1980.

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

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

[RW93] Michael Rathjen and Andreas Weiermann. Proof–theoretic investigations on Kruskal’s theorem. Annals of Pure and Applied Logic, 60:49–88, 1993.

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

[Sch77] K. Schütte. Proof Theory. Springer, Berlin, Heidelberg, New York, 1977.

[Sei94] M. Seisenberger. Das Ordinalzahlbezeichnungssystem OT(ϑ) und seine Verwendung im Beweis von Kruskals Satz. Master’s thesis, Universität München, March 1994.

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

[Set98a] A. Setzer. An introduction to well-ordering proofs in Martin-Löf’s type theory. To appear in: G. Sambin, J. Smith (Eds.), Twenty-five years of constructive type theory, Oxford University Press, 1998.

[Set98b] A. Setzer. Well-ordering proofs for Martin-Löf Type Theory. Ann. Pure App. Logic, 92:113 – 159, 1998.