An upper bound for the proof theoretical strength of Martin-Löf Type Theory

with W-type and one universe

Anton Setzer ^{∗} Mathematisches Institut, Universität München Theresienstr. 39, D-80333 München, Germany email: setzer@rz.mathematik.uni-muenchen.de

January 14, 1996

1 Definition of the formal system of Martin-Löf’s type theories

Definition 1.1 (a) The symbols of Martin-Löf’s type theory are infinitely many variables z_{i} (i ∈ ω); the symbols ⇒, :, ,, (, ), =, ∈, λ; the term constructors (with their arity in parenthesis) 0 (0), \underline{r} (0), \underline{n} (0), n_{k} (for each n < k, with arity 0), \underline{n}_{k} (for each k ∈ ω, with arity 0), S (1), i (1), j (1), p_{0} (1), p_{1} (1), p (2), sup (2), R (2), Ap (2), ˜+ (2), π (2), σ (2), w (2), D (3), P (3), ĩ (3), C_{n} (n ∈ ω, arity n + 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). To make it easier to remember the meaning of the symbols, we give the following hints: \underline{r} is the (unique) element of an identity type I; n_{k} is the nth element of the finite type N_{k} with k elements, C the Casedistinction for this type; O is the zero, S the Successor, P Primitive recursion or induction over the natural numbers N; i stands for left inclusion, j for right inclusion, D is the choice in the type A + B of disjoint union of A and B; p_{0} and p_{1} are the projections, p the pairing for the Σ-type; R the Recursion) over a W -type; Ap the application of a function (as an element of a Π-type) to an element; \underline{n}, \underline{n}_{k}, ĩ, ˜+, σ, π, w are codes for the types N, N_{k}, I, +, Σ, Π, W as elements of the universe U, which become, if the Tarski-operator T is applied to them, a type.

(b) The b-objects are variables, λx.b and C(b_{1}, …, b_{n}), if C is a n-ary term or type constructor and b, b_{1}, …, b_{n} are b-objects. The set of free variables of a b-object F V (b) are defined as usual. We write +, ˜+ infix (that is (a + b) for +(a, b)) (x)t for λx.t, (x, y)t for (x)(y)t, (x, y, z)t for (x)(y, z)t, and if S ∈ {Σ, Π, W, σ, π, w}, Sx ∈ s.t := S(s, (x)t). Further we write rs for Ap(r, s). We have the usual conventions about omitting brackets, especially the scope of λx. is as long as possible, for instance λx.st should be read as λx.(st). We define for b-objects b_{1}, …, b_{n}, b and variables x_{1}, …, x_{n} the simultaneous substitution b[x_{1}/b_{1}, …, x_{n}/b_{n}] as usual (using the convention, that if x_{i} = x_{j} then the first substitution applies) and “b[x_{1}/b_{1}, …, x_{n}/b_{n}] is an allowed substitution”. α-equality (=_{α}) is defined as usual.

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

(c) The set of g-objects (for generalized objects) is inductively defined as: variables x are g-terms; if n < k, n, k ∈ IN, then n_{k} is a g-term; and if k ∈ IN, then \underline{n}_{k} is a g-term; if r, s, t are g-terms, x, y, z, x′ ∈ V ar_{ML}, x ≠ y ≠ z ≠ x, 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), πx ∈ r.s, σx ∈ r.s, wx ∈ r.s, r ˜+s, ĩ(r, s, t) are g-terms; if n ∈ IN 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, U and Πx ∈ A.B, Σx ∈ A.B, W x ∈ A.B, A + B, I(A, r, s), T (r) are g-types. (where A, B are g-types, x ∈ V ar_{ML}, r, s g-terms).

(e) A g-context-piece is a string x_{1} : A_{1}, …, x_{n} : A_{n}, where n ≥ 0, x_{i} different variables, A_{i} g-types. A g-context is a g-context-piece x_{1} : A_{1}, …, x_{n} : A_{n}, s.t. F V (A_{i}) ⊂ {x_{1}, …, x_{n−1}}. A g-statement is A = B or s = t : A where A, B are g-types, s, t are g-terms.

(f) R-terms (for Russel-terms) are defined as the g-terms, except, that we replace π, σ, w, ˜+, ĩ by Π, Σ, W, +, I respectively. R-types are defined by the same definition as the g-types, but referring to r-terms instead of g-terms. R-context-pieces, -contexts, -statements are defined as the corresponding g-construc-tions, but referring to r-terms and -types instead of the g-terms and -types.

(g) We treat the usual statements A : type and s : A as abbreviations: A : type :≡ A = A, s : A :≡ s = s : A. Note, that this is in accordance with the usual formulation, because we have extensionality.

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

Definition 1.2 of the extensional Martin-Löf Type Theory with W -type and one Universe. We will define the rules, which are of the form

(Rule) \frac{Γ_{1}⇒Θ_{1}···Γ_{n}⇒Θ_{n}}{Γ⇒Θ} ,

where Γ_{1}, …, Γ_{n}, Γ are g-context-pieces, Θ_{1}, …, Θ_{n}, Θ are g-judgements (n = 0 is allowed) in the version à là Tarski, and r-context-pieces and r-judgements in the version à là Russell. Then we define for ML = ML_{1}^{e}W_{T} (the extensional version à là Tarski) or ML = ML_{1}^{e}W_{T,U} (the extensional version à là Tarski with additional rules for the universe, which can be embedded in the version à là Rusell), ML ⊢ Γ ⇒ Θ inductively by:

If (Rule) is a rule of ML as above, Δ is a g-context-piece such that Δ, Γ_{1}, , …, Δ, Γ_{n}, Δ, Γ are g-contexts, and if ML ⊢ Δ, Γ_{i} ⇒ Θ_{i} for i = 1, …, n, then ML ⊢ Δ, Γ ⇒ Θ. Analogously we define ML_{1}^{e}W_{R} ⊢ Γ ⇒ Θ (the extensional version à là Russell) and ML_{1}^{e}W_{R,U} ⊢ Γ ⇒ Θ ML_{1}^{e}W_{R,U} ⊢ Γ ⇒ Θ (the version à là Russell corresponding to ML_{1}^{e}W_{T,U}), but referring to r-context-pieces, r-contexts etc.instead of g-context-pieces, gcontexts etc. We will write Θ for ⇒ Θ as a premise of a rule. In the following, let A, B, A′, B′ be g-types (or r-types in the formualtion à là Russell), a, b, r, s, t, r_{i}, s_{i}, t_{i}, a′, b′, r′, s′, t′, r′_{i}, s′_{i}, t′_{i}, t′′ be g-terms (or r-terms) θ, θ′ be g-(or r- )judgements Γ′ be a g-(r-)context-pieces. Further let x, y, z, u ∈ V ar_{ML}. Additionally assume for all rules, that all substitution mentioned explicitly are allowed. For instance in the rule (N_{S}^{=}), assume that s_{1}[x/t, y/P (t, s_{0}, (x, y)s_{1})] and A[z/St] are allowed substitutions.

General rules

(ASS) \frac{A type}{x:A⇒x:A}  (T HIN) \frac{A type  Γ′⇒Θ}{x:A,Γ′⇒Θ}

(SY M) \frac{t=t′:A}{t′=t:A}  _{\frac{A=B}{B=A}}  (SUB) \frac{x:A,Γ′⇒Θ ⇒t:A}{Γ′[x/t]⇒Θ[x/t]}

(T RANS) \frac{t=t′:A t′=t′′:A}{t=t′′:A} \frac{A=B B=C}{A=C} (REP L1) \frac{x:A,Γ′⇒B type ⇒t=t′:A}{Γ′[x/t]⇒B[x/t]=B[x/t′]}

(REP L2) \frac{x:A,Γ′⇒s:B Γ′⇒t=t′:A}{Γ′[x/t]⇒s[x/t]=s[x/t′]:B[x/t]}  (REP L3) _{\frac{t:A A=B}{t:B}} \frac{t=t′:A A=B}{t=t′:B}

(ALP HA) \frac{x:A,Γ′⇒θ}{x:A′,Γ′⇒θ}  \frac{A type}{A=A′}  \frac{t:A}{t=t′:A}  (if A=_{α}A′, t=_{α}t′)

Type introduction rules

(N_{k}^{T}) N_{k} type (k ∈ IN)  (N^{T}) N type

(Π^{T}) \frac{A=A′ x:A⇒B=B′}{Πx∈A.B=Πx∈A′.B′}  (Σ^{T}) \frac{A=A′ x:A⇒B=B′}{Σx∈A.B=Σx∈A′.B′}

(W^{T}) \frac{A=A′ x:A⇒B=B′}{W x∈A.B=W x∈A′.B′}  (+^{T}) \frac{A=A′ B=B′}{A+B=A′+B′}

(I^{T}) \frac{A=A′ t=t′:A s=s′:A}{I(A,t,s)=I(A′,t′,s′)}

Introduction rules

(N_{k}^{I}) n_{k} : N_{k} (n < k, n, k ∈ IN)  (N^{I}) 0 : N \frac{t=t′:N}{St=St′:N}

(Π^{I}) \frac{x:A⇒t=t′:B x:A⇒B type}{λx.t=λx.t′:Πx∈A.B}  (Σ^{I}) \frac{s=s′:A t=t′:B[x/s] x:A⇒B type}{p(s,t)=p(s′,t′):Σx∈A.B}

(W^{I}) \frac{r=r′:A s=s′:B[x/r]→W x∈A.B x:A⇒B type}{sup(r,s)=sup(r′,s′):W x∈A.B}

(+_{1}^{I}) \frac{s=s′:A A type B type}{i(s)=i(s′):A+B}  (+_{1}^{I})\frac{s=s′:B A type B type}{j(s)=j(s′):A+B}

(I^{I}) \frac{t=t′:A}{\underline{r}:I(A,t,t′)}

Elimination rules

(N_{k}^{E}) \frac{t=t′:N_{k} s_{i}=s′_{i}:A[x/i_{k}](i=0...k−1) x:N_{k}⇒A type}{C_{k}(t,s_{0},...,s_{k−1})=C_{k}(t′,s′_{0},...,s′_{k−1}):A[x/t]} (k ∈ IN)

(N^{E}) \frac{r=r′:N s=s′:A[z/0] x:N,y:A[z/x]⇒t=t′:A[z/Sx] x:N⇒A[z/x] type}{P (r,s,(x,y)t)=P (r′,s′,(x,y)t′):A[z/r]}

(Π^{E}) \frac{r=r′:A s=s′:Πx∈A.B x:A⇒B type}{Ap(s,r)=Ap(s′,r′):B[x/r]}

(Σ_{0}^{E}) \frac{r=r′:Σx∈A.B x:A⇒B type}{p_{0}(r)=p_{0}(r′):A}  (Σ_{1}^{E}) \frac{r=r′:Σx∈A.B x:A⇒B type}{p_{1}(r)=p_{1}(r′):B[x/p_{0}(r)]}

(W^{E}) \frac{r=r′:W x∈A.B x:A,y:B→W x∈A.B,z:Πv∈B.C[u/Ap(y,v)]⇒t=t′:C[u/sup(x,y)] u:W x∈A.B⇒C type}{R(r,(x,y,z)t)=R(r′,(x,y,z)t′):C[u/r]}

(+^{E}) \frac{r=r′:A+B x:A⇒s=s′:C[z/i(x)] y:B⇒t=t′:C[z/j(y)] z:A+B⇒C type}{D(r,(x)s,(y)t)=D(r′,(x)s′,(y)t′):C[z/r]}

(I^{E}) \frac{r:I(A,s,t) s:A t:A}{s=t:A}

Equality rules

(N_{k}^{=}) \frac{s_{i}:A[x/i_{k}](i=0...k−1) x:N_{k}⇒A type}{C_{k}(n_{k},s_{0},...,s_{k−1})=s_{n}:A[x/n_{k}]} (n < k, n, k ∈ IN)

(N_{0}^{=}) \frac{s:A[z/0] x:N,y:A[z/x]⇒t:A[z/Sx] x:N⇒A[z/x] type}{P (0,s,(x,y)t)=s:A[z/0]}

(N_{S}^{=}) \frac{r:N s:A[z/0] x:N,y:A[z/x]⇒t:A[z/Sx] x:N⇒A[z/x] type}{P (Sr,s,(x,y)t)=s_{1}[x/r,y/P (r,s,(x,y)t)]:A[z/Sr]}

(Π^{=}) \frac{λx.t:Πx∈A.B r:A x:A⇒B type}{Ap(λx.t,r)=t[x/r]:B[x/r]}  ^{(Π^{η}) \frac{t:Πx∈A.B}{λx.Ap(t,x)=t:Πx∈A.B}  If x ∉ F V (t)}

(Σ_{0}^{=}) \frac{p(r,s):Σx∈A.B A type}{p_{0}(p(r,s))=r:A}  (Σ_{1}^{=}) \frac{p(r,s):Σx∈A.B x∈A⇒B type}{p_{1}(p(r,s))=s:B[x/r]}

(Σ_{2}^{=}) \frac{t:Σx∈A.B}{t=p(p_{0}(t),p_{1}(t)):Σx∈A.B}

(W^{=}) \frac{{r:A  s:(B[x/r]→W x∈A.B)  x:A,y:B→W x∈A.B,z:(Πv∈B.C[u/Ap(y,v)])⇒t:C[u/sup(x,y)] \atop u:W x∈A.B⇒C typex:A⇒B type}}{R(sup(r,s),(x,y,z)t)=t[x/r,y/s,z/λv.R(Ap(s,v),(x,y,z)t)]:C[u/sup(r,s)]}

(If v ∉ F V (s) ∪ F V ((x, y, z)t))

(+_{0}^{=}) \frac{r:A x:A⇒s:C[z/i(x)] y:B⇒t:C[z/j(y)] z∈A+B⇒C type}{D(i(r),(x)s,(y)t)=t[x/r]:C[z/i(r)]}

(+_{1}^{=}) \frac{r:B x:A⇒s:C[z/i(x)] y:B⇒t:C[z/j(y)] z∈A+B⇒C type}{D(j(r),(x)s,(y)t)=t[y/r]:C[z/j(r)]}

(I^{=}) \frac{r:I(A,s,t) A type}{r=\underline{r}:I(A,s,t)}

Rules for the universe Type introduction rules for the universe

(U^{I}) U type  (T^{I})\frac{a=a′:U}{T (a)=T (a′)}

Introduction rules for the universe

(\underline{n}_{k}^{I}) \underline{n}_{k} : U (k ∈ ω)  (\underline{n}^{I}) \underline{n} : U

(π^{I}) \frac{a=a′:U x:T (a)⇒b=b′:U}{πx∈a.b=πx∈a′.b′:U}  (σ^{I}) \frac{a=a′:U x:T (a)⇒b=b′:U}{σx∈a.b=σx∈a′.b′:U}

(w^{I}) \frac{a=a′:U x:T (a)⇒b=b′:U}{wx∈a.b=wx∈a′.b′:U}  ( ˜+^{I}) \frac{a=a′:U b=b′:U}{a_{+}b=a′_{+}b′:U}

(i^{I}) \frac{a=a′:U s=s′:T (a) t=t′:T (a)}{_{i}(a,s,t)=_{i}(a′,s′,t′):U}

Equality rules for the universe

(\underline{n}_{k}^{=}) T (\underline{n}_{k}) = N_{k} (k ∈ ω)  (\underline{n}^{=}) T (\underline{n}) = N

(π^{=}) \frac{a:U x:T (a)⇒b:U}{T (πx∈a.b)=Πx∈T (a).T (b)}  (σ^{=}) \frac{a:U x:T (a)⇒b:U}{T (σx∈a.b)=Σx∈T (a).T (b)}

(w^{=}) \frac{a:U x:T (a)⇒b:U}{T (wx∈a.b)=W x∈T (a).T (b)}  ( ˜+^{=}) \frac{a:U b:U}{T (a_{+}b)=T (a)+T (b)}

(i^{=}) \frac{a:U t:T (a) s:T (a)}{T (_{i}(a,t,s))=I(T (a),t,s)}

The rules of ML_{1}^{e}W_{T} are all rules mentioned above (using g-terms, g-types etc.). The rules of ML_{1}^{e}W_{T,U} are all rules of ML_{1}^{e}W_{T} and additionally the following rules:

(σ^{E}) \frac{σx∈a.b:U}{a:U} \frac{σx∈a.b:U}{x:T (a)⇒b:U}  (π^{E}) \frac{πx∈a.b:U}{a:U} \frac{πx∈a.b:U}{x:T (a)⇒b:U}

(w^{E}) \frac{wx∈a.b:U}{a:U} \frac{wx∈a.b:U}{x:T (a)⇒b:U}  ( ˜+^{E}) \frac{a_{+}b:U}{a:U} \frac{a_{+}b:U}{b:U}

(i^{=}) \frac{i(a,s,t):U}{s:a} \frac{i(a,s,t):U}{t:a}

The rules of ML_{1}^{e}W_{R} are the same as the rules of ML_{1}^{e}W_{T}, but referring to r-terms, r-types etc. and replacing the Rules for the Universe by:

Rules for the universe à là Russell

Type introduction rules for the universe

(U^{I}) U type  (T^{I})\frac{a=a′}{a=a′}

Introduction rules for the universe

