Set theoretical proofs as type theoretical programs

Anton Setzer Institut für Informatik Universität München Theresienstr. 39 D-80333 München Germany Tel. +49 89 2394 4462 Fax +49 89 2805 248

              email setzer@rz.mathematik.uni-muenchen.de

February 12, 1996

We show, that all Π_{2}^{0}-sentences, provable in the set theory KP I_{U}^{+} can be proved in Martin-Löf’s Type Theory with W -type and one universe. Therefore set theoretical proofs can be considered as programs in type theory. The method used is a formalisation of proof theoretical methods in type theory. The result will be a high level type theory program using the full strength of Martin-Löf’s Type Theory. We suggest the use of Kripke-Platek style set theory as a programming language.

Set theoretical proofs as type theoretical programs

Anton Setzer

1 Introduction

Mathematics is usually developed on the basis of set theory. When trying to use type theory as a new basis for mathematics, most of mathematics has to be reformulated. This is of great use, because then the step to programs is direct and one can expect to get the best programs. However, it seems that most mathematicians will continue to work in set theory. Even when changing to type theory for the formalisation, usually the proofs will be developed first having classical set theory in the background. Therefore methods for transferring directly set theoretical arguments to type theory could make the step from traditional mathematics to type theory and therefore to computer science far easier.

The reason why set theory is used in mathematics is its high flexibility and that it allows to write down expressions without having to care about the type of the object. Therefore, if set theoretical proofs can be transferred to type theory, one could use set theory as a programming language added to type theory.

In our definition of KP I_{U}^{+} only natural numbers are included as urelemente, which form the basic data structure, for which programs can be extracted. However, the method used is not at all restricted to this particular structure. Lists and free algebras can be included easily and we are working on an extension to data structures of higher type.

Π_{2}^{0}-sentences can be considered as specifications of programs, and proofs in Martin-Löf’s Type Theory are programs. In this abstract we will prove, that all Π_{2}^{0}-sentences provable in a certain set theory KP I_{U}^{+} = ⋃_{n∈ℕ} KP I_{U}^{+}_{n} can be proved in ML_{1}W, Martin-Löf’s Type Theory with W -type and one universe. KP I_{U}^{+} is Kripke Platek set theory with urelemente (the natural numbers), one admissible (admissible are the recursive analogue of cardinals) closed under the step to the next admissible (a recursive inaccessible) and finitely many admissibles above it. This works for all variations (intensional, extensional, different versions of the identity type). Since, in [Se93] we have shown, that all arithmetical sentences provable in ML_{1}W are theorems of KP I_{U}^{+}, it follows, that these two theories have the same Π_{2}-theorems. Therefore, transferring programs to ML_{1}W from proof theoretically stronger set theories is no longer possible.

The method used here is certainly feasible, the only exception is the well ordering proof, which will be used here, and seems to be too long for practical applications. However, one can think about conservative extensions of ML_{1}W by adding types, the elements of which represent ordinal denotations, and rules for transfinite induction. Then everything shown here can be easily implemented in Martin-Löf’s Type Theory.

We use here techniques from proof theory. These are based on ordinal analysis. However, very basic knowledge about ordinals is sufficient for understanding this proof, since we are just formalising a proof, which need not be understood itself.

Our method is heavily built on transfinite induction. In [Se95] the author has shown, that ML_{1}W shows transfinite induction up to the ordinals ψ_{Ω_{1}}(Ω_{I+n}), therefore as well up to α_{n} := ψ_{Ω_{1}}(ϵ_{Ω_{I+n}+1}) + 1. Transfinite induction up to α_{n} is exactly what we need in order to analyse KP I_{U}^{+}_{n}. Now it is just necessary to formalise this analysis in ML_{1}W using, that we have transfinite induction up to α_{n}, and to extract the validity of Π_{2}^{0}-sentences from the cut free proofs.

This formalisation is not trivial, since in modern methods (like Buchholz’ H-controlled derivations), proof theoretical analysis is carried out in full set theory. However, using proof trees with a correctness predicate, we are able to overcome this difficulty.

The methods used here can on one hand extended to all recent proof theoretical studies using infinitary derivations and ordinal analysis. Only, the type theory is not available yet, except for Mahlo universes. (For Mahlo, the author presented a type theory on the Logic Colloquium ’95 in Haifa, there is related work by Rathjen and Griffor). Further, one sees easily, that the well-foundedness of the W -type is not needed really here, since we have always a descent in ordinals. (For the RS^{∗}-derivations, ||Γ|| is descending). Therefore, by replacing the W -type by a recursive object obtained using the recursion theorem, (so I becomes now a not necessarily least fixed point – one naturally has to replace in the proof of lemma 7 f by a list coded as a natural number) which can be defined in P RA, one shows with nearly the same proof, that P RA + T I(OT_{n}) shows all Π_{2}-sentences of KP I_{U}^{+}.

