A Model for a type theory with Mahlo Universe

Anton Setzer ^{∗}

January 14, 1996

Abstract

We present a type theory T T M, extending Martin-Löf Type Theory by adding one Mahlo universe V, a universe being the type theoretic analogue of one recursive Mahlo ordinal. A model, formulated in a Kripke-Platek style set theory KP M^{+}, is given and we show that the proof theoretical strength of T T M is ≤ |KP M^{+}| = ψ_{Ω_{1}}(Ω_{M+ω}). By [Se96a], this bound is sharp.

1 Introduction

M is recursive Mahlo, iff M is admissible and every M-recursive closed unbounded subset of M contains an admissible ordinal. Equivalent to this is, that M is admissible and for all Δ_{0} formulas ϕ(x, y, z⃗), and all z⃗ ∈ L_{M} such that ∀x ∈ L_{M}.∃y ∈ L_{M}.ϕ(x, y, z⃗) there exists an admissible β ∈ L_{M}, which is admissible and ∀x ∈ L_{β}∃y ∈ L_{β}.ϕ(x, y, z⃗). One can easily see, that M is recursive inaccessible and that the β above can always be chosen to be recursive inaccessible. Now one universe in Martin-Löf Type Theory is the least fixed point of an operator, which includes in the presence of the W -type the step to the next admissible. Since, using the W -type we can construct from the universe codes for a least universe, we can regard the universe as the least fixed point. We can construct this therefore precisely by iterating the operator up to the first recursive inaccessible. Proof theoretical analysis on the other hand shows, that we reach using universe and W -type the first recursive inaccessible I in the sense that we can show transfinite induction up to ψ_{Ω_{1}}(I) (in fact up to ψ_{Ω_{1}}(Ω_{I+ω}), see [Se95] or [Se93] and the related results in [GR94]). Therefore, universes in type theory correspond to recursive inaccessibles in set theory.

∗Institut für Informatik, Universität München, Theresienstr. 39, D-80333 München, Germany, email: setzer@rz.mathematik.uni-muenchen.de

Further, the universe and its Tarski-operator T have to be defined simultaneously, therefore the full universe is not only U, but Σx ∈ U.T (x) → U.

If we put this together, we get the following formulation: V is a Mahlo-universe (together with Tarski-operator T), if V is a universe, and for every function f : (Σx ∈ V.T (x) → V) → (Σx ∈ V.T (x) → V) there exists an element u_{f} : V, and a decoding function s_{f} : T (u_{f}) → V, such that (with U_{f} := T (u_{f})) the following properties hold:

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

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

In order, to make this definition possible in Logical Frameworks, we have to split the function f into two functions g : V → (T (x) → V) → V and h : Πx : V.Πy : (T (x) → V).T (gxy) → V. Further we have to define first a type U_{g,h} inductively and then define T (u_{g,h}) := U_{g,h}. We give the resulting theory preliminarily the name T T M, type theory with Mahlo universe.

In this article, we will present a model for this type theory which is an extension of the model given in [Se93] and [Se96b]. This model will show, that the proof theoretical strength of T T M is ≤ |KP M^{+}| ≤ ψ_{Ω_{1}}Ω_{M+ω}. In [Se96a] we show, that this bound is in fact sharp by giving a series of well ordering proofs, showing transfinite induction up to ψ_{Ω_{1}}(Ω_{M+n}) for n ∈ ω. Therefore the resulting theory has exactly the desired strength.

There is related work by E. Griffor and M. Rathjen on the Mahlo universe, which treats other aspects of it. There will be probably soon a draft available.

The idea, to work with Σx ∈ U.T (x) → U instead of U goes back to E. Palmgren, who told this to the author in the Oberwolfach Meeting in Mathematical Logic 1995. E. Palmgren’s studies of the super universe [Pa91] was a first major step towards the Mahlo universe.

2 The Type Theory with one Mahlo Universe

