Well-ordering proofs for Martin-Löf Type Theory ⋆

Anton Setzer

Department of Mathematics, Uppsala University, Box 480, S-751 06 Uppsala, Sweden, email: setzer@math.uu.se

Abstract

We present well-ordering proofs for Martin-Löf’s type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in [Set93] show that the proof theoretical strength of the type theory is precisely ψ_{Ω_{1}}Ω_{I+ω}, which is slightly more than the strength of Feferman’s theory T_{0}, classical set theory KPI and the subsystem of analysis (Δ_{2}^{1} −CA)+(BI). The strength of intensional and extensional version, of the version à la Tarski and à la Russell are shown to be the same.

0 Introduction

0.1 Proof theory and Type Theory

Proof theory and type theory have been two answers of mathematical logic to the crisis of the foundations of mathematics at the beginning of the century. Proof theory was originally established by Hilbert in order to prove the consistency of theories by using finitary methods. When Gödel showed that Hilbert’s program cannot be carried out as originally intended, the focus of proof theory changed towards analyzing theories and determination of the minimum of strength needed in order to prove their consistency. Proof theory has been very successful in providing an excellent measure for theories, the proof theoretical strength.

On the other hand, type theories were designed to provide a new framework for mathematics, the consistency of which can be justified by itself.

⋆ part of this research was done while the author was visiting the University of Leeds as part of the EC Twinning Project “Proofs and Computation”

Preprint submitted to Elsevier Preprint 7 March 1998

Both directions of mathematical logic have become quite important recently because of their applicability to computer science. Proof theoretical methods are used for instance to extract programs from proofs, to analyze term rewriting systems and for theoretical questions in the area of logic programming.

On the other hand a lot of systems for machine assisted theorem proving are based on type theory. One reason why type theory is an excellent basis theory is that in type theory algorithms and proofs are more or less the same. We see here that in these areas questions concerning foundations and applications are very closely related: a good understanding of a situation is the best basis for finding ways to do what we want to do in a better way.

When looking at these two fields it seems to be interesting to apply proof theory to type theory. In particular, the question mainly answered in this article is: what is the precise proof theoretical strength of Martin-Löf’s type theory. This is interesting because the answer determines the exact place of Martin-Löf’s type theory on the proof theoretic scale. This allows to compare it with other theories, the strength of which is already known.

More precisely, in this article we are dealing with the strength of Martin-Löf’s type theory with one universe and W-type. This work was first presented in our thesis [Set93]. There are two directions to be proved. One is to determine an upper bound, a refined version of which is presented in [Set96c]. There we embed type theory in a Kripke-Platek style set theory, KPI^{+}, the strength of which can be determined easily. The more difficult direction of the proof, which is carried out in this article, is to show that this bound is sharp. The importance of this question became obvious to the author after a talk he gave on the upper bound, where a proof theorist commented: “Okay, it’s clear that Martin-Löf’s type theory can be embedded like this, but is Martin-Löf’s type theory really as strong as you claim it is?”. The answer now is: it has exactly the strength the author conjectured at that time.

0.2 Well-ordering Proofs

To prove that the strength conjectured is precise is technically complicated. We are going to prove directly that the type theory considered proves transfinite induction up to an ordinal notation for ψ_{Ω_{1}}Ω_{I+n} for every n ∈ ω. Since our proposed strength is ψ_{Ω_{1}}Ω_{I+ω} = sup_{n∈ω} ψ_{Ω_{1}}Ω_{I+n}, this shows that the proof theoretical strength, which is the supremum of all ordinals up to which the theory proves transfinite induction, is ≥ ψ_{Ω_{1}}Ω_{I+ω}.

We will use the method of distinguished sets (in German “ausgezeichnete Mengen”) developed mainly by Buchholz and Schütte for carrying out wellordering proofs. This well-established method has been modified by the author, who introduced some new techniques in order to make these methods applicable to the type theoretic setting.

Carrying out these well-ordering proofs means to present the logically most complicated proofs that can be carried out in the system. To reach the full strength we have to use the full power of the theory. In applications, often powerful theories like Calculus of Constructions or extensions of Martin-Löf’s type theory form the basis theory, although the full power of these theories is not needed. In a well-ordering proof for all ordinals below the proof theoretical strength, we actually have to use all the power available.

0.3 The State of Knowledge

In [GR94] Griffor and Rathjen were, independent of the author and in parallel, following another approach towards determining the proof theoretical strength of Martin-Löf’s type theory by embedding constructive set theory into type theory. [GR94] contains an excellent review of all the research carried out in the past in this area. We refer the interested reader to that article and only mention the main new results concerning type theory obtained in [GR94]. Griffor and Rathjen showed, that the theory ML_{1}V, Martin-Löf’s type theory with one universe and Aczel’s iterative set V or elimination rules for the universe or both has the strength of Kripke-Platek set theory KPω. They showed, that type theory with one universe and the W-type restricted to elements of the universe only, which they called ML_{1W}, has strength (Δ_{2}^{1} − CA) + (BI). Adding elimination rules for the universe and/or Aczel’s iterative set V is shown to yield the same strength. For the strength of ML_{1}W, the theory considered here, they determined independently the same upper bound as it was done by the author (ψ_{Ω_{1}}Ω_{I+ω}). The exact strength is not determined there, concerning the lower bound they only noted that it is naturally stronger than ML_{1W}. For the precise strength, they referred to our thesis [Set93], on which the present article is based. In [GR94] the obvious generalization of these results to n universes and ω universes together with their strength is mentioned as well (no proof is given). In order to avoid confusion, we would like to mention some typos in [GR94], as pointed out by Rathjen to the author, namely the ordinals on page 384, lines 20, 22 and 23 should be read as ψ_{Ω_{1}}Ω_{I+ω}, ψ_{Ω_{1}}Ω_{I+n} and ψ_{Ω_{1}}Ω_{I+ω} instead of ψΩ_{1}(I + ω), ψΩ_{1}(I + n) and ψΩ_{1}(I + ω).

0.4 Overview

The content of our article is as follows: In Sect. 1 we will introduce the ψfunction in ZF+∃x.(x regular cardinal ∧ℵ_{x} = x). Based on the set theoretical system we introduce in Sect. 2 the ordinal notation system OT. In Appendix B the reader can find a proof that the order-type of the ordinals is in accordance with the set theoretical definition of the functions. In Sect. 3 we introduce two versions of Martin-Löf’s type theory with W-type and one universe: ML_{J} (where J stands for the constructor in the elimination rules for the identity type) is what seems to be (apart from extensions by the logical framework) the currently most widely accepted version. ML_{[TD]} is essentially the version in the book by Troelstra and van Dalen [TD88] (the index [TD] refers to that book). In order to switch more easily between elements of the universe and types, we introduce variants ML_{J,aux} and ML_{[TD],aux}. Sect.4 of the article contains the well-ordering proof itself. The technique used there is a modification of the usual well-ordering techniques, which we hope, is more intuitive. Buchholz gave some useful hints for these modifications. We will omit in this section all the complicated type theoretic definitions. Instead we make assumptions about possible constructions, which are actually carried out in Sect. 5.

0.5 Why Do We Use Set Theory?

In this article we will work in Sect. 1 and in the appendix directly in set theory. Especially the readers coming from type theory might ask in what sense this is necessary.

First of all: In all other sections apart from those mentioned above we show, without referring to set theory, that in our version of Martin-Löf’s type theory we can show that a certain primitive recursive ordering on the primitive recursive subset OT of the natural numbers is a well-ordering. Therefore, those readers who reject set theory as a basis of mathematics might consider the set theoretic part as mere heuristic.

Second: Set theory is here needed in order to give a representation of the order type of the ordinal notation on the universal scale, namely the scale of ordinals in set theory. This can by definition not be done without using set theory, and exactly for this set theory is needed in this article.

Another point, the author was several times confronted with, is the fact that we need to assume the existence of a large cardinal: of one inaccessible. Now this is necessary for the approach taken here (in the sections dealing with set theory). But we could as well replace all cardinals by admissibles and the first inaccessible by the first recursively inaccessible and get in the only relevant part of the system, namely the part below Ω_{1}, exactly the same ordinals (see for instance [Rat93]). So all the set theoretic part could have been carried out in ZF or some weak fragment of set theory (e.g. Kripke-Platek set theory, extended by one inaccessible and ω + 1 admissibles above it) as well.

One could even replace the cardinals by smaller ordinals. Let o(b) be the ordinal denoted by b and Ω_{1} be the notation, which is in this article interpreted as ℵ_{1}. The only property for o(Ω_{1}), we need is that o(b) < o(Ω_{1}) for all b ≺ Ω_{1}. The minimal solution would be o(Ω_{1}) = min{γ|∀b ∈ OT.b ≺ Ω_{1} → o(b) < γ}, although in our setting we cannot define this, since we need to know o(Ω_{1}) in order to determining o(b) for all b ≺ Ω_{1}. Very roughly speaking the interpretation of an ordinal term which represents a cardinal is just an ordinal, “big enough for having some closure properties”.

0.6 Help for Researchers outside Proof Theory

In this article we will concentrate on carrying out the technical proofs carefully and in detail. In [Set97a] we will provide more intuition and motivation for the methods used and give some introduction into collapsing functions. Unfortunately, this article covers only the strength up to Ω_{ω}, but a future article is planned in which the bigger ordinals are covered as well.

0.7 Extensions and Future Research

It should be easy to extend the well-ordering proofs, carried out in this article, to stronger theories. To show, that the strength of Martin-Löf’s type theory with n Universes is ψ_{Ω_{1}}Ω_{I_{n}+ω}, where I_{n} is the n-th inaccessible, should not cause any problems and this implies that the strength of the theory with arbitrary finitely iterated universes is ψ_{Ω_{1}}I_{ω}, I_{ω} = sup{I_{n} | n ∈ ω}.

We have carried out the ordinal analysis of the extension of Martin-Löf’s type theory by one Mahlo universe ([Set96a,Set96b]), and determined its strength as ψ_{Ω_{1}}Ω_{M+ω}, where M is the first Mahlo cardinal (one needs to extend the ψ-functions to cover this strength). We are working on extensions by even bigger universes.

In [Set97b] we show that every arithmetical Π_{2}-sentence provable in KPI^{+}, Kripke-Platek set theory with ω universes, is provable in the type theory considered here. This is done by carrying out cut elimination for KPI^{+} using transfinite induction up to ψ_{Ω_{1}}Ω_{I+n}.

0.8 Concluding Remarks

The article is self-contained, except for some lemmata cited in Sect. 1. So all the proof-theoretical and type theoretical definitions are included.

The author wants to thank W. Buchholz for introducing him into proof theory and especially into the technique of well-ordering proofs and for his precious hints. Further he wants to thank H. Schwichtenberg and S.S. Wainer for their assistance and support, for motivation and for a lot of fruitful discussions.

1 Ordinals in Set Theory

We will first start to present set theoretically the ordinal functions. These functions form the basis of the ordinal notation system, which we will introduce in Sect. 2, and allow to determine the order-type of this system and of each ordinal notation. The system is a slight modification of the system presented in [Buc92], and some properties are determined as in [BS88].

1.1 The ψ-functions

Preliminaries 1.1 In this section we will work in ZF+∃x.(x regular cardinal ∧ℵ_{x} = x).

Definition 1.2 (variant of Definition 4.1 of [Buc92]) Let # be the natural sum on ordinals. Ω_{0} := 0, Ω_{σ} := ℵ_{σ} for σ > 0. I := min{σ | σ regular Cardinal ∧ Ω_{σ} = σ}, the first weakly inaccessible cardinal. I^{+} := sup{ζ_{n} | n < ω}, where ζ_{0} := Ω_{I+1}, ζ_{n+1} := Ω_{ζ_{n}}, Ord := {α | α ordinal , α < I^{+}}, R := {σ ∈ Ord | ω < σ ∧ σ regular } = {I} ∪ {Ω_{σ+1} | σ < I^{+}}. In this section let α, β, γ, δ, ρ be elements of Ord, κ, λ, π, σ, τ be elements of R, all possibly with subscripts or accents. Let φ be the usual Veblen function.

Definition 1.3 (variant of Definition 4.1 of [Buc92]) By transfinite recursion on α, we define simultaneously for all κ ordinals ψ_{κ}α (κ ∈ R) and sets C(α, β) ⊆ Ord as follows:

