A Type Theory for Iterated Inductive Definitions

Anton Setzer Department of Pure Mathematics, University of Leeds Leeds LS2 9JT email pmt6ans@leeds.ac.uk

9/iii/1994

Abstract

We introduce a type theory F A_{ω}, which has at least the strength of finitely iterated inductive definitions ID_{<ω}. This type theory has as ground types trees with finitely many branching degrees (so called free algebras). We introduce an equality in this theory, without the need for undecidable prime formulas. Then we give a direct well-ordering proof for this theory by representing a ordinal denotation system in the iteration of Kleene’s O. This can be easily done, by introducing functions on the trees, which correspond to the functions in the ordinal denotation system. The proof shows, that F A_{ω} proofs transfinite induction up to D_{0}D_{n}0, which shows, that the strength of F A_{ω} is at least ID_{<ω}. It seems to be obvious, that this bound is sharp.

1 Definition of the type theory F A_{ω}

Definition 1.1 The type theory F A_{ω} is defined as follows:

(a) The ground types are defined inductively by:

If n ≥ 0 and α_{1}, …, α_{n} are ground types, then (α_{1}, …, α_{n}) is a ground type.

The type (α_{1}, …, α_{n}) should be the type of well-founded trees with branching degrees α_{1}, …, α_{n}.

(b) Ground types are types, and if α, β are types then (α → β) is a type.

We will omit brackets, using the usual conventions.

(c) If α = (α_{1}, …, α_{n}) is a ground type, then for i = 1, …, n C_{i}^{α} is a constant of type (α_{i} → α) → α (C_{i}^{α} are the constructors for this type) and if α is as before and σ a type, then we have the recursion constant R_{α,σ} of type

((α_{1} → α) → (α_{1} → σ) → σ) → ⋯ → ((α_{n} → α) → (α_{n} → σ) → σ) → α → σ

We will write (C_{1} : α_{1}, …, C_{n} : α_{n}) for (α_{1}, …, α_{n}) to indicate, that C_{i} are names for C_{i}^{α}.

(d) The terms are the typed lambda terms, built using the constants of (c). We write t^{σ} for a term t of type σ.

(e) Special groundtypes are the empty type \underline{0} := () with no constructors and ex falsum quodlibet EF Q_{σ} := R_{\underline{0},σ} of type \underline{0} → σ, (we will omit the index σ, if it is clear from the context) the type of booleans bool := \underline{2} := (\underline{0}, \underline{0}) with special terms true := C_{1}^{bool}EF Q_{bool} and false := C_{2}^{bool}EF Q_{bool} of type bool.

(f) We have as reduction rules α, β and η-reduction and the rules for the recursion-constants (α = (α_{1}, …, α_{n})) R_{α,σ}s_{1} ⋯ s_{n}(C_{i}f) →_{red} s_{i}f(λx.R_{α,σ}s_{1} ⋯ s_{n}(fx)), where x is a new variable, which will be applied to subterms as well.

(g) We will identify terms, that are equivalent using these reduction-rules and write s ≃ t, if we identify two terms. Therefore ≃ is the transitive, reflexive and symmetric closure of the reduction-relation →_{red}.

Note, that [Ber94] proofs strong normalization for an extension of this type theory.

(h) The formulas are atom(t^{bool}) where t is a term of type bool and if ϕ, ψ are formulas, x a variable of type σ, then ϕ → ψ, ϕ ∧ ψ and ∀x^{σ}.ϕ are formulas.

We define ⊥:= atom(false), ¬ϕ := ϕ →⊥.

(i) We have the rules of intuitionistic logic. The axioms are atom(true) and induction over ground types: If α = (α_{1}, …, α_{n}) is a ground type, ϕ(x) a formula, then we have the axiom (∀f^{α_{1}→α}.(∀x^{α_{1}}ϕ(fx)) → ϕ(C_{1}f)) → ⋯ → (∀f^{α_{n}→α}.(∀x^{α_{n}}ϕ(fx)) → ϕ(C_{n}f)) → ∀x^{α}ϕ(x).

Definition 1.2 Further we have the following special types:

(a) The types with n elements \underline{n} := (C_{0}^{1} : \underline{0}, …, C_{n−1}^{1} : \underline{0}).

k_{n} := C_{k}^{n}EF Q\underline{n}.

(b) For the booleans we define \underline{if}\underline{then}\underline{else}_{σ}: B → σ → σ → σ, written \underline{if}_{σ} r \underline{then} s \underline{else} t for \underline{if}\underline{then}\underline{else}_{σ} rst, (we omit the σ usually) \underline{if}\underline{then}\underline{else}_{σ}:= λx, y, z.R_{\underline{2},σ}(λu, v.y)(λu, v.z)z, therefore \underline{if} tt \underline{else} s \underline{then} t →_{red}s, \underline{if} ff \underline{else} s \underline{then} t →_{red}t. This allows us to define a function on the booleans by case distinction on, wether a term is true or false.

(c) A boolean predicate P (x_{1}^{α_{1}}, …, x_{n}^{α_{n}}) is a formula atom(fx_{1} ⋯ x_{n}) where f : α_{1} → ⋯ → α_{n} → bool. In this case (P (t_{1}, …, t_{n}))_{bool} := ft_{1} ⋯ t_{n}. We will usually not mention f in the definition of boolean predicates. Therefore, if we say: “we define a prediacte P (x^{α}) by induction on x^{α}”, and define further “P (C_{i}^{α}g) iff Q(g) for some boolean property Q”, we mean, the following: we define a function f : α → bool by induction on α, such that f(C_{i}^{α}g) := (Q(g))_{bool}, and define P (t) := atom(ft).

Note, that negation, disjunction and conjunction of boolean predicates is a boolean predicate, since we have boolean functions ¬_{B} : bool → bool, ∨_{B} : bool → bool → bool, ∧_{B} : bool → bool → bool.

(d) \underline{ω} := (C_{0}^{ω} : \underline{0}, C_{1}^{ω}\underline{1}). We have the zero of type \underline{ω} 0_{ω} := C_{1}^{ω}EF Q, an the successor function succ_{ω} := λx.C_{1}^{ω}(λy.x), of type \underline{ω} → \underline{ω}.

