An Introduction to Well-ordering Proofs in Martin-Löf’s Type Theory

Anton Setzer^{1} Department of Mathematics, Uppsala University

Abstract We define ordinal notation systems from below and show that the prooftheoretic strength of theories, in which we can define the accessible part, cannot be expressed in such systems. It is shown that in Martin-Löf’s type theory with W-type we can define the accessible part. Ordinal notation systems which are stronger than those from below are introduced, we give well-ordering proofs for Martin-Löf’s Type Theory with non nested and with arbitrarily nested W-type and obtain (best possible) lower bounds for the proof-theoretic strength of the theories considered. The focus in this article is on explaining and motivating techniques of well-ordering proofs to researchers outside proof theory.

1 Introduction

The proof-theoretic strength α of a theory is the supremum of all ordinals up to which we can prove transfinite induction in that theory. Whereas for classical theories the main problem is to show that α is an upper bound for the strength – this means usually to reduce the theory to a weak theory like primitive recursive arithmetic or Heyting arithmetic extended by transfinite induction up to α, which can be considered to be more constructive then the classical theory itself – for constructive theories this is in most cases not difficult, since we can easily build a term model in a classical theory of known strength. For constructive theories in general the main problem is to show that α is a lower bound: that despite of the restricted principles available one has a proof theoretically strong theory.

In this article we will concentrate on the direct method for showing that α is a lower bound, namely well-ordering proofs: to carry out in the theory a sequence of proofs of the well-foundedness of linear orderings of order type α_{n}, such that sup_{n∈ω} α_{n} = α. Such proofs can be considered to be the logically most complex proofs which one can carry out in the theory: in most cases additionally to transfinite induction up to α_{n} for each n only primitive recursive arithmetic is needed in order to analyze the theory proof theoretically and in order to prove the same Π_{2}^{0}-sentences. Griffor and Rathjen (1994) have used the more indirect method of interpreting theories of known strength in type theory for obtaining lower bounds for the strength of it. Apart from the fact that in the case of one universe and W-type Griffor and Rathjens approach did not yield sharp bounds we believe that the direct method has the advantage of giving a deeper insight into the theory, since one examines the principles of the theory directly without referring to the analysis of another theory, and that the programs obtained by it are of independent interest.

1This article is based on a series of lecture the author has given while he was visiting — at that time based in Munich — the universities of Stockholm and Uppsala. He wants to thank P. Martin-Löf for inviting him and making this fruitful visit possible and the logic group in Uppsala for providing a creative and thoughtful environment.

In (Setzer 1995) and (Setzer 1996) we have carried out well-ordering proofs for Martin-Löf’s type theory with W-type and one universe and for the Mahlo universe. In this article, in contrast with these technical articles, we want to concentrate on explaining the techniques used and therefore help to make them accessible to researchers outside proof theory. We will do this for the theories without universes (except of a microscopic universe which contains two types) and plan to continue this exposition later with an article in which we explain well-ordering proofs for theories with an ordinary universe and with a Mahlo universe.

We will start our introduction to well-ordering proofs by explaining the ordinal notation systems needed. They seem to be the main obstacle to the understanding of the proof theory of strong systems. In order to motivate, what kind of systems are necessary, we will introduce in this article first ordinal notation systems in general (Sect. 2) and some weak ordinal notation systems (Sect. 3), which are relatively intuitive. We will analyze them, define the concept of ordinal notation systems from below and observe that the systems introduced fall under this concept. An ordinal notation system is essentially from below, if the notation of an ordinal α is based only on smaller ones and and all ordinals β below α have notations which can be introduced by a recursive process before α. Therefore the ordinal notations are systematically built up from below and this makes it easy to understand that they are well-founded.

In Sect. 4 we introduce the accessible part as the largest well-founded segment of a linear ordering (a segment of the ordinals is a subset of the ordinals A such that ∀β ∈ A.β ⊂ A). With this concept we can formalize, what we think is the reason why such systems can be seen as intuitively well-founded (see the proof of lemma 4.3 (b)): the accessible part is closed under the functions the notation system is built of and therefore we have transfinite induction over the full notation system. This proof can be carried out in a theory which allows to define the accessible part. Since this is the case for the theories considered here, the proof theoretic strength of them can no longer be expressed in systems which are from below, and stronger systems are needed.

We will explain the extended principles needed for the definition of stronger ordinal notation systems (Sect. 5) — we will denote ordinals by using bigger ones — and then carry out the well-ordering proofs for type theory with Kleene’s O, one unnested W-type. We will end this article in Sect. 6 with the introduction of stronger ordinal notation systems and well-ordering proofs for type theory with arbitrarily nested W-type.

Some conventions about sequences of ordinals and natural numbers follow:

The sequence of the ordinals α_{1}, …, α_{n} coded in the usual way is denoted by (α_{1}, …, α_{n}); α⃗, β⃗, … denote sequences of ordinals coded in this way; the ith element of α⃗, β⃗, … is α_{i}, β_{i}, …. Ord is the class of ordinals in set theory and Ord^{∗} the class of codes for sequences of ordinals. If a_{1}, …, a_{n} are natural numbers, <a_{1}, …, a_{k}> is a code for the sequence a_{1}, …, a_{k} (with the usual properties like primitive recursiveness); sequences of natural numbers are denoted by a⃗, b⃗, c⃗, …; the ith element of a⃗ is a_{i}, of b⃗ is b_{i}, etc.; seqlength(a⃗) is the length of the sequence a⃗; a⃗ ∗ b⃗ is the concatenation of the lists a⃗ and b⃗.

2 Ordinal Notation Systems

The usual way of introducing ordinal notation systems is to start with a collection of functions f_{i} : dom(f_{i}) ⊂ Ord^{∗} → Ord and then to introduce a collection of terms T built from symbols f̂_{i} representing the functions f_{i}. In T one usually has more than one notation for the ordinals denoted, therefore one selects normal forms, i.e. subsets nf(f_{i}) ⊂ dom(f_{i}), such that in the term system OT formed from terms built from normal forms only we have at most one notation for every ordinal. This will be formalized in the following:

Definition 2.1 Assume f_{i} : dom(f_{i}) ⊂ Ord^{∗} → Ord, nf_{i} ⊂ dom(f_{i}), (i = 1, …, n), F := (f_{i}, nf_{i})_{1≤i≤n}. If α⃗ = (α_{1}, …, α_{k}), then f̂_{i}(α⃗) := (i, α_{1}, …, α_{k}). We omit unnecessary brackets and write f_{i}, f̂_{i} instead of f_{i}(), f̂_{i}().

(a) nf(f̂_{i}) := nf_{i}, NF(f̂_{i}(α⃗)) :⇔ α⃗ ∈ nf_{i}, α =_{NF} f̂_{i}(β⃗) :⇔ NF(f̂_{i}(β⃗)) ∧ α = f_{i}(β⃗).

(b) Closure(F, ρ), the closure of ρ under f_{i} in normal form, is the least subset of Ord such that ρ ⊂ Closure(F, ρ) and, if α_{1}, …, α_{k} ∈ Closure(F, ρ) and α =_{NF} f̂_{i}(α_{1}, …, α_{k}), then α ∈ Closure(F, ρ).

(c) F is called a system of ordinal functions in normal form, iff the following holds: (NF 1) If α =_{NF} f̂_{i}(α⃗), α =_{NF} f̂_{j}(β⃗), then i = j and α⃗ = β⃗. (NF 2) If α⃗ = (α_{1}, …, α_{k}) ∈ dom(f_{i}), α_{1}, …, α_{k} ∈ Closure(F, ρ), then

f_{i}(α⃗) ∈ Closure(F, ρ).

(d) An ordinal function with normal form is a pair (f, nf) such that (f, nf)_{1≤i≤1} is a system of ordinal functions in normal form.

(e) We will in the following usually write f_{i} instead of f̂_{i}.

In condition (NF2) we refer to Closure(F, ρ) and not only to Closure(F, 0) in order to make the extension of the system by adding further ordinal functions easier.

Definition 2.2 Assume that F = ((f_{i}, nf_{i})_{1≤i≤n}) is a system of ordinal functions in normal form. Let f̃_{i}(n_{1}, …, n_{k}) := <i, n_{1}, …, n_{k}> (n_{1}, …, n_{k} ∈ ℕ). We write f̃_{i} instead of f̃_{i}(<>) and f̃_{i}(n_{1}, …, n_{k}) instead of f̃_{i}(<n_{1}, …, n_{k}>).

(a) T_{F}, or shorter T, the set of pre-terms for F, is defined inductively by: if k ∈ ℕ, t_{1}, …, t_{k} ∈ T, 1 ≤ i ≤ k, then f̃_{i}(t_{1}, …, t_{k}) ∈ T. Note that T is a primitive recursive subset of ℕ.

(b) length_{F} or shorter length : T_{F} → ℕ and o_{F} or shorter o : T_{F} → Ord are defined by: length(f̃_{i}(t_{1}, …, t_{k})) := max{length(t_{1}), …, length(t_{k})} + 1.

o(f̃_{i}(t_{1}, …, t_{k})) := \begin{cases}f_{i}(o(t_{1}), …, o(t_{k})) & if (o(t_{1}), …, o(t_{k})) ∈ dom(f_{i}), \\ 0 & otherwise. \end{cases}