ψ_{κ}α := min{β | κ ∈ C(α, β) ∧ C(α, β) ∩ κ ⊆ β} ,
C(α, β) := \{ \begin{matrix}the closure of β ∪ \{0, I\} under the functions \\ +, φ, σ ↦ Ω_{σ}, (π, ξ) ↦ ψ_{π}ξ (π ∈ R, ξ < α) \end{matrix} .

(Note that by IH ψ_{π}ξ is already defined for all ξ < α, π ∈ R.) We define ψ_{κ} : Ord ⟶ Ord, ψ_{κ}(α) := ψ_{κ}α. C_{κ}(α) := C(α, ψ_{κ}α).

Lemma 1.4 (Lemma 4.4 of [Buc92])

(a) β < π ⇒ cardinality(C(α, β)) < π

(b) C(α, β) = ⋃_{η<β} C(α, η), for each limit ordinal β.

(c) κ ∈ C(α, κ).

(d) C_{κ}(α) ∩ κ = ψ_{κ}α.

Proof: All statements are immediate consequences of Definition 1.3. ⊓ ⊔

Lemma 1.5 (Lemma 4.5 of [Buc92])

(a) ψ_{κ}α < κ ∧ ψ_{κ}α ∉ C_{κ}(α)

(b) (α_{0} < α ∧ α_{0} ∈ C_{κ}(α)) ⇒ ψ_{κ}α_{0} < ψ_{κ}α

(c) ψ_{κ}α ∉ {Ω_{σ} | σ < Ω_{σ}} ∪ {0} ∧ ∀ξ, η < ψ_{κ}α.φ_{ξ}η, ξ + η < ψ_{κ}α.

(d) Ω_{σ} ∈ C(α, β) ⇒ σ ∈ C(α, β)

(e) ω^{ξ_{0}}# ⋯ #ω^{ξ_{n}} ∈ C(α, β) ⇒ {ξ_{0}, …, ξ_{n}} ⊆ C(α, β)

(f) κ = Ω_{σ+1} ⇒ Ω_{σ} < ψ_{κ}α < Ω_{σ+1}

(g) Ω_{ψ_{I}α} = ψ_{I}α

(h) (Ω_{σ} ≤ γ ≤ Ω_{σ+1} ∧ γ ∈ C(α, β)) ⇒ σ ∈ C(α, β).

(i) α_{0} ≤ α ⇒ (ψ_{κ}α_{0} ≤ ψ_{κ}α ∧ C_{κ}(α_{0}) ⊆ C_{κ}(α))

Proof: See [Buc92]. Only in (c), we vary, but the unproven part is trivial. ⊓ ⊔

Lemma 1.6 (α ∈ C_{κ}(α) ∧ β ∈ C_{π}(β)) ⇒ (ψ_{κ}α = ψ_{π}β ⇔ (α = β ∧ κ = π))

Proof: Assume α ∈ C_{κ}(α) ∧ β ∈ C_{π}(β). “⇐”: trivial. “⇒”: Assume ψ_{κ}α = ψ_{π}β. Case κ = Ω_{σ+1} ∧ π = I. Then ψ_{π}β = Ω_{ψ_{π}β}, Ω_{σ} < ψ_{κ}α < Ω_{σ+1}, ψ_{κ}α ≠ Ω_{ψ_{κ}α}, a contradiction. The case κ = I ≠ π is similar. Case κ = Ω_{σ+1}, π = Ω_{ρ+1}, σ ≠ ρ. If σ < ρ, ψ_{κ}α < κ ≤ Ω_{ρ} < ψ_{π}β, a contradiction, similarly we get a contradiction if ρ < σ. Therefore π = κ. In case of α < β, α ∈ C(α, ψ_{κ}α) ⊆ C(β, ψ_{κ}α) = C_{π}(β), by Lemma 1.5 (b) ψ_{κ}α < ψ_{π}β a contradiction. The case β < α is similar. Therefore we conclude α = β. ⊓ ⊔

Definition 1.7 (a) Lim := {α ∈ Ord | α limit ordinal }, Suc := {α + 1 | α ∈ Ord}, A := {α ∈ Ord | α > 0 ∧ ∀β, γ < α.β + γ < α}, G := {α ∈ Ord | α Gamma ordinal } = {α ∈ Ord | α = φ_{α}0}, Car := {Ω_{α} | 0 < α ∈ Ord}, Fi := {α ∈ Ord | 0 < α = Ω_{α}}.

(b) α =′_{NF} β + γ :⇔ α = β + γ = β#γ ∧ γ ∈ A ∧ β ≠ 0. α =_{NF} β + γ :⇔ α = β + γ = β#γ ∧ β ≠ 0 ∧ γ ≠ 0. α =_{NF} φ_{β}γ :⇔ α = φ_{β}γ ∧ β, γ < α. α =_{NF} Ω_{β} :⇔ α = Ω_{β} ∧ β < α. α =_{NF} ψ_{π}γ :⇔ π ∈ R ∧ α = ψ_{π}γ ∧ γ ∈ C_{π}(γ).

(c) For κ ∈ R we define κ^{−} by: Ω_{σ+1}^{−} := Ω_{σ}, I^{−} := 0.

Remark 1.8 (a) If α =′_{NF} β +γ ∧α =′_{NF} β′ +γ′ or α =_{NF} φ_{β}γ ∧α =_{NF} φ_{β′}γ′ or α =_{NF} Ω_{β} ∧ α =_{NF} Ω_{β′} ∧ γ = γ′ or α =_{NF} ψ_{β}γ ∧ α =_{NF} ψ_{β′}γ′ then β = β′ ∧ γ = γ′.

(b) The sets {0}, {I}, {α | ∃β, γ.α =_{NF} β + γ}, {α | ∃β, γ.α =_{NF} φ_{β}γ}, {α | ∃β.α =_{NF} Ω_{β}}, {α | ∃π, γ.α =_{NF} ψ_{π}γ} are disjoint.

The following shows, that in the situation β < α, π, β ∈ C_{σ}(α) we only need to add ψ_{π}β to C_{σ}(α) if ψ_{π}β =_{NF} ψ_{π}β, i.e. if β ∈ C_{π}(β):

Definition 1.9

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

Lemma 1.10 (a) C_{κ}(α) = C′_{κ}(α).

(b) I ≠ κ ∈ R ⇒ C_{κ}(α) = C′(α, κ^{−} + 1).

(c) C_{Ω_{1}}(I^{+}) = C′(I^{+}, 0)

Proof: In the appendix, Sect. A. ⊓ ⊔

Corollary 1.11 Assume (I ≠ κ ∧ ρ = κ^{−} + 1) ∨ (κ = I ∧ ρ = ψ_{I}β), ρ ≤ α ∈ C_{κ}(β).

(a) α = I ∨ ∃γ, δ ∈ C_{κ}(β).(α =′_{NF} γ + δ ∨ α =_{NF} φ_{γ}δ ∨ α =_{NF} Ω_{γ} ∨ (α =_{NF} ψ_{γ}δ ∧ δ < β))

(b) If α =_{NF} φ_{γ}δ ∨ α =_{NF} γ + δ ∨ α =_{NF} ψ_{γ}δ ∨ (α =_{NF} Ω_{γ} ∧ γ = δ) then γ, δ ∈ C_{κ}(β).

Proof: α ∈ C_{κ}(β) = C′(β, ρ). ⊓ ⊔ 1.2 Definition of G_{π}ρ

We want to define in Sect. 2 primitive recursively an ordinal notation system for the ordinals in C_{Ω_{1}}(I^{+}) using the functions defined above. In order to obtain unique terms it is necessary to define the sets C_{π}(α) or more precisely represent these sets. This is done by first defining finite sets of ordinals G_{π}(α). These sets can be represented in our term system, and using Lemma 1.13 we can define representations of the sets C_{π}(α) in the system of terms.

Definition 1.12 Definition of finite sets G_{π}(α) for α ∈ C_{Ω_{1}}(I^{+}) = C′(I^{+}, 0) by recursion on the minimal n such that α ∈ C^{′n}(I^{+}, 0).

(G1) G_{π}0 := G_{π}I := ∅.
(G2) γ =′_{NF} δ + ρ or γ =_{NF} φ_{δ}ρ or (γ =_{NF} Ω_{δ} ∧ ρ = δ) then

G_{π}(γ) := G_{π}δ ∪ G_{π}ρ.

(G3) If ρ =_{NF} ψ_{κ}β, then

G_{π}ρ := \{ \begin{matrix}\{β\} ∪ G_{π}κ ∪ G_{π}β, & if π ≤ κ ≠ I∨ \\ & (κ = I ∧ (π ≤ ψ_{I}β ∨ π = I)), \\ G_{π}κ & if κ < π = I \\ ∅, & if κ < π ≠ I or \\ & κ = I ∧ ψ_{I}β < π < I. \end{matrix}

Lemma 1.13 If α ∈ C_{Ω_{1}}(I^{+}), then α ∈ C_{π}(β) ⇔ G_{π}(α) < β.

Proof: Induction on n, such that α ∈ C′^{n}(I^{+}, 0). If α = 0, I or α =′_{NF} γ + δ, φ_{γ}δ, Ω_{γ}, the assertion follows by IH or immediately. Let α = ψ_{κ}ξ, ξ ∈ C_{κ}(ξ), ξ, κ ∈ C′(I^{+}, 0). Suppose π = κ. Using the IH for ξ, β in one direction we infer α ∈ C_{π}(β) ⇒ α < ψ_{π}β ⇒ ξ < β ∧ κ, ξ ∈ C(ξ, α) ⊆ C(β, ψ_{π}β) = C_{π}(β) ⇒ G_{π}(α) = G_{π}(ξ) ∪ G_{π}(κ) ∪ {ξ} < β, and in the other direction G_{π}(α) < β ⇒ ξ, κ ∈ C_{π}(β) ∧ ξ < β ⇒ ψ_{κ}ξ ∈ C_{π}(β) Suppose κ < π ≠ I. Then G_{π}(α) = ∅, α ∈ C_{π}(β). Suppose π < κ ≠ I. Then α ∈ C_{π}(β) ⇔ κ, ξ ∈ C_{π}(β) ∧ ξ < β. Suppose π < κ = I. In case of ψ_{κ}ξ < π, it follows ψ_{κ}ξ ∈ C_{π}(β), G_{π}(α) = ∅, and if π ≤ ψ_{κ}ξ, ψ_{κ}ξ ∈ C_{π}(α) ⇔ κ, ξ ∈ C_{π}(β) ∧ ξ < β ⇔ G_{π}(α) < β. Suppose κ < π = I. Then α ∈ C_{π}(β) ⇔ ψ_{κ}ξ < ψ_{π}β ⇔ κ < ψ_{π}β ⇔ κ ∈ C_{π}(β) ⇔ G_{π}(κ) < β ⇔ G_{π}(α) < β. ⊓ ⊔ 2 The Notation System OT

2.1 Introduction of the Notation System

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 2.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 ∈ A.x ∈ B and A ≅ B :≡ A ⊆ B ∧ B ⊆ A. In the following assume a, b, c, n, m, π, κ, λ ∈ ℕ.

We will, as usual in proof theory, first introduce a system of terms and an ordering on these terms, and then define the set of ordinal notations OT as a subset of these terms.

Definition 2.2 We give an inductive definition of sets T′, Suc′, A′, G′, Car′, R′, Fi′ of terms together with length(a) for a ∈ T′, where we assume some coding of the terms as natural numbers. All the sets and length can be defined primitive recursively. (T′ is a set of terms denoting ordinals and Suc′, A′, G′, Car′, R′, Fi′ contain terms of T′, which, if in normal form, correspond to elements of Suc, A, G, Car, R, Fi respectively.)

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

t := (a_{0}, …, a_{n}) ∈ T′, if a_{n} ∈ Suc′, then t ∈ Suc′, length(t) := length(a_{0}) + ⋯ + length(a_{n}). (T′ 3) If a, b ∈ T′, then t := φ′_{a}b ∈ A′, 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 π = I, then t ∈ Fi′.

length(t) := length(π) + length(b).

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

(T′ 6) I ∈ Fi′ ∩ R′, length(I) := 1.

(T′ 7) R′ ⊆ Car′ ⊆ G′ ⊆ A′ ⊆ T′, Fi′ ⊆ Car′ ⊆ G′, Suc′ ⊆ T′.

Lim′ := T′ \ ({0_{OT}} ∪ Suc′). For a ∈ A′, (a) := a. () := 0. Therefore for every a ∈ T′ there exists a unique n ≥ 0 and unique a_{1}, …, a_{n} such that a = (a_{1}, …, 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 natural numbers considered as natural numbers not coding elements of T′.

Definition 2.3 Definition of a ≺′ b for a, b ∈ T′ (which can be defined as a primitive recursive relation) by recursion on length(a) + length(b), using in the definition a ⪯′ b as an abbreviation for a ≺′ b ∨ a = b. Later ≺ will be defined 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} ∈ A′, 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′,b, d ∈ T′, then
(ψ_{π}b ≺′ ψ_{κ}d) :⇔
(π = κ ∧ b ≺′ d) ∨ (κ ≠ I ≠ π ∧ π ≺′ κ)∨
(π = I ≠ κ ∧ ψ_{π}b ≺′ κ)∨
(π ≠ κ = I ∧ π ≺′ ψ_{κ}d)
(≺′ 6) If I ≠ π ∈ R′, κ ∈ Car′, b ∈ T′, then
(ψ_{π}b ≺′ κ) :⇔ π ⪯′ κ
(≺′ 7) b, c ∈ T′, then
(ψ_{I}b ≺′ Ω′_{c}) :⇔ ψ_{I}b ⪯′ c
(≺′ 8) If b ∈ T′, then
ψ_{I}b ≺′ I.
(≺′ 9) If a, c ∈ T′, then
(Ω′_{a} ≺′ Ω′_{c}) :⇔ (a ≺′ c)
(≺′ 10) If a ∈ T′, then
(Ω′_{a} ≺′ I) :⇔ (a ≺′ I).
(≺′ 11) In all other cases a ≺′ b :⇔ ¬(b ⪯′ a).

Lemma 2.4 ≺′ is a linear ordering on T′.

Proof: easy, but tedious. ⊓ ⊔

Definition 2.5 We assume some implementation of finite sets A as natural numbers together with an element relation ∈ in Heyting Arithmetic such that the usual properties hold, especially, if ϕ(x) is a primitive recursive decidable predicate, then ∀x ∈ A.ϕ(x) is decidable, and, if B is a primitive recursive set of natural numbers, the set P^{fin}(B) of finite sets which are subsets of B is primitive recursive.

Definition 2.6 Assume a ∈ T′, M, M′ primitive recursive sets. (Later, when we are going to work in Martin-Löf’s type theory, this definition will be applied to the subsets and subclasses of ℕ of this system. Further this definition applies to ≺, ⪯ as defined later as well)

M ⪯′ M′:⇔ ∀x ∈ M∃y ∈ M′(x ⪯′ y),
M ≺′ M′:⇔ ∀x ∈ M∃y ∈ M′(x ≺′ y),
a ⪯′ M :⇔ {a} ⪯′ M.

The ψ-function in the set theoretical system are not injective. Therefore, several terms of T′ denote the same ordinals. In order to get an injective map from ordinal terms into the ordinals, we need to define a set OT of restricted ordinal notations, such that every ordinal term in OT denotes a unique ordinal. The uniqueness is achieved, if we add ψ_{κ}c to OT only, if for the ordinals κ′, γ denoted by κ, c we have γ ∈ C_{κ′}(γ). Lemma 1.10 (c) allows us to show that in this way we get notations for all ordinals in C(I^{+}, 0). We introduce sets C_{κ}(c), corresponding to C_{κ′}(γ) by Lemma 1.13 via the sets G_{κ}(c), corresponding to G_{κ′}(γ).

Definition 2.7 Inductive definition of the finite subset G_{π}a of N for π ∈ R′, a ∈ T′ by recursion on length(a).

(G1) G_{π}(0) := ∅.
(G2) If a_{0}, …, a_{n} ∈ A′, n > 0 then
G_{π}((a_{0}, …, a_{n})) := G_{π}(a_{0}) ∪ ⋯ ∪ G_{π}(a_{n})
(G3) If a, b ∈ T′, then G_{π}(φ′_{a}b) := G_{π}(a) ∪ G_{π}(b).
(G4) If κ ∈ R′, b ∈ T′, then
G_{π}(ψ_{κ}b) :=
{b} ∪ G_{π}(κ) ∪ G_{π}(b), if π ⪯′ κ ≠ I∨
(κ = I ∧ (π ⪯′ ψ_{I}b ∨ π = I)),
G_{π}(κ)  if κ ≺′ π = I
∅,  if κ ≺′ π ≠ I or
κ = I ∧ ψ_{I}b ≺′ π ≺′ I.
(G5) If a ∈ T′, then G_{π}(Ω′_{a}) := G_{π}(a).
(G6) G_{π}(I) := ∅.

G_{π}^{0}(a) := G_{π}(a) ∪ {0}.

In the following we define some sets which are analogues to the set theoretic constructions. The restriction of these sets to OT, as defined later, will give the direct translation of the constructions in set theory.

Definition 2.8 (a) For a ∈ T′ we define the primitive-recursive set Cr′(a) of a-critical terms in T′, (more precisely λx.y.x ∈_{dec} Cr′(y) will be primitive recursive, where x ∈_{dec} Cr′(y) is the boolean value corresponding to the relation x ∈ Cr′(y)): 0, (a_{1}, …, a_{n}) ∉ Cr′(a). φ′_{b}c ∈ Cr′(a) :⇔ a ≺′ b. If b ∈ G′, then b ∈ Cr′(a) :⇔ a ≺′ b.

(b) For a, b ∈ T′ we define C̃_{a}(b) := {c ∈ T′ | G_{a}(c) ≺′ b}, which is primitive recursive (again more precisely λx.y, z.x ∈_{dec} C̃_{y}(z) will be primitive recursive). (C̃_{a}(b) corresponds to the set C_{α}(β) in set theory.)

Definition 2.9 We define the set OT of ordinal notations, which will be a subset of T′.

(OT 1) 0 ∈ OT.

(OT 2) If n > 0, a_{0}, …, a_{n} ∈ OT ∩ A′, a_{n} ⪯′ a_{n−1} ⪯′ ⋯ ⪯′ 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, G_{π}(b) ≺′ b, then
ψ_{π}b ∈ OT,
(OT 5) If a ∈ OT \ (Fi′ ∪ {0}), then Ω′_{a} ∈ OT.
(OT 6) I ∈ OT.

Fi := Fi′ ∩ OT, R := R′ ∩ OT, G := G′ ∩ OT, A := A′ ∩ 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}.

2.2 Functions in OT

Definition 2.10 (a) For a, b ∈ T′ we define a +_{OT} b, +_{OT} being a primitive recursive function. We will always omit the index OT. Let a = (a_{1}, …, a_{n}), b = (b_{1}, …, b_{m}), n, m ≥ 0. If m ≥ 1 and a_{i} ≺ b_{1} for all i = 1, …, n, then a + b := b. If m = 0 (therefore b = 0), a + b := a. Otherwise, there exists j ∈ {1, …, n} such that b_{1} ⪯ a_{j}, a_{i} ≺ b_{1} for all i ∈ {j + 1, …, m}. With this j we define a + b := (a_{1}, …, a_{j}, b_{1}, …, b_{m}).

(b) For a ∈ T′, n a natural number, we define a · n: a · 0 := 0, a · (n + 1) := (a · n) + a. (a, n) ↦ a · n is primitive recursive.

(c) For a, b ∈ T′ we define φ_{a}b. φ will be primitive recursively definable. If b ∈ Cr(a), then φ_{a}b := b. If b = 0 ∧ a ∈ G′, then φ_{a}b := a. Otherwise φ_{a}b := φ′_{a}b.

(d) For a ∈ T′ we define Ω_{a}, Ω will be primitive recursively definable. Ω_{0} := 0, if a ∈ Fi, then Ω_{a} := a, otherwise Ω_{a} := Ω′_{a}.

(e) Ω_{a}^{0} := a, Ω_{a}^{n+1} := Ω_{Ω_{a}^{n}}.

Definition 2.11 (a) We define a =_{NF} b + c, iff for some n, m ≥ 1 and c_{i}, d_{i} ∈ OT, b = (b_{1}, …, b_{n}), c = (c_{1}, …, c_{m}), a = (b_{1}, …, b_{n}, c_{1}, …, c_{m}) and a ∈ OT. a =′_{NF} b + c :⇔ a =_{NF} b + c ∧ c ∈ A.

(b) a =_{NF} φ_{b}c :⇔ a = φ′_{b}c ∧ a ∈ OT.

(c) a =_{NF} Ω_{b} :⇔ a = Ω′_{b} ∧ a ∈ OT.

(d) a =_{NF} ψ_{b}c :⇔ a = ψ_{b}c ∧ a ∈ OT.

Remark 2.12 (a) ∀x, y ∈ OT.∀n ∈ N.x + y, x · n, φ_{x}y, Ω_{x}, Ω_{x}^{n} ∈ OT.

(b) ∀x ∈ OT.∃y, z ∈ OT.x = 0 ∨ x = I ∨ x =′_{NF} y + z ∨ x =_{NF} φ_{y}z ∨ x =_{NF} Ω_{y} ∨ x =_{NF} ψ_{y}z.

(c) ∀x, y, z ∈ T′.(x =_{NF} y + z ∨ x =_{NF} φ_{y}z ∨ (x =_{NF} Ω_{y} ∧ y = z) ∨ x =_{NF} ψ_{y}z) → (length(y) < length(x) ∧ length(z) < length(x)).

(d) ∀x ∈ OT.∀y, z ∈ T′.(x =_{NF} y+z∨x =_{NF} φ_{y}z∨(x =_{NF} Ω_{y}∧y = z)∨x =_{NF} ψ_{y}z) → y, z ∈ OT.

(e) ∀x, y, y′ ∈ OT.(y ≺ y′ → x + y ≺ x + y′).

(f) ∀x, y, x′, y′ ∈ OT.φ_{x}y ≺ φ_{x′}y′ ↔ ((x ≺ x′ ∧ y ≺ φ_{x′}y) ∨ (x = x′ ∧ y ≺ y′) ∨ (x′ ≺ x ∧ φ_{x}y ⪯ y′)).

(g) ∀x, y ∈ OT.Ω_{x} ≺ Ω_{y} ↔ x ≺ y.

(h) ∀x, y.x ⪯ x + y ∧ y ⪯ x + y ∧ x ⪯ φ_{x}y ∧ y ⪯ φ_{x}y ∧ x ⪯ Ω_{x}.

Definition 2.13 (a) For κ ∈ R we define κ^{−}, the predecessor of a cardinal

by Ω′_{s+1}^{−} := Ω_{s}, I^{−} := 0.

(b) For a : N we define ã, a^{+}, a^{−Fi}, a^{+Fi}. (ã will be the largest cardinal below, a^{+} the least cardinal greater than a, a^{−Fi} the largest element of Fi′ below and, if a ≺ I, a^{+Fi} the least element of Fi′ greater than a). If a ∉ OT, ã, a^{−Fi}, a^{+}, a^{+Fi} are defined arbitrarily. ˜0 := 0^{−Fi} := 0, 0^{+} := Ω_{1}, 0^{+Fi} := ψ_{I}0. If a = (a_{0}, …, a_{n}), n > 0, then ã := ã_{0}, a^{+} := a_{0}^{+}, a^{−Fi} := a_{0}^{−Fi}, a^{+Fi} := a_{0}^{+Fi}. If a =_{NF} φ_{b}c, then with d := max{b, c} we define ã := d̃, a^{+} := d^{+}, a^{−Fi} := d^{−Fi}, a^{+Fi} := d^{+Fi}. If a =_{NF} ψ_{b}c, b ≠ I, then ã := b^{−}, a^{+} := b, a^{−Fi} := b^{−Fi}, a^{+Fi} := b^{+Fi}.

If a =_{NF} ψ_{I}c, ã := a^{−Fi} := a, a^{+} := Ω_{a+1}, a^{+Fi} := ψ_{I}(c + 1). If a =_{NF} Ω_{b}, ã := a, a^{−Fi} := b^{−Fi}, a^{+} := Ω_{b+1}, a^{+Fi} := b^{+Fi}. Ĩ := I, I^{+} := Ω_{I+1}, I^{−Fi} := I, I^{+Fi} := I.

(c) a^{−I} := \{ \begin{matrix}0 & if a ≺ I \\ I & otherwise \end{matrix}.

Remark 2.14 (a) ∀x, y ∈ OT.x̃, x^{+}, x^{−Fi}, x^{+Fi}, x^{−I}, x^{+I} ∈ OT.

(b) ∀x, y ∈ OT.x ⪯ y → (x̃ ⪯ ỹ∧ x^{+} ⪯ y^{+} ∧ x^{−Fi} ⪯ y^{−Fi} ∧ x^{+Fi} ⪯ y^{+Fi} ∧ x^{−I} ⪯ y^{−I} ∧ x^{+I} ⪯ y^{+I}).

(c) ∀x ∈ OT.∀y ∈ R.x ≺ y^{−} → G_{y}(x) ≅ ∅.

(d) ∀x ∈ R′.∀y ∈ T′.G_{x}(ỹ) ⊆ G_{x}(y) ∧ G_{x}(y^{−Fi}) ⊆ G_{x}(y) ∧ (y ∈ R′ → G_{x}(y^{−}) ⊆ G_{x}(y)).

(e) ∀x ∈ OT.x̃^{+} = x^{+}.

(f) ∀x ∈ OT.∃y ∈ OT.x̃ = Ω_{y} ∧ x^{+} = Ω_{y+1} ∧ x̃ ⪯ x ≺ x^{+}

(g) ∀x ∈ OT ∩ ψ_{I}0.x^{−Fi} = 0 ∧ x^{+Fi} = ψ_{I}0.

∀x ∈ OT.ψ_{I}0 ⪯ x ≺ I → ∃y ∈ OT.y ∈ C_{I}(y) ∧ x^{−Fi} = ψ_{I}y ∧ x^{+Fi} = ψ_{I}(y + 1) ∧ x^{−Fi} ⪯ x ≺ x^{+Fi}. ∀x ∈ OT.I ≺ x → x^{−Fi} = x^{+Fi} = I.

(h) ∀x ∈ OT.∀n, m ∈ N.n < m → Ω_{x+1}^{n} ≺ Ω_{x+1}^{m}.

(i) ∀x ∈ OT.∃n ∈ N.x ≺ Ω_{x^{−Fi}+1}^{n}.

(j) c ≺′ d → C̃_{b}(c) ⊆ C̃_{b}(d).

(k) a ∈ C̃_{b}(c) → a + 1 ∈ C̃_{b}(c), ψ_{a}b ∈ OT → ψ_{a}(b + 1) ∈ OT.

Remark 2.15 (a) 0, I ∈ C_{κ}(b).

(b) If b =_{NF} c + d or b =_{NF} φ_{c}d or b =_{NF} Ω_{c} ∧ c = d, then b ∈ C_{κ}(a) ⇔ c, d ∈ C_{κ}(a).

(c) If b ∈ OT ∧ b ≺ κ, then b ∈ C_{κ}(a) ⇔ b ≺ ψ_{κ}a.

(d) If b =_{NF} ψ_{π}d, then b ∈ C_{κ}(a) ⇔ (b ≺ ψ_{κ}a ∨ (π, d ∈ C_{κ}(a) ∧ d ≺ a)).

(e) If b =_{NF} ψ_{π}d, κ ≠ I, then b ∈ C_{κ}(a) ⇔ (b ⪯ κ^{−} ∨ (π, d ∈ C_{κ}(a) ∧ d ≺ a)).

3 The Type Theories ML_{[TD]}, ML_{J}

We are going to prove the lower bounds for two versions of type theory. Both are versions of intensional Martin-Löf’s type theory with W-type and a universe in the formulation à la Tarski. One is ML_{[TD]}, which is a slightly weakened version of the formulation by Troelstra and van Dalen in [TD88] and extends the version in Troelstra’s article [Tro87]. We have slightly changed the rules, in order to be as close as possible to the other version (see Remark 3.3 for details). The other version is ML_{J}, which is a formulation, where we have the elimination rules for the identity type using the constructor J. The rules for J can be found in [PSH90,NPS90]. We have chosen here a polymorphic version, since we have there less bureaucracy. However, there seems to be no problem to carry out the well-ordering proofs in monomorphic type theory as well. Although ML_{J} seems to be weaker than ML_{[TD]}, we do not know how to carry out an embedding and therefore, in order to obtain a lower bound for all versions, we will carry out the well-ordering proof in both ML_{J} and ML_{[TD],aux}, which will not cause almost any additional work. There has been a further change in the presentation of type theory, namely that one uses nowadays the logical framework. But since versions using the logical framework can be easily seen as extensions of ML_{J} and we are here interested in lower bounds, we will carry out the proof only in the weakest versions. However using abbreviations we are going to present the rules almost as if we had the logical framework available. We will write A type instead of A set, since we have in the absence of the logical framework no real types and we want to use the terminology set for subsets of the natural numbers. For technical reasons we introduce theories ML_{[TD],aux} and ML_{J,aux}, which are variants of ML_{[TD]} and ML_{J}. From every statement in ML_{[TD],aux} we get a statement in ML_{[TD]}, but in ML_{[TD],aux} we can more easily switch between the universe and the main level, similar for ML_{J,aux} and ML_{J}. We will afterwards work in ML_{[TD],aux} and ML_{J,aux}.

3.1 Definition of ML_{[TD]}, ML_{J} and ML_{[TD],aux}

Definition 3.1 (a) In the following “the four type theories” refers to ML_{[TD]}, ML_{J}, ML_{J,aux} and ML_{[TD],aux}. If not stated differently, every definition refers to all four type theories.

(b) The symbols are infinitely many variables z_{i} (i ∈ ω); the symbols ⇒, :, ,, (, ), =; the term constructors (with their arity in parenthesis) i_{k} (for each i < k, with arity 0), 0 (0), N̂_{k} (for each k ∈ ω, with arity 0), N̂ (0), S (1), λ (1), i (1), j (1), r (1), Ap (2), p (2), E (2), sup (2), R (2), Π̂ (2), Σ̂ (2), ˆ+ (2), Ŵ (2), P (3), D (3), Î (3), C_{k} (k ∈ ω, arity k + 1), the type constructors with their arity N_{k} (for each k ∈ ω, arity 0), N (0), U (0), T (1), Π (2), Σ (2), + (2), W (2) and I (3). Additionally ML_{J} and ML_{J,aux} have the term constructor J with arity 2 and ML_{[TD],aux} and ML_{J,aux} have the underlined type constructors \underline{N}_{k} (for each k ∈ ω, arity 0), \underline{N} (0), \underline{Π} (2), \underline{Σ} (2), \underline{+} (2), \underline{W} (2) and \underline{I} (3). N_{k}, N, Π, Σ, +, I, W are called the small type constructors, and for each of each such constructor C let \underline{C} is the corresponding underlined type constructor, and Ĉ is the corresponding term constructor with the “hat”.

(c) The b-objects of each of the four type theories are variables, (x_{1}, …, x_{n})b and C(b_{1}, …, b_{n}), if C is an n-ary term, type or (in case of ML_{[TD],aux}, ML_{J,aux}) underlined type constructor b, b_{1}, …, b_{n} are b-objects and x_{1}, …, x_{n} are variables. The set of free variables FV(b) of a b-object b are defined in the usual way. We write +, \underline{+} and ˆ+ infix (e.g. (a + b) for +(a, b)). 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}], which respects abstraction (y_{1}, …, y_{m}), in the usual way, using the convention, that if the same variable y occurs more than once, only the substitution x_{i} := b_{i} with i minimal such that x_{i} = y applies. “b[x_{1} := b_{1}, …, x_{n} := b_{n}] is an allowed substitution”, and α-equality (=_{α}) are defined in the usual way.