Definition 2.1 (a) We have the symbols of Martin-Löf Type Theory as in [Se93], definition 2.1, with the following modifications: we remove the term-construc-tors \underline{n}, \underline{n}_{k}, ˜+, π, σ, w, ĩ and the type constructor U; we add the termconstructors together with their arity \underline{n}_{V} (0), \underline{n}_{k,V} (0) (where k ∈ ω), ˜+_{V} (2), π_{V} (2), σ_{V} (2), w_{V} (2), ĩ_{V} (3), \underline{n} (2), \underline{n}_{k} (2) (where k ∈ ω), ˜+ (4), π (4), σ (4), w (4), ĩ (5), u (2), s (3), Res0 (4), Res1 (5), and the type constructors V (1), U (2).

(b) The b-objects are defined as in [Se93] definition 2.2 (a). We write +, ˜+_{V} infix (that is (a + b) for +(a, b)) r ˜+_{f,g}s for ˜+fgrs, (x)t for λx.t, (x, y)t for (x)(y)t, (x, y, z)t for (x)(y, z)t, \underline{n}_{f,g} for \underline{n}fg, \underline{n}_{k,f,g} for \underline{n}_{k}fg, σ_{f,g}(r, s) for σ(f, g, r, s), similarly for π, w, ĩ, Res0, Res1, u, s and if S ∈ {Σ, Π, W, σ_{V}, π_{V}, w_{V}, σ_{f,g}, π_{f,g}, w_{f,g}}, Sx ∈ s.t := S(s, (x)t). Further we write rs for Ap(r, s). The conventions about omitting brackets, the definition of simultaneous substitution (however we write t[x_{1} := s_{1}, …, x_{n} := s_{n}] instead of t[x_{1}/s_{1}, …, x_{n}/s_{n}] to avoid confusion) and α-conversion are as in [Se93], definition 2.2.

(c) The set of g-objects (for generalised objects) is inductively defined as: variables x are g-terms; if n < k, n, k ∈ ℕ, then n_{k} is a g-term; if k ∈ ℕ, then \underline{n}_{k} is a g-term; if r, s, t, s_{0}, t_{0} are g-terms, x, x′, y, z, u, u′, v, v′, v′′ ∈ V ar_{ML}, f := (u, v)s_{0}, g := (u′, v′, v′′)t_{0}, then 0, \underline{r}, \underline{n}, Sr, λx.r, p(r, s), sup(r, s), i(r), j(r), P (r, s, (x, y)t), Ap(r, s), p_{0}(r), p_{1}(r), R(r, (x, y, z)s), D(r, (x)s, (x′)t), π_{V} x ∈ r.s, σ_{V} x ∈ r.s, w_{V} x ∈ r.s, r ˜+_{V} s, ĩ_{V} (r, s, t), π_{f,g}x ∈ r.s, σ_{f,g}x ∈ r.s, w_{f,g}x ∈ r.s, r ˜+_{f,g}s, ĩ_{f,g}(r, s, t), Res0_{f,g}(r, (x)s), Res1_{f,g}(r, (x)s, t), s_{f,g}(r), u_{f,g} are gterms; if n ∈ ℕ and r, s_{1}, …, s_{n} are g-terms, then C_{n}(r, s_{1}, …, s_{n}) is a g-term. Let T erm_{Cl} be the set of closed g-terms.

(d) The g-types are N_{k} (k ∈ ω), N, V and if A, B are g-types, x, y, z, u, v, u′ ∈ V ar_{ML}, r, s, s_{0}, t_{0} g-terms, f := (y, z)s_{0}, g := (u, v, u′)t_{0}, then Πx ∈ A.B, Σx ∈ A.B, W x ∈ A.B, A + B, I(A, r, s), T (r), U_{f,g} are g-types.

(e) The g-context-pieces, g-contexts, g-statements and s[x⃗ := t⃗] are defined as in [Se93]. We treat here the usual statements A : type and s : A as abbreviations: A : type :≡ A = A, s : A :≡ s = s : A