(N_{k}^{U}) N_{k} : U (k ∈ ω)  (N_{k}^{U}) N : U

(Π^{U}) \frac{a=a′:U x:a⇒b=b′:U}{Πx∈a.b=Πx∈a′.b′:U}  (Σ^{U}) \frac{a=a′:U x:a⇒b=b′:U}{Σx∈a.b=Σx∈a′.b′:U}

(W^{U}) \frac{a=a′:U x:a⇒b=b′:U}{W x∈a.b=W x∈a′.b′:U}  (+^{U}) \frac{a=a′:U b=b′:U}{a+b=a′+b′:U}

(I^{U}) \frac{a=a′:U t=t′:a s=s′:a}{I(a,t,s)=I(a′,t′,s′):U}

The rules of ML_{1}^{e}W_{R,U} are all rules of ML_{1}^{e}W_{R} and additionally the following rules:

(Σ^{U,E}) _{\frac{Σx∈a.b:U}{a:U}} _{\frac{Σx∈a.b:U}{x:a⇒b:U}}  (Π^{U,E}) _{\frac{Πx∈a.b:U}{a:U}} _{\frac{Πx∈a.b:U}{x:a⇒b:U}}

(W^{U,E}) _{\frac{W x∈a.b:U}{a:U}} _{\frac{W x∈a.b:U}{x:a⇒b:U}}  (+^{U,E}) _{\frac{a+b:U}{a:U}} _{\frac{a+b:U}{b:U}}

(i^{U,E} \frac{I(a,s,t):U}{s:a} \frac{I(a,s,t):U}{t:a}

2 Comparison of the formulation à là Russell and the formulation à là Tarski

In this section we prove, that ML_{1}^{e}W_{R,U} can be embeddded in ML_{1}^{e}W_{T,U}. Therefore, the upper bound proved for ML_{1}^{e}W_{T,U} is an upper bound for ML_{1}^{e}W_{R} and ML_{1}^{e}W_{R,U} as well. Definition 2.1 (a) Define for C constructors,

ψ(N) :≡ \underline{n} ψ(N_{k}) :≡ \underline{n}_{k}, ψ(Π) :≡ π, ψ(Σ) :≡ σ, ψ(W) :≡ w, ψ(+) :≡ ˜+, ψ(I) :≡ ĩ

ψ(C) :≡ C otherwise

(b) Define ψ : r-term → g-term by recursion on the b-objects:

ψ(x) :≡ x (x ∈ V ar_{ML}), ψ(λx.t) :≡ λx.ψ(t), ψ(C(t_{1}, …, t_{n})) :≡ ψ(C)(ϕ(t_{1}), …, ϕ(t_{n})).

(c) Define the function ρ : r-type → g-type by recursion on the g-types:

ρ(Sx ∈ r.s) :≡ Sx ∈ ρ(r).ρ(s) (S ∈ Σ, Π, W),

ρ(r + s) :≡ ρ(r) + ρ(s),  ρ(I(r, s, t)) :≡ I(ρ(r), ψ(s), ψ(t)),
ρ(C) :≡ C for C ∈ {N, N_{k}, U},  ρ(t) :≡ T (ψ(t)), otherwise.

(d) If Γ = x_{1} : A_{1}, …, x_{n} : A_{n} is a g-context-piece, then ρ(Γ) :≡ x_{1} : ρ(A_{1}), …, x_{n} : ρ(A_{n})

(e) If r, s are g-terms, A is a g-type, then

ρ(r = s : A) :≡ (ψ(r) = ψ(s) : ρ(A)),  ρ(A = B) :≡ (ρ(A) = ρ(B)).

(f) Define μ : g-type → g-type by recursion on the g-types: μ(T (sx ∈ r.s)) :≡ Sx ∈ μ(T (r)).μ(T (s)) (where s = σ, π, w and S = Σ, Π, W respectively),

μ(T (r ˜+s)) :≡ μ(T (r)) + μ(T (s)),  μ(ĩ(r, s, t))) :≡ I(μ(T (r)), s, t),
μ(T (\underline{n})) :≡ N  μ(T (\underline{n}_{k})) :≡ N_{k}
μ(r + s) :≡ μ(r) + μ(s),  μ(I(r, s, t)) :≡ I(μ(r), s, t),

μ(Sx ∈ r.s) :≡ Sx ∈ μ(r).μ(s) (S ∈ {Σ, Π, W }) μ(t) :≡ t, otherwise.

Lemma 2.2 Assume r, s, t, s_{i} b-objects, x_{i} ∈ V ar_{ML}.

(a) F V (t) = F V (ψ(t)) = F V (ρ(t)) = F V (μ(t)).

(b) If t[x_{1}/s_{1}, …, x_{n}/s_{n}] allowed, then ψ(t)[x_{1}/ψ(s_{1}), …, x_{n}/ψ(s_{n})], μ(t)[x_{1}/ψ(s_{1}), …, x_{n}/ψ(s_{n})], ρ(t)[x_{1}/ψ(s_{1}), …, x_{n}/ψ(s_{n})] are allowed.

(c) If t is a r-term, then ρ(t) = μ(T (ψ(t))).

(d) If t, s_{i} are b-objects, then ψ(t[x_{1}/s_{1}, …, x_{n}/s_{n}]) = ψ(t)[x_{1}/ψ(s_{1}), …, x_{n}/ψ(s_{n})]. If t is a g-type, s_{i} are g-terms, then μ(μ(t)) = μ(t), μ(t[x_{1}/s_{1}, …, x_{n}/s_{n}]) = μ(μ(t)[x_{1}/s_{1}, …, x_{n}/s_{n}]), If t is an r-type, s_{i} are r-terms, then ρ(t[x_{1}/s_{1}, …, x_{n}/s_{n}]) = μ(ρ(t)[x_{1}/ψ(s_{1}), …, x_{n}/ψ(s_{n})]).

(e) If t is a g -judgement, -statement, -context, -context-piece, then ρ(t) is an r-judge-ment, -statement, -context, -context-piece.

(f) r=_{α}s → ψ(r)=_{α}ψ(s), ρ(r)=_{α}ρ(s), μ(r)=_{α}μ(s).

(g) If r is a g-term and b-term, then ψ(r) = r.

If r is a g-type and b-type, then ρ(r) = r.

Lemma 2.3 In all versions of Martin-Löf Type Theory, we have the following useful derived rule:

\frac{Γ, x : A, Γ′ ⇒ θ Γ ⇒ A = A′}{Γ, x : A′, Γ′ ⇒ θ}

Proof: Let y be a fresh variable. Then by (T HIN) Γ, y : A′, x : A, Γ′ ⇒ θ, easily we have Γ, y : A′ ⇒ y : A, By (SUB) Γ, y : A′, Γ′[x/y] ⇒ θ[x/y], and by change of the variable the assertion. Lemma 2.4 Let ML_{T} be ML_{1}^{e}W_{T} or ML_{1}^{e}W_{T,U} and Γ, Γ′ be g-context-pieces, a, b, t gterms, A, B g-types, x a variable. The following applies:

(a) If ML_{T} ⊢ Γ ⇒ s : A, or ML_{T} ⊢ Γ ⇒ s = t : A then ML_{T} ⊢ Γ ⇒ A type.

(b) If ML_{T} ⊢ Γ ⇒ Sx ∈ A.B type (S ∈ {Σ, Π, W }), then ML_{T} ⊢ Γ ⇒ A, ML_{T} ⊢ Γ, y : A ⇒ B[x/y] type, for all y ∈ V ar_{ML} \ X for some finite set X.

(c) If ML_{T} ⊢ Γ ⇒ A + B type then ML_{T} ⊢ Γ ⇒ A type, ML_{T} ⊢ Γ ⇒ B type.

(d) If ML_{T} ⊢ Γ ⇒ I(A, b, c) type, then ML_{T} ⊢ Γ ⇒ b : A, ML_{T} ⊢ Γ ⇒ c : A.

(e) If ML_{T} ⊢ Γ ⇒ T (b) : type then ML_{T} ⊢ Γ ⇒ b : U.

(f) If ML_{T} ⊢ Γ ⇒ A = B, then ML_{T} ⊢ Γ ⇒ A type, ML_{T} ⊢ Γ ⇒ B type.

(g) If ML_{T} ⊢ Γ, x : A, Γ ⇒ θ then ML_{T} ⊢ Γ ⇒ A type.

Note that (f) is trivial, but will be needed in the following as an additional premisse for the induction. Proof: We first change the calculus, treating A : type no longer as an abbreviation for A = A. (So we have additional rules, with the new statement A : type). Further we add all intensional rules, (ass defined in [TD88] or [Set93]) add the rules

(REP L1a) \frac{x:A,Γ′,Γ′′⇒B type ⇒t=t′:A}{Γ′[x/t],Γ′′[x/t′]⇒B[x/t′] type}  (ALP HA1) \frac{A type}{A′ type} if A=_{α}A′

(REF L) \frac{A type}{A=A}  \frac{t:A}{A type}

If for this calculus the theorem is provable, then this calculus is equivalent to the original: If we have a proof in the original calculus, then embed it into the calculus, by applying, whenever we need the removed rules the weak inferences. If we have a proof in the new calculus, the result is a proof in the original calculus, since we only added derived rules. Now the proof follows by induction on the length of the (new) derivation. The only difficult case is (SUB), where the difficulty are the the second conclusion in the cases (b): let the conclusion be for instance Γ, Γ′[x/t] ⇒ (Σx′ ∈ A.B)[x/t]. By IH Γ, Γ′, y : A′ ⇒ B′[x′/y] : type for y ∉ X, therefore Γ, Γ′[x/t], y : A′[x/t] ⇒ B′[x′/y][x/t] for x ≠ y, x ∉ X. (the substitution is allowed) Then for y ∉ X ∪{x}, if x = x′ or x ∉ F V (B) follows (Σx′ ∈ A.B)[x/t] = Σx′ ∈ A[x/t].B and we have the assertion, otherwise x′ ∉ F V (t) and B[x′/y][x/t] = B[x/t][x′/y]. Similarly we argue in (REP L), the other rules are easy.

Lemma 2.5 (a) ML_{1}^{e}W_{T,U} ⊢ Γ ⇒ r = s : U , then ML_{1}^{e}W_{T,U} ⊢ Γ ⇒ T (r) = μ(T (r)) and and ML_{1}^{e}W_{T,U} ⊢ Γ ⇒ T (s) = μ(T (s))

(b) ML_{1}^{e}W_{T,U} ⊢ Γ ⇒ A = B , then ML_{1}^{e}W_{T,U} ⊢ Γ ⇒ A = μ(A) and ML_{1}^{e}W_{T,U} ⊢ Γ ⇒ B = μ(B)

Proof: (a): Induction on the definition of r b-object. If for instance ML_{1}^{e}W_{T,U} ⊢ Γ ⇒ σx ∈ a.b : U, then by the additional rules of ML_{1}^{e}W_{T,U} follows Γ ⇒ a : Uand Γ, x : T (a) ⇒ b : U, by IH therefore Γ ⇒ T (a) = μ(T (a)), Γ, x : T (a) ⇒ T (b) = μ(T (b)), by extensional type introduction follows the assertion, similarly for the other terms, for which μ(T (t)) does something.

(b) Similar, using Lemma 2.4 instead of the new rules. Lemma 2.6 If ML_{1}^{e}W_{R,U} ⊢ Γ ⇒ θ then ML_{1}^{e}W_{T,U} ⊢ ρ(Γ) ⇒ ρ(θ). Especially, if Γ ⇒ θ is a statement of both ML_{1}^{e}W_{R,U} and ML_{1}^{e}W_{T,U}, then we have: If ML_{1}^{e}W_{R,U} ⊢ Γ ⇒ θ then ML_{1}^{e}W_{T,U} ⊢ Γ ⇒ θ. Proof: Induction on the derivation. In most rules, the assertion follows by the same rules. Difficult rules: (SUB), (REP L): Use 2.2 (d), 2.5 and 2.3. Equality rules and extensional equality rules: use for the substitution part the same argument. Second and third rule in (U^{I}): we conclude T (ψ(A)), and using 2.5 and an easy argument follows the assertion. Universe introduction rules (possibly extensional): easy.

Notation 2.7 In the followins we will write ML for ML_{1}^{e}W_{T,U}.

3 Definition of Kpi^{+}

We introduce now the Kripke-Platek set theory KP i^{+}, in which we will interpret afterwards ML. For more details on it, the reader should refer to [Bar75], [Jäg79], [Jäg83], [JP82], [Jäg86]and [Poh82]. Definition 3.1 Definition of Kripke-Platek set theory:

(a) Let L_{KP} be the classical first-order language, with terms being variables, atomic formulas being u ∈ v, ¬(u ∈ v), Ad(u), ¬Ad(u). The set of Variables should be V ar_{KP} = {u_{i}|i ∈ N} (a meta-set), u_{i} ≠ u_{j} for i ≠ j. The formulas are built from atomic formulas by ∧, ∨, ∀, ∃. We define ¬A by the deMorgan’s laws. The quantifier in ∀x.ϕ (∃x.ϕ) is bounded, if ϕ of the form x ∈ v → B (x ∈ v ∧ B) with x ≠ v. A Δ_{0}-formula is a formula with no unbounded quantifier. We abbreviate A → B :≡ ((¬A) ∨ B), ∀x ∈ v.B :≡ ∀x.x ∈ v → B, ∃x ∈ v.B :≡ ∃x.(x ∈ v ∧ B), (u = v) :≡ ((∀x ∈ u.x ∈ v) ∧ (∀x ∈ v.x ∈ u)), u ∉ v :≡ ¬(u ∈ v), tran(u) :≡ ∀x ∈ u.∀y ∈ x.y ∈ u, infinite(u) :≡ ∃x ∈ u.(x = x) ∧ ∀x ∈ u.∃y ∈ u.x ∈ y. Inacc(x) :≡ Ad(x) ∧ ∀y ∈ x.∃z ∈ x.y ∈ z ∧ Ad(z).

Inacc_{n}(x) :≡ ∃x_{0}, …, x_{n}.Inacc(x_{0})∧Ad(x_{1})∧Ad(x_{2})∧⋯∧Ad(x_{n})∧x_{0} ∈ x_{1} ∧x_{1} ∈ x_{2} ∧ ⋯ ∧ x_{n−1} ∈ x_{n} ∧ x = x_{n}.

ψ a formula, then ψ^{u} means the replacing of every unbounded quantifier ∀v by ∀v ∈ u and ∃v by ∃v ∈ u. Note, that Inacc(x) expresses, that x is an admissible, closed under admissibles, the ordinal of which is an inaccessible, and Inacc_{n}(x), that x is an admissible, which is at least the nth admissible above an x s.t. Inacc(x).

(b) Definition of axiom schemes:

(Ext) ∀x.∀y.∀z.x = y → (x ∈ z → y ∈ z) ∧ (Ad(x) → Ad(y))

(F ound) ∀z⃗.[∀x.(∀y ∈ x.ϕ(y, z⃗) → ϕ(x, z⃗)) → ∀x.ϕ(x, z⃗)] (ϕ an arbitrary formula )

(P air) ∀x.∀y.∃z.x ∈ z ∧ y ∈ z. (Union) ∀x.∃z.∀y ∈ x.∀u ∈ y.u ∈ z. (Δ_{0} − sep) ∀z⃗.∀w.∃y.[∀x ∈ y.(x ∈ w ∧ ϕ(x, z⃗)) ∧ ∀x ∈ w.ϕ(x, z⃗) → x ∈ y]

(ϕ a Δ_{0}-formula).

(Δ_{0} − coll) ∀z⃗.∀w.[∀x ∈ w.∃y.ϕ(x, y, z⃗) → ∃w′.∀x ∈ w.∃y ∈ w′.ϕ(x, y, z⃗)]

(ϕ a Δ_{0}-formula ). (Ad.1) ∀x.Ad(x) → tran(x) ∧ ∃w ∈ x.infinite(w). (Ad.2) ∀x.∀y.Ad(x) ∧ Ad(y) → x ∈ y ∨ x = y ∨ y ∈ x.

(Ad.3) ∀x.Ad(x) → ψ^{x},

(ψ an instance of (Pair), (Union), (Δ_{0}-sep), (Δ_{0}-coll) ).

(Lim) ∀x.∃y.Ad(y) ∧ x ∈ y. (inf) ∃x.infinite(x). (+_{n}) ∃x.Inacc_{n}(x).

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

Definition 3.2 (a) Ord is the class of ordinals.

(b) α(a) := ⋃(a ∩ Ord).

(c) Ad_{1} := ⋂{x|Ad(x)}, Ad_{2} := ⋂{x|Ad(x) ∧ Ad_{1} ∈ x}, Ad_{I} := ⋂{x|Inacc(x)}, Ad_{I,n} := ⋂{x|Inacc_{n}(x)}. Note, that Ad_{1}, Ad_{2}, Ad_{I}, Ad_{I,n} can be defined, since there exists b s.t. Ad(b) or Inacc(b) or Innacc_{n}(b), and therefore we can replace the class by {x η b ∪ {b}| ⋯}.

(d) Ω_{1} := α(Ad_{1}), I := α(Ad_{I}), I_{n} := α(Ad_{I,n}).

