Translating Set Theoretical Proofs into Type Theoretical Programs

Anton Setzer

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

                         email: setzer@math.uu.se

Abstract. We show how to translate proofs of Π_{2}^{0}-sentences in the fragment of set theory KPI_{U}^{+}, which is an extension of Kripke-Platek set theory, into proofs of Martin-Löf’s Type Theory using a cut elimination argument. This procedure is effective. The method used is an implementation of techniques from traditional proof theoretic analysis in type theory. It follows that KPI_{U}^{+} and ML_{1}W show the same Π_{2}^{0}-sentences and have therefore the same programs. As a side result we get that Π_{2}^{0}- sentences provable in intensional and extensional version of ML_{1}W are the same, solving partly a problem posed by M. Hofmann.

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 the step to programs is direct and one can expect to obtain good programs, provided we have an implementation of Martin-Löf’s as a real programming language. However, it seems that many mathematicians will continue to work in set theory. Even when changing to type theory for the formalization, often the proofs will be developed first having classical set theory in the background.

The advantage of set theory is that it is highly flexible – e.g. there are no problems with subtyping – and that it allows to write down expressions without having to care about the type of the objects. Therefore methods for transferring directly set theoretical arguments into type theory could not only make the step from traditional mathematics to type theory easier, but as well help to program in type theory.

Π_{2}^{0}-sentences can be considered as specifications of programs and proofs of such sentences in Martin-Löf’s Type Theory are implementations of such programs. In this article we will prove that all Π_{2}^{0}-sentences provable in the Kripke-Platek style set theory KPI_{U}^{+} are theorems of ML_{1}W, Martin-Löf’s Type Theory with W-type and one universe as well. KPI_{U}^{+} is Kripke Platek set theory with urelemente (the natural numbers), one admissible (admissibles are the recursive analogues of cardinals) closed under the step to the next admissible (a recursive inaccessible) and finitely many admissibles above it. The translation works for the usual variations of type theory (intensional vs. extensional, different formulations of the identity type). Since in [Se93] we have shown that all arithmetical sentences provable in ML_{1}W are theorems of KPI_{U}^{+} it follows that KPI_{U}^{+} and ML_{1}W (and the variations of ML_{1}W) have the same Π_{2}-theorems. Therefore we solve at the same time at least partly a question posed by M. Hofmann in a talk given in Munich, whether the Π_{2}^{0}-sentences of extensional and intensional type theory are the same.

It follows that transferring programs to ML_{1}W from proof theoretically stronger set theories is no longer possible, therefore our result is the best possible.

Our method is heavily built on transfinite induction. In [Se97] the author has shown that ML_{1}W proves 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 analyze KPI_{U,n}^{+} (KPI_{U}^{+} = ⋃_{n∈ω} KPI_{U,n}^{+}). Now it is just necessary to formalize 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.

We use here techniques from proof theory. These are based on the ordinal analysis of KPI as formalized by Buchholz in [Bu92]. Although it is very difficult to understand these cut elimination arguments, we think that it is not crucial to have full insight in what is going on there in order to be able to work with the techniques presented in this article.

The main problem we had to overcome for writing this article was to formalize modern proof theoretical methods (Buchholz’ H-controlled derivations), which are carried out in full set theory, in type theory. We solved this problem using proof trees with a correctness predicate.

Extensions of the result. The methods used here can be extended to all recent proof theoretical studies using infinitary derivations and ordinal analysis. Only, the type theory is not available yet in all cases, except for Mahlo universes. (For Mahlo, the author has given a formulation in [Se96]). Further, one can see easily that the well-foundedness of the W-type is not needed really here, since we have always a descent in ordinals assigned to the nodes of the tree. (For the RS^{∗}-derivations, ||Γ || is descending). Therefore, by replacing the W-type by a recursive object obtained using the recursion theorem, which can be defined in PRA, one shows with nearly the same proof that PRA + TI(OT_{n}) and KPI_{U,n}^{+} have the same Π_{2}-theorems.

The restriction to arithmetical Π_{2}^{0}-sentences is not crucial. The quantifiers in such sentences could range as well over bigger sets like lists, free algebras or sets built using Σ and sums. We have in this article added to KPI_{U}^{+} natural numbers as urelemente. By adding the types mentioned before as urelemente as well the proofs should go through without essential modifications.