(d) The set of m-terms of the four type theories is inductively defined as: a variable x is an m-term; if i < k, i, k ∈ ℕ, then i_{k} is an m-term; and if k ∈ ℕ, then N̂_{k} is an m-term; if r, s, t are m-terms, x, y, z, x′ ∈ Var_{ML}, x ≠ y ≠ z ≠ x, then 0, S(r), P(r, s, (x, y)t), λ((x)r), Ap(r, s), p(r, s), E(r, (x, y)s), i(r), j(r), D(r, (x)s, (x′)t), r(r), sup(r, s), R(r, (x, y, z)s), N̂, Π̂(r, (x)s), Σ̂(r, (x)s), r ˆ+s, Î(r, s, t) and Ŵ(r, (x)s) 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. Additionally with the same r, s, x as before in ML_{J} and ML_{J,aux} J(r, (x)s) is an m-term. Abstracted m-terms are (x_{1}, …, x_{n})r for some m-term r and variables x_{1}, …, x_{n} (In the case n = 0, ()r := r).

(e) The m-types of the four type theories are N_{k} (k ∈ ω), (k ∈ ω), N, U; and if A, B are m-types, x ∈ Var_{ML}, r, s m-terms, then Π(A, (x)B), Σ(A, (x)B), A + B, I(A, r, s), W(A, (x)B), T(r) are m-types. Additionally, in ML_{[TD],aux} and ML_{J,aux}, with the same k, A, B, x, r, s we have that \underline{N}_{k}, \underline{N}, \underline{Π}(A, (x)B), \underline{Σ}(A, (x)B), A\underline{+}B, \underline{I}(A, r, s), \underline{W}(A, (x)B) are m-types. Abstracted m-types are (x_{1}, …, x_{n})A for some m-type A (again ()A := A).

(f) If r ≡ (x_{1}, …, x_{n})s is an abstracted m-term or m-type, r_{1}, …, r_{n}, n ≥ 1 are m-terms or m-types, then r(r_{1}, …, r_{n}) := s[x_{1} := r_{1}, …, x_{n} := r_{n}]. r is a suitable abstracted m-term means in the following, that if r(r_{1}, …, r_{n}) occurs, then r ≡ (x_{1}, …, x_{n})s for some x_{i} and s, and the substitution is allowed. Similarly we define for abstracted m-types A and m-terms r_{i}, A(r_{1}, …, r_{n}) and suitable abstracted 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-type. 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. The empty context (n = 0) will be denoted by ∅ and the concatenation of the context pieces Δ and Δ′ by Δ, Δ′. The m-judgements are the following: context, A type, A = B, s : A and s = t : A where A, B are m-types and s, t m-terms. A dependent m-judgement is an expression Γ ⇒ Θ where Γ is a mcontext, Θ an m-judgement. Two dependent m-judgements Γ ⇒ Θ and Γ ⇒ Θ′ are α-equivalent, if they differ only in the choice of bounded variables.

We write, if Θ is a judgement, Θ instead of ∅ ⇒ Θ, and, if Γ is a contextpiece, Γ context instead of Γ ⇒ context.

Definition 3.2 of the four type theories ML_{[TD]}, ML_{J} and ML_{[TD],aux} and ML_{J,aux}.

(a) We will define the rules, which are of the form

{Γ_{1} ⇒ Θ_{1} \atop …} ; Γ_{n} ⇒ Θ_{n} (Rule) Γ ⇒ Θ

where Γ_{1}, …, Γ_{n}, Γ are m-context-pieces, Θ_{1}, …, Θ_{n}, Θ are m-judgements (n = 0 is allowed) of the four type theories. Then we define for T ∈ {ML_{[TD]}, ML_{J}, ML_{[TD],aux}} T ⊢ Γ ⇒ Θ inductively by: If (Rule) is a rule of T as above, Δ is an m-context of T such that the following holds:

• Δ, Γ_{1}, …, Δ, Γ_{n}, Δ, Γ are m-contexts of T;

• T ⊢ Δ, Γ_{i} ⇒ Θ_{i} for i = 1, …, n;

• if n = 0 and Δ, Γ ≢ ∅, then T ⊢ Δ, Γ context. Then T ⊢ Δ, Γ ⇒ Θ. In (b) - (d) let A, B, C, D be in each rule suitable abstracted m-types, a, b, c, r, s, t suitable abstracted m-terms, Θ be an m-judgement, Γ be an m-context-piece of the currently treated type theory, all possibly with indices or accents ′. Further let x, y, z, u be variables. If for some abstracted m-term or m-type A we have an occurrence of A(x_{1}, …, x_{n}), in the first such occurrence as a premise of a rule assume x_{i} ∉ FV(A) (i = 1, …, n). Further assume that all substitutions are allowed. A → B abbreviates Π(A, (x)B) for a new variable x.

(b) The rules of ML_{J} are as follows:

General Rules

A type ; (Cont) ; x : A context

x : A, Γ context

(Ass)

x : A, Γ ⇒ x : A

x : B not a context-piece in Γ

\begin{aligned}& r : A \\ (Ref_{1}) \\ & r = r : A \end{aligned}  \begin{aligned}& A type \\ (Ref_{2}) \\ & A = A \end{aligned}

\begin{aligned}& r = s : A \\ (Sym_{1}) \\ & s = r : A \end{aligned}  \begin{aligned}& A = B \\ (Sym_{2}) \\ & B = A \end{aligned}

{r = s : A \atop s = t : A} ; (Trans_{1}) ; r = t : A  \begin{matrix}A = B \\ B = C \end{matrix} ; (Trans_{2}) ; A = C

\begin{matrix}r : A \\ A = B \end{matrix} ; (Repl_{1}) ; r : B  {r = s : A \atop A = B} ; (Repl_{2}) ; r = s : B

{x : A, Γ ⇒ Θ \atop ⇒ t : A} ; (Sub_{1}) ; Γ[x := t] ⇒ Θ[x := t] {x : A, Γ ⇒ B(x) type \atop t = t′ : A} (Sub_{2}) Γ[x := t] ⇒

B(t) = B(t′)

{x : A, Γ ⇒ s(x) : B(x) type \atop t = t′ : A} (Sub_{3}) Γ[x := t] ⇒ s(t) = s(t′) : B(t)

Γ ⇒ Θ ; (Alpha) ; Γ′ ⇒ Θ′ Where Γ ⇒ Θ and Γ′ ⇒ Θ′, are α-equivalent

Type Introduction Rules

{(N_{k}^{T}) N_{k} type \atop (k ∈ ℕ)}  (N^{T}) N type
A type
x : A ⇒ B(x) type

(Π^{T})

Π(A, B) type

A type

x : A ⇒ B(x) type (Σ^{T}) Σ(A, B)

A type ; B type ; (+^{T}) ; A + B type

{A type \atop r : A} ; s : A

(I^{T})

I(A, r, s) type
A type

x : A ⇒ B(x) type (W^{T}) W(A, B)

Introduction Rules

{(N_{k}^{I}) i_{k} : N_{k} \atop (i < k, i, k ∈ ℕ)}  (N_{0}^{I}) 0 : N

\begin{aligned}& r : N \\ (N_{0}^{I}) \\ & S(r) : N \end{aligned}  \begin{aligned}& x : A ⇒ t(x) : B(x) \\ (Π^{I}) \\ & λ(t) : Π(A, B) \end{aligned}

{x : A ⇒ B(x) type \atop r : A} ; s : B(r) (Σ^{I}) p(r, s) : Σ(A, B)

\begin{matrix}r : A \\ B type \end{matrix} ; (+_{1}^{I}) ; i(r) : A+B

{A type \atop r : B} ; (+_{2}^{I}) ; j(r) : A+B  \begin{aligned}& s : A \\ (I^{I}) \\ & r(s) : I(A, s, s) \end{aligned}

{x : A ⇒ B(x) type \atop r : A} ; s : B(r) → W(A, B) (W^{I}) sup(r, s) : W(A, B)

Elimination Rules

{z : N_{k} ⇒ D(z) type \atop r : N_{k}} ; s_{i} : D(i_{k}) (i = 0 … k − 1) (N_{k}^{E}) C_{k}(r, s_{0}, …, s_{k−1}) : D(r)

(k ∈ ℕ)

{x : A ⇒ B(x) type \atop s : Π(A, B)} ; r : A (Π^{E}) Ap(s, r) : B(r)

\begin{matrix}r : N \\ z : N ⇒ C(z) type \end{matrix} ; s : C(0) ; x : N, y : C(x) ⇒

t(x, y) : C(S(x)) (N^{E}) P(r, s, t) : C(r)

{x : A ⇒ B(x) type \atop r : Σ(A, B)}

z : Σ(A, B) ⇒ C(z) type x : A, y : B(x) ⇒

t(x, y) : C(p(x, y)) (Σ^{E}) E(r, t) : C(r)

\begin{matrix}z : A+B ⇒ C(z) type \\ r : A + B \end{matrix} ; x : A ⇒ s(x) : C(i(x)) ; y : B ⇒ t(y) : C(j(y)) (+^{E}) D(r, s, t) : C(r) \begin{matrix}s : A \\ s′ : A \end{matrix} ; r : I(A, s, s′) ; x : A, y : A, z : I(A, x, y) ⇒ ; C(x, y, z) type ; x : A ⇒ t(x) : C(x, x, r(x)) (I^{E})^{∗} J(r, t) : C(s, s′, r)

{x : A ⇒ B(x) type \atop r : W(A, B)}

u : W(A, B) ⇒ C(u) type

x : A, y : B(x) → W(A, B), z : Π(B(x), (v)C(Ap(y, v)))

⇒ t(x, y, z) : C(sup(x, y)) (W^{E}) R(r, t) : C(r)

(v ∉ FV(C))

Equality Rules

\begin{matrix}z : N_{k} ⇒ D(z) type \\ s_{i} : D(i_{k})(i = 0, …, k − 1) \end{matrix} ; (N_{k}^{=}) ; C_{k}(i_{k}, s_{0}, …, s_{k−1}) = s_{i} : D(i_{k}) ; (i < k, i, k ∈ ℕ)

{z : N ⇒ C(z) type \atop s : C(0)} ; x : N, y : C(x) ⇒ t(x, y) : C(S(x)) (N_{0}^{=}) P(0, s, t) = s : C(0)

\begin{matrix}r : N \\ z : N ⇒ C(z) type \end{matrix} ; s : C(0)

x : N, y : C(x) ⇒ t(x, y) : C(S(x)) (N_{S}^{=})

P(S(r), s, t) = t(r, P(r, s, t)) : C(S(r))

{x : A ⇒ t(x) : B(x) \atop r : A} (Π^{=}) Ap(λ(t), r) = t(r) : B(r)

{x : A ⇒ B(x) type \atop r : A} ; s : B(r)

z : Σ(A, B) ⇒ C(z) type

x : A, y : B(x) ⇒ t(x, y) : C(p(x, y)) (Σ^{=}) E(p(r, s), t) = t(r, s) : C(p(r, s))

\begin{matrix}r : A \\ z : A+B ⇒ C(z) type \end{matrix} ; x : A ⇒ s(x) : C(i(x)) ; y : B ⇒ t(y) : C(j(y)) (+_{1}^{=}) D(i(r), s, t) = s(r) : C(i(r)) \begin{matrix}r : B \\ z : A+B ⇒ C type \end{matrix} ; x : A ⇒ s(x) : C(i(x)) ; y : B ⇒ t(y) : C(j(y)) (+_{2}^{=}) D(j(r), s, t) = t(r) : C(j(r))

\begin{matrix}s : A \\ x : A, y : A, z : I(A, x, y) ⇒ C(x, y, z) type \end{matrix} ; x : A ⇒ t(x) : C(x, x, r(x)) (I^{=})^{∗} J(r(s), t) = t(s) : C(s, s, r(s))

{x : A ⇒ B(x) type \atop r : A} ; s : B(r) → W(A, B)

u : W(A, B) ⇒ C(u) type

x : A, y : B(x) → W (A, B),
z : Π(B(x), (v)C(Ap(y, v))) ⇒ t(x, y, z) : C(sup(x, y))

(W^{=})

R(sup(r, s), t) = t(r, s, λ((v′)R(Ap(s, v′), t)))

: C(sup(r, s))
(if v ∉ FV(C), v′ ∉ FV(s) ∪ FV(t))

Rules for the Universe Type Introduction Rules for the Universe

(U^{I}) U type  a : U ; (T^{I}) ; T(a) type

Introduction Rules for the Universe

{(N̂_{k}^{I}) N̂_{k} : U \atop k ∈ ω}  (N̂^{I}) N̂ : U
\begin{matrix}a : U \\ x : T(a) ⇒ b(x) : U \end{matrix} ; (Π̂^{I}) ; Π̂(a, b) : U  \begin{matrix}a : U \\ x : T(a) ⇒ b(x) : U \end{matrix} ; (Σ̂^{I}) ; Σ̂(a, b) : U
\begin{matrix}a : U \\ b : U \end{matrix} ; ( ˆ+^{I}) ; a ˆ+b : U  \begin{matrix}a : U \\ r : T(a) \end{matrix} ; s : T(b) ; (Î^{I}) ; Î(a, r, s) : U

\begin{matrix}a : U \\ x : T(a) ⇒ b(x) : U \end{matrix} (Ŵ^{I}) Ŵ(a, b) : U

Equality Rules for the Universe

{(N̂_{k}^{=}) T(N̂_{k}) = N_{k} \atop (k ∈ ω )}  (N̂^{=}) T(N̂) = N

\begin{matrix}a : U \\ x : T(a) ⇒ b(x) : U \end{matrix}

(Π̂^{=})

T(Π̂(a, b)) = Π(T(a), (x)T(b(x)))

\begin{matrix}a : U \\ x : T(a) ⇒ b(x) : U \end{matrix}

(Σ̂^{=})

T(Σ̂(a, b)) = Σ(T(a), (x)T(b(x)))

\begin{matrix}a : U \\ b : U \end{matrix} ; ( ˆ+^{=}) ; T(a ˆ+b) = T(a) + T(b)

\begin{matrix}a : U \\ r : T(a) \end{matrix} ; s : T(b) (Î^{=}) T(Î(a, r, s)) = I(T(a), r, s)

\begin{matrix}a : U \\ x : T(a) ⇒ b(x) : U \end{matrix}

(Ŵ^{I})

T(Ŵ(a, b)) = W(T(a), (x)T(b(x)))

(c) The Rules for ML_{[TD]} are the same as for ML_{J} (but referring to m-terms, -types etc. of ML_{[TD]} instead of ML_{J}) but with the elimination- and equality rules for the identity type (I^{E}) and (I^{=}) (denoted by ∗) replaced by the following rule:

\begin{matrix}s : A \\ s′ : A \end{matrix} ; r : I(A, s, s′) (I^{E}) s = s′ : A

(d) The Rules for ML_{[TD],aux} (ML_{J,aux}) are the same rules as for ML_{[TD]} (ML_{J}). Additionally we have the following rules for the underlined constructors:

A type
x : A ⇒ B(x) type

(\underline{Π}^{T})

\underline{Π}(A, B) type

A type

x : A ⇒ B(x) type (\underline{Π}^{=}) \underline{Π}(A, B) = Π(A, B)

Similarly for N, N_{k}, Σ, +, I, W.

Remark 3.3 on the versions considered.

(a) Apart from modifications of names, we have changed ML_{[TD]} in the following sense relative to the formulation in [TD88], in order to be as close to “ML_{J}” (which slightly weakens the system, but this is no harm since we treating lower bounds only):

• We have omitted the rule, which derives r : A from r = r : A.

• We have replaced the thinning rule by the context rule.

• In [TD88] the elimination rule for Π has assumption λ(t) : Π(A, B) instead of x : A ⇒ t(x) : B(x), similarly for Σ. Our version is obviously slightly weaker.

• We have replaced the elimination rules for the Σ-type using projections by the elimination rules found e.g. in [ML84]. By defining E(r, s) := s(p_{0}(r), p_{1}(r)), our rules can be derived from the original rules. In the opposite direction we can define as well p_{0}, p_{1} using E by p_{0}(r) := E(r, (x, y)x) and p_{1}(r) := E(r, (x, y)y), however we do not get the ηrule, therefore our rules are slightly weaker.

• We have omitted the equality rule for the identity type. Further we have changed the constructor for the introduction rule to r(a) instead of r in order to be as close as possible to the other system (and we weaken the system microscopically).

• We have added the rule (Repl_{2}) for systematic reasons, which seems to be missing. However we will not use that rule. Note that the essential difference between ML_{[TD]} and ML_{J} are the elimination rules for the identity type.

(b) We have not added to ML_{J} the equality versions of type introduction, introduction and elimination rules (e.g. that from x : A ⇒ t = t : B(x) we can derive λ(t) = λ(t′) : Π(A, B)) as it can be found in [PSH90]. Our systems suffices, and is weaker than the system in [PSH90], since the substitution rules are provable there (see [PSH90], Theorem 4.2 for (Sub_{1}), for (Sub_{2}) and (Sub_{3}) this follows similarly) and we are interested in lower bounds only.

(c) One could have replaced N_{k} by \underbrace{N_{1} + ⋯ N_{1}}_{ktimes} for k ≥ 2, further N_{1} by

I(N, 0, 0), therefore only N_{0} is needed. We do not use N_{k} for k > 2.

3.2 Abbreviations

Definition 3.4 Let in this definition T be one of the four type theories. We introduce several abbreviations and conventions, to work more easily in T.

(a) We assume, that all free variables are chosen differently from bounded variables, and bounded variables are chosen in such a way that there are no variable clashes, identifying α-equivalent m-terms and m-types.

(b) We will write Γ ⇒ r : A for T ⊢ Γ ⇒ r : A, where T is the type theory we are working in. Further Γ ⇒ r, s : A for T ⊢ Γ ⇒ r : A ∧ T ⊢ Γ ⇒ s : A, etc. We say “Γ ⇒ A” for “T ⊢ Γ ⇒ t : A for some m-term”.

(c) By “assume Γ ⇒ A type, then (∗)” we mean: For every context Δ such that T ⊢ Δ, Γ ⇒ A type (∗) relative to the context Δ follows. (Usually A is in this situation a meta-variable for an m-type).

(d) We write (λx.t) for λ((x)t), if S ∈ \{Σ, Π, W, \underline{Σ}, \underline{Π}, \underline{W}, Σ̂, Π̂, Ŵ\}, Sx : A.B for S(A, (x)B), and (rs) for Ap(r, s). The usual conventions about omitting brackets apply. Especially the scope of λx. is as long as possible, for instance λx.s t should be read as λx.(s t). We will write λx, y.t for λx.λy.t, ∀x, y : A.B for ∀x : A.∀y : A.B, similarly for ∃, Π, Σ and for more than two variables.