(e) ad(u) := ⋂({c ∈ Ad_{I}|Ad(c) ∧ u ∈ c} ∪ Ad_{I}), α^{+}(u) := α(ad(u)).

Remark 3.3 In KP i^{+} we have

(a) Ad(Ad_{1}), Ad(Ad_{2}), Inacc(I), Inacc_{n}(I_{n}).

(b) u ∈ Ad_{I} → ad(u) ∈ Ad_{I} ∧ Ad(ad(u)) ∧ u ∈ ad(u).

4 Interpretation of terms and types

A type A will be interpreted basically as a set of pairs of closed terms: < t, s >∈ A^{∗} should mean, that t and s are equal elements of this types. We will define A^{∗} as the set of terms, which are by an introductory rule elements of this type, and close it under the reduction rule. For instance, if A^{∗} and B^{∗} are already defined, then

(A + B)^{∗} := +^{∗}(A^{∗}, B^{∗})

where again

+^{∗}(u, v) = Compl(+^{basis}(u, v))
+^{basis}(u, v) := {< i(a), i(a′)| < a, a′ >∈ u} ∪ {< j(b), j(b′) > | < b, b′ >∈ v}
Compl(u) := {< r, s > |∃r′, s′. < r′, s′ >∈ u ∧ r→_{red}r′ ∧ s→_{red}s′}

Since we only want to interpret finitely many types, namely those types, which occurr in a certain derivation, we interpret dependent types as Σ-functions, the arguments of which are represented by the free variables of the type, in such a way, that A^{∗}[x_{1}/t_{1}, …, x_{n}/t_{n}] = (A[x_{1}/t_{1}, …, x_{n}/t_{n}])^{∗}. The Π-type has an introductory rule with a premisse, where dependency occurrs. The intended meaning of the premisse x : A ⇒ t = t′ : B is

∀r, r′. < r, r′ >∈ A^{∗} →< t[x/r], t′[x/r′] >∈ B^{∗}

Further we know

< r, r′ >∈ A^{∗} ⇒ B^{∗}[x/r] = B^{′∗}[x/r′]

Since we have to close it under α-conversion we can therefore define (Πx ∈ A.B)^{∗} := Π^{∗}(A^{∗}, (x)B^{∗}), where Π^{∗}(u, f) = Compl(Π^{basic}(u, f)) and

Π^{basis}(u, f) := {< λy.t, λy′.t′ > |∀ < r, r′ >∈ u. < t[y/r], t′[y′/r′] >∈ f(r)})

For technical reason will add the additional condition f(r) = f(r′). In order to make proofs about the terms easy, we will have deterministic reduction-rules. We will allow e.g. Ap(λx.r, s)→_{red}r[x/s] only, if s is in normal form. Further we donot allow any reductions of λx.r, so giving reduction rules generally only for closed terms This simple approach is possible, since, from the definition of (Πx ∈ A.B)^{∗}, we see, that, if < λx.t, λx.t >∈ (Πx ∈ A.B)^{∗}, and if t → t′ in a general sense for open terms, t[x/r]→_{red}t′[x/r] for closed terms r. But now, if B^{∗} is closed under →_{red}, we conclude < λx.t, λx.t′ >∈ (Πx ∈ A.B)∗. The interpretation of the W -type, which represents an inductive definition, is done in the usual way: we take some operator on sets and iterate it up to the closure ordinal, which is the next admissible above the components A and B of it. By the introduction rule, we get as the operator F such that

F_{W} (u, f)(v) = Compl({< sup(s, λy.t), sup(s′, λy′.t′) > | < s, s′ >∈ u
∧∀ < r, r′ >∈ f(s). < t[y/r], t′[y′/r′] ∈ v})

(W x ∈ A.B)^{∗} := F_{W}^{α} (A^{∗}, (x)B^{∗}). We can choose as α any admissible ordinal s.t. A^{∗} and (x)B^{∗} are elements of L_{α}. We will take as α I_{n}, the nth admissible above I, and n is the maximum of level(A) and level(B), which is the number of nestings of W -types in A and B. Although this ordinal is usually too big, it suffices for our construction. In the introduction rules for the elements of the universe, e.g.

(π^{I})  \frac{a∈U x∈T (a)⇒b∈U}{πx∈a.b:U}

we introduce simultaneously the elements a of the universe and its interpretation T (a) as a type. We will therefore first define a set Û of tripels < a, A, b >, where a and b are terms, considered as equal elements of the universe, such that T (a)^{∗} = T (b)^{∗} = A. Therefore

U^{∗} = {< a, b > |∃A. < a, A, b >∈ Û}

and T (a)^{∗} = f(a), where

f = {< a, A > |∃b. < a, A, b >∈ Û}

Û is again the fixed point of an operator Ũ, so Û = Ũ^{α} for some admissible α. Since U is closed under the W -type, in the definition of Ũ we need to go to the next admissible, α must be closed under the step to the next admissible, I is a recursive inaccessible, an admissible closed under admissibles. Here we see, why we need the theory KP i^{+}: We need, one admissible, closed under admissibles, and ω many admissibles above it. We want to interpret an intuitionistic theory in a classical one, using some realization. Now if we have a realization interpretation as indices for recursive functions and there is naturally a very easy realization of ¬∀x.∃y.ϕ(x, y), if ∀x.∃y.ϕ(x, y) is arithmetical formula, such that the y is not recursive in x, then we have an obvious realization: every term λx.t does it — there is no realization of ∀x.∃y.ϕ(x, y). Therefore there are false recursive realizations. But proof carried out in an intuitionistic theory like Martin-Löf Type Theory should not prove false statements. The reason, why it oes it not prove any, is, that we can apply the realizing termλu.s of ¬∀x.∃y.ϕ(x, y), in some sense to non intuitionistic proofs as well. We can add a constructor, which has a non recursive reduction rule, and gives us the y depending on the x, then we have a realizing term t for ∀x.∃y.ϕ(x, y), and can apply any proof λu.s of ¬∀x.∃y.ϕ(x, y) to it to get an element of type ⊥ which is empty. Therefore, adding non recursive constructors, we can achieve, that there is no realizing term for a false formula. We want to extend our result even for Π_{1}^{1}-sentences. Here again we have the problem, that the powerset of the natural numbers, N → U, does not represent all sets in KP i^{+}. We will not be able to get a result, where we conclude from ML∀X ∈ (N → U).ϕ(X), that KP i^{+} ⊢ ∀x.x ⊂ ω → ϕ′(x) for the translation ϕ′ of ϕ, but only, if we have, that x is an element of the first admissible. (We could easily extend it for x being an element of the first recursive inaccessibel admissible without any trouble, but the result is enough to get an upper bound for the provable proof theoretical strength).) Anyway, this text serves only to motivate the introduction of non recursive constructors. We have to quantify over all possible choices of new constructors. We will have either constructors, that give as a natural number (functions ω^{l} → ω for some l), or functions, that gives us an element of the universe, in order to get elements of the powerset of N, but we only need the elements \underline{n}_{0} (for is not element) and \underline{n}_{1} (for is an element).

Definition 4.1 (a) We assume, that we have chosen some Gödel-numbers ⌈S⌉ for all symbols S of ML.

(b) A tripel < C, l, f > is a constructor definition, if C, l are natural numbers (C is a Gödel number for the constructor), such that C is different from the Gödel-numbers for the symbols, l > 0 and f is a function f : ω^{l−1} → ω or l = 0 ∧ f : ω → \{⌈\underline{n}_{0}⌉, ⌈\underline{n}_{1}⌉\}. In this situation we define arity(C) := max\{l, 1\}.

(c) A constructor extension set is a finite set of constructor definitions, such that the Gödel-numbers for the constructors are different. We write CES(a_{0}) for a_{0} being a constructor extension set and a_{0} ∈ Ad_{2}.

(d) The a_{0}-extended g-terms, g-types, b-objects are defined as the g-terms, g-types, bobjects, but having on arity(C) term constructor for each element < C, l, f > of a_{0}. T erm_{Cl,a_{0}} is the set of closed a_{0}-extended t-terms.

(e) ∀CES(a_{0}).ϕ(a_{0}) :≡ ∀a_{0} ∈ Ad_{2}.CES(a_{0}) → ϕ(a_{0}) Assumption 4.2 As long as there is no other CES mentioned, let a_{0} be a CES s.t. a_{0} ∈ Ad_{2}. Most of the next definitions will depend on a_{0}, which we will not mention in the following. If we have to mention it, we will add it as a subscript. Definition 4.3 (a) We choose some Gödelization of a_{0}-extended b-terms, but will omit

the Gödel-brackets.

(b) The introductory term constructors are the term constructors 0, \underline{r}, \underline{n}, S, i, j, p, sup, ˜+, π, σ, w, ĩ and for k ∈ ω, \underline{n}_{k}.

(c) Let →_{red,imm}_{a_{0}} or short →_{red,imm} be the relation between closed a_{0}-extended g-terms, defined by

p_{0}(p(r, s))→_{red,imm}r  p_{1}(p(r, s))→_{red,imm}s
Ap(λx.r, s)→_{red,imm}r[x/s]  C_{n}(i_{n}, r_{1}, …, r_{n})→_{red,imm}r_{i}
D(i(r), s, t)→_{red,imm}sr  D(j(r), s, t)→_{red,imm}tr
P (0, s, t)→_{red,imm}s  P (Sr, s, t)→_{red,imm}(trP (r, s, t))

(note that we write rs for Ap(r, s)), R(sup(r, s), t)→_{red,imm}(trs(λz_{i}.R(sz_{i}, t))), where i is minimal such that z_{i} ∉ F V (s) ∪ F V (t) C(S^{n_{1}}0, …, S^{n_{l}}0)→_{red,imm}_{a_{0}}S^{f(n_{1},...,n_{l})}0, (if < C, l + 1, f >∈ a_{0}), C(S^{n}0)→_{red,imm}_{a_{0}}g(n) (if < C, 0, f >∈ a_{0}, and f : ω → \{\underline{n}_{0}, \underline{n}_{1}\})

(d) We define inductively a set of (indices for) terms in normal-form T erm_{nf}, a subset of the closed a_{0}-extended g-terms: If C is an introductory n-ary term constructor, t_{1}, …, t_{n} ∈ T erm_{nf}, then C(t_{1}, …, t_{n}) ∈ T erm_{nf}. If C is a n-ary term constructor (possibly an extended term constructor) that is not introductory, t_{1}, …, t_{n} ∈ T erm_{nf}, and there exists no t such that C(t_{1}, …, t_{n})→_{red,imm}t, then C(t_{1}, …, t_{n}) ∈ T erm_{nf}. If t ∈ T erm, x ∈ V ar_{ML}, F V (t) ⊂ {x}, then λx.t ∈ T erm_{nf}.

(e) We define for a_{0}-extended g-terms t, the next reduced term t^{red}.

For t ∈ T erm_{nf}. t^{red} := t. If C is a n-ary (possibly extended) term constructor, r_{i} ∈ T erm_{Cl}, ∃i.r_{i} ∉ T erm_{nf}, then C(r_{1}, …, r_{n})^{red} := C(r_{1}^{red}, …, r_{n}^{red}). If t := C(r_{1}, …, r_{n}) ∉ T erm_{nf}, r_{i} ∈ T erm_{nf}, then t→_{red,imm}t′ for some t′, t^{red} := t′.

We define r →_{red} s iff there exists a sequence < s_{0}, …, s_{n} > such that r = s_{0}, s = s_{n} and ∀i < n.s_{i+1} = (s_{i})^{red}.

Lemma 4.4 (a) KP i^{+} ⊢ ∀r, s, s′ ∈ T erm_{Cl}.(r→_{red}s ∧ r→_{red}s′) → (s→_{red}s′ ∨ s′→_{red}s).

(b) KP i^{+} ⊢ ∀r, s, s′ ∈ T erm_{Cl}.(r→_{red}s ∧ r→_{red}s′ ∧ s, s′ ∈ T erm_{nf}) → s = s′.

(c) If C is a n-ary constructor, then

KP i^{+} ⊢ ∀r_{1}, …, r_{n}, r′_{1}, …, r′_{n}.(r_{1}→_{red}r′_{1} ∈ T erm_{nf} ∧ ⋯ ∧ r_{n}→_{red}r′_{n} ∈ T erm_{nf})
→ (C(r_{1}, …, r_{n})→_{red}C(r′_{1}, …, r′_{n}))

(d) KP i^{+} ⊢ ∀t, t′, s ∈ T erm_{Cl}.(t→_{red}s ∧ t=_{α}t′) → ∃s′ ∈ T erm_{Cl}.t′→_{red}s′ ∧ s=_{α}s′.

(e) KP i^{+} ⊢ ∀t, t′ ∈ T erm_{Cl}.t=_{α}t′ → (t ∈ T erm_{nf} ↔ t′ ∈ T erm_{nf}). Definition 4.5 If F is a Σ function, we define by recursion on α ∈ Ord