Independently, W. Buchholz has taken a different approach for obtaining the same result, by using denotation systems (extending [Bu91]). This has the advantage of giving directly executable programs, whereas our method has the advantage of being very perspicuous and explicit.

The other approach for extracting programs from classical proofs are based on the Atranslation. This can even be carried out for full set theory, as shown by Friedman (a good presentation can be found in [Be85] section VIII.3). A lot of research is carried out for extracting practical programs using the A-translation, see for instance [BS95] or [Sch92]. However, since Martin-Löf’s Type Theory is already a programming language, we believe, that our approach allows to switch more easier between classical proofs and direct programming. Further, in KP I_{U}^{+} one has constructions corresponding precisely to the different type constructors in type theory, so with our method we have good control over the strength of the methods used.

2 General Assumptions

Assumption 1 (a) We assume some coding of sequences of natural numbers. < k_{0}, …, k_{l} > denotes the sequence k_{0}, …, k_{l} and (k)_{i} the i-th element (beginning with i = 0) of the sequence k.

(b) In the following we will omit the use of Gödel-brackets.

(c) Let n_{0} : N be fixed.

Definition 2 (a) Let OT be defined as in [Se95], definition 3.9. We define OT_{n_{0}} by: O, I ∈ OT_{n_{0}}. If α, β ∈ OT_{n_{0}}, γ =′_{NF} α + β ∨ γ =_{NF} ϕ_{α}β ∨ γ =_{NF} Ω_{γ} ∨ γ =_{NF} ψ_{β}γ, γ ∈ OT ∩ ϵ_{Ω_{I+n_{0}}+1}, then γ ∈ OT_{n_{0}}. In the following α, β, γ denote elements of OT_{n_{0}}.

(b) We restrict the ordering ≺ on OT to OT_{n_{0}} (replace ≺ by ≺ ∩OT_{n_{0}} × OT_{n_{0}})

(c) Let ML_{1}W be Martin-Löf’s Type Theory with W -type and one universe, as for instance formulated in [Se95], or any other formulation (for instance we can use the the identity type together with the elimination operator).

(d) For arithmetical sentences ϕ, let ϕ̂ the canonical interpretation of ϕ in ML_{1}W.

Theorem 3 If ML_{1}W ⊢ n : N ⇒ ϕ(n) type, then ML_{1}W ⊢ ∀k ∈ OT_{n_{0}}.((∀l ≺ k.ϕ(k)) → ϕ(l)) → ∀k ∈ OT_{n_{0}}.ϕ(k).

Proof: Let W′ := W_{n_{0}+1} as in [Se95], definition 5.37. Then OT_{n_{0}} ⊂ W′. Let ψ(x) := x ∉ OT_{n_{0}} ∨ ϕ(x). Then P rog(W_{0}, (x)ψ(x)), ∀k ∈ W_{0}.ψ(k), and the assertion.

3 The set theory KP I_{U}^{+}_{n}

Definition 4 of the theory Kpi_{u}^{+}

(a) The language of KP I_{U}^{+}_{n_{0}} consists of infinitely many number variables, infinitely many set variables, symbols for finitely many primitive recursive relations (on natural numbers) P of arbitrary arity, the relations Ad, \overline{Ad}, ∈ and ∉ (the latter are written infix) and the logical symbols ∧, ∨, ∀, ∃.

In the following n, m denote number variables and a, b, c denote set variables, to which we might add (this will apply to all future such conventions) indices, tildesymbol or accents.

an, bn, cn, am, bm, cm denote variables, which are either set variables or number variables.

We assume that that P_{=}, the 2-ary equalitybetween two natural numbers, ⊥, the 0ary false relation, and for every primitive recursive relation P, the negation of this relation \overline{P} are in the set of primitive recursive relations. ⊤ := \overline{⊥}.

(b) Number terms are S^{k}(0) and S^{k}(n), where k ∈ ℕ, S^{0}(r) := r, S^{k+1}(r) := S(S^{k}(r)). sn and tn denote number terms. The set terms are the set variables.

We define val(S^{k}(0)) := k.

(c) Prime formulas are P (tn_{1}, …, tn_{k}), where P is an k-ary primitive recursive relation symbol, Ad(a), \overline{Ad}(a), s ∈ a, s ∉ a.