Practicability It should not be too complicated to program the method used here directly in type theory, 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 of 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.

Other approaches. Independently, W. Buchholz has taken a different approach for obtaining the same result, by using denotation systems for derivations (extending [Bu91]). He uses transfinite induction as well. His approach 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 A-translation. This can even be carried out for full set theory, as shown by Friedman (a good presentation can be found in [Be85] Sect. 1VIII.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 easily between classical proofs and direct programming. Further, in KPI_{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) In type theory a class is an expression {x | ϕ} such that we can prove x ∈ N ⇒ ϕ set, and s η {x | ϕ} := ϕ[x := s]. We identify primitive recursive sets with the class corresponding to it.

(d) In type theory, let P(N) := N → U. For A ∈ P(N), a ∈_{U} A := T(A(u)) (where T(s) is the set represented by an element s ∈ U).

We introduce OT, the set of ordinal notations as in [Se97]:

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

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

(c) Let ML_{1}W be Martin-Löf’s Type Theory with W-type and one universe, as for instance formulated in [Se97] (we can use other formulations of the identity type as well).

(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}.((∀l ≺ k.ϕ(k)) → ϕ(l)) → ∀k η OT_{n}.ϕ(k).

Proof: Let W′ := W_{n+1} as in [Se97], Definition 5.37. Then OT_{n_{0}} ⊂ W′. Let ψ(x) := x η OT_{n} → ϕ(x). Then Prog(W_{0}, (x)ψ(x)), ∀k ∈ W_{0}.ψ(k) and we get the assertion.

3 The Set Theory KPI_{U,n}^{+}

We introduce an extension of Kripke-Platek set theory KPI_{U,n}^{+}. The best references for this theory are [Ba75] which is an excellent introduction to Kripke-Platek set theory and [Jä86], in which Kripke-Platek set theory is extended by adding a predicate for admissibles – the recursive analogue of regular cardinals – and many variations of such theories are analyzed proof theoretically. Our definition is in the spirit of [Jä86] and adds axioms, which assert the existence of one inaccessible I (which is an admissible closed under the step to the next admissible) and finitely many admissibles above it.

Definition 4. of the theory KPI_{U,n}^{+}

(a) The language of KPI_{U,n}^{+} consists of infinitely many number variables, infinitely many set variables, symbols for finitely many primitive recursive relations (on the natural numbers) P of arbitrary arity (the corresponding primitive recursive relation is denoted by P̃), the relations Ad, \overline{Ad}, ∈ and ∉ (the latter are written infix) and the logical symbols ∧, ∨, ∀, ∃. In the following x^{nat}, y^{nat}, z^{nat}, u^{nat}, v^{nat} denote number variables and x^{set}, y^{set}, … denote set variables, to which we might add (this will apply to all future such conventions) indices or accents. x^{?}, y^{?}, … denote either a set or a number variable. In a formula, we will omit the superscripts nat, set and ? after the first occurrence of the variable. We assume that P_{=} (the equality of natural numbers), P_{<} (the <-relation on IN) ⊥ (the 0-ary false relation) are represented in the languge and that for every primitive recursive relation P represented in the language, the negation of this relation \overline{P} is represented as well. ⊤ := \overline{⊥}.

(b) Number terms are S^{k}(0) and S^{k}(x^{nat}), where k ∈ IN, S^{0}(r) := r, S^{k+1}(r) := S(S^{k}(r)). The set terms are the set variables. r^{nat}, s^{nat} and t^{nat} denote number terms. The superscript will be omitted again after the first occurrence. We define val(S^{k}(0)) := k.

(c) Prime formulas are P(t_{1}^{nat}, …, t_{k}^{nat}), where P is a symbol for a k-ary primitive recursive relation (the correspongind relation will be denoted by P̃), Ad(x^{set}), \overline{Ad}(x^{set}), r^{set} ∈ y^{set}, r^{nat} ∈ y^{set}, r^{set} ∉ y^{set}, r^{nat} ∉ y^{set}.

(d) Formulas are prime-formulas, and, if ϕ and ψ are formulas, then ϕ∧ψ, ϕ∨ψ, ∀x^{?}.ϕ, ∃x^{?}.ϕ are formulas, too.

(e) We define the negation of a formula by the de Morgan rules:

¬P(t_{1}^{nat}, …, t_{k}^{nat}) := \overline{P}(t_{1}^{nat}, …, t_{k}^{nat}), ¬(r ∈ y^{set}) := r ∉ y, ¬Ad(x^{set}) := \overline{Ad}(x), ¬(ψ∧ϕ) := ¬(ψ)∨¬(ϕ), ¬(∀x^{?}.ϕ) := ∃x^{?}.¬ϕ, ¬(¬(ϕ)) := ϕ otherwise. The set of free variables FV(A) of a formula A is defined as usual.

(f) ϕ → ψ := ¬ϕ ∨ ψ, ϕ ↔ ψ := (ϕ → ψ) ∧ (ψ → ϕ). ∀x^{?} ∈ y^{set}.ϕ := ∀x^{?}.x ∈ y^{set} → ϕ, ∃x^{?} ∈ y^{set}.ϕ := ∃x^{?}.x ∈ y^{set} ∧ ϕ. x^{set} ⊂ y^{set} := (∀u^{nat} ∈ x.u ∈ y) ∧ (∀z^{set} ∈ x.z ∈ y), x^{set} = y^{set} := (x ⊂ y ∧ y ⊂ x ∧ (Ad(x) ↔ Ad(y))). r^{nat} = s^{nat} := P_{=}(r, s), r < s := P_{<}(r, s). trans(x^{set}) := ∀y^{set} ∈ x.((∀u^{nat} ∈ y.u ∈ x) ∧ (∀z^{set} ∈ y.z ∈ x)).

(g) The quantifier ∀x^{set} in front of a formula ϕ is bounded, if ∀x.ϕ can be written as ∀x^{set} ∈ y^{set}.ψ, similarly for ∃x^{set}. Quantifieres over number variables are always bounded.

(h) A formula is arithmetical, if it contains neither set terms nor set variables; it is a Σ_{1}^{arith}-formula, if it is arithmetical and all sub-formulas starting with universal number quantifiers are of the form ∀x^{nat}.x^{nat} < s^{nat} → ϕ; it is an arithmetical Π_{2}^{0}-formula, if it is of the form ∀x^{nat}.ϕ where ϕ is a Σ_{1}^{arith}- formula. A formula is Δ_{0}, if it contains only bounded set-quantifiers. It is Σ_{1}, if it contains no unbounded universal set-quantifiers. If ϕ is a formula, let ϕ^{y^{set}} be the result of replacing in ϕ every unbounded setquantifier ∀ ∃x^{set}.ψ by ∀ ∃x^{set} ∈ y^{set}.ψ (note that number quantifiers remain unchanged).

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

(j) The logical rules of KPI_{U,n}^{+} are

Γ, ϕ, ¬ϕ  \frac{Γ, ϕ Γ ψ}{Γ ϕ ∧ ψ}  \frac{Γ, ϕ}{Γ ϕ ∨ ψ}  \frac{Γ, ψ}{Γ ϕ ∨ ψ}
\frac{Γ, ϕ}{Γ, ∀x^{?}.ϕ} (if x ∉ FV(Γ))  \frac{Γ, ϕ[x^{nat} := t^{nat}]}{Γ, ∃x^{nat}.ϕ}  \frac{Γ, ϕ[x^{set} := y^{set}]}{Γ, ∃x^{set}.ϕ}

\frac{Γ, ϕ Γ, ¬ϕ}{Γ}.

(k) Axioms of KPI_{U,n}^{+} ∀z^{?} stands in the following for ∀z_{1}^{?}, …, z_{l}^{?} for some l. The set axioms are

(Ext_{1}) ∀x^{set}, y^{set}, z^{set}.(x = y → x ∈ z → y ∈ z) ,
∀x^{nat}, y^{nat}, z^{set}.(x = y → x ∈ z → y ∈ z) .
(Ext_{2}) ∀x^{set}.∀y^{set}.(x = y → Ad(x) → Ad(y)) .
(Found) ∀z^{?}.[(∀x^{set}.(∀y^{set} ∈ x^{set}.ϕ(y, z⃗)) → ϕ(x, z⃗)) →
∀x^{set}.ϕ(x, z⃗)] .
(Pair) ∀x^{?}, y^{?}.∃z^{set}.x ∈ z ∧ y ∈ z .
(Union) ∀x^{set}.∃y^{set}.∀z^{set} ∈ x.((∀u^{nat} ∈ z.(u ∈ y)) ∧
(∀v^{set} ∈ z.(v ∈ y))) .
(Δ_{0} − Sep) ∀z^{?}.∀x^{set}.∃y^{set}.[[∀u^{nat} ∈ y.ϕ_{nat}(u, z⃗))] ∧
[∀v^{set} ∈ y.v ∈ x ∧ ϕ_{set}(v, z⃗))] ∧