F^{α} := \{ \begin{matrix}∅ & if α = 0, \\ F (F^{β}) & if α = β + 1, \\ ⋃_{β<α,β∈Ord} F^{β} & if α ∈Lim. \end{matrix}

Definition 4.6 (a) Let Compl be the Σ-function

Compl(u) := {< r, s >∈ T erm_{cl} × T erm_{cl}|∃r′, s′ ∈ T erm_{a,nf}.
r→_{red}r′ ∧ s→_{red}_{a}s′∧ < r′, s′ >∈ u}

(b) N_{k}^{basis} := {< n_{k}, n_{k} > |n < k}, N_{k}^{∗∗} := Compl(N_{k}^{basis}), which are Σ-functions, depending on the parameter k.

(c) N^{basis} := {< S^{n}0, S^{n}0 > |n < ω}, N_{k}^{∗∗} := Compl(N^{basis}). (d)

Π^{basis}(u, f) := {< λx.s, λx′.s′ >∈ T erm_{nf} × T erm_{nf}|
∀ < r, r′ >∈ u. < s[x/r], s′[x′/r′] >∈ f(r) ∧ f(r) = f(r′)}

(more precisely we have to write:

Π^{∗}(u, f) := {< t, t′ >∈ T erm_{nf} × T erm_{nf}|
∃x, x′ ∈ V ar_{ML}, r, r′ ∈ T erm.t = λx.s ∧ t′ = λx′.s′ ∧
∀r, r′ ∈ T erm_{Cl}. < r, r′ >∈ u →
< s[x/r], s[x′/r′] >∈ f(r) ∧ f(r) = f(r′)}

similarly in the following definitions) Π^{∗}(u, f) := Compl(Π^{basis}(u, f)).

(e)

Σ^{basis}(u, f) := {< p(r, s), p(r′, s′) >∈ T erm_{nf} × T erm_{nf}|
< r, r′ >∈ u∧ < s, s′ >∈ f(r) ∧ f(r) = f(r′)}

Σ^{∗}(u, f) := Compl(Σ^{basis}(u, f)).

(f) Let λ^{∗}(u) := {< t, u > |t ∈ T erm_{Cl}}.

(g) W^{∗}(u, f, α) := F_{W} (u, f)^{α}, where F_{W} (u, f)(v) = Compl(F_{W}^{basis}(u, f)(v)), and

F_{W}^{basis}(u, f)(v) := {< sup(r, s), sup(r′, s′) >∈ T erm_{nf} × T erm_{nf}|

< r, r′ >∈ u∧ < s, s′ >∈ Π^{basis}(f(r), λ^{∗}(v)) ∧ f(r) = f(r′)} (h)

+^{basis}(u, v) :=  {< i(r), i(r′) >∈ T erm_{nf} × T erm_{nf}| < r, r′ >∈ u}
∪ {< j(r), j(r′) >∈ T erm_{nf} × T erm_{nf}| < r, r′ >∈ v}

+^{∗}(u, v) := Compl(+^{basis}(u, v)).

(i)

i^{basis}(u, s, t) := \{< \underline{r}, \underline{r} >∈ T erm_{nf} × T erm_{nf}| < s, t >∈ u\}

i^{∗}(u, s, t,) := Compl(i^{basis}(u, s, t)).

We will interpret each g-type occurring in a proof of Martin-Löf’s type theory as Σfunctions, with arguments represented by the free variables of the type. More precisely, if F V (A) = {z_{1}, …, z_{n}}, (z_{i} as in the definition 1.1 of V ar_{ML}) the arguments of the interpretation A^{∗} will have arguments given by the variables {u_{1}, …, u_{n}} (u_{i} as in definition 3.1 (a) of V ar_{KP}). We introduce the following abbreviation: Definition 4.7 (a) If A is a Σ function in KP i^{+}, u_{i} as in the definition 3.1 (a) of

V ar_{KP} z_{i} as in the definition 1.1 of V ar_{ML}, r_{1}, …, r_{m} extended b-objects,

A[z_{i_{1}}/r_{1}, …, z_{i_{n}}/r_{n}] := A[u_{i_{1}}/r_{j_{1}}, …, u_{i_{n}}/r_{j_{n}}],

where on the right-hand side we have the real substitution in KP i^{+} in such a way, that, if a variable occurrs more than once, only the first occurrence is carried out. If we introducing symbols for Σ-functions, this substitution is the application of the Σ-function to the arguments in the ordering as specified by the definition of the function. We will write A[x⃗/n⃗] for A[x_{1}/n_{1}, …, x_{n}/n_{n}].

(b) In the situation as above let (z_{i})A be the Σ-function with the same arguments as A except u_{i} s.t. ((z_{i})A)[x⃗/r⃗] = {< u, A[z_{i}/u, x⃗/r⃗] > |u ∈ T erm_{Cl}}.

Definition 4.8 We define for every g-type A the Sigma-function A^{∗} together with level(A) ∈ ω. If F V (A) = {z_{1}, …, z_{n}}, (z_{i} as in definition 1.1 of V ar_{ML}), A^{∗} will have arguments given by the variables {u_{1}, …, u_{n}} (u_{i} as in defition 3.1 (a) of V ar_{KP}). We will define it by giving the values A^{∗}[x⃗/s⃗]. Additionally we define lev(A) ∈ ω. For k ∈ ω, N_{k}^{∗}[ ] := N_{k}^{∗∗}, lev(N_{k}) := 0.

N^{∗}[ ] := N^{∗∗}, lev(N) := 0. Let A, B be g-types, m := max{lev(A), lev(B)}. lev(Πx ∈ A.B) := m, (Πx ∈ A.B)^{∗}[x⃗/s⃗] := Π^{∗}(A^{∗}[x⃗/s⃗], (x)B^{∗}[x⃗/s⃗]), lev(Σx ∈ A.B) := m, (Σx ∈ A.B)^{∗}[x⃗/s⃗] := Σ^{∗}(A^{∗}[x⃗/s⃗], (x)B^{∗}[x⃗/s⃗]), lev(W x ∈ A.B) := m + 1, (W x ∈ A.B)^{∗}[x⃗/s⃗] := W^{∗}(A^{∗}[x⃗/s⃗], (x)B^{∗}[x⃗/s⃗], I_{m}), lev(A + B) := m, (A + B)^{∗}[x⃗/s⃗] := +^{∗}(A^{∗}[x⃗/s⃗], B^{∗}[x⃗/s⃗]), lev(I(A, s, t)) := level(A), (I(A, s, t))^{∗}[x⃗/s⃗] := I^{∗}(A^{∗}[x⃗/s⃗], s[x⃗/s⃗], t[x⃗/s⃗]). lev(U) := 1, U^{∗}[ ] :=∼ (Û), lev(T (t)) := 0, (T (t))^{∗}[x⃗/s⃗] := func(Û)(t[x⃗/s⃗]), where Û, ∼ (u), func(u) will be defined in the next definition. Definition 4.9 (a) ∼ (u) := {< s, s′ >∈ T erm_{Cl} × T erm_{Cl}|∃v ∈ T C(u). < s, v, s′ >∈

u}.

(b) func(u) := {< s, v >∈ T erm_{Cl} × T C(u)|∃s′ ∈ T erm_{Cl}. < s, v, s′ >∈ u}.

(c) Compl_{U}(u) := {< r, b, r′ >∈ T erm_{Cl} × T C(u) × T erm_{Cl}|∃s, s′ ∈ T erm_{nf}. r→_{red}s ∧ r′→_{red}s′∧ < s, b, s′ >∈ u}.

(d) Ũ(u) := Compl_{U}(Ũ^{basis}(u)), where

Ũ^{basis}(u) :=
\{< \underline{n}_{k}, N_{k}^{∗∗}, \underline{n}_{k} >∈ ad(u)|k ∈ ω\}
∪ \{< \underline{n}, N^{∗∗}, \underline{n} >\}
∪ {< πx ∈ r.s, Π^{∗}(b, f), πx′ ∈ r′.s′ > |ϕ(r, x, s, r′, x′, s′, b, f, u) ∧ b, f ∈ ad(u)}
∪ {< σx ∈ r.s, Σ^{∗}(b, f), σx′ ∈ r′.s′ > |ϕ(r, x, s, r′, x′, s′, b, f, u) ∧ b, f ∈ ad(u)}
∪ {< wx ∈ r.s, W^{∗}(b, f, α^{+}(u)), wx′ ∈ r′.s′ > |
ϕ(r, x, s, r′, x′, s′, b, f, u) ∧ b, f ∈ ad(u)}
∪ {< r ˜+s, +^{∗}(b, c), r′ ˜+s′ >∈ ad(u)|ψ_{+}(r, s, r′, s′, b, c, u) ∧ b, c ∈ ad(u)}
∪ {< ĩ(r, s, t), I^{∗}(b, s, t), ĩ(r′, s′, t′) >∈ ad(u)|ψ_{i}(r, s, t, r′, s′, t′, b, u) ∧ b ∈ ad(u)}

and

ϕ( r, x , s, r′, x′, s′, b, f, u)
:= r, r′ ∈ T erm_{nf} ∧ s, s′ ∈ T erm
∧F V (s) ⊂ {x} ∧ F V (s′) ⊂ {x′}∧ < r, b, r′ >∈ u ∧
(∀ < t, t′ >∈ b. < s[x/t], f(t), s′[x′/t′] >∈ u)

(note that f(t) = ⋃{c ∈ T C(f)| < t, c >∈ f})

ψ_{+}(r, s, r′, s′, b, c, u) := r, s, r′, s′ ∈ T erm_{nf}∧ < r, b, r′ >∈ u∧ < s, c, s′ >∈ u,

ψ_{i}(r, s, t, r′, s′, t′, b, u) := r, s, t, r′, s′, t′ ∈ T erm_{nf}∧ < r, b, r′ >∈ u ∧
< s, s′ >∈ b∧ < t, t′ >∈ b,

(e) Û := Ũ^{I}.

5 Properties of the interpretation

Lemma 5.1 (a) ∀v ⊂ v′.F_{W}^{∗} (b, f)(v) ⊂ F_{W}^{∗} (b, f)(v′).

(b) ∀γ < δ.W^{∗}(b, f, γ) ⊂ W^{∗}(b, f, δ)

(c) (b ∈ a ∧ f ∈ a ∧ Ad(a)) → ∀γ > α(a).W^{∗}(b, f, γ) = W^{∗}(b, f, α(a)). Proof: (a) immediate, (b) follows from (a) by induction on δ.

(c) It is sufficient to show, with α := α(u), v := W^{∗}(b, f, α), that F_{W} (b, f)(v) ⊂ v. Since Compl(v) ⊂ v it is sufficient to prove F_{W}^{basis}(b, f)(v) ⊂ v). Now, if < sup(r, t), sup(r′, t′) >∈ F_{W}^{basis}(b, f)(v), then t = λx.s, t′ = λx′.s′, and ∀u, u′ ∈ T erm_{Cl}. < u, u′ >∈ f(r) → ∃δ ∈ Ord ∩ α. < s[x/u], s′[x′/u′] >∈ W^{∗}(b, f, δ) Since Ad(a), we have (Δ_{0} − coll)^{a}, therefore for some ρ < α, ∀t, t′ ∈ T erm_{Cl}. < t, t′ >∈ f(r) → ∃δ < ρ. < s[x/t], s′[x′/t′] >∈ W^{∗}(b, f, δ). Now follows < sup(r, λx.s), sup(r′, λx′.s′) >∈ W^{∗}(b, f, ρ) ⊂ v and the assertion.

Definition 5.2 (a) equiv(u) :⇔ ∀r, s, t, r′, s′ ∈ T erm_{Cl}.(< r, s >∈ u →< s, r >∈ u)∧ ((< r, s >∈ u∧ < s, t >∈ u) →< r, t >∈ u).

(note that we do not claim reflexivity)

(b) equivfun(f) :⇔ ∀x ∈ dom(f).equiv(f(x)).

(c) Cor(u) :⇔