(d) Formulas are prime formulas, and if ϕ and ψ are formulas then ϕ ∧ ψ, ϕ ∨ ψ, ∀a.ϕ, ∀n.ϕ, ∃a.ϕ, ∃n.ϕ are formulas. ϕ, ψ denote formulas in the following.

(e) We define the negation of a formula by the deMorgan rules: ¬P (tn_{1}, …, tn_{k}) := \overline{P} (tn_{1}, …, tn_{k}), ¬(s ∈ a) := s ∉ a, ¬Ad(a) := \overline{Ad}(a), ¬(ψ ∧ ϕ) := ¬(ψ) ∨ ¬(ϕ), ¬(∀an.ϕ) := ∃an.¬ϕ, ¬(¬(ϕ)) := ϕ otherwise.

(f) ∀an ∈ b.ϕ := ∀an.an ∈ b → ϕ, ∃an ∈ b.ϕ := ¬(∀an ∈ b.¬ϕ).

(g) A formula is arithmetical, if it contains neither set terms nor set variables, Δ_{0}, if it contains only restricted set-quantifiers. It is in Σ_{1}, if it contains no unrestricted universal set quantifier, in Σ_{1}^{arith}, if it is arithmetical and contains no unrestricted universal number quantifier. The arithmetical Π_{2}^{0}-formulas are formulas ∀n.ϕ, ϕ ∈ Σ_{1}^{arith}. ϕ ∈ Σ(κ) :⇔ ϕ = ψ^{L_{κ}} for some ψ ∈ Σ_{1}. In this situation, ϕ^{t,κ} := ψ^{t}. Further ϕ^{β,κ} := ϕ^{L_{β},κ}. If ϕ is a formula, let ϕ^{a} be the result of replacing in ϕ every unrestricted set-quantifier (not number quantifier) ∀b by ∀b ∈ a, and ϕ^{β} := ϕ^{L_{β}}.

(h) ∀x.ϕ := (∀n.ϕ[x := n]) ∧ (∀a ∈ b.ϕ[x := a]), where ϕ[x := n] is the result of substituting for x n in ϕ, if the result is a formula, and ϕ[x := n] := ⊥ otherwise, similar for ϕ[a := n].

(i) Γ, Δ denote multi-sets of formulas. Γ, Δ := Γ ∪ Δ, Γ, ϕ := Γ ∪ {ϕ}.

(j) ϕ → ψ := ¬ϕ ∨ ψ, ϕ ⟺ ψ := (ϕ → ψ) ∧ (ψ → ϕ).

For number or set terms s, t we define: a ⊂ b := ∀x ∈ a.x ∈ b.