(c) We define OT_{F} ⊂ T_{F} (or shorter OT), the set of ordinal notations corresponding to F simultaneously by: If a_{1}, …, a_{k} η OT and NF(f_{i}(o(a_{1}), …, o(a_{k}))), then f̃_{i}(a_{1}, …, a_{k}) η OT.

(d) For a, b η OT_{F}, a ≺_{F} b :⇔ o_{F}(a) < o_{F}(b), a ⪯_{F} b :⇔ a ≺_{F} b ∨ a = b. Again, we will usually omit the index F.

(e) The ordinal notation system defined by F is the triple (OT_{F}, ≺_{F}, o_{F}). An ordinal notation system defined by functions in normal form is a triple (OT, ≺, o) such that for some functions F in normal form (OT, ≺, o) = (OT_{F}, ≺_{F}, o_{F}). We write (OT, ≺), if o is obvious or not used.

(f) The ordinal notation system (OT, ≺, o) is called primitive recursive, if OT and ≺ can be defined primitive recursively.

(g) ÑF_{F}(f̃_{i}(t_{1}, …, t_{k})) :⇔ (o(t_{1}), …, o(t_{k})) ∈ nf_{i} ∧ t_{1}, …, t_{k} η OT; ñf_{F}(f̃_{i}) := {t⃗ ∈ OT^{∗} | ÑF_{F}(f̃_{i}(t⃗))}; t =_{NF,F} f̃_{i}(t_{1}, …, t_{k}) :⇔ NF_{F}(f̃_{i}(t_{1}, …, t_{k})) ∧ t = f̃_{i}(t_{1}, …, t_{k}).

(h) We will usually omit the tilde and indices F.

(i) In the following usually r, s, t denote elements of T and a, b, c elements of OT (possibly with subscripts).

Note that, since we have normal forms, o : OT → Closure(F, 0) is bijective. Further, if we have a primitive recursive ordinal notation system for F, then the relation t =_{NF} f_{i}(t_{1}, …, t_{k}) is primitive recursive in t, t_{1}, …, t_{k}, since t =_{NF} f_{i}(t_{1}, …, t_{k}) ⇔ t = f_{i}(t_{1}, …, t_{k}) ∧ t, t_{1}, …, t_{k} η OT.

We will give some examples of primitive recursive ordinal notation systems:

1. The Cantor Normal Form. Let dom(CNF) := {(α_{1}, m_{1}, …, α_{k}, m_{k}) | k ∈ ω, α_{i} ∈ Ord, m_{i} ∈ ω}, CNF(α_{1}, n_{1} …, α_{k}, n_{k}) := ω^{α_{1}}(n_{1} + 1) + ⋯ + ω^{α_{k}}(n_{k} + 1), CNF() := 0. NF(CNF(α_{1}, n_{1}, …, α_{k}, n_{k})) :⇔ α_{1} < ⋯ < α_{k} < CNF(α_{1}, n_{1}, …, α_{k}, n_{k}), NF(CNF()). The ordinal notation system defined by CNF can be easily seen to be primitive recursive by using that in case of NF(CNF(α_{1}, n_{1}, …, α_{k}, n_{k})) and NF(CNF(β_{1}, m_{1}, …, β_{l}, m_{l})) we have CNF(α_{1}, n_{1}, …, α_{k}, n_{k}) < CNF(β_{1}, m_{1}, …, β_{l}, m_{l}) ⇔ ((α_{1}, n_{1}) …, (α_{k}, n_{k})) <_{lex,lex} ((β_{1}, m_{1}) …, (β_{l}, m_{l})), where <_{lex,lex} is the lexicographic ordering on strictly descending sequences based on the lexicographic ordering on pairs (γ, n) which itself is based on <.

2. The Veblen function φ. Let φ_{α}β be the (1 + β)th common fixed point of the functions λγ.φ_{α′}γ (α′ < α) and of λγ.ω^{γ}. We can show (see for instance (Schütte 1977)) φ_{α}β < φ_{α′}β′ ⇔ (β < φ_{α′}β′ ∧ α < α′) ∨ (β < β′ ∧ α = α′) ∨ (φ_{α}β < β′ ∧ α′ < α). Let NF(φ_{α}β) :⇔ α, β < φ_{α}β, and NF(CNF) defined as before. Then CNF and φ define a primitive recursive ordinal notation system.

3. The n-ary Veblen-function φ^{n} : Ord^{n} → Ord is defined by φ^{n}(0, …, 0, β) := φ_{0}β and, if α_{k} ≠ 0, then φ^{n}(α_{1}, …, α_{k}, 0, …, 0, β) is the (1 + β)th common fixed point of the functions λγ.φ^{n}(α_{1}, …, α_{k−1}, α^{−}, γ, 0, …, 0) with α^{−} < α_{k}. Define NF(φ^{n}(α⃗)) :⇔ α_{1}, …, α_{n} < φ^{n}(α⃗). CNF and φ^{n} define a primitive recursive system of functions in normal form.

4. The Schütte Klammersymbole Schütte (1954) introduced an extension of the Veblen functions by allowing arguments indexed by ordinals, of which

only finitely many are present. The symbol φ(A), with A := ( \begin{matrix}α_{1} & ⋯ & α_{n} \\ β_{1} & ⋯ & β_{n} \end{matrix} )

stands for the value of the extended Veblen function, where the β_{i}th argument is α_{i} (and the others are 0). They can be defined formally by transfinite recursion on ((β_{1}, α_{1}), …, (β_{n}, α_{n})) ordered by <_{lex,lex}, where <_{lex,lex} is the lexicographic ordering on descending sequences based on the lexicographic on pairs, which is itself based on the ordering < on the ordinals. For A as above we define NF(φ(A)) if 0 ≠ α_{i} < φ(A), β_{n} < ⋯ β_{1} < φ(A). With the properties shown in (Schütte 1954) one can see, that the Schütte Klammersymbole together with the constant 0 form a primitive recursive ordinal notation system.

Simplification of the general situation. We can code a system of ordinal functions (f_{i}, nf_{i})_{1≤i≤n} into one function with normal form (f, nf) as follows: Assume (after some small changes in F) that dom(f_{1}) = {()}, and i − 2 ∈ Closure((f_{j}, nf_{j})_{1≤j<i}, 0) (2 ≤ i ≤ n). Therefore 0 =_{NF} f_{0}(). Let {dom(f) \atop nf(f)} :=

\{()\} ∪ ⋃_{2≤i≤n}\{(i − 2, α_{1}, …, α_{m}) | m ∈ ω ∧ (α_{1}, …, α_{m}) ∈ {dom(f_{i}) \atop nf(f_{i})}\}, f() := 0, f(i − 2, α_{1}, …, α_{m}) := f_{i}(α_{1}, …, α_{m}) (2 ≤ i ≤ n). Now the ordinal notation systems formed by (f, nf) and (f_{i}, nf_{i})_{1≤i≤n} are essentially the same. In order to simplify the considerations we will in the following in the development of the general theory restrict ourselves to systems of ordinal functions consisting of only one function. The examples of systems given will be identified with the system consisting of one function only obtained by the above procedure.

3 Ordinal Notation Systems from Below

Ordinal notation systems from below are those, in which ordinals are introduced in a systematic way by denoting ordinals using smaller ones. Such systems should be intuitively well-ordered. The formalization of this leads to three conditions:

Ordinals should be denoted by smaller ones, therefore we need that, if a⃗ ∈ NF(f_{i}), then a_{i} ≺ f_{i}(a⃗). One might think, that this already defines systems from below completely. However, any ordinal notation system OT can be immediately seen as a system fulfilling this condition: take the system consisting of the constant 0, the successor function restricted to natural numbers and the function which assigns to a natural number a, which is a code for an infinite ordinal notation in OT, the ordinal o(a). This example shows that, in order to have notation systems which are intuitively well-ordered, we need that new notations for ordinals are introduced only after having denoted all smaller ordinals.

Therefore we have the second condition: all ordinals b below some ordinal a = NFf(a⃗) should be introduced before a: Either b ⪯ a_{i} and, since a_{i} is known, b is known as well, or b = NFf(b⃗) and b⃗ ≺′ a⃗, where ≺′ is some ordering on the argument tuples which expresses what is meant by the word “before”.

We can view this process of introducing new ordinals as recursion on ≺′. In fact it will essentially the same as the recursion, by which the ordinal function corresponding to f can be defined. Now, since we have a recursive process, ≺′ needs to be a well-ordering. We will look at our examples in order to make more precise, what condition is required for ≺′:

In the first example ≺′ is the lexicographic ordering on descending sequences based on the lexicographic ordering on pairs. If we code up the second example into one function we need the additional constant 0, therefore have to omit () from NF(CNF), and get f() = 0, f(0, c⃗) = CNF(c⃗) and f(1, b, c) = φ_{b}c. We can define now () ≺′ (0, c⃗) ≺′ (1, b, c), and order tuples (0, c⃗) by the double lexicographic ordering on c⃗ as before, and triples (1, b, c) by the lexicographic ordering on pairs (b, c). Then for instance, if a ≺ b =_{NF} φ_{c}d = f(1, c, d), a =_{NF} 0 = f() with () ≺′ (1, c, d) or a = CNF(e⃗) = f(0, e⃗) with (0, e⃗) ≺′ (1, c, d) or a =_{NF} φ_{e}f = f(1, e, f), with c ≺ e and a ≺ d or (e, f) ≺_{lex} (c, d), (1, d, e) ≺′ (1, b, c). For the system built from CNF, φ^{n} we can take a similar ordering with the lexicographic ordering on n-tuples instead of pairs, and in the last example of the Schütte Klammersymbole we can take as ≺′ the double lexicographic ordering similar to that used in the first example.