∀r, r′, r′′ ∈ T erm_{Cl}.∀b, b′.(< r, b, r′ >∈ u → [< r′, b, r >∈ u ∧ equiv(b)

∧[< r′, b′, r′′ >∈ u → (< r, b, r′′ >∈ u ∧ b = b′ >]])

Remark 5.3 (a) (Cor(u)∧ < r, b, r′ >∈ u∧ < r, b′, r′′ >∈ u) → (b = b′∧ < r, b, r′′ >∈ u).

(b) If Cor(u) then with ∼:=∼ (u), f := func(u) we have ∼ is a symmetric and transitive relation, f is a function s.t. ∀a, b.a ∼ b → f(a) = f(b) and equivfun(f).

Lemma 5.4 (a) (equiv(u) ∧ u ⊂ T erm_{nf} × T erm_{nf}) → equiv(Compl(u)).

(b) (equiv(u) ∧ equiv(v) ∧ equivfun(f) ∧ k ∈ ω ∧ s, t ∈ T erm_{Cl}) →

(equiv(N^{basis}) ∧ equiv(N_{k}^{basis}) ∧ equiv(Π^{basis}(u, f)) ∧ equiv(Σ^{basis}(u, f)) ∧ equiv(F_{W}^{basis}(u, f)(v)) ∧ equiv(+^{basis}(u, v)) ∧ equiv(i^{basis}(u, s, t))).

(c) (equiv(u) ∧ equiv(v) ∧ equivfun(f) ∧ α ∈ Ord ∧ k ∈ ω ∧ s, t ∈ T erm_{Cl}) →

(equiv(N^{∗})∧equiv(N_{k}^{∗})∧equiv(Π^{∗}(u, f))∧equiv(Σ^{∗}(u, f))∧equiv(F_{W}^{∗} (u, f)(v))∧

equiv(W^{∗}(u, f, α)) ∧ equiv(+^{∗}(u, v)) ∧ equiv(i^{∗}(u, s, t))).

Lemma 5.5 Assume r, s, t, r′, s′, t′ ∈ T erm, x, x′ ∈ V ar_{ML}, b, f, u sets.

(a) (ϕ(r, x, s, r′, x′, s′, b, f, u) ∧ Cor(u)) → (b ∈ ad(u) ∧ ∃f ∈ ad(u).∀ < t, t′ >∈ b.f(t) = f(t′) = f′(t) = f′(t′)).

(b) ψ_{+}(r, s, r′, s′, b, c, u) → b, c ∈ ad(u).

(c) ψ_{i}(r, s, t, r′, s′, t′, b, u) → b ∈ ad(u).

(d) Cor(u) → Ũ(u) ∈ ad(ad(u)).

(e) ∀γ ∈ Ord ∩ I.Ũ^{γ} ∈ Ad_{I}.

Proof:

(a) b ∈ T C(u) ∈ ad(u). Let f′ := {< t, c >∈ T erm_{Cl} × T C(u)| < t, t >∈ b∧ < s[x/t], c, s[x/t] >∈ u}. f′ ∈ ad(u). Further, if < t, t′ >∈ b follows < s[x/t], f(t), s′[x/t′] >∈ u, by Cor(u) < s[x/t], f(t), s[x/t] >∈ u, f(t) = f′(t), and, since < s′[x/t], f(t), s[x/t] >∈ u∧ < s′[x/t], f(t′), s[x/t′] >∈ u follows f(t) = f(t′). (b), (c),(d): easy. (e): Induction on γ, using (d) and 3.3 (b). Lemma 5.6 Assume r, s, t, r′, s′, t′, r′′, s′′, t′′ ∈ T erm, x, x′, x′′ ∈ V ar_{ML}, b, b′, f, f′, u, u′ sets.

(a) ϕ(r, x, s, r′, x′, s′, b, f, u) → Cor(u) → ϕ(r′, x′, s′, r, x, s, b, f, u).

(b) (ϕ(r, x, s, r′, x′, s′, b, f, u) ∧ ϕ(r′, x′, s′, r′′, x′′, s′′, b′, f′, u′) ∧ Cor(u ∪ u′)) → ϕ(r, x, s, r′′, x′′, s′′, b, f, u ∪ u′) ∧ b = b′∧ ∀ < t, t′ >∈ b.f(t) = f′(t) = f(t′) = f′(t′)

(c) ψ_{+}(r, s, r′, s′, b, c, u) → Cor(u) → ψ_{+}(r′, s′, r, s, b, c, u).

(d) (ψ_{+}(r, s, r′, s′, b, c, u) ∧ ψ_{+}(r′, s′, r′′, s′′, b′, c′, u′) ∧ Cor(u ∪ u′) → (ψ_{+}(r, s, r′′, s′′, b, c, u ∪ u′) ∧ b = b′ ∧ c = c′))

(e) ψ_{i}(r, s, t, r′, s′, t′, b, u) → Cor(u) → ψ_{i}(r′, s′, t′, r, s, t, b, u).

(f) (ψ_{i}(r, s, t, r′, s′, t′, b, u) ∧ ψ_{i}(r′, s′, t′, r′′, s′′, t′′, b′, u′) ∧ Cor(u ∪ u′) → (ψ_{i}(r, s, t, r′′, s′′, t′′, b, u ∪ u′) ∧ b = b′))

Lemma 5.7 (a) (Cor(u)∧ ∼ (u) ⊂ T erm_{nf} × T erm_{nf}) → Cor(Compl_{U}(u)).

(b) Cor(u) → Cor(Ũ(u)),

(c) u ⊂ u′ ∧ Cor(u′) → Ũ(u) ⊂ Ũ(u′),

(d) Cor(Û). Lemma 5.8 If A g-type, then KP i^{+} ⊢ ∀s_{1}, …, s_{n} ∈ T erm_{Cl}.equiv(A^{∗}[x⃗/s⃗]) Proof: Induction on the definition of types. Definition 5.9 Let A, B g-types, s, t g-terms, F V (A), F V (B), F V (s), F V (t) ⊂ {x_{1}, …, x_{n}}, r_{1}, …, r_{n}, s_{1}, , …, s_{n} be extended g-terms.

(a) (A = B)^{∗}[x⃗/r⃗; s⃗] :⇔ (A = B)^{∗}[x_{1}/r_{1}; s_{1}, …, x_{n}/r_{n}; s_{n}] :⇔ (A^{∗}[x⃗/r⃗] = B^{∗}[x⃗/s⃗]).

(b) (t = t′ : A)^{∗}[x⃗/r⃗; s⃗] :⇔ (t = t′ : A)^{∗}[x_{1}/r_{1}; s_{1}, …, x_{n}/r_{n}; s_{n}] :⇔ < t[x⃗/r⃗], t′[x⃗/s⃗] >∈ A^{∗}[x⃗/r⃗].

We will not mention the variables x_{1}, …, x_{n} explicitly, if they are the variables, mentioned in the context, writing (A = B)^{∗}[r⃗; s⃗] and (t = t′ : A)^{∗}[r⃗; s⃗]. Note that s : A, A type abbreviate s = s : A, A = A, therefore (s : A)^{∗}[r⃗; s⃗], (A type)^{∗}[r⃗; s⃗] are defined as well. Lemma 5.10 (Substitution lemma). Let C, D be g-types, r, s, t_{i}, t′_{i} g-terms, x_{i}, y_{i} ∈ V ar_{ML}. Then:

(a) If r[x⃗/t⃗] is an allowed substitution, F V (r[x⃗/t⃗]) ⊂ {y_{1}, …, y_{n}}, then KP i^{+} ⊢ ∀r⃗ ∈ T erm_{Cl}.r[x⃗/t⃗][y⃗/r⃗] = r[x_{1}/t_{1}[y⃗/r⃗], …, x_{n}/t_{n}[y⃗/r⃗], y⃗/r⃗]. (Note that, if variables occur more than once in [y⃗/r⃗], only the first substitution is relevant.)

(b) If C[x⃗/t⃗] is an allowed substitution, F V (C[x⃗/t⃗]) ⊂ {y_{1}, …, y_{n}}, then KP i^{+} ⊢ ∀r⃗, r′ ∈ T erm_{Cl}.C[x⃗/t⃗]^{∗}[y⃗/r⃗] = C^{∗}[x_{1}/t_{1}[y⃗/r⃗], …, x_{n}/t_{n}[y⃗/r⃗], y⃗/r⃗].

(c) If A[x⃗/t⃗], B[x⃗/t⃗′] are allowed substitutions, F V (A[x⃗/t⃗]), F V (B[x⃗/t⃗′]) ⊂ {y_{1}, …, y_{n}}, then KP i^{+} ⊢ ∀r⃗, s⃗ ∈ T erm_{Cl}.(A = B)^{∗}[x⃗/(t⃗[y⃗/r⃗]); (t⃗′[y⃗/s⃗]), y⃗/r⃗; s⃗] ↔

(A[x⃗/t⃗] = B[x⃗/t⃗′])^{∗}[y⃗/r⃗; s⃗].

(d) If A[x⃗/t⃗], r[x⃗/t⃗] are allowed substitutions, F V (A[x⃗/t⃗]), F V (r[x⃗/t⃗]) ⊂ {y_{1}, …, y_{n}}, then KP i^{+} ⊢ ∀r⃗, s⃗ ∈ T erm_{Cl}.(r : A)^{∗}[x⃗/(t⃗[x⃗/r⃗]); (t⃗[x⃗/s⃗]), x⃗/r⃗; s⃗] ↔

(r[x/t] : A[x/t])^{∗}[x⃗/r⃗; s⃗].

(e) If A[x⃗/t⃗], r[x⃗/t⃗], s[x⃗/t⃗′] are allowed substitutions, F V (A[x⃗/t⃗]), F V (r[x⃗/t⃗]), F V (s[x⃗/t⃗′]) ⊂ {y_{1}, …, y_{n}}, then KP i^{+} ⊢ ∀r⃗, s⃗ ∈ T erm_{Cl}.(r = s : A)^{∗}[x⃗/(t⃗[x⃗/r⃗]); (t⃗′[x⃗/s⃗]), x⃗/r⃗; s⃗] ↔ (r[x⃗/t⃗] = s[x/t⃗′] : A[x/t⃗])^{∗}[x⃗/r⃗; s⃗].

Proof by induction on the definition of the terms and types. Lemma 5.11 For every g-type A F V (A) ⊂ {x_{1}, …, x_{n}}, follows

(a) ∀r⃗, r, r′, s, s′ ∈ T erm_{Cl}.(r→_{red}r′) → (s→_{red}s′) →< r, s >∈ A^{∗}[x⃗/r⃗] →< r′, s′ >∈ A^{∗}[x⃗/r⃗].

(b) ∀r⃗, r, r′ ∈ T erm_{Cl}. < r, r′ >∈ A^{∗}[x⃗/r⃗] → ∃s, s′ ∈ T erm_{nf}.r→_{red}s ∧ r′→_{red}s′. Proof: easy, since for each type, Compl was applied to some set. Definition 5.12 (a) Stable(a) := ∀r, s, r′, s′ ∈ T erm_{Cl}. < r, s >∈ a → r=_{α}r′ →

s=_{α}s′ →< r′, s′ >∈ a

(b) For every g-type A with F V (A) = {x_{1}, …, x_{n}} we define

F lex(A) := ∀r_{1}, …, r_{n}, s_{1}, …, s_{n} ∈ T erm_{Cl}.v(r_{1}=_{α}s_{1} ∧ ⋯ ∧ r_{n}=_{α}s_{n}) →

A^{∗}[x⃗/r⃗] = A^{∗}[x⃗/s⃗]

Lemma 5.13 For every g-type C, D with F V (C) = {x_{1}, …, x_{n}} and C=_{α}D we have (a) KP i^{+} ⊢ F lex(C)

(b) KP i^{+} ⊢ ∀r_{1}, …, r_{n} ∈ T erm_{Cl}.Stable(C^{∗}[x⃗/r⃗])

(c) KP i^{+} ⊢ ∀r_{1}, …, r_{n} ∈ T erm_{Cl}.C^{∗}[x⃗/r⃗] = D^{∗}[x⃗/r⃗]. Proof Easy, simultaneously by induction on the definition of g-types. In the case C ≡ U, T (t) we define

Stable_{U}(u) := ∀s, s′, t, t′ ∈ T erm_{Cl}.∀b ∈ T C(u).
s=_{α}s′ → t=_{α}t′ → pair(s, b, t) ∈ u → (pair(s′, b, t′) ∈ u ∧ Stable(b))

easily conclude Stable_{U}(u) → Stable_{U}(Ũ(u)) and therefore Stable_{U}(Û), and are now able to prove easily the assertion. In order to state our Main Lemma, we need to express, that, if we assume elements of the types of the context, the interpretation of the conclusion Θ of a statement of Martin-Löf is valid. Since we need, that this is independent of the choice of equal elements of A_{i}, we will introduce the following abbreviation: Definition 5.14 Let Γ ≡ x_{1} : A_{1}, …, x_{k} : A_{k} be a g-context.

∀Γ^{=}(r⃗; s⃗).ϕ :≡ ∀r_{1}, …, r_{k}, s_{1}, …, s_{k} ∈ T erm_{Cl}.(< r_{1}, s_{1} >∈ A_{1}^{∗}[ ] ∧

< r_{2}, s_{2} >∈ A_{2}^{∗}[x_{1}/r_{1}] ∧ ⋯ ∧ < r_{k}, s_{k} >∈ A_{k}^{∗}[x_{1}/r_{1}, …, x_{k−1}/r_{k−1}]) → ϕ

“Assume Γ^{=}(r⃗; s⃗)” means: “Assume r_{1}, …, r_{k}, s_{1}, …, s_{k} ∈ T erm_{Cl} such that < r_{1}, s_{1} >∈ A_{1}^{∗}[ ]∧

< r_{2}, s_{2} >∈ A_{2}^{∗}[x_{1}/r_{1}] ∧ ⋯ ∧ < r_{k}, s_{k} >∈ A_{k}^{∗}[x_{1}/r_{1}, …, x_{k−1}/r_{k−1}].

6 Main Lemma

In this section we prove the Main Lemma, which expresses that if ML ⊢ r : A, then KP i^{+} ⊢< r, r >∈ A^{∗}. We have to go through all statements. Lemma 6.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 g-judge-ment. Assume Γ = x_{1} : A_{1}, …, x_{n} : A_{n}.

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

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

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

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

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

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

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

Proof of the Main Lemma: We proof simultaneously (a) - (c) by induction on the derivation. We write IH 3 for the Induction-hypothesis for the 3rd premise, etc. IH 3(c) for the Induction-hypothesis (c) for the 3rd premise of the rule etc. If there is more than one rule of one category (as in the case of (REF L) ), we refer to them by (REF L)_{1}, (REF L)_{2}, etc. Let Γ = x_{1} : A_{1}, …, x_{n} : A_{n}, Γ′ = y_{1} : B_{1}, …, y_{m} : B_{m}. If r⃗ = r_{1}, …, r_{n}, i ≤ n, then r̂_{i} := r_{1}, …, r_{i−1} (r̂_{1} is empty). If θ is t = t′ : A or A = B, let θ′ = A type (the judgement treated in the cases (i) of (a),(b), or which follows from the assertion in (c). Distinction by the last rule applied. Assume that lemma is proved for the premisses of a rule, as stated in the definition, weakened by the context Γ. We treat only some examples of the rules, covering the more complicated ones. Case (SY M)_{1} Assume Γ^{=}(r⃗; s⃗). From < r_{i}, s_{i} >∈ A_{i}^{∗}[r̂_{i}] follows < s_{i}, r_{i} >∈ A_{i}^{∗}[r̂_{i}] and by IH (a,ii) < s_{i}, r_{i} >∈ A_{i}^{∗}[ŝ_{i}]. By IH (a,i) follows < t[s⃗], t′[r⃗] >∈ A^{∗}[s⃗], and by IH (a,ii) A^{∗}[r⃗] = A^{∗}[s⃗], and by 5.8 follows (t′ = t : A)^{∗}[r⃗; s⃗]. (a,ii) follows from IH (a,ii). Case (SY M)_{2} Assume Γ^{=}(r⃗; s⃗). As for (SY M)_{1} we have < s_{i}, r_{i} >∈ A_{i}^{∗}[ŝ_{i}], by IH A^{∗}[s⃗] = B^{∗}[r⃗] and therefore the assertion. Case (SUB) Assume Γ^{=}(r⃗; r′), < s_{i}, s′_{i} >∈ B_{i}[x/t]^{∗}[r⃗, ŝ_{i}]. Now by lemma 5.10

B_{i}[x/t]^{∗}[r⃗, ŝ_{i}] = B_{i}^{∗}[x/t[r⃗, ŝ_{i}], r⃗, ŝ_{i}] = B_{i}^{∗}[x/t[r⃗], r⃗, ŝ_{i}]

By IH 2 (a,i) < t[r⃗], t′[r′] >∈ A^{∗}[r⃗], therefore

θ^{∗}[x⃗/r⃗; r′, x/t[r⃗]; t′[r′], y⃗/s⃗; s′],

and by lemma 5.10 θ[x/t]^{∗}[x⃗/r⃗; r′, s⃗; s′], similarly for θ′. Proof for (c): If ,,y : B” in Γ, follows assertion by IH.

If ,,y : B” in Γ′[x/t], follows by IH B^{∗}[r⃗, x/t⃗[r⃗], ŝ_{i}] = B^{∗}[r′, x/t[r′], ŝ′_{i}], and by 5.10 the assertion. Case (REP L1) Assume Γ^{=}(r⃗; r′), < s_{i}, s′_{i} >∈ B_{i}[x/t]^{∗}[r⃗, ŝ_{i}]. We have < t[r⃗], t′[r′] >∈ A^{∗}[r⃗]. By 5.10 follows B_{i}^{∗}[x⃗/r⃗, x/t[r⃗], ŷ_{i}/ŝ_{i}] = B_{i}[x/t]^{∗}[r⃗, ŝ_{i}]. Therefore we have < s_{i}, s′_{i} >∈ B_{i}^{∗}[x⃗/r⃗, x/t[r⃗], ŷ_{i}/ŝ_{i}] Then by IH 1 B^{∗}[x⃗/r⃗, x/t[r⃗], y⃗/s⃗] = B^{∗}[x⃗/r′, x/t′[r′], y⃗/s′], and by 5.10 follows the assertion. Proof for (c): From IH 2 follows, arguing as for the rule (REF L), the assertion for Γ ⇒ t′ = t : A and further, arguing as for (T RANS) the assertion for Γ ⇒ t = t : A, which is the same as for Γ ⇒ t : A and now the proof follows as in (SUB). Case (REP L2) Assume Γ^{=}(r⃗, r′), < s_{i}, s′_{i} >∈ B_{i}[x/t]^{∗}[r⃗, ŝ_{i}]. Then < t[r⃗], t′[r′] >∈ A^{∗}[r⃗], and by IH 1(a,i)

(s = s : B)^{∗}[x⃗/r⃗; r′, x/t[r⃗]; t′[r′], y⃗/s⃗; s′]

and by 5.10 follows the assertion for (a,i). (a,ii) follows as in (REP L1), using that we get the assertion for Γ ⇒ t = t : A, and (c) follows exactly as in (REP L1). Case (ALP HA): Immediate by the IH since if A=_{α}A′, t=_{α}t′, A[s⃗] = A′[s⃗], t[r′]=_{α}t′[r′] and < t[r⃗], t[r′] >∈ A^{∗}[r⃗] ↔< t[r⃗], t′[r′] >∈ A^{∗}[r⃗]. Case (Π^{T,=}) Assume Γ^{=}(r⃗; r′). By IH (c) A^{∗}[r⃗] = A^{′∗}[r′], and, if < r, s >∈ A^{∗}[r⃗], follows < r, r >, < s, s >∈ A^{∗}[r⃗], therefore by IH B^{∗}[r⃗, x/r] = B^{′∗}[r′, x/r], B^{∗}[r⃗, x/s] = B^{′∗}[r′, x/s], Πx ∈ A.B^{∗}[r⃗] = (Πx ∈ A′.B′)^{∗}[r′]. Case (N^{I,=})_{2}: Assume Γ^{=}(r⃗; r′). By IH we have for some k ∈ ω t[r⃗]→_{red}S^{k}0 and t′[r′]→_{red}S^{k}0, therefore St[r⃗]→_{red}S^{k+1}0, St′[r′]→_{red}S^{k+1}0, and we have the assertion. Case (Π^{I,=}): Assume Γ^{=}(r⃗; r′), < r, r′ >∈ A^{∗}[r⃗]. Then by IH (a,i) < t[x/r, r⃗], t′[x/r′, r′] >∈ B^{∗}[x/r, r⃗] = B^{∗}[r⃗, x/r], < (λx.t)[x⃗/r⃗], (λx.t′)[x⃗/r′] >∈ (Πx ∈ A.B)^{∗}[r⃗]. (a,ii) follows as in (Π_{1}^{T,=}), since from IH (a,ii) follows (b) for x : A ⇒ B type. Case (W^{I,=}): Let n := max{level(A), level(B)}, W x ∈ A.B^{∗}. Assume Γ^{=}(r⃗; r′). Let F := F_{W} (A^{∗}[x⃗/r⃗], (x)B^{∗}[x⃗/r⃗]). Then by IH < r[r⃗], r′[r′] >∈ A^{∗}[r⃗], s[r⃗]→_{red}λx.t, s′[r′]→_{red}λx′.t′, B^{∗}[x/r[r⃗], r⃗] = B^{∗}[x/r′[r′], r′], and

∀ < u, u′ >∈ B[x/t]^{∗}[x⃗/r⃗](= B^{∗}[x/t[r⃗], x⃗/r⃗])∃γ < I_{n}. < t[x/u], t′[x/u′] >∈ F^{γ}

By (Δ_{0} − coll) and Ad(L_{I_{n}}) there exist a δ < I_{n} such that the γ can be chosen to be < δ. Then < sup(r, s)[r⃗], sup(r, s)[r′] ∈ F^{γ+1} ⊂ W x ∈ A.B^{∗}[r⃗]. (a,ii) follows as in (W^{T,=}). Case(N^{E,=}): Assume Γ^{=}(r⃗; r′). Then by IH 1 < r[r⃗], r′[r′] >∈ N^{∗}, therefore r[r⃗]→_{red}S^{n}0, r′[r⃗]→_{red}S^{n}0 for some n < ω. Further by IH 2 and 5.11 (b) exist s̃, s̃′ ∈ T erm_{nf} such that s[r⃗]→_{red}s̃, t[r⃗]→_{red}s̃′, < s̃, s̃′ >∈ A[x/0]^{∗}[r⃗] = A^{∗}[x/u, r⃗]. Let [x′/s⃗] := [x⃗/r⃗] \ {x, y}, [x′/s′′] := [x⃗/r′] \ {x, y}. Let P_{0}(r) := P (r, s̃, λx.λy.(t[x′/s⃗])). P_{1}(r) := P (r, s̃′, λx.λy.(t′[x′/s′])). Then

P (r, s, (x, y)t)[r⃗]→_{red}P_{0}(S^{n}0), P (r′, s′, (x, y)t′)[r′]→_{red}P_{1}(S^{n}0)

We have A[z/r]^{∗}[r⃗] = A^{∗}[z/r[r⃗], r⃗] = A^{∗}[z/S^{n}0, r⃗], and therefore assertion (a,i). We show: ∀m ∈ ω. < P_{0}(S^{m}0), P_{1}(S^{m}0) >∈ A^{∗}[z/S^{m}0, r⃗]. If m = 0, P_{0}(S^{m}0)→_{red}s̃, P_{1}(S^{m}0)→_{red}s̃′, < s̃, s̃′ >∈ A^{∗}[z/0, r⃗]. If m = k + 1, follows by IH P_{0}(S^{k}0)→_{red}s̃, P_{1}(S^{k}0)→_{red}s̃′, s̃, s̃′ ∈ T erm_{nf}, < s̃, s̃′ >∈ A^{∗}[z/S^{k}0, r⃗] = A[z/x]^{∗}[x/S^{k}0, r⃗].

P_{0}(S^{m}0)→_{red}t[x′/s⃗, x/S^{k}0, y/s̃], P_{1}(S^{m}0)→_{red}t′[x′/s′′, x/S^{k}0, y/s̃′]. Now < S^{k}0, S^{k}0 >∈ N^{∗}, therefore by IH 3 follows

< t[x′/s⃗, x/S^{k}0, y/s̃], t′[x′/s′′, x/S^{k}0, y/s̃′] >∈ A[z/Sx]^{∗}[r⃗] = A^{∗}[z/S^{m}0, r⃗],

and the side induction is finished. (a,ii) is easy. Case(Π^{E,=}): Assume Γ^{=}(r⃗; r′). By IH 1,2 there exist r̃, r̃′ ∈ T erm_{nf} such that r[r⃗]→_{red}r̃_{1}, r′[r′]→_{red}r̃′ < r̃_{1}, r̃′ >∈ A^{∗}[r⃗], and there are t, t′ ∈ T erm and Variables x, x′ ∈ V ar_{ML} such that

s[r⃗]→_{red}λx.r, s′[s⃗]→_{red}λx′.r′, < λx.r, λx′.r′ >∈ (Πx ∈ A.B)^{basis}[r⃗].

Therefore

Ap(s, r)[r⃗]→_{red}Ap(λx.t, r̃)→_{red}t[x/r̃, r⃗],
Ap(s′, r′)[r′]→_{red}t′[x′/r̃, r′]
< t[x/r̃, r⃗], t′[x′/r̃′, r′] >∈ B^{∗}[x/r̃, r⃗].

As before we conclude

< r[r⃗], r[r⃗] >∈ A^{∗}[r⃗]
< r̃, r_{1}[r⃗] >∈ A^{∗}[r⃗]
B^{∗}[x/r̃, r⃗] = B^{∗}[x/r[r⃗], r⃗] = B[x/r]^{∗}[r⃗],

and we have IH (a,i). (a,ii) follows as before Case(Σ^{E,=}): Assume Γ^{=}(r⃗; r′). By IH 1 exist s, s′, t, t′ ∈ T erm_{nf} such that

r[r⃗]→_{red}p(s, t), r′[r′]→_{red}p(s′, t′), < s, s′ >∈ A^{∗}[r⃗], < t, t′ >∈ B^{∗}[x/s, r⃗].

Then p_{0}(r[r⃗])→_{red}s, p_{0}(r′[r′])→_{red}s′, and we are done for the first rule, and p_{1}(r[r⃗])→_{red}t, p_{1}(r′[r′])→_{red}t′, and since from < s, s′ >∈ A[r⃗], follows

< s, s′ >∈ A[r⃗], < p_{0}(r)[r⃗], s >∈ A[r⃗],

therefore by IH 2

B^{∗}[x/s, r⃗] = B^{∗}[x/p_{0}(r)[r⃗], r⃗] = B[x/p_{0}(r)]^{∗}[r⃗]

follows (a,i) for the second rule. (a,ii) is in (Σ^{E,=})_{1} trivial, in (Σ^{E,=})_{2} we use the proof of (Σ^{E,=})_{1} and argue as before. Case(W^{E,=}): Assume Γ^{=}(r⃗; r′), n := max{level(A), level(B)}, F := F_{W} (A^{∗}[r⃗], (x)B^{∗}[r⃗]). By IH r[r⃗]→_{red}r̃, r′[r′]→_{red}r̃′, < r̃, r̃′ >∈ F^{δ}(r⃗, ·). for some δ < α. Let

[x′/s⃗] := [x⃗/r⃗] \ {x, y, z},
[x′/s′] := [x⃗/r′] \ {x, y, z},
R_{0}(r) := R(r, (x, y, z)t)[r⃗](= R(r, λx.λy.λz.(t[s⃗])))
R_{1}(r) := R(r, (x, y, z)t′)[r′].

We show by induction on γ,

∀γ < α.∀ < s̃, s̃′ >∈ F^{γ}. < R_{0}(s̃), R_{1}(s̃′) >∈ C^{∗}[u/s̃, r⃗] (+)

Since C[u/t]^{∗}[r⃗] = C^{∗}[u/r[r⃗], r⃗] = C^{∗}[u/r̃, r⃗] = C^{∗}[u/r̃′, r′] (using arguments as before), follows the assertion. The case γ = 0 is trivial, and if γ ∈ Lim follows the assertion by IH Let now γ = γ′ + 1, u′ := F^{γ′}, < s̃, s̃′ >∈ F (u′). If s̃→_{red}s, s̃′→_{red}s′, < s, s′ >∈ F^{basis}(r′, ·), < R_{0}(s), R_{1}(s′) >∈ C^{∗}[u/s, r⃗], follows < R_{0}(s̃), R_{1}(s̃′) >∈ C^{∗}[u/s, r⃗], further, like similar arguments before,

C^{∗}[u/s, r⃗] = C^{∗}[u/s̃, r⃗] = C^{∗}[u/s̃′].

We therefore assume < s̃, s̃′ >∈ F^{basis}(r⃗, u′). Let < s̃, s̃′ >=< sup(a, λx.s), sup(a′, λx′.s′) >, < a, a′ >∈ A^{∗}[r⃗]. Let < r′′, r′′′ >∈ B^{∗}[x/a, r⃗]. Then r′′→_{red}b, r′′′→_{red}b′ for < b, b′ >∈ B^{∗}[x/a, r⃗], b, b′ ∈ T erm_{nf}, and we have < s[x/r′′], s′[x′/r′′′] >∈ u′ and

< s[x/b], s′[x′/b′] >∈ u′ (∗)

Since u′ ⊂ (W x ∈ A.B)^{∗}[r⃗] follows from the first of these assertions

< λx.s, λx′.s′ >∈ (B → W x ∈ A.B)^{∗}[r⃗]

Further, for < b, b′ >∈ B^{∗}[x/r, r⃗],

(R_{0}((λx.s)v))[v/r′′]→_{red}R_{0}(s[x/b])(v ∉ F V (λx.s))
(R_{1}((λx.s′)v′))[v′/r′′′]→_{red}R_{1}(s′[x/b′])(v′ ∉ F V (λx.s))

and by side IH, follows

< (R_{0}((λx.s)v))[v/r′′], (R_{1}((λx′.s′)v))[v′/r′′′] >∈ C^{∗}[u/(s[x/b]), r⃗]
= C^{∗}[u/(s[x/r′′]), r⃗]

Now we have < r_{i}, r_{i} >∈ A_{i}[r̂_{i}], Ap(λx.s, r′′)→_{red}s[x/b], and by (∗), u′ ⊂ (W x ∈ A.B)^{∗}[r⃗], equiv((W x ∈ A.B)^{∗}[r⃗]) and 5.11 follows

< s[x/b]], Ap(λx.s, r′′) >∈ (W x ∈ A.B)^{∗}[r⃗]

therefore

C[u/Ap(y, v)]^{∗}[v/r′′, y/λx.s, x⃗/r⃗] = C^{∗}[u/Ap(λx.s, r′′), r⃗] = C^{∗}[u/(s[x/b]), r⃗]

further

C[u/Ap(y, v)]^{∗}[v/r′′, y/λx.s, x⃗/r⃗] = C[u/Ap(y, v)]^{∗}[v/r′′′, y/λx.s, x⃗/r⃗],

and we have

< λv.R_{0}((λx.s)v), λv′.R_{1}((λx′.s′)v′) >∈ (Πv ∈ B.C[u/Ap(y, v)])^{∗}[y/λx.s, x⃗/r⃗]

Now by IH 2 follows

< t[x/r, y/λx.s, z/λv.R_{0}((λx.s)v), r⃗], t′[x/r′, y/λx′.s′, z/λv′.R_{1}((λx.s′)v′), r′] >
∈ C[u/sup(x, y)]^{∗}[x/r, y/λx.s, r⃗]

Since

C[u/sup(x, y)]^{∗}[x/r, y/λx.s, r⃗] = C^{∗}[u/sup(r, λx.s), r⃗] = C^{∗}[u/s, s],

and

R_{0}(s)→_{red}(λx.λy.λz.t[x′/s⃗])r(λx.s)(λv.R_{0}((λx.s)v))
→_{red}t[x/r, y/λx.s, z/(λv.R_{0}((λx.s)v))]
R_{1}(s′)→_{red}t′[x/r′, y/λx.s′, z/(λv′.R_{1}((λx′.s′)v′))]

follows (+), and we are done. (a,ii) follows as in the case (N_{k}^{E,=}). Case (+^{E,=}): Assume Γ^{=}(r⃗; r′). By IH r[r⃗]→_{red}i(r̃) ∈ T erm_{nf}, r′[r′]→_{red}i(r̃′) ∈ T erm_{nf} and < r̃, r̃′ >∈ A^{∗}[r⃗] or r[r⃗]→_{red}j(r̃) ∈ T erm_{nf}, r′[r′]→_{red}j(r̃′) ∈ T erm_{nf} and < r̃, r̃′ >∈ B^{∗}[r⃗]. Let [x′/s⃗] := [x⃗/r⃗] \ {x}. In the first case we have

D(r, (x)s, (y)t)[r⃗]→_{red}(λx.(s[s⃗]))r̃→_{red}s[x/r̃, x⃗/r⃗],
D(r′, (x)s′, (y)t′)[r⃗]→_{red}s′[x/r̃′, x⃗/r′],
< s[x/r̃, r⃗], s′[x/r̃′, r′] >∈ C[z/i(x)]^{∗}[x/r̃, r⃗] = C^{∗}[z/i(r̃), r⃗]

and using arguments as before

C^{∗}[z/i(r̃), r⃗] = C^{∗}[z/r[r⃗], r⃗] = C[z/r]^{∗}[r⃗]

and we are done. The second assertion follows in the same way. (a,ii) follows as before. Case (I^{E}): Assume Γ^{=}(r⃗; r′). By IH 1 follows (I(A, s, t))^{∗}[r⃗] ≠ ∅, < s[r⃗], t[r⃗] >∈ A^{∗}[r⃗]. Further by IH 3 < t[r⃗], t[r′] >∈ A^{∗}[r⃗], and by equiv(A^{∗}[r⃗]) follows (a,i). (a,ii) is trivial. Case (Π^{=}), (Σ_{0}^{=}), (Σ_{1}^{=}): By using the proof for the elimination rules we see, that if the conclusion is r = s : C, we conclude assuming Γ^{=}(r⃗; r′), that (r = r : C)[r⃗; r′], further (r[r′]→_{red}t ∈ T erm_{nf}) → (s[r′]→_{red}t), therefore follows (r = s : C)[r⃗; r′]. Case (Π^{η}):Assume Γ^{=}(r⃗, r′) By IH we have

< t[r⃗], t[r′] >∈ (Πx ∈ A.B)^{∗}[r⃗],

therefore t[r⃗]→_{red}λx.s, t[r′]→_{red}λx′.s′,

< λx.s, λx′.s′ >∈ (Πx ∈ A.B)^{basis}[r⃗],

Assume < r, r′ >∈ A^{∗}[r⃗]. Then r→_{red}r̃, r′→_{red}r̃′, < r̃, r̃′ >∈ A^{∗}[r⃗], r̃, r̃′ ∈ T erm_{nf}.

Ap(t, x))[r⃗][x/r] = Ap(t[r⃗], r)→_{red}Ap(λx.s, r̃)→_{red}s[x/r̃],