We intruduce some basic predicates and functions: Definition 1.3 Let α = (C_{1} : α_{1}, …, C_{n}α_{n}).

(a) We define the boolean predicate τ_{α}(t) = α_{i} by recursion on t : α. (More precisely, if several of the types are identical, we have to use a name α̃_{i} for each type α_{i}, such that for i ≠ j α̃_{i} ≠ α̃_{j}, and have to write τ_{α}(t) = α̃_{i}, but want to keep the notation simple): τ_{α}(C_{i}f) = α_{i} is true, and τ_{α}(C_{j}f) = α_{i} is false, if j ≠ i.

We will usually omit the index α and write τ(t) ≠ α_{j} for ¬(τ(t) = α_{j}).

(b) We define ·[·]_{α_{i}}^{α} : α → α_{i} by recusion on α, (C_{i}f)[s]_{α_{i}}^{α} := fs, (C_{j}f)[s]_{α_{i}}^{α} := C_{j}f, if j ≠ i. If we have τ(a) = α_{i}, than by a[s] stands for a[s]_{α_{i}}^{α}.par

(c) We define pred_{α_{i}}^{α} : α → (α_{i} → α) by recursion, pred_{α_{i}}^{α}(C_{i}f) := f, pred_{α_{i}}^{α}(C_{j}f) := λx.(C_{j}f), if j ≠ i.

We have to distinguish between empty and non empty types, in order to define dummy elements of non empty types. The empty types are those, which are built of non empty types. Definition 1.4 (a) We define the Meta-predicate “α is empty” for ground-types α by induc-

tion on the definition of α:

If α = (α_{1}, …, α_{n}), then α is empty iff all α_{i} are not empty.

(b) We define for empty ground types α and arbitrary type γ the function EF Q_{σ}^{α} : α → σ, and for not empty ground types α an element dummy_{α} : α, simultaneously by Meta-induction on the types:

If α = (C_{1} : α_{1}, …, C_{n}α_{n}) is not empty, i minimal such that α_{i} is empty then dummy_{α} := C_{i}EF Q^{α_{i}}α, and if α is empty, we define by recursion EF Q_{σ}^{α}t for t : α: EF Q_{σ}^{α}(C_{i}f) := EF Q_{σ}^{α}(f dummy_{α_{i}}), which is possible, since α_{i} is not empty. The last arguments allows as well to prove ∀x^{α}. ⊥, by replacing the recursion by induction.

Definition 1.5 We will introduce lists as functions \underline{ω} → α. Assume α is a ground-type.

(a) list(α) := \underline{ω} → α.

(b) nil_{α} := λx.dummy_{α}, defined only, if α is not empty.

(c) car_{α} := λx.(x0_{ω}) of type list(α) → α.

(d) cdr_{α} := λx.λy.x(succ y) of type list(α) → list(α).

(e) We define cons_{α} : α → list(α) → list(α), cons xyn is defined by induction on n : \underline{ω}: cons xy0 := x, cons xy(succ t) := yt.

(f) (·)_{·,α} : list(α) → \underline{ω} → α, (f)_{i,α} := fi.

Remark 1.6 car(cons s^{α}t^{list(α)}) ≃ s, cdr(cons s^{α}t^{list(α)}) ≃ t. Proof: car(cons st) ≃ (cons st)0 ≃ s, cdr(cons st) ≃ λx.(cons st)(succ x) ≃ λx.tx ≃ t.

2 Definition of the equality

The idea for the well-ordering proof is, to reduce it to the well-ordering on our trees. We want to show

(∀x ∈ OT_{n}.(∀y ≺ τ(x).y ∈ OT_{n} → ϕ(x[y])) → ϕ(x)) → ∀x ∈ OT_{n}.ϕ(x).

by defining

ψ(x^{\underline{Ω}^{n+1}}) := ∀y ∈ OT_{n}.ι_{OT,n}y = x → ϕ(x).

and using now transfinite induction over the type \underline{Ω}_{n+1} (which is the nth iteration of Kleene’s O). But in order to do this, we need an equality in our system. But we do not want any undecidable prime formulas in our theory (see [Sch92] for some discussion about it), therefore we have to work hard to do this. An element of a ground type α is a tree, which has, if α = (α_{1}, …, α_{n}), branching degrees α_{1}, …, α_{n}. Now the idea is, that two terms are equal, if, whenever we go by a path in both trees to subtree, we have nodes, which are locally equal: they have the same constructor. Therefore we need to define the paths, which may consist of elements of the branching degrees. We will define a concept s[l_{1}^{list(α_{1})}, …, l_{k}^{list(α_{k})}; m^{ω}], the intended meaning being, that we go m times to the predecessor, starting at s, selecting the branch, which corresponds to the first element of the list of type list(α_{i}), if we have branching degree α_{i}. If the type α_{k} is empty, we will stop with this process. Further we introduce local equality =_{α}^{loc}. Definition 2.1 Assume α = (C_{1} : α_{1}, …, C_{n} : α_{n}). W.l.o.g. α_{1}, …, α_{k} are not empty, α_{k+1}, …, α_{n} are empty.

(a) We define ·[·, …, ·; ·]_{α} : α → list(α_{1}) → ⋯ → list(α_{k}) → \underline{ω} → α. We define a[l_{1}, …, l_{k}; m] by recursion on m, side-recursion on a:

a[l_{1}, …, l_{k}; C_{0}^{ω}f] := a,

if i ≤ k we define

(C_{i}f)[l_{1}, …, l_{k}; C_{1}^{ω}f] := (f car(l_{i}))[l_{1}, …, l_{i−1}, cdr(l_{i}), l_{i+1}, …, l_{k}; , f0_{1}]

and if k < i we have

(C_{i}f)[l_{1}, …, l_{k}; C_{1}^{ω}f] := C_{i}f,

We will write a[l⃗; m] for a[l_{1}, …, l_{k}; m], and ∀x^{list(α)} for ∀x_{1}^{list(α_{1})}, …, x_{n}^{list(α_{n})}.