(e) The projections r0, r1 are defined by r0 := E(r, (x, y)x), r1 := E(r, (x, y)y). Further (r =_{A} s) := I(A, r, s).

(f) We use ∀ and Π, ∃ and Σ as the same symbol, similarly for ˆ∀, \underline{∀} etc.

(g) ⊥ := N_{0}, A∨B := A+B, A×B := A∧B := Σx : A.B for a new variable x, A ↔ B := (A → B) ∧ (B → A), (remember A → B := Πx : A.B for a new variable x) ¬A := A → ⊥, (r ≠_{A} s) := ¬(r =_{A} s). ∧, ∨, ∀, ∃ are used for types considered as propositions, whereas ×, +, Π, Σ are used for types as functions and sets in the sense of Martin-Löf.

(h) We define ∀x rel s.A := ∀x : C.x rel s → A and ∃x rel s.A := ∃x : C.x rel s ∧ A, in any situation where we have x : B ⇒ x rel s type, and can read the type B from rel . ( rel will be either a binary relation between elements of a type, e.g. <_{N},and s a term of type B, or rel will be the ∈-relation defined between terms for natural numbers and types as defined later). If x ∈ FV(s), then we first have to change to an α-equivalent form, considering ∀x rel s.A =_{α} ∀y rel s.A[x := y], if y ∉ FV(A) and substitutable for x, similar for ∃.

(i) In this and the next chapter we assume that A, B, C are m-types, a, b, c, r, s, t m-terms, Γ, Δ m-context-pieces, Θ an m-judgement, u, v, w, x, y, z variables, all possibly with indices or accents (′). Elements of OT are usually denoted by a, b, c.

3.3 Working with the Universe

Remark 3.5 We can derive in ML_{J,aux} and ML_{[TD],aux} from the rules (C^{T}), (C^{I}), (C^{E}), (C^{=}) for a type constructor C ≠ U, T new rules by replacing some of the explicit occurrences of C by \underline{C}. This is possible since from the assumption and the new type-introduction-rules we can derive C(t_{1}, …, t_{n}) = \underline{C}(t_{1}, …, t_{n}) (e.g. in the (Π) rules we always get Π(A, B) = \underline{Π}(A, B)). The only exception are the types B(t) → W(A, B) and B → W(A, B) in the rules (W^{I}), (W^{E}) and (W^{=}) in the case of ML_{[TD],aux}: We do not have B → W(A, B) = B \underline{→} \underline{W}(A, B), therefore \underline{W} cannot be replaced by W.

So, when we reason informally, we have only to be careful with the use of underlining in the case of the W-type, and here only for the cases mentioned. (Note that in the presence of the equality versions of the type introduction rules this problem does not occur).

Definition 3.6 (a) We define ψ(C) for all term, type and underlined type constructors C of the four type theories: If C is a small type constructor, ψ(\underline{C}) := C. For all other constructors C we define ψ(C) := C.

(b) For a b-object ψ(b) is the result of applying ψ to each symbol. The same applies for m-context-pieces, -contexts, -judgements.

(c) We define γ(C) and \underline{γ}(C) for some type constructors C: If C is a small type constructor, γ(\underline{C}) := Ĉ. For all other type constructors C γ(C) is undefined.

(d) If A is an abstracted m-type, then \underline{A} is the result of underlining all small type constructors in A.

(e) Definition of γ(A) for some abstracted m-types A. (For all other m-types, the value of γ(A) will be a symbol for undefined). We will write γ(A) ↓ for “γ(A) is defined”, and s ≃ t for (s ↓↔ t ↓) ∧ (s ↓→ s = t), where a more complex term is defined, if the process of successively evaluating it always leads to defined terms. γ(T(t)) := t. For underlined type constructors \underline{C} and abstracted m-terms or -types D_{i}, γ(\underline{C}(D_{1}, …, t_{n})) :≃ γ(\underline{C})(γ(D_{1}), …, γ(D_{n})), where γ(t) := t for m-terms t and γ((x_{1}, …, x_{n})D) :≃ (x_{1}, …, x_{n})γ(D). For all other type constructors (especially U) γ(C(t_{q}, …, t_{n})) is undefined.

(f) We define ϕ(A) for m-types A. If γ(A) is defined, ϕ(A) := T(γ(A)). If this instance does not apply, we define ϕ(C(D_{1}, …, D_{n})) := C(ϕ(D_{1}), …, ϕ(D_{n})), where C is a constructor and D_{i} are abstracted m-terms or types. Here ϕ(t) := t,for m-terms t and ϕ((x_{1}, …, x_{n})A) := (x_{1}, …, x_{n})ϕ(A).

(g) ϕ(B) is defined for m-judgements, -contexts etc. by applying ϕ to all the types occurring there.

Lemma 3.7 Assume A[x := t], B[x := t] are allowed substitutions, where A, B are m-terms or m-types and t an m-term.

(a) γ(A) ↓⇔ γ(A[x := t]) ↓

(b) If γ(B) is defined, then γ(B)[x := t] is allowed, γ(B)[x := t] = γ(B[x := t]).

(c) ϕ(B)[x := t] and ψ(B)[x := t] are allowed, ϕ(B)[x := t] = ϕ(B[x := t]), ψ(B)[x := t] = ψ(B[x := t]).

Lemma 3.8 Let T = ML_{[TD]} and T_{aux} = ML_{[TD],aux} or T = ML_{J} and T_{aux} = ML_{J,aux}

(a) If T_{aux} ⊢ Γ ⇒ Θ, then T ⊢ ψ(Γ) ⇒ ψ(Θ).

(b) If T_{aux} ⊢ Γ ⇒ Θ, then T_{aux} ⊢ ϕ(Γ) ⇒ ϕ(Θ).

(c) If T_{aux} ⊢ Γ ⇒ Θ, where Θ ∈ {A type, s : A, s = t : A, A = B, B = A} or T_{aux} ⊢ Γ, x : A, Δ ⇒ Θ′, and if further γ(A) ↓, then T_{aux} ⊢ ϕ(Γ) ⇒ γ(A) : U.

Proof: (a) and simultaneously (b) and (c) follow by an easy induction on the derivation. ⊓ ⊔

Definition 3.9 We say “Γ ⇒ A type is correctly defined from Γ_{i} ⇒ Θ_{i} (i = 1, …, n)”, iff the following holds for all contexts Δ:

• Δ, Γ_{i} ⇒ Θ_{i} for all i implies Δ, Γ ⇒ A type.

• If for all i ∈ {1, …, n} such that Θ_{i} ≡ (B type) for some B we have γ(B) ↓, ϕ(Γ_{i}) ⇒ γ(B) : U, and for all other i we have Δ, ϕ(Γ_{i}) ⇒ ϕ(Θ_{i}) then Δ, ϕ(Γ) ⇒ γ(\underline{A}) : U.

We write “A is a type correctly defined from …” for “A type is correctly defined from …”.

From now on we are working in ML_{J,aux} and ML_{[TD],aux}. Let ML be one of these two theories.

3.4 The Basic Types and Sets in ML

Definition and Remark 3.10 (a) Let 𝔹 := N_{2}. Obviously γ(\underline{𝔹}) ↓.

(b) Let ff := 0_{2}, tt := 1_{2}. Obviously tt, ff : 𝔹.

(c) \underline{if} r \underline{then} s \underline{else} t := C_{2}(r, s, t). Obviously x : 𝔹, y : A, z : A ⇒\underline{if} x \underline{then} y \underline{else} z : A.

(d) atom(t) := T(\underline{if} t \underline{then} N̂_{0} \underline{else} N̂_{1}). atom(t) is obviously a type correctly defined from t : 𝔹.

(e) r ∧_{𝔹} s :=\underline{if} r \underline{then} s \underline{else} ff, r ∨_{𝔹} s :=\underline{if} r \underline{then} tt \underline{else} s, ¬_{𝔹} 1r :=\underline{if} r \underline{then} ff \underline{else} tt. r ∧_{𝔹} s, r ∨_{𝔹} s, ¬_{𝔹} 1r : 𝔹. Obviously atom(r ∧_{𝔹} s) ↔ atom(r) ∧ atom(s) etc.

(f) We assume the usual ordering of the natural numbers defined, i.e. there are m-terms <_{N,𝔹}, ≤_{N,𝔹} of type N → (N → 𝔹), written infix (i.e. r <_{N,𝔹} s for <_{N,𝔹} rs), we define r <_{N} s := atom(r <_{N,𝔹} s), r ≤_{N} s := atom(r ≤_{N,𝔹} s), and assume that the usual properties of <_{N}, ≤_{N} can be proved in ML.

In the following we will define classes of natural numbers, the subsets of the natural numbers and decidable subsets of the natural numbers. Classes are properties on the natural numbers. If this property is small, i.e. can be seen as an element of the universe, than the class will be an element of the power set of the natural numbers. The decidable subsets are those for which we can decide by having a function N → 𝔹, whether an element belongs to the set. The distinction between classes and sets is similar to this distinction in subsystems of analysis and set theory.

Definition and Remark 3.11 (a) Γ ⇒ (x)A : Cl(N) :⇔ Γ, x : N ⇒ A type. We will identify (x)A and (y)A[x := y], if y ∉ FV(A) and substitutable.

(b) In the following, if we say Γ ⇒ A : Cl(N), A stands for (x)B for some variable x and some m-type B. We say “A is a class” for A : Cl(N). Note, that “A is a class, correctly defined from …” stands for “A ≡ (x)B for some m-type B and x : N ⇒ B type is correctly defined from …”.

(c) (t ∈ (x)A) := A[x := t]. This is a type correctly defined from A : Cl(N) and t : N.

(d) P(N) := N → U, the power-set of the natural numbers.

(e) t^{Cl} := (y)T(ty). t^{Cl} is a class, correctly defined from t : P(N). If it is clear, that t is an element of P(N), we omit the superscript Cl, writing s ∈ t for s ∈ t^{Cl}, which is an abbreviation for T(ts).

(f) P^{dec}(N) := N → 𝔹, the decidable subsets of the natural numbers.

(g) a ∈_{dec} b := ba. We have x : N, y : P^{dec}(N) ⇒ x ∈_{dec} y : 𝔹.

(h) t^{dec,Cl} := (y)atom(y ∈_{dec} t). t^{dec,Cl} is obviously a class, correctly defined from t : P^{dec}(N). If it is clear, that t is an element of P^{dec}(N), we will omit again the superscript dec, Cl (so s ∈ t stands for atom(ts)).

(i) t ∉ A := ¬(t ∈ A), a type correctly defined from t : N and A : Cl(N).

(j) A ⊆ B := ∀x ∈ A.x ∈ B for some new variable x, A ≅ B := A ⊆ B ∧ B ⊆ A, both are types correctly defined from A, B : Cl(N). Obviously we have that ≅ is an equivalence relation, ⊆ a partial ordering.

(k) (x)A ∪ (x)B := (x)(A ∨ B), (x)A ∩ (x)B := (x)(A ∧ B) (note that we identify α-equivalent objects in Cl(N)) Obviously, both are classes correctly defined from A, B : Cl(N).

(l) ∅ := (x)⊥, a correctly defined class.

(m) {a_{1}, …, a_{n}} := (x)(x =_{N} a_{1} ∨ ⋯ ∨ x =_{N} a_{n}), a class correctly defined from a_{i} : N.

(n) To ease the intuition {x | A} := (x)A, which we will use if we are talking about an element of Cl(N), P(N), P^{dec}(N). {x ∈ A | B} := {x | x ∈ A ∧ B}.

(o) If A is an m-term or m-type, which possibly depends on x, then ⋃_{x:B} A := {y | ∃x : B.ϕ(x) ∧ y ∈ A}, ⋃_{x:B.ϕ(x)} A := {y | ∃x : B.ϕ(x) ∧ y ∈ A}, ⋃_{x∈B} A := {y | ∃x ∈ B.y ∈ A}, ⋃_{x∈B.ϕ(x)} A := {y | ∃x ∈ B.ϕ(x) ∧ y ∈ A}. If t is a term ≢ x, then {t | x ∈ A} := {y | ∃x ∈ A.y = t}, {t | x : A} := {y | ∃x : A.y = t}.

Remark 3.12 (a) If Γ ⇒ B : Cl(N), B ≡ (x)A, then γ(B) ↓↔ γ(A) ↓, and

if γ(B) ↓, then γ(A) = (x)γ(B), and we have ϕ(Γ) ⇒ λ(γ(A)) : P(N).

(b) If A, A′, B, B′ : Cl(N), A ≅ A′, B ≅ B′, then A ∪ B ≅ A′ ∪ B′, A ∩ B ≅ A′ ∩ B′

Definition 3.13 By “R′ is a decidable n-ary relation” we mean that there is an n-ary function R′_{dec} : N^{n} → 𝔹, written as R′_{dec}(t_{1}, …, t_{n}), and that in the following R′(t_{1}, …, t_{n}) := atom(R′_{dec}(t_{1}, …, t_{n})). Sometimes, if n = 2, R′ and R′_{dec} will be written infix.

3.5 Using the W-type

The following is a preparation for the definition of W(A) in Sect. 5.

Definition 3.14 (a) index := λy′.R(y′, (x, y, z)x).

(b) pred := λy′.R(y′, (x, y, z)λu.yu).

(c) s ≺_{W(A,B)}^{1} t := ∃u : B(index(t)).s =_{W(A,B)} pred(t)u. (s is an immediate subtree of t).

(d) s ≺_{W(A,B)} t := ∃f : (N → W(A, B)).∃n : N.0 <_{N} n ∧ (f0) =_{W(A,B)} s ∧ (fn) =_{W(A,B)} t ∧ ∀i : N.i <_{N} n → (fi) ≺_{W(A,B)}^{1} f(S(i)). (s is a subtree of t).

(e) s ⪯_{W(A,B)} t := (s ≺_{W(A,B)} t) ∨ (s =_{W(A,B)} t).

(f) We will in the following omit the index W(A, B), if there is no confusion.

Remark 3.15 Assume x : A ⇒ B(x) type

(a) u : W(A, B) ⇒ index(u) : A, x : A, y : (B(x) → W(A, B)) ⇒ index(sup(x, y)) = x : A.

(b) v : W(A, B) ⇒ pred(v) : (B(index(v)) → S(A, B)), and x : A, y : (B(x) → W(A, B)) ⇒ pred(sup(x, y)) = λu.yu : (B(x) → S(A, B)), where S can be W and \underline{W}.

(c) We have s ≺_{W(A,B)}^{1} t, s ≺_{W(A,B)} t and s ⪯_{W(A,B)} t are types correctly defined from A type, x : A ⇒ B(x) type and s, t : W(A, B) (where x ∉ FV(B)).

Lemma 3.16 Assume x : A ⇒ B(x) type.

(a) ∀x, y : W(A, B).x ⪯ y ↔ (x ≺ y ∨ x = y).

(b) ∀x, y, z : W(A, B).(x ≺ y ∧ y ≺ z) → x ≺ z.

(c) ∀x, y : W(A, B).x ≺^{1} y → x ≺ y.

(d) ∀u : W(A, B).∀x : A.∀y : (B(x) → W(A, B)).(u ≺^{1} sup(x, y)) ↔ (∃v : B(x).u =_{W(A,B)} yu).

(e) ∀u : W(A, B).∀x : A.∀y : (B(x) → W(A, B)).u ≺ sup(x, y) ↔ ∃v : B(x).u ⪯ (yv).

(f) ∀x : W(A, B).¬x ≺ x.

Proof: (a) –(c) are immediate. (d) follows by using the substitution rules and x : A, y : (B(x) → W(A, B)), u : B(x) ⇒ pred(sup(x, y))u = yu : W(A, B).

(e) follows from (d). (f): Induction on u : W(A, B): Assume x : A, y : (B(x) → W(A, B)), p : (∀u : B(x).¬yu ≺ yu). Assume sup(x, y) ≺ sup(x, y). Then sup(x, y) ⪯ (yv) for some v : B(x), yv ≺^{1} sup(x, y), therefore (yv) ≺ (yv), and using p we get ⊥, and therefore the assertion. ⊓ ⊔

4 The Well-ordering Proofs

4.1 Overview

The usual method for establishing well ordering proofs in strong theories is the method of distinguished sets (in German “ausgezeichnete Mengen”) developed mainly by Buchholz and Schütte. The first publication can be found in [Buc75], and this paper – unfortunately it is in German – might serve as an excellent introduction for the reader, who does not know this area well. Jäger used the methods in [Jäg83] to determine the proof theoretical strength of Feferman’s theory T_{0} and therefore applied it to a system for constructive mathematics. The methods were refined in the book by Buchholz and Schütte ([BS88]) and a draft on recent research can be found in [Buc90]. This last article was the major basis for our well-ordering proof. We have modified it in order to avoid fundamental sequences.

In [Set97a] we have tried to give motivation and an introduction to wellordering proofs in type theory (restricted to systems without a universe).

Originally the methods for carrying out well-ordering proofs were developed for the use in subsystems of analysis and in set theory. In our proof we are just going to adapt these techniques to the type theoretic setting. The best way to get an understanding of what is going on seems to be to study it first in the set theoretic setting, and then to look at the way this proof can be carried out in type theory. Therefore, in this section, we are trying to refer as little as possible to the type theory. We will characterize the constructions we are giving and will present the type theoretic definitions themselves in Sect. 5. In the current section we work almost as we would work in traditional theories as well.

We start in the well ordering proofs with a set A which we want to extend to a bigger set W(A) (Assumption 4.10, the actual definition of W(A) will be carried out in Lemma 5.6 (d)). In order to do this, we define first a set or class M(A) (Definition 4.5 (c)), which is a set of ordinal terms, which are potential elements of W(A), and the set or class τ^{A}(a) of predecessors of a relative to A, (Definition 4.5 (a)). Now in pure set theory we would define W(A) = ⋂{Y ⊆ ℕ | ∀x ∈ M(A).τ^{A}(x) ⊆ Y → x ∈ Y }. In our setting we characterize W(A) as a set (or class), such that for all b ∈ M(A), from τ^{A}(b) ⊆ W(A) follows b ∈ W(A), and further, W(A) is the least set with this property, i.e. for any class C, if for all b ∈ M(A), τ^{A}(b) ⊆ C implies b ∈ C, then W(A) ⊆ C.

If we look at W(A) between Ω_{a} and Ω_{a+1}, then (at least as long as the weak condition W ⊆ M(A) is fulfilled) W(A) is the well-founded part of the set of ordinals the atoms of which below Ω_{a} are in A. Gaps in the set A below Ω_{a} will create gaps in W(A). (For instance if there is a gap between b and Ω_{a}, then there is a gap in W(A) between Ω_{a} · e + b and Ω_{a} · (e + 1) for e ≺ Ω_{a+1}.)

A set A will be called distinguished (Definition 4.18), if A is a segment of W(A). In a classical theory, this would mean that A = W(A) ∩ b for some b, but in an intuitionistic theory we cannot determine in general such a b. If A is a distinguished set and Ω_{a+1} ⪯ A, then A ∩ {x ∈ OT|Ω_{a} ⪯ x ≺ Ω_{a+1}} is the well-founded part of the ordinal terms the components below Ω_{a} are in A itself (so the atoms themselves are again in the well-founded part of similar kind). Very roughly we could say that A is some kind of fixed point of W(A) (in fact in general W(A) is bigger, but all ordinal terms in W(A)\A are bigger than the ordinal terms in A) or A is well-founded with support in itself.

Using the definition of distinguished sets, we get another understanding of W(A): If A is distinguished, A ≅ W(A) ∩ κ (A is the distinguished part up to κ), then W(A) ∩ κ^{+} is distinguished (the distinguished part up to κ^{+}). So W(A) is some kind of jump operator, which gives the step to the next cardinal.

We conclude the principle of induction over distinguished sets (Lemma 4.21 (a)), and that the ordinal terms in the countable part of distinguished sets form a segment (Lemma 4.21 (b)), which is well-ordered in the usual sense (Lemma 4.21 (c)).

In order to prove transfinite induction up to some big ordinal notation (in the countable part), we therefore need just to find a distinguished set, which contains this ordinal notation. Since distinguished sets are closed under the collapsing function ψ, in order to get a distinguished set which contains ψ_{Ω_{1}}Ω_{I+n}, it suffices to define such a set which contains Ω_{I+n}. With sets this is not possible, but we can introduce distinguished classes as well (note that we have only restricted comprehension schemes available). If we take the union over all distinguished sets, which is a class, we get a distinguished class W (Definition 4.25) with the property W ∩ I ≅ W(W) ∩ I (Lemma 4.38 (c)). We can define now distinguished classes (Definition 4.39) which contain Ω_{I+n} and are done (Theorem 4.41).

Assumption 4.1 In this section we will not care about underlining constructors. Essentially we can underline any parts of the formula except for the classes it is built from (denoted by A, B, C) as long as we underline everything in an abbreviation consistently (e.g. in M(A), W(A) or A ≅ B as defined below, either all constructors apart from those positioned in A and B are underlined or none). When introducing a new element A of the universe by writing A : P(N) we will be a little bit sloppy and write A instead of λ(γ(\underline{A})).