and since

< s[x/r̃], s′[x′/r̃′] >∈ B^{∗}[x/r̃, r⃗] = B^{∗}[x/r, r⃗],

follows

< Ap(t, x)[r⃗][x/r], s′[x′/r̃′] >∈ B^{∗}[x/r, r⃗],

therefore

< λx.Ap(t, x)[r⃗], λx′.s′ >∈ (Πx ∈ A.B)^{∗}[r⃗],
< λx.Ap(t, x)[r⃗], t[r⃗] >∈ (Πx ∈ A.B)^{∗}[r⃗].

Case (Σ_{2}^{=}): Assume Γ^{=}(r⃗; r′). By IH t[r⃗]→_{red}r, t[r′]→_{red}r′ for some < r, r′ >∈ Σx ∈ A.B^{∗}[r⃗] ∩ (T erm_{nf} × T erm_{nf}), p(p_{0}(t), p_{1}(t))[r⃗]→_{red}r and we are done. Case (I^{=}): Assume Γ^{=}(r⃗; r′). By IH we conclude < t_{0}[r⃗], t_{0}[r′] >∈ I(A, t_{1}, t_{2})^{∗}[r⃗], therefore t_{0}[r′]→_{red}\underline{r}, < \underline{r}, \underline{r} >∈ I(A, t_{1}, t_{2})^{∗}[r⃗], < t_{0}[r⃗], \underline{r} >∈ I(A, t_{1}, t_{2})^{∗}[r⃗]. (a,ii) is trivial. Case other equality rules: Let r̃ = s̃ : A be the conclusion of the rules. By using several times the rules general rules, elimination rules and in case W^{=} the introduction rules we can conclude r̃ = r̃ : A, and s̃ = s̃ : A. (For (W^{=}) we argue that Γ, v : B[x/t_{0}] ⇒ Ap(t_{1}, v) : W x ∈ A.B, by (W^{E,=}) Γ, v : B[x/t_{0}] ⇒ R(Ap(s′, v), (x, y, z)t′) : C[u/Ap(s′, v)], by Π^{I,=} Γ ⇒ λv.R(Ap(s′, v), (x, y, z)t′) : Πv ∈ B.C[u/Ap(s′, v)], by (ALP HA) for the z_{i}, that we need, and it follows Γ ⇒ λz_{i}.R(Ap(s′, z_{i}), (x, y, z)t′) : Πv ∈ B.C[u/Ap(s′, v)], and now by (SUB) follows the assertion). Now, assuming Γ^{=}(r⃗, r′), and using the proofs above we can conclude < r[r⃗], r[r′] >∈ A^{∗}[r⃗] and A^{∗}[r⃗] = A^{∗}[r′], so (a,i). In all the cases, we have, if the right side is written as t[x_{1}/r_{1}, …, x_{n}/t_{n}], if x_{i} corresponds to the type B_{i} (read off from the rule) follows easily by IH and using the proofs of several rules handled before the assertion for Γ ⇒ r_{i} : B_{i}, therefore r_{i}[r⃗]→_{red}r̃_{i} ∈ T erm_{nf} for some r̃_{i}, < r̃_{i}, r_{i}[r⃗] >∈ B_{i}[r⃗], further r̃[r⃗]→_{red}t[x_{1}/r̃_{1}, ⋯ x_{n}r̃_{n}, r⃗]. We conclude

< t[x_{1}/r̃_{1}, …, x_{n}/r̃_{n}, r⃗], t[x_{1}/r_{1}[r⃗], …, x_{n}/r_{n}[r⃗], r⃗] >∈ A^{∗}[r⃗].

Now using equiv(A^{∗}[r⃗]) and lemma 5.11 we conclude

< r̃[r⃗], s̃[r⃗] >∈ A^{∗}[r⃗], < s̃[r⃗], s̃[r′] >∈ A^{∗}[r⃗],

and have (a,i). Case (U^{I}): trivial. (T^{I,=}) we have by IH, assuming Γ^{=}(r⃗; r′),

< a[r⃗], a′[r′] >∈ U^{∗}

therefore,

< a[r⃗], b, a′[r′] >∈ Û

for some b, by Cor_{U}(Û),

< a[r⃗], b, a[r⃗] >∈ Û, < a[r′], b, a[r′] >∈ Û,

and

T (a)^{∗}[r⃗] = b = T (a′)^{∗}[r′]

Case (π^{I,=}): Assume Γ^{=}(r⃗; r′). By IH a[r⃗]→_{red}ã, a′[r′]→_{red}ã′,

∃γ < I∃b′ ∈ T C(Ũ^{γ})(< ã, b′, ã >, < ã′, b′, ã >∈ Ũ^{γ}),

and

∀ < t, t′ >∈ b′ → ∃δ < I.∃c ∈ T C(Ũ^{δ}).
(< b[x/t, r⃗], c, b′[x/t′, r′] >∈ Ũ^{δ}).

Since Ad(L_{I}) (here is the central point where we need (Δ_{0}-coll) and an admissible a which is closed under the step to the next admissible), and T C(Ũ^{β}) ∈ L_{I} (β < I), there is a ρ < I, such that γ < ρ and δ can be chosen < ρ. There are now b, f such that ([x′/s⃗] := [x⃗/r⃗] \ {x}, [x′/s′] := [x⃗/r′] \ {x}) ϕ(ã, x, b[s⃗], ã′, x, b[s′], b, f, Ũ^{ρ}), (note that the c we used above is correct by Cor(Û)) and by 5.5 (a) follows

< πx ∈ a.b, Π^{∗}(b, f), πx ∈ a′.b′ >∈ Ũ^{ρ+1}.

Case (π^{=}): Assume Γ^{=}(r⃗; r′) and chose b′, f, ρ as in (π^{I,=}). Then T (a)^{∗}[r′] = b′, and if < t, t′ >∈ b′, T (b)^{∗}[x/t, r⃗] = f(t) = f(t′) = T (b)^{∗}[x/t′, r′]. Since we have Cor(Û) (by lemma ?? ??) follows

T ((πx ∈ a.b))^{∗}[r⃗] = Π^{∗}(T (a)[r⃗], (x)T (b)[r⃗]) = (Πx ∈ T (a).T (b))^{∗}[r⃗].

In the case of (w^{=}) we conclude as before, that

F_{W} (T (a)^{∗}[r⃗], (x)T (b)^{∗}[r⃗]) = F_{W} (T (a)^{∗}[r′], (x)T (b)^{∗}[r⃗‘])

and, since α^{+}(Ũ^{ρ}) < I, (ρ chosen as in (π^{I,=})) follows by 5.1

T (wx ∈ a.b)^{∗}[r⃗] = F_{W}^{α^{+}(_{U^{ρ}})}(T (a)^{∗}[r⃗], (x)(T (b))^{∗}[r⃗]) = F_{W}^{I} (T (a)^{∗}[r⃗], (x)(T (b))^{∗}[r⃗]) =

(W x ∈ T (a).T (b))^{∗}[r′] Case (σ^{E}): Assume Γ^{=}(r⃗; r′). By IH exists c, α ≺ I such that

< (σx ∈ a.b)[r⃗], c, (σx ∈ a.b)[r′] >∈ Ũ^{α}.

Let α be chosen minimal. Then, α = α′ +1, and with u := Ũ^{α′} there exist r, r′ ∈ T erm_{nf}, c, c′, f, f′ such that a[r⃗]→_{red}r, a[r′]→_{red}r′, < r, c, r′ >∈ u and (with [x′/s⃗] := [x⃗/r⃗] \ {x}, [x′/s′] := [x⃗/r′] \ {x}) ∀ < t, t′ >∈ c. < s[s⃗][x/t], f(t), s[s′][x/t′] >∈ u. Therefore T (a[r⃗])^{∗} = c = T (a[r′])^{∗}, and for < t, t′ >∈ T (a[r⃗])^{∗}, < s[x/t, r⃗], s[x/t′, s′] >∈ U^{∗}[ ]. (π^{E}), (w^{E}), ( ˜+^{E}) are checked in the same way. For (ĩ^{E}) we observe, that a[r⃗]→_{red}ã, a[r′]→_{red}ã′, s[r⃗]→_{red}s̃, s[r′]→_{red}s̃′, t[r⃗]→_{red}t̃, t[r′]→_{red}t̃′, and < ã, c, ã′ >∈ u, for some u as before, T (a)^{∗}[r⃗] = c, < s̃, s̃′ >∈ c, < t̃, t̃′ >∈ c, and since c is closed under →_{red} follows the assertion.

7 Arithmetical formulas in ML and KP i^{+}

