Extending Martin-Löf Type Theory by One Mahlo-Universe

Anton Setzer ^{∗}

September 3, 1998

Abstract We define a type theory MLM, which has proof theoretical strength slightly greater then Rathjens theory KPM. This is achieved by replacing the universe in Martin-Löf’s Type Theory by a new universe V, which has the property that for every function f, mapping families of sets in V to families of sets in V, there exists a universe closed under f. We show that the proof theoretical strength of MLM is ≥ ψ_{Ω_{1}}Ω_{M+ω}. Therefore we reach a strength slightly greater than |KPM| and V can be considered as a Mahlo-universe. Together with [Se96a] it follows |MLM| = ψ_{Ω_{1}}(Ω_{M+ω}).

1 Introduction

An ordinal M is recursively Mahlo iff M is admissible and every M-recursive closed unbounded subset of M contains an admissible ordinal. Equivalently, this is the case iff M is admissible and for all Δ_{0} formulas ϕ(x, y, z⃗), and all z⃗ ∈ L_{M} such that ∀x ∈ L_{M}.∃y ∈ L_{M}.ϕ(x, y, z⃗) there exists an admissible ordinal β < M such that ∀x ∈ L_{β}∃y ∈ L_{β}.ϕ(x, y, z⃗) holds. One can easily see that M is inaccessible and that β can always be chosen to be inaccessible. On basis of this definition Rathjen has in [Ra91] developed a formulation called KPM of Kripke Platek set theory with one recursive Mahlo ordinal and has proof theoretically analyzed it ([Ra90, Ra91, Ra94]) — a major break through in proof theory after the treatment of inaccessibles. A universe in Martin-Löf Type Theory can be interpreted as the least fixed point of an operator, which, in the presence of the W-type, can be obtained by iterating this operator up to the first recursively inaccessible: we need one admissible to obtain closure under the inductive definition of U, but because this inductive definition refers to another inductive definition, which interprets the W-type, we need that this admissible is closed under the step to the next admissible. If we include a family of sets into the universe, the first inaccessible greater than the least α such that this family of sets is in L_{α} is needed. Therefore, the step to the next universe in type theory corresponds to the step to the next recursively inaccessible in set theory.

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

setzer@math.uu.se

In order to get a type-theoretic formulation of Mahloness, we replace therefore in the definition of recursive Mahlo in a first step inaccessibles by universes and Π_{2}-formulas by functions. We will arrive then at a universe V, which reflects functions V → V. However, we cannot decompose elements of V, the only elimination rule for V is the Tarski-operator (or decoding function) T. Therefore reference to functions f : V → V only is too weak. Instead (this idea goes back to E. Palmgren, who suggested this to the author in the Oberwolfach Meeting in Mathematical Logic 1995) we have to consider functions from families of sets in V, i.e. from Σx : V.T(x) → V, into itself. We arrive then at the following definition: V is a Mahlo-universe (together with Tarski-operator T), if V is a universe, and for every function f : (Σx : V.T(x) → V) → (Σx : V.T(x) → V) there exists an element Û_{f} : V, and a decoding function s_{f} : T(Û_{f}) → V such that (with U_{f} := T(Û_{f})) the following properties hold:

• U_{f} is a sub-universe of V, i.e. it is closed under ordinary type constructions. For instance, if a : U_{f} and x : T(s_{f}(a)) ⇒ b : U_{f}, then Σ̂_{f}x : a.b : U_{f}, and we have s_{f}(Σ̂_{f}x : a.b) = Σ̂_{V}x : s_{f}(a).s_{f}(b) : V, T(Σ̂_{V}x : a.b) = Σx : T(a).T(b).

• There exists the restriction of f to U_{f}: Res_{f} : (Σx : U_{f}.T(s_{f}(x)) → U_{f}) → (Σx : U_{f}.T(s_{f}(x)) → U_{f}) and with ι_{f} : (Σx : U_{f}.T(s_{f}(x)) → U_{f}) → (Σx : V.T(x) → V), ι_{f}(p(r, t)) := p(s_{f}(r), λx.s_{f}(t x)) we have ι_{f} ∘ Res_{f} = f ∘ ι_{f}.

In order to make it easier to work with the universe, we decompose the Σ-type and split therefore the function f into two functions g : V → (T(x) → V) → V and h : Πx : V.Πy : (T(x) → V).T(g x y) → V. Further we define first a set U_{g,h} inductively and then T(Û_{g,h}) := U_{g,h} (this was suggested by P. Martin-Löf). Note that the introduction of U_{g,h} is rather unproblematic and weak. That U_{g,h} can be represented in the form of Û_{g,h} as an element of V is, what makes this theory so strong. We give the resulting theory tentatively the name MLM for extension of Martin-Löf’s type theory by one Mahlo universe (note that this does not imply that this is a version of Martin-Löf’s type theory — this is still a matter of discussion). In this article we will introduce this type theory and carry out a series of well-ordering proofs, which show that the proof theoretical strength of MLM is ≥ ψ_{Ω_{1}}Ω_{M+ω}. This is done by extending the well-ordering proofs carried out in [Se98] and showing that MLM proves transfinite induction up to ψ_{Ω_{1}}Ω_{M+m} for every m ∈ ω. Since in [Se96a] we showed by modeling MLM in KPM^{+} that this is an upper bound as well, we have determined the precise proof theoretical strength. The content of this article, in which we mainly follow the proof in [Se98], is as follows: In Sect. 2 and 3 we show how to extend the ordinal notation system in [Bu93] (in which the approach of using H-controlled derivations of [Bu92] was applied to Rathjens KPM-paper [Ra91]) in order to reach the proof theoretical strength of MLM. In Sect. 4 we introduce the type theory by modifying the version with one ordinary universe ML_{J} treated in [Se98]. In Sect. 5 we carry out the well-ordering proofs themselves. We will use most of what is done in [Se98]. We only have to carry out some technical work in order to show closure under the ψ-function (Lemma 5.2) and have to show how to reach M. The latter is mainly achieved in Lemma 5.10. Here, assuming that a ∈ C^{a}(W), C^{a}(W) ∩ a ⊂ W, we define a function from families of sets in V to itself by adding to a given such family one distinguished element B in the power set of N (large enough such that a ∈ C^{a}(B)) and enlarge this family to a set of families such that, if the original family contains a distinguished set A, then C^{a}(A) ⊂ D for a distinguished set D in the new universe. The universe closed under this function Uf⃗ must now necessarily have as element the distinguished set B and have the property, if b ∈ C^{a}(Wf⃗) ∩ a, then, since it is closed under the function mentioned above, b ∈ D for some distinguished set D in the power set of N in Uf⃗, which means b ∈ Wf⃗. Since Wf⃗ is now an element of the power set in V, we obtain a distinguished set, which we can extend to a set A such that for the given a ∈ A^{W}(W) it follows that a ∈ A ⊂ W. From this it follows in 5.11 that, if ψ_{M}α ∈ A^{W}(W), then ψ_{M}α ∈ W, and we can add M to W in order to get a distinguished set containing M. Ω_{M+n} is then reached by putting the W-type on top of it as in [Se98]. The general technique for carrying out well-ordering proofs goes back to Buchholz and was first presented in [Bu75] and improved in [Bu90]. Related work. E. Palmgren’s studies of the super universe [Pa91] was a first major step towards the Mahlo universe. M. Rathjen, E. Griffor and E. Palmgren ([RGP98]) have defined and analyzed a substantial extension of the super universe. E. Palmgren has extended [Pa91] and defined a higher order universe ([Pa98]), which is conjectured by the author and M. Rathjen to have the strength of KPM. In [Pa98], E. Palmgren has also shown that adding elimination rules to the Mahlo universe leads to an inconsistency (in the author’s opinion this only shows that we do not know yet how to formulate the correct elimination rules for it). An alternative approach to the determination of lower bounds for type theories with W-type and one universe by interpreting versions of constructive set theory was taken by E. Griffor and M. Rathjen in [GR94]. Variations of the type theory : The well-ordering proof can be carried out as well (even more easily) in the formulation à la Russell. Using the techniques from [Se93], we can easily show that our upper bound is an upper bound for the version à la Russell as well, i.e. the strength of both formulations is the same. The well-ordering proof indicates that we do not need all functions from families of sets into itself, with P_{V}(N) := N → V reflection of functions P(N) → P(N) suffices. Preliminaries 1.1 In the following we will often refer to lemmata in [Se98], but with small changes, which we will indicate. In order to cite the lemmata shortly, we write “Lemma n.m of [Se98]” instead of “the adaption of Lemma n.m of [Se98] to the extended system”.

2 Ordinals in Set Theory

The set theoretical definition and analysis of the the ordinal functions can be found in the first part of [Bu93]. We only vary in so far as we replace M^{Γ} by Λ := min{α > M|α = ℵ_{α}} = sup{α_{n}|n ∈ ω} with α_{0} := M + 1, α_{n+1} := ℵ_{α}, consider ordinals up to Λ, and replace SC_{M} by our definition below. With this small variation all the proofs of the first section of the [Bu93] remain the same. Unfortunately, the third section, in which the ordering between ψ-terms is determined, has to be modified. We define γ =′_{NF} δ +ρ, γ =_{NF} δ +ρ, γ =_{NF} φ_{δ}ρ, γ =_{NF} Ω_{δ} as in [Se98], and γ =_{NF} ψ_{κ}α :⇔ γ = ψ_{κ}α ∧ κ, α ∈ C_{κ}(α). Definition 2.1

C^{0}(α, β) := β ∪ {0, M}
C^{n+1}(α, β) := C^{n}(α, β)
∪ {γ | ∃δ, ρ ∈ C^{n}(α, β).γ =′_{NF} δ + ρ ∨ γ =_{NF} φ_{δ}ρ
∨γ =_{NF} Ω_{δ} ∨ γ =_{NF} ψ_{δ}ρ}

As usual (or as in [Se98], Lemma 1.10) we can prove ⋃_{n<ω} C^{n}(Λ, 0) = C(Λ, 0) and ⋃_{n<ω} C^{n}(α, ψ_{κ}α) = C_{κ}(α). Definition 2.2 Assume α ∈ C(Λ, 0), κ ∈ R.

(a) For α ∈ C(Λ, 0) we define by recursion on min{n|α ∈ C^{n}(Λ, 0)} the set SC_{κ}(α):

SC_{κ}(α) := \begin{cases}∅, & if α = 0, M, \\ SC_{κ}(α_{1}) ∪ SC_{κ}(α_{2}), & if α =_{NF} α_{1} + α_{2} or α =_{NF} φ_{α_{1}}α_{2} or \\ & α =_{NF} Ω_{α_{1}} ∧ α_{1} = α_{2}, \\ \{α\}, & if α = ψ_{π}γ < κ, \\ SC_{κ}(π) ∪ SC_{κ}(γ), & if κ ≤ α = ψ_{π}γ, γ, π ∈ C_{π}(γ). \end{cases}

(b) By recursion on min{n|α ∈ C^{n}(Λ, 0)} we define G_{κ}(α) for α ∈ C(Λ, 0):

G_{κ}(α) := \begin{cases}∅, & if α = 0, M, \\ G_{κ}(α_{1}) ∪ G_{κ}(α_{2}), & if α =_{NF} α_{1} + α_{2} or α =_{NF} φ_{α_{1}}α_{2} or \\ & α =_{NF} Ω_{α_{1}} ∧ α_{1} = α_{2}, \\ ∅, & if α = ψ_{π}γ < κ, \\ G_{κ}(π) ∪ G_{κ}(γ) ∪ \{γ\}, & if κ ≤ α = ψ_{π}γ, γ, π ∈ C_{π}(γ). \end{cases}

(c)

sc_{κ}(α) := \begin{cases}SC_{κ}(α), & if κ = M, \\ ∅, & otherwise. \end{cases}

Lemma 2.3 Assume α ∈ C(Λ, 0).

(a) (ψ_{π}β = ψ_{κ}α ∧ π, β ∈ C_{π}(β) ∧ α, κ ∈ C_{κ}(α)) ⇒ (β = α ∧ κ = π).

(b) α < κ ⇒ G_{κ}(α) = ∅.

(c) SC_{κ}(α) ≤ min{κ, α}.

(d) α ∈ C_{κ}(β) ⇔ (SC_{κ}(α) < ψ_{κ}β ∧ G_{κ}(α) < β).

(e) (γ ∈ C_{κ}(α) ∧ κ ≤ M) ⇒ SC_{M}(γ) ⊂ C_{κ}(α).