(b) We define the boolean predicate s^{α} =_{α}^{loc} t^{α} by recursion on s and side-recursion on t: C_{i}f =_{α}^{loc}, C_{j}g iff i = j.

The definition of the equality will be a little bit more complicated, than it seems at first sight. We will not be able to prove ∀f^{α→β}.x^{α} =_{α} y^{α} → (fx) =_{β} (fy). All terms, we can construct, will fulfill this condition. We will call functions respectful, if they have this condition. Now this implies, that we need some notion of respectfulness on ground terms as well: We want, that in each occurrence of C_{i}f, we have f is respectful. Now we want only to check equality, using respectful lists. Therefore we have to define simultaneously for all ground types α the predicate Resp_{α}(t^{α}) for t is respectful, and the equality s^{α} =_{α} t^{α} for s and t are equal elements of type α. Definition 2.2 We define simultaneously for all ground types the predicate Resp_{α}(t^{α}), the predicate s^{α} =_{α} t^{α} and Resplist_{α}(l^{list(α)}) (an auxiliary definition for l is a respectful list) and Locresp_{α}(t^{α}) (for t is locally respectful). Assume α = (C_{1} : α_{1}, …, C_{n} : α_{n}), w.l.o.g. α_{1}, …, α_{k} not empty, α_{k+1}, …, α_{n} empty. We write Resplist_{α}(x⃗) for Resplist_{α_{1}}(x_{1}) ∧ ⋯ ∧ Resplist_{α_{k}}(x_{k}).

(a) s^{α} =_{α} t^{α} is defined as ∀x^{list(α)}, m^{ω}.Resplist_{α}(x⃗) → s[x⃗; m] =_{α}^{loc} t[x⃗; m].par

(b) Locresp_{α}(t) := ⋀_{i=1,...,n}(τ(t) = α_{i} → ∀x^{α_{i}}, y^{α_{i}}.Resp_{α_{i}}(x) → x =_{α_{i}} y → t[x] =_{α} t[y]).

(c) Resp_{α}(t) := ∀x^{list(α)}, m^{ω}(Resplist_{α}(x⃗) → Locresp_{α}(t[x⃗; m]).

(d) Resplist_{α}(l) := ∀n\underline{ω}.Resp_{α}((l)_{n})).

We will now characterize the equality: Lemma 2.3 Assume α is a ground type.

(a) ∀x^{α}, y^{list(α)}.Resp(x) → Resplist(y) → Resplist(cons xy)).

(b) ∀x^{list(α)}.Resplist(x) → (Resp(car x) ∧ Resplist(cdr x)).

Proof: trivial. Lemma 2.4 (a) =_{α} and =_{α}^{loc} are equivalence relations (for ground-types α).