In this section we want to evaluate the results we have found out to get the proof theoretical strength of Martin-Löf’s type theory. We will interpret the language of analysis (L_{analysis}, introduced in 7.1) in L_{ML} and L_{KP} (definition7.5) and prove that it permutes with the interpretation of Martin-Löf’s type theory in KP i^{+} (lemmata 7.7 and 7.9). Next we observe, that we could interpret every proof in KP i^{+}, ???? and have a stronger bound (lemma ??). At the end we analyze the proof theoretical strength of KP i_{n}^{+} and have the desired upper bound (theorem 7.14).

Definition 7.1 Definition of the language of Peano Arithmetic L_{analysis}: we have first order variables v_{i} (i ∈ ω, var_{analysis} := {v_{i}|i ∈ ω}); second order variables V_{i} (i ∈ ω, V AR_{analysis} := {V_{i}|i ∈ ω}); further we have symbols for each primitive recursive function, =, ∧, ∨, →, ∀, ∃, ⊥, and ., , , (,). Terms are first-order variables and f(t_{1}, …, t_{n}) if t_{i} are terms and f is a symbol for a n-ary primitive recursive function. Prime formulas are ⊥, equations r = s, and r ∈ X for r, s terms, X ∈ V AR_{analysis}. Formulas are prime formulas and A → B, A ∧ B, A ∨ B, ∀x.A, ∃x.A, if A, B formulas, x ∈ var_{analysis} ∪ V AR_{analysis}. A Δ_{0}^{1} formula is a formula, not containing bounded second-order quantifiers, and a Π_{1}^{1}- formula is ∀X.ϕ, where ϕ is a Δ_{0}^{1}-formula.

Assumption 7.2 After renaming all variables, we assume, we have additional new variables U_{i} of KP i^{+} (i ∈ ω) and Z_{i} of ML (i ∈ ω), s.t. in the step from a g-type to A^{∗}, Z_{i} becomes U_{i} and in 4.7 (a), if x_{i} = Z_{j}, then on the right side we put U_{j}. Definition 7.3 (a) Let ⌈C_{i}^{set}⌉ be new Gödelnumbers for new construstructors C_{i}^{set}.

(b) Let for a set b, Embset_{ML}(f) := \{< n, \underline{n}_{0} > |n ∈ ω \ b\} ∪ \{< n, \underline{n}_{1} > |n ∈ ω ∩ b\}.

(c) If CES(b), the constructors in b are ≠ ⌈C_{i}^{set}⌉, b_{1}, …, b_{m} ∈ Ad_{2}, b_{i} ⊂ ω, Z_{i_{j}} ≠ Z_{i_{k}}, (j ≠ k), then a_{0}(b, Z_{i_{1}}/b_{1}, …, Z_{i_{m}}/b_{m}) := b ∪ {< ⌈C_{i_{1}}^{set}⌉, 0, f_{1} >, …, < ⌈C_{i_{m}}^{set}⌉, 0, f_{m} >}, where f_{i} := Embset_{ML}(b_{i}).

Definition 7.4 Let P(N) := N → U, ML_{1}^{i}W_{T} ⊢ N → U type. Definition 7.5 (a) For each primitive recursive g : IN^{k} → IN we define a closed g-term

int_{P A,ML}(g), (we abbreviate this as ĝ := int_{P A,ML}(g)) such that

ML ⊢ ĝ : \underbrace{N → ⋯ N}_{k times} → N,

and we define a set int_{P A,KP} (g) short g̃ in L_{KP} such that KP i^{+} ⊢ fun(g̃) ∧ dom(g̃) = IN^{k} ∧ ∀x ∈ IN^{k}.g̃(x) ∈ IN. Case g = S: ĝ := λx.Sx, g̃ := {< x, x + 1 > |x ∈ IN}. Case g = P roj_{i}^{n} ĝ := λx_{1}, …, x_{n}.x_{i}, g̃ := {<< x_{1}, …, x_{n} >, x_{i} > |x_{1}, …, x_{n} ∈ IN}. Case g = Cons_{c}^{n}:

ĝ := λx_{1}, …, x_{n}.S^{c}0, g̃ := {<< x_{1}, …, x_{n} >, c > |x_{1}, …, x_{n} ∈ IN}. Case g(x_{1}, …, x_{n}) = h(g_{1}(x_{1}, …, x_{n}), …, g_{m}(x_{1}, …, x_{n})):

ĝ := λx_{1}, …, x_{n}.ĥ(ĝ_{1}x_{1} ⋯ x_{n}) ⋯ (ĝ_{m}x_{1} ⋯ x_{n}),

g̃ := {<< x_{1}, …, x_{n} >, h(g_{1}(x_{1}, …, x_{n}), …, g_{m}(x_{1}, …, x_{n})) >

|x_{1}, …, x_{n} ∈ IN}. Case g(x_{1}, …, x_{n}, 0) = h(x_{1}, …, x_{n}),

g(x_{1}, …, x_{n}, y + 1) = k(x_{1}, …, x_{n}, y, g(x_{1}, …, x_{n}, y)):

ĝ := λx_{1}, …, x_{n}, y.P (y, ĥx_{1} ⋯ x_{n}, (u, v)k̂x_{1} ⋯ x_{n}uv),

define l(x_{1}, …, x_{n}, 0) := h̃(x_{1}, …, x_{n}),

l(x_{1}, …, x_{n}, Sy) := k̃(x_{1}, …, x_{n}, y, l(x_{1} ⋯ x_{n}, y)),

then

g̃ := {<< x_{1}, …, x_{n}, y >, l(x_{1}, …, x_{n}, y) > |x_{1}, …, x_{n}, y ∈ IN}.

(b) For each term t of analysis we define a g-term int_{P A,ML}(t), short t̂ and a term of L_{KP} int_{P A,KP} (t), short t̃, such that, if F V (t) = {v_{i_{1}}, …, v_{i_{n}}} (i_{1} < ⋯ < i_{n}) (v_{i} as in definition 7.1 of var_{analysis}) then F V (t̂) ⊂ {z_{i_{1}}, …, z_{i_{n}}}, F V (t̃) ⊂ {u_{i_{1}}, …, u_{i_{n}}} and ML ⊢ z_{i_{1}} : N, …, z_{i_{n}} : N ⇒ t̂: N, and KP i^{+} ⊢ ∀u_{i_{1}}, …, u_{i_{n}} ∈ ω.(t̃ ∈ ω). Case t = v_{i}: t̂:= z_{i}, t̃:= u_{i}. Case t = 0: t̂:= 0, t̃:= 0. Case t = gt_{1} ⋯ t_{n}: t̂:= ĝt̂_{1} ⋯ t̂_{n}, t̃:= g̃(t̃_{1}, …, t̃_{n}).

(c) For each formula A of analysis we define a g-type int_{P A,ML}(A) (short Â), and a formula of L_{KP} int_{P A,KP} (A), short Ã, such that in KP i^{+} Ã is equivalent to a Δ_{0}- formula, and if F V (A) = {v_{i_{1}}, …, v_{i_{n}}, V_{j_{1}}, …, V_{j_{m}}}, i_{k} ≠ i_{l}, j_{k} ≠ j_{l} for k ≠ l, then F V (Â) ⊂ {z_{i_{1}}, …, z_{i_{n}}, Z_{j_{1}}, …, Z_{j_{m}}}, F V (Ã) ⊂ {u_{i_{1}}, …, u_{i_{n}}, U_{j_{1}}, …, U_{j_{m}}} and for all four versions of Martin-Löf Type Theory (ML, ML_{1}^{i}W_{T} , ML_{1}^{e}W_{R}, ML_{1}^{i}W_{R} ML ⊢ z_{i_{1}} : N, …, z_{i_{n}} : N, Z_{j_{1}} : P(N), …, Z_{j_{m}} : P(N) ⇒ Â type. Case A = (s = t): Â := I(N, ŝ, t̂), Ã := (s̃ = t̃). Case A = (t ∈ V_{i}): Â := T (Z_{i}t̂) for the Tarski-version Â := Z_{i}t̂ for the Russellversion, Ã := t̃ ∈ U_{i}. Case A = (B ∧ C): Â := (B̂ × Ĉ), Ã := B̃ ∧ C̃. Case A = (B ∨ C): Â := (B̂ + Ĉ), Ã := (B̃ ∨ C̃). Case A = (B → C): Â := (B̂ → Ĉ), Ã := (B̃ → C̃). Case A = ∀v_{i}.B: Â := Πz_{i} ∈ N.B̂, Ã := ∀u_{i} ∈ ω.B̃. Case A = ∃v_{i}.B: Â := Σz_{i} ∈ N.B̂, Ã := ∃u_{i} ∈ ω.B̃. Case A = ∀V_{i}.B: Â := ΠZ_{i} ∈ P(N).B̂, Ã := ∀U_{i} ∈ Ad_{2}.U_{i} ⊂ ω → B̃. Case A = ∃V_{i}.B: Â := ΣZ_{i} ∈ P(N).B̂, Ã := ∃U_{i} ∈ Ad_{2}.U_{i} ⊂ ω ∧ B̃. Case A =⊥: Â := N_{0}, Ã := (0 ≠ 0).

Definition 7.6 (a) We define emb : ω → ω, embnat(n) := S^{n}0(=: ˆ n̂) (or more precisely ⌈S^{n}0⌉), a function definable in KP i^{+}.

(b) < a, · >:=< a, a >. Lemma 7.7 (a) If g : IN^{k} → IN is primitive recursive, then

KP i^{+} ⊢ ∀t_{1}, …, t_{k} ∈ T erm_{Cl}.∀n_{1}, …, n_{k}.

(r^{1}→_{red}ˆn̂_{1} ∧ ⋯ ∧ r^{k}→_{red}ˆn̂_{k}) → ĝr_{1}, …, r_{k}→_{red}emb(g̃(n_{1}, …, n_{k})).

(b) If t is a term of analysis, F V (t) ⊂ {v_{1}, …, v_{n}}, then

KP i^{+} ⊢ ∀r_{1}, …, r_{n} ∈ T erm_{Cl}.∀n_{1}, …, n_{k}.(r_{1}→_{red}ˆn̂_{1} ∧ ⋯ ∧ r_{k}→_{red}ˆn̂_{k}) →
t̂[z_{1}/r_{1}, …, z_{n}/r_{n}]→_{red}emb(t̃[u_{1}/n_{1}, …, u_{n}/n_{n}]).

Proof: (a) Case g = S: ĝr_{1}→_{red}(λx.Sx)ˆn̂_{1}→_{red}Sˆn̂_{1} = emb(Sn_{1}). Case g = P roj_{i}^{n}: ĝt_{1}, …, r_{n}→_{red}ˆn̂_{i} = emb(g̃(n_{1}, …, n_{k})). Case g = Cons_{c}^{n}: trivial. Case g(x⃗) = h(g_{1}(x⃗), …, g_{m}(x⃗)), l_{i} := g̃_{i}(n_{1}, …, n_{n}):

ĝ_{i}(r_{1}, …, r_{n})→_{red}emb(g̃_{i}(n_{1}, …, n_{n})) =: emb(l_{i}),

therefore

ĝr_{1}, …, r_{n}
= ĥĝ_{1}(r_{1}, …, r_{n}), …, ĝ_{m}(r_{1}, …, r_{n})
→_{red} ĥl̂_{1}, …, l̂_{n}
→_{red} emb(h̃(l_{1}, …, l_{m}))
= embnat(g(n_{1}, …, n_{n}))

Case g(x_{1}, …, x_{n}, 0) = h(x_{1}, …, x_{n}), g(x⃗, x_{n+1}) = k(x⃗, y, g(x⃗, x_{n+1}))). Let ĥ(r_{1}, …, r_{n})→_{red}embnat(h̃(n_{1}, …, n_{n})) =: l_{0}. We show by induction on n_{n+1}, that P (ˆn̂_{n+1}, l_{0}, (λu, v.k̂r_{1}, …, r_{n}uv))→_{red}emb(g̃n_{1}, …, n_{n+1}) (since g(r_{1}, …, r_{n})→_{red}P (ˆn̂_{n+1}, l_{0}, (λu, v.k̂r_{1}, …, r_{n}uv)) follows the assertion) If n_{n+1} = 0,

P (nhathat_{n+1}, l_{0}, (λu, v.k̂r_{1}, …, r_{n}uv))
→_{red} l_{0}
= emb(g̃(n_{1}, …, n_{n}, n_{n+1}))

If n_{n+1} = m + 1,