All these orderings have in common that their well-foundedness reduces by a proof theoretically weak argument to the well-ordering of ≺: We will see later that in all examples for every formula ϕ(b⃗) there exist formulas ϕ_{i}(a, z_{1}, …, z_{l}) such that from transfinite induction on (OT, ≺) for {a | ϕ_{i}(a, z_{1}, …, z_{l})} we can conclude transfinite induction for the class {b⃗ | ϕ(b⃗)} by a simple argument. Simple means that this argument can be carried out uniformly in primitive recursive arithmetic PRA. Uniformly means now that we can show that for all subsets R of ℕ transfinite induction over (nf(f) ∩ R^{∗}, ≺′) reduces to transfinite induction over (OT ∩ R, ≺). The extension to subsets R of OT expresses that, whenever we have introduced a set of ordinal notations R such that R is well-ordered, then we have already well-ordering of the corresponding set of argument tuples nf(f) ∩ R^{∗}.

We will give now the precise definitions:

Definition 3.1 Let PRA be primitive recursive arithmetic, i.e. Heyting arithmetic, but with induction restricted to quantifier free formulas. PRA^{+} is the extension of PRA by additional predicates of arbitrary arity without defining axioms and without induction for formulas containing such predicates. We call such predicates free predicates.

Definition 3.2 Assume that T is some theory with some standard interpretation of the connectives of PRA and of primitive recursive functions in it (the primitive recursive functions might be represented by relations representing the graphs such that we can show the existence and uniqueness conditions for functions). T is an extension of PRA, if all the rules and axioms of PRA can be derived in the extended language (with this representation of connectives and functions).

Definition 3.3

(a) Let in the following ≺, ≺′, … denote binary relations represented by formulas in PRA^{+}, i.e. n ≺ m is some fixed formula, s ≺ t := (n ≺ m)[n := s, m := t]. Let ≺ be fixed in the following.

(b) ∀n ≺ s.ϕ := ∀n.n ≺ s → ϕ, ∃n ≺ s.ϕ := ∃n.n ≺ s ∧ ϕ.

(c) A class in any extension of PRA is an expression of the form {n | ϕ}, where n is a variable and ϕ a formula in the extended language (which means, if the theory is Martin-Löf’s type theory, that we can prove n ∈ N ⇒ ϕ set). The variables of the class {n | ϕ} are the free variables of ϕ, excluding n. In the following A, A′, B, … denote classes.

(d) sη{n | ϕ} := ϕ[n := s]; ∀n η A.ϕ := ∀n.n η A → ϕ, similarly for ∃n η A.ϕ; {n η A | ϕ} := {n | n η A ∧ ϕ}.

(e) We identify a primitive recursive set A with the class {n | f(n) = 1}, where f is the primitive recursive function ℕ → ℕ such that f(n) = 1 iff n is an element of A, f(n) = 0 otherwise.

(f) We identify {n | Q(n)} with Q, if Q is a unary free predicate.

(g) A × B := {n⃗ | seqlength(n⃗) = 2 ∧ n_{0} η A ∧ n_{1} η B}; A^{∗} := \{n⃗ | ∀i < seqlength(n⃗).n_{i} η A\}; A{∩ \atop ∪}B := \{n | n η A{∧ \atop ∨}n η B\}; a_{≺} := {n | n ≺ a}, and we omit usually the index ≺.

(h) A ⊂ B := ∀n η A.n η B; A ≅ B := A ⊂ B ∧ B ⊂ A.

(i) Prog_{(A,≺)}(B) := ∀n η A.(A ∩ n_{≺}) ⊂ B → n η B. TI_{(A,≺)}(B) := Prog_{(A,≺)}(B) → A ⊂ B.