Definition 2.2 We define Type Theory with one Mahlo-universe T T M similarly as the definition of ML_{1}^{e}W_{T} in [Se93] definition 2.5, inductively defining T T M ⊢ Γ ⇒ Θ. We only remove all the rules for the Universe and replace them by the following rules for the Mahlo-universe V:

Type introduction rules for V

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

r = r′ : V  x : T (r) ⇒ s = s′ : V (π_{V})_{I} π_{V} x ∈ r.s = π_{V} x ∈ r′.s′ : V

r : V  x : T (r) ⇒ s : V ((π_{V})_{=}) T (π_{V} x ∈ r.s) = Πx ∈ T (r).T (s)

Similar rules for N, N_{k}, Σ, W, + and I

\begin{matrix}x : V, y : (T (x) → V) ⇒ s_{0} = s′_{0} : V \\ x : V, y : (T (x) → V), z : T (s_{0}) ⇒ t_{0} = t′_{0} : V \end{matrix} (u_{I}) u_{(x,y)s_{0},(x,y,z)t_{0}} = u_{(x,y)s′_{0},(x,y,z)t′_{0}} : V

x : V, y : (T (x) → V) ⇒ s_{0} : V  x : V, y : (T (x) → V), z : T (s_{0}) ⇒ t_{0} : V (u_{=}) T (u_{(x,y)s_{0},(x,y,z)t_{0}}) = U_{(x,y)s_{0},(x,y,z)t_{0}}

Rules for U

\begin{matrix}x : V, y : (T (x) → V) ⇒ s_{0} = s′_{0} : V \\ x : V, y : (T (x) → V), z : T (s_{0}) ⇒ t_{0} = t′_{0} : V \end{matrix} (U_{T}) U_{(x,y)s_{0},(x,y,z)t_{0}} = U_{(x,y)s′_{0},(x,y,z)t′_{0}}

\begin{matrix}r = r′ : U_{f,g} & x : V, y : (T (x) → V) ⇒ s_{0} = s′_{0} : V \\ x : V, y : (T (x) → V), z : T (s_{0}) ⇒ t_{0} = t′_{0} : V \end{matrix} (s_{I}) s_{(x,y)s_{0},(x,y,z)t_{0}}(r) = s_{(x,y)s_{0},(x,y,z)t_{0}}(r′) : V

Introduction-Rules for U

In the following in all of the introduction-rules we have additional assumptions (rules with subscript I) x : V, y : (T (x) → V) ⇒ s_{0} : V and x : V, y : (T (x) → V), z : T (s_{0}) ⇒ t_{0} : V; and in all of the equality-rules (rules with subscript =) additional assumptions x : V, y : (T (x) → V) ⇒ s_{0} = s′_{0} : V and x : V, y : (T (x) → V), z : T (s_{0}) ⇒ t_{0} = t′_{0} : V. Let f := (x, y)s_{0}, f′ := (x, y)s′_{0}, g := (x, y, z)t_{0}, g′ := (x, y, z)t′_{0}.

r = r′ : U_{f,g} u : T (s_{f,g}(r)) ⇒ s = s′ : U_{f,g} (Res0_{I}) Res0_{f,g}(r, (u)s) = Res0_{f′,g′}(r′, (u)s′) : U_{f,g}
r : U_{f,g} u : T (s_{f,g}(r)) ⇒ s : U_{f,g} (Res0_{=}) s_{f,g}(Res0_{f,g}(r, (u)s)) = s_{0}[x := s_{f,g}(r), y := λu.s_{f,g}(s)] : V

\begin{matrix}u : T (s_{f,g}(r)) ⇒ s = s′ : U_{f,g} & t = t′ : T (s_{f,g}(Res0_{f,g}(r, (x)s))) \\ r = r′ : U_{f,g} \end{matrix} (Res1_{I}) Res1_{f,g}(r, (u)s, t) = Res1_{f′,g′}(r′, (u)s′, t′) : U_{f,g}