(f) If β ∈ C_{M}(β), γ ∈ C_{M}(γ), then ψ_{M}β < ψ_{M}γ ⇔ (β < γ ∧ SC_{M}(β) < ψ_{M}γ) ∨ ψ_{M}β ≤ SC_{M}(γ).

(g) (κ, α ∈ C_{κ}(α) ∧ π, β ∈ C_{π}(β) ∧ ψ_{π}β < κ < π ∧ sc_{π}(β) < ψ_{κ}α) ⇒ ψ_{π}β < ψ_{κ}α.

Proof:

(a) Assume α ≠ β, w.l.o.g. α < β. Then κ, α ∈ C(α, ψ_{κ}α) ⊂ C(β, ψ_{π}β), ψ_{κ}α ∈ C_{π}(β) ∩ π = ψ_{π}β, a contradiction. Therefore C_{κ}(α) = C_{π}(β), κ = min{κ′ ∈ R|ψ_{κ}α < κ′} = π. (b), (c): immediate. (d): Induction on min{n|α ∈ C^{n}(Λ, 0)}. Case α < ψ_{κ}β: α ∈ C_{κ}(β) ⇔ SC_{κ}(α) ≤ α < ψ_{κ}β ∧ G_{κ}(α) = ∅ < β. Case ψ_{κ}β ≤ α =_{NF} α_{1} + α_{2}, =_{NF} φ_{α_{1}}α_{2} or α =_{NF} Ω_{α_{1}} ∧ α_{1} = α_{2}: α ∈ C_{κ}(β) ⇔ α_{1}, α_{2} ∈ C_{κ}(β), and the assertion follows by IH. Case ψ_{κ}β ≤ α = ψ_{π}γ < κ: ψ_{κ}β ∉ C_{κ}(β), SC_{κ}(α) = {α} ≮ ψ_{κ}β. Case κ ≤ α = ψ_{π}γ, γ, π ∈ C_{π}(γ): α ∈ C_{κ}(β) ⇔ (γ, π ∈ C_{κ}(β) ∧ γ < β) ⇔ (SC_{κ}(π) ∪ SC_{κ}(γ) < ψ_{κ}β ∧ G_{κ}(π) ∪ G_{κ}(γ) < β ∧ γ < β) ⇔ SC_{κ}(α) < ψ_{κ}β ∧ G_{κ}(α) < β. (e): Induction on min{n ∈ ω | γ ∈ C^{n}(α, ψ_{κ}α)}. If γ = 0, M, γ =_{NF} γ_{1} + γ_{2}, φ_{γ_{1}}γ_{2}, Ω_{γ_{1}}, the assertion follows directly or by IH. If γ =_{NF} ψ_{π}δ, π ≤ M, it follows SC_{M}(γ) = {γ} ⊂ C_{κ}(α). If γ =_{NF} ψ_{π}δ, M < π, it follows π, δ ∈ C_{κ}(α) and the assertion by IH.

(f) “⇐”: If β < γ ∧ SC_{M}(β) < ψ_{M}γ, it follows G_{M}(β) < β < γ, β ∈ C_{M}(γ), ψ_{M}β ∈ C_{M}(γ) ∩ M = ψ_{M}γ. If ψ_{M}β ≤ SC_{M}(γ), follows the assertion by SC_{M}(γ) < ψ_{M}γ. “⇒” Assume right side is wrong. Then SC_{M}(γ) < ψ_{M}β ∧ (γ ≤ β ∨ ψ_{M}γ ≤ SC_{M}(β)). If β = γ, it follows ψ_{M}β = ψ_{M}γ, otherwise by “⇐” ψ_{M}γ < ψ_{M}β, contradicting the assumption. (g): Ω_{π} = π. If κ = Ω_{ρ+1}, the assertion is easy. Assume κ = Ω_{κ}. κ < M, therefore κ =_{NF} ψ_{M}γ for some γ ∈ C_{M}(γ). By κ ∈ C_{κ}(α) it follows γ < α ∧ γ ∈ C_{κ}(α) ∩ C_{M}(γ). Therefore SC_{M}(γ) ⊂ C_{κ}(α)∩C_{M}(γ)∩M = ψ_{κ}α. Further G_{M}(γ) < γ. ψ_{π}β < κ = ψ_{M}γ < π. Therefore ψ_{M}γ ∉ C_{π}(β), β ≤ γ ∨ γ ∉ C_{π}(β), β ≤ γ ∨ ψ_{π}β ≤ SC_{π}(γ) ∨ β ≤ G_{π}(γ). If π = M ∧ ψ_{π}β ≤ SC_{π}(γ), it follows ψ_{π}β ≤ SC_{M}(γ) ≤ ψ_{κ}α, ψ_{π}β ≠ ψ_{κ}α and the assertion. If π = M ∧ β ≤ γ, it follows, since ψ_{π}β < κ = ψ_{M}γ, by (f) (β < γ ∧ SC_{M}(β) < ψ_{M}γ) ∨ ψ_{M}β ≤ SC_{M}(γ). If ψ_{M}β ≤ SC_{M}(γ), it follows by SC_{M}(γ) ≤ ψ_{κ}α and ψ_{π}β ≠ ψ_{κ}α the assertion. Otherwise we have G_{M}(β) < β < γ < α, SC_{M}(β) < ψ_{κ}α, β ∈ C_{κ}(α), ψ_{π}β ∈ C_{κ}(α) ∩ κ = ψ_{κ}α. If π = M ∧ β ≤ G_{π}(γ), it follows G_{π}(γ) ≤ γ, β ≤ γ and we get as before the assertion. The case π = M is therefore complete. If π < M, it follows from ψ_{M}γ < π < M, ψ_{π}β < ψ_{M}γ and by the case π = M ψ_{π}β ≤ sc_{M}(γ) ≤ ψ_{κ}α and by ψ_{π}β ≠ ψ_{κ}α therefore the assertion. If M < π, it follows Ω_{π} ≠ π. Theorem 2.4 Assume κ, α ∈ C_{κ}(α) ∧ π, β ∈ C_{π}(β). Then ψ_{π}β < ψ_{κ}α ⇔ π ≤ ψ_{κ}α

∨ψ_{π}β ≤ sc_{κ}(α)

∨(π = κ ∧ β < α ∧ sc_{π}(β) < ψ_{κ}α)
∨(ψ_{π}β < κ < π ∧ sc_{π}(β) < ψ_{κ}α).

Proof: “⇐” If π ≤ ψ_{κ}α, follows the assertion by ψ_{π}β < π, and if ψ_{π}β ≤ sc_{κ}(α), by sc_{κ}(α) < ψ_{κ}α. If π = κ ∧ β < α ∧ sc_{π}(β) < ψ_{κ}α, it follows, if π ≠ M, ψ_{π}β < ψ_{κ}α as in [Bu93] 1.6(b), otherwise we have SC_{M}(β) < ψ_{κ}α ∧ G_{M}(β) < β < α, π, β ∈ C_{κ}(α), therefore ψ_{π}β ∈ C_{κ}(α) ∩ κ = ψ_{κ}α. Otherwise follows the assertion by 2.3 (g). “⇒” If the right side is not fulfilled, we have π = α ∧ β = α or the right side with π, κ and α, β interchanged, therefore ψ_{κ}α ≤ ψ_{π}β.

3 The Notation system OT

Now we will introduce the ordinal notation system OT. We will work in Heyting-Arithmetic, which can be embedded in Martin-Löf’s Type Theory in a straightforward way. Preliminaries 3.1 In this section, a primitive recursive set is given by a primitive recursive function f such that ∀x ∈ ℕ.fx = 0 ∨ fx = 1. We write t ∈ A for ft = 1, if A is the set denoted by f. A ⊂ B :≡ ∀x ∈ ℕ.x ∈ A → x ∈ B and A ≅ B :≡ A ⊂ B ∧ B ⊂ A. In the following assume a, b, c, n, m, π, κ, λ ∈ N. We will, as usual in proof theory, first introduce a system of terms and an ordering on these terms, and then define the ordinal notation system OT as a subset of these terms. Definition 3.2 We give an inductive definition of sets T′, Suc′, P′, G′, Fi′, R′, Car′ of terms together with length(a) for a ∈ T′ ∪ Suc′ ∪ P′ ∪ G′ ∪ R′ ∪ Fi′ ∪ Car′, where we assume some coding of the terms as natural numbers. All the sets and length can be defined primitive recursively. (T′ is the set of terms, Suc′ the set of successor ordinals, P′ the additive principal numbers (except 0_{OT}), G′ the Gamma numbers, R′ the regular cardinals, Fi′ the fixed points of the function Ω_{·}, I′ the inaccessibles, i.e. the regular fixed points of the function Ω_{·}).

(T′ 1) 0_{OT} ∈ T′, length(0_{OT}) := 1. (T′ 2) If n > 0, a_{0}, …, a_{n} ∈ P′, then

t := (a_{0}, …, a_{n}) ∈ T′, if a_{n} ∈ Suc′, then t ∈ Suc′,

length(t) := length(a_{1}) + ⋯ length(a_{n}).

(T′ 3) If a, b ∈ T′, then t := φ′_{a}b ∈ P′, if a = b = 0_{OT}, then t ∈ Suc′, length(φ′_{a}b) := length(a) + length(b). 1_{OT} := φ′_{0_{OT}}0_{OT}.

(T′ 4) If b ∈ T′ π ∈ R′, then t := ψ_{π}b ∈ G′, and, if π = M, then t ∈ I′, and, if π ∈ I′, then t ∈ Fi′, length(t) := length(π) + length(b).

(T′ 5) If a ∈ T′, then t := Ω′_{a} ∈ G′, if a ≠ 0_{OT}, then t ∈ Car′, if a ∈ Suc′, then t ∈ R′, in all cases length(t) := length(a) + 1.

(T′ 6) M ∈ I′, length(M) := 1. (T′ 7) I′ ⊂ R′ ⊂ G′ ⊂ P′ ⊂ T′, I′ ⊂ Fi′ ⊂ Car′ ⊂ G′, Suc′ ⊂ T′.

Lim′ := T′ \ ({0_{OT}} ∪ Suc′). For a ∈ P′, (a) := a. () := 0. So for every a ∈ T′ there exists a unique n and unique a_{1}, …, a_{n} such that a = (a_{0}, …, a_{n}). After some change of the coding we assume 0 = 0_{OT}, 1 = 1_{OT}. In the following π, κ, λ will indicate elements of R′, a, b, c of T′, whereas n will be used for denoting natural numbers. Definition 3.3 By recursion on the length of length(a) + length(c) we define simultaneously the relation a ≺′ c and, if c = κ ∈ R′, finite sets SC_{κ}(a), sc_{κ}(a) and G_{κ}(a) such that ∀c ∈ sc_{κ}(a) ∪ G_{κ}(a).length(a) ≠ 0 → length(c) < length(a). In this definition a ⪯′ b is an abbreviation for a ≺′ b ∨ a = b, and for a finite set A a ⪯′ A stands for ∃x ∈ A.a ⪯′ x, A ≺′ a for ∀x ∈ A.x ≺′ a. Later we will define ≺ as the restriction of ≺′ to OT. a ≺′ b is false, if a ∉ T′ ∨ b ∉ T′ ∨ a = b.

(≺′ 1) c ≠ 0 → 0 ≺′ c. (≺′ 2) n + m ≥ 1, a_{0}, …, a_{n}, b_{0}, …, b_{m} ∈ P′, then (a_{0}, …, a_{n}) ≺′ (b_{0}, …, b_{n}) :↔

(n < m ∧ ∀i ≤ n.a_{i} = b_{i})∨

(∃j ≤ min{n, m}.∀i < j.a_{i} = b_{i} ∧ a_{j} ≺′ b_{j}).

(≺′ 3) If a, b, c, d ∈ T′, then (φ′_{a}b ≺′ φ′_{c}d) :↔

((a ≺′ c ∧ b ≺′ φ′_{c}d) ∨ (a = c ∧ b ≺′ d)∨
(c ≺′ a ∧ φ′_{a}b ⪯′ d)).

(≺′ 4) If a, b ∈ T′, c ∈ G′, then

(φ′_{a}b ≺′ c) :↔ (max{a, b} ≺′ c).

(≺′ 5) π, κ ∈ R′,a, b ∈ T′, then

(ψ_{π}a ≺′ ψ_{κ}b) :↔