(b) If α is not empty, then Resp(dummy_{α}), and Resplist(nil_{α}). Proof:(a): For =_{α}^{loc} this follows by induction on the type α, for =_{α} by Meta-induction on the definition of the ground-types. (b): We have Locresp_{α}(dummy_{α}), since τ(dummy_{α}) ≠ α_{j} for not empty types α_{j}. Now follows by induction on n^{ω}, Locresp(dummy[x⃗; n]): In both cases i = 0, 1 we have dummy[x⃗; C_{i}f] ≃ dummy, therefore Locresp(dummy[x⃗; C_{i}f]. Resplist(nil_{α}) follows now directly.

We charactrize equality and Resp(t) as follows: Lemma 2.5 Assume α = (C_{1} : α_{1}, …, C_{n} : α_{n}), f, g : α_{i} → α, h : α_{j} → α, r, s : α. W.l.o.g. α_{1}, …, α_{k} are not empty, α_{k+1}, …, α_{n} are empty.

(a) ¬(C_{i}f =_{α} C_{j}h), if i ≠ j.

(b) C_{i}f =_{α} C_{i}g ↔ ∀x^{α_{i}}.Resp(x) → fx =_{α} gx.

(c) Locresp_{α}(C_{i}f) ↔ allx^{α_{i}}, y^{α_{i}}.Resp(x) → x = y → fx =_{α} fy.

(d) Resp_{α}(C_{i}f) ↔ (Locresp_{α}(C_{i}f) ∧ ∀x^{α_{i}}.Resp(x) → Resp(fx)).

(e) If α_{i} is empty, then C_{i}f =_{α} C_{i}g, Locresp(C_{i}f), Resp(C_{i}f).

(f) s =_{α} t → ((Locresp(s) ↔ Locresp(t)) ∧ (Resp(s) ↔ Resp(t))).

Proof: Let n⃗il := nil_{α_{1}}, …, nil_{α_{k}}. Then we have Resplist(n⃗il). (a): If C_{i}f =_{α} C_{j}g, then, C_{i}f[n⃗il; 0] =_{α}^{loc} C_{j}g[n⃗il; 0], C_{i}f[n⃗il; 0] ≃ C_{i}f, C_{i}g[n⃗il; 0] ≃ C_{i}g, therefore i = j.

(b) Case α_{i} is not empty: Assume C_{i}f = C_{i}g and x^{α_{i}}, Resp(x), and l⃗^{list(α)}, m^{ω}, Resplist(l⃗). Then Resplist(cons xl_{i}), therefore

(fx)[l⃗; m] ≃ (f(car (cons xl_{i})))[l_{1}, …, cdr (cons xl_{i}), …, l_{k}; m]
≃ (C_{i}f)[l_{1} …, cons xl_{i}, …, l_{k}; succ m]
=_{α}^{loc} (C_{i}g)[l_{1} …, cons xl_{i}, …, l_{k}; succ m]
≃ (gx)[l⃗; m],

therefore fx =_{α} gx. If we have the r.h.s. l⃗^{list(α)}, Resplist(l⃗), then we have: If m = C_{0}g, (C_{i}f)[l_{1} … l_{k}; m] ≃ C_{i}f =_{α}^{loc} C_{i}g ≃ (C_{i}g)[l_{1} … l_{k}; m]. If m = C_{1}g, Resp(car l_{i}), Resplist(cdr l_{i}), therefore

(C_{i}f)[l_{1} … l_{k}; m] ≃ (f(car l_{i}))[l_{1}, …, cdr l_{i}, …, l_{k}; g0]
=_{α}^{loc} (g(car l_{i}))[l_{1}, …, cdr l_{i}, …, l_{k}; g0]
≃ (C_{i}g)[l_{1} … l_{k}; m]

Case α_{i} is empty: Assume C_{i}f = C_{i}g l⃗^{list(α)}, m^{ω}, Resplist(l⃗). Then we have, in both cases r = 0, 1 and m = C_{r}g, (C_{i}f)[l_{1} … l_{k}; m] ≃ C_{i}f =_{α}^{loc} C_{i}g ≃ (C_{i}g)[l_{1} … l_{k}; m]. Therefore C_{i}f =_{α} C_{i}g, and ∀x_{i}^{α}. ⊥, therefore the r.h.s. as well. (c): Follows, in case α_{i} is not empty, since (C_{i}f)[x] ≃ fx by definition. If α_{i} is empty, then we have Locresp(C_{i}f), and the r.h.s. follows from ex falsum quodlibet. (d): Follows as (a), (b). (e): Follows from the proofs above. (f): Follows from (a), (b), (c), (d) by induction on s and t.

We can then define the equality on arbitrary types as follows: Definition 2.6 We define =_{α} and Resp_{α} for all types by induction on the definition. For ground types we have already defined it. Let α = β → γ.

(a) f^{α} =_{α} g^{α} iff ∀x^{β}, Resp_{β}(x) → fx =_{γ} gx.

(b) Resp_{α}(f^{α}) iff ∀x^{β}, y^{β}.Resp_{β}(x) → x =_{β} y → (fx =_{γ} fy ∧ Resp_{γ}(fx).

We have now:

Lemma 2.7 (a) =_{α} is an equivalence relation on types.

(b) s =_{α} t → (Resp(s) ↔ Resp(t))).

(c) For every constructor C and every recursion constant R we have Resp(C), Resp(R) and if s^{α→β}, t^{α} are terms, then Resp(s) → Resp(t) → Resp(st).

(d) For every term t with free varibles among x_{1}^{α_{1}}, …, x_{n}^{α_{n}} we have

∀x_{1}, …, x_{n}, x′_{1}, …, x′_{n}.Resp(x_{1}) → ⋯ → Resp(x_{n}) → x_{1} = x′_{1} → ⋯ → x_{n} = x′_{n} →

Resp(t) ∧ t(x_{1}, …, x_{n}) = t(x′_{1}, …, x_{n}).

Proof: (a): Easy. (b): Follows by Meta-induction on the definition of types. (c): If C : (β → α) → α, and f, g : β → α, Resp(f), f =_{α} g, then ∀x.Resp(x) → fx = gx, therefore Cf = Cg, and we have Resp(Cf). If R = R_{α,σ}, α = (C_{1} : α_{1}, …, C_{n} : α_{n}), and we have s_{i}, s′_{i} : ((α_{i} → α) → (α_{i} → σ) → σ), Resp(s_{i}), s_{i} = s′_{i}, we have to show ∀x^{α}, x^{′α}.Resp(x) → x = x′ → (Rs_{1} ⋯ s_{n}x = Rs_{1} ⋯ s_{n}x′ ∧ Resp(Rs_{1} ⋯ s_{n}x)). We show this by induction on x, x′. Assume x = C_{i}f, x′ = C_{j}f′. If i ≠ j, then x ≠ x′, and if i = j, then by Resp(x) and x = x′ follows Resp(f), Resp(x′), Resp(f′), and by IH (since

∀y^{α_{i}}, y′^{α_{i}}.Resp(y) → y = y′ → (Resp(fy) ∧ fy = fy′ ∧ fy = f′y)

for all y^{α_{i}}, y′^{α_{i}}, with Resp(y), y = y′, we have Resp(Rs_{1} ⋯ s_{n}(fy)),

Rs_{1} ⋯ s_{n}(fy) = Rs_{1} ⋯ s_{n}(fy′),
Rs_{1} ⋯ s_{n}(fy) = Rs′_{1} ⋯ s′_{n}(f′y),

therefore Resp(λy.Rs_{1} ⋯ s_{n}(fy)),

λy.Rs_{1} ⋯ s_{n}(fy) = λy.Rs′_{1} ⋯ s′_{n}(f′y).

Now follows Resp(s_{i}f(λy.Rs_{1} ⋯ s_{n}(fy))), and

s_{i}f(λy.Rs_{1} ⋯ s_{n}(fy)) = s_{i}f′(λy.Rs′_{1} ⋯ s′_{n}(f′y)) = s′_{i}f′(λy.Rs′_{1} ⋯ s′_{n}(f′y)).

since

Rs_{1}, …, s_{n}(C_{i}f) ≃ s_{i}f(λy.Rs_{1} ⋯ s_{n}(fy))
Rs′_{1}, …, s′_{n}(C_{i}f′) ≃ s′_{i}f′(λy.Rs′_{1} ⋯ s′_{n}(f′y))

follows the assertion. Resp(st) is trivial.

(d) Follows immediately from (c) by induction on the defintion of terms. Notation 2.8 We write ∀x^{σ}; ϕ for “∀x^{σ}.Resp(x) → ϕ”. If we write “assume Resp(x^{σ})” we mean, “assume x^{σ}, assume Resp(x)” and if we write “for all respectful x^{σ}” we mean “for all x^{σ} such that Resp(x)”. Definition 2.9 (a) We define flat : \underline{ω} → \underline{ω} by recursion on \underline{ω}:

flat(C_{0}f) := zero, flat(C_{1}f) := succ(flat(f0)).

(b) We define the boolean predicate eqnat(x\underline{ω}, y\underline{ω}) by recursion on \underline{ω}:

eqnat(C_{0}f, C_{0}g) is true, eqnat(C_{0}f, C_{1}g) is false, eqnat(C_{1}f, C_{1}g) iff eqnat(f0, g0). Lemma 2.10 ∀x\underline{ω}, y\underline{ω}.Resp(flat(x)) ∧ (eqnat(x, y) → flat(x) = flat(y)).

Proof by induction on \underline{ω}, using, that Resp(0), Resp(succ) (since both are terms), therefore x = y → succ(x) = succ(y), Resp(x) → Resp(succx). Definition 2.11 We interpret n ary primitive recursive functions in F A_{ω} as functions \underbrace{\underline{ω} → ⋯ → \underline{ω}}_{ntimes} as follows: the function with constant value n is interpreted as succ\underline{ω}, the

identity as λx.x, the composition of f with n-ary functions g_{i} as

λx_{1}, …, x_{n}.f(g_{1}x_{1} ⋯ x_{n}) ⋯ (g_{m}x_{1} ⋯ x_{n}),

and the primitive recursive function f0x⃗ := gx⃗, f(succn)x⃗ := hn(fnx⃗)x⃗ as

R\underline{ω}(λu, v.g)(λu, v.h(u0)(v0)).

. Lemma 2.12 If f is a n-ary primitive recursive function, then

∀x_{1}, …, x_{n}.flat(fx_{1} ⋯ x_{n}) = f(flat x_{1}) ⋯ (flat x_{n})

. Proof: Induction on the definition of the primitive recursive functions.

3 The ordinal denotation system OT

We introduce a primitive recursive denotation system, omitting the proofs (see [Buc86],

[BS88] for proofs and details, for this particular system it is worked out in [Set90]). Definition 3.1 Let 0_{OT} , D_{0}, D_{1}, … be a sequence of formal symbols (We will write 0 for 0_{OT}). Then for n ∈ ω the set T_{n} of terms is defined by 0 ∈ T_{n} is a term, if a ∈ T_{n}, k ≤ n, then D_{k}a ∈ T_{n}, and if k ≥ 1, a_{0}, …, a_{k} ∈ T_{n}, then (a_{0}, …, a_{k}) ∈ T_{n}. We assume some coding of T := ⋃_{n∈ω} T_{n} in ω, s.t. we have some boolean predicate s ∈ T_{n} (depending on s\underline{ω} and n\underline{ω}), and a function length : ω → ω for the length of the term. The terms D_{k}a are called principal terms. If a is a principal term, then (a) := a. Ω_{n+1} := D_{n}0, 1 := D_{0}0, ω := D_{0}1. We will write ∀x ∈ T.ϕ(x) for ∀x\underline{ω}.x ∈ T → ϕ(x), where x ∈ T is the boolean predicate correponding to T, similar for other sets, which are introduced as boolean predicates. Definition 3.2 We define a ≺ b for a, b ∈ T by a ≺ b if b ≠ 0, D_{u}a ≺ D_{v}b if u < v or (u = v and a ≺ b) and if n ≥ 1 or m ≥ 1, then for a = (a_{0}, …, a_{n}), b = (b_{0}, … b_{m}), a ≺ b ⇔ (n < m ∧ ∀i ≤ n.a_{i} = b_{i}) ∨ ∃k ≤ min{n, m}.a_{k} ≺ b_{k} ∧ ∀i < n.a_{i} = b_{i}. Let a ⪯ b :↔ (a ≺ b ∨ a = b). ≺, ⪯ can be defined as boolean predicates on \underline{ω} × \underline{ω}.

We define for a ∈ T and M, M′ ⊂ T: M ⪯ M′ :⇔ ∀x ∈ M∃y ∈ M′(x ⪯ y), M ≺ a :⇔ ∀x ∈ M(x ≺ a), a ⪯ M :⇔ ∃x ∈ M(a ⪯ x). Definition 3.3 We define G_{u}a ⊂ T for a ∈ T by G_{u}0 := ∅, G_{u}(a_{0}, …, a_{k}) := G_{u}a_{0} ∪ ⋯ ∪ G_{u}a_{k} (if k ≥ 1),

G_{u}D_{v}b := \{ \begin{matrix}\{b\} ∪ G_{u}b, if u ≤ v, \\ ∅, if v < u. \end{matrix}

Definition 3.4 We define the set of terms OT (OT ⊂ T): by 0 ∈ OT, if a_{0}, …, a_{k} ∈ OT (k ≥ 1), a_{k} ⪯ ⋯ ⪯ a_{0}, then (a_{0}, …, a_{k}) ∈ OT and if b ∈ OT, G_{v}b ≺ b, then D_{v}b ∈ OT. OT_{n} := OT ∩ T_{n}. In the following ∀x ≺ t.ϕ(x) := ∀x ∈ OT.x ≺ t → ϕ(x), similar for ⪯. Further for a ∈ OT a considered as a set will be the set {x ∈ OT |x ≺ a}. Definition 3.5 Definition of a + b for a, b ∈ T: a + 0 := 0 + a := a, (a_{0}, …, a_{k}) + (b_{0}, …, b_{m}) := (a_{0}, …, a_{k}, b_{0}, …, b_{m}) (if (a_{0}, …, a_{k}) and (b_{0}, …, b_{m}) ≠ 0). Definition of a · n for a ∈ T, n ∈ OT, n ≺ ω: a · 0 := 0, a · (n + 1) := a · n + a. Definition 3.6 (Definition of τ(a) and a[z] for a ∈ OT, z ∈ τ(a)).

([ ].0) τ(0) := 0.

([ ].1) τ(1) := 1. 1[0] := 0.
([ ].2) τ(D_{u+1}0) := Ω_{u+1}. (D_{u+1}0)[z] := z.
([ ].3) Assume a = D_{v}b s.t. b ≠ 0:
(i) If τ(b) = 1: τ(a) := ω,
a[n] := (D_{v}b[0]) · (n + 1).
(ii) If τ(b) = Ω_{u+1} (v ≤ u < ω): τ(a) := ω, a[n] := D_{v}b[ζ_{n}],
wobei ζ_{0} := D_{u}0, ζ_{n+1} := D_{u}b[ζ_{n}].
(iii) τ(b) ∈ {ω} ∪ {Ω_{u+1} | u < v}: τ(a) := τ(b),
a[z] := D_{v}b[z].
([ ].5) a = (a_{0}, …, a_{k})(k ≥ 1): τ(a) := τ(a_{k}),
a[z] := (a_{0}, …, a_{k−1}) + a_{k}[z].

Wir define 0[n] := 0, a[n] := a[0] for a ∈ T with τ(a) = 1. Lemma 3.7 (a) ≺ is a linear ordering on OT.

(b) {x ∈ OT |x ≺ ω} is the least set X such that 0 ∈ X and if x ∈ X, x + 1 ∈ X.

(c) ∀a ∈ OT.∀x ≺ τ(a).a[x] ∈ OT ∧ a[x] ≺ a.

(d) ∀a ∈ OT.∀b ∈ OT.b ≺ a → ∃x ∈ OT.b ≺ a[x].

(e) ∀a ∈ OT.a ≺ ω → (a = 0 ∨ ∃x ∈ OT.length(x) < a ∧ a = x + 1).

(f) ∀a ∈ OT.a ≺ D_{0}D_{n+1}0 → a ∈ OT_{n}. Proof: Is done in the cited literature.

4 The nth numberclasses in the type theory F A

We introduce now the iteration of Kleene’s O. Definition 4.1 (a) We define the n-th numberclass \underline{Ω}_{n} (\underline{Ω}_{n} = O_{n}, where O_{n} is the iteration

of Kleene’s O) by Meta-recursion on n for n ≥ 1: \underline{Ω}_{n} := (C_{0}^{Ω_{n}} : \underline{0}, C_{1}^{Ω_{n}} : \underline{1}, C_{ω}^{Ω_{n}} : \underline{ω}, C_{Ω_{1}}^{Ω_{n}} : \underline{Ω}_{1}, …, C_{Ω_{n−1}}^{Ω_{n}} : \underline{Ω}_{n−1}).

We define 0_{Ω_{n}} := C_{0}^{Ω_{n}}EF Q, succ_{Ω_{n}} : λx.C_{1}^{Ω_{n}}(λu.x) of type Ω_{n} → Ω_{n}.

(b) The branch ordinals are the ordinals 0, 1, ω, Ω_{1}, Ω_{2}, Ω_{3}, . . ..

The ordinal types are \underline{α} for α a branch ordinal.

(c) We define for α, β branch ordinals \underline{α}⊂_{type}\underline{β} :⇔ α ≺ β, and \underline{α}⊆_{type}\underline{β} :⇔ α ⪯ β.

(d) For an letter τ = 0, 1, ω, Ω_{1}, …, \underline{τ} is the corresponding type \underline{0}, \underline{1}, \underline{ω}, \underline{Ω}, . . ..

(e) If σ ⪯ τ, then we define the embedding ι_{σ,τ} : \underline{σ} → \underline{τ}, by recursion on \underline{σ}: For α ≺ σ, ι_{σ,τ}(C_{α}^{σ}f) := C_{α}^{τ}λx.ι_{σ,τ}(fx).

Further the projection is defined, proj_{τ,σ} : \underline{τ} → \underline{σ}, (σ ⪯ τ) by recursion on \underline{τ}: For α ≺ σ, proj_{τ,σ}(C_{α}^{τ}f) := C_{α}^{σ}λx.proj_{τ,σ}(fx).

and if σ ⪯ α ≺ τ, then proj_{τ,σ}(C_{α}^{τ}f) := 0\underline{σ}. Lemma 4.2 Assume α ⪯ β ⪯ γ are branch ordinals.

(a) ∀x\underline{α}; proj_{β,α}ι_{α,β}x = x.

(b) ∀x\underline{α}; ι_{β,γ}ι_{α,β}x = ι_{α,γ}x.

(c) ∀x\underline{γ}; proj_{β,α}proj_{γ,β}x = proj_{γ,α}x.

Proof: (a): Induction on x\underline{α}. If f : \underline{σ} → \underline{α}, and by IH ∀y\underline{σ}; proj(ι(fy)) = fy, then proj(ι(C_{α}^{σ}f)) ≃ C_{α}^{σ}λy.proj(ι(fy)) = C_{α}^{σ}λy.fy ≃ C_{α}^{σ}f.

5 Representation of OT in \underline{Ω}_{n}

Definition 5.1 We define the functions, representing the usual ordinal functions on OT as follows

(a) We define addition +\underline{σ} : \underline{σ} → \underline{σ} → \underline{σ} for an ordinaltype \underline{σ} by recursion on the second argument:

s + C_{0}f := s, s + C_{1}f := succ (s + f(0_{1})), s + C\underline{σ}f := C\underline{σ}λx.(s + x).

(b) We define multiplication ·\underline{σ} : \underline{σ} → \underline{ω} → \underline{σ} for an ordinaltype \underline{σ} by recursion on the second argument:

s · C_{0}f := 0, s + C_{1}f := (s · (f0_{1})) + s.

(c) Ω_{0}^{σ} := 1^{σ} := succ 0_{σ} (if σ ≠ 0, 1).

(d) For Ω_{1} ⪯ σ, we define ω^{σ} := C_{ω}λx.1 · (succ x).

(e) For Ω_{k} ≺ σ, we define Ω_{k}^{σ} := C_{Ω_{k}}^{σ}λx.ι_{Ω_{k},σ}x.

(f) We define for natural numbers n ≥ 1, D̃_{n} : \underline{Ω}_{n} → (\underline{n} → \underline{Ω}_{n}). (D̃_{n}xk is the representation of the collapsing function Dk in n (which we will call D_{k}^{Ω_{n}}. This is a way, to define simultaneously the functions D_{0}^{Ω_{n}}, …, D_{n−1}^{Ω_{n}}). We define D̃_{n} by recursion on \underline{Ω}: D̃_{n}(C_{0}f)k := Ω_{k,Ω_{n}}. D̃_{n}(C_{1}f)k := C_{ω}λx.(D̃_{n}(f0)k) · x. If Ω_{k} ≺ Ω_{l+1} = α, then

D̃_{n}(C_{α}f)k := C_{ω}λx.D̃_{n}(f(proj_{Ω_{n+1},α}ζ_{succ x}))k,

where ζ_{·} : \underline{ω} → \underline{Ω}_{n+1} is defined by recursion on \underline{ω},

ζ_{C_{0}f} := Ω_{l}, ζ_{C_{1}f} := D̃_{n}(f(proj_{Ω_{n},Ω_{l+1}}ζ_{f0_{1}})).

If 1 ≺ α ⪯ Ω_{k}, then D̃_{n}(C_{α}f)k := C_{α}λx.D̃_{n}(fx)k,

(g) D_{k}^{Ω_{n}} := λx.D̃_{n}x(k + 1), D_{k}^{Ω_{n}} : \underline{Ω}_{n} → \underline{Ω}_{n}.

(h) We define for branch ordinals α ≺ Ω_{n+1} the interpretation of OT_{n} ∩ α in \underline{Ω}_{k+1} ι′_{OT,n} : \underline{ω} → \underline{α} (ι′ := ι_{OT,n}): ι′(0) := 0_{α}, ι′(D_{k}a) := D_{k}^{Ω_{n}}ι_{OT,n}a, ι′(a_{0}, …, a_{n}) := ι′(a_{0}) + ⋯ ι′(a_{n}). To avoit problems with equality, we define: ι := λx.ι′(flat(x)).

Lemma 5.2 (a) ∀x\underline{ω}.Resp(ι(x)).

(b) ∀x\underline{ω}, y\underline{ω}.eqnat(x, y) → ι(x) = ι(y). Lemma 5.3 If α, β are branch ordinals, α ⪯ β, ι := ι_{α,β}, proj := proj_{β,α}, then

(a) ∀x\underline{α}, y\underline{α}; ι(x + y) = ι(x) + ι(y).

(b) ∀x\underline{α}, y\underline{ω}; ι(x · y) = ι(x) · y.

(c) For x branch ordinal or x = Ω_{0} s.t. x ≺ α. we have ι(x_{α}) = x_{β}, proj(x_{β}) = x_{α},

(d) If α = Ω_{n}, β = Ω_{m}, then ∀x\underline{α}; ι(D̃_{n}xk) = D̃_{m}ι(x)k, ∀x\underline{α}; ι(D̃_{n,k}x) = D̃_{m,k}ι(x). The proof follows immediately by induction on the definition of the respective functions (using naturally the implicit predicates Resp. Definition 5.4 We define for α ⪯ β branch ordinals t\underline{β} ≺_{β} α for ι_{α,β}(proj_{β,α}t) = t. The meaning is, that t is the embedding of term of type \underline{β} in \underline{α}. Remark 5.5 If α ⪯ β are branch ordinals, γ ≺ β, then

(a) If α ⪯ γ, ¬(C_{γ}^{β}f ≺_{β} α).

(b) If γ ≺ α, then C_{γ}^{β}f ≺_{β} α ↔ ∀x\underline{γ}.fx ≺_{β} α.

(c) If α ⪯ β ⪯ γ, then ∀x\underline{γ}; x ≺ α → x ≺ β. Proof:

(a) ι_{α,β}proj_{α,β}C_{γ}^{β}f = C_{0}^{β}g for some g, therefore not equal to C_{γ}^{β}f.

(b) ιproj(C_{γ}f) = C_{γ}λx.ι(proj(fx)) = C_{γ}f, iff ∀x\underline{γ}; ι(proj(fx) = fx. (Note, that we have implicitly always the respectfulness predicate.

(c) follows by induction on \underline{γ}, using (a) and (b). Lemma 5.6 Assume α ⪯ β branch ordinals.

(a) ∀x\underline{β}, y\underline{β}; x ≺_{β} α → y ≺_{β} α → x + y ≺_{β} α.

(b) ∀x\underline{β}, y\underline{ω}; x ≺_{β} α →→ x · y ≺_{β} α.

(c) If x = 0, 1, ω, Ω_{0}, Ω_{1}, …, then x_{β} ≺ α iff x ≺ α.

(d) If β = Ω_{n+1}, α ≺ β, then ∀x^{α}; D_{k}^{Ω_{n}}x ≺_{β} Ω_{k+1}.

(e) D_{0}^{Ω_{n}}0 ≺_{β} \underline{ω}.

(f) If a ∈ OT_{n}, a ≺ β ⪯ γ ≺ Ω_{n+1}, then ι_{OT,n}(x) ≺ β. Proof: (a) - (e) follow by induction on the types.

(f) follows by (a) - (e) by induction on the length of a. Lemma 5.7 Let α be a branch ordinal.

(a) τ(0_{α}) = \underline{0} ∧ ∀x\underline{0}. ⊥. (α ≠ 0)

(b) τ(1_{α}) = \underline{1} ∧ ∀x\underline{1}; 1_{α}[x] = \underline{0} (α ≠ 0, 1).

(c) τ(Ω_{u+1,α}) = \underline{Ω}_{u+1} ∧ ∀x^{\underline{Ω}^{u+1}}; Ω_{u+1}^{α}[x] = ι_{Ω_{u+1}^{α}}x.(Ω_{u+1} ≺ α).

(d) ∀x^{\underline{Ω}^{n+1}}; τ(x) = \underline{0} → τ(D_{u+1}^{Ω_{n}}x) = \underline{Ω}_{u+1} ∧ ∀y^{\underline{Ω}^{u+1}}; (D_{u+1}^{Ω_{n}}x)[y] = ι_{Ω_{u+1},α}y.

(e) ∀x^{\underline{Ω}^{n+1}}; τ(x^{Ω_{n+1}}) = \underline{1} → τ(D_{u}^{Ω_{n}}x) = \underline{ω} ∧ ∀x\underline{ω}; (D_{u}^{Ω_{n}}x)[n] = (D_{u}^{Ω_{n}}(x[0])) · succ n.

(f) If v ≤ u < n, then with ζ′_{n,u,v}x : \underline{ω} → \underline{Ω}_{n+1}, s.t.

ζ′_{n,u,v}x(C_{0}f) := D_{u}^{Ω_{n}}0, ζ′_{n,u,v}x(C_{1}f) := D_{u}^{Ω_{n}}(x[proj_{Ω_{n+1},Ω_{u+1}}(ζ′_{n,u,v}x(f0))]), we have

∀x^{\underline{Ω}^{n+1}}; τ(x) = \underline{Ω}_{u+1} → τ(D_{v}^{Ω_{n}}x) = \underline{ω}∧
∀y\underline{ω}; (D_{v}^{Ω_{n}}x)[y] = D_{v}^{Ω_{n}}(x[proj_{Ω_{n+1},Ω_{u+1}}(ζ′_{n,u,v}x(succ y))]).

(g) If β = ω or β = Ω_{u+1}, u < v, then ∀x^{\underline{Ω}^{n}}; τ(x) = \underline{β} → τ(D_{v}^{Ω_{n}}x) = \underline{β} ∧ ∀y\underline{β}; (D_{v}^{Ω_{n}}x)[y] = D_{v}^{Ω_{n}}(x[y])

(h) If β ≠ 0, then

∀x\underline{α}, y\underline{α}; τ(x) = \underline{β} → τ(y + x) = \underline{β} ∧ ∀z\underline{β}; (y + x)[z] = y + (x[z])

Proof: Either immediate, oder transfinite induction on the type of x (where we actually do not need really induction, but just that we have we have x ≡ Cf for some constructor. Lemma 5.8 (a) ∀x ∈ OT_{n}.ι_{OT,n}(x) = ι_{OT,n}(flat(x)).

∀x, y ∈ OT_{n}.eqnat(x, y) → ι_{OT,n}(x) = ι_{OT,n}(y).

(b) ∀y ∈ OT_{n}.ι_{OT,n}(y + 1) = succ ι_{OT,n}(y).

(c) ∀x, y ∈ OT_{n}.ι_{OT,n}(x + y) = (ι_{OT,n}x) + (ι_{OT,n}y).

(d) ∀x, y ∈ OT_{n}.y ≺ ω → (ι_{OT,n}x) · (ι_{OT,n}y) = ι_{OT,n}(x · y). Proof: Induction on the length of y. Lemma 5.9 If α = Ω_{n+1}, then

∀x ∈ OT_{n}.τ(ι_{OT,n}x) = \underline{x} ∧ ∀y ∈ OT_{n} ∩ τ(x).ι_{OT,n}(x[y]) = (ι_{OT,n})[proj_{Ω_{n+1},τ(x)}ι_{OT,n}y].

(Where this stands more precisely for the formula:

∀x ∈ OT_{n}. ⋀_{\{α|α≺Ω_{n+1}∧αbranch ordinal\}} τ(x) = α → τ(ι_{OT,n}x) = \underline{α} ∧ ∀y ∈ OT_{n}.y ≺ α →

ι_{OT,n}(x[y]) = (ι_{OT,n})[proj_{Ω_{n+1},α}ι_{OT,n}y].

Proof: Induction on the definition of OT_{n}, using eqnat(flat(x[y]), flat(x)[flat(y)]), (by ·[·] is primitive recursive and 2.12), Lemmata 5.6, 5.7, 5.8. In the case x = D_{v}b, τ(b) = Ω_{u+1}, we prove by induction on the length of y

∀y ∈ OT.ι_{OT,n}ζ_{y} = ζ′_{n,u,v}(ι_{OT,n}b)(proj_{Ω_{n+1},ω}ι_{OT,n}y),

using 3.7 (e).

6 Proof of transfinite induction

Lemma 6.1 If ϕ(x\underline{ω}) is a formula, then

(∀x ∈ OT_{n}.(∀y ≺ τ(x).y ∈ OT_{n} → ϕ(x[y])) → ϕ(x)) → ∀x ∈ OT_{n}.ϕ(x).

Proof: Assume ∀x ∈ OT_{n}.(∀y ≺ τ(x).y ∈ OT_{n} → ϕ(x[y])) → ϕ(x). Let ψ(x^{\underline{Ω}^{n+1}}) := ∀y ∈ OT_{n}.ι_{OT,n}y = x → ϕ(x). Then, we have for all branch ordinals α ≺ Ω_{n+1} respectful f^{\underline{α}→\underline{Ω}_{n}} (∀z\underline{α}.ψ(fz)) → ψ(C_{α}f): Assume ∀z\underline{α}; ψ(fz). If ι_{OT,n}(y) = C_{α}f, then τ(y) = α and for z ∈ OT_{n}, z ≺ α, ι_{OT,n}(y[z]) = (C_{α}f)[proj_{Ω_{n+1},\underline{α}}(ι_{OT,n}z)] = f(proj_{Ω_{n+1},\underline{α}}(ι_{OT,n}z)), by IH therefore ϕ(y[z]) and therefore by assumption ϕ(y) and we get ψ(C_{α}f). By transfinite induction on \underline{Ω}_{n+1} follows therefore ∀x^{\underline{Ω}^{n+1}}; ψ(x), therefore ∀y ∈ OT_{n}.ϕ(x).

Theorem 6.2 If ϕ(x\underline{ω}) is a formula (where after every quantifier we have the predicate Resp(x)), then

(∀x ∈ OT ∩ Ω_{1}.(∀y ≺ τ(x).ϕ(y)) → ϕ(x)) → ∀x ≺ D0D_{n}0.ϕ(x).

Proof: Let ψ(x) := x ≺ D_{0}D_{n}0 → ∀y ≺ x.ϕ(x). Then ∀x ∈ OT_{n}.(∀y ≺ τ(x).y ∈ OT_{n} → ϕ(x[y])) → ϕ(x): τ(x) = 0, 1, ω therefore OT_{n}∩τ(x) = τ(x). From ∀y ∈ OT_{n}∩τ(x).ϕ(x[y]) follows therefore using 3.7 (d) ∀y ≺ τ(x).ϕ(y) and therefore ϕ(x). By 6.1 follows ∀x ∈ OT_{n}.ψ(x), therefore ∀x ∈ OT_{n}.ψ(x + 1) and we are done.

References

[Ber94] U. Berger. Strong normalization for the typed lambda-calculus with recursion over wellfounded trees. abstract, submitted to PPC’94, 1994.

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

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

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

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

[Set90] A. Setzer. Ordinalzahlanalyse prädikativer Theorien unter Verwendung von Fundamentalfolgen. Master’s thesis, Universität München, January 1990.

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