[∀u^{nat}.(ϕ_{nat}(u, z⃗) → u ∈ y)] ∧
[∀v^{set} ∈ x.(ϕ_{set}(v, z⃗) → v ∈ y)]]
where ϕ_{nat} and ϕ_{set} are Δ_{0}-formulas .
(Δ_{0} − Coll) ∀z^{?}.∀x^{set}.[(∀y^{nat} ∈ x.∃v^{set}.ϕ_{nat}(y, v, z⃗)) ∧
(∀u^{set} ∈ x.∃v^{set}.ϕ_{set}(u, v, z⃗))] → ∃w^{set}.
[(∀y^{nat} ∈ x.∃v^{set} ∈ w.ϕ(y, v, z⃗)) ∧
(∀u^{set} ∈ x.∃v^{set} ∈ w.ϕ(u, v, z⃗))]
where ϕ_{nat} and ϕ_{set} are Δ_{0}-formulas .
(Ad.1) ∀x^{set}.Ad(x) → (trans(x) ∧ x ≠ ∅) .
(Ad.2) ∀x^{set}, y^{set}.((Ad(x) ∧ Ad(y)) →
(x ∈ y ∨ x = y ∨ y ∈ x)) .
(Ad.3) ∀x^{set}.(Ad(x) → ϕ^{x}), where ϕ is an instance of an axiom
(Pair), (Union), (Δ_{0} − Sep) or (Δ_{0} − Coll) .
(+)_{n} ∃x^{set}, x_{1}^{set}, …, x_{n}^{set}.Ad(x) ∧
(∀y ∈ x.∃z^{set} ∈ x.(Ad(z) ∧ y ∈ z)) ∧
Ad(x_{1}) ∧ ⋯ ∧ Ad(x_{n}) ∧
x ∈ x_{1} ∧ x_{1} ∈ x_{2} ∧ ⋯ ∧ x_{n−1} ∈ x_{n} .