Definition 3.4 Transfinite induction over (≺, A) is in PRA reducible to transfinite induction over (A_{i}, ≺_{i}) (i = 1, …, n), in short TI_{(A,≺)} is PRAreducible to TI_{(A_{i},≺_{i})}, if there exist n_{i} ∈ ℕ, variables z_{ijk}, classes B_{ij} with free variables ⊂ {z_{ij1}, …, z_{ijm_{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.

Lemma 3.5

(a) If TI_{(A,≺)} is PRA-reducible to TI_{(A_{i},≺_{i})}, then for every class B of PRA^{+} there exists classes B_{ij} with free variables ⊂ {z_{ij1}, …, z_{ijm_{ij}}} such that PRA^{+} ⊢ ⋀_{ij}(∀z_{ij1}, …, z_{ijm_{ij}}TI_{(A_{i},≺_{i})}(B_{ij})) → TI_{(A,≺)}(B).

(b) If TI_{(A,≺)} is PRA-reducible to TI_{(A_{i},≺_{i})} (i = 1, …, n) and for each i TI_{(A_{i},≺_{i})} is PRA-reducible to TI_{(B_{ij},≺′_{ij})} (j = 1, …, m_{i}), then TI_{(A,≺)} is PRA-reducible to TI_{(B_{ij},≺′_{ij})} (i = 1, …, n, j = 1, …, m_{i}).

(c) TI_{(A∩B,≺)} is PRA-reducible to TI_{(A,≺)}.

(d) Assume A ∩ B = ∅. Define n ≺ m :⇔ (n, m η A ∧ n ≺_{1} m) ∨ (n, m η B ∧ n ≺_{2} m) ∨ (n η A ∧ m η B). Then TI_{(A∪B,≺)} is PRA-reducible to TI_{(A,≺_{1})} and TI_{(B,≺_{2})}.

(e) Let ≺_{lex} be the lexicographic combination of ≺_{1}, ≺_{2}, i.e. a ≺_{lex} b := seqlength(a) = seqlength(b) = 2 ∧ ((a)_{0} ≺_{1} (b)_{0} ∨ ((a)_{0} = (b)_{0} ∧ (a)_{1} ≺ (b)_{1})). Then TI_{((A_{1}×A_{2},≺_{lex})} is PRA-reducible to TI_{(A_{1},≺_{1})}, TI_{(A_{2},≺_{2})}.

(f) Let Des_{≺}(A) := {n⃗ | n⃗ η A^{∗} ∧ ∀i.i + 1 < seqlength(n⃗) → n_{i+1} ≺ n_{i}} be the set of all descending sequences in A, ≺_{lex} be the lexicographic ordering defined from ≺, (n⃗ ≺ m⃗ := (seqlength(n⃗) < seqlength(m⃗) ∧ ∀i < seqlength(n⃗).n_{i} = m_{i})∨

∃i < min({seqlength(n⃗), seqlength(m⃗)}).(∀j < i.n_{j} = m_{j}) ∧ n_{i} ≺ m_{i}). Then TI_{(Des_{≺}(A),≺_{lex})} is PRA-reducible to TI_{(A,≺)}.

(g) If PRA^{+} ⊢ (∀n η A.∃m η B.ϕ(n, m)) ∧ ∀n, n′ η A.∀m, m′ η B.ϕ(n, m) → ϕ(n′, m′) → (n ≺ n′ ↔ m ≺′ m′), then TI_{(A,≺)} is PRA-reducible to TI_{(B,≺′)}.

Proof: (a): replace Q by B. (b): by (a). (c): From TI_{(A,≺)}({n | n η B → n η Q}) follows TI_{(A∩B,≺)}(Q). (d), (e): easy.

(f) We use in this proof the notations (n⃗, m⃗) := n⃗ ∗ m⃗, (n⃗, n, m⃗) := n⃗∗ < n > ∗m⃗ etc. We adapt the Gentzen proof (Gentzen 1943), which shows that from PA ⊢ TI(α) follows PA ⊢ TI(ω^{α}) (this proof is well explained in (Schütte 1977)). We write Des for Des_{≺}(A), and show that from TI_{(A,≺)}(S), where S := {n | ∀m⃗.(Des ∩ m⃗_{≺_{lex}} ⊂ Q → ∀k⃗.(m⃗, n, k⃗) η Des → (m⃗, n, k⃗) η Q}, follows TI_{(Des,≺_{lex})}(Q): Assume Prog_{(Des,≺_{lex})}(Q). We show Prog_{(A,≺)}(S): Assume n η A, A ∩ n_{≺} ⊂ S (this will be called IH), Des∩m⃗_{≺_{lex}} ⊂ Q, (m⃗, n, k⃗) η Des. We show (m⃗, n, k⃗) η Q: First, by Des∩m⃗_{≺_{lex}} ⊂ Q, m⃗ η Des and Prog_{(Des,≺_{lex})}(Q) follows m⃗ η Q. Further, ∀l⃗ ≺_{lex} (m⃗, n).l⃗ η Des → l⃗ η Q: If l⃗ ≺_{lex} (m⃗, n), then l⃗ ≺_{lex} m⃗, therefore l⃗ η Q, or l⃗ = m⃗ and l⃗ η Q or l⃗ = (m⃗, l, l⃗′), with l ≺ n, l η A. In the last case follows by Des∩m⃗_{≺_{lex}} ⊂ S and the IH l⃗ η Q. Therefore we have (m⃗, n) η Q. If now k⃗ = <>, we are done. Otherwise k⃗ = (k_{0}, k⃗′), k_{0} ≺ n, k_{0} η A, Des ∩ (m⃗, n)_{≺_{lex}} ⊂ Q, by IH therefore (m⃗, n, k⃗) = (m⃗, n, k_{0}, k⃗′) η Q. We have now shown A ⊂ S. Des ∩ <>_{≺_{lex}} ⊂ Q, therefore <> η Q and, if n⃗ η Des, n⃗ ≠ <>, then n⃗ = (n, m⃗) for some n η A, m⃗, and by n η S, (n, m⃗) η Des and n η S follows n⃗ η Q. Therefore Des ⊂ Q.

(g) PRA^{+} ⊢ TI_{(B,≺′)}(C) → TI_{(A,≺)}(Q) with C := {m | ∀n η A.ϕ(n, m) → n η Q}.

Now we can define what an ordinal notation system from below is: Definition 3.6

(a) Let (f, nf) be an ordinal function with normal form, (OT, ≺, o) be the ordinal notation system defined from (f, nf), and assume that it is primitive recursive and that the linearity of ≺ can be proved in PRA. (OT, ≺, o) is an ordinal notation system from below, if for some primitive recursive relation ≺′ the following holds: (Below 1) PRA ⊢ ∀a⃗ η OT^{∗}.NF(f(a⃗)) → ∀i < seqlength(a⃗).a_{i} ≺ f(a⃗). (Below 2) PRA ⊢ ∀a⃗ η OT^{∗}.∀b η OT.NF(f(a⃗)) → b ≺ f(a⃗) →

((∃i < seqlength(a⃗).b ⪯ a_{i}) ∨ ∃c⃗ ≺′ a⃗.b =_{NF} f(c⃗)). (Below 3) TI_{(NF(f)∩R^{∗},≺′)} is PRA-reducible to TI_{(OT∩R,≺)} for a unary free

predicate R.

(b) Assume that F = (f_{i}, nf_{i})_{1≤i≤n} is a system of ordinal functions, (OT, ≺, o) is the ordinal notation system defined from (f_{i}, nf_{i}), and assume that it is primitive recursive. (f_{j}, nf_{j}) is a part of (OT, ≺, o) from below, if the conditions from (a) hold with OT_{F}, ≺_{F}, o_{F} instead of OT, ≺, o and f := f_{j}.

Remark: In Corollary 5.8 (b) we will see that ordinal notation systems from below have order type less than the Bachmann-Howard ordinal. Naturally we would like to get beyond this bound in a way which is still from below. One idea is to weaken condition (Below 3) and allow proof theoretically stronger principles for the reduction of ≺′ to ≺. This will be considered in a future article where we will reach at least the strength of systems which require usually one large cardinal (one inaccessible). Another approach was taken by Feferman (1970), Howard (1970) by taking finite and later by Aczel (1972) by taking transfinite types to denote ordinals. This approach can be seen in the spirit of our first two conditions, although it is not directly comparable. Again we need proof theoretically stronger principles in order to show that all ordinals below some notation are introduced before it, namely the use of higher types.

In all our examples, TI over ≺′ (where ≺′ is the ordering of the arguments we defined there) was PRA-reducible to TI over ≺: ≺′ could be obtained from ≺ by a combination of the lexicographic ordering on pairs (Lemma 3.5 (e)), the lexicographic ordering on descending sequences (Lemma 3.5 (f)), the union of orderings (Lemma 3.5 (d)), the selection of a subset of a ordering (Lemma 3.5 (b)), reordering of the arguments and moving to isomorphic orderings (Lemma 3.5 (g)). Therefore these systems were ordinal notation systems from below.

4 The Accessible Part

Definition 4.1 Assume T is an extension of PRA. Acc(A, ≺) is the accessible part of (A, ≺) in T, iff in T follows:

(Acc 1) Prog_{(A,≺)}(Acc(A, ≺))

(Acc 2) For every class B of T Prog_{(A,≺)}(B) → Acc(A, ≺) ⊂ B. (Acc 2) is called induction over the accessible part. We write Acc(A), if the choice of ≺ is clear, and Acc, if A ≡ OT, where the choice of OT is clear from the context.

Remark 4.2 Under the assumptions of Definition 4.1 follows:

(a) T ⊢ Acc(A, ≺) ⊂ A.

(b) T ⊢ ∀n η Acc(A, ≺).A ∩ n_{≺} ⊂ Acc(A, ≺).

(c) For every class B of T we have TI_{(Acc(A,≺),≺)}(B).

Proof: induction on Acc(A, ≺).

We will see later that Martin-Löf’s type theory with one universe containing a type atom(t) and one non nested W-type is a theory in which we can define the accessible part of primitive recursive linear orderings.

Lemma 4.3 Assume that (OT, ≺) is a primitive recursive ordinal notation system, and T is a theory such that T proves induction over the natural numbers for arbitrary formulas, PRA can be interpreted in T, and we can define in T the accessible part Acc(OT, ≺).

(a) If (f, nf) is a part of (OT, ≺) which is from below, then T ⊢ ∀a⃗ η nf(f) ∩ Acc^{∗}.f(a⃗) η Acc.

(b) If (OT, ≺) is from below, then T ⊢ TI_{(OT,≺)}(B) for every class B.

Proof: (a) We argue in T. Let B := {a⃗ η nf(f) | f(a⃗) η Acc}. We have that TI_{(nf(f)∩Acc^{∗},≺′)}(B) follows from TI_{(Acc,≺)}(B′) for some class B′. By assumption, the latter formula is provable, therefore it suffices to show Prog_{(nf(f)∩Acc^{∗},≺′)}(B). Now assume a⃗ η nf(f) ∩ Acc^{∗}, nf(f) ∩ Acc^{∗} ∩ a_{≺′} ⊂ B (this is called the main-IH). We show ∀b η OT ∩ A.b ≺ f(a⃗) → b η Acc — we call this formula (∗) — by side-induction on length(b): If b ⪯ a_{i} for some i, then by a_{i} η Acc follows b η Acc. Otherwise, b =_{NF} f(b⃗) with b⃗ ≺′ a⃗. b_{i} ≺ b ≺ f(a⃗), therefore by side-IH b⃗ η nf(f) ∩ Acc^{∗}, by main-IH b = f(b⃗) η Acc. By f(a⃗) η OT and Acc ∩ f(a⃗)_{≺} ⊂ Acc follows now f(a⃗) η Acc. (b) From (a) follows by induction on length(b) ∀b η OT.b η Acc. We can deduce now transfinite induction on OT from induction over Acc.

Therefore no ordinal notation system from below suffices to denote the prooftheoretic ordinal of a theory, in which we can define the accessible part for primitive recursive linear orderings.

The following lemma allows to reduce transfinite induction over the closure of a class by one application of an ordinal function from below to transfinite induction over the class itself:

Lemma 4.4 Assume that (OT, ≺) is a primitive recursive ordinal notation system defined from ordinal functions (f_{i}, nf_{i}), the linearity of ≺ can be proved in PRA and that with f := f_{0}, nf := nf_{0} (f, nf) is a part from below. Let A be a free predicate, B := {a η OT | a η A ∨ ∃b⃗ η (OT ∩ A)^{∗}.a =_{NF} f(b⃗)}. Then TI_{(OT∩B,≺)} is PRA-reducible to TI_{(OT∩A,≺)}.

Proof: Assume Prog_{(OT∩B,≺)}(Q). First we show ∀a η OT ∩ A.OT ∩ B ∩ a ⊂ Q by (main-)induction over OT ∩ A: Assume a η A, ∀b ≺ a.b η OT∩A → OT∩B∩b ⊂ Q. By Prog_{(OT∩B,≺)}(Q) follows OT ∩ A ∩ a ⊂ Q. We show ∀b⃗ η (OT ∩ A)^{∗}.NF(f(b⃗)) → f(b⃗) ≺ a → f(b⃗) η Q by (side-)induction on ≺′, the ordering referred to in the definition of “f is a part from below”, using that ≺′ is PRA-reducible to ≺. Assume b⃗ η (OT ∩ A)^{∗}, f(b⃗) ≺ a, NF(f(b⃗)) and the assertion for b⃗′ ≺′ b⃗.

We show ∀c ≺ f(b⃗).c η OT∩B → c η Q. If c η A, we are done. Assume therefore c =_{NF} f(c⃗), c⃗ η (OT ∩ A)^{∗}. c ≺ f(b⃗), therefore c ⪯ b_{i} (and by main-IH, since b_{i} ≺ f(b⃗) ≺ a, OT ∩ B ∩ b_{i} ⊂ Q, c η Q) or c =_{NF} f(c′) for some c′ ≺′ b⃗, c′ = c⃗, c_{i} ≺ c ≺ f(b⃗) ≺ a, by side-IH f(c⃗) η Q and the proof of (∗) is complete. Now by Prog_{(OT∩B,≺)}(Q) follows f(b⃗) η Q and the side induction is complete. Therefore we have OT ∩ B ∩ a ⊂ Q and the main induction is complete. By Prog_{(OT∩B,≺)}(Q) follows ∀b η OT ∩ A.b η Q. Now using the same proof as in the inductive proof above (using instead of the main-IH OT ∩ A ⊂ Q), we show ∀b⃗ η (OT ∩ A)^{∗}.NF(f(b⃗)) → f(b⃗) η Q and therefore ∀b η OT ∩ B.b η Q.

Definition 4.5

(a) Let (ML) be intensional Martin-Löf’s type theory in the polymorphic formulation with sets N, N_{i}, Σ, Π, +, list and I, where I is the intensional identity type, using the logical framework.

(b) In order to avoid having to write El we define x ∈ (x_{1} : A_{1}, …, x_{n} : A_{n})B as x : (x_{1} : A_{1}, …, x_{n} : A_{n})El(B), further, if in an expression (x_{1} : A_{1}, …, x_{n} : A_{n}) a variable is not mentioned, i.e. it is of the form (…, A, …), this should be read as (…, x : El(A), …) for a fresh variable x.

(c) We write r =_{A} s for I(A, r, s). 𝔹 := N_{2}, false := 0_{2}, true := 1_{2}. We write f(r) instead of Ap(f, r), which does not cause any confusion with the logical framework function application, since it is distinct from this by the arity of f.

(d) (ML) + (atom) is the extension of (ML) by the type atom(t) with the following rules: atom : (𝔹) Set, atom(false) = N_{0}, atom(true) = N_{1}.

(e) (ML)+(atom)+(O_{1}) is the extension of (ML)+(atom) by the types Br(x) and O_{1} (which stands for for Kleene’s O) with the rules Br : (N_{3}) Set, Br(0_{3}) = N_{0}, Br(1_{3}) = N_{1}, Br(2_{3}) = N; O_{1} set, sup ∈ (r ∈ N_{3}, (Br(r))O_{1})O_{1}, and the usual elimination rules for the W-type O_{1} (= Wx ∈ N_{3}.Br(x)).

(f) Let (ML) + (atom) + (W) be the extension of (ML) + (atom) by the rules for the W-type.

In (d) we chose the notation atom(t), which stands for “atomic formula” and is used by Schwichtenberg. In (Smith 1988) atom(t) was denoted by T(a). In (e) the addition of the type Br(s) is not necessary, by using the type atom(s) it can be replaced by atom(f_{1}(s)) + atom(f_{2}(s)) × N, where

f_{i}(j_{3}) = \begin{cases}true & if i = j \\ false & if i ≠ j. \end{cases} It is only added to avoid coding.

We can interpret PRA in a straight forward way into (ML) + (atom) + (O_{1}). Further we can define Acc in the following way:

Definition 4.6 Let (OT, ≺) be a primitive recursive ordinal notation system from below. Let n_{0} ∈ N such that ¬(n_{0} η OT).

(a) Let index ∈ (O_{1})N_{3} and pred ∈ (w ∈ O_{1}, Br(index(w)))O_{1} such that index(sup(r, s)) = r and pred(sup(r, s), t) = s(t).

(b) For n ∈ N, w ∈ O_{1} we define w[n] ∈ O_{1} such that sup(0_{3}, s)[n] = sup(0_{3}, s), sup(1_{3}, s)[n] = s(0_{1}), sup(2_{3}, s)[n] = s(n).

(c) By recursion on l ∈ list(N) we define w[l]_{list} ∈ O_{1} such that w[nil]_{list} = w, w[cons(n, l)]_{list} = w[n][l]_{list}.

(d) Acc := {a η OT | ∃w ∈ O_{1}.∃f ∈ (list(N) → N).Correct(w, f) ∧ f(nil) =_{N} a}, where Correct(w, f) := ∀l ∈ list(N).f(l) η OT → (index(w[l]_{list}) =_{N_{3}} 2_{3}∧ ∀a η OT.a ≺ f(l) → f(append(l, cons(a, nil))) =_{N} a)

and append(l, l′) is the concatenation of the lists l, l′.

Correct(w, f) means that the function f, a labeling function for the subtrees of w, is in accordance with the ordering of w.

Lemma 4.7 Acc as defined above is an accessible part for (OT, ≺).

Proof: First we have to show that, if a ∈ N, p ∈ (a η OT), q ∈ (OT ∩ a ⊂ Acc), then a η Acc. From q we can extract s ∈ (N)O_{1} and g ∈ (N, list(N))N such that, if n η OT and n ≺ a, then index(s(n)) = 2_{3}, g(n, nil) =_{N} n, Correct(s(n), (l)g(a, l)), and if ¬(n η OT) or ¬(n ≺ a), then index(s(n)) = 0_{3}, g(n, l) = n_{0} (the element not in OT). We define now w := sup(2_{3}, s) and f such that f(nil) = a, f(cons(n, l)) = g(n, l) and conclude Correct(w, f) and therefore a η Acc. Further we have to show that, if B ∈ Cl(N) and p ∈ Prog_{(OT,≺)}(B), then Acc ⊂ B. It suffices to show that for all w ∈ O_{1}, f ∈ list(N) → N, p ∈ Correct(w, f) from f(nil) η OT follows f(nil) η B. This will be done by induction on w. By Correct(w, f), f(nil) η OT follows w = sup(2_{3}, s) for some s, for all b η OT, b ≺ f(nil) we have Correct(s(b), λl.f(cons(b, l))), f(cons(b, nil)) =_{N} b, b η OT, b η B, therefore by Prog_{(OT,≺)}(B) f(nil) η B, the assertion.

5 Well-ordering Proofs for (ML) + (atom) + (O_{1})

(ML) + (atom) + (O_{1}) allows to define the accessible part. Therefore its proof theoretic strength can not be expressed in such systems and we need to define ordinal notation systems, which are not from below. The traditional way of defining such systems is to violate the condition (Below 1). The idea goes back to Bachmann (1950). We will follow the most refined version, introduced by Buchholz (1986).

We start with ordinal functions which are from below and take here CNF. Further we add one ordinal Ω. We will violate (Below 1) and define ordinals smaller than Ω by using ordinals bigger than Ω. Therefore Ω has to be chosen in such a way that these ordinals can be shown to be smaller than Ω. One approach in order to obtain this is by choosing Ω := ℵ_{1}, the first uncountable cardinal and observing that the set of ordinals which are supposed to be below Ω form a countable segment of the ordinals and are therefore actually below Ω. We will take this approach here. In a refined approach, one defines Ω := ω_{1}^{ck} and observes that the set of ordinals below Ω form a segment which can represented by a primitive recursive ordinal notation system and is therefore below Ω.

As long as we add no further functions or only extend the part from below, we have not violated (Below 1) and can easily see that in fact we have defined an ordinal notation system from below. We add a function ψ : Ord → Ord, violating (Below 1), defined by recursion on the first argument. In the ordinal notation system defined by CNF, Ω and ψ we will have a value ψ(Ω), although we might denote later new ordinals below Ω using ordinals greater than Ω. Therefore below ψ(α) there should be only ordinals ψ(β) which we can define before ψ(α). “Before ψ(α)” will now be defined similarly as for ordinal notation systems from below: Let f be the function unifying CNF, Ω, ψ (we need the additional constant 0 to reach the indices of the functions), namely f() = 0, f(0, α_{1}, n_{1}, …, α_{k}, n_{k}) := CNF(α_{1}, n_{1}, …, α_{k}, n_{k}), f(1) = Ω and f(2, α) = ψ(α). Then f(α⃗) is defined before f(β⃗), if α⃗ is lexicographically smaller than β⃗. The set of ordinals previously defined is the smallest set C(α) closed under f restricted to lexicographic smaller arguments than (2, α): the closure of {0, Ω} under CNF and λβ < α.ψ(β). Now ψ(α) will be defined as the least ordinal which was not reached yet, i.e. ψ(α) := min{γ | γ ∉ C(α)}. We will see later that C(α) ∩ Ω is always a segment. If α ∈ C(α), α < β then ψ(α) ∈ C(β) ∩ Ω, ψ(α) ≠ ψ(β). If α ∉ C(α), then ψ(α) = ψ(α′) for α′ := min{γ > α | γ ∈ C(α)} and α′ ∈ C(α′). Therefore a good normal form for ψ is NF(ψ(α)) ⇔ α ∈ C(α), and we will restrict C(α) by closing it under ψ with arguments only in normal form. Definition 5.1

(a) We define simultaneously C(α) ⊂ Ord and ψ(α) by recursion on α: C(α) is the least set such that 0, Ω ∈ C(α), C(α) closed under CNF applied to arguments in normal form, and, if β ∈ C(α), β ∈ C(β), β < α, then ψ(β) ∈ C(α). ψ(α) := min{γ | γ ∉ C(α)}.

(b) The normal forms of the functions 0, Ω, CNF and ψ are defined by 0 =_{NF} 0; Ω =_{NF} Ω; NF(CNF) is defined as before (with the exception ¬NF(CNF()); NF(ψ(α)) iff α ∈ C(α).

(c) ω_{0}(α) := α, ω_{n+1}(α) := ω^{ω_{n}(α)}. Lemma 5.2

(a) 0 < ψ(α) < Ω.

(b) α < β → ψ(α) ≤ ψ(β) ∧ C(α) ⊂ C(β).

(c) If α is a limit ordinal, then C(α) = ⋃_{ξ<α} C(ξ) and ψ(α) = sup{ψ(ξ) | ξ < α ∧ ξ ∈ C(ξ)}.

(d) C(α) ∩ Ω is a segment of Ord.

(e) C(α) ⊂ ϵ_{Ω+1}, where ϵ_{Ω+1} is the first fixed point of λβ.ω^{β} above Ω. Proof: C(α) is countable, therefore ψ(α) < Ω. (d) follows by induction on α. The other proofs are easy. Remark: The only property needed for Ω is that Lemma 5.2 (a) holds (and that it is an ϵ-Number). Below we will see that for every α there is a primitive recursive ordinal notation system denoting all ordinals in C(α), especially all ordinals below ψ(α). Therefore ψ(α) < ω_{1}^{ck} and we can replace Ω by ω_{1}^{ck}. The details of this argument can be found for instance in (Rathjen 1993).

Lemma 5.3 Let γ =_{NF} CNF(α_{1}, n_{1} …, α_{k}, n_{k}), δ =_{NF} CNF(β_{1}, m_{1}, …, β_{l}, m_{l}), ρ =_{NF} ψ(α), ν =_{NF} ψ(β).

(a) γ < δ ⇔ ((α_{1}, n_{1}), …, (α_{k}, n_{k})) <_{lex,lex} ((β_{1}, m_{1}), …, (β_{l}, m_{l})). γ = δ ⇔ ((α_{1}, n_{1}), …, (α_{k}, n_{k})) = ((β_{1}, m_{1}), …, (β_{l}, m_{l})).

(b) α_{i}, n_{i} < γ; γ < ρ ⇔ α_{1}, …, α_{k} < ρ; γ ≠ ρ.

(c) ρ = ν ⇔ α = β; ρ < ν ⇔ α < β.

(d) α ≠ ρ.

(e) 0 < γ ≠ Ω; γ < Ω ⇔ α_{1}, …, α_{k} < Ω.

(f) ((0, nf_{0}), (Ω, nf_{Ω}), (CNF, nf_{CNF}), (ψ, nf_{ψ})) is a system of ordinal functions with normal forms.

Proof: (c): we have that, if α < β, then α ∈ C(α) ⊂ C(β), ψ(α) ∈ C(β) ∩ Ω, ψ(α) < ψ(β) = sup(C(β) ∩ Ω). (d): ρ =_{NF} ψ(α), therefore α ∈ C(α), ψ(α) ∉ C(α). (f): (NF1) follows from Lemma 5.2 (a) and the previous assertions of the lemma. (NF2): Assume (α_{1}, …, α_{k}) ∈ dom(f_{i}), α_{i} ∈ Closure(F, ρ) =: Closure, δ := f_{i}(α_{1}, …, α_{k}). If f_{i} = 0, Ω we have nothing to prove. If f_{i} = CNF, δ = α_{i} ∈ Closure, δ = 0 ∈ Closure, or δ =_{NF} CNF(β_{1}, m_{1} …, β_{k}, m_{k}), where β_{1}, m_{1}, …, β_{k}, m_{k} is the result of deleting some pairs (α, m) at even positions in (α_{1}, …, α_{k}), therefore δ ∈ Closure. If f_{i} = ψ, then with α′ := min{ρ ≥ α | ρ ∈ C(α)} (which exists, since α < ω_{n}(Ω + 1) ∈ C(α) for some n ∈ ω) we have ∀α′′.α ≤ α′′ ≤ α′ → C(α′′) = C(α′) ∧ ψ(α′′) = ψ(α′), ψ(α) = ψ(α′), further C(α′) ⊂ Closure, α′ ∈ C(α′), α′ ∈ Closure, NF(ψ(α′)), δ = ψ(α′) ∈ Closure.

Definition 5.4 Let F := ((0, nf_{0}), (Ω, nf_{Ω}), (CNF, nf_{CNF}), (ψ, nf_{ψ})) By induction on max{length(s), length(t)} we define for s, t η T_{F} simultaneously whether t η OT, s˜≺t and whether s η C̃(t). We write s˜⪯t for s˜≺t ∨ s = t. Further we define s ≺ t :⇔ s, t η OT ∧ s˜≺t, s ⪯ t :⇔ s, t η OT ∧ s˜⪯t and s η C(t) :⇔ s, t η OT ∧ s η C̃(t). All functions and relations will be primitive recursive. Let n̂ := CNF(0^{2n}), N̂ := {n̂ | n ∈ ℕ}.

(a) 0 η OT; 0˜≺t iff t ≠ 0; 0 η C̃(t).

(b) Let s⃗m := (s_{1}, m_{1}, …, s_{k}, m_{k}), t⃗n := (t_{1}, n_{1}, …, t_{l}, n_{l}). CNF(s⃗m) η OT iff s_{1}, …, s_{k} η OT, m_{i} η N̂, k ≥ 1, s_{k} ˜≺ ⋯ ˜≺s_{1} and, if k = 1 and m_{1} = 0, then s_{1} is not of the form ψ(t′) or Ω. CNF(s⃗m)˜≺CNF(t⃗n) iff ((s_{1}, m_{1}) …, (s_{k}, m_{k}))˜≺_{lex,lex}((t_{1}, n_{1}), …, (t_{l}, n_{l})) (which reduces to ˜≺). If t = ψ(t′) ∨ t = Ω, then CNF(s⃗m)˜≺t iff s_{1} ˜≺t ∧ ⋯ ∧ s_{k} ˜≺t. CNF(s⃗m) η C̃(t′) iff s_{1}, …, s_{k} η C̃(t′).

(c) ψ(r) η OT iff r η OT ∧ r η C̃(r); ψ(r)˜≺ψ(s) iff r ˜≺s; ψ(r)˜≺Ω; ψ(r) η C̃(t) iff r η C̃(t) and r ˜≺t.

(d) Ω η OT; Ω η C̃(t).

(e) If for r, t η T_{F} r ˜≺t is not decided by (a) - (d) then t = r or whether t˜≺r holds is decided by the above clauses and we define r ˜≺t iff ¬(t˜⪯r).

Lemma 5.5 Let OT, ≺, C, F be as in Definition 5.4

(a) (OT, ≺) = (OT_{F}, ≺_{F}).

(b) For a η OT in set theory holds {o(b) | b η C(a)} = C(o(a)).

(c) We can prove in PRA that for a, b η OT we have a ≺ ψ(b) ⇔ a η C(b) ∩ Ω.

(d) (OT, ≺) and C are primitive recursive and therefore F defines a primitive recursive ordinal notation system.

An outline of the well-ordering proof is as follows: Let Acc be the accessible part of the ordinals below Ω and define A_{n} as closure of Acc ∪ {Ω} under ntimes application of CNF. Using transfinite induction over Acc we conclude transfinite induction over Acc∪{Ω}, which is A_{0}. Using that CNF is from below we can show transfinite induction over A_{n} for every n (but not uniformly for all n). Using transfinite induction we can show that, if a η A_{n}, a η C(a), then C(a) ∩ ω_{n}(Ω + 1) ⊂ A_{n} and therefore ψ(a) = sup(C(a) ∩ Ω) η A_{n}. We conclude ψ(ω_{n}(Ω + 1)) η A_{n+1} ∩ Ω ≅ Acc and, since Acc is a segment of OT, transfinite induction up to ψ(ω_{n}(Ω + 1)).

Definition 5.6

(a) For a η OT we define the finite subset P(a) ⊂ OT ∩ Ω (which can be represented as a list of natural numbers in type theory) by: P(0) := P(Ω) := ∅; P(CNF(a_{1}, n_{1}, …, a_{k}, n_{k})) := P(a_{1}) ∪ ⋯ ∪ P(a_{k}); P(ψ(c)) := {ψ(c)}.

(b) Acc^{+} := {a η OT | P(a) ⊂ Acc}; A_{n} := Acc^{+} ∩ ω_{n}(Ω + 1).

Since Acc is closed under CNF, Acc^{+} is the closure of Acc ∪ {Ω} under CNF and A_{n} the closure of the same set under n times application of CNF.

Lemma 5.7 In (ML) + (atom) + (O_{1}) we can show:

(a) N̂ ⊂ Acc.

(b) ∀a_{1}, …, a_{k} η Acc.∀n_{1}, …, n_{k} η N̂.NF(CNF(a_{1}, n_{1}, …, a_{k}, n_{k})) → CNF(a_{1}, n_{1}, …, a_{k}, n_{k}) η Acc.

(c) Acc^{+} ∩ Ω ≅ Acc ∩ Ω.

(d) For every n and every B ∈ Cl(N) (these quantifiers are Meta-quantifiers) TI_{(A_{n},≺)}(B).

(e) For every n ∀a η A_{n}.NF(ψ(a)) → ψ(a) η Acc.

(f) For every B ∈ Cl(N) we have Prog_{(OT,≺)}(B) → ∀a η OT.a ≺ ψ(ω_{n}(Ω + 1)) → a η B,

Proof: (b) By Lemma 4.3 (a), since 0, CNF form together a part of (OT, ≺) which is from below. (c): by (b). (d): By Meta induction on n for all B: n = 0: Assume Prog_{(A_{0},≺)}(B). Since A_{0} ∩Ω ≅ Acc∩Ω, we have Prog_{(Acc,≺)}({a | a ≺ Ω → B}), therefore ∀a η Acc.a ≺ Ω → a η B, ∀a η A_{0} ∩ Ω.a η B, by Prog_{(A_{0},≺)}(B) therefore Ω η B, ∀a η A_{0}.a η B. n → n + 1: A_{n+1} is the onetimes closure of A_{n} under CNF and we can reduce by Lemma 4.4 TI_{(OT∩A_{n+1},≺)} to TI_{(OT∩A_{n},≺)}, since CNF forms a part from below.

(e) We show using TI_{(A_{n},≺)} that ∀a η A_{n}.a η C(a) → ψ(a) η Acc: Assume the IH. We show ∀c η C(a)∩ω_{n}(Ω+1).c η A_{n} by induction on length(c): 0 η A_{n}. Ω η A_{n}. If c =_{NF} CNF(a_{1}, n_{1}, …, a_{k}, n_{k}) with a_{i} η C(a), then a_{i} ≺ ω_{n}(Ω + 1), by IH a_{i} η A_{n}, P(CNF(a_{1}, n_{1}, …, a_{k}, n_{k})) ≅ P(a_{1}) ∪ ⋯ ∪ P(a_{k}) ⊂ Acc, c η A_{n}. If c =_{NF} ψ(c′), c′ η C(a), c′ ≺ a, c′ η A_{n}, then c′ η C(c′) ∩ ω_{n}(Ω + 1), by IH ψ(c′) η Acc ∩ Ω ⊂ A_{n}. Now the side-induction is complete and we have ∀c η C(a)∩Ω.c η A_{n} ∩Ω ≅ Acc, OT∩ψ(a) ⊂ Acc, ψ(a) η Acc. (f) ω_{n}(Ω+1) η A_{n+1}, therefore ψ(ω_{n}(Ω + 1)) η Acc, and by TI_{(Acc,≺)} follows the assertion.

Corollary 5.8

(a) |(ML) + (atom) + (O_{1})| ≥ ψ_{0}(ϵ_{Ω+1}) = sup_{n∈ω} ψ_{0}(ω_{n}(Ω + 1)).

(b) Ordinal notation systems from below have order type smaller than the Bachmann-Howard ordinal.

Proof: (a) By Lemma 5.7 (f). (b): 4.3 (b), 4.7 and (a) of this Corollary. Remark: This bound is sharp.

6 Well-ordering Proofs for (ML) + (atom) + (W)

We now extend the ordinal notation system and the well-ordering proof from the last section to Martin-Löf’s type theory with full W-type.

In the last section, using one non nested W-type we could define the accessible part of any ordinal notation system OT and define Acc^{+}, the class of ordinals such that the components below Ω_{1} are in Acc. Further we could prove transfinite induction up to A_{n} := Acc^{+}∩ω_{n+1}(Ω+1) and closure of A_{n} under ψ and therefore show transfinite induction up to ψ(ω_{n}(Ω + 1)).

Now, with no restrictions on the nesting of W-types, we can define the accessible part of any class, especially the accessible part Acc_{2} of Acc^{+}. We can easily show that Acc ⊂ Acc_{2}, Ω η Acc_{2} and that Acc_{2} is closed under any ordinal functions from below and ψ. Therefore we have transfinite induction over any ordinal notation system having a part from below, Ω and ψ. An additional function which is not from below is needed in order to express the proof-theoretic ordinal of the theory considered.

The method used is just an iteration of what we did before. Call the old ψ, C now ψ_{1}, C_{1}. We need to add an ordinal Ω_{2} bigger than any ordinal for which we can prove that it is in Acc_{2}. We can use Ω_{2} := ℵ_{2} or in a refined approach, where Ω := ω_{1}^{ck}, Ω_{2} := ω_{2}^{ck}, the next admissible ordinal above ω_{1}^{ck}. Further, in order to really use Ω_{2}, we need another collapsing function ψ_{2}. ψ_{2} can now be defined similarly as ψ_{1} before. However, in order not to interfere with the original ψ, we want to guarantee that Ω_{1} < ψ_{2}(α) < Ω_{2}. Therefore we can define C_{2}(α) as the closure of Ω_{1} ∪ {Ω_{1}} under CNF, ψ_{2}(α) := min{γ | γ ∉ C_{2}(α)}.

We have to modify ψ_{1} as well, since the original definition is constant above ϵ_{Ω_{1}+1}. Therefore we add Ω_{2} to C_{1}(α) and close it under ψ_{2}. We could close it under arbitrary ψ_{2}, since the definition of ψ_{2} is complete. However, in the generalization which follows we have to define collapsing functions ψ_{n} for all n ∈ ω, and our first attempt would require to define them in decreasing order, which is not possible, since ω with the ordering > is not well-founded. Instead we define ψ_{1} and ψ_{2} simultaneously, which means that C_{1}(α) will be closed under λβ < α.ψ_{2}(β) instead of full ψ_{2}.

We already mentioned the extension to higher cardinals and collapsing functions and therefore get the following definition: Definition 6.1

(a) Let Ω_{0} := 0 and Ω_{n} := ℵ_{n} for 0 < n < ω.

(b) We define simultaneously for all n ∈ ω C_{n}(α) ⊂ Ord and ψ_{n}(α) by recursion on α: C_{n}(α) is the least set such that Ω_{n} ∪ {Ω_{k} | n ≤ k ∈ ω} ⊂ C_{n}(α), C_{n}(α) is closed under CNF with arguments in normal form and if β ∈ C_{n}(α), β ∈ C_{m}(β), β < α, n ≤ m < ω, then ψ_{m}(β) ∈ C_{n}(α). ψ_{n}(α) = min{γ | γ ∉ C_{n}(α)}.

(c) The normal forms nf_{0}, nf_{Ω}, nf_{CNF}, nf_{ψ} of the ordinal functions 0, λn.Ω_{n}, CNF and ψ are defined by 0 =_{NF} 0, Ω_{n} =_{NF} Ω_{n} iff 1 ≤ n < ω, NF(CNF(α_{1}, n_{1}, …, α_{k}, n_{k})) is defined as before, NF(ψ_{n}(α)) iff α ∈ C_{n}(α).

Lemma 6.2

(a) Ω_{n} < ψ_{n}(α) < Ω_{n+1}.

(b) α < β → ψ_{n}(α) ≤ ψ_{n}(β) ∧ C_{n}(α) ⊂ C_{n}(β).

(c) If α is a limit ordinal, then C_{n}(α) = ⋃_{ξ<α} C_{n}(ξ) and ψ_{n}(α) = sup{ψ_{n}(ξ) | ξ < α ∧ ξ ∈ C_{n}(ξ)}.

(d) C_{n}(α) ∩ Ω_{n+1} is a segment of Ord.

(e) C_{n}(α) ⊂ Ω_{ω}. Lemma 6.3 Let γ =_{NF} CNF(α_{1}, n_{1}, …, α_{k}, n_{k}), ρ =_{NF} ψ_{n}(α), ν =_{NF} ψ_{m}(β).

(a) γ < ρ ⇔ α_{1}, …, α_{k} < ρ; γ ≠ ρ.

(b) ρ = ν ⇔ α = β ∧ n = m; ρ < ν ⇔ n < m ∨ (n = m ∧ α < β).

(c) ρ ≠ α.

(d) γ < Ω_{n} ⇔ α_{1}, …, α_{k} < Ω_{n}; γ ≠ Ω_{n}.

(e) ((0, nf_{0}), (Ω, nf_{Ω}), (CNF, nf_{CNF}), (ψ, nf_{ψ})) is a system of ordinal functions with normal forms.

As before we can now define a primitive recursive ordinal notation system based on 0, CNF, λn.Ω_{n}, λn, α.ψ_{n}α. We write Ω_{n}, ψ_{n} instead of Ωn̂(0) and ψn̂. Remark 6.4 In (ML) + (atom) + (W) we can show: ∀a, b η OT.∀n ∈ N.NF(ψ_{n}(b)) → (a ≺ ψ_{n}(b) ↔ a η C_{n}(b) ∩ Ω_{n+1}).

Definition 6.5 Assume A ∈ Cl(N).

(a) W_{A} := Wn ∈ N.Degree_{A}(n), where Degree_{A}(n) := Σm ∈ N.m ≺ n ∧ m η A.

(b) index and pred are defined as in Definition 4.6.

(c) We define under the assumption w, w′ : W_{A} the sets w ≺_{W_{A}}^{1} w′ := ∃u ∈ Degree_{A}(index(w′)).pred(w′, u) =_{W_{A}} w and w ⪯_{W_{A}} w′ := ∃f ∈ (N → W_{A}).∃n ∈ N.f(0) =_{W_{A}} w′ ∧ f(n) =_{W_{A}} w∧

∀k ∈ N.k < n → f(k + 1) ≺_{W_{A}}^{1} f(k).

(d) For w ∈ W_{A} we define LocCor_{A}(w) (w is locally correct) by:

LocCor_{A}(w) := ∀u ∈ Degree_{A}(index(w)).index(pred(w, u)) =_{N} p_{0}(u). (p_{0} is the projection of an element of a Σ-type to its first component.)

(e) For w ∈ W_{A} we define Correct_{A}(w) (w is correctly defined) by: Correct_{A}(w) := ∀w′ ∈ W_{A}.w′ ⪯_{W_{A}} w → LocCor_{A}(w′).

(f) The accessible part of A is defined by

Acc(A) := {n | ∃w ∈ W_{A}.Correct_{A}(w) ∧ index(w) = n}. Lemma 6.6

(a) w ≺_{W_{A}}^{1} sup(r, s) ⇔ ∃u ∈ Degree_{A}(r).s(u) =_{W_{A}} w.

w ⪯_{W_{A}} sup(r, s) ⇔ w =_{W_{A}} sup(r, s) ∨ ∃u ∈ Degree_{A}(r).w ⪯_{W_{A}} s(u).

(b) LocCor_{A}(sup(r, s)) ⇔ ∀m ∈ N.∀p ∈ (m ≺ r ∧ m η A).index(s(<m, p>)) =_{N} m. Correct_{A}(sup(r, s)) ⇔ LocCor_{A}(sup(r, s)) ∧ ∀m ∈ N.∀p ∈ (m ≺ r ∧ m η A).Correct_{A}(s(<m, p>)).

(c) Acc(A) is an accessible part of (A, ≺) as defined in Definition 4.1 Proof: (a): obvious. (b) by (a). (c): (Acc 1) follows, since using the assertion we can construct a correct tree from trees of the assumption, and we have that it is correct by (b). In order to conclude (Acc 2), we show that, under the assumption if Prog_{(A,≺)}(B), by induction on the trees ∀w ∈ W_{A}.Correct_{A}(w) → index(w) η B. Definition 6.7

(a) By induction on length(a) we can define for a η OT, n ∈ ℕ the component set K_{n}(a) relative to Ω_{n}, which is a finite subset of OT. K_{n}(a) := {a}, if n ≥ 1 ∧ a ≺ Ω_{n}. Otherwise K_{n}(0) := ∅, K_{n}(Ω_{m}) := ∅, K_{n}(ψ_{m}(a)) := K_{n}(a), K_{n}(CNF(a_{1}, n_{1}, …, a_{k}, n_{k})) := ⋃_{i=1}^{k} K_{n}(a_{i}).

(b) We define simultaneously by Meta-recursion on n ∈ ℕ M_{n} ⊂ OT and Acc_{n}: M_{0} := OT, M_{n+1} := {a | a η OT ∧ K_{n+1}(a) ⊂ Acc_{n}}. Acc_{n} := Acc(M_{n}) ∩ Ω_{n+1}.

Remark 6.8 If n ≤ m, then K_{n}(a) ≅ K_{n}[K_{m}(a)] (K_{n}[M] := ⋃_{aηM} K_{n}(a)). Lemma 6.9

(a) M_{n+1} ∩ Ω_{n+1} ≅ Acc_{n}.

(b) If 0 ≤ n < m, then ∀a η M_{m}.K_{n+1}(a) ⊂ Acc_{n}.

(c) Acc_{n} ≅ Acc_{n+1} ∩ Ω_{n+1}.

(d) ∀0 < m ≤ n.Ω_{m} η Acc_{n}, N̂ ⊂ Acc_{n}.

(e) ∀a_{1}, …, a_{k} η Acc_{n}, n_{1}, …, n_{k} η N̂.NF(CNF(a_{1}, n_{1}, …, a_{k}, n_{k})) → CNF(a_{1}, n_{1}, …, a_{k}, n_{k}) η Acc_{n}.

(f) ∀a η Acc_{n}.∀m ≤ n.NF(ψ_{m}(a)) → ψ_{m}(a) η Acc_{n}.

(g) If n ∈ N ⇒ ϕ(n) set, then (∀a η OT.(∀b ≺ a.ϕ(b)) → ϕ(a)) → ∀a ≺ ψ_{0}(Ω_{n}).ϕ(a).

(h) |(ML) + (atom) + (W)| ≥ ψ_{0}(Ω_{ω}).

Proof: (a) For a ≺ Ω_{n+1} K_{n+1}(a) ≅ {a}. (b) induction on m using 6.8.

(c) “⊂”: ∀a η Acc_{n}.a η Acc_{n+1} ∩ Ω_{n+1} follows by induction on Acc_{n}. “⊃”: Acc_{n+1}∩Ω_{n+1} ⊂ M_{n+1}∩Ω_{n+1} ≅ Acc_{n} by (a). (d) k̂ η Acc_{n} is trivial. Ω_{0} η Acc_{n}. If m′ + 1 = m < n, Ω_{m} η M_{m}, by (a) and (c) M_{m} ∩ Ω_{m} ≅ Acc_{m′} ⊂ Acc_{m}, Ω_{m} η Acc_{m} ⊂ Acc_{n}. (e) By Lemma 4.3 (a).

(f) Induction on a η Acc_{n}. Assume the assumption for a′ ≺ a a′ η Acc_{n}. We show ∀b η C_{m}(a) ∩ Ω_{n+1} ∩ M_{m}.b η Acc_{n}, which we call (∗), by induction on length(b). If b ≺ Ω_{m}, then b η M_{m} ∩ Ω_{m} ≅ Acc_{m−1} ⊂ Acc_{n}. Assume now Ω_{m} ⪯ b. If b = 0 or b = Ω_{k}, b η Acc_{n}. If b =_{NF} CNF(b_{1}, m_{1}, …, b_{l}, m_{l}), b_{i} η C_{m}(a) ∩ Ω_{n+1} ∩ M_{m}, by side-IH b_{i} η Acc_{n} and by (e) b η Acc_{n}. Otherwise b =_{NF} ψ_{l}(c), c ≺ a ≺ Ω_{n+1}, m < l ≤ n, c η C_{m}(a). b η M_{m}, therefore (0 < m ∧ K_{m}(c) ≅ K_{m}(b) ⊂ Acc_{m−1}) ∨ m = 0, c η M_{m}, by side-IH c η Acc_{n} and by main-IH ψ_{l}(c) η Acc_{n}. The proof of (∗) is now complete and we have ψ_{m}(a) ∩ M_{m} ≅ C_{m}(a) ∩ Ω_{m+1} ∩ M_{m} ⊂ Acc_{n} ∩ Ω_{m+1} ≅ Acc_{m}. If m = 0, ψ_{m}(a) η M_{m}, and if 0 < m, K_{m}(ψ_{m}(a)) ≅ K_{m}(a) ⊂ Acc_{m−1} by a η Acc_{n} ⊂ M_{n} and (b), again ψ_{m}(a) η M_{m}. We conclude ψ_{m}(a) η Acc_{m} ⊂ Acc_{n}.

(g) Ω_{n} η Acc_{n+1}, therefore ψ_{0}(Ω_{n}) η Acc_{n+1} ∩ Ω_{1} ≅ Acc_{0}, therefore ∀a ≺ ψ_{0}(Ω_{n}).a η Acc_{0}, and from the assumptions about ϕ follows ∀a η Acc_{0}.ϕ(a) and the assertion. (h): ψ_{0}(Ω_{ω}) = sup_{n∈ω} ψ_{0}(Ω_{n}).

Bibliography

Aczel, P. (1972). Describing ordinals using functionals of transfinite type. J. Symb. Logic 37 (1), 35 – 47. Bachmann, H. (1950). Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordnungszahlen. Vierteljahresschrift der Naturforschenden Gesellschaft in Zürich, XCV, 5–37. Buchholz, W. (1986). A new system of proof-theoretic ordinal functions. Ann. Pure Appl. Logic, 32, 195 – 207. Buchholz, W. and Schütte, K. (1988). Proof theory of impredicative subsystems of analysis, Bibliopolis, Napoli. Feferman, S. (1970). Hereditarily replete functionals over the ordinals. In: Kino, A., Myhill, J. and Vesley, R.E. Intuitionism and Proof Theory. Amsterdam, North-Holland, pp. 289 - 301.

Gentzen, G. (1943). Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie. Math. Ann., 119, 149 – 161. Griffor, E. and Rathjen, M. (1994). The strength of some Martin-Löf type theories. Arch. math. Logic, 33, 347 – 385. Howard, W. (1970). Assignment of ordinals to terms for primitive recursive functionals of finite type. In: Kino, A., Myhill, J. and Vesley, R.E. Intuitionism and Proof Theory. Amsterdam, North-Holland, pp. 303 - 326. Jäger, G. (1983). A well-ordering proof for Feferman’s theory T_{0}. Arch. math. Logic, 23, 65 – 77. Martin-Löf, P. (1984). Intuitionistic type theory, Bibliopolis, Napoli. Nordström, B., Peterson, K. and Smith, J. (1990). Programming in Martin-Löf’s type theory. An introduction, Oxford University-Press, Oxford. Pohlers, W. (1989). Proof theory. An introduction. Springer Lecture Notes in Mathematics, vol. 1407, Springer, Berlin, Heidelberg, New York. Rathjen, M. (1991). Proof-theoretical analysis of KPM. Arch. math. Logic, 30, 377 – 403. Rathjen, M. (1993). How to develop proof–theoretic ordinal functions on the basis of admissible ordinals. Math. Log. Quarterly, 39, no. 1, 47 – 54. Rathjen, M. and Weiermann, A. (1993). Proof–theoretic investigations of Kruskal’s theorem. Ann. Pure Appl. Logic, 60, 49–88. Schütte, K. (1954). Kennzeichnung von Ordinalzahlen durch rekursiv definierte Funktionen. Math. Ann., 127, 16–32. Schütte, K. (1977). Proof Theory, Springer, Berlin, Heidelberg, New York. Seisenberger, M. (1994). Das Ordinalzahlbezeichnungssystem OT(ϑ) und seine Verwendung von Kruskals Satz. Masters Thesis, University of Munich, Dept. of Mathematics. Setzer, A. (1993). Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe, Ph.D. thesis, University of Munich, Department of Mathematics. Setzer, A. (1994). A type theory for iterated inductive definitions, Draft. Setzer, A. (1995). Well-ordering proofs for Martin-Löf Type Theory, submitted. Setzer, A. (1996). Extending Martin-Löf Type Theory by one Mahlo-Universe, submitted. Smith, J. (1988). The independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes. J. Symb. Logic, 53, 840 – 845. Troelstra, A. and van Dalen, D. (1988). Constructivism in mathematics. An introduction. Vol. II. North-Holland, Amsterdam.