g(t_{1}, …, t_{n}, t_{n+1})
→_{red} P (S ˆm̂, l_{0}, (λu, v.k̂r_{1}, …, r_{n}uv))
→_{red} (λu, v.k̂r_{1}, …, r_{n}uv)) ˆm̂P (k̂, l_{0}, (λu, v.k̂r_{1}, …, r_{n}uv))
→_{red} (λu, v.k̂r_{1}, …, r_{n}uv)) ˆm̂emb(g(n_{1}, …, n_{n}, m)
→_{red} k̂r_{1}, …, r_{n} ˆm̂emb(g(n_{1}, …, n_{n}, m)
→_{red} k̂ˆn̂_{1}, …, ˆ n̂_{n} ˆm̂emb(g(n_{1}, …, n_{n}, m)
→_{red} emb(k̃(n_{1}, …, n_{n}mg(n_{1}, …, n_{n}, m))
= emb(g̃(n_{1}, …, n_{n+1})

(b): If t = v_{i}, 0, this is trivial, and if t = gt_{1}, …, t_{n} follows

t_{i}[r⃗]→_{red}emb(t̃_{i}[n⃗]),

by (a) therefore

t[r⃗]→_{red}g̃(t̃_{1}[r⃗], …, t̃_{n}[r⃗]) = t̃[r⃗]

Next task would now be to prove, that, when we first interpret a formula of L_{analysis} in L_{ML} and then use the interpretation, as we have done in section 4, we get an equivalent formula to the one, we get by directly interpreting L_{analysis} in L_{KP}. But in this formulation, this is not correct, here is the place, where we need to extend the set of term constructors by non constructive constructors. In order to interpret a true Π_{2}^{0} formula A = ∀x.∃y.ϕ in such a way, that for the false formula ¬A we have (¬A)^{∗} = ∅ we need an element of A^{∗}, which gives for the x a witness y of ϕ. But this might be non constructive, so we add here a (possibly) non constructive new constructor. So for every formula we need certain new constructors. Further, we want that Π_{1}^{1}-formulas are interpreted correctly as well, that is, we want, that if we have a free set variable V_{i}, we can replace it in the KP i^{+}-interpretation as arbitrary subsets U_{i} ⊂ ω, U_{i} ∈ Ad_{2}. We achieve this by allowing here arbitrary interpretations for the constructor C_{i}^{set}. Lemma 7.8 For every Δ_{0}^{1}-formula A with

F V (A) ⊂ {v_{i_{1}}, …, v_{i_{l}}, V_{j_{1}}, …, V_{j_{m}}}

with i_{k} ≠ i_{l}, j_{k} ≠ j_{l}, (k ≠ l) there is a CES c not referring to the constructors C_{i}^{set} (i ∈ ω) and a g-term h ∈ T erm_{Cl} s.t. F V (h) ⊂ {z_{i_{1}}, …, z_{i_{l}}}, and with z⃗ := z_{i_{1}}, …, z_{i_{l}}, Z⃗ := Z_{j_{1}}, …, Z_{j_{m}}, u⃗ := u_{i_{1}}, …, u_{i_{l}}, U⃗ := U_{j_{1}}, …, U_{j_{m}}, C⃗^{Z} := C_{j_{1}}^{set}, …, C_{j_{m}}^{set}, n⃗ := n_{1}, …, n_{l}, E⃗mbset(b) := Embset(b_{1}, …, b_{m}), we have

KP i_{n}^{+} ⊢ ∀n_{1}, …, n_{l} ∈ ω.∀r_{1}, …, r_{l} ∈ T erm_{Cl}.
∀b_{1}, …, b_{m} ∈ Ad_{2}.∀a_{0} ∈ Ad_{2}.
b_{1} ⊂ ω → b_{m} ⊂ ω → CES(a_{0}) ∧
a_{0}(c, b_{1}, …, b_{m}) ⊂ a_{0} →
(r_{1}→_{red}ˆn̂_{1} → ⋯ → r_{l}→_{red}ˆn̂_{l}) →
((∃r ∈ T erm_{nf}.h[z⃗/r⃗]→_{red}r) ∧
(Ã[u⃗/n⃗, U⃗/ ] ↔< h[z⃗/r⃗], · >∈ Â^{∗}[z⃗/r⃗]) ∧
(Ã[u⃗/n⃗] ↔ Â^{∗}[z⃗/r⃗] ≠ ∅))

Proof: by induction on the definition of the formulas. Again we will not mention explicitly Variables, that occur in subterms, or do not occur at all. Case A =⊥: Choose c := ∅, h := 0 We have ¬Ã[n⃗], Â^{∗}[r⃗] = ∅. Case A = (s = t): Choose as c := ∅, h := \underline{r} ∈ T erm_{nf}. We have, using that for r→_{red}s ∈ T erm_{nf} s is unique, and 7.7

Ã[n⃗] ↔ s̃[n⃗] = t̃[n⃗]
↔ (∃n ∈ ω.ŝ[r⃗]→_{red}S^{n}0 ∧ t̂[r⃗]→_{red}S^{n}0)
↔ < ŝ[r⃗], t̂[r⃗] >∈ N^{∗}
↔ < \underline{r}, \underline{r} >∈ Â^{∗}[r⃗]
↔ Â^{∗}[r⃗] ≠ ∅

Case A = (s ∈ V_{i}): Let c := ∅, h := 0_{1}. Assume r⃗, n⃗, b_{i}, a_{0} as in the assumption. Then ŝ[z⃗/r⃗]→_{red}emb(s̃[u⃗/n⃗]) = S^{k}0 for some k. Â[z⃗/r⃗, Z⃗/C⃗^{Z}]_{a_{0}}^{∗} = T (C_{i}^{set}(s⃗[z⃗/r⃗]))_{a_{0}}

= \{ \begin{matrix}T (\underline{n}_{0}) & if k ∉ b_{i} \\ T (\underline{n}_{1}) & if k ∈ b_{i} \end{matrix} = \{ \begin{matrix}∅ & if k ∉ b_{i} \\ Compl(\{0_{1}\}) & if k ∈ b_{i} \end{matrix}.

Ã[u⃗/n⃗, U⃗/E⃗mbset(b)] = s̃[u⃗/n⃗] ∈ Embset(b_{i}). Then the assertion is immediate. Case A = (A_{1}∧A_{2}): Let c_{i}, h_{i} for A_{i} chosen, c := c_{1}∪c_{2}, h := p(h_{1}, h_{2}). Then for n⃗, r⃗, b⃗, a_{0} as in the assumption of the assertion there exist s_{1}, s_{2} ∈ T erm_{nf}, such that r_{i}[r⃗]→_{red}s_{i}, h[r⃗]→_{red}p(s_{1}, s_{2}) ∈ T erm_{nf}.

Ã[n⃗] ↔ B̃_{1}[n⃗] ∧ B̃_{2}[n⃗]
↔ < s_{1}, · >∈ B̂_{1}^{∗}[n⃗]∧ < s_{2}, · >∈ B̂_{2}^{∗}[n⃗]
↔ < h[r⃗], · >∈ Â^{∗}[n⃗]
↔ B̂_{1}^{∗}[r⃗] ≠ ∅ ∧ B̂_{2}^{∗}[r⃗] ≠ ∅
↔ Â^{∗}[n⃗] ≠ ∅

Case A = (B_{1} ∨ B_{2}): Let c_{i}, h_{i} for B_{i} chosen. Let

f := {<< n_{1}, …, n_{l} >, i > |(i = 0 ∧ B̃_{0}[n⃗]) ∨ (i = 1 ∧ ¬B̃_{0}[n⃗])}

(note that B̃_{0} is a Δ_{0}-formula). Let ⌈C⌉ be a Gödel-number for a new constructor, different from all ⌈C^{set}⌉, c := c_{1}∪c_{2}∪{< ⌈C⌉, l + 1, f}, h := P (Cz⃗, h_{1}, (u, v)h_{2}) (u, v new variables). Assume n⃗, r⃗, b⃗, a_{0} as in the assumption. Then there exist s_{i} such that h_{i}[r⃗]→_{red}s_{i} ∈ T erm_{nf}

C(r_{1}, …, r_{n})→_{red}C(ˆn̂_{1}, …, ˆ n̂_{i})→_{red}S^{i}0

for i = f(n⃗) ∈ {0, 1}, if i = 0,

h[r⃗]→_{red}P (0, s_{1}, (u, v)h_{2}[r⃗])→_{red}s_{1} ∈ T erm_{nf},

and if i = 1,

h[r⃗]→_{red}s_{2}.

We have

Ã[n⃗] ↔ B̃_{1}[n⃗] ∨ (¬B̃_{1}[n⃗] ∧ B̃_{2}[n⃗])
↔ (f(n⃗) = 0∧ < s_{1}, · >∈ B̂_{1}^{∗}[r⃗]) ∨ (f(n⃗) = 1∧ < s_{2}, · >∈ B̂_{2}^{∗}[r⃗])
↔ < h[r⃗], · >∈ Â^{∗}[r⃗]
↔ B̂_{1}^{∗}[r⃗] ≠ ∅ ∨ B̂_{2}^{∗}[r⃗] ≠ ∅
↔ Â^{∗}[r⃗] ≠ ∅

Case A = (B_{1} → B_{2}). Let c_{i}, h_{i} for B_{i} chosen, c := c_{1} ∪ c_{2}, h := λx.h_{2}. Assume r⃗, n⃗, b⃗, a_{0} as in the assumption. Then h_{2}[r⃗]→_{red}s_{2} for some s_{2} ∈ T erm_{nf}. Subcase Ã[n⃗]. If B̃_{1}[n⃗] is false, then by IH B̂_{1}^{∗}[r⃗] = ∅, therefore

∀ < r, r′ >∈ B̂_{1}^{∗}[r⃗]. < h_{2}[x/r, r⃗], h_{2}[x/r′, r⃗] >∈ B̂_{2}^{∗}[r⃗]

therefore < h[r⃗], · >∈ Â^{∗}[r⃗]. If B̃_{1}[n⃗] is true, then B̃_{2}[r⃗] is true, therefore < s_{2}, · >∈ B̂_{2}^{∗}[r⃗],

∀ < r, r′, · >∈ B̂_{1}^{∗}[r⃗].h_{2}[x/r, r⃗]→_{red}s_{2} ∧ h_{2}[x/r′, r⃗]→_{red}s_{2}∧ < s_{2}, · >∈ B̂_{2}^{∗}[n⃗],

h[r⃗] ∈ Â^{∗}[n⃗]. Subcase ¬Ã[n⃗]. Then by IH exists s_{1} such that h_{1}[r⃗]→_{red}s_{1} ∈ T erm_{nf} and we have < s_{1}, · > inB̂_{1}^{∗}[r⃗] and, if we had < s, s′ >∈ Â^{∗}[r⃗], then < s, · >∈ Â^{∗}[r⃗], s→_{red}λx.t for some t, < t[x/s_{1}], · >∈ B̂_{2}^{∗}[r⃗] = ∅, a contradiction, therefore Â^{∗}[r⃗] = ∅. Case A = ∀v_{i}.B: Let c_{1}, h_{1} for B be chosen, c := c_{1}, h := λv_{i}.h_{1}. Assume n⃗, r⃗, b⃗, a_{0} as in the assertion, h[r⃗] ∈ T erm_{nf}. Assume < r, r′ >∈ Â^{∗}[r⃗], then < r, r >∈ Â^{∗}[r⃗], r→_{red}λx.t and

∀k ∈ ω < r[x/k̂, r⃗], · > . ∈ B̂^{∗}[z_{i}/k̂, r⃗],

by IH follows ∀k ∈ ω.B̃[u_{i}/k, n⃗], therefore Ã[n⃗]. Assume Ã[n⃗]. Then for all k ∈ ω B̃[v_{i}/k, r⃗], therefore by I.H. < h[v_{i}/r, r⃗], · >∈ B̂^{∗}[z_{i}/r, r⃗], whenever r→_{red}S^{k}0, therefore < h[r⃗], · >∈ Â[r⃗]. Case A = ∃v_{i}.B, c_{1}, h_{1} be chosen for B,

f := {<< n⃗ >, k > | (B̃[u_{i}/k, n⃗] ∧ ∀k′ < k.¬(B̃[u_{i}/k, n⃗])) ∨
(k = 0 ∧ ∀k ∈ ω.¬(B̃[u_{i}/k, n⃗]))}

Let ⌈C⌉ be a new name for a constructor ≠ C_{i}^{set}, c := c_{1} ∪ {< ⌈C⌉, l + 1, f}. h := p(C(z⃗), h_{1}[z_{i}/C(z⃗)]) Assume n⃗, r⃗ b⃗, a_{0} as in the assertion, k := f(n⃗).

C(r⃗)→_{red}C(ˆn̂_{1}, …, ˆ n̂_{n})→_{red}S^{k}0.

By IH we have h_{1}[z_{i}/C(z⃗)][r⃗] = h_{1}[z_{i}/C(r⃗), r⃗]→_{red}t_{1} for some t_{1} ∈ T erm_{nf}, therefore h[r⃗]→_{red}p(S^{k}0, t_{1}). Assume < r, r′ >∈ Â^{∗}[r⃗]. Then < r, r >∈ Â^{∗}[r⃗], r→_{red}p(S^{l}0, r′′) ∈ T erm_{nf}. Then < r′′, · >∈ B̂^{∗}[z_{i}/S^{l}0, r⃗], by I.H. B̃[u_{i}/l, n⃗], therefore Ã[n⃗]. Assume Ã[n⃗]. Then by definition B̃[u_{i}/k, n⃗] and by IH

< t_{1}, · >∈ B̂^{∗}[z_{i}/k̂, r⃗] = B̂^{∗}[z_{i}/A_{k}(r⃗), r⃗] = B̂[z_{i}/A_{k}(z⃗)]^{∗}[z⃗/r⃗],

(we use that ML ⊢ z⃗ : N ⇒ A type, < A_{k}(r⃗), k̂ >∈ N^{∗} and the Main Lemma), therefore < h[r⃗], · >∈ Â^{∗}[r⃗].

Lemma 7.9 If ϕ is a Π_{1}^{1}-formula, ML ⊢ s : ϕ̂, then KP i^{+} ⊢ ϕ̃. Proof: Let ϕ = ∀V_{i}.B. ML ⊢ s : ϕ̂. By 6.1 follows KP i^{+} ⊢ ∀CES(b). < ŝ_{b}^{∗}, · >∈ ϕ̂_{b}^{∗}. ϕ̂^{∗} = Π^{∗}(N̂ → U^{∗}, B̂). Assume b_{1} ∈ Ad_{2}, x a variable, c the CES chose for B as in lemma 7.8, a_{0} := b_{0} ∪ {< C_{i}^{set}, 0, Embset(b) >}. C_{i} ∈ (N → U)_{a_{0}}^{∗}. Therefore, under the assumption b_{i} ∈ Ad_{2}, b_{i} ⊂ ω, KP i^{+} ⊢< ŝ^{∗}C_{i}^{set}, · >∈ B̂_{a_{0}}^{∗}[V_{i}/C_{i}^{set}], by lemma 7.8 KP i^{+} ⊢ B̃[U_{i}/b_{i}], and we have KP i^{+} ⊢ ∀V_{i} ∈ Ad_{2}.V_{i} ⊂ ω → B̃ which is ϕ̃. We are

now coming to the end and just have to prove, that the result we have suffices to show, that we have really an upper bound for the proof-theoretical strength. We have to overcome the fact, that we did only prove, that if ML ⊢ T I(≺) (T I(≺) for transfinite induction over a primitive recursive relation ≺), we get KP i^{+} ⊢ T I^{Ad_{2}}(≺), where T I^{Ad_{2}} means transfinite induction, with the quantifier over subsets of ω, which are elements of Ad_{2}. But we will see, that this will be enough: Definition 7.10 We define some formulas in L_{KP}:

(a) In the following, (a, ≺) will be a pair where a is a set, and ≺⊂ a×a. In this context s ≺ t :=< s, t >∈≺, ∀x ≺ t.ϕ := ∀x ∈ a.x ≺ t → ϕ, and ∃x ≺ t.ϕ := ∃x ∈ a.x ≺ t ∧ ϕ. Further s ⪯ t := s ≺ t ∨ s = t.

(b) W f^{d}(a, ≺) :=≺⊂ a × a ∧ ∀x ∈ d.x ⊂ a → x ≠ ∅ → ∃y ∈ x.∀z ≺ y.z ∉ x. (≺ is a relation on a which is well-founded, restricted to d).

(c) Collaps(a, ≺, f) := F un(f) ∧ dom(f) = a ∧ ∀x ∈ a.f(x) = {f(y)|y ≺ x}. (f is a collapsing function on (a, ≺).

Lemma 7.11 If ϕ(y, y_{1}, …, y_{n}) is a Δ_{0}-formula with only the free variables mentioned, then KP i^{+} ⊢ W f^{d}(a, ≺) → Ad(c) → ∀y_{1}, …, y_{n} ∈ c.(∀x ∈ a.(∀y ≺ x.ϕ(y, y_{1}, …, y_{n}) → ϕ(x, y_{1}, …, y_{n}))) → ∀x ∈ a.ϕ(x, y_{1}, …, y_{n}). The formula after the second arrow is called principle of restricted induction over (a, ≺). Proof: Immediate. Lemma 7.12 KP i^{+} ⊢ Ad(c) → Ad(d) → c ∈ d → W f^{d}(a, ≺) → c, d ∈ a → ∃f ∈ c.Collaps(a, ≺, f). Proof: As in [Jäg86], theorem 4.6, but replacing Δ_{0}-induction by d-induction. Lemma 7.13 If KP i^{+} ⊢ ∀x.Ad(x) → ϕ(x) for a Σ_{1}-formula ϕ^{x}, then L_{v} ⊧ ϕ, where ϕ^{x} is the restriction of all unrestricted quantifiers to x, and v := ψ_{Ω_{1}}(Ω_{I+ω}). Proof: We follow the lines of [Buc92]. First observe, that we can prove as in theorem 2.9 there, using several applications of ∃_{κ}, (⋀), and ⊢^{∗} Ad(L_{κ}) for κ ∈ R, and if we have λ ∈ Lim, (κ_{i})_{i∈ω} a sequence, s.t. κ_{0} ∈ R, ∀α ∈ κ.∃ρ ∈ κ.α ∈ ρ ∈ R and κ_{i} ∈ κ_{i+1} ∈ R ∩ λ (i ∈ ω), and if we extend X^{∗} by including as well κ_{i} (i ∈ ω) follows

⊢_{λ}^{∗} (KP i^{+})^{λ}.

(⊢_{λ}^{∗} ϕ^{λ} for every axiom ϕ of KP i^{+}). We can adjust theorem 3.12 of [Buc92] to obtain, if we have in this situation, if λ ∈ H, κ_{i} ∈ H (i ∈ ω) and H closed under ξ ↦ ξ^{R}, then:

For each theorem ϕ of KP i^{+} exists k ∈ IN such that H ⊢_{λ+k}^{ω^{λ+k}} ϕ^{λ}.

Now observe, that H_{γ} in [Buc92] has the desired properties (with λ := Ω_{I+ω}, κ_{i} := Ω_{I+i}) and we conclude that if KP i^{+} ⊢ ∀x.Ad(x) → ϕ^{x}, where ϕ is a Σ-sentence, then L_{v} ⊧ ϕ for v := ψ_{Ω_{1}}(Ω_{I+ω}).

Theorem 7.14 |ML|, |ML|, |ML_{1}^{e}W_{R,U}|, |ML_{1}^{e}W_{R}|, |ML_{1}^{i}W_{T} |, |ML_{1}^{i}W_{R}| ≤ v with v := ψ_{Ω_{1}}(Ω_{I+ω}), where the ordinal denotation is as in [Buc92]. Proof: Since all the theories can be embedded in ML in such a way, that the principle of transfinite induction remains unchanged (except, that T (U_{i}t) becomes U_{i}t in the version à là Russell), it is sufficient, to prove it for ML. Assume ≺ is a primitive recursive linear ordering on the primitive recursive subset T of ω, ϕ := ∀X.(∀y.y ∈ T → (∀z.z ≺ y → z ∈ X) → y ∈ X) → ∀y.y ∈ T → y ∈ X and ML ⊢ ϕ̂. Then by lemma 7.9 KP i^{+} ⊢ ϕ̃. We follow the proof of [Rat91] theorem 7.14, define a := {x ∈ ω|x ∈ T }, prec′ := {< x, y >∈ ω × ω|x ≺ y}. Then KP i^{+} ⊢ Ad(Ad_{1}) ∧ Ad(Ad_{2}) ∧ Ad_{1} ∈ Ad_{2} ∧ W f^{Ad_{2}}(a, ≺′) ∧ a, ≺′∈ Ad_{1}, therefore by 7.12 KP i^{+} ⊢ ∃f ∈ Ad_{1}.Collaps(a, ≺′, f), KP i^{+} ⊢ ∀x.Ad(x) → ∃f ∈ x.Collaps(a, ≺′, f). Therefore L_{v} ⊧ ∃f.Collaps(a, ≺′, f). Since ≺ is linear ordering, follows Image(f) is an ordinal, and, because v ∈ Lim we have Image(f) ∈ L_{v}, ordertype(≺) = Image(f) < v.

References

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

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

[Jäg79] G. Jäger. Die konstruktible Hierarchie als Hilfsmittel zur beweistheoretischen Untersuchung von Teilsystemen der Analysis. PhD thesis, Universität München, 1979. Dissertation.

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

[Jäg86] G. Jäger. Theories for Admissible Sets: A Unifying Approach to Proof Theory. Bibliopolis, Naples, 1986.

[JP82] G. Jäger and W. Pohlers. Eine beweistheoretische Untersuchung von (Δ_{2}^{1} − CA) + BI und verwandter Systeme. Sitzungsberichte der Bayer. Akad. d. Wiss., Math.-Nat. Kl., pages 1 – 28, 1982.

[Poh82] W. Pohlers. Admissibility in proof theory, a survey. In Logic, Methodology and Philosphy of Science VI, Hannover 1979, pages 123 – 139, Amsterdam, 1982. North-Holland.

[Rat91] M. Rathjen. Proof-theoretical analysis of KPM. Archiv math. Logik, 30:377 – 403, 1991.

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

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