The arithmetical axioms are: Some formulas ∀x^{nat}.∃y^{nat}.ϕ(x⃗, y⃗), where ϕ is quantifier free and for some primitive recursive functions f_{1}, …, f_{l} ML_{1}W proves ∀k⃗ ∈ IN.ϕ̂(n⃗, f_{1}(k⃗), …, f_{l}(k⃗)). Additionally induction: ϕ(0) ∧ ∀x^{nat}.(ϕ(x) → ϕ(S(x))) → ∀x^{nat}.ϕ(x).

(l) KPI_{U}^{+} is the union of all theories KPI_{U,n}^{+} (n ∈ ω).

4 Formalization of the Infinitary System RS

Let from now on be n_{0} ∈ ω fixed. As in [Bu92], we introduce set terms indexed by variables, where [x^{set} ∈ L_{α} : ϕ(x)] stands for the the set {x ∈ L_{α} | ϕ(x)}, and [x^{nat} : ϕ(x)] for {x ∈ IN | ϕ(x)} (RS stands for ramified set theory):

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

(a) T_{nat} := {S^{k}(0) | k ∈ IN}.

(b) We define inductively simultaneously for all α ∈ OT_{n_{0}} the sets of terms T′_{α} and of formulas FOR′_{α} by: L_{α} ∈ T′_{α}. If ϕ, ψ ∈ FOR′_{α} and x^{set} ∈ FV(ϕ) ∨ y^{nat} ∈ FV(ψ), then [x ∈ L_{α} : ϕ^{L_{α}}] ∪ [y : ψ^{L_{α}}] ∈ T′_{α}. If r, s ∈ T′_{α}, t ∈ T′_{nat}, then r ∈ s, r ∉ s, t ∈ s, t ∉ s, Ad(r), \overline{Ad}(r) ∈ FOR′_{α}. If ϕ, ψ ∈ FOR′_{α}, then ϕ ∧ ψ, ϕ ∨ ψ, ∀x^{?}.ϕ, ∃x^{?}.ψ ∈ FOR′_{α}.