(π ⪯ ψ_{κ}b∨
ψ_{π}a ⪯ sc_{κ}(b)∨
(π = κ ∧ a ≺′ b ∧ sc_{π}(a) ≺′ ψ_{κ}b)∨
(ψ_{π}a ≺′ κ ≺′ π ∧ sc_{π}(a) ≺′ ψ_{κ}b).

(≺′ 6) If π ∈ R′ \ I′, (κ = Ω′_{c} ∨ κ = M), b ∈ T′, then

(ψ_{π}b ≺′ κ) :↔ π ⪯′ κ.

(≺′ 7) b, c ∈ T′, π ∈ I′, then

(ψ_{π}b ≺′ Ω′_{c}) :↔ ψ_{π}b ⪯′ c.

(≺′ 8) If b ∈ T′, π ∈ I′, then

ψ_{π}b ≺′ M.

(≺′ 9) If a, c ∈ T′, then

(Ω′_{a} ≺′ Ω′_{c}) :↔ (a ≺′ c).

(≺′ 10) If a ∈ T′, then

(Ω′_{a} ≺′ M) :↔ (a ≺′ M).

(≺′ 11) In all other cases a ≺′ b :↔ ¬(b ⪯′ a).

SC_{κ}(a) := \begin{cases}∅, & if a = 0, M, \\ SC_{κ}(a_{1}) ∪ ⋯ ∪ SC_{κ}(a_{n}), & if a = (a_{1}, …, a_{n}), n ≥ 2, \\ SC_{κ}(a_{1}) ∪ SC_{κ}(a_{2}), & if a = φ′_{a_{1}}a_{2} ∨ (a = Ω′_{a_{1}} ∧ a_{1} = a_{2}), \\ \{a\} & a = ψ_{λ}c ≺′ κ, \\ SC_{κ}(λ) ∪ SC_{κ}(c), & if κ ⪯′ a = ψ_{λ}c. \end{cases}

sc_{κ}(a) := \begin{cases}SC_{M}(a), & if κ = M, \\ ∅ & otherwise. \end{cases}

G_{κ}(a) := \begin{cases}∅, & if a = 0, M, \\ G_{κ}(a_{1}) ∪ ⋯ ∪ G_{κ}(a_{n}), & if a = (a_{1}, …, a_{n}), n ≥ 2, \\ G_{κ}(a_{1}) ∪ G_{κ}(a_{2}), & if a = φ′_{a_{1}}a_{2} ∨ (a = Ω′_{a_{1}} ∧ a_{1} = a_{2}), \\ ∅, & if a = ψ_{λ}c ≺′ κ, \\ G_{κ}(λ) ∪ G_{κ}(c) ∪ \{c\}, & if κ ≺′ a = ψ_{λ}c. \end{cases}

We define for finite sets M, M′ M ⪯′ M′ :⇔ ∀x ∈ M∃y ∈ M′(x ⪯′ y), M ≺′ M′ :⇔ ∀x ∈ M∃y ∈ M′(x ≺′ y). Lemma 3.4 (≺′) is a linear ordering on T′. Proof: easy, but very long. Definition 3.5 (a) We define the (primitive-recursively decidable) subset Cr′(a) of T′:

0, (a_{1}, …, a_{n}) ∉ Cr′(a). φ′_{b}c ∈ Cr′(a) :⇔ a ≺′ b. If b ∈ G′, then b ∈ Cr′(a) :⇔ a ≺ b.

(b) We define C̃_{a}(b) as the primitive recursively definable set such that c ∈ C̃_{a}(b) :⇔ c ∈ T′ ∧ SC_{a}(c) ≺ ψ_{a}b ∧ G_{a}(c) ≺ b.

Definition 3.6 We define the set OT of ordinal notations, which will be a subset of T′, by:

(OT 1) 0 ∈ OT.
(OT 2) If n > 0, a_{0}, …, a_{n} ∈ OT ∩ P′, a_{n} ⪯ ⋯ ⪯ a_{0}, then
(a_{0}, …, a_{n}) ∈ OT,
(OT 3) If a, b ∈ OT, b ∉ Cr′(a), ¬(b = 0 ∧ a ∈ G′), then
φ′_{a}b ∈ OT.
(OT 4) If b ∈ OT π ∈ R′ ∩ OT, b, π ∈ C̃_{π}(b), then
ψ_{π}b ∈ OT,
(OT 5) If a ∈ OT \ (Fi′ ∪ {0}), then Ω′_{a} ∈ OT.
(OT 6) M ∈ OT.

I := I′ ∩ OT, Fi := Fi′ ∩ OT, R := R′ ∩ OT, G := G′ ∩ OT, P := P′ ∩ OT, Suc := Suc′ ∩ OT, Car := Car′ ∩ OT, Cr(a) := Cr′(a) ∩ OT, C_{a}(b) := C̃_{a}(b) ∩ OT. a ≺ b :⇔ a ≺′ b ∧ a ∈ OT ∧ b ∈ OT, a ⪯ b :⇔ a ⪯′ b ∧ a ∈ OT ∧ b ∈ OT. In the following, we write sometimes a for the primitive recursively decidable set {x ∈ OT|x ≺ a}.

We define all the functions in OT as in Sect. 2.2 of [Se98] and have the same lemmata, except that we don’t define a^{+F i}, a^{−F i}, a^{+I}, a^{−I}, replace in some lemmata I by M and define ã, a^{+}, κ^{−} as follows: Definition 3.7 (a) For a ∈ T′, we define ã, a^{+}, (ã will be the largest cardinal below,

a^{+} the least element of Car greater than a). ˜0 := 0, 0^{+} := Ω_{1}. If a = (a_{0}, …, a_{n}), n > 0, then ã := ã_{0}, a^{+} := a_{0}^{+}. If a =_{NF} φ_{b}c, then with d := max{b, c} we define ã := d̃, a^{+} := d^{+}. If a = ψ_{b}c, b ∉ I, then ã := b^{−}, a^{+} := b. If a = ψ_{b}c, b ∈ I, ã := a, a^{+} := Ω_{a+1}. If a =_{NF} Ω_{b}, ã := a, a^{+} := Ω_{b+1}. M̃ := M, M^{+} := Ω_{M+1}.

(b) For κ ∈ R, κ^{−} := \begin{cases}Ω_{s}, & if κ = Ω_{s+1}, \\ κ, & if κ ∈ I. \end{cases}

Lemma 3.8 Assume a ∈ OT, κ, π ∈ R.

(a) SC_{κ}(a) ⪯ min{κ, a}.

(b) a ≺ κ ⇒ G_{κ}(a) = ∅.

(c) SC_{π}(a) ≺ κ ≺ π ⇒ SC_{κ}(a) = SC_{π}(a).

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

(c) by induction on length(a): If a = 0, M or a =_{NF} a_{0} + a_{1}, φ_{a_{0}}a_{1}, Ω_{a_{0}}, this is obvious or follows by IH. If a = ψ_{κ′}e, it follows, if a ≺ π, {a} ≅ SC_{π}(a) ≺ κ, SC_{κ}(a) ≅ {a} ≅ SC_{π}(a), and if π ⪯ a, it follows by IH SC_{κ}(a) = SC_{κ}(κ′) ∪ SC_{κ}(e) = SC_{π}(a) by IH.

4 Definition of the Type Theory MLM

Definition 4.1 (a) The symbols of MLM are infinitely many variables z_{i} (i ∈ ω); the symbols ⇒, :, ,, (, ), =, λ, type, context; the term constructors (with their arity in parenthesis) 0 (0), l_{k} (for each l < k, with arity 0), S (1), i (1), j (1), p_{0} (1), p_{1} (1), r (1), λ (1), E (2), p (2), sup (2), R (2), Ap (2), J (2), D (3), P (3), and C_{n} (n ∈ ω, arity n + 1); the U-universe-term-constructors, which are term-constructors as well: N̂ (2), N̂_{k} (for each k ∈ ω, with arity 2), ˆ+ (4),Π̂ (4), Σ̂ (4), Ŵ (4) and Î (5); the V-universe-term-constructors, which are again term-constructors: N̂_{V} (0), N̂_{V,k} (for each k ∈ ω, with arity 0), ˆ+_{V} (2), Π̂_{V} (2), Σ̂_{V} (2), Ŵ_{V} (2) and Î_{V} (3) (which correspond to the U-universe-term-constructors N̂, N̂_{k}, Π̂, Σ̂, Ŵ, Î respectively); the Mahlo-term-constructors which are term-constructors Û (2), s (3), Res0 (4), Res1 (5); the type constructors with their arity N_{k} (for each k ∈ ω, arity 0), N (0), + (2), Π (2), Σ (2), W (2), I (3), V (0), T (1) and U (2).

(b) The b-objects are variables, further (x_{1}, …, x_{n})b and C(b_{1}, …, b_{n}), if C is an n-ary term- or type-constructor, x_{1}, …, x_{n} are variables and b, b_{1}, …, b_{n} are b-objects. The set FV(b) of free variables of a b-object b are defined in the usual way. We write +, ˆ+_{V} infix (for instance (a + b) for +(a, b)), aˆ+_{f,g}b for ˆ+(f, g, a, b), λx.t for λ((x)t), for E ∈ {Σ, Π, W, Σ̂_{V}, Π̂_{V}, Ŵ_{V}} Ex : s.t := E(s, (x)t), for E ∈ {Π̂, Ŵ, Σ̂} E_{f,g}x : s.t := E(f, g, s, (x)t), s_{f,g}(a) := s(f, g, a), Res0_{f,g}(r, s) := Res0(f, g, r, s), similarly for N̂, N̂_{k}, Res1, U, Û, Î. Further we write (rs) for Ap(r, s). We have the usual conventions about omitting brackets, especially the scope of λx. is as long as possible, for instance λx.st should be read as λx.(st). We define for b-objects b_{1}, …, b_{n}, b and variables x_{1}, …, x_{n} the simultaneous substitution b[x_{1} := b_{1}, …, x_{n} := b_{n}] (using the convention that, if x_{i} = x_{j}, then the first substitution applies) and “b[x_{1} := b_{1}, …, x_{n} := b_{n}] is an allowed substitution” in the usual way. α-equality (=_{α}) is defined again as always.

(c) The set of m-terms (for MLM-objects) is inductively defined as: a variable x is an m-term; if l < k, l, k ∈ ℕ, then l_{k} is an m-term; if r, s, t, s_{0}, t_{0} are m-terms, x, y, z, x′, y′, z′ ∈ Var_{ML}, x ≠ y ≠ z ≠ x, x′ ≠ y′ ≠ z′ ≠ y′, f := (x′, y′)s_{0}, g := (x′, y′, z′)t_{0} and f⃗ abbreviates f, g, then 0, S(r), λx.r, p(r, s), i(r), j(r), sup(r, s), r(r), P(r, s, (x, y)t), Ap(r, s), p_{0}(r), p_{1}(r), R(r, (x, y, z)s), D(r, (x)s, (y)t), J(r, (x)s); Π̂f⃗x : r.s, Σ̂f⃗x : r.s, Ŵf⃗x : r.s, r ˆ+f⃗s, Îf⃗(r, s, t), N̂f⃗, N̂_{k,f⃗} (for k ∈ ω), Ûf⃗, sf⃗(r), Res0f⃗(r, (x)s), Res1f⃗(r, (x)s, t); N̂_{V}, N̂_{k,V} (for k ∈ ω), Π̂_{V}x : r.s, Σ̂_{V}x : r.s, Ŵ_{V}x : r.s, r ˆ+_{V}s, Î_{V}(r, s, t)are m-terms; if n ∈ ℕ and r, s_{1}, …, s_{n} are m-terms, then C_{n}(r, s_{1}, …, s_{n}) is an m-term. Let Term_{Cl} be the set of closed m-terms.

(d) The pseudo-term-constructors are N̂f⃗, N̂_{k,f⃗} (k ∈ ω), Π̂f⃗, Σ̂f⃗, Ŵf⃗, ˆ+f⃗, Îf⃗ for any m-term f. If C ∈ {N̂, N̂_{k}, Π̂, Σ̂, Ŵ, ˆ+, Î}, C of arity n, Cf⃗ the corresponding pseudoterm-constructor, then Cf⃗ can be treated as a constructor of arity n − 2 by Cf⃗(t_{1}, …, t_{n−1}) := C(f, g, t_{1}, …, t_{n−1}). C_{V} is the V-universe-term-constructor, corresponding to C.

(e) Further we define T_{V} := T, Tf⃗(t) := T(sf⃗(t)). U_{V} := V.

(f) The m-types are N_{k} (k ∈ ω), N, V; and if A, B are m-types, x ∈ Var_{ML}, r, s mterms, f⃗ as above, then T(r), Πx : A.B, Σx : A.B, Wx : A.B, A + B, Uf⃗ I(A, r, s) are m-types.

(g) An m-context-piece is a string x_{1} : A_{1}, …, x_{n} : A_{n}, where n ≥ 0, x_{i} different variables, A_{i} m-types. An m-context is an m-context-piece x_{1} : A_{1}, …, x_{n} : A_{n} such that FV(A_{i}) ⊂ {x_{1}, …, x_{i−1}} for i = 1, …, n. A m-judgements are context, A = B, and s = t : A where A, B are m-types, s, t are m-terms. We treat the usual judgements A type and s : A as abbreviations: A type :≡ A = A, s : A :≡ s = s : A.

(h) We abbreviate [x⃗ := t⃗] := [x_{1} := t_{1}, …, x_{n} := t_{n}], if x⃗ = x_{1}, …, x_{n} and t⃗ = t_{1}, …, t_{n}. [x_{1} := t_{1}, …, x_{n} := t_{n}] \ {y} := [x⃗ := t⃗] \ {y} is the result of omitting in [x⃗ := t⃗] all x_{i} := t_{i} such that x_{i} = y, and [x⃗ := t⃗] \ {y_{1}, …, y_{m}} := (⋯ (([x⃗ := t⃗] \ {y_{1}}) \ {y_{2}}) ⋯ \ {y_{m}}).

(i) We have the usual conventions that Γ is a m-context, θ is a m-judgement etc. as in [Se98]. This can however be as well T -contexts, T -judgements for the intermediate systems T = ML_{1}^{(n)}, ML_{2}. Which one, should be clear from the general context.

Preliminaries 4.2 Let in the following always, unless stated differently f⃗ := f, g, f⃗′ := f′, g′, where f = (x, y)s, f′ = (x′, y′)s′, g = (x, y, z)t, g′ = (x′, y′, z′)t′ for some variables x, y, z, x′, y′, z′ and some m-terms s, t, s′, t′ Definition 4.3 of the type theory MLM. We define MLM ⊢ Γ ⇒ θ in the same way as in the definition of ML_{J} in [Se93], (esp. with the same convention concerning the use of abstracted m-terms and -types), with the following modifications:

• We switch from a version which is close to [TD88] to a version close to [PSH90], (this doesn’t have an influence on the proof in the following which works for most variants), i.e.:

– (Ref_{i}) become trivial, since we treat A type as an abbreviation for A = A, s : A as an abbreviation for s = s : A.

– (Sub_{i}), can be derived and therefore omitted.

– We replace all type introduction, introduction and elimination rules by their equality versions, e.g. for the case of the Π-type:

A = A′ x : A ⇒ B(x) = B′(x) (Π^{T}) Π(A, B) = Π(A′, B′)

x : A ⇒ t(x) = t′(x) : B(x) (Π^{I}) λ(t) = λ(t′) : Π(A, B)

x : A ⇒ B(x) type s = s′ : Π(A, B) r = r′ : A

(Π^{E})

Ap(s, r) = Ap(s′, r′) : Π(A, B)

• We replace the rules for the universe by the new rules for the Mahlo universe below.

r →_{V} s := Π̂_{V}x : r.s, r →f⃗ s := Π̂f⃗x : r.s for a new variable x.

Rules for the Mahlo-universe

Type introduction rules for V

(V_{I}) V = V  \begin{aligned}& r = r′ : V \\ (T_{I}) \\ & T(r) = T(r′) \end{aligned}

Introduction rules for V

(N̂_{k,V,I}) N̂_{k,V} = N̂_{k,V} : V (k ∈ ω)  (N̂_{k,V,=}) T(N̂_{k,V}) = N_{k} (k ∈ ω)
r = r′ : V x : T(r) ⇒ s(x) = s′(x) : V

(Π̂_{V,I})

Π̂_{V}(r, s) = Π̂_{V}(r′, s′) : V
r : V x : T(r) ⇒ s(x) : V

(Π̂_{V,=})

T(Π̂_{V}(r, s)) = Πx : T(r).T(s(x))

Similarly for N̂, Σ̂, Ŵ, ˆ+, i.

x : V, y : (T(x) → V) ⇒ f(x, y) = f′(x, y) : V

x : V, y : (T(x) → V), z : T(f(x, y)) ⇒ g(x, y, z) = g′(x, y, z) : V (Û_{I}) Û_{f,g} = Û_{f′,g′} : V

x : V, y : (T(x) → V) ⇒ f(x, y) : V

x : V, y : (T(x) → V), z : T(f(x, y)) ⇒ g(x, y, z) : V (Û_{=})

T(Û_{f,g}) = U_{f,g}

Rules for U

x : V, y : (T(x) → V) ⇒ f(x, y) = f′(x, y) : V

x : V, y : (T(x) → V), z : T(f(x, y)) ⇒ g(x, y, z) = g′(x, y, z) : V (U_{T}) U_{f,g} = U_{f′,g′}

x : V, y : (T(x) → V) ⇒ f(x, y) = f′(x, y) : V x : V, y : (T(x) → V), z : T(f(x, y)) ⇒ g(x, y, z) = g′(x, y, z) : V

r = r′ : U_{f,g} (s_{I}) s_{f,g}(r) = s_{f′,g′}(r′) : V

Introduction-Rules for U

Let in the following Ass_{I} be the assumptions (for the introduction rules)

x : V, y : (T(x) → V) ⇒ f(x, y) = f′(x, y) : V ,
x : V, y : (T(x) → V), z : T(f(x, y)) ⇒ g(x, y, z) = g′(x, y, z) : V .

and Ass_{=} be the assumptions (for the equality rules)

x : V, y : (T(x) → V) ⇒ f(x, y) : V ,
x : V, y : (T(x) → V), z : T(f(x, y)) ⇒ g(x, y, z) : V ,
r = r′ : U_{s,t} x : T(s_{s,t}(r)) ⇒ s(x) = s′(x) : Uf⃗ Ass_{I}

(Res0_{I})

Res0f⃗(r, s) = Res0f⃗′(r′, s′) : Uf⃗
r : Uf⃗ x : T(sf⃗(r)) ⇒ s(x) : Uf⃗ Ass_{=}

(Res0_{=})

sf⃗(Res0f⃗(r, s)) = f(sf⃗(r), λx.sf⃗(s(x))) : V

r = r′ : Uf⃗ x : T(sf⃗(r)) ⇒ s(x) = s′(x) : Uf⃗
t = t′ : T(sf⃗(Res0f⃗(r, s))) Ass_{I}

(Res1_{I})

Res1f⃗(r, s, t) = Res1f⃗′(r′, s′, t′) : Uf⃗
r : Uf⃗ x : T(sf⃗(r)) ⇒ s(x) : Uf⃗ t : T(sf⃗(Res0f⃗(r, s)))  Ass_{=}

(Res1_{=})

sf⃗(Res1f⃗(r, s, t)) = g(sf⃗(r), λx.sf⃗(s(x)), t) : V
Ass_{I} (N̂_{k,f⃗,I})
N̂_{k,f⃗} = N̂_{k,f⃗′} : Uf⃗

Ass_{=} (N̂_{k,f⃗,=})
sf⃗(N̂_{k,f⃗}) = N̂_{k,V} : V
r = r′ : Uf⃗ x : T(sf⃗(r)) ⇒ s(x) = s′(x) : Uf⃗ Ass_{I}

(Π̂_{f⃗,I})

Π̂f⃗(r, s) = Π̂f⃗′(r′, s′) : Uf⃗
r : Uf⃗ x : T(sf⃗(r)) ⇒ s(x) : Uf⃗ Ass_{=}

(Π̂_{f⃗,=})

sf⃗(Π̂f⃗(r, s)) = Π̂_{V}(sf⃗(r), (x)sf⃗(s(x)) : V

Similarly for N̂, Σ̂, Ŵ, ˆ+, i Definition 4.4 (a) The intermediate system ML_{1}^{(n)} is defined as follows:

The ML_{1}^{(n)}-term-constructors are the m-term-constructors except the U-universe-term-constructors, V-universe-term-constructors and Mahlo-term-constructors. The ML_{1}^{(n)}-type-constructors are the m-type-constructors except of V, U, T, but additionally with 1-ary constructors Eq and X_{1}, …, X_{n}. The ML_{1}^{(n)}-terms are the m-terms, built only from ML_{1}^{(n)}-term-constructors. The ML_{1}^{(n)}-types are defined as the m-types, but referring to ML_{1}^{(n)}-types instead of m-types, only using ML_{1}^{(n)}-type-constructors and by adding the clause: if t is a ML_{1}^{(n)}-type, then Eq(t) and X_{i}(t) are ML_{1}^{(n)}-type, too. (Eq(t) will be needed only to prove 0 ≠_{N} 1). The definition of ML_{1}^{(n)}-contexts, -context-pieces, -judgements are defined as usual. The ML_{1}^{(n)}-rules are the rules of MLM, but omitting all rules for the universe and adding the rules: \frac{r = s}{X_{i}(r) = X_{i}(s)}, \frac{r = s : N_{2}}{Eq(r) = Eq(s)}, Eq(0_{2}) = N_{0}, Eq(1_{2}) = N_{1}.

ML_{1}^{(n)} ⊢ Γ ⇒ θ is then defined as usual.

(b) The intermediate system ML_{2} is the restriction of MLM by omitting the U-universe-term-constructors, Mahlo-universe-constructors and the type-constructor U.

Definition 4.5 (a) V_{V} := V, Vf⃗ := Uf⃗.

(b) T_{V}(t) := T(t), Tf⃗(t) := T(sf⃗(t)).

(c) P_{V}(N) := N → V_{v}. Definition 4.6 Let v = f⃗ or v = V.

(a) For ML_{1}^{(n)}-types A, m-types A_{1}, …, A_{n} and variables x_{1}, …, x_{n} we define, with B_{i} := (x_{i})A_{i} the m-type A[X_{1} := B_{1}, …, X_{n} := B_{n}], short A[X⃗ := B⃗] inductively by: Is C an ML_{1}^{(n)}-type-constructor, C ∉ {Eq, X_{1}, …, X_{n}}, then C(t_{1}, …, t_{n})[X⃗ := B⃗] := C(t_{1}[X⃗ := B⃗], …, t_{n}[X⃗ := B⃗]), where ((x)D)[X⃗ := B⃗]) := (x)(D[X⃗ := B⃗]), and for ML_{1}^{(n)}-terms t, t[X⃗ := B⃗] := t. X_{i}(t)[X⃗ := B⃗] := A_{i}[x_{i} := t]. Eq(t)[X⃗ := B⃗] := T(C_{2}(t, N̂_{0,V}, N̂_{1,V})). (Γ ⇒ θ)[X⃗ := B⃗] is the result of applying this operation to the (outermost) types in Γ ⇒ θ.

(b) For ML_{1}^{(n)}-type-constructors C we define γ_{v}(C): γ_{v}(N_{k}) := N̂_{k,v}, γ_{v}(N) := N̂_{v}, γ_{v}(Σ) := Σ̂_{v}, γ_{v}(Π) := Π̂_{v}, γ_{v}(W) := Ŵ_{v}, γ_{v}(I) := Î_{v}, γ_{v}(+) := ˆ+_{v}, γ_{v}(C) := C otherwise.

(c) For ML_{1}^{(n)}-types A, and variables Y_{1}, …, Y_{n} (which will later range over elements of N → V_{v}) we define γ_{v}(A)[X_{1} := Y_{1}, …, X_{n} := Y_{n}], where we abbreviate [X_{1} := Y_{1}, …, X_{n} := Y_{n}] by [X⃗ := Y⃗]: If C ∉ {Eq, X_{1}, …, X_{n}}, then γ_{v}(C(t_{1}, …, t_{n})[X⃗ := Y⃗] := γ_{v}(C)(γ_{v}(t_{1})[X⃗ := Y⃗], …, γ_{v}(t_{n})[X⃗ := Y⃗]), where γ_{v}((x)D)[X⃗ := Y⃗]) := (x)(γ_{v}(D)[X⃗ := Y⃗]), and for ML_{1}^{(n)}-terms t, γ_{v}(t)[X⃗ := Y⃗] := t. γ_{v}(X_{i}(t))[X⃗ := Y⃗] := Y_{i}t, γ_{v}(Eq(t))[X⃗ := Y⃗] := C_{2}(t, N̂_{0,v}, N̂_{1,v}).

(d) We define γ_{v}(θ)[X⃗ := Y⃗] for ML_{1}^{(n)}-judgements θ:

γ_{v}(context)[X⃗ := Y⃗] := {context}, γ_{v}(s = t : A) := {γ_{v}(A)[X⃗ := Y⃗] : V_{v}, s = t : T_{v}(γ_{v}(A))}, γ_{v}(A = B) := {γ_{v}(A)[X⃗ := Y⃗] = γ_{v}(B)[X⃗ := Y⃗] : V_{v}}. γ_{v}(x_{1} : A_{1}, …, x_{n} : A_{n}) := x_{1} : T(γ_{v}(A_{1})), …, x_{n} : T(γ_{v}(A_{n})). γ_{v}(x_{1} : A_{1}, …, x_{n} : A_{n} ⇒ θ)[X⃗ := Y⃗] :=

{x_{1} : T_{v}(γ_{v}(A_{1})), …, x_{i−1} : T_{v}(γ_{v}(A_{i−1})) ⇒ γ_{v}(A_{i}) : V_{v} | i = 1, …, n} ∪ {x_{1} : T_{v}(γ_{v}(A_{1})), …, x_{n} : T_{v}(γ_{v}(A_{n})) ⇒ θ′|θ′ ∈ γ_{v}(θ)}.

(e) For ML_{2}-term-constructors C we define δf⃗(C): δf⃗(N̂_{k,V}) := N̂_{k,f⃗}, δf⃗(N̂) := N̂f⃗, δf⃗(Σ̂_{V}) := Σ̂f⃗, δf⃗(Π̂_{V}) := Π̂f⃗, δf⃗(Ŵ_{V}) := Ŵf⃗, δf⃗(Î_{V}) := Îf⃗, δf⃗(ˆ+_{V}) := ˆ+f⃗, δf⃗(C) := C otherwise. For ML_{2}-type-constructors C we define δf⃗(C): δf⃗(N_{k}) := N̂_{k,V}, δf⃗(N) := N̂_{V}, δf⃗(Σ) := Σ̂_{V}, δf⃗(Π) := Π̂_{V}, δf⃗(W) := Ŵ_{V}, δf⃗(I) := Î_{V}, δf⃗(+) := ˆ+_{V}, δf⃗(V) := Uf⃗, δf⃗(T) := sf⃗, δf⃗(C) := C otherwise.

(f) ρf⃗(C) := δf⃗(C) for term-constructors C, ρf⃗(V) := T(Uf⃗), ρf⃗(T) := Tf⃗, ρf⃗(C) := C otherwise.

(g) For ML_{2}-terms or types t, δf⃗(t), ρf⃗(t) is the result of replacing all constructors C in t by δf⃗(C) or ρf⃗(C) respectively.

(h) We define δf⃗(θ) for ML_{1}^{(n)}-judgements θ: δf⃗(context) := {context}, δf⃗(s = t : A) := {δf⃗(A) : Uf⃗, δf⃗(s) = δf⃗(t) : Tf⃗(δf⃗(A))}, δf⃗(A = B) := {δf⃗(A) = δf⃗(B) : Uf⃗}. δf⃗(x_{1} : A_{1}, …, x_{n} : A_{n} ⇒ θ) := {x_{1} : Tf⃗(δf⃗(A_{1})), …, x_{i−1} : Tf⃗(δf⃗(A_{i−1})) ⇒ δf⃗(A_{i}) : Uf⃗ | i = 1, …, n} ∪ {x_{1} : Tf⃗(δf⃗(A_{1})), …, x_{n} : Tf⃗(δf⃗(A_{n})) ⇒ θ′|θ′ ∈ δf⃗(θ)}.

(i) ρf⃗(Γ ⇒ θ) is the result of replacing all terms and types t in Γ ⇒ θ by ρf⃗(t).

(j) If v = V Assumptions_{Δ}(v) is empty, and if v = f⃗ as usual, Assumptions_{Δ}(v) is the condition MLM ⊢ Δ, x_{1} : V, y : T(x_{1}) → V ⇒ f(x_{1}, y) : V and MLM ⊢ Δ, x_{1} : V, y : T(x_{1}) → V, z : T(f(x_{1}, y)) ⇒ g(x_{1}, y, z) : V.

Lemma 4.7 Assume v = V, Assumptions_{Δ}(v).

(a) If ML_{1}^{(n)} ⊢ Γ ⇒ θ, MLM ⊢ Δ, x_{i} : N ⇒ B_{i} type (i = 1, …, n), then MLM ⊢ Δ, (Γ ⇒ θ)[X_{1} := (x_{1})B_{1}, …, X_{n} := (x_{n})B_{n}]. The same holds with MLM replaced by ML_{1}^{(n)} or ML_{2}; only in the case T = ML_{1}^{(n)}, we have to modify the definition of t[X⃗ := B⃗] by Eq(t)[X⃗ := B⃗] := Eq(t).

(b) If ML_{1}^{(n)} ⊢ Γ ⇒ θ, (Γ_{1} ⇒ θ_{1}) ∈ γ_{v}(Γ ⇒ θ)[X⃗ := Y⃗], then MLM ⊢ Δ, Y_{1} : P_{v}(N), …, Y_{n} : P_{v}(N), Γ ⇒ θ_{1}. The same holds in the case v = V with MLM replaced by ML_{2}.

(c) If ML_{1}^{(n)} ⊢ Γ ⇒ A : type, then MLM ⊢ Δ, Y_{1} : P_{v}(N), …, Y_{n} : P_{v}(N), Γ ⇒ r : T_{v}(γ_{v}(A))[X⃗ := Y⃗] ↔ A[X⃗ := Y⃗^{V,Cl}] for some r, where Y⃗^{V,Cl} := Y_{1}^{V,Cl}, …, Y_{n}^{V,Cl}.

(d) If ML_{2} ⊢ Γ ⇒ θ, then MLM ⊢ Γ ⇒ θ.

(e) If v = f⃗ as in the assumptions of this lemma, (Γ_{1} ⇒ θ_{1}) ∈ δf⃗(Γ ⇒ θ), then MLM ⊢ Δ, Γ_{1} ⇒ θ_{1} and MLM ⊢ Δ, ρf⃗(Γ ⇒ θ).

Proof: By an easy induction on the ML_{1}^{(n)}, ML_{2}-derivations. In (c) we conclude for instance in the case of Π-type-introduction, having h_{1} : T_{v}(γ_{v}(A)) → A, h_{2} : B → T_{v}(γ_{v}(B)) that λh_{3}.λy.h_{2}[x := h_{1}y](h_{3}(h_{1}y)) : ((Πx : A.B) → T_{v}(γ_{v}(Πx : A.B))). In the case of the W-type, we use induction over the W-type. We use all the abbreviations from Sect. 3.2 and the definitions and lemmata in Sect. 3.3 - 3.5 of [Se98]. The changes are

• We replace the underlined constructors by their non-underlined version.

• All proofs and definitions can be carried out in ML_{1}^{(n)}.

• We add the following definition and lemma: Definition 4.8 Assume v = V or v = f⃗.

(a) t ∈_{V} A := At, t ∈f⃗ A := At. (Note that, if A : P_{v}(N), t : N, then t ∈_{v} A : V_{v}).

(b) t^{V,Cl} := {y : N | T(ty)}, t^{f⃗,V} := λy.sf⃗(ty), t^{f⃗,Cl} := (t^{f⃗,V})^{V,Cl}. Lemma 4.9 Assume v = V or v = f⃗, Assumptions_{Δ}(v), ML_{1}^{(n)} ⊢ Δ ⇒ A ∈ Cl(N).

(a) MLM ⊢ Δ, Y_{1} : P_{v}(N), …, Y_{n} : P_{v}(N) ⇒ γ_{v}(A)[X⃗ := Y⃗] : P_{v}(N).

(b) MLM ⊢ Δ, Y_{1} : P_{v}(N), …, Y_{n} : P_{v}(N) ⇒ γ_{v}(A)^{v,Cl}[X⃗ := Y⃗] ≅ A[X⃗ := Y⃗^{V,Cl}]. Proof: easy.

5 The Well-ordering Proofs

The definition of M(A), τ^{A}(a), A^{A}(B), W (A), Ag(A), A^{+}, Prog(A, B), Prog(A), weakly upward and downward closed can be done as in Sect. 4.2 - 4.4 of [Se98]. Further nearly all the lemmata in these section go through again. We have the following changes:

• We can do all the proofs in ML_{1}^{(n)}. We only replace the assumptions of A, B, C, … ∈ Cl(N) by: let A = (x)X_{i_{1}}(x), B = (x)X_{i_{2}}(x) . . ..

• We have to replace I by M.

• Lemma 4.17 in [Se98] is replaced by Lemma 5.2 below.

• We add Lemma 5.1 below, which is proved in ML_{1}^{(n)}. Lemma 5.1 Let A = X_{i} for some i ≤ n.

(a) (τ^{A}(ψ_{κ}b) ⊂ A ∧ ψ_{κ}b ⪯ c ⪯ κ) → C^{ψ_{κ}b}(A) ∩ C_{κ}(b) ⊂ C^{c}(A).

(b) If a ∈ C^{b}(A), A ⊂ M(A), A ∩ b̃ weakly downward closed, b ≺ M, then sc_{M}(a) ⊂ C^{b}(A).

(c) a ∈ C_{κ}(c) ⇒ sc_{M}(a) ⊂ C_{κ}(c).

(d) ψ_{ψ_{M}a}b ∈ OT ⇒ sc_{M}(a) ≺ ψ_{ψ_{M}a}b.

(e) If a, ψ_{κ}b ∈ OT, sc_{M}(a) ≺ ψ_{κ}b and G_{M}(a) ≺ b, then a ∈ C_{κ}(b).

Proof: (a): We show ∀x ∈ C^{ψ_{κ}b}(A) ∩ C_{κ}(b).x ∈ C^{c}(A) by induction on length(x). If x ≺ ψ_{κ}b, it follows x ∈ C^{ψ_{κ}b}(A) ∩ ψ_{κ}b = τ^{A}(ψ_{κ}b) ⊂ A ∩ c ⊂ C^{c}(A). If ψ_{κ}b ⪯ x, it follows κ ⪯ x, and, if in this case x = 0, M or x =_{NF} x_{1} + x_{2}, φ_{x_{1}}x_{2}, Ω_{x_{1}}, follows the assertion by IH or directly, and, if x = ψ_{π}d, π, d ∈ C_{π}(d), it follows c ⪯ κ ≺ π, π, d ∈ C^{ψ_{κ}b}(A) ∩ C_{κ}(b) ⊂ C^{c}(A), x ∈ C^{c}(A). (b), (c): easy. (d): ψ_{M}a ∈ C_{ψ_{M}a}(b), a ∈ C_{ψ_{M}a}(b), sc_{M}(a) ⊂ C_{ψ_{M}a}(b), further sc_{M}(a) ≺ ψ_{M}a, therefore sc_{M}(a) ⊂ C_{ψ_{M}a}(b) ∩ ψ_{M}a ≅ ψ_{ψ_{M}a}b (e): Induction on length(a). If a = 0, M, or a =_{NF} a_{1} +a_{2}, φ_{a_{1}}a_{2}, Ω_{a_{1}}, the assertion follows by IH or directly. If a = ψ_{π}c, π ⪯ M, it follows a ≺ ψ_{κ}b, a ∈ C_{κ}(b), and if a = ψ_{π}c, M ≺ π, follows the assumption by IH for π, c. Lemma 5.2 (replaces Lemma 4.17 in [Se98])

(a) 0 ∈ W (A).

(b) If A ∩ κ ≅ W (A) ∩ κ, A ⊂ M(A), then W (A) ∩ κ^{+} is downward closed, upward closed bounded by κ^{+}.

(c) Assume A ⊂ M(A). Then ∀κ, y ∈ W (A).∀z ∈ OT.(z = max{κ, y} ∧ W (A) ∩ z̃ ≅ A ∩ z̃ ∧ κ ∈ R ∧ κ, y ∈ C_{κ}(y)) → ψ_{κ}y ∈ W (A).

Proof: (a): trivial. (b): as in the proof of Lemma 4.17 in [Se98]. (c): Assume A ⊂ M(A), τ ∈ Car ∩ W (A), W (A) ∩ τ ≅ A ∩ τ. We show by Ind(y ∈ W (A))

∀y ∈ W (A).∀κ ∈ R.(y ≺ τ^{+} ∧ y, κ ∈ C_{κ}(y) ∧ ψ_{κ}y ≺ τ^{+}

∧(κ = M ∨ ∃z ∈ OT.(κ = ψ_{M}z ∧ z ∈ C^{y}(A) ∩ C_{M}(z)) ∨ κ^{−} ∈ W (A)|τ)
→ ψ_{κ}y ∈ W (A).

Then follows with τ := z̃ the assertion. Assume y according to Induction, κ, y as in the premise of the assertion. We note first: if c ∈ W (A) ∩ y, then c ∈ τ^{A}(y) (if c ≺ τ, then c ∈ A ∩ y, otherwise c̃ = ỹ, c ∈ C^{c}(A) ∩ y ≅ τ^{A}(y)) and c ∈ C^{c}(A) ∩ y. We show

∀x′ ∈ C_{κ}(y) ∩ C^{ψ_{κ}y}(A) ∩ τ^{+}.x′ ∈ W (A) (∗)

by side-induction on length(x′) and assume x′ according to induction, x′ ∈ C_{κ}(y) ∩ C^{ψ_{κ}y}(A) ∩ τ^{+}. If x′ = 0, M, follows the assertion by (b). If x′ =_{NF} x_{1} + x_{2}, φ_{x_{1}}x_{2} or Ω_{x_{1}}, it follows by IH x_{i} ∈ W (A), by (b) x′ ∈ W (A). Case x′ = ψ_{π}x_{1}. Subcase x′ ≺ ψ̃_{κ}y. Then x′ ∈ A ∨ (ψ_{κ}y ≺ π ∈ I ∧ π, x_{1} ∈ C^{ψ_{κ}y}(A)). If x′ ∈ A, it follows x′ ∈ A ∩ τ ⊂ W (A). Assume now π, x_{1} ∈ C^{ψ_{κ}y}(A), ψ_{κ}y ≺ π ∈ I. If κ = Ω_{c+1}, it follows x′ ∈ C^{κ^{−}}(A) ∩ κ^{−} ⊂ W (A). Otherwise κ, π ∈ I ∧ x′ ≺ ψ_{κ}y ≺ π. Therefore ψ_{π}x_{1} ⪯ sc_{κ}(y) ∨ (π = κ ∧ x_{1} ≺ y ∧ sc_{π}(x_{1}) ≺ ψ_{κ}y) ∨ (ψ_{π}x_{1} ≺ κ ≺ π ∧ sc_{π}(x_{1}) ≺ ψ_{κ}y). Subsubcase ψ_{π}x_{1} ⪯ sc_{κ}(y). y ∈ W (A), sc_{κ}(y) ⊂ τ^{A}(y) ∪ {y} ⊂ W (A), sc_{κ}(y) ⊂ ψ_{κ}y. Let a := max(sc_{κ}(y)). Then ψ_{π}x_{1} ∈ C^{ψ_{κ}y}(A)|a ⊂ C^{a}(A)|a ≅ τ^{A}(a) ∪ {a} ⊂ W (A). Subsubcase π = κ ∧ x_{1} ≺ y ∧ sc_{π}(x_{1}) ≺ ψ_{κ}y: G_{κ}(x_{1}) ≺ x_{1} ≺ y ≺ τ^{+}, therefore x_{1} ∈ C_{κ}(y) ∩ τ^{+}, x_{1} ∈ C^{ψ_{κ}y}(A). By side-IH x_{1} ∈ W (A) ∩ τ^{+}. Therefore x_{1} ∈ τ^{A}(y), and by main-IH x′ ∈ W (A). Subsubcase ψ_{π}x_{1} ≺ κ ≺ π ∧ sc_{π}(x_{1}) ≺ ψ_{κ}y: Then κ = ψ_{M}b for some b, b ∈ C^{y}(A) ∨ κ ∈ W (A). By ψ_{π}x_{1} ≺ ψ_{M}b ≺ π it follows ψ_{π}x_{1} ⪯ sc_{M}(b) ∨ (π = M ∧ x_{1} ≺ b ∧ sc_{π}(x_{1}) ≺ ψ_{M}b). Subsubsubcase ψ_{π}x_{1} ⪯ sc_{M}(b): Let a := max(sc_{M}(b)). If κ ∈ W (A), then κ ∈ C^{κ}(A), b ∈ C^{κ}(A), a ∈ C^{κ}(A), b ∈ C_{M}(b), a ∈ C_{M}(b) ∩ M ≅ ψ_{M}b, κ ∈ C_{κ}(y), a ∈ C_{κ}(y) ∩ κ ≅ ψ_{κ}y a ∈ τ^{A}(κ) ⊂ W (A), a ∈ W (A)∩ψ_{κ}y, ψ_{π}x_{1} ∈ C^{ψ_{κ}y}(A)∩a ⊂ τ^{A}(a) ⊂ W (A). If b ∈ C^{y}(A), it follows a ∈ C^{y}(A), by κ ∈ C_{κ}(y) a ⪯ b ≺ y, again a ∈ τ^{A}(y) ⊂ W (A), as before ψ_{π}x_{1} ∈ W (A). Subsubsubcase (π = M ∧ x_{1} ≺ b ∧ sc_{π}(x_{1}) ≺ ψ_{M}b): sc_{M}(x_{1}) ≺ ψ_{κ}y, G_{M}(x_{1}) ≺ x_{1} ≺ b ≺ y ≺ τ^{+}, by Lemma 5.1 (e) it follows x_{1} ∈ C_{κ}(y) ∩ C^{ψ_{κ}y}(A) ∩ τ^{+}, by side-IH x_{1} ∈ W (A), x_{1} ≺ y, therefore x_{1} ∈ τ^{A}(y), by IH x′ ∈ W (A). Subcase ψ̃_{κ}y = x′. x′ ≠ ψ_{κ}y, therefore κ ∉ I, x′ = κ^{−} ∈ W (A). Subcase ψ̃_{κ}y ≺ x′ ≺ ψ_{κ}y: Then κ = Ω_{d+1} = π for some d, x_{1} ≺ y, x_{1} ∈ C^{ψ_{κ}y}(A) ∩ C_{κ}(y) ∩ τ^{+}, by side-IH x_{1} ∈ W (A), x_{1} ∈ τ^{A}(y), by main-IH follows the assertion. Subcase ψ_{κ}y ⪯ x′. Then κ ⪯ x′. π, x_{1} ∈ C^{ψ_{κ}y}(A) ∩ C_{κ}(y), x_{1} ≺ y ≺ τ^{+}, by side-IH x_{1} ∈ W (A), x_{1} ∈ τ^{A}(y). Subsubcase τ^{+} ≺ π = M: by main-IH follows the assertion. Subsubcase τ^{+} ≺ π = ψ_{M}b: b ≺ x_{1} ≺ y ≺ τ^{+}, b ∈ C^{ψ_{κ}y}(A) ∩ C_{κ}(y) ∩ τ^{+}, by side IH b ∈ W (A), b ∈ C^{y}(A) ∩ C_{M}(b), by main-IH x′ ∈ W (A). Subsubcase otherwise: Then π ⪯ τ^{+}. π = τ^{+}, π^{−} ∈ W (A), or π ≺ τ^{+}, by side-IH π ∈ W (A), again π^{−} ∈ W (A). By main-IH it follows x′ ∈ W (A). The proof of (∗) is now complete.

We have therefore C^{ψ_{κ}y}(A) ∩ ψ_{κ}y ⊂ W (A). Further, if y ≺ ψ̃_{κ}y, y ∈ W (A) ∩ τ ∩ ψ̃_{κ}y ⊂ C^{ψ_{κ}y}(A), otherwise y ∈ M(A), y ∈ C^{y}(A) ⊂ C^{ψ_{κ}y}(A). If κ = M, κ ∈ C^{ψ_{κ}y}(A). If κ = ψ_{M}b, b ∈ C^{y}(A),it follows b ≺ y ≺ τ^{+}, b ∈ W (A). If M ⪯ τ^{+}, it follows ψ_{M}b ∈ W (A) by main IH. Otherwise, if b ≺ τ, it follows b ∈ A ⊂ C^{ψ_{κ}y}(A) and, if τ ⪯ b, we have b ∈ C^{b}(A) ⊂ C^{ψ_{κ}y}(A), in both cases therefore ψ_{M}b ∈ C^{ψ_{κ}y}(A). If κ = κ^{−} ∈ W (A)|τ, it follows κ ∈ C^{κ}(A) ⊂ C^{ψ_{κ}y}(A). If κ ≠ κ^{−} ∈ W (A)|τ, it follows κ = Ω_{d+1} for some d, κ^{−} = Ω_{d} ∈ C^{κ^{−}}(A) ≅ C^{ψ_{κ}y}(A), κ ∈ C^{ψ_{κ}y}(A). In any case therefore κ, y ∈ C^{ψ_{κ}y}(A), ψ_{κ}y ∈ C^{ψ_{κ}y}(A), ψ_{κ}y ∈ M(A), ψ_{κ}y ∈ A^{A}(W (A)) ⊂ W (A).

We define W and prove Lemma 4.26 - 4.29 as in [Se98]. The modifications with respect to [Se98] are that we can carry out all the proofs in ML_{2}, and can replace the assumptions A, B, … ∈ Cl(N) by A, B, …: P(N) (replacing s ∈ A by T(As) etc.) The following Lemma 5.3, 5.4, 5.5, 5.6 and 5.7 can be proved in ML_{2}. Wf⃗ := δf⃗(W). Lemma 5.3 Assume a ∈ (M(W) \ I) ∩ M, B : P(N), B^{V,Cl} ⊂ W|a such that τ^{W}(a) ⪯ B^{V,Cl}. Then a ∈ W. Proof: Let B′ := B^{V,Cl}, B̂ := Σx : N.x ∈ B′. From the assertion we conclude that there is some g : B̂ → P(N) such that ∀y : B̂.Ag((g y)^{V,Cl}) ∧ y0 ∈ (g y)^{V,Cl}. Let ĝ(y) := (g y)^{V,Cl}, C := {x : N | ∃y ∈ B̂.x ∈ ĝ(y)} ∩ a}. By [Se98], Lemma 4.28 it follows Ag(C). We have τ^{W}(a) ⊂ W: If y ∈ τ^{W}(a), then y ∈ C^{a}(W)∩a, y ⪯ x ∈ W for some x ∈ B′ ⊂ W, x ⪯ a, y ∈ C^{a}(W)|x ⊂ τ^{W}(x) ∪ {x} ⊂ W. We show C ≅ W ∩ a: “⊂” is obvious. “⊃”: Assume y ∈ W ∩ a. Then y ∈ τ^{W}(a), y ⪯ z for some z ∈ B′, z ∈ ĝ(p(z, p)) ⊑ W for some p : z ∈ B′, y ∈ W, therefore y ∈ g(p(z, p)) ∩ a ⊂ C. We show ∀d ∈ W (C).d ≺ a → d ∈ C, (i.e. W (C) ∩ a ⊂ C) by Ind(d ∈ W (C)). Assume d according to induction, d ≺ a. Then τ^{C}(d) ⊂ C, d ∈ C^{d}(C). We show ∃e ∈ W.d ⪯ e: If d̃≺ d, it follows d̃∈ C^{d}(C) ∩ d ⊂ C ⊂ W, d ≺ d^{+} ∈ W. If d̃ = d =_{NF} Ω_{d′}, it follows d ∈ C^{d}(C), d′ ∈ C^{d}(C) ∩ d ⊂ C ∩ a ⊂ C^{a}(C), d = d̃ ∈ C^{a}(C) ∩ a ≅ C^{a}(W) ∩ a ⊂ W. If d̃ = d = ψ_{M}e_{1}, it follows by Lemma 5.1 (a) e_{1} ∈ C^{d}(C) ∩ C_{M}(e_{1}) ⊂ C^{a}(C), d ∈ C^{a}(C) ∩ a ⊂ W. Otherwise it follows d̃ = d = ψ_{κ}e_{1}, κ = ψ_{M}d′, κ, e_{1} ∈ C^{d}(C) ∩ C_{κ}(e_{1}). If a ≺ κ, it follows κ, e_{1} ∈ C^{d}(C) ∩ C_{κ}(e_{1}) ⊂ C^{a}(C), d ∈ C^{a}(C) ∩ a ⊂ W. In the case κ = a we have a ∈ I, contradicting the assumption. If κ ≺ a, it follows κ = ψ_{M}d′ ∈ C^{κ}(C), d′ ∈ C^{κ}(C) ∩ C_{M}(d′) ⊂ C^{a}(C) by Lemma 5.1 (a), κ ∈ C^{a}(C) ∩ a ⊂ W. In all cases we have therefore d ⪯ e ∈ W, W ∩ e ≅ W (W) ∩ e, C|d ≅ W|d ≅ W (W)|d ≅ W (C)|d, d ∈ W (C)|d ⊂ C and the induction is complete. Let C′ := C ∪ {a}. W (C′) ∩ a ≅ W (C) ∩ a ≅ C′ ∩ a. τ^{C′}(a) ≅ τ^{W}(a) ⊂ W ∩ a ≅ C ≅ C′ ∩ a ⊂ W (C′), a ∈ M(W)|a ≅ M(C′)|a, therefore a ∈ W (C′) ∩ C′, W (C′)|a ≅ C′|a ≅ C′, Ag(C′), a ∈ C′. With C′′ := γ_{V}(C′) we have C′′ : P(N) (provable as in 4.9 (b)) C′′^{V,Cl} ≅ C′, therefore Ag(C′′^{V,Cl}) and a ∈ C′′^{V,Cl} ⊂ W. Lemma 5.4 ∀x ∈ W.Ω_{x} ∈ W. Proof: As in [Se98], Lemma 4.31. Lemma 5.5 Assume ψ_{ψ_{M}a}b ∈ A^{W}(W), Z := C^{ψ_{ψ_{M}a}b}(W) ∩ C_{ψ_{M}a}b.

(a) sc_{M}(a) ∪ {0, M} ⊂ Z.

(b) If x_{1}, x_{2} ∈ Z, x =_{NF} x_{1} + x_{2} ∨ x =_{NF} φ_{x_{1}}x_{2} ∨ x =_{NF} Ω_{x_{1}}, then x ∈ Z.

(c) If κ, c ∈ Z, κ ∈ R, κ, c ∈ C_{κ}(c), ψ_{M}a ⪯ κ, c ≺ b, then ψ_{κ}c ∈ Z.

(d) If c ∈ Z ∩ ψ_{M}a, then there exists A : P_{V}(N) such that Ag(A^{V,Cl}) ∧ c ∈ Z ⊂ c + 1 ∧ A^{V,Cl} ⊂ Z.

Proof: only (a): ψ_{M}a ∈ C_{ψ_{M}a}(b), therefore a ∈ C_{ψ_{M}a}(b), sc_{M}(a) ⊂ C_{ψ_{M}a}(b), sc_{M}(a) ≺ ψ_{M}a, further ψ_{ψ_{M}a}b ∈ C^{ψ_{ψ_{M}a}b}(W), ψ_{M}a ∈ C^{ψ_{ψ_{M}a}b}(W), a ∈ C^{ψ_{ψ_{M}a}b}(W), sc_{M}(a) ⊂ C^{ψ_{ψ_{M}a}b}(W). Lemma 5.6 Assume ψ_{ψ_{M}a}b ∈ A^{W}(W), Z := C^{ψ_{ψ_{M}a}b}(W) ∩ C_{ψ_{M}a}(b). Let Y_{0}^{0} := sc_{M}(a) ∪ {0, M}, P^{0} be a proof of Y^{0} ⊂ Z. Assume Y^{n} : P_{V}(N) be defined, P^{n} : (Y^{n})^{V,Cl} ⊂ Z. Y_{0}^{n+1} := {0, M} ∪ sc_{M}(a)∪

{x ∈ OT | ∃y, z ∈ (Y^{n})^{V,Cl}.x =_{NF} y + z ∨ x =_{NF} φ_{y}z ∨ x =_{NF} Ω_{y}} ∪ {x : N | ∃κ ∈ R ∩ Z.∃c ∈ Z.x = ψ_{κ}c ∈ OT ∧ ψ_{M}a ⪯ κ ∧ c ≺ b} ∪ {x : N|∃y ∈ (Y^{n})^{V,Cl} ∩ ψ_{ψ_{M}a}b.x ∈ (A_{y,P^{n}})^{V,Cl}}), where A_{y,P^{n}} : P_{V}(N), Ag(A_{y,P^{n}}^{V,Cl}), y ∈ A_{y,P^{n}}^{V,Cl} ⊂ y + 1 (which in fact depends on the proof of y ∈ (Y^{n})^{V,Cl} ∩ ψ_{ψ_{M}a}b) and Y^{n} := γ_{V}(Y_{0}^{n}), Y^{n} : P_{V}(N). P_{0}^{n+1} is a proof Y_{0}^{n+1} ⊂ Z. Let Y_{0} := {y : N | ∃n : N.y ∈ Y_{0}^{n}}, Y := γ_{V}(Y_{0}). Then it follows Y : P_{V}(N), Y^{V,Cl} ≅ Z. Proof: We easily see thatY^{V,Cl} ≅ Y_{0}, ∀n.(Y^{n})^{V,Cl} ≅ Y_{0}^{n}. Therefore it suffices to show Y_{0} ≅ Z. “⊂” follows by 5.5. “⊃” We first show by an easy induction on length(x):