r : U_{f,g} u : T (s_{f,g}(r)) ⇒ s : U_{f,g} t : T (s_{f,g}(Res0_{f,g}(r, (u)s))) (Res1_{=}) s_{f,g}(Res1_{f,g}(r, (u)s, t)) = t_{0}[x := s_{f,g}(r), y := λu.s_{f,g}(s), z := t] : V

r = r′ : U_{f,g} x : T (s_{f,g}(r)) ⇒ s = s′ : U_{f,g} (π_{f,g})_{I} π_{f,g}x ∈ r.s = π_{f′,g′}x ∈ r′.s′ : U_{f,g}
r : U_{f,g} x : T (s_{f,g}(r)) ⇒ s : U_{f,g} (π_{f,g})_{=} s_{f,g}(π_{f,g}x ∈ r.s) = π_{V} x ∈ s_{f,g}(r).s_{f,g}(s) : V

Similar rules for N, N_{k}, Σ, W, + and I

3 Definition of KP M^{+}

Definition 3.1 (a) The language of KP M^{+} is defined as the language of KP i^{+} in [Se93] but by adding one constant ad_{m} (the Mahlo admissible). We will use all the abbreviations of [Se93].

(b) The axiom schemes for KP M^{+} are defined as for KP i^{+} in [Se93] (in the extended language) except that we replace the axiom schemes (+_{n}) by the following:

(Mahlo)^{ad_{M}} ∀z⃗ ∈ ad_{M}.((∀x ∈ ad_{M}.∃y ∈ ad_{M}.ϕ(x, y, z⃗)) →

∃w ∈ ad_{M}(Ad(w) ∧ ∀x ∈ w.∃y ∈ w.ϕ(x, y, z⃗)))

(ϕ a Δ_{0}-formula)

(Ad(ad_{M})) Ad(ad_{M}) (+_{n}) ∃x_{1}, …, x_{n}.Ad(x_{1}) ∧ ⋯ ∧ Ad(x_{n}) ∧ ad_{M} ∈ x_{1} ∧ x_{1} ∈ x_{2} ∧ ⋯

∧x_{n−1} ∈ x_{n}.

(c) KP M^{+} is the theory (Ext) + (Found) + (Pair) + (Union) + (Δ_{0}-sep) + (Δ_{0}-coll) + (inf) + (Ad.1 - 3) + (Mahlo)^{ad_{M}} + (Ad(ad_{M}))+ {(+_{n})|n ∈ ω}. So KP M^{+} is a theory, which guarantees the existence of one recursive Mahlo and of finitely many admissibles above it.

(d) We define L_{α}, func(f) (for f is a function) dom(f), rng(f) (for domain and range of a function) and Ord (the class of ordinals) as usual. M := ⋃_{α∈Ord∩ad_{M}} α. In the following α, β always denote ordinals. Inacc(α) := α ∈ Ord ∧ Ad(L_{α}) ∧ ∀x ∈ L_{α}∃y ∈ L_{α}.(Ad(y) ∧ x ∈ y) (α is an inaccessible).

(e) We define α(a), ad(u), α^{+}(u), Ad_{1}, Ad_{2} as in [Se96b].

(f) In the following in all definitions and lemmata, where we don’t mention which part can be done in KP M^{+}, the statement and definition can be carried out in KP M^{+}.

4 Interpretation of terms and types

As in [Se96b], definition 4.1 we define the meaning of a_{0}-extended g-terms, -types, b-objects.

Definition 4.1 (a) The introductory term constructors are the term constructors i, j, p, 0, S, \underline{r}, sup, \underline{n}_{V}, \underline{n}_{k,V} (k ∈ ω), ˜+_{V}, π_{V}, σ_{V}, w_{V}, ĩ_{V}, u.

(b) Let →_{red,imm}_{a_{0}} or short →_{red,imm} be the relation between closed a_{0}-extended g-terms, having the clauses for p_{0}, p_{1}, Ap, C_{n}, D, P, R, A_{i} as in [Se93], definition 5.1 (c), additionally:

\underline{n}_{f,g}→^{red,imm}\underline{n}_{V}  \underline{n}_{k,f,g}(r, s)→_{red,imm}\underline{n}_{k,V}
s_{f,g}(r)→_{red,imm}r  σ_{f,g}(r, s)→_{red,imm}σ_{V} (r, s)
π_{f,g}(r, s)→_{red,imm}π_{V} (r, s)  w_{f,g}(r, s)→_{red,imm}w_{V} (r, s)
r ˜+_{f,g}s→_{red,imm}r ˜+_{V} s  ĩ_{f,g}(r, s, t)→_{red,imm}ĩ_{V} (r, s, t)

Res0_{(x,y)s_{0},(x′,y′,z′)t_{0}}(r, (u)s)→_{red,imm}s_{0}[x := r, y := λu.s] Res1_{(x,y)s_{0},(x′,y′,z′)t_{0}}(r, (u)s, t)→_{red,imm}t_{0}[x′ := r, y′ := λu.s, z′ := t]

(c) T erm_{nf}, t^{red}, t →_{red,imm} t′ are defined as in [Se93] definition 5.1

Lemma 4.2 Lemma 5.3 of [Se93], with KP i^{+} replaced by KP M^{+}, holds.

Definition 4.3 (a) We define F^{α}, Compl(u), N_{k}^{basis}, N_{k}^{∗∗}, N^{basis}, N_{k}^{∗∗}, Π^{basis}, Π^{∗}, Σ^{basis}, Σ^{∗}, λ^{∗}, F_{W}^{basis}, F_{W}, W^{∗}, +^{basis}, +^{∗}, i^{basis}, i^{∗} as in [Se96b].

(b) u →^{∗} v := Π^{basis}(u, λ^{∗}(v)).

(c) For A being a Σ-function, n_{j} ∈ ω, i ∈ ω we define A[x⃗ := n⃗] as in [Se93], definition 5.7 (where it is written as A[x⃗/n⃗]).

(d) In the situation of (c), let (z_{i})A be the Σ-function with the same arguments as A except u_{i} i.e. ((z_{i})A)[x⃗ := n⃗] = {< u, A[z_{i} := u, x⃗ := n⃗] > |u ∈ T erm_{Cl}}.

(e) Overloading a little bit the notation of (c), we define for z ∈ V ar_{ML}, t a set (which should be a function), r ∈ T erm, (z)t(r) := {< s, t(r[z := s]) >∈ T erm_{Cl} × T C(t)|r[z := s] ∈ dom(t)}.

(f) We define the interpretation of g-types A as in [Se96b], except that we remove the definition of U^{∗}, and T (t)^{∗} and add instead: lev(V) := 1, V^{∗} := V̂^{M}, lev(T (t)) := 0, (T (t))^{∗}[x⃗ := s⃗] := T̂^{M}(t[x⃗ := s⃗]), lev(U_{f,g}) := 0, (U_{f,g})^{∗} := T̂^{M}(u_{f,g}), where V̂^{α}, T̂^{α} are defined in the next definition. For finitely many g-types this definition can be done in KP M^{+}.

Definition 4.4 (a) Complv(v) := {< r, r′ >∈ T erm_{Cl} × T erm_{Cl}|

∃s, s′ ∈ T erm_{nf}.r→_{red}s ∧ r′→_{red}s′∧ < s, s′ >∈ v}.

Complt(tv) := {< s, v >∈ T erm_{Cl} × T C(tv)| ∃s′ ∈ T erm_{Cl}.s→_{red}s′∧ < s′, v >∈ tv}.

(b) Ṽ_{α}(fv, tv) := Complv(Ṽ_{α}^{basis}(fv, tv)), T̃_{α}(fv, tv) := Complt(T̃_{α}^{basis}(fv, tv)), where

Ṽ_{α}^{basis}(fv, tv) := \{< \underline{n}_{V} , \underline{n}_{V} >\}