4.2 Definition of M(A), τ^{A}(a), A^{A}(B)

Preliminaries 4.2 In this chapter we assume, unless stated differently, A, B, C : Cl(N), a, b, c, d : N, κ, π : N such that κ, π ∈ R, all possibly with subscripts or accents (′).

Assumption 4.3 In the following we assume that for every primitive recursive set A and every k-ary primitive recursive function f defined in Sect. 2 we have defined corresponding sets A : P^{dec}(N) and functions f : N^{k} → N, such that the same lemmata, provable now in Martin-Löf’s type theory, hold.

In order to define M(A) and τ^{A}(a) we will first introduce a set C^{a}(A) (Definition 5.4). This is roughly speaking the set of ordinals built from atoms in A ∩ a by all ordinal functions, except that we restrict ψ_{κ} to κ such that a ≺ κ. For a ∈ OT, A ⊆ OT, C^{a}(A) is the least set of ordinals Y, such that:

(C1) A ∩ a ⊆ Y, (C2) 0, I ∈ Y, (C3) If b, c ∈ Y, d =′_{NF} b + c ∨ d =_{NF} φ_{b}c ∨ d =_{NF} Ω_{b} then d ∈ Y (C4) If κ, c ∈ Y, a ≺ κ, d =_{NF} ψ_{κ}c, then d ∈ Y.

Since in (C2)–(C4) we are referring to terms with length less than a, this definition can be transformed into an ordinary (not inductive) definition. This is done in Definition 5.4 in Sect. 5. In this section we only need what is stated in Assumption 4.4.

Assumption 4.4 For every A : Cl(N), and a : N we assume that there exists a b-object C^{a}(A) such that C^{a}(A) : Cl(N), which is correctly defined from A : Cl(N), and a : N, and such that (in this version and in the underlined version according to Assumption 4.1), if a ∈ OT, the following holds:

(a) C^{a}(A) ⊆ OT.

(b) 0, I ∈ C^{a}(A).

(c) ((d =_{NF} φ_{b}c ∨ d =′_{NF} b + c ∨ (d =_{NF} Ω_{b} ∧ b = c))) → (d ∈ C^{a}(A) ↔ (d ∈ A ∩ a ∨ {b, c} ⊆ C^{a}(A))).

(d) Assume d =_{NF} ψ_{κ}c.

If a ≺ κ, then d ∈ C^{a}(A) ↔ (d ∈ A ∩ a ∨ {κ, c} ⊆ C^{a}(A)).

If κ ⪯ a, then d ∈ C^{a}(A) ↔ d ∈ A ∩ a.

C^{a}(A) will be defined in Definition 5.4 and the properties are verified in Lemma 5.5.

Definition 4.5 (a) τ^{A}(a) := C^{a}(A) ∩ a.

(b) A^{A}(B) := {y ∈ M(A) | τ^{A}(y) ⊆ B}.

(c) M(A) := {y ∈ OT | y ∈ C^{y}(A)}.

Remark 4.6 (a) M(A), τ^{A}(a), A^{A}(B), are classes, correctly defined from

A, B : Cl(N) and a : N.

(b) M(A), τ^{A}(a) ⊆ OT and A^{B}(A) ⊆ M(A).

(c) Assume A ≅ A′, B ≅ B′. Then C^{a}(A) ≅ C^{a}(A′), M(A) ≅ M(A′), τ^{A}(a) ≅ τ^{A′}(a), A^{A}(B) ≅ A^{A′}(B′).

Lemma 4.7 Assume a, b ∈ OT.

(a) A ⊆ M(A) → C^{a}(A) ≅ C_{a}(A).

(b) (A ⊆ M(A) ∧ a ⪯ b) → C^{b}(A) ⊆ C^{a}(A).

(c) (A ⊆ M(A) ∧ B ⊆ M(B) ∧ A ∩ ã ≅ B ∩ ã) → C^{a}(A) ≅ C^{a}(B).

(d) a ≺ Ω_{1} → C^{a}(A) ≅ OT.

(e) Assume ψ_{I}a ⪯ b ≺ I, ψ_{I}a ⪯ c ≺ I and a ∈ C_{I}(a). Then C^{b}(A) ∩ C_{I}(a) ≅ C^{c}(A) ∩ C_{I}(a).

(f) Assume a ≺ κ, d := ψ_{κ}c ∈ OT, z := min{a, d}, A ⊆ M(A). Then d ∈ C^{a}(A) ↔ d ∈ A ∩ ã ∨ {κ, c} ⊆ C^{z}(A).

(g) (A ⊆ M(A) ∧ b̃ ⪯ c ∧ b^{−I} = c^{−I}) → C^{b}(A) ∩ (b̃ + 1) ≅ C^{c}(A) ∩ (b̃ + 1).

(h) A ∩ a ⊆ C^{a}(A).

Proof: (a), (b): We show under the assumption A ⊆ M(A) and ã ⪯ b that C^{b}(A) ⊆ C^{a}(A). Assume A ⊆ M(A). We show ∀x ∈ OT.∀a, b ∈ OT.ã ⪯ b → x ∈ C^{b}(A) → x ∈ C^{a}(A) by induction on length(x). Suppose x =_{NF} φ_{y}z ∨ x =′_{NF} y + z ∨ (x =_{NF} Ω_{y} ∧ y = z). Then x ∈ A ∩ b ∨ y, z ∈ C^{b}(A). Suppose y, z ∈ C^{b}(A). Then the assertion follows using the IH. The case x ∈ A ∩ a is trivial. Suppose x ∈ A ∩ b and a ⪯ x. Then x ∈ M(A), x ∈ C^{x}(A), y, z ∈ C^{x}(A), by IH y, z ∈ C^{a}(A), x ∈ C^{a}(A). Suppose x =_{NF} ψ_{κ}y. Then the assertion follows in a similar way. (c), (d), (h): easy. (e): Assume a, b, c as in the assertion. We show ∀u ∈ C_{I}(a).u ∈ C^{b}(A) ↔ u ∈ C^{c}(A) by Ind(length(u)) and assume u according to induction. Case u = 0, I: trivial.

Case u =_{NF} φ_{u_{1}}u_{2}∨u =′_{NF} u_{1}+u_{2}∨(u =_{NF} Ω_{u_{1}} ∧u_{1} = u_{2}). Then u_{1}, u_{2} ∈ C_{I}(a) and u ∈ C^{b}(A) ⇔ u_{1}, u_{2} ∈ C^{b}(A) ∨ u ∈ A ∩ b ⇔ u_{1}, u_{2} ∈ C^{b}(A) ∨ u ∈ A ∩ ψ_{I}a ⇔ u_{1}, u_{2} ∈ C^{c}(A) ∨ u ∈ A ∩ c ⇔ u ∈ C^{c}(A) (using the IH). Case u =_{NF} ψ_{κ}u_{1}. If κ ≺ I, then u ≺ ψ_{I}a, κ ⪯ b, c, u ∈ C^{b}(A) ⇔ u ∈ A ⇔ u ∈ C^{c}(A). If I ⪯ κ, then κ, u_{1} ∈ C_{I}(a) and (by IH) u ∈ C^{b}(A) ⇔ κ, u_{1} ∈ C^{b}(A) ∨ u ∈ A ∩ e ⇔ κ, u_{1} ∈ C^{c}(A) ∨ u ∈ A ∩ ψ_{I}a ⇔ κ, u_{1} ∈ C^{c}(A) ∨ u ∈ A ∩ c ⇔ u ∈ C^{c}(A).

(f) If ã ⪯ d, then z̃ = ã, C^{z}(A) ≅ C_{a}(A). Suppose d ≺ ã. Then κ = I,

d ∈ C^{a}(A) ⇔ d ∈ C_{a}(A) ⇔ d ∈ A ∩ ã ∨ c ∈ C^{a}(A), and by (e) ⇔ d ∈

A ∩ ã ∨ c ∈ C^{z}(A) ⇔ d ∈ A ∩ ã ∨ κ, c ∈ C^{z}(A). (g): We show ∀x ∈ OT.x ≺ b̃ → (x ∈ C^{b}(A) ↔ x ∈ C^{c}(A)) by induction on length(x), assume x according to induction. Case x = 0, I: x ∈ C^{b}(A) ∩ C^{c}(A). Case x =_{NF} φ_{b′}c′ or x =′_{NF} b′ + c′ or x =_{NF} Ω_{b′} ∧ b′ = c′. x ∈ C^{b}(A) ⇔ x ∈ A ∩ b ∨ {b′, c′} ⊂ C^{b}(A) ⇔ x ∈ A ∩ c ∨ {b′, c′} ⊂ C^{c}(A) ⇔ x ∈ C^{c}(A). Case x =_{NF} ψ_{κ}b′. Subcase κ ≺ b: x ∈ C^{b}(A) ⇔ x ∈ A ∩ b ⇔ x ∈ A ∩ c ⇔ x ∈ C^{c}(A). Subcase b ⪯ κ: By x ≺ b̃ follows κ = I, c ≺ κ. Now by (f) x ∈ C^{b}(A) ⇔ x ∈ A ∨ κ, I ∈ C^{x}(A) ⇔ x ∈ C^{c}(A). Now C^{b}(A) ∩ b̃ ≅ C^{c}(A) ∩ b̃. Further b̃ ∈ C^{c}(A) ⇔ b̃ ∈ C^{b}(A) (and therefore the assertion): “⇐” follows by (a), (b). “⇒”: Case b̃ = Ω_{d+1}: b̃ ∈ C^{c}(A) ⇔

b̃ ∈ C_{b}(A) ⇔ d ∈ C_{b}(A) ∩ b̃ ⇔ d ∈ C^{c}(A) ⇔ b̃ ∈ C^{c}(A). Case b̃ =_{NF} ψ_{I}e:

b̃ ∈ C^{b}(A) ⇒ b̃ ∈ C_{b}(A) ⇒ e ∈ C_{b}(A) ∩ C_{I}(e) ⊆ C^{c}(A) (by (e)) ⇒ ψ_{I}e ∈ C^{c}(A). ⊓ ⊔

Assumption 4.8 If not stated differently, let in the following A, A_{i}, A′, B, B_{i}, B′ : Cl(N), a, a_{i}, a′, b, b_{i}, b′, c, c_{i}, c′ : N, κ, π ∈ R.

Lemma 4.9 (a) A ⊆ M(A), b ⪯ a → τ^{A}(a) ∩ b ⊆ τ^{A}(b).

(b) (A ⊆ M(A) ∧ b ⪯ a ∧ b̃ = ã) → τ^{A}(b) ≅ τ^{A}(a) ∩ b.

(c) a ≺ Ω_{1} → τ^{A}(a) ≅ a.

(d) 0, I ∈ M(A).

(e) If A ⊆ M(A), b, c ∈ (A ∩ ã) ∪ (M(A) \ ã), a =_{NF} b + c or a =_{NF} φ_{b}c or a =_{NF} Ω_{b}, then a ∈ M(A).

Proof: (a): Lemma 4.7 (b). (b): Lemma 4.7 (a). (c): Lemma 4.7 (d). (d): 0, I ∈ C^{y}(A) for every y ∈ OT. (e): In case of b ≺ ã, b ∈ A ∩ ã ⊆ C^{a}(A), otherwise b̃ = ã, b ∈ C^{b}(A) ≅ C^{a}(A). Similarly c ∈ C^{a}(A), therefore a ∈ C^{a}(A), a ∈ M(A). ⊓ ⊔ 4.3 The Step to the Next Cardinal – W(A)

We introduce now W(A), such that essentially

W(A) = ⋂{Y ⊆ ℕ | ∀x ∈ M(A).τ^{A}(x) ⊆ Y → x ∈ Y } .

More precisely this will be characterized in the following assumption, the definition of W(A) can be found in Definition 5.6 in Sect. 5.

Assumption 4.10 For every m-type A we assume that we can define a mtype W(A), which is correctly defined from A : Cl(N), such that

(a) A^{A}(W(A)) ⊆ W(A)

(b) If B : Cl(N), then A^{A}(B) ∩ W(A) ⊆ B → W(A) ⊆ B.

Notation 4.11 By “we prove ∀x ∈ W(A).ϕ(x) by Ind(x ∈ W(A))” we mean that with B := {y : N | ϕ(y)} we show A^{A}(B) ∩ W(A) ⊆ B, i.e. for all x ∈ W(A) under the assumption ∀y ∈ τ^{A}(x).ϕ(y), which will be called induction hypothesis, holds ϕ(x). By Assumption 4.10 (b) follows then ∀x ∈ W(A).ϕ(x). By “assume x according to induction” we mean in this context “assume x ∈ W(A) and the induction hypothesis”.

Definition 4.12 (a) Let for A : Cl(N), b : N A|b := A ∩ (b + 1).

(b) A ⊑ B := A ⊆ OT ∧ ∀x ∈ A.A|x ≅ B|x (this is equivalent to A ⊆ OT ∧ A ⊆ B ∧ ∀x ∈ A.B ∩ x ⊆ A, “A is a segment of B”).

Lemma 4.13 (a) ∀x ∈ W(A).τ^{A}(x) ⊆ W(A) ∧ x ∈ M(A).

(b) (A ∩ Ω_{a} ≅ B ∩ Ω_{a} ∧ A ⊆ M(A) ∧ B ⊆ M(B)) → (M(A) ∩ Ω_{a+1} ≅ M(B) ∩ Ω_{a+1} ∧ W(A) ∩ Ω_{a+1} ≅ W(B) ∩ Ω_{a+1}).

(c) If A ≅ B, then W(A) ≅ W(B).

(d) W(A) ∩ Ω_{1} ⊑ OT.

Proof: (a): We show by Ind(x ∈ W(A)) that ∀x ∈ W(A).(τ^{A}(x) ⊆ W(A) ∧ x ∈ M(A)), which is immediate. (b): The assertion for M(A) is obvious. For W(A) we show by Ind(x ∈ W(A)) that ∀x ∈ W(A).x ≺ Ω_{a+1} → x ∈ W(B), therefore W(A) ∩ Ω_{a+1} ⊆ W(B) ∩ Ω_{b+1}, which is immediate, because of ∀y ≺ Ω_{a+1}.τ^{A}(y) ≅ τ^{B}(y). W(A) ∩ Ω_{a+1} ⊇ W(B) ∩ Ω_{b+1} follows in the same way. (c): Immediate by (b). (d): ∀x ≺ Ω_{1}.τ^{A}(x) ≅ x, therefore by (a) ∀x ∈ W(A).x ⊆ W(A), and, since W(A) ⊆ OT, ∀x ∈ W(A) ∩ Ω_{1}.W(A)|x ≅ x. ⊓ ⊔

Definition 4.14 Assume A : Cl(N).

(a) A is weakly downward closed iff ∀x, y ∈ OT.∀κ ∈ R.∀z ∈ A.(((z =′_{NF} x + y ∨ z =_{NF} φ_{x}y ∨ (z =_{NF} Ω_{x} ∧ x = y)) → (x ∈ A ∧ y ∈ A)) ∧ (z =_{NF} ψ_{κ}y → κ^{−} ∈ A)).

(b) A is downward closed, iff A is weakly downward closed, ∀x, y ∈ OT.∀z ∈ A.z =_{NF} x + y → (x ∈ A ∧ y ∈ A), ∀x ∈ A.x̃, x^{−Fi}, x^{−I} ∈ A and ∀κ ∈ R ∩ A.κ^{−} ∈ A.

(c) A is weakly upward closed bounded by C, iff (∀x, y ∈ A.∀z ∈ OT.z ⪯ C → ((z =′_{NF} x + y ∨ z =_{NF} φ_{x}y ∨ z =_{NF} Ω_{x}) → z ∈ A)) ∧ (0 ⪯ C → 0 ∈ A) ∧ (I ⪯ C → I ∈ A).

(d) A is upward closed bounded by C, iff (∀x, y ∈ A.∀z ∈ OT.z ⪯ C → ((z = x + y ∨ z = φ_{x}y ∨ z = Ω_{x} ∨ z = x^{+}) → z ∈ A)) ∧ (0 ⪯ C → 0 ∈ A) ∧ (I ⪯ C → I ∈ A).

(e) A is (weakly) upward closed, iff A is (weakly) upward closed bounded by OT.

Remark 4.15 If A is weakly downward closed and weakly upward closed bounded by C and A ⪯ C, then A is downward closed and upward closed bounded by C.

Proof: easy. ⊓ ⊔

Lemma 4.16 (a) If A ⊆ M(A) and A ∩ ã is weakly downward closed, then C^{a}(A) is downward and upward closed, τ^{A}(a) downward closed and upward closed bounded by a, and W(A) ∩ a^{+}, M(A) ∩ a^{+} are downward closed.

(b) If A ∩ κ ⊑ W(A), then A ∩ κ is weakly downward closed.

Proof: (a) Assume A ⊆ M(A), A ∩ ã weakly downward closed. We show C_{a}(A) is weakly downward closed. (Note that C^{a}(A) ≅ C_{a}(A)). Assume x =′_{NF}

y + z ∨ x =_{NF} φ_{y}z ∨ (x =_{NF} Ω_{y} ∧ y = z), x ∈ C_{a}(A). Then x ∈ A ∩ ã,

y, z ∈ A ∩ ã ⊆ C_{a}(A) or directly y, z ∈ C_{a}(A). Assume x =_{NF} ψ_{κ}y ∈ C_{a}(A), y ∈ C_{κ}(y). We show κ^{−} ∈ C_{a}(A): If κ ⪯ a, then x ∈ A ∩ ã, κ^{−} ∈ A ∩ ã ⊆ C^{a}(A). Case κ = I: κ^{−} = 0 ∈ C^{a}(A). Case a ≺ κ ≠ I: ã ⪯ x, κ ∈ C_{a}(A), κ = Ω_{z+1}for some z, by the first part of this proof z ∈ C_{a}(A), κ^{−} = z ∈ C_{a}(A) or κ^{−} =_{NF} Ω_{z} ∈ C_{a}(A). C^{a}(A) is trivially weakly upward closed, therefore C^{a}(A) is downward and upward closed. τ^{A}(a) downward and upward closed bounded by a follows from the above. W(A) ∩ a^{+}, M(A) ∩ a^{+} downward closed: Assume x =_{NF} y_{1} + y_{2} ∨ x =_{NF} φ_{y_{1}}y_{2} ∨ (x =_{NF} Ω_{y_{1}} ∧ y_{1} = y_{2}) ∨ (x =_{NF} ψ_{κ}u ∧ y_{1} = y_{2} = κ^{−}) ∨ y_{1} = y_{2} ∈ {x̃, x^{−Fi}, x^{−I}} ∨ (x ∈ R ∧ y_{1} = y_{2} = x^{−}). Assume x ∈ W(A) ∩ a^{+}. Then x ∈ C^{x}(A), y_{i} ∈ C^{x}(A) ∩ x ≅ τ^{A}(x) ⊆ W(A). Assume x ∈ M(A) ∩ a^{+}. Then x ∈ C^{x}(A), by (a) y_{i} ∈ C^{x}(A), by Lemma 4.7 (b) y_{i} ∈ C^{y_{i}}(A), y_{i} ∈ M(A).

(b) Assume A ∩ κ ⊑ W(A). Assume x =′_{NF} y_{1} + y_{2} ∨ x =_{NF} φ_{y_{1}}y_{2} ∨ (x =_{NF} Ω_{y_{1}} ∧ y_{1} = y_{2}), x ∈ A ∩ κ. Then x ∈ W(A) ⊆ M(A), x ∈ C^{x}(A), x ∉ A ∩ x, therefore y_{1}, y_{2} ∈ C^{x}(A) ∩ x ≅ τ^{A}(x) ⊆ W(A)|x ≅ A|x. Assume x =_{NF} ψ_{π}y, y ∈ C_{π}(y) and x ∈ A. Then x ∈ W(A) ⊆ M(A), x ∈ C^{x}(A), π ∈ C^{x}(A). If π = I, then π^{−} = 0 ∈ W(A). Otherwise π = Ω_{z+1} ∈ C^{x}(A), z + 1 ∈ C^{x}(A). If x ⪯ z + 1, z ∈ C^{x}(A), otherwise z + 1 ∈ τ^{A}(x) ⊆ W(A) ∩ x ⊆ A, by the first part z ∈ A ∩ x ⊆ C^{x}(A), in both cases therefore z ∈ C^{x}(A), π^{−} = z ∈ τ^{A}(x) or π^{−} =_{NF} Ω_{z} ∈ τ^{A}(x), π^{−} ∈ W(A). ⊓ ⊔

Lemma 4.17 (a) 0 ∈ W(A).

(b) If A ∩ κ ≅ W(A) ∩ κ, A ⊆ M(A), then W(A) ∩ κ^{+} is downward closed and 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): We show W(A) ∩ κ^{+} is weakly upward closed bounded by κ^{+}. By Lemma 4.16 (a) and Remark 4.15 follows the assertion.

(i) 0 ∈ W(A): (a).