∀x ∈ OT.sc_{M}(x) ⊂ Y_{0} ∧ G_{M}(x) ≺ b → x ∈ Y_{0} (∗)

Now we show by induction on length(a), c ∈ Z → c ∈ Y_{0}: If c = 0, M, it follows c ∈ Y_{0}. If c ⪯ sc_{M}(a), it follows c ∈ Z| max(sc_{M}(a)), max(sc_{M}(a)) ∈ Y_{0}, c ∈ A_{max(sc_{M}(a)),P^{0}}^{V,Cl} ⊂ Y_{0}. If c =_{NF} a_{1} + a_{2}, φ_{a_{1}}a_{2}, Ω_{a_{1}}, the assertion follows by IH. Assume now c = ψ_{κ}e, max(sc_{M}(a)) ≺ c. If ψ_{M}a ⪯ c, it follows κ, e ∈ Z, e ≺ b, by IH the assertion. If c ≺ ψ_{M}a, it follows c ≺ ψ_{ψ_{M}a}b, c ∈ W. Subcase κ = Ω_{e+1}: Ω_{e} ∈ W, e ∈ W, by IH e ∈ Y_{0}, κ ∈ Y_{0}, c ∈ W ∩ κ ⊂ Y_{0}. Subcase κ = M: then by ψ_{M}e ≺ ψ_{M}a, it follows e ≺ a, further ψ_{M}e ∈ W, ψ_{M}e ∈ C^{ψ_{M}e}(W), e ∈ C^{ψ_{M}e}(W), e ∈ C_{M}(e), sc_{M}(e) ⊂ C_{M}(e) ∩ M = ψ_{M}e, sc_{M}(e) ⊂ C^{ψ_{M}e}(W) ∩ ψ_{M}e ⊂ W ∩ ψ_{ψ_{M}a}b ⊂ Z, by IH sc_{M}(e) ⊂ Y_{0}, further G_{M}(e) ≺ e ≺ a ≺ b, and by (∗) e ∈ Y_{0}. ψ_{M}e ≺ ψ_{M}a, ψ_{M}e ⪯ sc_{M}(a) ∨ (e ≺ a ∧ sc_{M}(e) ≺ ψ_{M}a), by max(sc_{M}(a)) ≺ c, e ∈ Y_{0}, e ≺ a ≺ b, c = ψ_{M}e ∈ Y_{0}. Subcase κ = ψ_{M}d: ψ_{ψ_{M}d}e ≺ ψ_{ψ_{M}a}b. Then ψ_{M}d ⪯ ψ_{ψ_{M}a}b ∨ (d = a ∧ e ≺ b) ∨ ψ_{ψ_{M}d}e ≺ ψ_{M}a ≺ ψ_{M}d. Subsubcase ψ_{M}d ⪯ ψ_{ψ_{M}a}b. Then ψ_{M}d ≺ ψ_{M}a ∧ sc_{M}(d) ≺ ψ_{ψ_{M}a}b, therefore (ψ_{M}d ⪯ sc_{M}(a)∨d ≺ a)∧sc_{M}(d) ≺ ψ_{ψ_{M}a}b. If ψ_{M}d ⪯ sc_{M}(a), it follows ψ_{ψ_{M}d}e ∈ W| max(sc_{M}(a)) ⊂ Y_{0}. Otherwise d ≺ a ∧ sc_{M}(d) ≺ ψ_{ψ_{M}a}b. ψ_{ψ_{M}d}e ∈ W, therefore ψ_{M}d ∈ C^{ψ_{ψ_{M}d}e}(W) ∩ C_{ψ_{M}d}(e) ⊂ C^{ψ_{M}d}(W) by Lemma 5.1 (a), d ∈ C^{ψ_{M}d}(W), sc_{M}(d) ⊂ C^{ψ_{M}d}(W), sc_{M}(d) ⊂ C_{ψ_{M}d}(e) ∩ C_{M}(d) ∩ M = ψ_{ψ_{M}d}e, sc_{M}(d) ⊂ C^{ψ_{ψ_{M}d}e}(W ∩ ψ_{ψ_{M}d}e ⊂ Z. By IH sc_{M}(d) ⊂ Y_{0}, G_{M}(d) ≺ d ≺ a, by (∗) d ∈ Y_{0}. Since d ≺ a, it follows ψ_{M}d ∈ Y_{0}, ψ_{ψ_{M}d}e ∈ A_{ψ_{M}d,P^{n}}^{V,Cl} ⊂ Y_{0} for some n : N. Subsubcase d = a ∧ e ≺ b: c ∈ W. Therefore e, ψ_{M}a ∈ C^{ψ_{ψ_{M}a}e}(W) ∩ C_{ψ_{M}a}(e), by IH ψ_{M}a, e ∈ Z, e ≺ b, therefore c ∈ Z. Subsubcase ψ_{κ}e ≺ ψ_{M}a ≺ κ. From ψ_{κ}e ≺ ψ_{M}a it follows ψ_{κ}e ⪯ sc_{M}(a), ψ_{κ}e ∈ Y_{0}. Lemma 5.7 a ∈ A^{W}(W) ∩ M ⇒ A^{W}(W) ∩ a ≅ W ∩ a. Proof: “⊃”: trivial. “⊂”: Assume x ∈ A^{W}(W) ∩ a, show x ∈ W by induction on length(x). If x = 0, this is trivial. If x =_{NF} x_{1} + x_{2}, φ_{x_{1}}x_{2}, Ω_{x_{1}}, it follows x ∈ C^{x}(W), x_{i} ∈ τ^{W}(x) ⊂ W, x ∈ W. If x = ψ_{Ω_{c+1}}c, it follows Ω_{c} ∈ τ^{W}(x) ⊂ W, Ω_{c+1} ∈ W, x ∈ A^{W}(W)∩Ω_{c+1} ≅ A^{W}(W (W))∩ Ω_{c+1} ⊂ W (W) ∩ Ω_{c+1} ≅ W ∩ Ω_{c+1}. If x = ψ_{M}b, it follows ψ_{M}b ∈ C^{ψ_{M}b}(W), by 5.1 (a) b ∈ C^{ψ_{M}b}(W) ∩ C_{M}(b) ⊂ C^{a}(W), ψ_{M}b ∈ C^{a}(W) ∩ a ⊂ W. Case x = ψ_{ψ_{M}b}c. By Lemma 5.6 exists a Y : P_{V}(N) such that Y^{V,Cl} ≅ τ^{W}(ψ_{ψ_{M}b}c). Then by Lemma 5.3 it follows ψ_{ψ_{M}a}b ∈ W.

From now on, we will work in MLM. Lemma 5.8 (a) If a ∈ C^{b}(B), then ∃C : N.C ∈ P^{fin}(N)∧a ∈ C^{b}(C^{fin,Cl})∧C^{fin,Cl} ⊂ B,

where C^{fin,Cl} := {y : N | atom(y ∈_{fin} C)}.

(b) a ∈ C^{b}(B), B ⊂ C ⇒ a ∈ C^{b}(C).

(c) Assume C : P_{V}(N), C ⊂ W. Then ∃A : P_{V}(N).Ag(A^{V,Cl}) ∧ C ⊂ A^{V,Cl}.

(d) ∀x ∈ C^{a}(W).∃C : P_{V}(N).Ag(C^{V,Cl}) ∧ a ∈ C^{a}(C^{V,Cl})).