s = t := \{ \begin{matrix}P_{=}(s, t) & if s, t are number terms \\ s ⊂ t ∧ t ⊂ s∧ \\ (Ad(s) ⟺ Ad(t)) & if s, t are set terms \\ ⊥ & otherwise \end{matrix}

trans(a) := ∀b ∈ a.∀x ∈ b.x ∈ a.

(k) The logical rules are Γ, ϕ, ¬ϕ, \frac{Γ,ϕ Γψ}{Γϕ∧ψ}, \frac{Γ,ϕ}{Γϕ∨ψ}, \frac{Γ,ψ}{Γϕ∨ψ}, \frac{Γ,ϕ}{Γ,∀n.ϕ} (if n ∉ F V (Γ)), \frac{Γ,ϕ}{Γ,∀a.ϕ(a)}

(if a ∉ F V (Γ)), \frac{Γ,ϕ[n:=tn]}{Γ,∃n.ϕ}, \frac{Γ,ϕ[n:=a]}{Γ,∃a.ϕ}, and \frac{Γ,ϕ Γ¬ϕ}{Γ}.

(l) Axioms of KP I_{U}^{+}_{n_{0}} The set axioms are:

(Ext_{1})  ∀x.∀y.∀a.(x = y → x ∈ a → y ∈ a).
(Ext_{2})  ∀a.∀b.(a = b → Ad(a) → Ad(b)).
(F ound) ∀a⃗n.[∀a.(∀b ∈ a.ϕ(b, a⃗n))ϕ(a, a⃗n)] → ∀a.ϕ(a, a⃗n).
(P air)  ∀x, y.∃a.x ∈ a ∧ y ∈ a.
(Union) ∀a.∃b.∀y ∈ a.∀x ∈ y.(x ∈ b).
(Δ_{0} − Sep) ∀a⃗n∀a.∃b.[[∀x ∈ b.(x ∈ a ∧ ϕ(x, a⃗n))] ∧ [∀x ∈ a.(ϕ(x, a⃗n) → x ∈ b)]]
(Δ_{0} − Coll) ∀a⃗n.∀a.[∀x ∈ a.∃y.ϕ(x, y, a⃗n)] → ∃b.[∀x ∈ a.∃y ∈ b.ϕ(x, y, a⃗n)]
(Ad.1)  ∀a.Ad(a) → trans(a).
(Ad.2)  ∀a, b.((Ad(a) ∧ Ad(b)) → (a ∈ b ∨ a = b ∨ b ∈ a)).
(Ad.3)  ∀a.(Ad(a) → ϕ^{a}), where ϕ is an axiom (P air), (Union)
(Δ_{0} − Sep), (Δ_{0} − Coll).
(+)_{n_{0}}  ∃a, a_{1}, …, a_{n_{0}}.Ad(a) ∧ (∀x ∈ a.∃c ∈ a.(Ad(c) ∧ x ∈ c)) ∧

Ad(a_{1}) ∧ ⋯ ∧ Ad(a_{n_{0}}) ∧ a ∈ a_{1} ∧ a_{1} ∈ a_{2} ∧ ⋯ ∧ a_{n_{0}−1} ∈ a_{n_{0}} The arithmetical axioms are: Some formulas ∀n⃗.∃m⃗.ϕ(n⃗, m⃗), where ϕ is quantifier free and for some primitive recursive functions f_{1}, …, f_{l} ML_{1}W proves ∀k⃗ ∈ ℕ.ϕ(n⃗, f_{1}(k⃗), …, f_{l}(k⃗)). Additionally induction: ϕ(0) ∧ ∀n.(ϕ(n) → ϕ(S(n))) → ∀n.ϕ(n).

4 Formalisation of the infinitary system RS

Definition 5 We define the RS-terms and RS-formulas as follows:

(a) T_{ℕ} := {S^{k}(0) | k ∈ ℕ}. F OR_{ℕ} is the set of formulas in KP I_{U}^{+}_{n_{0}}.

(b) T_{α} := {L_{α}}∪ {[a ∈ L_{α} : ϕ(a)] ∪ [n ∈ ℕ : ψ(n)] | ϕ, ψ ∈ F OR_{α} ∧ (a ∈ F V (ϕ) ∨ n ∈ F V (ψ)) ∧ F V (ϕ) ⊂ {a} ∧ F V (ψ) ⊂ {n}}

F OR_{α} is the result of replacing in KP I_{U}^{+}_{n_{0}}-formulas set terms by elements of T_{≺α}, and restricting all unrestricted quantifiers to L_{α}. K(L_{α}) := {α}, K([a ∈ L_{α} : ϕ(a)] ∪ [n ∈ ℕ : ψ(n)]) := {α} ∪ K(ϕ) ∪ K(ψ). K(ϕ) := ⋃t setterm occurring in ϕ K(t), |r| := maxK(r) for r formula or term. F OR_{≺α} := {ψ | ψ ∈ F OR_{|ϕ|} ∧ |ϕ| ≺ α}, T_{α} := {t | t ∈ F OR_{|t|} ∧ |t| ≺ α}.

(c) F OR := ⋃{F OR_{α} | α ∈ OT_{n_{0}}}, F OR_{cl} := {ϕ ∈ F OR | F V (ϕ) = ∅}, F OR_{cl,a} := F OR_{cl} ∩ F OR_{α}, F OR_{cl,≺α} := F OR_{cl} ∩ F OR_{≺α}. T_{set} := ⋃{T_{α} | α ∈ OT_{n_{0}}}, T := T_{ℕ} ∪ T_{set}, T^{0,1} := T ∪ {0, 1}. In the following ra, sa, ta, ra, sa, ta denote elements of T_{set}, and r, s, t elements of T .

Note, that elements of T_{α}, F OR_{α}, T_{ℕ}, F OR_{ℕ} are finite objects, therefore we can implement this easily in Martin-Löf Type Theory.

Definition 6 (a) For s, t ∈ T such that |s| ≺ |t| we define s∈^{∘}t:

s∈^{∘}L_{α} := ⊤, sa∈^{∘}[a ∈ L_{α} : ϕ(a)] ∪ [n ∈ ℕ : ψ(n)] := ϕ[a := sa], sn∈^{∘}[a ∈ L_{α} :

ϕ(a)] ∪ [n ∈ ℕ : ψ(n)] := ψ[n := sn].

(b) We assign to formulas ϕ in F OR_{cl} expressions ϕ ≃ ⋀_{ι∈J} ϕ_{ι} or ϕ ≃ ⋁_{ι∈J} ϕ_{ι}, where J ⊂ T^{0,1}, as follows: If P (val(sn_{1}), …, val(sn_{k})) is false, then P (sn_{1}, …, sn_{k}) :≃ ⋁_{ι∈∅} ϕ_{ι}. (ϕ_{0} ∨ ϕ_{1}) := ⋁_{ι∈{0,1}} ϕ_{ι},

sa ∈ ta :≃ ⋁_{sb∈T_{|ta|}}(sb∈^{∘}ta ∧ sa = sb)

sn ∈ sa :≃ ⋁_{tn∈T_{ℕ}}(tn∈^{∘}sa ∧ sn = tn).

∃n.ϕ :=≃ ⋁_{sn∈T_{ℕ}} ϕ[sn] ∃a ∈ t.ϕ :≃ ⋁_{sa∈T_{|t|}}(sa∈^{∘}t ∧ ϕ[a := sa]).

Ad(s) :≃ ⋁_{t∈J}(t = s) with J := {L_{κ}|κ ∈ R ∧ κ ⪯ |s|}. In all other cases, we have for some J, ψ_{ι}, ¬ϕ ≃ ⋁_{ι∈J} ψ_{ι} and ϕ :≃ ⋀_{ι∈I}(¬ψ_{ι}).

If ϕ ≃ ⋁_{ι∈I} ϕ_{ι}, we call ϕ an ∨-formula, and if ϕ ≃ ⋀_{ι∈I} ϕ_{ι}, ϕ an ∧-formula. In both situations let Index(ϕ) := J, ϕ[ι] := ϕ_{ι}. Note, that we can primitive recursively decide, whether ϕ is an ∨ or ∧-formula, and for the J as above whether ι ∈ J. Further ϕ[ι] is primitive recursive in ϕ and ι.

We write ⋀_{ι∈J} ϕ_{ι} for any formula ϕ such that ϕ ≃ ⋀_{ι∈J} ϕ_{ι}, similar for ⋁_{ι∈J} ϕ_{ι}.

(c) We define rk(θ) for θ ∈ F OR_{cl} ∪ T by rk(L_{α}) := ω · (α + 1), rk([a ∈ L_{α} : ϕ] ∪ [n ∈ ℕ : ψ]) := max{ω · α + 1, rk(ϕ[a := L_{0}]), rk(ψ[n := 0])}, rk(Ad(t)) := rk(t) + 5, rk(sa ∈ t) := max{rk(sa) + 6, rk(t) + 1}, rk(∃a ∈ t.ϕ) := max{rk(t), rk(ϕ[a := L_{0}]) + 2}, rk(∃n.ϕ) := rk(ϕ[n := 0]) + 2, rk(ϕ_{0} ∨ ϕ_{1}) := max{rk(ϕ_{0}), rk(ϕ_{1})} + 1, rk(¬ϕ) := rk(ϕ) otherwise.

[Bu92], lemma 1.9 and definitions 1.10, 1.11, 1.12, 2.1. can be define accordingly. The α^{R} and ∥Γ∥ are primitive recursive functions.

Lemma 7 Assume ML_{1}W ⊢ B : N → P(N), (P(N) := N → U) ML_{1}W ⊢ Φ : N^{3} → U, ML_{1}W ⊢ Ψ : N → U. Let Γ : P(N) → P(N), Γ(B) := {k : N | Ψ(k) ∧ ∀l ∈ B(k).∃l′ ∈ I.Φ(k, l, l′)}. Then we can define I such that ML_{1}W ⊢ I : P(N), and we can prove in ML_{1}W: Γ(I) ⊂ I, and for every sub-class A of N we have Γ(A) ⊂ A → A ⊂ I.

Proof: Define W_{Γ} := W k : N.τ(k) with τ(k) := Σl : N.(l ∈ B(k)) (where here l ∈ B(k) is the proposition corresponding to the property l ∈ B(k)). Let for sup(k, s) : W_{Γ}, LocCor(sup(k, s)) := Ψ(k) ∧ ∀l : N.∀p : l ∈ B(k).Φ(k, l, index(s < l, p >)). Let index(sup(r, s)) := r, pred(sup(r, s)) := λx.sx. Define w ≺_{W}^{1} sup(k′, s) :⇔ ∃r : τ(k).sr = w. Let w ⪯_{W} w′ :⇔ ∃l : N.∃f : N → W_{Γ}.f0 = w′ ∧ fl = w ∧ ∀i < l.f(i + 1) ≺_{W}^{1} fi. Let for w : W_{Γ}, Cor(w) :⇔ ∀w′ ⪯_{W} w.LocCor(w′). Let I := λk.∃w : W_{Γ}.Cor(w) ∧ index(w) = k. Then one easily sees, that I fulfils the conditions of the theorem.

Definition 8 (a) As in [Bu92] we define the infinitary system RS^{∗} as the collection of all derivations generated by five inference rules:

(⋀)^{∗}  \frac{⋯ ⊢^{ρ} Γ, ϕ_{ι} ⋯ (ι ∈ J)}{⊢_{ρ} Γ, ⋀_{ι∈J} ϕ_{ι}}
(⋁)^{∗}  \frac{⊢_{ρ} Γ, ϕ_{ι_{0}}, …, ϕ_{ι_{k}}}{⊢_{ρ} Γ, ⋁_{ι∈J} ϕ_{ι}} (if ι_{0}, …, ι_{k} ∈ J ∧ K(ι_{0}, …, ι_{k}) ⊂ k(Γ, ⋁_{ι∈J} ϕ_{ι}))
(Ad)^{∗}  \frac{⋯ ⊢_{ρ} Γ, ϕ[a := L_{κ}] ⋯ (κ ⪯ |t|)}{⊢_{ρ} Γ, Ad(t) → ϕ[a := t]}, if rk(ϕ[a := L_{0}]) ≺ ρ
(Ref)^{∗} Γ, ϕ → ∃a ∈ L_{κ}.ϕ^{a,κ}, if ϕ ∈ Σ(κ) ∧ κ ∈ R ∧ ρ ≠ 0
(F ound)^{∗} Γ, ∃a ∈ L_{α}((∀b ∈ a.ϕ[a := b])∧ ϕ̸), ∀a ∈ L_{α}.ϕ ifρ ≠ 0.

(b) We formalise 1 in Martin-Löf Type Theory as follows:

In order to get unique predecessors, we replace the information on the nodes by sequences < rule, ρ, Γ >, where rule =< ⋀, ϕ > or rule =< ⋁, ϕ, iota_{0}, …, ι_{l} > or rule =< Ad, ϕ, a, s > or rule =< Ref, ϕ, a, κ > or rule =< F ound, ϕ, a, b, α >. Then, we have

B(<< ⋀, ϕ >, Γ >) := Index(ϕ), Ψ_{ρ}(<< ⋀, ϕ >, Γ >) := ϕ ∈ Γ ∧ ϕ ∧ −Formula, Φ(< ⋀, ϕ, Γ >, ι, p) := (p)_{1} = Γ \ ϕ ∪ {ϕ[ι]}. B(<< ⋁, ϕ, ι_{0}, …, ι_{l} >, Γ >) := Index(ϕ), Ψ_{ρ}(< ⋀, ϕ, ι_{0}, …, ι_{l} >, Γ >, p) := ϕ ∈ Γ ∧ ϕ ∨ −Formula ∧ι_{0}, …, ι_{l} ∈ J, Φ(< ⋀, ϕ, ι_{0}, …, ι_{l} >, Γ >, p) := (p)_{1} = Γ \ ϕ ∪ {ϕ[ι_{0}], …, ϕ[ι_{l}]}. The other rules are treated in a similar way.

Then with the set I_{ρ} as in 7 defined for B, Ψ_{ρ}, Φ, {(p)_{1}|p ∈ I} is the set of sequences derivable in RS, and we define ⊢_{ρ}^{∗} Γ :⇔ ∃p ∈ I_{ρ}.(p)_{1} = Γ.

(c) q ⊢_{ρ}^{∗} (index(q))_{1}.

q ⊢_{ρ}^{∗} Γ is now the formalisation of, what is defined in [Bu92] definition 2.3. q ⊢^{∗} Γ :⇔ q ⊢_{0}^{∗} Γ.

Lemmata and theorems 2.4 – 2.9 of [Bu92] follow now with nearly the same proofs. The only modifications to be made are, to define [s ≠ t], if either s or t is not a set-term, to add instances for the case A = P (n_{1}, …, n_{m}) in lemma 2.7. Further we can easily prove that for all arithmetical axioms ϕ, except the induction theorem we have ⊢^{∗} ϕ (here we need, that the m_{i} are primitive recursive in the n⃗, so we can easily define the proof). The only case, where we really have to work is to give a cut-free proof of the induction axiom, and the reader can easily find such a proof, so for every instance ϕ of the induction axiom we have ⊢^{∗} ϕ.

5 H-controlled derivations

Next step is to formalise H-controlled derivations. However, this is only necessary for operators H_{γ}[θ], where H_{γ} is defined in [Bu92], definition 4.3. Further, not that H_{γ}(X) is needed only for finite sets X. We formalise H_{γ} first:

Definition 9 (a) γ ∈ C(α, β) :⇔ γ ≺ β ∨ γ η {0, I} ∨ ∃δ, ρ.γ =′_{NF} δ + ρ ∨ γ =_{NF} Ω_{δ} ∨ (γ =_{NF} ψ_{δ}ρ ∧ ρ ≺ γ), where =_{NF} is defined as in definition 3.11 of [Se95]. C(α, β) can be defined easily as a primitive recursive set.

(b) For X being a finite subset of N we define H_{γ}(X) := {γ ∈ OT_{n_{0}} | ∀β, γ ∈ OT_{n_{0}}.(X ∩ OT_{n_{0}} ⊂ C(α, β) ∧ γ ≺ α) → γ ∈ C(α, β)}. Note that the condition X ∩ OT_{n_{0}} ⊂ C(α, β) is primitive recursive, since X is finite.

(c) H_{γ}[θ](X) := H_{γ}(k(θ) ∪ X).

α ∈ H_{γ}[θ] :⇔ α ∈ H_{γ}[θ](∅).

We check easily, that for C_{κ}(α), as defined in [Se95], definition 3.9., we have C_{κ}(α) = C(α, ψ_{κ}α). The properties in [Bu92], lemma 4.4 b - d, 4.5 - 4.7 follow now directly from the properties of the ordinal denotation system in [Se95].

Definition 10 (see theorem 3.8 of [Bu92]).

Inductive definition of H_{γ}[θ] ⊢_{ρ}^{α} Γ: Assume {α} ⊂ k(Γ) ⊂ H_{γ}[θ]. Then we can conclude H_{γ}[θ] ⊢ Γ, iff one of the following cases holds: (⋀) ⋀_{ι∈J} ϕ_{ι} ∈ Γ ∧ ∀ι ∈ J.∃α_{ι} ≺ α.(H[θ, ι] ⊢_{ρ}^{α_{ι}} Γ, ϕ_{ι}) (⋁) ⋁_{ι∈J} ϕ_{ι} ∈ Γ ∧ ∃ι_{0} ∈ J.∃α_{0} ≺ α.(H[θ] ⊢_{ρ}^{α_{0}} Γ, ϕ_{ι_{0}} ∧ ι_{0} η J ∩ (α + 1)) (Cut) rk(ψ) ≺ ρ ∧ ∃α_{0} ≺ α.(H[θ] ⊢_{ρ}^{α_{0}} Γ, ψ ∧ H[θ] ⊢_{ρ}^{α_{0}} Γ, ¬ψ). (Ref) ∃z ∈ L_{κ}.ϕ^{(a,κ)} ∈ Γ ∧ H[θ] ⊢_{ρ}^{α_{0}} Γ, ϕ ∧ α_{0} + 1 ≺ α ∧ ϕ ∈ Σ(κ) ∧ κ ∈ R.

One sees easily, that we can formalise H-controlled derivations in a similar way as in definition 8. Now in [Bu92] lemma 3.9, 3.13 - 3.17 with H replaced by H_{γ}[θ] and by omitting all conditions on H (we are fulfilled), and lemma 3.10, 3.11 with H replaced by H_{γ} and again by omitting conditions on H, further lemma 4.7, theorem 4.8 and the corollary, follow with the same proofs and can be formalised in ML_{1}W. Theorem 3.12 reads now as follows:

Theorem 11 For each theorem ϕ of KP I_{U}^{+}_{n_{0}} there exists an m < ω such that with λ := Ω_{I+m} for all γ H_{γ} ⊢_{λ+m}^{ω^{λ+m}} ϕ^{λ}.

Theorem 12 For every arithmetical formula ϕ, if Kpi_{n_{0}}^{+} ⊢ ϕ, then H_{β} ⊢^{γ} for some γ ≺ ϵ_{Ω_{I+n_{0}}+1}.

Proof: Let λ := Ω_{I+n_{0}}. From Kpi_{n_{0}}^{+} ⊢ ϕ follows by 12 H_{0} ⊢_{λ+m}^{ω^{λ+m}} ϕ, by [Bu92] 3.12 (adapted to our setting) H_{0} ⊢_{λ+1}^{α} ϕ for some α ≺ ϵ_{λ+1}, by [Bu92] 4.8 Hα̂0 ⊢_{ψ_{Ω_{1}} α̂}^{ψ_{Ω_{1}} α̂} ϕ with α̂ := ω^{λ+1+α_{0}} ≺ ϵ_{λ+1}, by

[Bu92] 3.12 with γ := ϕ_{ψ_{Ω_{1}} α̂}(ψ_{Ω_{1}} α̂) ℵα̂ ⊢_{0}^{β} ϕ, let β := α̂.

Lemma 13 If H_{ρ}[θ] ⊢_{ρ}^{α} Γ, ⋀_{ι∈J} ϕ_{ι}, then H_{ρ}[θ, ι] ⊢_{ρ}^{α} Γ, ϕ_{ι}.

Proof: If ϕ := ⋀_{ι∈J} ϕ_{ι} is not the main formula of the last premise, the assertion follows by IH and the same rule. Otherwise we have the case of last rule (⋀), H_{ρ}[θ, ι] ⊢_{ρ}^{α_{ι}} Γ, ϕ_{ι}, or H_{ρ}[θ, ι] ⊢_{ρ}^{α_{ι}} Γ, ϕϕ_{ι}, in which case by IH we conclude the first case. By [Bu92] lemma 3.9 (a) follows the assertion.

6 Result

Definition 14 We define a primitive recursive relation k rel l: e rel b is false, if b ∉ Σ_{1}^{arith}. e rel P (S^{k_{1}}(0), …, S^{k_{l}}(0)) ⇔ e = 0 ∧ P (k_{1}, …, k_{l}) where on the right side stands the primitive recursive relation corresponding to P. e rel ϕ ∧ ψ ⟺ ∃l, k.e =< l, k > ∧l rel ϕ ∧ k rel ψ. e rel ϕ ∨ ψ ⟺ ∃l, k.(e =< l, k > ∧((l = 0 ∧ krellϕ) ∨ (l = 1 ∧ k rel ψ))). e rel ∃n.ϕ ⟺ ∃l, k.e =< l, k > ∧k rel ϕ[n := S^{l}(0)].

e rel ϕ_{1}, …, ϕ_{n} :⇔ e rel ϕ_{1} ∨ ⋯ ∨ ϕ_{n}.

Lemma 15 (a) For every formula ϕ ∈ Σ_{1}^{arith}, F V (ϕ) ⊂ {m_{1}, …, m_{l}}. ML_{1}W ⊢ ∀k_{1}, …, k_{l}.((n rel ϕ[m_{1} := S^{k_{1}}(0), …, m_{l} := S^{k_{l}}(0)]) → ϕ̂[m_{1} := k_{1}, …, m_{l} := k_{l}]), where the latter is the formula in ML_{1}W.

(b) ∀Γ ∈ Σ_{1}^{arith}.∀α, ρ, δ.H_{ρ}[θ] ⊢_{0}^{α} Γ → ∃n.n rel Γ.

Proof: b: by an easy induction on the rules. Note that only the rules (⋁) and (⋀) occur.

Theorem 16 Let ϕ = ∀n.ψ, ψ ∈ Σ_{1}^{arith}. Assume KP I_{U}^{+}_{n_{0}} ⊢ ϕ. Then ML_{1}W ⊢ ϕ̂.

Proof: By 12 follows H_{ρ} ⊢_{0}^{α} ϕ. Assume k : N. Then by 13 follows H_{ρ} ⊢_{0}^{α} ψ[n := S^{k}(0)]. Then by lemma 15 follows ψ̂[m := k], therefore ∀m.ψ.

Corollary 17 ML_{1}W proves the consistency of KP I_{U}^{+}_{n}.

References

[Be85] Beeson, M.: Foundations of Constructive Mathematics Springer, Berlin, 1985

[BS95] Berger, U. and Schwichtenberg, H.: Program Extraction from Classical Proofs. To appear in Proceedings of the LCC conference,1995

[Bu91] Buchholz, W.: Notation systems for infinitary derivations. Arch. Math. Logic (1991) 30:277-296.

[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.

[Sch92] Schwichtenberg, H.: Proofs as programs. In:Aczel, P. et al. (Eds.): Proof Theory. Cambridge University Press, Cambridge, 1992, pp. 81 – 113.

[Se93] Setzer, A.: Proof theoretical strength of Martin-Löf Type Theory with W-type and

one  universe.  PhD-thesis,  Munich,  1993.

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

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

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