∪ \{< \underline{n}_{k,V} , \underline{n}_{k,V} > |k ∈ ω\}
∪ {< π_{V} x ∈ r.s, π_{V} x′ ∈ r′.s′ >∈ T erm_{nf} × T erm_{nf}|
ϕ(r, x, s, r′, x′, s′, fv(α), tv)}
∪ {< σ_{V} x ∈ r.s, σ_{V} x′ ∈ r′.s′ >∈ T erm_{nf} × T erm_{nf}|
ϕ(r, x, s, r′, x′, s′, fv(α), tv)}
∪ {< w_{V} x ∈ r.s, w_{V} x′ ∈ r′.s′ >∈ T erm_{nf} × T erm_{nf}|
ϕ(r, x, s, r′, x′, s′, fv(α), tv)}
∪ {< r ˜+_{V} s, r′ ˜+_{V} s′ >∈ T erm_{nf} × T erm_{nf}|
| < r, r′ >, < s, s′ >∈ fv(α)}
∪ {< ĩ_{V} (r, s, t), ĩ_{V} (r′, s′, t′) >∈ T erm_{nf} × T erm_{nf}|
| < r, r′ >∈ fv(α)∧ < s, s′ >, < t, t′ >∈ tv(r)}
∪ {< u_{(x,y)s,(x_{0},y_{0},z)t}, u_{(x′,y′)s′,(x′_{0},y′_{0},z′)t′} >∈ T erm_{nf} × T erm_{nf}|

|ψ(x, y, s, x_{0}, y_{0}, z, t, x′, y′, s′, x′_{0}, y′_{0}, z′, t′, β, α + 1, fv, tv)},

T̃_{α}^{basis}(fv, tv) := \{< \underline{n}_{V} , N^{∗∗} >\}

∪ \{< \underline{n}_{k,V} , N_{k}^{∗∗} > |k ∈ ω\}
∪ {< π_{V} x ∈ r.s, Π^{∗}(tv(r), (x)tv(s)) >∈ T erm_{nf} × ad(fv ∪ tv)|
ϕ(r, x, s, r, x, s, fv(α), tv)}
∪ {< σ_{V} x ∈ r.s, Σ^{∗}(tv(r), (x)tv(s)) >∈ T erm_{nf} × ad(fv ∪ tv)|
ϕ(r, x, s, r, x, s, fv(α), tv)}
∪ {< w_{V} x ∈ r.s, W^{∗}(tv(r), (x)tv(s)), α^{+}(fv ∪ tv) >

∈ T erm_{nf} × ad(ad(fv ∪ tv))|ϕ(r, x, s, r, x, s, fv(α), tv)}

∪ {< r ˜+_{V} s, +^{∗}(tv(r), tv(s)) >∈ T erm_{Cl} × ad(fv ∪ tv)|
< r, r >, < s, s >∈ fv(α)}
∪ {< ĩ_{V} (r, s, t), I^{∗}(tv(r), s, t) >∈ ad(fv ∪ tv)|
< r, r >∈ fv(α)∧ < s, s >, < t, t >∈ tv(r)}
∪ {< u_{(x,y)s,(x_{0},y_{0},z)t}, fv(β) >∈ T erm_{nf} × ad(fv ∪ tv)|

ψ(x, y, s, x_{0}, y_{0}, z, t, x, y, s, x_{0}, y_{0}, z, t, β, α + 1, fv, tv)}

ϕ(r, x, s, r′, x′, s′, v, tv) :=

< r, r′ >∈ v ∧ (∀ < t, t′ >∈ tv(r). < s[x := t], s′[x′ := t′] >∈ v) ψ(x, y, s, x_{0}, y_{0}, z, t, x′, y′, s′, x′_{0}, y′_{0}, z′, t′, β, α, fv, tv) :=

ψ′(x, y, s, x_{0}, y_{0}, z, t, x′, y′, s′, x′_{0}, y′_{0}, z′, t′, β, α, fv, tv) ∧ ∀β′ < β¬ψ′(x, y, s, x_{0}, y_{0}, z, t, x′, y′, s′, x′_{0}, y′_{0}, z′, t′, β′, α, fv, tv),