(e) (a) - (d) can be proved in ML_{2}. Proof: (a): Induction on length(a). (b): easy, (c): by [Se98], Lemma 4.26. Definition 5.9 (a) Univ_{0}(u_{0}, v_{0}) := u_{0}, Univ_{1}(u_{0}, v_{0}, z_{1}) := v_{0}z_{1},

Univ(u_{0}, v_{0}) := (x_{1}, y_{1})Univ_{0}(u_{0}, v_{0}), (x_{1}, y_{1}, z_{1})Univ_{1}(u_{0}, v_{0}, z_{1}). Under the assumption u_{0} : V, v_{0} : T(u_{0}) → V we have x_{1} : V, y_{1} : T(u) → V ⇒ Univ_{0}(u_{0}, v_{0}) : V, x_{1} : V, y_{1} : T(u) → V, z_{1} : T(Univ_{0}(u_{0}, v_{0})) ⇒ Univ_{1}(u_{0}, v_{0}, z_{1}) : V.

(b) Let f⃗:= Univ(u_{0}, v_{0}).

u_{1} := N̂f⃗, v_{1} := (x)N̂_{0,f⃗}, ι_{0,f⃗} := Res0f⃗(u_{1}, v_{1}), ι_{1,f⃗}(y) := Res1f⃗(u_{1}, v_{1}, y). Then, assuming u_{0}, v_{0} as above we have sf⃗(ι_{0,f⃗}) = Univ_{0}(u_{0}, v_{0}) = u_{0}, and for x : Tf⃗(ι_{0,f⃗}) sf⃗(ι_{1,f⃗}(y)) = Univ_{1}(u_{0}, v_{0}, y) = v_{0}y.