Here the free variables FV(A) of A ∈ T′_{α} or A ∈ FOR′_{α} and ϕ^{r} are defined as usual or before.

(c) T_{α} := {t ∈ T′_{α} | FV(t) = ∅}, FOR_{α} := {A ∈ FOR′_{α} | FV(A) = ∅}. T_{set} := ⋃_{α∈OT_{n_{0}}} T_{α}, T := T_{set} ∪ T_{nat}, FOR := ⋃_{α∈OT_{n_{0}}} FOR_{α}. The elements of FOR are called RS-formulas. An RS-formula is Δ_{0}, if it contains no unbounded set-quantifiers, Σ_{1}, if it contains no unbounded universal set-quantifiers, and Σ(α), if it is of the form ψ^{L_{α}}[x_{1}^{set} := t_{1}, …, x_{n}^{set} := t_{n}] for some Σ_{1}-formula ψ of KPI_{U,n_{0}}^{+} and some t_{i} ∈ T_{≺α}. In the last situation ϕ^{t,α} := ψ^{t}. Further ϕ^{β,α} := ϕ^{L_{β},α}, ϕ^{β} := ϕ^{L_{β}}.

(d) FOR^{Δ_{0}} := {ϕ ∈ FOR | ϕ Δ_{0}-formula}, FOR_{α}^{Δ_{0}} := FOR^{Δ_{0}} ∩ FOR_{α}.

(e) For t ∈ T , A ∈ FOR we define K(t), K(A) ⊂ OT_{n_{0}}:

K(t^{nat}) := ∅. K(L_{α}) := {α}, K([x^{set} ∈ L_{α} : ϕ] ∪ [y^{nat} : ψ]) := {α} ∪ K(ϕ) ∪ K(ψ). K(A) is the union of K(t) for all terms t ∈ T which occur A. |A| := max K(A) for A ∈ FOR ∪ T .

(f) In the following r^{set}, s^{set}, t^{set} denote elements of T_{set}, and r^{?}, s^{?}, t^{?} elements of T_{set} ∪ T_{nat}.

Note that elements of T and FOR are finite objects, which can be coded easily in Martin-Löf Type Theory in such a way that all the above mentioned sets, relations and functions are primitive recursive.

In order to assign infinitary formulas to s^{?} ∈ t^{set} we define first the auxiliary formula s^{?}∈^{∘}t^{set}:

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

s∈^{∘}L_{α} := ⊤,

s^{set}∈^{∘}[x^{set} ∈ L_{α} : ϕ(x)] ∪ [y^{nat} : ψ(y)] := ϕ[x := s], s^{nat}∈^{∘}[x^{set} ∈ L_{α} : ϕ(x)] ∪ [y^{nat} : ψ(y)] := ψ[y := s].

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

r^{set} ∈ s^{set} :≃ ⋁_{t^{set}∈T_{≺|s|}}(t∈^{∘}s ∧ t = r) .

r^{nat} ∈ s^{set} :≃ ⋁_{t^{nat}∈T_{nat}}(t∈^{∘}s ∧ t = r) .

∃x^{nat}.ϕ(x) :=≃ ⋁_{s^{nat}∈T_{nat}} ϕ(s) .

∃x^{set} ∈ t^{set}.ϕ :≃ ⋁_{s^{set}∈T_{≺|t|}}(s∈^{∘}t ∧ ϕ[x := s]) .