(ii) Assume b ∈ W(A) ∩ κ^{+}. We show ∀c ∈ W(A).∀a ∈ OT.a =_{NF} b + c → a ∈ W(A) by Ind(c ∈ W(A)) and assume c according to induction, a =_{NF} b + c, c ∈ OT. c ∈ W(A), by Lemma 4.9 (e) therefore a ∈ M(A). Assume d ∈ τ^{A}(a). Assume d ≺ b. Then d ∈ τ^{A}(a) ∩ b ⊆ τ^{A}(b) ⊆ W(A). Assume d = b. Then d ∈ W(A). Assume b ≺ d. Then d = b + d′, 0 ≺ d′ ≺ c, therefore d =_{NF} b + d′. d′ ∈ C^{a}(A) ∩ c ⊆ τ^{A}(c), by IH d ∈ W(A). Therefore a ∈ A^{A}(W(A)) ⊆ W(A) and the assertion.

(iii) Proof for a =_{NF} φ_{b}c: We show ∀b ∈ W(A).∀c ∈ W(A).∀a ∈ OT.a =_{NF} φ_{b}c → a ≺ κ^{+} → d ∈ W(A) by Ind(b ∈ W(A)), side-Ind(c ∈ W(A)). Assume b according to maininduction, c according to side-induction. Assume a, a =_{NF} φ_{b}c, a ≺ κ^{+}. We show a ∈ W(A). Lemma 4.9 (e) yields a ∈ M(A). We show ∀d ∈ τ^{A}(a).d ∈ W(A) by side-side-Ind(length(d)). Assume d according to side-side-induction. Suppose d ⪯ max{b, c}. Then d ∈ τ^{A}(b) ∪ τ^{A}(c) ∪ {b, c} ⊆ W(A). Otherwise max{b, c} ≺ d ≺ φ_{b}c, d ∉ G. Case d =′_{NF} d_{1} + d_{2}. Then d_{i} ∈ τ^{A}(a), by side-side-IH d_{i} ∈ W(A), and by (ii) d ∈ W(A). Assume now max{b, c} ≺ d =_{NF} φ_{d_{1}}d_{2}. Subcase d_{1} ≺ b: d_{2} ≺ a, d_{2} ∈ C^{a}(A)∩a ≅ τ^{A}(a), by side-side-IH d_{2} ∈ W(A), further d_{1} ∈ C^{a}(A) ∩ b ⊆ τ^{A}(b), by main-IH d ∈ W(A). Subcase d_{1} = b: d_{2} ∈ C^{a}(A) ∩ c ⊆ τ^{A}(c), by side-IH d ∈ W(A). Subcase b ≺ d_{1}: d ⪯ c, contradicting the assumption above.

(iv) We show ∀b ∈ W(A).Ω_{b} ≺ κ^{+} → Ω_{b} ∈ W(A) by Ind(b ∈ W(A)) and assume b according to induction. If b = Ω_{b} the assertion is trivial. Let a = Ω_{b} and assume a =_{NF} Ω_{b}, a ≺ κ^{+}. a ∈ M(A) by Lemma 4.9 (e). We show ∀y ∈ τ^{A}(a).y ∈ W(A) by side-induction on length(y), and assume y according to induction. Suppose y ⪯ b. Then y ∈ τ^{A}(a)|b ⊆ τ^{A}(b) ∪ {b} ⊆ W(A). Assume b ≺ y ≺ a. Then y ∉ Fi. Case y =′_{NF} y_{1} + y_{2} or y =_{NF} φ_{y_{1}}y_{2}: y_{i} ∈ τ^{A}(a), by side-IH y_{i} ∈ W(A), by (ii), (iii) y ∈ W(A). Case y =_{NF} Ω_{y_{1}}: y_{1} ∈ τ^{A}(a) ∩ b ⊆ τ^{A}(b), by main-IH y ∈ W(A). Case y =_{NF} ψ_{κ}y_{1}. κ ≠ I. y ≺ a, therefore κ ⪯ a, y ∈ C^{a}(A), therefore y ∈ A ∩ a ⊆ W(A).

(v) We show I ≺ κ^{+} → I ∈ W(A). I ∈ M(A). We show ∀y ∈ τ^{A}(I).y ∈ W(A) by induction on length(y): If y ∈ A ∩ I, y ∈ W(A). If y = 0, y ∈ W(A) by (i). If y =′_{NF} y_{1} + y_{2} or y =_{NF} φ_{y_{1}}y_{2} or y =_{NF} Ω_{y_{1}} ∧ y_{1} = y_{2}, then by IH y_{i} ∈ W(A), by (ii), (iii), (iv) y ∈ W(A). If y =_{NF} ψ_{κ}z, y ∈ A ∩ I ⊆ W(A).

The assertion follows now by (i)–(v).

(c): Assume A ⊆ M(A), τ ∈ Car ∩ W(A), W(A) ∩ τ ≅ A ∩ τ. We show ∀y ∈ W(A).y ≺ τ^{+} → ∀κ ∈ R.(κ = I ∨ κ^{−} ∈ W(A)|τ) ∧ y ∈ C_{κ}(y) ∧ ψ_{κ}y ≺ τ^{+})

→ ψ_{κ}y ∈ W(A) by Ind(y ∈ W(A)). Then with τ := z̃ follows the assertion. Assume y according to Induction, y, κ according to the assumptions of the assertion. We show

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

by side-induction on length(u). Assume u according to induction, u ∈ C_{κ}(y) ∩ C^{ψ_{κ}y}(A) ∩ τ^{+}. Case u = 0, I: (b). Case u =′_{NF} u_{1} + u_{2} or u =_{NF} φ_{u_{1}}u_{2} or u =_{NF} Ω_{u_{1}} ∧ u_{1} = u_{2}: By IH u_{i} ∈ W(A), by (b) u ∈ W(A). Case u =_{NF} ψ_{π}u′. Subcase u ≺ ψ̃_{κ}y. Then by Lemma 4.7 (f) u ∈ A ∨ (ψ_{κ}y ≺ π = I ∧ π, u′ ∈ C^{u}(A)). If u ∈ A, u ∈ A ∩ τ ⊆ W(A). Assume now π = I and I, u′ ∈ C^{u}(A). If κ ≠ I, u ⪯ κ^{−} ∈ W(A), u ∈ C^{ψ_{κ}y}(A) ∩ κ^{−} ⊆ τ^{A}(κ^{−}) ⊆ W(A). If κ = I, u′ ≺ y. By Lemma 4.7 (e) u′ ∈ C^{ψ_{π}u′}(A) ∩ C_{π}(u′) ⊆ C^{ψ_{κ}y}(A), u′ ∈ C_{π}(u′) ∩ τ^{+} ⊆ C_{κ}(y) ∩ τ^{+}, by side-IH u′ ∈ W(A) ∩ τ^{+}. If u′ ≺ τ, u′ ∈ A ∩ y ∩ τ ⊆ C^{y}(A) ∩ y ≅ τ^{A}(y) (using Lemma 4.7 (h)). If τ ⪯ u′, ũ′ = τ = ỹ, u′ ∈ W(A) ⊆ M(A), u′ ∈ C^{u′}(A) ∩ y ≅ C^{y}(A) ∩ y ≅ τ^{A}(y). In both cases the main-IH yields u ∈ W(A). Subcase ψ̃_{κ}y = u. Then κ ≠ I, u = κ^{−} ∈ W(A). Subcase ψ̃_{κ}y ≺ u. Then using Lemma 2.15 (e) π, u′ ∈ C_{κ}(y) ∩ C^{ψ_{κ}y}(A), u′ ≺ y ≺ τ^{+}, u′ ∈ C_{π}(u′), π ⪯ τ^{+} ∨ π = I. If π ≺ τ^{+}, by side-IH π ∈ W(A), π^{−} ∈ W(A). If π = τ^{+}, π^{−} ∈ W(A). Therefore in all cases π = I ∨ π^{−} ∈ W(A)|τ. By side IH further u′ ∈ W(A), u′ ∈ M(A), u′ ∈ C^{u′}(A). If u′ ≺ ỹ, u′ ≺ τ, u′ ∈ W(A)∩τ ⊆ A∩τ, u′ ∈ A∩ỹ ⊆ τ^{A}(y). Otherwise u′ ∈ C^{u′}(A) ∩ y ≅ C^{y}(A) ∩ y ≅ τ^{A}(y). The main IH yields in all cases ψ_{π}u′ ∈ W(A), and the proof of (∗) is complete. It follows 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 κ ≠ I, κ^{−} ∈ M(A), κ^{−} ∈ C^{κ^{−}}(A) ≅ C^{ψ_{κ}y}(A), κ ∈ C^{ψ_{κ}y}(A), otherwise directly κ = I ∈ C^{ψ_{κ}y}(A), ψ_{κ}y ≺ κ, therefore ψ_{κ}y ∈ C^{ψ_{κ}y}(A), ψ_{κ}y ∈ M(A), ψ_{κ}y ∈ A^{A}(W(A)) ⊆ W(A). ⊓ ⊔

4.4 Distinguished Sets and Classes

Definition 4.18 Ag(A) := A ⊆ OT ∧ A ⊑ W(A), A is a “distinguished set” (in German “ausgezeichnete Menge”). Prog(A, B) := ∀x ∈ A.A ∩ x ⊆ B → x ∈ B. Prog(B) := Prog(Ω_{1}, B), (which is equivalent to ∀x ≺ Ω_{1}.x ⊆ B → x ∈ B) A^{+} := ⋃_{z∈A}((W(A) ∩ z^{+}) ∪ {z^{+}})

Remark 4.19 (a) A^{+} is correctly defined from A : Cl(N), a : N.

(b) If A ≅ A′, B ≅ B′, then A ⊑ B ↔ A′ ⊑ B′, Ag(A) ↔ Ag(A′), Prog(A, B) ↔ Prog(A′, B′), Prog(A) ↔ Prog(A′), A^{+} ≅ A′^{+}.

Remark 4.20 If a ∈ A, Ag(A), then τ^{A}(a) ≅ A ∩ a.

Proof: A ∩ a ⊆ C^{a}(A) ∩ a ≅ τ^{A}(a). Further a ∈ A ⊆ W(A), τ^{A}(a) ⊆ W(A) ∩ a ≅ A ∩ a. ⊓ ⊔

Lemma 4.21 Assume Ag(A).

(a) Prog(A, B) → A ⊆ B.

(b) A ∩ Ω_{1} ⊑ OT.

(c) Prog(B) → A ∩ Ω_{1} ⊆ B.

Proof: (a) Assume Prog(A, B). Let C := {y ∈ OT|y ∈ A → y ∈ B}. Then by Remark 4.20 follows A^{A}(C) ⊆ C, W(A) ⊆ C, A ⊆ B.

(b) A ∩ Ω_{1} ⊑ W(A) ∩ Ω_{1} ⊑ OT by Lemma 4.13 (d).

(c) By Prog(B), i.e. Prog(Ω_{1}, B) follows Prog(A ∩ Ω_{1}, B), and by A ∩ Ω_{1} ⊑ Ω_{1} therefore A ∩ Ω_{1} ⊆ B. ⊓ ⊔

Notation 4.22 If we have Ag(A), then by “we show ∀x ∈ A.ϕ(x) by Ind(x ∈ A)” we mean that we prove Prog(A, {x : N | ϕ(x)}), i.e. we show for all x ∈ A under the assumption (which will be called induction hypothesis) ∀y ≺ x.y ∈ A → ϕ(y) that ϕ(x) holds. By the lemma above follows then ∀x ∈ A.ϕ(x). By “assume x according to assumption” we mean “assume x ∈ A and the induction hypothesis for x”.

Lemma 4.23 Assume Ag(A).

(a) A is downward closed and upward closed bounded by A.

(b) If κ, c ∈ A, κ ∈ R, c ∈ C_{κ}(c), then ψ_{κ}c ∈ A.

(c) Ag(A^{+}) ∧ A ⊆ A^{+} ∧ ∀x ∈ A.x^{+} ∈ A^{+}.

Proof: (a): Lemma 4.17 (b). (b): Lemma 4.17 (c). (c): A ⊆ A^{+} ⊆ OT: immediate. If x ∈ A, then x̃ ∈ A, A ∩ x̃ ≅ W(A) ∩ x̃ ≅ A^{+} ∩ x̃, A^{+} ∩ x^{+} ≅ W(A) ∩ x^{+} ≅ W(A^{+}) ∩ x^{+}, x̃ ∈ A ∩ x^{+} ⊆ W(A) ∩ x^{+} ≅ W(A^{+}) ∩ x^{+}, x^{+} ∈ A^{+}, further x̃ ∈ A^{+} ∩ x^{+} ≅ W(A^{+}) ∩ x^{+}, x^{+} ∈ W(A^{+}), therefore A^{+}|x^{+} ≅ W(A^{+})|x^{+}, therefore ∀z ∈ A^{+}.A^{+}|z ≅ W(A^{+})|z, A^{+} ⊑ W(A^{+}). ⊓ ⊔

Lemma 4.24 (Uniqueness of distinguished sets). Assume A_{i} : Cl(N), A_{i} ≅ W(A_{i}) ∩ a_{i} (i = 0, 1), a_{0} ⪯ a_{1}. Then A_{0} ≅ A_{1} ∩ a_{0}.

Proof: W.l.o.g. a_{0} = a_{1}. (Otherwise replace A_{1} by A_{1} ∩ a_{0}). We show ∀y ∈ A_{0}.y ≺ a_{0} → y ∈ A_{1} by Ind(y ∈ A_{0}), assume y according to induction, y ≺ a_{0}. We show ∀z ∈ A_{1}.z ≺ y → z ∈ A_{0} by Ind(z ∈ A_{1}) and assume z according to induction, z ≺ y. A_{0} ∩ y ⊆ A_{1}, therefore A_{0} ∩ z ⊆ A_{1} ∩ z. By A_{1} ∩ z ⊆ C follows A_{1} ∩ z ⊆ A_{0} ∩ z. Therefore A_{0}|z ≅ W(A_{0})|z ≅ W(A_{1})|z ≅ A_{1}|z, z ∈ A_{0}, the side-induction is complete. Now A_{1} ∩ y ⊆ A_{0} ∩ y. Further A_{0} ∩ y ⊆ A_{1} ∩ y. Therefore y ∈ A_{0}|y ≅ W(A_{0})|y ≅ W(A_{1})|y ≅ A_{1}|y, and the main induction is complete. Therefore A_{0} ≅ A_{0} ∩ a_{0} ⊆ A_{1}, similarly A_{1} ⊆ A_{0} and we are done. ⊓ ⊔ 4.5 The Union of all Distinguished Sets – W

Definition 4.25 W := ⋃_{X:P(N).Ag(X)} X. Obviously W : Cl(N).

Lemma 4.26 (a) ∀X : P(N).Ag(X) ↔ X ⊑ W, that is: the distinguished

sets are just segments of W.

(b) If B : Cl(N) and B ⊑ W, then Ag(B).

Proof: (a), “→”: X ⊆ W is clear. Assume a ∈ X, b ∈ W ∩ a. Then there exists B : P(N) with b ∈ B and Ag(B). X′ := X|b, B′ := B|b. Then by Lemma 4.13 (b) W(X′)|b ≅ W(X)|b ≅ X|b ≅ X′ and W(B′)|b ≅ W(B)|b ≅ B|b ≅ B′. Therefore by Lemma 4.24 X′ ≅ B′, b ∈ B′ ≅ X′ ⊆ X.

“←”If a ∈ X, then there exists B : P(N) such that a ∈ B and Ag(B). The proof of “→” shows B ⊑ W, therefore X|a ≅ W|a ≅ B|a ≅ W(B)|a, therefore W(X)|a ≅ W(B)|a ≅ X|a, and we conclude Ag(X). (b): As (a), “←”. ⊓ ⊔

Lemma 4.27 Ag(W).

Proof: Assume a ∈ W. Then a ∈ A ⊑ W for some A : P(N), W|a ≅ A|a, therefore W(W)|a ≅ W(A)|a ≅ A|a ≅ W|a. ⊓ ⊔

Lemma 4.28 (a) Assume A : Cl(N), ∀x ∈ A.∃Y : P(N).Ag(Y) ∧ x ∈ Y ∧

Y ⊆ A. Then Ag(A).

(b) If A : Cl(N), y ∈ OT, Ag(A), then Ag(A ∩ y).

Proof: (a):We show A ⊑ W. Assume x ∈ A, Ag(Y), x ∈ Y ⊆ A. Then Y ⊑ W, W|x ≅ Y |x ⊆ A|x ⊆ W|x. By Lemma 4.26 Ag(A). (b): If a ∈ A ∩ y, then W(A ∩ y)|a ≅ W(A)|a ≅ A|a ≅ A ∩ y|a. ⊓ ⊔

Lemma 4.29 (a) W is downward closed and upward closed bounded by W.

(b) ∀y, z ∈ W.∀x ∈ OT.(x =_{NF} y + z ∨ x =_{NF} φ_{y}z ∨ x =_{NF} ψ_{y}z) → x ∈ W.

(c) ∀x ∈ OT.Ω_{x} ∈ W → Ω_{x+1} ∈ W.

Proof: (a) follows using Ag(W). (b): Assume Ag(A), Ag(B), y ∈ A, z ∈ B. Then A, B ⊑ W, A ∪ B ⊑ W, Ag(A∪B), y, z ∈ A∪B, y, z ∈ C := (A∪B)^{+}, Ag(C), and if x =_{NF} y +z, φ_{y}z or x =_{NF} ψ_{y}z, z ⪯ C, z ∈ C ⊆ W. (c): If Ω_{x} ∈ A, Ag(A), then Ω_{x+1} ∈ A^{+}, Ag(A^{+}). ⊓ ⊔ Lemma 4.30 Assume a ∈ M(W) ∩ I, B : P(N), τ^{W}(a) ⪯ B ⊆ W|a. Then a ∈ W.

Proof: Let B̂ := (Σx : N.x ∈ B). By assumption there is some g : B̂ → P(N) such that ∀y : B̂.Ag(gy) ∧ y0 ∈ gy. Let C : P(N), C := (⋃_{y:B̂}(gy)) ∩ a. By Lemma 4.28 follows Ag(C). We show τ^{W}(a) ⊆ W: If y ∈ τ^{W}(a), then y ∈ C^{a}(W) ∩ a, y ⪯ x ∈ W for some x ∈ B, 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 ∈ g(p(z, p)) ⊑ W for some p : z ∈ B, y ∈ W, therefore y ∈ g(p(z, p)) ⊆ C. We show ∀d ∈ W(C).d ≺ a → d ∈ C, (therefore W(C) ∩ a ⊆ C) by Ind(d ∈ W(C)). Assume d according to induction, d ≺ a. Then τ^{C}(d) ⊆ C, d ∈ C^{d}(C), by Lemma 4.7 (g) d̃ ∈ C^{d}(C)|d̃ ≅ C^{a}(C)|d̃ ≅ C^{a}(W)|d̃ ⊆ τ^{W}(a) ⊆ W, d^{+} ∈ W, W ∩ d^{+} ≅ W(W) ∩ d^{+}, W|d ≅ W(W)|d, C|d ≅ W|d ≅ W(W)|d ≅ W(C)|d, d ∈ W(C)|d ⊆ C and the induction is complete. Let C′ : P(N), 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′ ⊆ W. ⊓ ⊔

Lemma 4.31 (a) ∀x ∈ W ∩ I.Ω_{x} ∈ W.

(b) ψ_{I}0 ∈ W ∧ ∀x ∈ OT.ψ_{I}x ∈ W → ψ_{I}(x + 1) ∈ W.

Proof: (a): We show ∀a ∈ W.a ≺ I → Ω_{a} ∈ W by Ind(a ∈ W). Assume a ∈ W according to induction, a ≺ I. We have to show Ω_{a} ∈ W. If a ∈ Fi, a = Ω_{a} ∈ W. Otherwise a ≺ Ω_{a} =_{NF} Ω_{a}. Assume a ∈ A with A : P(N) such that Ag(A). τ^{W}(a) ≅ τ^{A}(a). Let B := {Ω_{y+1}|y ∈ τ^{A}(a)}. By IH and Lemma 4.29 (c) B ⊆ W|Ω_{a}, B : P(N). If y ∈ τ^{W}(Ω_{a}), ỹ ∈ τ^{W}(Ω_{a}), ỹ = Ω_{c} for some c, c ∈ τ^{W}(Ω_{a}) ∩ a ⊆ τ^{A}(a), y ≺ Ω_{c+1} ∈ B. a ∈ C^{a}(W) ⊆ C^{Ω_{a}}(W), therefore Ω_{a} ∈ C^{Ω_{a}}(W), Ω_{a} ∈ M(W). By Lemma 4.30 we conclude Ω_{a} ∈ W and therefore the assertion.