and ψ′(x, y, s, x_{0}, y_{0}, z, t, x′, y′, s′, x′_{0}, y′_{0}, z′, t′, β, α, fv, tv) := Inacc(L_{β}) ∧ β < α ∈ Ord ∧

(∀ < r, r′ >∈ fv(β).∀ < r_{0}, r′_{0} >∈ tv(r) →^{∗} fv(β).

(< s[x := r, y := r_{0}], s′[x′ := r′, y′ := r′_{0}] >∈ fv(β) ∧
∀ < s_{0}, s′_{0} >∈ tv(s[x := r, y := r_{0}]).

< t[x := r, y := r_{0}, z := s_{0}], t′[x′ := r′, y′ := r′_{0}, z := s′_{0}] >∈ fv(β))).

(c) By simultaneous recursion on α ∈ Ord we define V̂^{α}, T̂^{α}: V̂^{0} := T̂^{0} := ∅. V̂^{α+1} := Ṽ_{α}(V̂ |α, T̂^{α}), T̂^{α+1} := T̃_{α}(V̂ |α, T̂^{α}), where V̂ |α := {< γ, V̂^{γ} > |γ ≤ α}. V̂^{λ} := ⋃_{α<λ} V̂^{α}, T̂^{λ} := ⋃_{α<λ} T̂^{α} for λ limit ordinal.

We verify that similar properties as in 6.1 - 6.17 of [Se93] hold and assume the same definitions as there. Additionally we have

Lemma 4.5 ∀α ∈ M.U↾(α + 1), T^{α} ∈ L_{M}.

5 Main Lemma

Lemma 5.1 (Main lemma) Let Γ, Δ be g-context-pieces, x, x_{i} ∈ V ar_{ML}, A_{i}, A, B g-types, t, t′ g-terms, θ a gjudgement. Assume Γ = x_{1} : A_{1}, …, x_{n} : A_{n}.

(a) If T T M ⊢ Γ ⇒ t = t′ : A, then

(i) KP M^{+} ⊢ ∀Γ^{=}(r⃗; s⃗).(t = t′ : A)^{∗}[x⃗/r⃗; s⃗].

(ii) KP M^{+} ⊢ ∀Γ^{=}(r⃗; s⃗).(A = A)^{∗}[x⃗/r⃗; s⃗].

(b) If T T M ⊢ Γ ⇒ A = A′, then

KP M^{+} ⊢ ∀Γ^{=}(r⃗; s⃗).(A = A′)^{∗}[x⃗/r⃗; s⃗].

(c) If T T M ⊢ Γ, x : A, Δ ⇒ θ, then

KP M^{+} ⊢ ∀Γ^{=}(r⃗; s⃗).(A = A)^{∗}[x⃗/r⃗; s⃗].

Proof: As lemma 6.18 in [Se93], with changes for the new rules. Because of lack of space, we only give hints for some rules and treat the rule (u_{I}) carefully. For simplicity we assume for this rule that the context Γ is empty. Assume α < M. If < r, r′ >∈ V̂^{α}, < s, s′ >∈ T̂^{α}(s) →^{∗} V̂^{α}, then < r, r′ >∈ V^{∗}, < s, s′ >∈ (T (s) → V)^{∗}, by IH therefore < s_{0}[x := r, y := s], s′_{0}[x := r′, y := s′] >∈ V^{β} for some α < β < M. By (Δ_{0} − Coll)^{M} there exists α < h_{0}(α) < M such that all β can be chosen to be less than h_{0}(α).