Ad(s^{set}) :≃ ⋁_{t^{set}∈J}(t = s) with J := {L_{κ}|κ ∈ R ∧ κ ⪯ |s|} . In all other cases, we have for some J, ψ_{ι}, ¬ϕ ≃ ⋁_{ι∈J} ψ_{ι} and define ϕ :≃ ⋀_{ι∈J}(¬ψ_{ι}). If ϕ ≃ ⋁_{ι∈J} ϕ_{ι}, we call ϕ an ∨-formula, and if ϕ ≃ ⋀_{ι∈J} ϕ_{ι}, ϕ 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 θ ∈ FOR ∪ T by rk(L_{α}) := ω · (α + 1), rk([x^{set} ∈ L_{α} : ϕ] ∪ [y^{nat} : ψ]) := max{ω · α + 1, rk(ϕ[x := L_{0}]) + 2, rk(ψ[y := 0]) + 2}, rk(Ad(t^{set})) := rk(t) + 5, rk(s^{?} ∈ t^{set}) := max{rk(s) + 6, rk(t) + 1}, rk(∃x^{set} ∈ t.ϕ) := max{rk(t), rk(ϕ[x := L_{0}]) + 2}, rk(∃x^{nat}.ϕ) := rk(ϕ[x := 0]) + 2, rk(ϕ_{0} ∨ ϕ_{1}) := max{rk(ϕ_{0}), rk(ϕ_{1})} + 1, rk(¬ϕ) := rk(ϕ) otherwise.

[Bu92], Lemma 1.9 and Definitions 1.11, 1.12, 2.1. can be shown and defined accordingly. The functions α ↦ α^{R} and Γ ↦ ∥Γ ∥ (considered as functions on the codes) are primitive recursive.

Lemma 7. Assume ML_{1}W ⊢ B ∈ N → P(N), ML_{1}W ⊢ Φ ∈ N^{3} → U, ML_{1}W ⊢ Ψ ∈ N → U. Let Γ ∈ P(N) → P(N), Γ (M) := {k ∈ N | Ψ(k) ∧ ∀l ∈_{U} B(k).∃l′ ∈_{U} M.Φ(k, l, l′)}. (the interpretation is that B(k) is the set of predecessors of a node k, Ψ(k) is the condition at every nodes, and Φ(k, l, l′) is the condition relating a node with its predecessors). Then we can define 𝕀 such that ML_{1}W ⊢ 𝕀 ∈ P(N), and we can prove in ML_{1}W: Γ (𝕀) ⊂ 𝕀, and for every subclass A of N we have Γ (A) ⊂ A → A ⊂ 𝕀.

Proof: Define W_{Γ} := Wk ∈ N.τ(k) with τ(k) := Σl ∈ N.(l ∈_{U} B(k)). Let for sup(k, s) ∈ W_{Γ}, index(sup(r, s)) := r, pred(sup(r, s), a) := s(a), LocCor(sup(k, s)) := Ψ(k) ∧ ∀l ∈ N.∀p ∈ (l ∈_{U} B(k)).Φ(k, l, index(s(<l, p>))). Define w ≺_{W}^{1} sup(k′, s) :⇔ ∃r ∈ τ(k).s(r) = w. Let w ⪯_{W} w′ :⇔ ∃l ∈ N.∃f ∈ N → W_{Γ} .f(0) = w′∧f(l) = w∧∀i < l.f(i+1) ≺_{W}^{1} f(i). Let for w ∈ W_{Γ}, Cor(w) :⇔ ∀w′ ⪯_{W} w.LocCor(w′). Let 𝕀 := {k | ∃w ∈ W_{Γ} .Cor(w) ∧ index(w) = k}. Then one easily sees that 𝕀 fulfills 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 (ϕ, ϕ_{ι} ∈ FOR^{Δ_{0}}, Γ ⊂ FOR^{Δ_{0}}):

(⋀)^{∗}  \frac{⋯ ⊢^{ρ} Γ, ϕ_{ι} ⋯ (ι ∈ J)}{⊢_{ρ} Γ, ⋀_{ι∈J} ϕ_{ι}}
(⋁)^{∗}  \frac{⊢_{ρ} Γ, ϕ_{ι_{0}}, …, ϕ_{ι_{k}}}{⊢_{ρ} Γ, ⋁_{ι∈J} ϕ_{ι}} (if ι_{0}, …, ι_{k} ∈ J and

K(ι_{0}, …, ι_{k}) ⊂ K(Γ, ⋁_{ι∈J} ϕ_{ι}))^{∗}