(b) Let for the proof of ψ_{I}0 ∈ W, c := 0, d := ψ_{I}0, e := 0, (and ψ_{I}e ∈ M(W)) and for the proof of ψ_{I}x ∈ W → ψ_{I}(x+1) ∈ W under the assumption ψ_{I}x ∈ W, c := ψ_{I}x, d := ψ_{I}(x + 1), e := x + 1 (and ψ_{I}x ∈ C^{ψ_{I}x}(W), x ∈ C^{ψ_{I}x}(W), e ∈ C^{ψ_{I}x}(W) ∩ C_{I}(x) ⊆ C^{ψ_{I}e}(W), ψ_{I}e ∈ M(W)). Let B := {Ω_{c+1}^{n} | n : N}. Then using (a) B ⊆ W, ∀y ∈ τ^{W}(d).∃n : N.y ≺ Ω_{c+1}^{n} ∈ B, d ∈ M(W). By Lemma 4.30 follows the assertion. ⊓ ⊔ 4.6 A Distinguished Class Containing I

The next goal is to show, (Lemma 4.38 (a)) that

W(W) ∩ I ≅ W ∩ I. (∗)

This allows us to show W(W) ∩ Ω_{I+1} is distinguished, and therefore we have defined a distinguished class, namely W(W)∩Ω_{I+1}, such that I ∈ W(W)∩Ω_{I+1}. With this result it is easy to define distinguished classes containing Ω_{I+n}. We show (∗) by proving

A^{W}(W) ∩ I ⊆ W. (∗)

In order to achieve this, by Lemma 4.31 (b) it suffices to show

ψ_{I}c ∈ A^{W}(W) → ψ_{I}c ∈ W (∗∗.)

In order to prove (∗∗), by Lemma 4.30 it suffices to show

ψ_{I}c ∈ A^{W}(W) → C^{ψ_{I}c}(W) ∩ ψ_{I}c is in P(N). (∗ ∗ ∗ )

We prove the stronger assertion that C_{I}^{W}(c) := C_{I}(c) ∩ C^{ψ_{I}c}(W) is a set (and not only a class) under the premise of (∗ ∗ ∗). This can be shown by first observing that C_{I}(c) is the least set B such that

(A1) 0, I ∈ B; (A2) B is closed under +, φ, Ω; (A3) if d =_{NF} ψ_{κ}b, κ, b ∈ B, b ≺ c, then d ∈ B; (A4) if a ∈ B ∩ I, then a ⊆ B.

(In [BS76], C_{I}(a) was essentially defined like this). This can be modified to: C_{I}(c) is the least set B, such that

(B1) 0, I ∈ B; (B2) if a, b ∈ B, d =′_{NF} a + b ∨ d =_{NF} φ_{a}b ∨ d =_{NF} Ω_{a}, then d ∈ B; (B3) if d =_{NF} ψ_{κ}b, I ≺ κ, κ, b ∈ B, b ≺ c, then d ∈ B; (B4) ψ_{I}0 ⊆ B; (B5) if b ∈ B ∩ C_{I}(b) ∩ a, then ψ_{I}b ⊆ B.

From this we derive that (this will be essentially proved in the following – in this formulation it is just no valid formula, whereas the former statements can be proved easily, but are not needed here), that, if ψ_{I}c ∈ A^{W}(W), C_{I}^{W}(c) is the least class Y, such that (D1) 0, I ∈ Y; (D2) if a, b ∈ Y, d =′_{NF} a + b, d =_{NF} φ_{a}b or d =_{NF} Ω_{a} then d ∈ Y; (D3) if κ, b ∈ Y, b ≺ c, I ≺ κ ∈ R, d =_{NF} ψ_{κ}b, then d ∈ Y; (D4) B := W ∩ ψ_{I}0 ⊆ C_{I}^{W}(c); (D5) if b ∈ Y, b ∈ C_{I}(b) ∩ c, then B := ψ_{I}(b + 1) ∩ W ⊆ Y;

where the “B” in (D4) and (D5) can always be chosen as a set. Further the definition above is a continuous inductive definition, i.e. the closure ordinal is ω. Using that in Martin-Löf’s type theory the axiom of choice holds, we can introduce C_{I}^{W}(c) as a set.

We introduce the operator Γ_{c} corresponding to the inductive definition:

Definition 4.32 Assume A : Cl(N). Then

Γ_{c}(A) := {0, I}

∪{d ∈ OT | ∃a, b ∈ A.d =′_{NF} a + b ∨ d =_{NF} φ_{a}b ∨ d =_{NF} Ω_{a}} ∪{d ∈ OT | ∃κ, b ∈ A.b ≺ c ∧ I ≺ κ ∈ R ∧ d =_{NF} ψ_{κ}b} ∪(W ∩ ψ_{I}0)

∪ ⋃_{b∈A.b∈C_{I}(b)∩c}(W ∩ ψ_{I}(b + 1))

We note that Γ_{c}(A) : Cl(N).

Definition 4.33 C_{I}^{W}(c) := C_{I}(c) ∩ C^{ψ_{I}c}(W), (which is : Cl(N)).

Lemma 4.34 Assume c ∈ OT, τ^{W}(ψ_{I}c) ⊆ W. Then

(a) If A, B : Cl(N), A ⊆ B, then Γ_{c}(A) ⊆ Γ_{c}(B).

(b) Γ_{c}(C_{I}^{W}(c)) ⊆ C_{I}^{W}(c).

Proof: (a): easy. (b): For the parts corresponding to (D1)–(D3) this is easy. Further W ∩ ψ_{I}0 ⊆ C_{I}(c) ∩ (ψ_{I}c ∩ W) ⊆ C_{I}(c) ∩ C^{ψ_{I}c}(W), and if b ∈ C_{I}^{W}(c), b ∈ C_{I}(b) ∩ c, then ψ_{I}b ∈ C_{I}(c), W ∩ ψ_{I}(b + 1) ⊆ C_{I}(c) ∩ (ψ_{I}c ∩ W) ⊆ C_{I}^{W}(c). ⊓ ⊔

If A ⊆ C_{I}^{W}(c), then Γ_{c}(A) can be defined as a set:

Lemma 4.35 Assume c : N, X : P(N), p : X ⊆ C_{I}^{W}(c), q : c ∈ OT ∧ τ^{W}(ψ_{I}c) ⊆ W. Then we can define Γ′_{p,q,c}(X) : P(N), such that Γ′_{p,q,c}(X)^{Cl} ≅ Γ_{c}(X).

Proof: ψ_{I}0 ∈ W by Lemma 4.31 (b). If b ∈ X ⊆ C_{I}^{W}(c), b ∈ C_{I}(b) ∩ c, then ψ_{I}b ∈ C_{I}^{W}(c), ψ_{I}b ∈ τ^{W}(ψ_{I}c) ⊆ W, by Lemma 4.31 (b) ψ_{I}(b + 1) ∈ W. Therefore replace in the definition of Γ_{c}(A), W ∩ ψ_{I}0 by a (definable) A : P(N) such that Ag(A) ∧ ψ_{I}0 ∈ A and W ∩ ψ_{I}(b + 1) by a A such that Ag(A) ∧ ψ_{I}(b + 1) ∈ A, and we obtain Γ′_{p,q,c}(A). ⊓ ⊔

We can now define (the type theoretical definition can be found in Sect. 5) the iteration of Γ_{c}:

Assumption and Definition 4.36 Assume c : N, X : P(N), q : c ∈ OT ∧ τ^{W}(ψ_{I}c) ⊆ W,

(a) We assume (and will explicitly define this in Definition 5.8) that for n : N we can define Γ_{c,q}^{n} : P(N) such that Γ_{c,q}^{0} ≅ ∅ and ∀n : N.Γ_{c,q}^{n+1} ≅ Γ(Γ_{c,q}^{n}) (here the n + 1 is the successor of n in N)

(b) Let Γ_{c,q}^{ω} : P(N), Γ_{c,q}^{ω} := ⋃_{n:N} Γ_{c,q}^{n}.

Lemma 4.37 Assume c : N, X : P(N), q : c ∈ OT ∧ τ^{W}(ψ_{I}c) ⊆ W. Then Γ_{c,q}^{ω} ≅ C_{I}^{W}(c).

Proof: We will omit the index c, q in this proof. “⊆” Γ^{n} ⊆ C_{I}^{W}(c) follows by induction on n : N using Lemma 4.34. “⊇” We show

∀x ∈ C_{I}^{W}(c). x ∈ Γ(∅)
∨∃x_{1}, x_{2} ∈ C_{I}^{W}(c).({x_{1}, x_{2}} ⊆ C_{I}^{W}(c) ∧
length(x_{1}) < length(x) ∧ length(x_{2}) < length(x) ∧
∀X : P(N).{x_{1}, x_{2}} ⊆ X → x ∈ Γ(X)) .

Then, using that n < m → Γ^{n} ⊆ Γ^{m} (which follows directly from Lemma 4.34) follows by induction on length(x) that ∀x ∈ C_{I}^{W}(c)∃n : N.x ∈ Γ^{n}. Case x =′_{NF} a + b or x =_{NF} φ_{a}b or (x =_{NF} Ω_{a} ∧ a = b). Then a, b ∈ C_{I}^{W}(c), let x_{1} := a, x_{2} := b. Case x =_{NF} ψ_{κ}b, I ≺ κ, b ≺ c. Then κ, b ∈ C_{I}^{W}(c), let x_{1} := κ, x_{2} := b. Case x ≺ ψ_{I}0. By Lemma 4.31 (b) ψ_{I}0 ∈ W, x ∈ C^{ψ_{I}c}(W) ∩ ψ_{I}c ∩ ψ_{I}0 ⊆ W ∩ ψ_{I}0 ⊆ Γ(∅). Otherwise ψ_{I}0 ⪯ x ≺ I, x ≺ ψ_{I}c, x ∈ C^{ψ_{I}c}(W) ∩ ψ_{I}c ≅ τ^{ψ_{I}c}(c) ⊆ W, x^{−Fi} =_{NF} ψ_{I}b for some b, ψ_{I}b ⪯ d ≺ ψ_{I}(b + 1), length(b) < length(ψ_{I}b) ≤ length(x), therefore x ∈ C_{I}^{W}(c), ψ_{I}b = x^{−Fi} ∈ C^{ψ_{I}c}(W) ∩ ψ_{I}c ⊆ W, ψ_{I}b ∈ M(W), ψ_{I}b ∈ C^{ψ_{I}b}(W), b ∈ C^{ψ_{I}b}(W) ∩ C_{I}(b) ⊆ C^{ψ_{I}c}(W) ∩ C_{I}(c) ≅ C_{I}^{W}(c) by Lemma 4.7 (e), x ∈ ψ_{I}(b + 1) ∩ W, let x_{1} := x_{2} := b. ⊓ ⊔ Lemma 4.38 (a) If ψ_{I}c ∈ A^{W}(W), then ψ_{I}c ∈ W.

(b) A^{W}(W) ∩ I ⊆ W.

(c) W ∩ I ≅ W(W) ∩ I.

Proof: (a): Assume c ∈ C_{I}(c), ψ_{I}c ∈ A^{W}(W). Then for some q Γ_{c,q}^{ω} ≅ C_{I}(c) ∩ C^{ψ_{I}c}(W) holds. Let A : P(N), A := Γ_{c,q}^{ω} ∩ I. Then A ≅ ψ_{I}c ∩ C^{ψ_{I}c}(W) ≅ τ^{W}(ψ_{I}c) ≅ ψ_{I}c ∩ W. ψ_{I}c ∈ A^{W}(W), ∀x ∈ τ^{W}(ψ_{I}c).x ⪯ x ∈ A, therefore by Lemma 4.30 ψ_{I}c ∈ W. (b): If x ∈ A^{W}(W) ∩ I, then x^{−Fi} ∈ C^{x}(W) ∩ x ⊆ W or x^{−Fi} = x ∈ A^{W}(W), by (a) again x^{−Fi} ∈ W, by Lemma 4.31 (b) x^{+Fi} ∈ W, x ∈ W(W)|x^{+Fi} ⊆ W. (c): W ⊆ W(W), and by Ind(y ∈ W(W)), using (b) follows ∀y ∈ W(W).y ≺ I → y ∈ W. ⊓ ⊔

4.7 Proving Well-ordering up to ψ_{Ω_{1}}Ω_{I+n}

Definition 4.39 W_{0} := W ∩ I, W_{S(i)} := W(W_{i}) ∩ Ω_{I+1·S(i)}. In the following we write I + i instead of I + 1 · i, similar for j, S(j), S(i) etc. instead of i.

Lemma 4.40 For all i ≺ ω Ag(W_{i}) ∧ Ω_{I+i} ∈ W_{Si} ∧ W_{i} ≅ W_{Si} ∩ Ω_{I+i}.

Proof: Meta Induction on i : N: i = 0: By Lemma 4.38 (c) W_{0} ≅ W(W) ∩ I ≅ W(W_{0}) ∩ I ≅ W_{1} ∩ I. Therefore Ag(W_{0}) ∧ W_{0} ≅ W_{1} ∩ Ω_{I}. Further I ∈ C^{I}(W), and by an easy induction on length(x) follows for all ∀x ∈ τ(I)^{W} ≅ C^{I}(W) ∩ I.x ∈ W ∩ I ≅ W_{0} ⊆ W(W_{0}), therefore Ω_{I} = I ∈ W(W_{0}) ∩ Ω_{I+1} ≅ W_{1}.

i = j +1: W_{j} ≅ W_{j+1}∩Ω_{I+j}. Therefore W_{j+1} ≅ W(W_{j})∩Ω_{I+j+1} ≅ W(W_{j+1})∩ Ω_{I+j+1} ≅ W_{j+2} ∩Ω_{I+j+1}, therefore Ag(W_{i}). Further Ω_{I+j+1} ∈ C^{Ω_{I+j+1}}(W), and if x ∈ τ^{W_{j+1}}(Ω_{I+j+1}), follows by induction on length(x) immediately x ∈ W_{j+1} ∩ Ω_{I+j+1}, x ∈ W(W_{j+1}), and therefore Ω_{I+j+1} ∈ W(W_{j+1}) ∩ Ω_{I+(j+2)} ≅ W_{j+2}. ⊓ ⊔

Theorem 4.41 For all n ∈ ℕ and each of the theories T = ML_{J}, ML_{[TD]}, ML_{J,aux}, ML_{[TD],aux} the following holds: T ⊢ ∀X : P(N).(∀y ∈ OT.(∀x ≺ y.x ∈ X) → y ∈ X) → ∀y ≺ ψ_{Ω_{1}}Ω_{I+n}.y ∈ X.

Proof: We argue first in the theories with “aux”. Assume the premise of the assertion. Then X : P(N) and Prog(X), therefore by Lemmata 4.21 (c) and 4.40 W_{Sn}∩Ω_{1} ⊆ X. By Lemma 4.40 Ω_{I+n} ∈ W_{Sn} and Ω_{1} ∈ W∩R∩I ⊆ W_{Sn}∩R, therefore by Lemma 4.23 (b) ψ_{Ω_{1}}Ω_{I+n} ∈ W_{Sn}. By W_{Sn} ∩Ω_{1} ⊑ OT we conclude ∀y : N.y ≺ ψ_{Ω_{1}}Ω_{I+n} → y ∈ X. The assertion for theories “without the aux” follows by Lemma 3.8 (a). ⊓ ⊔

Corollary 4.42 The proof theoretic strength of ML_{J}, ML_{[TD]}, ML_{J,aux}, ML_{[TD],aux} and of the extensional version of it is ψ_{Ω_{1}}(Ω_{I+ω}).

Proof: The lower bound follows by Theorem 4.41 and since the extensional version is an extension of ML_{[TD]}. The upper bound for the extensional version (and therefore of ML_{[TD]} and ML_{[TD],aux}, too) can be found in [Set96c] and by a straightforward modification of that embedding one gets the upper bounds for ML_{J} and ML_{J,aux}. ⊓ ⊔

5 The Type Theoretic Constructions used in the Well-ordering Proofs

5.1 Definition of C^{a}(A)

We will code finite sets of natural numbers as natural numbers. This makes the definition of P^{fin}(P^{fin}(N)) easy.

Definition 5.1 (a) We assume some coding of finite sets of natural numbers as lists of natural numbers, which are again coded as elements of the natural numbers. This should be done in such a way, that the set of codes for finite subsets of N, written as P^{fin}(N), is a decidable subset of the natural numbers, and that the element-relation a ∈_{fin} A and the subset-relation A ⊆_{fin} B for A : P^{fin}(N), B : P^{dec}(N) or B : P^{fin}(N) are decidable. (We usually omit the superscript fin). If A : P^{dec}(N), we define P^{fin}(A) := {y | y ∈ P^{fin}(N)∧y ⊆_{fin} A}, which should be a decidable subset of N. We assume that the operations ≅_{fin}, ∪_{fin}, ∩_{fin} can be defined as operations on P^{fin}(N) and that for for a_{1}, …, a_{n} : N the term {a_{1}, …, a_{n}}_{fin} is an element of P^{fin}(N). Further we assume all the usual properties of such an implementation.

(b) For A, B : P^{fin}(P^{fin}(N)), let A ⊗ B := {K ∪ L | K ∈ A ∧ L ∈ B}, A ⊗ B : P^{fin}(P^{fin}(N)).

(c) For A : P^{fin}(N), a ∈ OT, let A ↾ a := {K ∈ A | K ⊆_{fin} a}, A ↾ a : P^{fin}(P^{fin}(N)).

Remark 5.2 (a) (∃K ∈ A ⊗ B.K ⊆_{fin} C) ⇔ (∃K ∈ A.K ⊆_{fin} C) ∧ (∃K ∈

B.K ⊆_{fin} C).

(b) (∃K ∈ A ↾ a.K ⊆_{fin} C) ⇔ ∃K ∈ A.K ⊆_{fin} C ∩ a.

Definition 5.3 We define K_{a}(b) : P^{fin}(P^{fin}(N)) for a, b : OT by recursion on length(b). K_{a}(d) := ∅, if d ∉ OT ∨ a ∉ OT. Otherwise: K_{a}(0) := K_{a}(I) := {∅}. If d =_{NF} φ_{b}c or d =′_{NF} b + c then K_{a}(d) := (K_{a}(b) ⊗ K_{a}(c)) ∪ ({{d}} ↾ a). If d =_{NF} Ω_{b} then K_{a}(d) := K_{a}(b) ∪ ({{d}} ↾ a).