Lemma 5.10 Assume a ∈ A^{W}(W). Then there exists f, g such that u_{0} : V, v_{0} : T(u_{0}) → V ⇒ f(u_{0}, v_{0}) : V, u_{0} : V, v_{0} : T(u_{0}) → V, z_{1} : T(f(u_{0}, v_{0})) ⇒ g(u_{0}, v_{0}, z_{1}) : V, and with

f := (u_{0}, v_{0})s_{0}, g := (u_{0}, v_{0}, z_{1})t_{0}, f⃗:= f, g we have a ∈ A^{WV,Cl ; f⃗}(WV,Cl ; f⃗)

Proof: a ∈ C^{a}(W). By Lemma 5.8 (d) exists C : P_{V}(N) such that Ag(C^{V,Cl}) and a ∈ C^{a}(C^{V,Cl}). Let C′ := C^{V,Cl}. Assume u_{0} : V, v_{0} : T(u_{0}) → V. Let D := W_{Univ(u_{0},v_{0})}^{V,Cl} ∪ C′. Ag(D), γ_{V}(D) : P_{V}(D). C^{a}(D) ∩ a ⊂ τ^{W}(a) ⊂ W. Therefore there exists E_{u_{0},v_{0}} : P_{V}(N), Ag(E_{u_{0},v_{0}}) such that C^{a}(D)∩a ⊂ E_{u_{0},v_{0}}^{V,Cl}. f := (x_{1}, y_{1})N̂_{V}, and g := (x_{1}, y_{1}, z_{1})z_{1} ∈_{V} E_{u_{0},v_{0}} We have now:

(i) a ∈ C^{a}(WV,Cl ; f⃗):

u_{1} := N̂_{0,f⃗} : Uf⃗, u′_{1} := sf⃗(u_{1}), v_{1} := (x)C_{0}(x), v′_{1} := λx.sf⃗(C_{0}(x)), u_{2} := Res0f⃗(u_{1}, v_{1}) : Uf⃗, E_{0} := λy.Res1f⃗(u_{1}, v_{1}, y) : Pf⃗(N), sf⃗(u_{2}) = f(u′_{1}, v′_{1}) = N̂_{V}, and for x : T(N̂_{V}) = N, sf⃗(x ∈f⃗ E_{0}) = sf⃗(Res1f⃗(u_{1}, v_{1}, x)) = x ∈_{V} E_{u′_{1},v′_{1}}, as above C′ ∩ a ⊂ D ∩ a ⊂ C^{a}(D) ∩ a ⊂

E_{u′_{1},v′_{1}}^{V,Cl}, E_{u′_{1},v′_{1}}^{V,Cl} ≅ E_{0}^{f⃗,Cl}, Ag(E_{u′_{1},v′_{1}}^{V,Cl}), therefore Ag(E_{0}^{f⃗,Cl}), a ∈ C^{a}(C′), a ∈ C^{a}(C′ ∩ a),