If < t, t′ >∈ T̂^{h_{0}(α)}(s_{0}[x := r, y := s]), then < t_{0}[x := r, y := s, z := t], t′_{0}[x := r′, y := s′, z := t′] >∈ V̂^{γ} for some γ, again by the collection-axiom we can find some h_{0}(α) < h_{1}(α) < M such that we can bound the γ as before by h_{1}(α). Further we can find h_{1}(α) < h_{2}(α) < M such that Ad(h_{2}(α)). Since M is Mahlo, we can find some β < M s.t. Ad(β), ∀α < β.h_{2}(α) < β. Therefore Inacc(β) and β fulfils ψ′(x, y, s_{0}, x, y, z, t_{0}, x, y, s′_{0}, x, y, z, t′_{0}, β, β + 1, Û|β, T̂^{β}), therefore with the minimal such β′ we have ψ(x, y, s_{0}, x, y, z, t_{0}, x, y, s′_{0}, x, y, z, t′_{0}, β′, β + 1, Û|β, T̂^{β}), and therefore < u_{(x,y)s_{0},(x,y,z)t_{0}}, u_{(x,y)s′_{0},(x,y,z)t′_{0}} >∈ V̂^{β+1} ⊂ V̂^{M}. The other rules are easy, since U_{(x,y)r,(x,y,z)s}^{∗} = (T (u_{(x,y)r,(x,y,z)s}))^{∗} = V^{β} (if the assumptions as for the rule u_{I} are fulfilled) for some inaccessible β, therefore has (as in the construction of U^{∗} in [Se93]) the closure properties of a universe, and by our reduction rules we identify π_{V} and π_{f,g}, the same for the other type constructors, omit s_{f,g} and evaluate Res0_{f,g}, Res1_{f,g}. A more detailed proof will be given in a forthcoming paper.

6 Results

Lemma 6.1 |KP M^{+}| ≤ ψ_{Ω_{1}}(Ω_{M+ω}).

Proof: Adapt [Ra91] or [Bu93] as in similar to the arguments for KP i^{+} in the proof of theorem 7.8 in [Se93].

Remark: We write ≤ instead of = in 6.1 only, because we haven’t seen a wellordering proof for KP M yet (which could then be lifted to KP M^{+}) although such a proof probably exists. However the sequence (which is an unnecessary detour) |T T M| ≤ |KP M^{+}| ≤ ψ_{Ω_{1}}(Ω_{M+ω}) ≤ |T T M| shows anyway, that = holds.

Lemma 6.2 Assume ϕ is a Π_{1}^{1}-formula. Let ϕ̂ be the standard interpretation of ϕ in type theory and ϕ̃ its interpretation in KP M^{+} as in [Se96b] (with the power set of the natural numbers restricted to sets in Ad_{1}). Then, if T T M ⊢ s : ϕ̂, follows KP M^{+} ⊢ ϕ̃.

Proof: By modifying the interpretation slightly by taking in the above proof the corresponding definitions and proofs of [Se96b] instead of those in [Se93] and then as in [Se93].

Theorem 6.3 |T T M| ≤ ψ_{Ω_{1}}(Ω_{M+ω}).

Proof: as in [Se96b].

References

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

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

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

[Pa91] Palmgren, E.: Transfinite Hierarchies of Universes. U.U.D.M. Report 1991:7, Uppsala University, Department of Mathematics, Thunbergsvägen 3, S-752 38 Uppsala, Sweden.

[Ra91] Rathjen, M.: Proof-Theoretical Analysis of KP M, Arch. math. log. 30, 1991, pp. 377 – 403.

[Se93] Setzer, A.: Proof theoretical strength of Martin-Löf Type Theory with Wtype and one universe. PhD-thesis, Munich, 1993. available via

http://www.mathematik.uni-muenchen.de/∼setzer/articles/
weor0.dvi.gz

[Se95] Setzer, A.: Well-ordering proofs for Martin-Löf Type Theory with W-type and one universe. Submitted to Annals of Pure and Applied Logic. Available

via http://www.mathematik.uni-muenchen.de/∼setzer/articles/
2papdiss.dvi

[Se96a] Setzer, A.: A Type Theory for one Mahlo Universe. A preliminary version

is available via http://www.mathematik.uni-muenchen.de/∼setzer/
articles/mahlo.dvi.gz

[Se96b] Setzer, A.: An upper bound for the proof theoretical strength of Martin-Löf Type Theory with W-type and one Universe. In preparation. A preliminary

version is available via http://www.mathematik.uni-muenchen.de/
∼setzer/articles/1papdiss.dvi.gz