If d =_{NF} ψ_{κ}c, K_{a}(b) := \{ \begin{matrix}(K_{a}(κ) ⊗ K_{a}(c)) ∪ (\{\{d\}\} ↾ a) & if a ≺ κ \\ \{\{d\}\} & otherwise. \end{matrix}

Definition 5.4 Assume A : Cl(N). C^{a}(A) := {y ∈ OT | ∃L ∈ K_{a}(y).L ⊆_{fin} A}. Obviously, C^{a}(A) is a class, correctly defined from A : Cl(N).

Lemma 5.5 Assume A : Cl(N).

(a) C^{a}(A) ⊆ OT.

(b) 0, I ∈ C^{a}(A).

(c) ((d =_{NF} φ_{b}c ∨ d =′_{NF} b + c ∨ (d =_{NF} Ω_{b} ∧ b = c)) ∧ d ∈ OT) → (d ∈ C^{a}(A) ⇔ d ∈ A ∩ a ∨ {b, c} ⊆ C^{a}(A)).

(d) Assume d =_{NF} ψ_{κ}c.

If a ≺ κ, then d ∈ C^{a}(A) ⇔ d ∈ A ∩ a ∨ {κ, c} ⊆ C^{a}(A).

If κ ⪯ a, then d ∈ C^{a}(A) ⇔ d ∈ A ∩ a.

Proof: by Remark 5.2. ⊓ ⊔

5.2 Definition of W(A)

W(A) will be defined in such a way that it fulfills the properties in Assumption 4.10, which express: W(A) is the least set of ordinal terms B, such that A^{A}(B) ⊆ B. We define this by using the W-type as follows: W_{1}^{A} will be a tree, each node of which has as index a natural number a (which will be usually an ordinal term), and as branching degree τ̂^{A}(a), which is Σx : N.x ∈ τ^{A}(a), the collection of elements in τ^{A}(a). An ordinal term a is in W(A), if there exists a correctly defined tree (which means, that at every node the p(b, p)-th subtree has index b), the root of which has index a. The tree just considered is a verification, that a belongs to ⋂{Y |A^{A}(Y) ⊆ Y }.

Definition 5.6 (a) τ̂^{A}(a) := Σy : N.y ∈ τ^{A}(a),

(b) W_{1}^{A} := (Wx : N.τ̂^{A}(x)).

(c) Cor^{A}(t) := (∀u : W_{1}^{A}.u ⪯ t → (index(u) ∈ M(A) ∧ ∀v : τ̂^{A}(index(u)).index(pred(u)v) = v0)).

(d) W(A) := {y | ∃v : W_{1}^{A}.Cor^{A}(v) ∧ index(v) = y}.

Remark 5.7 (a) W(A) is a class, τ̂^{A}(s), W_{1}^{A} are types correctly defined from A, B : Cl(N) and a : N. Cor^{A}(t) is a type, correctly defined from A : Cl(N) and t : W_{1}^{A}.

(b) W(A) ⊆ M(A).

(c) ∀x : N.∀y : τ̂^{A}(x) → W_{1}^{A}.Cor^{A}(sup(x, y)) ↔

(x ∈ M(A) ∧ ∀v : τ̂^{A}(x).Cor^{A}(yv) ∧ index(yv) = v0). (Assumption 4.1 applies except for the last statement, where the leading W in W_{1}^{A} must not be underlined).

Proof of (c): “→”: if v : τ̂^{A}(x), u ⪯ yv, then u ≺ sup(x, y), therefore from Cor^{A}(sup(x, y)) we can infer Cor^{A}(yv), further index(sup(x, y)) = x, index(yv) = index(pred(sup(x, y))v) = v0. “←” follows similarly, using u ⪯ sup(x, y) ↔ (u = sup(x, y) ∨ ∃v : τ̂^{A}(x).u ⪯ yv). ⊓ ⊔

Proof that W(A), as defined in Definition 5.6 fulfills the conditions of Assumption 4.10: Assumption 4.10 (a): If x ∈ A^{A}(W(A)), then x ∈ M(A) and τ^{A}(x) ⊆ W(A), therefore there exist y : τ̂^{A}(x) → W_{1}^{A} and p : ∀u : τ̂^{A}(x).Cor(yu)∧index(yu) = u0. Let w := sup(x, y). By Remark 5.7 (c) follows Cor(w), index(w) = x, x ∈ W(A). Assumption 4.10 (b): Assume A^{A}(B) ∩ W(A) ⊆ B. We show ∀u : W_{1}^{A}. Cor^{A}(u) → index(u) ∈ B, by induction on W_{1}^{A} from which follows the assertion. Assume x : N, y : τ̂^{A}(x) → W_{1}^{A}, and ∀v : τ̂^{A}(yv).Cor^{A}(yv) → index(yv) ∈ B. Assume Cor^{A}(sup(x, y)). Then x = index(sup(x, y)) ∈ M(A). By Remark 5.7 (c) and the IH we get for v : τ̂^{A}(x), that v0 = index(yv) ∈ B, therefore, if u ∈ τ^{A}(x), u ∈ B, x ∈ A^{A}(B), x = index(sup(x, y)) ∈ W(A), therefore index(sup(x, y)) = x ∈ B and we are done. ⊓ ⊔

5.3 Definition of Γ_{cq}^{n}

Definition 5.8 Assume c : N, q : (c ∈ OT ∧ τ^{W}(ψ_{I}c) ⊆ W), A : P(N), p : A ⊆ C_{I}^{W}(c). By simultaneous induction on n : N we define Γ_{c,q}^{n} : P(N) and P_{c,q}^{n} : Γ_{c,q}^{n} ⊆ C_{I}^{W}(c). (Then Γ_{c,q}^{n} fulfills the assertion of Assumption 4.36 (a)). We omit the indices c, q for simplification in the following: Γ^{0} := ∅, P^{0} is a proof of ∅ ⊆ C_{W}^{I}(c). Γ^{n+1} := Γ′_{P^{n},q,c}(Γ^{n}), P^{n+1} is the proof we obtain by Γ^{n+1} ≅ Γ′_{P_{n},q,c}(Γ^{n}) ≅ Γ(Γ^{n}) ⊆ Γ(C_{I}^{W}(c)) ⊆ C_{I}^{W}(c).

A Proof of Lemma 1.10

Definition A.1 Assume α, β ∈ Ord.

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

C_{κ}^{n}(α) := C^{n}(α, ψ_{κ}α).

Lemma A.2 ⋃_{n<ω} C^{n}(α, β) = C(α, β).

Lemma A.3 (Lemma 2.7 of [BS88]) If α < β and for all α ≤ δ < β δ ∉ C_{π}(α) holds, then C_{π}(β) = C_{π}(α) and ψ_{π}β = ψ_{π}α.

Proof: “⊇” is trivial, for “⊆” we prove by induction on n ∀γ ∈ C_{π}^{n}(β).γ ∈ C_{π}^{n}(α). The only difficult case is γ = ψ_{κ}δ, δ < α, κ, δ ∈ C_{π}^{n−1}(β). But in this case δ < β, and we are done. ⊓ ⊔

Lemma A.4 (Lemma 2.8 of [BS88]) If β = min{ξ | α ≤ ξ ∈ C_{π}(α)}, then C_{π}(α) = C_{π}(β), ψ_{π}α = ψ_{π}β, and β ∈ C_{π}(β).

Proof: Lemma A.3. ⊓ ⊔

Lemma A.5 (Corresponds to Lemma [BS88] 2.11.) Assume π, γ, γ_{0} ∈ C_{κ}^{n}(α), κ ≤ π ∧ β ≤ α. Then δ := min{ξ | γ ≤ ξ ∈ C_{π}(β)} ∈ C_{κ}^{n}(α), δ′ := min{ξ | γ ≤ φ_{γ_{0}}ξ ∈ C_{π}(β)} ∈ C_{κ}^{n}(α),

Proof: Induction on n. Case γ < ψ_{κ}α: Subcase γ < ψ_{π}β: δ = γ, δ′ ≤ γ < ψ_{π}β. Subcase ψ_{π}β ≤ γ: ψ_{π}β ≤ γ < ψ_{κ}α ≤ κ ≤ π. Since C_{π}(β) ∩ π = ψ_{π}β, π ∈ C_{π}(β), follows δ = π, π ∈ C_{κ}^{n}(α). δ′ < ψ_{π}β or δ′ = π, δ′ ∈ C_{κ}^{n}(α). Case γ = 0, 1, I: δ = γ, δ′ ∈ {0, I}. In all other cases n = n′ + 1. Case γ =_{NF} γ_{1} + γ_{2}, γ_{i} ∈ C_{π}^{n′}(β): Let δ_{i} be chosen for γ_{i}. If γ ≤ δ_{1}, δ = δ_{1}. Otherwise γ_{1} ≤ δ_{1} < γ_{1} + γ_{2}, δ_{1} = γ_{1} + ρ ∈ C_{π}(β), 0 ≤ ρ < γ_{2}, therefore δ_{1} =_{NF} γ_{1} + ρ, γ_{1} ∈ C_{π}(β). Therefore γ_{1} + γ_{2} ≤ δ ≤ γ_{1} + δ_{2}, δ = γ_{1} + ρ with γ_{2} ≤ ρ ≤ δ_{2}, ρ ∈ C_{π}(β), ρ = δ_{2}, we easily check that δ_{2} ∈ A, therefore δ = δ_{1} + δ_{2} ∈ C_{κ}^{n}(β). δ′ = δ′_{1} or δ′ = δ′_{1} + 1, where δ′_{1} ∈ C_{κ}^{n′}(α) by the second IH for γ_{1}. Case γ =_{NF} φ_{γ_{1}}γ_{2}, γ_{i} ∈ C_{π}^{n′}(β): Let δ_{i} be determined for γ_{i}. Then γ ≤ φ_{δ_{1}}δ_{2}. If γ ≤ δ_{i}, δ = δ_{i}. Assume δ_{i} < γ (i = 1, 2). Then δ_{i} ≤ δ ≤ φ_{δ_{1}}δ_{2}, therefore δ ∉ G, otherwise δ = max{δ_{1}, δ_{2}}. If δ =_{NF} δ_{3} + δ_{4}, we had γ ≤ δ_{3} < δ, δ_{3} ∈ C_{π}(β), a contradiction. Therefore δ =_{NF} φ_{δ_{3}}δ_{4}, γ ≤ δ ≤ φ_{δ_{1}}δ_{2}. If δ_{3} < γ_{1}, we had γ ≤ δ_{4} < δ, δ_{4} ∈ C_{π}(β), a contradiction. Therefore γ_{1} ≤ δ_{3} ∈ C_{π}(β), δ_{1} ≤ δ_{3}. If δ_{1} < δ_{3}, by φ_{γ_{1}}γ_{2} ≤ φ_{δ_{3}}δ_{4} and γ_{1} < δ_{3} follows γ_{2} ≤ φ_{δ_{3}}δ_{4}, δ_{2} ≤ φ_{δ_{3}}δ_{4}, γ ≤ φ_{δ_{1}}δ_{2} ≤ φ_{δ_{3}}δ_{4}, φ_{δ_{1}}δ_{2} = φ_{δ_{3}}δ_{4}, δ = δ_{2} ∈ C_{κ}^{n′}(α). Otherwise δ_{1} = δ_{3}, δ_{4} = δ′_{2} ∈ C_{κ}^{n′}(α) by the second IH for γ_{0} := δ_{3}. Second part in this case: If γ_{0} < γ_{1}, then δ′ = δ, if γ_{0} = γ_{1}, then δ′ = δ_{2}, and if γ_{0} > γ_{1}, choose δ′_{2} for γ_{2}, δ = δ′_{2}. In all cases, where γ ∈ G, follows immediately δ ∈ G, δ′ ∈ {0, δ} and the assertion in the second case. Case γ = ψ_{γ_{1}}γ_{2}, γ_{i} ∈ C_{κ}^{n}(α). The case γ ∈ C_{π}(β) is trivial, let therefore γ < δ. Let δ_{i} be chosen for γ_{i}. Subcase γ_{1} < δ_{1}: γ_{1} ≠ I, δ = δ_{1}. Subcase γ_{1} = δ_{1} = δ or γ = δ: easy. Assume now γ_{1} = δ_{1}, γ < δ < γ_{1}: Subcase γ_{1} ≠ I: Then δ = ψ_{γ_{1}}δ_{3}, by γ < δ, γ_{2} < δ_{3} < β ≤ α it follows δ_{3} ∈ C_{π}(β), therefore δ_{2} ≤ δ_{3}, and by minimality and since ψ_{π}δ_{2} ≤ ψ_{π}δ_{3}, δ = ψ_{π}δ_{2} ∈ C_{κ}^{n}(α). Subcase γ_{1} = I. If δ =_{NF} Ω_{δ_{3}}, γ ≤ δ_{3} ∈ C_{π}(β), a contradiction, and if δ = ψ_{δ_{3}}δ_{4} with δ_{3} ≠ I, γ ≤ δ_{3}^{−} < δ, δ_{3}^{−} ∈ C_{π}(β), again a contradiction, therefore δ = ψ_{I}δ_{4}, and as in the subcase before follows the assertion. Case γ =_{NF} Ω_{γ_{1}}: Let δ_{1} be chosen for γ_{1}. If γ ≤ δ_{1}, δ = δ_{1}. Otherwise follows δ ∈ G, δ ≠ ψ_{δ_{3}}δ_{4} with δ_{3} ≠ I (otherwise γ ≤ δ_{3}^{−}). Therefore δ = I or =_{NF} Ω_{δ_{3}} (therefore δ_{3} = δ_{1}) or δ = ψ_{I}δ_{3} (but in this case γ ≤ Ω_{δ_{1}} < δ, a contradiction). ⊓ ⊔

Proof of Lemma 1.10: (a): “⊇” is obvious. “⊆”: We show C_{κ}^{n}(α) ⊆ C′_{κ}^{n+1}(α) by induction on n : N. Here the only difficulty is the case γ = ψ_{π}β ∈ C_{κ}^{n+1}(α), π, β ∈ C_{κ}^{n}(α), β < α. If π ≤ κ or π = I∧ψ_{I}β < κ, then γ ≤ ψ_{κ}α, otherwise follows by Lemma A.5 β_{0} := min{ξ | β ≤ ξ ∈ C_{π}(β)} ∈ C_{κ}^{n}(α) ⊆ C′_{κ}^{n+1}(α), by Lemma A.4 ψ_{π}β = ψ_{π}β_{0}, β_{0} ∈ C_{π}(β_{0}). If β = β_{0}, β_{0} < α. Otherwise β ∉ C_{π}(β_{0}) = C_{π}(β), if π ≠ I, by κ < π β ∉ C_{κ}(β_{0}), since β ∈ C_{κ}(α), β_{0} < α, and, if π = I, κ < ψ_{I}β, and from β ∉ C_{π}(β_{0}) and ψ_{κ}β_{0} < ψ_{π}β_{0} we infer β ∉ C_{κ}(β_{0}) and again β_{0} < α. Therefore γ ∈ C′_{κ}^{n+2}(α).

(b) “⊇” is obvious. “⊆”: We show by induction on α, side-induction on ρ ρ < ψ_{κ}α → ρ ∈ C′(α, κ^{−} + 1) and the assertion follows. If ρ ≤ κ^{−}, this is obvious, and, if ρ =_{NF} ρ_{1} + ρ_{2} or ρ =_{NF} φ_{ρ_{1}}ρ_{2}, or ρ =_{NF} Ω_{ρ_{1}}, this follows by side-IH. Otherwise ∃δ.δ ∈ C_{κ}(δ) ∧ δ < α ∧ ρ = ψ_{κ}δ. Then δ ∈ C_{κ}(δ) = C′(δ, κ^{−} + 1) ⊆ C′(α, κ^{−} + 1) by IH, ψ_{κ}δ ∈ C′(α, κ^{−} + 1).

(c): C_{Ω_{1}}(I^{+}) = C′(I^{+}, 1) = C′(I^{+}, 0). ⊓ ⊔

B The Order-type of the Ordinal Notation System

In this section we show that the ordinal functions in OT correspond to the those defined in Sect. 1. It is based on proofs in [Buc86].

Definition B.1 For a ∈ OT we define an ordinal o(a) ∈ Ord: o(0) := 0, o(I) := I, o((a_{1}, …, a_{n})) := o(a_{1}) + ⋯ + o(a_{n}), o(φ′_{a}b) := φ_{o(a)}o(b), o(Ω′_{a}) := Ω_{o(a)}, o(ψ_{a}b) := ψ_{o(a)}o(b).

We will prove the following lemma:

Lemma B.2 (a) C_{Ω_{1}}(I^{+}) = {o(x) | x ∈ OT}.

(b) If a ∈ OT such that a ≺ Ω_{1}, then o(a) = ordertype({x ∈ OT | x ≺ a}, ≺).

(c) ψ_{Ω_{1}}I^{+} = ordertype({x ∈ OT | x ≺ Ω_{1}}, ≺).

Proof: At the end of this section.

Lemma B.3 Assume a, b ∈ OT, u ∈ R.

(a) o(a) ∈ C_{Ω_{1}}(I^{+}).

(b) a ∈ G ⇔ o(a) ∈ G, similarly for Lim, Suc, A, R, Fi. (the first G is a subset of OT, the second G a subset of the ordinals, note the difference in the fonts).

(c) G_{o(u)}(o(a)) = {o(x) | x ∈ G_{u}(a)}.

(d) a ≺ b ⇒ o(a) < o(b).

Proof: (by induction on length(a) + length(u)), simultaneously for (a) –(d):

1. a =_{NF} ψ_{b}c: Then G_{b}(c) ≺ c and b, c ∈ OT.

(a) By IH o(b), o(c) ∈ C_{Ω_{1}}(I^{+}) and G_{o(b)}(o(c)) = {o(x) | x ∈ G_{b}(c)} < o(c). By Lemma 1.13 follows o(c) ∈ I^{+} ∩C_{o(b)}(o(c)) and therefore o(a) = ψ_{o(b)}o(c) ∈ C_{Ω_{1}}(I^{+}).

(b) trivial.

(c) Immediate by IH and definition of G_{u}(a).

(d) follows by side-induction on length(b) using the usual properties of the ordinals 0, I, of the functions +, φ, Ω_{·}, and Lemma 1.5(a), (b), (c), (f), (g).

2. All other cases follow immediately, using in (c) again side induction on length(b).

Lemma B.4 For all α ∈ C′^{n}(I^{+}, 0) exists a ∈ OT such that b = o(a).

Proof: If α = 0, I, this is immediate, if α =′_{NF} γ + δ, or α =_{NF} φ_{γ}δ or α =_{NF} Ω_{γ}, this follows by IH for γ, δ and if b =_{NF} ψ_{κ}δ, especially G_{κ}(δ) < δ, follows κ = o(r) for some r ∈ R, δ = o(d) for some d ∈ OT, G_{r}(d) < d by Lemma B.3, b = o(ψ_{r}d) with ψ_{r}d ∈ OT. ⊓ ⊔

Proof of Lemma B.2: (a) is proven. Further {o(x) | x ≺ Ω′_{0} ∧ x ∈ OT} = C_{Ω_{1}}(I^{+}) ∩ Ω_{1} = ψ_{Ω_{1}}I^{+}, o(·) is an order preserving map {x | x ≺ Ω′_{0} ∧ x ∈ OT} ⟶ ψ_{Ω_{1}}I^{+}, and for a ≺ Ω′_{1}, {o(x) | x ≺ a ∧ x ∈ OT} = C_{Ω_{1}}(I^{+}) ∩ o(a) = o(a), again o(·) is an order preserving isomorphism. ⊓ ⊔

References

[Acz77] P. Aczel. The strength of Martin-Löf’s intuitionistic type theory with one universe. In S. Miettinen and J. Väänänen, editors, Proceedings of the symposium on mathematical logic (Oulu, 1974), University of Helsinki, 1977. Report no. 2, Dept. of philosophy.

[Bar75] J. Barwise. Admissible Sets and Structures. An Approach to Definability Theory. Springer, Berlin, Heidelberg, New York, 1975.

[BB85] E. Bishop and D. Bridges. Constructive Analysis. Springer, Berlin, Heidelberg, New York, 1985.

[Bee85] M. J. Beeson. Foundations of Constructive Mathematics. Metamathematical Studies. Springer, Berlin, Heidelberg, New York, 1985.

[BFPS81] W. Buchholz, S. Feferman, W. Pohlers, and W. Sieg. Iterated Inductive Definitions. Recent Prooftheoretical Studies, volume 897 of Springer Lecture Notes in Mathematics, 1981.

[BS76] W. Buchholz and K. Schütte. Die Beziehungen zwischen den Ordinalzahlsystemen Σ und Θ̄(ω). Arch. math. Log., 17:179 – 190, 1976.

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

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

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

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

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

[Fef75] S. Feferman. A language and axioms for explicit mathematics. In J. N. Crossley, editor, Algebra and Logic. Proc. 1974, Monash Univ Australia, volume 450 of Springer Lecture Notes in Mathematics, pages 87 – 139, 1975.

[Gir87] J.-Y. Girard. Proof Theory and Logical Complexity. Bibliopolis, Napoli, 1987.

[GR94] E. Griffor and M. Rathjen. The strength of some Martin-Löf type theories. Arch. math. Log., 33:347 – 385, 1994.

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

[JP82] G. Jäger and W. Pohlers. Eine beweistheoretische Untersuchung von (Δ_{2}^{1} − CA) + BI und verwandter Systeme. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-Naturwissenschaftliche Klasse, pages 1 – 28, 1982.

[ML75] P. Martin-Löf. An intuitionistic theory of types: predicative part. In H.E. Rose and J. Sheperdson, editors, Logic Colloquium ’73, pages 73 – 118, North-Holland, Amsterdam, 1975.

[ML82] P. Martin-Löf. Constructive mathematics and computer programming. In L.J. Cohen, J. Los, H. Pfeiffer, and K.-P. Podewski, editors, Logic, Methodology and Philosophy of Science VI, pages 153–175, North-Holland, Amsterdam, 1982.

[ML84] P. Martin-Löf. Intuitionistic type theory. Bibliopolis, Naples, 1984.

[NPS90] B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s type theory. An Introduction. Oxford University-Press, Oxford, 1990.

[Pal92] E. Palmgren. Type-theoretic interpretation of iterated, strictly positive inductive definitions. Arch. math. Log., 32:75–99, 1992.

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

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

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

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

[Schü88] K. Schütte. Eine beweistheoretische Abgrenzung des Teilsystems der Analysis mit Π_{2}^{1}-Separation und Barinduktion. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, mathematisch-natur-wissenschaftliche Klasse, 1988.

[Schw92] H. Schwichtenberg. Proofs as programs. In P. Aczel, H. Simmons, and S. S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 79 – 113, Cambridge University Press, Cambridge, 1992.

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

[Set96a] A. Setzer. Extending Martin-Löf type theory by one Mahlo-universe. Submitted, 1996.

[Set96b] A. Setzer. A model for a type theory with Mahlo universe. Draft, 1996.

[Set96c] A. Setzer. An upper bound for the proof theoretical strength of Martin-Löf Type Theory with W-type and one Universe. 33pp. Draft, 1996.

[Set97a] A. Setzer. An introduction to well-ordering proofs in Martin-Löf’s type theory. Submitted, 1997.

[Set97b] A. Setzer. Translating set theoretical proofs into type theoretical programs. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Computational Logic and Proof Theory, volume 1289 of Springer Lecture Notes in Mathematics, pages 278 – 289, 1997.

[Tak87] G. Takeuti. Proof Theory. North–Holland, Amsterdam, second edition, 1987.

[TD88] A. Troelstra and D. van Dalen. Constructivism in Mathematics. An Introduction, Vol. II. North-Holland, Amsterdam, 1988.

[Tro87] A. Troelstra. On the syntax of Martin-Löf’s type theories. Theoretical Computer Science, 51:1 – 26, 1987.