(Ad)^{∗} \frac{⋯ ⊢_{ρ} Γ, ϕ[x^{set} := L_{κ}] ⋯ (κ ⪯ |t^{set}|)}{⊢_{ρ} Γ, Ad(t) → ϕ[x := t]}, if rk(ϕ[a := L_{0}]) ≺ ρ
(Ref)^{∗} Γ, ϕ → ∃x^{set} ∈ L_{κ}.ϕ^{x,κ}, if ϕ ∈ Σ(κ) ∧ κ ∈ R ∧ ρ ≠ 0
(Found)^{∗} Γ, ∃x^{set} ∈ L_{α}((∀y^{set} ∈ x.ϕ[z := y]) ∧ ¬ϕ[z := x]),

∀x^{set} ∈ L_{α}.ϕ[z := x] if ρ ≠ 0.

(More precisely (⋀)^{∗} should be read as: if ϕ ≃ ⋀_{ι∈J} ϕ_{ι}, then

\frac{⋯ ⊢^{ρ} Γ, ϕ_{ι} ⋯ (ι ∈ J)}{⊢_{ρ} Γ, ϕ} is a rule etc.)

(b) We formalize (a) 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 is of the form < ⋀, ϕ>, < ⋁, ϕ, ι_{0}, …, ι_{l}>, <Ad, ϕ, x, t^{set}, κ>, <Ref, ϕ, x, κ> or <Found, ϕ, x, y, z, α>. We want to apply Lemma 7 to B, Ψ_{ρ}, Φ. We define B(<< ⋀, ϕ>, Γ >) := Index(ϕ), Ψ_{ρ}(<< ⋀, ϕ>, Γ >) := ϕ ∈ Γ ∧ ϕ ∧ −Formula, Φ(< ⋀, ϕ, Γ >, ι, p) := (((p)_{1} = (Γ \ {ϕ}) ∪ {ϕ[ι]}) ∨ ((p)_{1} = Γ ∪ {ϕ[ι]})). B(<< ⋁, ϕ, ι_{0}, …, ι_{l}>, Γ >) := {0}, Ψ_{ρ}(<< ⋁, ϕ, ι_{0}, …, ι_{l}>, Γ >) := ϕ ∈ Γ ∧ ϕ ∨ −Formula ∧

ι_{0}, …, ι_{l} ∈ J ∧ K(ι_{0}, …, ι_{k}) ⊂ K(Γ, ⋁_{ι∈J}, ϕ)^{∗}, Φ(<< ⋁, ϕ, ι_{0}, …, ι_{l}>, Γ >, ι, p) := (((p)_{1} = (Γ \ {ϕ}) ∪ {ϕ[ι_{0}], …, ϕ[ι_{l}]})∨

((p)_{1} = Γ ∪ {ϕ[ι_{0}], …, ϕ[ι_{l}]}. The other rules are treated in a similar way. Then with the set 𝕀_{ρ} as in Lemma 7 defined for B, Ψ_{ρ}, Φ, {(p)_{1}|p ∈ 𝕀} is the set of sequences derivable in RS, and we define ⊢_{ρ}^{∗} Γ :⇔ ∃p ∈ 𝕀_{ρ}.(p)_{1} = Γ.

(c) 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^{nat} ≠ t^{nat}] and to add instances for the case A = P(t_{1}^{nat}, …, t_{m}^{nat}) in Lemma 2.7. Further we can easily prove that for all arithmetical axioms ϕ, except the induction theorem we have ⊢^{∗} ϕ^{λ}. The only case, where some work is necessary 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

The next step is to formalize H-controlled derivations as in [Bu92]. However, this is only necessary for operators H_{γ}[θ], where H_{γ} is defined in [Bu92], Definition 4.3. Further note that H_{γ}(X) is needed only for finite sets X. We formalize H_{γ} first:

Definition 9. (a) γ ∈ C(α, β) :⇔ γ ≺ β ∨ γ η {0, I} ∨ ∃δ, ρ ∈ C(α, β).γ =′_{NF} δ + ρ ∨ γ =_{NF} Ω_{δ} ∨ (γ =_{NF} ψ_{δ}ρ ∧ ρ ≺ α), where =_{NF} is defined as in Definition 3.11 of [Se97]. 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 [Se97], 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 [Se97].

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} ⪯ α) . (Cut) rk(ψ) ≺ ρ ∧ ∃α_{0} ≺ α.((H_{γ}[θ] ⊢_{ρ}^{α_{0}} Γ, ψ) ∧ (H_{γ}[θ] ⊢_{ρ}^{α_{0}} Γ, ¬ψ)). (Ref) (∃z^{set} ∈ L_{κ}.ϕ^{(z,κ)}) ∈ Γ ∧(H_{γ}[θ] ⊢_{ρ}^{α_{0}} Γ, ϕ)∧α_{0}+1 ≺ α∧ϕ ∈ Σ(κ)∧κ ∈ R.