a ∈ C^{a}(E_{0}^{f⃗,Cl}) ⊂ C^{a}(WV,Cl ; f⃗).

(ii) C^{a}(WV,Cl ; f⃗) ∩ a ⊂ Wf⃗:

Assume x ∈ C^{a}(WV,Cl ; f⃗) ∩ a. Then x ∈ C^{a}(A^{f⃗,Cl}) ∩ a for some A : Pf⃗(N), Ag(A^{f⃗,Cl}).

Let A′ := A^{f⃗,Cl}, u_{2} := N̂f⃗, u′_{2} := sf⃗(N̂f⃗), v_{2} := (y)y ∈f⃗ A, v′_{2} := λy.sf⃗(y ∈f⃗ A), E_{0} := λx.Res1f⃗(u_{2}, v_{2}, x). For x : N we have sf⃗(x ∈f⃗ E_{0}) = g(u′_{2}, v′_{2}, x) = x ∈_{V} E_{u′_{2},v′_{2}}, therefore

E_{0}^{f⃗,Cl} ≅ E_{u′_{2},v′_{2}}^{V,Cl}. C^{a}(W_{Univ(u′_{2},v′_{2})^{V,Cl}} ∪ C′) ∩ a ⊂ E_{u′_{2},v′_{2}}^{V,Cl} ≅ E_{0}^{f⃗,Cl}, Ag(E_{u′_{2},v′_{2}}^{V,Cl}), Ag(E_{0}^{f⃗,Cl}). By

Definition 5.9b ι_{0,u′_{2},v′_{2}} : U_{Univ(u′_{2},v′_{2})}, s_{Univ(u′_{2},v′_{2})}(ι_{0,u′_{2},v′_{2}}) = u′_{2} = N̂_{V}, s_{Univ(u′_{2},v′_{2})}(ι_{1,u′_{2},v′_{2}}(y)) = v′_{2}y = sf⃗(y ∈f⃗ A), with B := λy.ι_{1,u′_{2},v′_{2}}(y) we have B^{Univ(u′_{2},v′_{2}),Cl} ≅ A^{f⃗,Cl}, by Ag(A^{f⃗,Cl}) Ag(B^{Univ(u′_{2},v′_{2}),Cl}), A^{f⃗,Cl} ≅ B^{Univ(u′_{2},v′_{2}),Cl} ⊂

W_{Univ(u′_{2},v′_{2})}, x ∈ C^{a}(A^{f⃗,Cl}) ∩ a ⊂ C^{a}(W_{Univ(u′_{2},v′_{2})} ∪ C′) ∩ a ⊂ E_{u′_{2},v′_{2}}^{V,Cl} ≅ E_{0}^{f⃗,Cl} ⊂ WV,Cl ; f⃗.

Lemma 5.11 (a) A^{W}(W) ∩ M ⊂ W.

(b) W ∩ M ≅ W(W) ∩ M. Proof:

(a) Assume a ∈ A^{W}(W) ∩ M. By 5.10 exists f⃗ as before such that a ∈ A^{WV,Cl ; f⃗}(WV,Cl ; f⃗).

Let W′ := WV,Cl ; f⃗. By 5.7 it follows A^{W′}(W′)∩a ≅ W′ ∩a. Therefore W(W′)∩a ≅ W′ ∩a. A := (W′ ∩ a) ∪ {a}. Ag(A), γ_{V}(A) : P(N), γ_{V}(A)^{V,Cl} ≅ A, a ∈ A ⊂ W. (b): W ⊂ W(W), and by Ind(y ∈ W(W)), using (a) it follows ∀y ∈ W(W).y ≺ M → y ∈ W. Definition 5.12 W_{0} := W ∩ M, W_{S(i)} := W(W_{i}) ∩ Ω_{M+1·S(i)}. In the following we write M + i instead of M + 1 · i, similar for j, S(j), S(i) etc. instead of i. Lemma 5.13 For all i ≺ ω Ag(W_{i}) ∧ Ω_{M+i} ∈ W_{S(i)} ∧ W_{i} ≅ W_{S(i)} ∩ Ω_{M+i}. Proof: As in [Se98], Lemma 4.40. Theorem 5.14 For all n ∈ ℕ we have:

(a) MLM ⊢ ∀X : P(N).(∀y ∈ OT.(∀x ≺ y.x ∈ X) → y ∈ X) → ∀y ≺ ψ_{Ω_{1}}Ω_{M+n}.y ∈ X.

(b) If MLM ⊢ Δ ⇒ A ∈ Cl(N), then MLM ⊢ Δ ⇒ (∀y ∈ OT.(∀x ≺ y.x ∈ A) → y ∈ A) → ∀y ≺ ψ_{Ω_{1}}Ω_{M+n}.y ∈ A.

Proof: As Theorem 4.41 in [Se98]

References

[Bu75] W. Buchholz: Normalfunktionen und konstruktive Systeme von Ordinalzahlen. In J. Diller and G.H. Müller (Eds.): Proof Theory Symposium, Kiel 1974, Springer lecture notes in Mathematics 500, 1975, pp. 4 – 25.

[Bu90] W. Buchholz: Wellordering proofs for systems of fundamental sequences, Draft, München, 1990.

[Bu92] W. Buchholz: A simplified version of local predicativity. In: P. Aczel et al. (Eds.): Proof theory. Cambridge University Press, Cambridge, 1992, pp. 115 – 147.

[Bu93] W. Buchholz: A note on the ordinal analysis of KPM in: J. Oikkonen and J. Väänänen (Eds.): Logic Colloquium’90, Proceedings of the ASL Summer Meeting Helsinki. Springer Lecture Notes in Logic 3, 1993, pp. 1 – 9.

[GR94] E. Griffor and M. Rathjen: The strength of some Martin-Löf type theories. Archive for Mathematical Logic 33, 1994, pp. 347 – 385.

[Pa91] E. Palmgren: Transfinite hierarchies of universes. U.U.D.M. Report 1991:7, Uppsala University, Department of Mathematics, P.O. Box 480, S-756 45 Uppsala, Sweden.

[Pa92] E. Palmgren: Type-theoretic interpretation of iterated, strictly positive inductive definitions, Archive for Mathematical Logic 32, 75 – 99, 1992.

[Pa98] E. Palmgren On universes in type theory. To appear in G. Sambin and J. Smith (Eds.): Twenty five years of constructive type theory. Oxford University Press.

[PSH90] E. Palmgren and V. Stoltenberg-Hansen. Domain interpretations of Martin-Löf’s partial type theory. Annals of Pure and Applied Logic 48, 135 – 196, 1990.

[Ra90] M. Rathjen: Ordinal notations based on a weakly Mahlo cardinal. Archive for Mathematical Logic 29, 249 – 263, 1990.

[Ra91] M. Rathjen: Proof-theoretical analysis of KPM, Archive for Mathematical Logic 30, 377 – 403, 1991.

[Ra94] M. Rathjen: Collapsing functions based on recursively large ordinals. A wellordering proof for KPM. Archive for Mathematical Logic 33, 35 – 55, 1994.

[RGP98] M. Rathjen, E. R. Griffor and E. Palmgren, Inaccessibility in constructive set theory and type theory. Annals of Pure and Applied Logic 94, 181 – 200, 1998.

[Se93] A. Setzer: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe. PhD-thesis, Munich, 1993. Available via http://www.math.uu.se/∼setzer/articles/weor0.dvi.gz.

[Se96a] A. Setzer: A Model for a type theory with Mahlo universe. Draft. Available via http://www.math.uu.se/∼setzer/articles/uppermahlo.dvi.gz.

[Se96b] A. Setzer: An upper bound for the proof theoretical strength of Martin-Löf type theory with W-type and one universe. Draft. Available via http://www.math.uu.se/∼setzer/articles/1papdiss.dvi.gz [Se98] A. Setzer: Well-ordering proofs for Martin-Löf type theory. Annals of Pure and

Applied Logic 92:113 – 159, 1998.

[TD88] A. Troelstra and D. van Dalen. Constructivism in mathematics. An introduction, vol. II. North-Holland, Amsterdam, 1988.