One sees easily that we can formalize 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 (which 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 formalized in ML_{1}W. Theorem 3.12 reads now as follows:

Theorem 11. For every theorem ϕ of KPI_{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_{U,n_{0}}^{+} ⊢ ϕ, then H_{β} ⊢^{γ} ϕ for some γ ≺ ϵ_{Ω_{I+n_{0}} +1}.

Proof: Let λ := Ω_{I+n_{0}}. From KPI_{U,n_{0}}^{+} ⊢ ϕ follows by Theorem 11 H_{0} ⊢_{λ+m}^{ω^{λ+m}} ϕ, by [Bu92] 3.16 (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.16 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 e rel l, where l is considered as the code of a formula of RS-formula (and Gödel-brackets are omitted): e rel l is false, if l is not the code of a Σ_{1}^{arith}-formula. e rel P(S^{k_{1}}(0), …, S^{k_{l}}(0)) ⇔ e = 0 ∧ P̃(k_{1}, …, k_{l}). e rel ϕ ∧ ψ ↔ ∃l, k.e = <l, k> ∧ l rel ϕ ∧ k rel ψ. e rel ϕ ∨ ψ ↔ ∃l, k.(e = <l, k> ∧ ((l = 0 ∧ k rel ϕ) ∨ (l = 1 ∧ k rel ψ))). e rel ∃x^{nat}.ϕ ↔ ∃l, k.e = <l, k> ∧ k rel ϕ[x := S^{l}(0)].

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

Lemma 15. (a) For every formula ϕ ∈ Σ_{1}^{arith} such that FV(ϕ) ⊂ {x_{1}^{nat}, …, x_{l}^{nat}} we have ML_{1}W ⊢ ∀k_{1}, …, k_{l} ∈ N.∀n ∈ N.((n rel ϕ[x_{1} := S^{k_{1}}(0), …, x_{l} := S^{k_{l}}(0)])

→ ϕ̂[x_{1} := k_{1}, …, x_{l} := k_{l}]).

(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 ϕ = ∀x^{nat}.ψ, ψ ∈ Σ_{1}^{arith}. Assume KPI_{U,n_{0}}^{+} ⊢ ϕ. Then ML_{1}W ⊢ ϕ̂.

Proof: By Theorem 11 follows H_{ρ} ⊢_{0}^{α} ϕ. Assume k ∈ N. By Lemma 13 follows H_{ρ} ⊢_{0}^{α} ψ[x := S^{k}(0)]. Then by Lemma 15 follows ψ̂[x := k], therefore ∀x.ψ.

Corollary 17. ML_{1}W proves the consistency of KPI_{U,n_{0}}^{+}.

References

[Ba75] Barwise, J.: Admissible Sets and Structures. An Approach to Definability Theory, Springer, 1975.

[Be85] Beeson, M.: Foundations of Constructive Mathematics Springer, Berlin, 1985 [BS95] Berger, U. and Schwichtenberg, H.: Program Extraction from Classical Proofs.

In: D. Leivant (Ed.): Logic and Computational Complexity, LCC ’94, Indianapolis, October 1994, Springer Lecture Notes in Computer Science 960, pp. 77–97.

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

[Jä86] Jäger, G.: Theories for Admissible Sets: A Unifying Approach to Proof Theory.

Bibliopolis, Naples, 1986.

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

[Se96] Setzer, A.: Extending Martin-Löf Type Theory by one Mahlo-Universe. Submitted.

[Se97] Setzer, A.: Well-ordering proofs for Martin-Löf Type Theory with W-type and one universe. Submitted.