Proof Theory of Martin-Löf Type Theory – An Overview

Anton Setzer^{∗}

February 22, 2004

Abstract

We give an overview over the historic development of proof theory and the main techniques used in ordinal theoretic proof theory. We argue, that in a revised Hilbert’s programme, ordinal theoretic proof theory has to be supplemented by a second step, namely the development of strong equiconsistent constructive theories. Then we show, how, as part of such a programme, the proof theoretic analysis of Martin-Löf type theory with W-type and one microscopic universe containing only two finite sets is carried out. Then we look at the analysis of Martin-Löf type theory with W-type and a universe closed under the W-type, and consider the extension of type theory by one Mahlo universe and its proof-theoretic analysis. Finally we repeat the concept of inductive-recursive definitions, which extends the notion of inductive definitions substantially. We introduce a closed formalisation, which can be used in generic programming, and explain, what is known about its strength. Keywords: Martin-Löf type theory, proof theory, Kripke-Platek set theory, W-type, well-founded trees, Kleene’s O, Mahlo universe, inductive-recursive definitions, generic programming.

1 Introduction

The goal of this article is to introduce the reader, who is not necessarily an expert in proof theory, into the current state of the art of proof theory of Martin-Löf type theory and the techniques used there. We start by giving a brief overview over the contents of this article.

In Sect. 2, we first reconsider the original form of Hilbert’s programme: to prove the consistency of theories for carrying out mathematical proofs using finitary methods. We then discuss the theory PRA, which is usually taken as the formalisation of finitary methods. Next we look at Gödel’s second incompleteness theorem and the fall of Hilbert’s programme. Then we discuss Gentzen’s proof theoretic analysis of Peano arithmetic. We will look at the techniques used there – the notion of an ordinal notation system and cut elimination. Then we introduce the two main (usually equivalent) notions of proof theoretic strength.

In the short Sect. 3, we discuss, why a traditional proof theoretic analysis should be supplemented by a second step, namely the development of equiconsistent constructive theories.

In Sect. 4, we consider a relatively small variant of type theory, Martin-Löf type theory with W-type and a microscopic universe atom. This is used in order to introduce the basic techniques of proof theory, the relationship of these type theories to so called admissible ordinals, and to variants of a weak version of set theory called Kripke-Platek set theory.

∗Supported by Nuffield Foundation, grant ref. NAL/00303/G and EPSRC grant GR/S30450/01. Department of Computer Science, University of Wales Swansea, Singleton Park, Swansea SA2 8PP, UK. Email: a.g.setzer@swan.ac.uk, Fax: +44 1792 295651.

In Sect. 5 we will look at the first major example, Martin-Löf type theory with W-type and one universe. We will see that, in order to obtain an upper bound, one can model type theory in Kripke-Platek set theory extended by one recursively inaccessible and finitely many admissibles above it, which can be analysed easily.

In Sect. 6, we first develop a formalisation of a Mahlo universe and discuss its constructive validity. We then discuss a suitable extension of Kripke-Platek set theory of the same strength, and give some hints about how to model type theory in this set theory.

In Sect. 7, we look at one application of the results obtained in the area of generic programming. We consider P. Dybjer’s concept of inductive-recursive definitions, which is a substantial generalisation of the concept of inductive definitions and includes standard (non-Mahlo-) universe constructions. Then we will develop a theory in which one can introduce all inductive-recursive sets. This theory will have a data type of inductive-recursive definitions, and allows therefore to introduce functions, which take a data type, analyse it and create another data type from it – this is a very general form of generic programming. This type theory makes use of the ideas contained in the definition of the Mahlo universe, and subsumes a slightly weakened form of the Mahlo universe.

In appendix A, we give a direct well-ordering proof for an ordinal notation system of strength ϵ_{0}. This forms the basis for developing well-ordering proofs, the main tool for determining lower bounds for the strength of type theories.

In appendix B we give details about the how to model Martin-Löf type theory with W-type and one universe in a corresponding variant of Kripke-Platek set theory, which can be analysed easily. We will as well show how to obtain a lower bound by carrying out a direct well-ordering proof for a corresponding ordinal notation system.

Appendix C will describe some details about how to obtain an upper bound for the strength of type theory with W-type and one Mahlo universe by modelling it in Kripke-Platek set theory with one recursively Mahlo ordinal. We will not go into details w.r.t. the well-ordering proof for this type theory.

In appendix D we will show that type theory introduced in Sect. 7 reaches the strength of Kripke-Platek set theory plus recursive Mahloness of the universe.

2 The Notion of Proof-Theoretic Strength

Hilbert’s programme. Proof theory was established as a science by D. Hilbert. In his famous list of mathematical problems [Hilbert, 1900], he posed as second problem to show the consistency of an axiomatisation of the real numbers developed by him. He argued that, if this axiomatisation is shown to be consistent, this would prove the mathematical existence of the concept of real numbers and of the continuum: consistency implies existence. He stated as well the main problem, namely that, if one shows the consistency of a theory for formalising mathematics in the same theory, one has not achieved anything: if the original theory is inconsistent, it proves everything, even its own consistency. So in order to achieve something, one has to do more: namely show the consistency using methods which are considered to be safe. According to Hilbert, finitary methods were to be considered to be safe. By finitary methods he considered finitary calculations, as we can carry them out on a piece of paper.

Later his problem was generalised to what is now known as Hilbert’s programme: to prove the consistency of axiom systems, in which certain parts of mathematics can be carried out, by finitary means.

There are two main approaches for carrying out consistency proofs. One is to introduce a model of the system in question in the Meta-theory. However, it seems to be implausible to assume that one can prove this way the consistency of a theory by using finitary methods, since such methods do not allow the use of sets. Hilbert realized this and suggested therefore that one should instead analyse proofs and show this way directly that it is not possible to derive in the formal system in question a contradiction. He called the mathematical discipline, in which such investigations are carried out, proof theory.

The first step was to establish a precise formalisation of what is meant by mathematical theories. A theory for formalising basic logic had to be introduced. One of these formalisations, the Hilbert-calculus, is due to Hilbert. Later many other equivalent ones were developed, and the probably currently in proof theory most popular one is the Tait calculus [Tait, 1968]. By adding axioms about mathematical entities to such logic calculi, one obtains theories in which mathematical proofs can be formalised.

Hilbert developed one technique for carrying out consistency proofs in his sense, the epsilon-substitution method ([Hilbert and Bernays, 1939], see as well recent work by Mints and Tupailo, e.g. [Mints and Tupailo, 1999, Mints et al., 1996]).

Primitive-Recursive Arithmetic was introduced by Skolem in his article [Skolem, 1923]. There he reasoned informally in a system, which was later formalised and called primitive-recursive arithmetic (PRA). This system is nowadays generally regarded as being a formalisation of what Hilbert meant by finitary methods.

The only objects in PRA are natural numbers. The basic notion is that of a primitive recursive function. The primitive recursive functions, which are functions ℕ^{n} → ℕ for arbitrary n, are those, which can be constructed from the constant zero function (λx.0), projection functions (i.e. λ(x_{0}, …, x_{n−1}).x_{i}, which denotes the function f : ℕ^{n} → ℕ s.t. f(x_{0}, …, x_{n−1}) = x_{i}), and successor function (λx.x + 1) by using composition (i.e. if f, g_{i} are primitive recursive, so is λ(x_{0}, …, x_{n−1}).f(g_{1}(x_{0}, …, x_{n−1}), …, g_{k}(x_{0}, …, x_{n−1})) and the schema of primitive recursion: if f and g are primitive recursive, so is the function h defined by h(x⃗, 0) = f(x⃗), h(x⃗, y + 1) = g(x⃗, y, h(x⃗, y)). Addition, multiplication and exponentiation can easily be defined using primitive recursion. The defining equations for the primitive recursive functions provide a schema for calculating the result of these functions in finite amount of time. Therefore the primitive recursive functions can be regarded as finitary operations.

The terms of PRA are now expressions which are constructed from variables and 0 by application of symbols for primitive recursive functions. If we substitute the free variables by numbers, they can be evaluated in finite amount of time. Therefore these terms can be regarded as finitary schemata.

The formulae in Skolem’s system were all propositional formulae constructed from equations, i.e. the set of formulae is the least set containing the equations, and which is closed under negation, conjunction and disjunction. Define first a−^{·} b := max{0, a−b}, which can be defined primitive-recursively. Then we can encode a = b as (a−^{·} b) + (b−^{·} a) = 0, ¬(a = 0) as (1−^{·} a) = 0, (a = 0) ∧ (b = 0) as a + b = 0 and a = 0 ∨ b = 0 as a · b = 0. By repetitively applying these operations we can encode all propositional formulae as equations of the form a = 0, and can restrict the set of formulae therefore to equations. These equations relate finitary schemata with each other.

Skolem used in his reasoning as basic laws the defining equations for primitiverecursive functions, the standard laws of = (reflexivity, symmetry, transitivity and substitution) and the classical laws for the propositional connectives. (One can show that restricted to quantifier free formulae with decidable prime formulae, classical and intuitionistic logic coincide). The only strong law he used is that of induction over primitive recursive formulae. Using the above encoding, the system can be restricted to a theory having as formulae equations only, and where we omit therefore the laws for the propositional connectives (a systematic development of this can be found in [Goodstein, 1964]). The resulting laws can now be regarded as a formulation of what Hilbert meant by finitary methods: Assume an equation t = t′ is derived this way, and let s, s′ be the result of substituting all variables in t, t′ respectively by numbers. By going through the derivation (a proof of a corresponding Meta-theorem requires induction on the derivation) one can easily see that s and s′ reduce to the same number, and, when investigating it, one has never to refer to the set of natural numbers as an entity, but needs to refer only to finitely many numbers.

It can easily be shown that the following system is conservative over Skolem’s version of PRA for equational formulae, i.e. that both theories derive the same propositional formulae: One takes as formulae arbitrary first-order formulae (i.e. all formulae with quantifiers ranging over natural numbers), built from equations of terms as given before. As rules one takes the basic rules of the predicate calculus (i.e. basic logic for formulae), and basic laws of equality (which involve the extended language). Furthermore, one adds the rule of induction over quantifier-free (i.e. propositional) formulae. The proof that we obtain a conservative extension can be carried out using proof theoretic techniques in PRA. In proof theory, by PRA one usually means the just mentioned theory, and we will follow in the rest of this article this convention.

Gödel’s second incompleteness theorem and the failure of Hilbert’s original programme. 1931 Gödel showed in his second incompleteness theorem [Gödel, 1931], that Hilbert’s original programme cannot be carried out – assuming minimal conditions on a theory T, which hold for practically all theories with a natural encoding of the natural numbers (natural theories which have been considered and do not fulfil these conditions are weaker than PRA), he could show that a consistent theory T does not prove its own consistency. It follows that the consistency of theories T with a natural embedding of PRA and which fulfil Gödel’s conditions cannot be shown by finitary means. Most natural theories except for extremely weak ones fulfil the premise of the last sentence – Hilbert’s original programme had failed.

Gentzen’s proof of the consistency of Peano Arithmetic. 1936 Gerhard Gentzen [Gentzen, 1936] showed the consistency of Peano Arithmetic (PA) using transfinite induction up to ϵ_{0}. This was the birth of ordinal theoretic proof theory.

PA is the extension of PRA by allowing induction over all (first-order) formulae. (one often restricts the set of functions to addition, multiplication, successor function and the constant zero however – the addition of all primitive-recursive functions is conservative over that theory). Gentzen considered a primitive recursive ordinal notation system up to ϵ_{0}:

In set theory, an ordinal α is a set which is transitive and the elements of which are transitive. Especially the elements of ordinals are ordinals. Let Ord be the class of all ordinals. As usual, Greek letters will in the following refer to ordinals, so e.g. ∀α.φ(α) stands for ∀x ∈ Ord.φ(x). The relation ∈ on the class of ordinals is a linear ordering, and one usually writes α < β for α ∈ β. < is well-founded, i.e. for any formulae we have the principle of transfinite induction over ordinals: (∀α.(∀β < α.φ(β)) → φ(α)) → ∀α.φ(α). An ordering which is both linear and well-founded is called a well-ordering. The union of a set of ordinals A forms an ordinal which is the supremum of the ordinals, therefore written as sup A. There is a standard definition of addition, multiplication and exponentiation of ordinals. All natural numbers can be regarded as ordinals (using 0 = ∅ and α + 1 = {α} ∪ α) and the set of natural numbers forms an ordinal ω, which is the least infinite ordinal. Every ordinal α is either 0, a successor ordinal, i.e. of the form β + 1, or a limit ordinal, which means that ∀β < α.∃γ < α.β < γ. Furthermore, for every ordinal α there exists an k ∈ ℕ and unique α ≥ α_{1} > ⋯ > α_{k} and n_{i} ∈ ℕ s.t. n_{i} > 0 and α = ω^{α_{1}} · n_{1} + ⋯ + ω^{α_{k}} · n_{k} (here we use the just mentioned operations of addition, multiplication and exponentiation on ordinals). If the expression on the right fulfils the previous conditions on α_{i} and n_{i}, it is called the Cantor Normal Form CNF of α. One can show that the ordering on ordinals in CNF is the lexicographic ordering: If α = ω^{α_{1}} · n_{1} + ⋯ + ω^{α_{k}} · n_{k}, β = ω^{β_{1}} · m_{1} + ⋯ + ω^{β_{l}} · m_{l} are the CNFs of α, β, then α < β iff ((α_{1}, n_{1}), …, (α_{k}, n_{k})) < ((β_{1}, m_{1}), …, (β_{l}, m_{l})) with respect to the lexicographic ordering on pairs and descending sequences: one forms first the lexicographic ordering on pairs (α, n) s.t. α ∈ Ord and n ∈ ℕ, and then the lexicographic ordering on descending sequences of such pairs. We will use this property in appendix A in a direct well-foundedness proof for the ordinal notation system up to ϵ_{0}. An ordinal α which has a CNF with ordinal coefficients α_{i} < α can be considered to be constructed using CNF from smaller ordinals, and ϵ_{0} is the least ordinal which does not have this property. It can be defined as

ϵ_{0} = sup\{\underbrace{ω^{ω^{·^{·^{·^{1}}}}}}_{n times} | n ∈ ω\}. One can easily show that ϵ_{0} = ω^{ϵ_{0}}.

An ordinal notation system is a pair (OT, <_{OT}) consisting of a set OT ⊆ ℕ and a primitive relation <_{OT}⊆ OT^{2}, such that <_{OT} is linear and well-founded, i.e. the principle of transfinite induction over OT holds with respect to all sets: ∀X ⊆ ℕ.(∀x ∈ OT.(∀y ∈ OT.y <_{OT} x → y ∈ X) → x ∈ X) → OT ⊆ X. We will write < instead of <_{OT}, if it will be clear from the context, whether < or <_{OT} is meant by <. (OT, <) is primitive recursive, if both OT and < are primitive recursive. In a context, in which only natural numbers and one ordinal notation system are mentioned, one writes Greek letters for elements of OT using the same convention as before – e.g. ∀β.φ(β) stands for ∀x ∈ OT.φ(x).

Now it is easy to introduce an ordinal notation system based on CNF: One encodes sequences of natural numbers (n_{1}, …, n_{k}) as natural numbers ⟨n_{1}, …, n_{k}⟩, and defines simultaneously inductively OT_{ϵ_{0}} and <_{ϵ_{0}}⊆ OT_{ϵ_{0}} × OT_{ϵ_{0}} as follows: If k ∈ ℕ, a_{1}, …, a_{k} ∈ OT_{ϵ_{0}}, a_{k} <_{ϵ_{0}} ⋯ <_{ϵ_{0}} a_{1}, n_{i} > 0 then ⟨⟨a_{1}, n_{1}⟩, …, ⟨a_{k}, n_{k}⟩⟩ ∈ OT_{ϵ_{0}}. (In the special case k = 0 we obtain ⟨⟩ representing 0). ⟨⟨a_{1}, n_{1}⟩, …, ⟨a_{k}, n_{k}⟩⟩ <_{ϵ_{0}} ⟨⟨b_{1}, m_{1}⟩, …, ⟨b_{k}, m_{k}⟩⟩, if the underlying sequences are in this order with respect to lexicographic ordering on pairs ⟨a, n⟩ ∈ OT_{ϵ_{0}} × ℕ and lexicographic ordering on sequences formed from such pairs, which reduces to the underlying ordering. It is a standard exercise (assuming a standard properties of the encoding of sequences of natural numbers as natural numbers) to show that (OT_{ϵ_{0}}, <_{ϵ_{0}}) forms a linear ordering which is primitive-recursive. Using set theory one can easily show that it is well-founded, by defining an embedding o of OT_{ϵ_{0}} into Ord by o(⟨⟨a_{1}, n_{1}⟩, …, ⟨a_{k}, n_{k}⟩⟩) = ω^{o(a_{1})} · n_{1} + ⋯ + ω^{o(a_{k})} · n_{k}, and by then showing that a <_{ϵ_{0}} b ⇔ o(a) < o(b). We will, as usual in proof theory, identify ordinal notations with the ordinals they denote, and write ω^{a_{1}} · n_{1} + ⋯ + ω^{a_{k}} · n_{k} instead of ⟨⟨a_{1}, n_{1}⟩, …, ⟨a_{k}, n_{k}⟩⟩, if there is no confusion.

In Appendix A we will sketch a direct well-foundedness proof of the ordinal system of strength ϵ_{0} – more precisely, we show that for every n the restriction of

OT_{ϵ_{0}} to ordinals less than \underbrace{ω^{ω^{·^{·^{·^{1}}}}}}_{n times} is well-founded. By Meta-induction on n, this

argument can be formulated directly in Peano Arithmetic, and therefore we can show for (Meta-)every b < ϵ_{0} transfinite induction over OT_{ϵ_{0}} restricted to ordinals less than b. The first proof carried out in PA we could find was in Hilbert/Bernays ([Hilbert and Bernays, 1939], §5, 3c). However we cannot show in PA that the union is well-founded, provided PA is consistent. This follows from Gödel’s second incompleteness theorem and the fact that PRA plus the principle of transfinite induction over (OT_{ϵ_{0}}, <_{ϵ_{0}}) proves the consistency of PA (therefore PA plus this principle proves the consistency as well), as shown by Gentzen using cut elimination:

Cut elimination. We will in the following give a modern version (in this compact form essentially due to Buchholz) of Gentzen’s proof of the consistency of PA in PRA extended by quantifier free transfinite induction up to ϵ_{0}. First one can embed proofs of closed formulae of Peano arithmetic into a semi-formal system, i.e. a system of proof rules having rules with infinitely many premises, which we call PA^{∗}:

We take as set of formulae those constructed from prime formulae and negated prime formulae using ∧, ∨, ∀ and ∃. The negation for non-prime formulae is defined by the deMorgan rules, e.g. ¬(P (x) ∧ Q(x)) := (¬P (x)) ∨ (¬Q(x)). Similarly we define A → B := ¬A ∨ B.

PA^{∗} is a Tait-style sequent calculus. Here sequents Γ, Δ are sets of formulae {A_{1}, …, A_{n}}, with the intended meaning being A_{1} ∨⋯∨A_{n}. Especially the empty sequent, denoted by ∅, stands for falsity. One writes Γ, A for Γ ∪ {A} and Γ, Δ for Γ ∪ Δ. In PA^{∗} one derives closed sequents Γ, i.e. sequents such that the formulae don’t contain any free variables.

The basic rules of the system are introduction rules for the logical connectives. Γ, A is an axiom, if A is a true prime formula. Furthermore, we have the following rules:

\begin{matrix}Γ, A & Γ, B \\ Γ, A ∧ B \end{matrix} \begin{matrix}Γ, A \\ Γ, A ∨ B \end{matrix} \begin{matrix}Γ, B \\ Γ, A ∨ B \end{matrix}

\begin{matrix}Γ, A(0) Γ, A(1) & Γ, A(2) ⋯ \\ Γ, ∀x.A(x) \end{matrix}

\begin{matrix}Γ, A(t) \\ Γ, ∃x.A(x) \end{matrix}

Note that ∀-introduction has infinitely many premises. The main formula in the conclusion of any rule (e.g. A ∧ B in the ∧-introduction rule) can be an element of Γ and therefore occur in the premise as well.

One can easily show that, if Γ is derivable, so is Γ, Δ. Therefore we can omit formulae in the premises of a rule which are not needed (e.g. if Γ, A and B are provable, then Γ, A∧B is provable, since from a proof of B we can obtain a proof of the second premise Γ, B of the ∧-introduction rule). We will therefore in derivations omit unnecessary formulae in sequents.

Additionally to the above rules, we add the cut rule and for technical purposes the repetition rule, which does not do anything (essentially due to Mints):

\begin{aligned}Γ, A & & Γ, ¬A \\ & Γ \end{aligned} {Γ \atop Γ}

In the cut rule, A is called the cut-formula. If one allows non-well-founded proofs, i.e. proofs with infinite chains Γ_{1}, Γ_{2}, … s.t. Γ_{1} is the conclusion and Γ_{i+1} is a premise of Γ_{i}, one can derive everything in this theory: derive Γ from Γ using the repetition rule, which is again derived from Γ etc. (Without the repetition rule one can instead apply any other rule applicable to the premise repetitively). Proofs without infinitely descending chains are called well-founded. Positively, one can define the set of well-founded proofs as the least set of proofs, such that if there are derivations d_{i} of Γ_{i} (i ∈ I) in this set and a rule deriving Γ from Γ_{i}(i ∈ I) then the derivation

d_{i}

⋯ Γ_{i} ⋯ (i ∈ I)

Γ

is in this set.

Without using the cut- and repetition rule one can derive A, ¬A by induction on the built-up of formulae. For prime formulae this is clear (since either A or ¬A is true), and for instance in case A = B ∧ C (note that ¬(A ∧ B) = ¬A ∨ ¬B) this follows by:

\begin{matrix}\begin{matrix}A, ¬A \\ A, ¬A ∨ ¬B \end{matrix} & \begin{matrix}B, ¬B \\ B, ¬A ∨ ¬B \end{matrix} \\ A ∧ B, ¬A ∨ ¬B \end{matrix}

Elimination rules for the logical connectives are provable using the cut rule. For instance, the proof that from Γ, A ∧ B we can derive Γ, A is as follows (note that ¬(A ∧ B) = ¬A ∨ ¬B):

Γ, A ∧ B  \begin{matrix}¬A, A \\ ¬A ∨ ¬B, A \end{matrix} (Cut)
Γ, A

Interpretation of PA into PA^{∗}. We show, by induction over the derivation, that if a sequent Γ is derivable in PA depending on free variables x_{1}, …, x_{k}, then for all n_{1}, …, n_{k} ∈ ℕ the sequent Γ[x_{1} := n_{1}, …, x_{k} := n_{k}] is derivable in PA^{∗}. Here Γ[x_{1} := n_{1}, …, x_{k} := n_{k}] denotes the result of substituting in all formulas in Γ the variables x_{i} by n_{i}. We consider some of the more important cases:

Case Γ is an axiom of PA: All instances of defining equations for primitiverecursive functions are true prime formulae, and therefore axioms in PA^{∗}. The equality axioms can be written as sequents of prime formulae (e.g. x = y → y = x can be rewritten as x ≠ y, y = x), and then each instantiation is an axiom of PA^{∗} (if we substitute x by n and y by m in x ≠ y, y = x, then we get n ≠ m, m = n and either n ≠ m or m = n is true, hence an axiom). One minor problem is the transfer principle x = y → A(x) → A(y) for arbitrary formulae A. One can easily see that, from the transfer principle restricted to prime formulae and negated prime formulae A one can prove using logical rules only the transfer principle for arbitrary formulae, so we can restrict in PA the principle to (negated) prime formulae. If we rewrite the transfer principle for (negated) prime formulae as x ≠ y, ¬A(x), A(y), we get a sequent, such that every instance is an axiom of PA^{∗}.

Case Γ is derived from logical rules: The introduction rules for ∧ and ∨ follow from the corresponding rules of PA^{∗}, and the elimination rules are derivable, as we have seen above. We consider the case of ∀-introduction: Assume that Γ = Δ, ∀x.A(x), which is derived from Δ, A(x), where x is not free in Δ. Assume for simplicity that x is the only free variable in Δ, A(x). Then by induction hypothesis we know that we can show Δ, A(n) for all n, and obtain therefore the following proof of Δ, ∀x.A(x):

\begin{aligned}Δ, A(0) & Δ, A(1) & ⋯ \\ & Δ, ∀x.A(x) \end{aligned}

The case of an introduction rule for ∃ is similar.

Induction: We haven’t specified precisely yet, how to formulate the induction principle in PA, and for our purposes the easiest way is to use the induction rule

\begin{aligned}Δ, A(0) & Δ, ∀x(A(x) → A(x + 1)) \\ & Δ, ∀x.A(x) \end{aligned}

Assume that Γ = ∀x.A(x) is derived by the above rule, and for simplicity assume that Δ is empty. By induction hypothesis, we have proofs in PA^{∗} of A(0) and ∀x(A(x) → A(x+1)). From ∀x(A(x) → A(x+1)), which is the same as ∀x(¬A(x)∨ A(x + 1)), we obtain, using the fact that elimination for ∀ is derivable, a proof of ¬A(n), A(n + 1) as follows (note that ¬(¬A(n) ∨ A(n + 1)) = A(n) ∧ ¬A(n + 1)):

{∀x(¬A(x) ∨ A(x + 1)) \atop ¬A(n) ∨ A(n + 1)}  \begin{matrix}A(n), ¬A(n) & ¬A(n + 1), A(n + 1) \\ A(n) ∧ ¬A(n + 1), ¬A(n), A(n + 1) \end{matrix} (Cut)
¬A(n), A(n + 1)

Now we obtain proofs in PA^{∗} of A(n) for all n as follows:

\begin{matrix}\begin{aligned}A(0) & ¬A(0), A(1) \\ & A(1) \end{aligned} & ¬A(1), A(2) \\ A(2) \end{matrix} ; · ; · ; · ; A(n)

Using the introduction rule for ∀ we obtain therefore a proof of ∀x.A(x) as follows (note that the proof of A(n) has height at least n):

\begin{aligned}A(0) & A(1) & A(2) ⋯ \\ & ∀x.ϕ(x) \end{aligned}

Since the proof of the nth premise has height at least n, the proof of ∀x.A(x) has infinite height.

Every well-founded set can be linearised, and the resulting well-ordered set is order isomorphic to the set of ordinals, and therefore the height of infinite proofs can be measured by ordinals. One writes ⊢_{n}^{α} Γ for “Γ is provable in the system with ordinal height at most α and cut rank < n”, where the rank n of a formula is a natural number which measures the size of the formula (for instance the number of connectives ∧, ∨, ∀, ∃ in the formula), and the cut rank of a proof is the maximum rank of all cut formulas, if it exists. So, if we have ⊢_{n_{i}}^{α_{i}} Γ_{i} for the premises Γ_{i} of a rule with conclusion Γ, and if α_{i} < α, n_{i} ≤ n, and, in case we have a cut, if the rank of the cut formula is < n, then ⊢_{n}^{α} Γ follows.

Every proof in Peano Arithmetic can now be interpreted in this system as a proof of height < ω + ω and with finite cut rank. The main step in the consistency proof is to prove cut elimination, i.e. that from a derivation of a sequent in this calculus one obtains a cut-free derivation of the same sequent. As an example for how cut elimination is carried out, consider the following derivation:

\begin{matrix}\begin{matrix}Γ, A ∧ B, A & Γ, A ∧ B, B \\ Γ, A ∧ B \end{matrix} & {Γ, ¬A ∨ ¬B, ¬A \atop Γ, ¬A ∨ ¬B} \\ Γ \end{matrix}

This can be replaced by the following derivation, in which the original cut is reduced by ones with smaller cut rank or same cut rank and smaller natural sum of the heights of the subderivations:

\begin{aligned}\begin{aligned}Γ, A ∧ B, A & & Γ, ¬A ∨ ¬B \\ & Γ, A \end{aligned} & & \begin{matrix}Γ, ¬A ∨ ¬B, ¬A & Γ, A ∧ B \\ Γ, ¬A \end{matrix} \\ & Γ \end{aligned}

By systematically carrying out reduction steps like the above, one can eventually eliminate all cuts. More formally, one can show that from ⊢_{n+1}^{α} Γ it follows ⊢_{n}^{2^{α}} Γ.

Therefore we have that if Peano arithmetic proves falsity, i.e. the empty sequent,

then ⊢_{n}^{β} ∅ for β = \underbrace{2^{2^{·^{·^{ρ}}}}}_{n times} for some ρ < ω + ω. It follows that β < ϵ_{0}. Since a

cut-free proof of the empty sequent can only end by a repetition rule, it follows by transfinite induction up to ϵ_{0} that there is no cut free proof of the empty sequent, and therefore no proof of an inconsistency in Peano Arithmetic.

One can formulate the above argument in PRA extended by the principle of transfinite induction up to ϵ_{0} over quantifier-free formulae. The most elegant proof is due to Buchholz [Buchholz, 1991] (see as well [Michelbrink, 2000] for an extension to Kripke-Platek set theory plus Π_{3}-reflection). Buchholz introduces a primitive recursive notation system for infinitary derivations as follows: He starts with a notation system for proofs in Peano Arithmetic. Furthermore, for each lemma in the cut elimination proof he introduces a notation, which takes one or more infinitary derivations corresponding to the assumptions of that lemma, and has as result an infinitary derivation corresponding to the conclusion. Then he computes for every notation the last formula, the last rule, the cut rank, the height, and notations for the derivations of the premises. The notations for the subderivations might be longer than that of the derivation itself. The functions computing these results are primitive-recursive, and one can show in PRA that the computed derivations of the premises of a rule actually compute the premises of the last rule, have a smaller height and that the condition on the cut rank is fulfilled. We need now quantifierfree transfinite induction up to ϵ_{0} (and this is the only place where this principle is needed) in order to show that there is no derivation of the empty sequent, i.e. that PA is consistent. Note that in this proof the use of the principle of quantifier-free transfinite induction up to ϵ_{0} is concentrated in the last step of the proof.

Proof-theoretic strength. It follows therefore that PRA plus transfinite induction up to ϵ_{0} proves the consistency of PA. Since PRA can be embedded into PA, it follows that PA does not prove transfinite induction up to ϵ_{0}. We have indicated above that PA proves transfinite induction up to every ordinal less than ϵ_{0} (w.r.t. the ordinal notation system we use). Therefore it follows that, for the ordinal notation system chosen, ϵ_{0} is the supremum of all ordinals, up to which transfinite induction can be shown.

One can obtain as well a sharper result, which refers to arbitrary ordinal notation systems. It can be shown that, if we add to PA one free predicate symbol (i.e. a symbol for a set X with no further axioms, but with all the logic and equality rules and the principle of induction extended to formulas containing X), then the supremum of the ordinals α, s.t. there exists an ordinal notation system of order type α and we can prove transfinite induction w.r.t. the free predicate in it, is ϵ_{0}.

For the above reasons, ϵ_{0} is called the proof theoretic strength of Peano Arithmetic. Note that we were referring to two slightly different notions: one is referring to the limit w.r.t. a canonical notation system. The other one refers to the principle of transfinite induction for a new predicate X in an extended language, but w.r.t. arbitrary ordinal notation systems. For most theories considered, both notations coincide, and therefore the limit of transfinite induction provable in a theory T, understood in one of the two ways above, is called the proof theoretic strength |T | of T.

In ordinal-theoretic proof theory, the techniques of Gentzen were extended further and the strength of increasingly strong theories was developed. One open question is what is meant by a canonical ordinal notation system, and one usually uses the notion “natural ordinal notation system”. No conclusive answer has been found, and it might be in principal impossible to characterise all natural ordinal notation systems – if one has a mathematical precise notation, it is likely that one can diagonalise over it and then find a ordinal notation system, which is intuitively natural, but not covered by the definition. However, the standard ordinal notation systems used in ordinal theoretic analyses are regarded in general as natural ones, and it might be that this is the right approach to the notion of naturalness: to develop strong ordinal notation systems and investigate afterwards, whether they can be regarded as natural ones.

3 A Proof-Theoretic Programme

A foundational programme. What Gentzen has achieved, is to reduce the consistency of Peano Arithmetic to the principle of transfinite induction up to ϵ_{0}. The well-foundedness proof up to ϵ_{0} is very perspicuous, and this gives strong evidence to the fact that PA is consistent. This proof together with other analyses of PA has contributed to the fact that not many people nowadays still have doubts about the consistency of PA, even so we cannot prove that fact.

In ordinal theoretic proof theory increasingly strong theories were analysed, with increasingly complicated ordinal notation systems. The corresponding wellfoundedness proofs became less and less perspicuous. Although by Gödel’s second incompleteness theorem, a real reduction of the principles needed in order to prove the consistency of a theory is not possible, one could at least hope for a reduction to principles which are more evident. By carrying out an ordinal analysis alone that has not necessarily been achieved – what one obtains is the concentration of the consistency strength to the well-ordering of an ordinal notation system. Therefore the author believes that the determination of the proof theoretic strength should only be a first step in a proof theoretic analysis. A second step is required, namely to develop theories, in which we can prove the well-foundedness of the ordinal notation system and therefore (assuming that PRA can be embedded into those theories) the consistency of the theories involved. And such theories should be formulated in such a way that in every proof step of such a theory there is direct evidence that the truth of the premises implies the truth of the conclusion. This insight needs to be, because of Gödel’s theorem, a philosophical argument. If such an analysis has been carried out, we know that everything derived in such a theory is correct. Such theories will then be a substitute for Hilbert’s finitary methods, we can call them extended finitary methods. The up to now most successful theories used for this purpose seem to be extensions of Martin-Löf type theory, and the philosophical argument are meaning explanations as given by Per Martin-Löf. An alternative approach taken have been Feferman’s theories of explicit mathematics, but unfortunately up to now only partial philosophical analyses have been carried out for those theories. In the following, we will discuss how strong extensions of type theory are developed and how the corresponding reductions are carried out. However, in this article we will not investigate meaning explanations in detail.

Applications. Philosophical reasons are one motivation for following the programme described. Another major motivation for it comes from applications.

Martin-Löf type theory can be considered as a functional programming language, and there exists one fully developed functional language, Cayenne [1] based on dependent types. When considering Martin-Löf type theory as it stands, we already have data structures available which do not occur in other languages or are not often used there: we have the W-type, which represents infinitely branching trees (instances of this type can be represented in other languages, it is only when we want to introduce the W-type as a general concept that we need dependent types), and we have universes, which are types, the elements of which represent types. Both principles increase the strength of type theory substantially, and this is one of the reasons, why they were added. When investigating strong extensions of type theory, which allow to prove the well-foundedness of strong ordinal notation systems, we are searching for new data types, which we hope will be of use in general programming as well. One result of this programme is the development of the data type of inductive-recursive definitions (see Sect. 7), which uses principles developed first in the context of the Mahlo universe as part of this programme.

4 Type Theory with W-Type and Atom

One step in this proof theoretic programme was the proof theoretic analysis of the theory ML_{1}W of Martin-Löf type theory with one standard universe and one Wtype by the author ([Setzer, 1993], [Setzer, 1998]). Independently, E. Griffor and M. Rathjen [Griffor and Rathjen, 1994] have analysed a slightly weaker theory, which has one standard universe closed under the W-type, and additionally Aczel’s type V of iterated sets, but in which the formation of the W-type is restricted to elements of the universe only. Both theories do not include the logical framework, so there is no type Set and there are no judgements of the form A : Set or A = B : Set. In our analysis, we obtained an upper bound for the proof theoretic strength of ML_{1}W with extensional equality, and proved the lower bound for ML_{1}W with intensional equality. Since both bounds coincide, this showed that both theories have the same strength.

In this section we make a first step towards this result, and consider the strength of type theory with W-type and a microscopic universe atom. In the Sect. 5 we will then look at the full theory.

The W-type. The assumptions for forming the W-type are A : Type and x : A ⇒ B(x) : Type, from which one can form (Wx : A.B(x)) : Type. (When writing B(x) we mean that B might depend on x, and that later on B(r) means the result of substituting x by r in B.) Its canonical elements are introduced by the following introduction rule:

Γ ⇒ r : A  Γ ⇒ s : B(r) → (Wx : A.B(x))
Γ ⇒ sup(r, s) : (Wx : A.B(x))

An element sup(r, s) of Wx : A.B(x) is a tree with label r and subtrees s(b) for b : B(r). The elements of Wx : A.B(x) are therefore trees with branching degrees (B(a))_{a:A}. They can be visualised as follows (assume in this picture that B(r′′) is empty, therefore sup(r′′, s′′) has no subtrees s′′(y) for y : B(r′′)):

no subtrees

s′(c′)  ⋯  s′(c) = sup(r′′, s′′)
s(b′)  ⋯  s(b) = sup(r′, s′)
sup(r, s)
b′ b c′ c

The elimination rule for the W-type formalises induction over trees, which expresses that we have the “least type closed under the introduction rule”, and that therefore elements of Wx : A.B(x) are well-founded trees.

In standard models of the Wx : A.B(x), one can define the height height(t) of a tree t, which is an ordinal, inductively as follows: height(sup(r, s)) = sup{s(b) + 1 | b ∈ B′(b)}, where B′(b) is the interpretation of B(x) for x = b. The height of Wx : A.B(x) (in a standard model) is defined as the supremum of the heights of its elements (in a standard model).

Finite types. In all type theories which we will consider in this article, we have types with finitely many elements, which we denote for the sake of simplicity by {0, 1, …, n − 1} (or ∅ in case of n = 0). (The real type theoretic notation is N_{n}, having elements called i_{k} or A_{i}^{k}.) For the sake of readability, we sometimes write False for ∅ (the formula with no proof), True for {0} (the formula with exactly on proof), tt for the element of True, Bool for {0, 1}, and true, false for the elements of Bool.

Atom and the type theory MLW_{atom}. We add a type constructor atom with typing x : Bool ⇒ atom(x) : Type to our type theory, together with equality rules atom(true) = True and atom(false) = False. So atom takes a Boolean value and translates it into a formula corresponding to its value.

When looking later at universes, we will see that we have here the case of a microscopic universe Bool with two elements representing True and False. Without any universe at all one can show that one can model type theory in such a way that the interpretation of a type A(x) does not depend on x. If we interpret in such a model Wx : A.B(x) in a standard way, then we have that the interpretation of B(x) is either empty for all x, or non-empty for all x. If B(x) is empty for all x, then trees have no subtrees, hence have height 0. If the interpretation of B(x) is non-empty for all x, the interpretation of Wx : A.B(x) is empty, since in order to form an element sup(r, s), we need to have defined before s(y) : (Wx : A.B(x)) for one of the elements y of B(x). In both cases, the height of Wx : A.B(x) is 0. Type theory without a universe is known to be very weak – it does not even show Peano’s fourth axiom, namely that in the type N of natural numbers, 0 is different from S(n).

We call the type theory having standard types, atom, and the W-type, MLW_{atom}.

Admissibles and ℵ_{α}^{rec}. In order to understand the strength of type theories involving the W-type, we need the notion of recursively regular or (an equivalent name) admissible ordinals, a notion originating from generalised computability theory. Classical computability is the theory of computable functions, where computable means computable by any mechanical device. There, one has developed a schema for defining so called partial recursive functions f : ℕ^{n} →^{∼} ℕ. Partial as expressed by the symbol →^{∼} means that f : dom(f) → ℕ for some set dom(f) ⊆ ℕ^{n}. Recursive functions are total partial recursive functions, i.e. functions f : ℕ^{n} →^{∼} ℕ s.t. dom(f) = ℕ^{n}. One assumes that the set of partial recursive functions coincides with the set of computable functions. Note that computable is not a mathematical notion, therefore the fact that all computable functions are partial recursive is not a mathematical statement and can therefore not be proved – however, most researchers believe that all computable functions are partial recursive. One can encode partial recursive functions as natural numbers, and writes f = {e}^{n}, if

f : ℕ^{n} →^{∼} ℕ has code e.

In generalised computability theory, one extends the schema for defining partial recursive functions to ordinals, and obtains the notion of κ-partial recursive functions f : κ^{n} →^{∼} κ (where κ is an ordinal). For a detailed description, see for instance Chapter VIII of [Hinman, 1978]. f : α → κ is κ-recursive in parameters < κ, if f = λγ.g(γ, β_{0}, …, β_{n−1}) for some β_{i} < κ and κ-partial recursive g : κ^{n+1} → κ, and if f(γ) is defined for all γ < α. A limit ordinal κ is admissible, if it is closed under the formation of suprema of κ-recursive functions in parameters < κ: If α < κ and f : α → κ is κ-recursive in parameters < κ, then sup_{γ<α} f(γ) < κ.

One defines now by recursion on the ordinal α ordinals ℵ_{α}^{rec} as follows: ℵ_{0}^{rec} = ω, the least infinite ordinal and least admissible ordinal; ℵ_{α+1}^{rec} is the least admissible ordinal above ℵ_{α}^{rec}; and if λ is a limit ordinal, then ℵ_{λ}^{rec} = sup_{β<λ} ℵ_{β}^{rec}. Usually, for limit ordinals λ, ℵ_{λ}^{rec} is not an admissible; but ℵ_{0}^{rec} and ℵ_{α+1}^{rec} are admissible. Every admissible ordinal is of the form ℵ_{α}^{rec} for some α.

Admissible ordinals are the recursive analogue of regular cardinals. An ordinal κ is a regular cardinal, if κ is not the supremum of β < κ many ordinals < κ: There exists no β < κ and f : β → κ s.t. κ = sup_{α<β} f(α). Note that here f can be arbitrary, whereas for admissibles it had to be recursive, having parameters < κ.

Admissibles and the W-type. The heights of W-types are closely related to admissible ordinals. Assume, that terms are encoded as natural numbers and assume a standard interpretation A′ of A and of B(x) for x ∈ A′ as B′(x), where A′ and B′(x) are sets of natural numbers encoding the elements of this type. (A rough idea would be to interpret N as ℕ and A → B as {e | ∀x ∈ A′.{e}(x) ∈ B′}. The detailed model is more complicated – in fact, more precisely one has to take equality of terms into account and interpret a type as a set of pairs of natural numbers, where a pair (n, m) being an element of the interpretation of A means that n and m are codes for equal elements of A). Then the standard interpretation of Wx.A.B(x) is the least set C s.t., if k ∈ A′ and ∀l ∈ B′(k).{e}^{1}(l) ∈ C, then π(k, e) ∈ C. Here π : ℕ^{2} → ℕ is the standard encoding of pairs of natural numbers as natural numbers. So C is the least set of recursive trees with branching degrees B′(k) for k ∈ A′.

If we take A = {0, 1} and B(0) = ∅, B(1) = {0} and let O_{0} := (Wx : A.B(x)), we can see that the elements of the interpretation of O_{0} are of the form sup(1, λx. sup(1, λx. sup(1, ⋯ sup(0, λx.e)) ⋯))) (more precisely, they are equal modulo the η-rule to such a tree). These trees have heights n for n ∈ ω, so (the standard interpretation of) O_{0} has height ω = ℵ_{0}^{rec}, the least admissible ordinal.

If we take A = {0, 1, 2} and B(2) = O_{0}, otherwise B(x) as before, we obtain Kleene’s O (in the usual definition, one has B(2) = ℕ instead of O_{0}), which has height ℵ_{1}^{rec}, the second admissible ordinal.

In general, the nth admissible ordinal ℵ_{n}^{rec} is the height of (the standard interpretation of) O_{n} := Wx : {0, 1, …, n + 1}.B(x), where B(0) = ∅, B(1) = {0}, B(k) = O_{k−2} for k > 1.

We can obtain a more uniform version of this, by replacing B(0) by O_{−2} := Wx : ∅.B(x), which is empty, and by replacing B(1) by O_{−1} := Wx : {0}.B(x), where B(0) = O_{−2}, which contains only trees of height 0. Then we obtain O_{n} = Wk : {0, …, n + 1}.O_{k−2} for n ≥ −2.

Lower bound for |MLW_{atom}|. Using the admissibles (ℵ_{n}^{rec})_{n∈ω}, one can form an ordinal notation system. The ordinal notations will be terms for expressions formed from 0, some standard operations on ordinals, and so called collapsing function ψ_{κ} for κ > ω admissible, mapping ordinals to ordinals < κ. We won’t introduce ψ_{κ} in detail. ψ_{κ} collapses ordinals into the interval [0, κ[ and is weakly monotone (α < β → ψ_{κ}(α) ≤ ψ_{κ}(β)). Ordinal notation systems like this are usually constructed using regular cardinals instead of admissibles, but with some extra work, which has been carried out in some cases (e.g. [Schlüter]), one can see that one can replace those regular cardinals by their recursive analogues. One can simulate now these functions by replacing ordinals by elements of O_{n} and then show that the type theory in question proves transfinite induction up to ψ_{ℵ_{1}^{rec}}(ℵ_{n}^{rec}), which in the limit reaches ψ_{ℵ_{1}^{rec}}(ℵ_{ω}^{rec}). This provides a lower bound for this theory. Details for the lower bound of a closely related type theory can be found in [Setzer, 1994].

Kripke-Platek set theory. For an upper bound, one interprets type theory into an extension of Kripke-Platek set theory, which we will introduce in the following.

This will show that the formation of O_{n} essentially exhausts the strength of type theory with W-type and a microscopic universe.

Kripke-Platek set theory KP is a weak version of set theory, which is closely connected to admissibles. It was developed by Kripke [Kripke, 1964] and Platek [Platek, 1966]. KP is obtained from standard ZF-set theory essentially as follows: one omits the existence of the power set of any set; one omits the infinity axiom, claiming the existence of an infinite set; one restricts the formation of {x ∈ a | φ(x)} to Δ_{0}-formulae φ (i.e. formulae in which all quantifiers are bounded, i.e. of the form ∀x ∈ a or ∃x ∈ a) – the corresponding principle is called Δ_{0}-separation; one restricts the so called collection principle expressing that if ∀x ∈ a.∃y.φ(x, y) then there exists a b s.t. ∀x ∈ a.∃y ∈ b.φ(x, y) to Δ_{0}-formulae φ – the new principle is correspondingly called Δ_{0}-collection. The precise axiomatisation can be found in the detailed monograph [2] on Kripke-Platek set theory.

The relationship to admissible ordinals is as follows: There exists an operation (called constructible hierarchy) which maps ordinals α to sets L_{α}, where L_{0} = ∅, L_{λ} = ⋃_{α<λ} L_{α} for λ limit ordinal, and L_{α+1} is the result of applying certain operations for forming new sets (such as forming pairs, unions of sets or the domain and range of relations) to sets in L_{α} ∪ {L_{α}}. Now one can show that L_{α} is a model of KP iff α is admissible, and introduce a notion of “admissible set” (as opposed to “admissible ordinal”), which holds for a set iff it is of the form L_{α} for an admissible α.

KP in Proof Theory. In proof theory, extensions of KP by axioms claiming the existence of many admissibles are often used as reference theories (see especially the monograph [Jäger, 1986]). More precisely, one adds a predicate Ad(x) standing for “x is an admissible set”, axioms stating that Ad(x) implies that x is a model of KP, and axioms claiming the existence of elements fulfilling this predicate (for instance a fixed number of admissibles, arbitrarily finitely many admissibles, or axioms claiming the existence of admissibles closed under certain operations). Many of these extensions have been analysed proof theoretically, and are used as reference theories. The strength of other theories is usually obtained by comparing them with those reference theories.

General Technique for Developing Upper Bounds of Martin-Löf Type Theory. Our standard technique for determining upper bounds for the strength of variants of Martin-Löf type theories is to model them in extensions of KP having the same proof-theoretic strength. Assume that we have done this for a variant of type theory called MLTT^{var} and a variant of KP called KP^{var}. Then the above provides us with a model of MLTT^{var} in a set theory of minimal strength. The main purpose for developing this model is to obtain an upper bound for the proof theoretic strength of MLTT^{var}. We will be able to show using this model that, if MLTT^{var} proves transfinite induction up to a certain ordinal (more precisely up to an ordinal notation), then the same holds for KP^{var}. Therefore |MLTT^{var}| ≤ |KP^{var}|. If the variants of KP chosen have been analysed proof theoretically, one obtains a concrete ordinal α = |KP^{var}|, and we have |MLTT^{var}| ≤ α.

Note that KP and its extensions are classical theories and therefore not constructive. However, apart from the proof theoretic result, which measures the strength of the theory, we believe that modelling a theory in a set theory of minimal strength provides additional insight into what can be achieved in type theory. Furthermore, once we have shown the other direction, i.e. that |MLTT^{var}| ≥ α = |KP^{var}|, one can easily show that MLTT^{var} shows the consistency of approximations of KP^{var}, such that each proof in KP^{var} can be formalised in one of these approximations. This provides us with a constructive understanding of KP^{var}.

A more refined analysis often shows as well that MLTT^{var} and KP^{var} show the same arithmetic Π_{2}-sentences, i.e. the same formulae ∀x ∈ ℕ.∃y ∈ ℕ.φ(x, y), where φ(x, y) is a quantifier-free arithmetic formula. Such formulae can be considered as the specifications of programs, and from each proof of such a formula in MLTT^{var} one obtains a program computing a function f : ℕ → ℕ s.t. ∀x ∈ ℕ.φ(x, f(x)) holds. So one can say that the provably total programs in KP^{var} and MLTT^{var} coincide.

Upper bound for |MLW_{atom}|. In MLW_{atom}, we can define O_{n}, which corresponds to the possibility of forming finitely many admissible, and we claimed that this essentially exhausts the strength of this theory. A variant of Kripke-Platek set theory, which allows to form finitely many admissibles, is the theory KPl. Its standard model is L_{ℵ_{ω}^{rec}}. ℵ_{ω}^{rec} is not an admissible, so the standard model of KPl doesn’t fulfil the axioms KP, and we can’t include all axioms of KP into those of KPl. What is omitted is that the set theoretic universe fulfils Δ_{0}-collection – however, restricted to any a s.t. Ad(a), Δ_{0}-collection will hold. Further one demands that every set is contained in an admissible set. So we can form a sequence Ad_{0} = ∅, and Ad_{n+1} as being one admissible above Ad_{n} for Meta-n ∈ ω, but without Δ_{0}-collection it is not possible to form this sequence inside the theory. If one could, then one could form Ad_{ω} := ⋃_{n∈ω} Ad_{n} and hence an admissible above Ad_{ω}.

One can now form a model of MLW_{atom} in KPl. Essentially, we interpret each type A(x) as an element of Ad_{n} for some n uniformly for all x. The main step is to interpret Wx : A.B(x). If A and B′(x) are interpreted as A′ and B′(x), which are elements of Ad_{n}, and if κ is the supremum of the ordinals in Ad_{n}, then Wx : A.B(x) is interpreted by iterating a certain operator (which forms trees with subtrees having been formed before) κ many times. The result is an element of Ad_{n+1}.

In general, in order to obtain a fixed point of such kind of operators (more precisely Σ_{1}-operators), we need to iterate the operator up to an admissible ordinal corresponding to the least admissible set containing all set parameters used by this operator.

5 Type Theory with W-Type and one Universe

In this section we consider the theory ML_{1}W, which is Martin-Löf type theory with W-type and a universe closed under the W-type.

Universes and the type theory ML_{1}W. A universe is the type theoretic formalisation of a type the elements of which are types. This suggests that a universe should be a type U, s.t. for x : U we have x : Type, as in so called “universes à la Russell”. However, this causes conceptual problems, since in this step a term x becomes a type, and changes therefore its category. (Note that in a term model, a term is interpreted by itself, whereas a type is interpreted for instance as a set of terms; something similar happens in meaning explanations.) In order to avoid such conceptual problems (note that Martin-Löf type theory is considered as well as a foundation of mathematics), it is better to keep terms and types separted and work with “universes à la Tarski”: a universe is a type U, the elements of which are codes for types. We need therefore an additional decoding function T, the typing of which is giving by the judgement x : U ⇒ T(x) : Type. If x is an element of U, i.e. a code for type, T(x) is the type, x denotes.

The microscopic universe atom introduced in Sect. 4 is a universe in this sense: the underlying set is Bool and the decoding function is atom: we have x : Bool ⇒ atom(x) : Set.

A standard universe U is a universe closed under all standard type constructions. This means for instance that there is a code N̂ : U (i.e. a constructor N̂ of U) for the type N of natural numbers, so T(N̂) = N. Similarly, we have codes for the types {0, …, l − 1}. Standard universes are closed under +, Π, Σ, so for instance we have that, if r : U, and s is s.t. x : T(r) ⇒ s(x) : U, then (Σ̂x : r.s(x)) : U and T(Σ̂x : r.s(x)) = Σx : T(r).T(s(x)) for a constructor Σ̂ of U.

ML_{1}W has now the standard types, the W-type and a standard universe U, which is closed additionally under the W-type: if r and s(x) are as for the premises of the Σ̂-introduction rule above, then (Ŵx : r.s(x)) : U and T(Ŵx : r.s(x)) = Wx : T(r).T(s(x)) for a constructor Ŵ of U.

Strength of ML_{1}W. We will in this section provide some intuition concerning the strength of ML_{1}W, more details can be found in Appendix B. In the presence of a universe closed under the W-type, we can define by induction on n : N codes Ô_{n} : U for the finitely iterated trees O_{n}, and therefore form O_{ω+1} := Wx : N.T(Ô_{n}), which is a W-type of height ℵ_{ω+1}^{rec}, the first admissible bigger than ℵ_{n}^{rec} for n ∈ ω. O_{ω+1} can be represented by an element of U. We can iterate the above process as well over any W-type which has a code in U. By iterating it over W_{1} := O_{1}, we can form trees of height ℵ_{α}^{rec} for α < ℵ_{1}^{rec}, and then form a W-type W_{1} of height ℵ_{ℵ_{1}^{rec}+1}^{rec}. Doing the same with W_{2} instead of O_{1}, we reach ℵ_{ℵ_{ℵ{rec \atop 1}+1}^{rec}+1}^{rec} by a tree W_{3}. Continuing this

process, we obtain W-types W_{n} for n ∈ ω, s.t. the supremum of their heights is Λ^{rec} = sup_{n∈ω} \underbrace{ℵ_{ℵ_{ℵ{rec \atop ··_{·_{1}}}}^{rec}}^{rec}}_{n times}. Λ^{rec} is the first (non-admissible) fixed point of λα.ℵ_{α}^{rec}. W_{n}

can be formed as elements of U, and therefore we can form a W-type inside U, which has as height the least admissible ℵ_{Λ^{rec}+1}^{rec} above Λ^{rec}. In general, if we have formed a W-type of height α, then we can iterate the formation of O_{γ} for γ < α as elements of U and form therefore a W-type of height ℵ_{α+1}^{rec}. So the height of the W-types, we can form as elements of U, must be an admissible κ, which is closed under λβ.ℵ_{β}^{rec}. In order to obtain this is property, it suffices to demand that for every α < κ there exists an admissible π s.t. α < π < κ, and admissibles with this property are called recursively inaccessible ordinal. Admissible sets corresponding to such ordinals are called recursively inaccessible sets. Recursively inaccessible ordinals are the recursive analogue of strongly inaccessible cardinals. One can form a model of ZFC (Zermelo-Fraenkel set theory with axiom of choice), s.t. the supremum of ordinals in this model is the first strongly inaccessible cardinal, therefore the existence of strongly inaccessible cardinals cannot be shown in ZFC.

So we have now obtained some intuition that we can form inside the universe W-types, s.t. the supremum of their heights reaches (in the standard model) I^{rec}, the least recursively inaccessible ordinal. We can form further W-types on top of U, which are no longer elements of U, and which have heights κ_{n} := ℵ_{I^{rec}+n}^{rec}, the nth admissible above I^{rec}. We can do this only by Meta-induction over n, and the supremum of the heights of W-types, we can form, is I^{+} := ℵ_{I^{rec}+ω}^{rec} = sup_{n∈ω} κ_{n}.

Upper bound for |ML_{1}W|. An upper bound for the strength of ML_{1}W can be obtained by modelling it in a theory KPI^{+}, which has standard model L_{I^{+}}. In KPI^{+} we have one recursively inaccessible set Ad_{I}, and constants for finitely many admissibles above it. (Alternatively, one can define it as the theory KPl plus the existence of one recursively inaccessible.) We can model U by iterating an operator (which essentially forms new sets representing Ŵx : a.b(x), Σ̂x : a.b(x) etc. from sets previously defined). In order to reach a fixed point, we have to iterate this operator up to I^{rec}, which is the union of all ordinals in the recursively inaccessible set Ad_{I}. If we form the representation of Wx : A.B(x) from sets A and B(x) s.t. A and B(x) are elements of L_{α}, one can see that the representation of Wx : A.B(x) is an element of L_{α^{++}}, where α^{++} is the second admissible above α. A fixed point of this operator is obtained if we iterate it up to an admissible, which is closed, in order to accommodate for the formation of Wx : A.B(x), under the step from α to α^{++}. That’s why we need a recursively inaccessible ordinal, in order to reach the fixed point. The interpretation of U is an element of L_{κ_{1}}. We can form Wtypes making use of U and sets constructed from it, and each W-type construction corresponds to iterating an operator up to the next admissible. An n-times nested W can be interpreted by iterating an operator up to κ_{n+1}, and the interpretation is an element of κ_{n+2}. This way we can model it in KPI^{+}.

A lower bound for |ML_{1}W| can be obtained by carrying out a well-ordering proof for an ordinal notation system which has the strength of KPI^{+}. Details for this proof can be found in Appendix B.

6 The Mahlo Universe

In proof theory, the next major step taken after treating theories of strength KPI was the analysis of KPM, Kripke Platek set theory plus the recursive Mahloness of the set theoretic universe, by Michael Rathjen [Rathjen, 1991]. An ordinal M is a recursively Mahlo ordinal, if it is admissible, and if for all f : M → M, which are M-recursive with parameters in M, there exists an admissible κ < M s.t. ∀α < κ.f(α) < κ. If one replaces in this definition “admissible” by “recursively inaccessible”, one obtains an equivalent definition. Recursively Mahlo sets are sets of the form L_{M} for recursively Mahlo ordinals M. In order to extend dependent type theory by a principle which reaches the strength of KPM, the author introduced in [Setzer, 2000] a type theory with one Mahlo universe. This type theory is substantially stronger than Martin-Löf type theory extended by standard types (including W-type and standard universes). We will in the following develop the rules for this type theory from the definition of recursively Mahloness.

In order to translate the Mahlo principle into type theory, we replace M by a family of types (V, T), i.e. we have V : Type and x : V ⇒ T(x) : Type.

A recursively inaccessible ordinal corresponds in type theory to a standard universe, so we add rules expressing that (V, T) is closed under the universe constructions and under the W-type.

The function f : M → M in the definition of recursively Mahloness can be translated as having a function f : Fam(V, T) → Fam(V, T), where Fam(V, T) := Σa : V.T(a) → V is the set of families of sets in V.

The existence of a recursively inaccessible κ can be translated into the existence of a subuniverse (U_{f}, s_{f}) of (V, T). This means that we have U_{f} : Type and s_{f} : U_{f} → V, which interprets each code in U_{f} as a code in V. For a : U_{f} we define S_{f}(a) := T(s_{f}(a)), which is the type corresponding to the code a.

We demand that (U_{f}, S_{f}) is a standard universe closed under the W-type, and that codes for the standard universe constructions in U_{f} correspond to codes in V. For instance, Ñ : U_{f} and s_{f}(Ñ) = N̂ for the code N̂ of N in V. s_{f} : U_{f} → V can now be lifted to a function s_{f}^{Fam} : Fam(U_{f}, S_{f}) → Fam(V, T), where s_{f}^{Fam}(⟨x, y⟩) = ⟨s_{f}(x), λy.s_{f}(y(x))⟩.

That ∀α < κ.f(α) < κ. will be interpreted as rules expressing that f : Fam(V, T) → Fam(V, T) is reflected by a function Res : Fam(U_{f}, S_{f}) → Fam(U_{f}, S_{f}), i.e. s_{f} ∘Res = f ∘s_{f}. Res constructs new elements of U_{f}, and we obtain corresponding constructors by splitting Res into two parts, namely Res0 : Fam(U_{f}, S_{f}) → U_{f} and Res1 : (x : Fam(U_{f}, S_{f})) → S_{f}(Res0(x)) → U_{f}. So Res as before is λx.⟨Res0(x), λy.Res1(x, y)⟩.

In type theory we split s_{f} ∘ Res = f ∘ s_{f} into two equality rules, one for Res0, namely s_{f}(Res0(⟨x, y⟩)) = π_{0}(f(s_{f}^{Fam}(⟨x, y⟩))), and one for Res1, namely s_{f}(Res1(⟨x, y⟩, z)) = π_{1}(f(s_{f}^{Fam}(⟨x, y⟩)))(z). Here π_{0}, π_{1} stand for the first and second projection.

Up to now the rules do not reach more strength than ML_{1}W, since we could easily model U_{f} := V and s_{f} := λx.x. Strength is reached by modelling the condition that κ ∈ M. This can be modelled as the existence of a constructor Û with argument f of V and the condition T(Û_{f}) = U_{f}. Note that this means that V has now a constructor which depends negatively on V, namely Û : (f : Fam(V, T) → Fam(V, T)) → V.

In type theory, it is more natural to replace f : Fam(V, T) → Fam(V, T) by two functions f_{0} : (a : V, b : T(a) → V) → V and f_{1} : (a : V, b : T(a) → V, T(f_{0}(a, b))) → V. In the same way, one replaces the type of Res0 by (a : U_{f_{0},f_{1}}, b : S_{f_{0},f_{1}}(a) → U_{f_{0},f_{1}}) → U_{f_{0},f_{1}}, similarly for Res1. The type of ⟨f_{0}, f_{1}⟩ is (Fam(V, T) → Fam(V, T))′ := ((a : V, b : T(a) → V) → V) × ((a : V, b : T(a) → V, T(f_{0}(a, b))) → V). By f⃗ : (Fam(V, T) → Fam(V, T))′ we mean in the following that ⟨f_{0}, f_{1}⟩ : (Fam(V, T) → Fam(V, T))′, similarly for g⃗.

MLM denotes the type theory with W-type and one Mahlo universe.

Constructive understanding of the Mahlo universe. There are two approaches in order to get a constructive understanding of the Mahlo universe.

The first approach uses partial functions. In order to give meaning explanations, we have to say what it means to be an element of the Mahlo universe, when two elements of the Mahlo universe are equal, and we have to understand for every element a of the Mahlo universe T(a) as a set. The understanding of the standard constructors for the universe is as usual. For instance, if a is an element of the Mahlo universe and for x in T(a), b is as well an element of it, then Σ̂x : a.b is an element of the Mahlo universe, and T(Σ̂x : a.b) is defined as Σx : T(a).T(b). Here we refer to the fact that we have understood already how to form from a set A and a set B(x) depending on x : A the set Σx : A.B(x). Σ̂x : a.b and Σ̂x : a′.b′ are equal, if a and a′ are equal, and if for x : T(a), b and b′ are equal.

In order to define, when Ûf⃗ is an element of the Mahlo universe, we introduce sets Uf⃗ together with functions sf⃗ : Uf⃗ → V for arbitrary terms f⃗. Note the reference to arbitrary terms. As an abbreviation, let in the following sFam ; f⃗ :

Fam(Uf⃗, Sf⃗) → Fam(V, T) be defined as sFam ; f⃗(⟨x, y⟩) = ⟨s_{f}(x), λy.s_{f}(y(x))⟩. We

write loosely f_{0}(sFam ; f⃗(⟨a, b⟩)) for f_{0}(π_{0}(sFam ; f⃗(⟨a, b⟩)), π_{1}(sFam ; f⃗(⟨a, b⟩))), similarly for

f_{1}(sFam ; f⃗(⟨a, b⟩), c).

By ⟨a, b⟩ being an element of Fam(Uf⃗, Sf⃗) we mean that a is an element of Uf⃗ and that for x in Sf⃗(a) it follows that b x is an element of Uf⃗.

First of all, we demand that Uf⃗ is closed under the usual universe constructions. For instance, if a is an element of Uf⃗, and for x in T(sf⃗(a)), b is an element of Uf⃗, then Σ̃x : a.b is an element of Uf⃗. Furthermore, sf⃗(Σ̃x : a.b) = Σ̂x : sf⃗(a), sf⃗(b), of which we know already that it is an element of the Mahlo universe.

We demand as well that Uf⃗ is closed under f⃗, provided f⃗ applied to the corresponding elements in V has a result in V: Assume ⟨a, b⟩ is an element of Fam(Uf⃗, Sf⃗). Assume that f_{0}(sFam ; f⃗(⟨a, b⟩) is an element of the Mahlo universe. Then we reflect this in Uf⃗ as an element Res0(a, b). So we demand that Res0(a, b) is an element of Uf⃗, and decode sf⃗(Res0(a, b)) = f_{0}(sFam ; f⃗(⟨a, b⟩)).

Assume additionally c is an element of T(f_{0}(sFam ; f⃗(⟨a, b⟩))), and f_{1}(sFam ; f⃗(⟨a, b⟩), c) is an element of the Mahlo universe. Then we reflect this in U_{f} and demand that Res1(a, b, c) is an element of Uf⃗ and sf⃗(Res1(a, b, c)) = f_{1}(sFam ; f⃗(⟨a, b⟩), c). Note that Uf⃗ depends on V.

Assume now Uf⃗ is closed under f, i.e. for every ⟨a, b⟩, which is an element of Fam(Uf⃗, Sf⃗) it is the case that f_{0}(sFam ; f⃗(⟨a, b⟩)) is an element of the Mahlo universe,

and that for every c as above, f_{1}(sFam ; f⃗(⟨a, b⟩), c) is an element of V. Then we have a complete understanding of Uf⃗ independently of any further elements added to V, and we demand that Ûf⃗ is an element of V and T(Ûf⃗) = Uf⃗.

Ûf⃗ and Ûg⃗ are equal iff for every element ⟨a, b⟩ of Fam(Uf⃗, Sf⃗) we have that f_{0}(sFam ; f⃗(⟨a, b⟩)) and g_{0}(sFam ; f⃗(⟨a, b⟩)) are equal elements of V, and, if for every c in

T(f_{1}(sFam ; f⃗(⟨a, b⟩))) we have that f_{1}(sFam ; f⃗(⟨a, b⟩), c) and g_{1}(sFam ; f⃗(⟨a, b⟩), c) are equal elements of V. We observe it is correct to identify the two sets since Uf⃗ and Ug⃗ are the same set, and therefore T(Ûf⃗) and T(Ûg⃗) are equal.

We have to show now that V fulfils the rules for the Mahlo universe. Assume f⃗ : (Fam(V, T) → Fam(V, T))′. Then it follows that Uf⃗ is closed under f⃗ in the sense as stated above, and therefore Ûf⃗ : V. If f⃗ and g⃗ are equal elements of (Fam(V, T) → Fam(V, T))′, then it follows that for a, b as above f_{0}(sFam ; f⃗(⟨a, b⟩))

g_{0}(sFam ; f⃗(⟨a, b⟩)) are equal, similarly for f_{1} and g_{1}, and therefore Ûf⃗ and Ûg⃗ are equal.

The problem with this construction is that we need to refer to the collection of all terms, and that we construct elements of the Mahlo universe, which we cannot derive in the type theory, namely those elements Ûf⃗, for which f⃗ is only total on the restriction to the elements sf⃗(a) of V, but not on the whole of Fam(V, T). This differs from ordinary meaning explanations, in which the rules are in one to one correspondence with the explanations.

A second approach to a constructive understanding of the Mahlo universe is directly in accordance with the rules for the Mahlo universe. However, up to now no mathematical precise model corresponding to it has been developed. Here we understand the Mahlo universe as an open concept. The Mahlo universe is again closed under the usual universe constructions. Assume now that we know from our knowledge about the Mahlo universe up to now that it is closed under some function f⃗ in the sense of being a function from Fam(V, T) into itself (more precisely in the sense of the primed version of the function space), independently of any further elements to be added later, and therefore not assuming a complete knowledge about V. Then we define Uf⃗ and sf⃗ as before, and then Ûf⃗ is an element of the Mahlo universe and T(Ûf⃗) = Uf⃗. Assume now that, independent of any elements to be added later to the Mahlo universe, f⃗ and g⃗ coincide as functions from Fam(V, T) into itself. Then Ûf⃗ and Ûg⃗ are equal elements of V.

Inconsistency of Mahlo universe with elimination rules. Erik Palmgren discovered in [Palmgren, 1998] that the Mahlo universe, extended by elimination rules, is inconsistent. This was shown in the following way. Let C be any fixed element of V. Let for ⟨f_{0}, f_{1}⟩ : (Fam(V) → Fam(V))′, F_{↓}(⟨f_{0}, f_{1}⟩) := λx.f_{0}(x, λy.C) : V → V, and for g : V → V, F_{↑}(g) := ⟨λx, y.g(x), λx, y, z.C⟩ : (Fam(V) → Fam(V))′. Then we have F_{↓}(F_{↑}(g)) = g : V → V, so we have (in a trivial way) embedded V → V into (Fam(V) → Fam(V))′. Let for ⟨f_{0}, f_{1}⟩ : (Fam(V) → Fam(V))′ G_{↓}(⟨f_{0}, f_{1}⟩) := Û_{f_{0},f_{1}} : V, and define, using the elimination rules of the Mahlo universe, G_{↑} : V → (Fam(V) → Fam(V))′ s.t. G_{↑}(Û_{f_{0},f_{1}}) = ⟨f_{0}, f_{1}⟩. Then we have G_{↑}(G_{↓}(⟨f_{0}, f_{1}⟩)) = ⟨f_{0}, f_{1}⟩, so we have embedded (Fam(V) → Fam(V))′ into V. Define for f : V → V f^{−} := G_{↓}(F_{↑}(f)) : V, and for v : V, v^{+} := F_{↓}(G_{↑}(v)) : V → V.

Then we have (f^{−})^{+} = f : V → V, so we have embedded V → V into V. Now we can interpret the untyped lambda-calculus into V by having as code for λ-abstraction the expression λ̂x.t := (λx.t)^{−}, and as code for the application of s to t the expression Âp(s, t) := s^{+}(t). It is easy to verify that for s : V, x : V ⇒ t : V β-equality holds: Âp(λ̂x.t, s) = t[x := s] : V. Now one defines as usual in the untyped lambdacalculus the Y-combinator as Y := λ̂x.Âp(V, V) where V := λ̂y.Âp(x, Âp(y, y)) and one gets for a : V, Âp(Y, a) = Âp(a, Âp(Y, a)) : V. Let { \atop False} be a code for False in U. Let u := Âp(Y, λ̂x.xˆ→{ \atop False}) : V. Then u = uˆ→{ \atop False} : V and therefore with A := T(u) A = A → False : Type. Now assuming a : A we obtain a : A → False and therefore a(a) : False. This shows f := λa.a(a) : A → False and therefore f(f) : False, so False is inhabited.

A model for the Mahlo universe and the upper bound for the prooftheoretic strength. A Model for the Mahlo universe was introduced in [Setzer, 1996] and used in order to determine an upper bound for the proof theoretic strength of the Mahlo universe, and to show the consistency relative to the corresponding set theory. The model was constructed using KPM^{+} as Meta theory.

KPM^{+} is similar to KPI^{+} Kripke-Platek set theory plus the existence of one admissible set Ad_{M} , for which the Mahlo axiom holds, i.e. if ∀x ∈ Ad_{M}.∃y ∈ Ad_{M}.φ(x, y) for some Δ_{0}-formula φ, then there exists a b ∈ Ad_{M}, which is admissible, and such that ∀x ∈ b.∃y ∈ b.φ(x, y). Furthermore, similarly as for KPI^{+}, we demand that there exist finitely many admissibles above Ad_{M}. (Again one could alternatively define KPM^{+} as KPl plus the existence of one recursively Mahlo ordinal.) One can now model the Mahlo universe by iterating an operator up to M, which is the first recursively Mahlo ordinal and the union of ordinals in Ad_{M}. That the universe is closed under the Mahlo operation follows by the fact that we have iterated the operator up to the first recursively Mahlo ordinal. More details about this model can be found in Appendix C.

Lower Bound. The lower bound [Setzer, 2000] was carried out similarly to the lower bound for ML_{1}W by carrying out a well-ordering proof. That proof is rather technical, and to go into details is beyond the scope of this article.

7 Application: Inductive-Recursive Definitions

Induction-recursion. The concept of induction-recursion is due to Dybjer [Dybjer, 2000]. It is an abstract formalisation of the general principles used for introducing new sets in Martin-Löf type theory (excluding the Mahlo principle).

The principle of strictly positive inductive definitions in simple type theory has been studied since long time ago. An algebraic data type A (introduced by constructors C_{i}) is defined strictly positive inductively, if the constructors are of the form C_{i} : B_{1} → ⋯ → B_{n} → A, where B_{i} either do not depend on A, or are of the form D_{1} → ⋯ → D_{k} → A, where D_{i} do not depend on A. Both n and k can be 0. An argument of a constructor of type B_{i} not referring to A is called a non-inductive argument, an argument of type D_{1} → ⋯ → D_{k} → A is called an inductive argument. Examples are the finite sets N_{l} with constructors A_{l}^{i} : N_{l} for i = 0, …, l − 1 (the constructors have no arguments); the set of natural numbers N with constructors 0 : N and S : N → N (the constructor S has one inductive argument where k as above is 0); the set Nlist of lists of natural numbers with constructors nil : Nlist (no arguments) and cons : N → Nlist → Nlist (one non-inductive and one inductive argument).

In dependent type theory, the argument types B_{i} can depend on previous noninductive arguments. So here we have C_{i} : (x_{1} : B_{1}) → (x_{2} : B_{2}) → ⋯ → (x_{n} : B_{n}) → A where B_{i} are either independent of A or of the form (y_{1} : D_{1}) → ⋯ → (y_{k} : D_{k}) → A. Examples are the set Σx : A.B(x) with constructor p : (x : A) → B → Σx : A.B(x) (two non-inductive arguments, the second depends on the first); the set Πx : A.B(x) with constructor λ : ((x : A) → B(x)) → (Πx : A.B(x)) (no inductive argument); the set Wx : A.B(x) with constructor sup : (x : A) → (B(x) → (Wx : A.B(x))) → (Wx : A.B(x)) (the first argument is non-inductive, the second is inductive and depends on the first).

The above can be generalised to indexed inductive definitions, where we define several sets A_{i} simultaneously inductively. This can take the form of finitely many sets, each of which has different constructors. An example for this is the set of finitely branching trees FinTree together with the set of lists of such trees FinTreeList (the example is due to U. Berger): lists of finite trees are introduced in a standard way by having constructors nil : FinTreeList, cons : FinTree → FinTreeList → FinTreeList. Furthermore, if we have a list of trees, we can form a tree, having the elements of the list as subtrees, so we have a constructor maketree : FinTreeList → FinTree. A more general form of indexed inductive definition is, when we introduce simultaneously possibly infinitely many sets A(i) (i : I) indexed over a set I. One degenerate example for this is the equality set I(A, a, b), which can be considered as a set C(⟨a, b⟩) indexed over ⟨a, b⟩ : A × A. It has constructor refl : (a : A) → C(⟨a, a⟩). An example, which is really inductive, is the predicate Even(n) for n : N, meaning “n is even”. It has constructors zeroproof : Even(0) and succproof : (n : N, Even(n)) → Even(S(S(n))). The general form of indexed inductive definition is that we have constructors of type (x_{1} : B_{1}) → ⋯ → (x_{n} : B_{n}) → A(j), and where B_{l} either does not depend on A(i), or is of the form (y_{1} : D_{1}) → ⋯ → (y_{k} : D_{k}) → A(j′), where j′ might depend on y_{1}, …, y_{k}. j might depend on the noninductive arguments x_{i} of type B_{i}, where B_{i} does not depend on A(i).

In inductive definitions, the argument types cannot depend on previous inductive arguments: Before introducing a new set (or sets) inductively, we have to introduce the argument types of the constructors, which cannot refer to the set(s) to be introduced. Inductive-recursive definitions go beyond inductive definition, and will allow an indirect dependency of argument types on previous inductive arguments. An example of a truly inductive-recursive definition is a standard universe. The constructor introducing the code for the Σ-set as an element of the universe has the form Σ̂ : (a : U) → (b : T(a) → U) → U. When looking at a process for constructing the elements of such a universe, we see that, whenever one constructs an element a : U, one has to define immediately T(a). Otherwise one cannot use this element for forming further elements of U. This means that we define elements of U inductively, while defining simultaneously recursively T(a) for every element a : U introduced – therefore the terminology inductive-recursive definition. In the above example for instance, one defines T(Σ̂(a, b)) = Σx : T(a).T(b x).

In inductive-recursive definitions, later arguments can depend on arbitrary previous non-inductive arguments and on the recursively defined function applied to previous inductive arguments. The result of T can depend in the same way on the arguments, as can later arguments depend on previous ones.

A closed formalisation of inductive-recursive definitions. In P. Dybjer’s original formalisation, the dependency of arguments on previous arguments was syntactic, and meant essentially the occurrence of a variable for one argument in the term for a later argument. Therefore, his type theory is a schema, which allows to introduce for each inductive-recursively defined set new rules. However, we can see that, before we can introduce a new inductive-recursive definition, we often need first to carry out a proof using the rules defined before.

We give an example: Assume we want to define inductive-recursively a nonstandard universe U, T (i.e. a universe which is not closed under standard type theoretic constructions). Instead it should contain a code for N and, if a_{0}, a_{1}, a_{2} : U, and T(a_{i}) = A_{i}, then U should contain a code for A_{0} + (A_{1} + A_{2}). For this to be a good definition, we need to know, before adding the rules for such a universe to type theory, that we have that A + (B + C) : Type, provided A, B, C : Type. In this toy example, this is of course obvious, but one can easily construct more complicated examples, which require a long derivation. So in general, before introducing an inductive-recursive definition, one has to derive certain type theoretic judgements. Therefore we see that in P. Dybjer’s original framework one has to work as follows: one starts with basic inductive-recursive definitions. Then one derives type theoretic formulae, using which one can introduce additional inductive-recursive definitions. Then one can introduce further inductive-recursive definitions, and so on.

It is difficult to analyse a framework like this proof theoretically and to construct models of it. Therefore P. Dybjer and myself developed in a series of articles [Dybjer and Setzer, 1999, Dybjer and Setzer, 2001, Dybjer and Setzer, 2003b, Dybjer and Setzer, 2003a] a closed formalisation of inductive-recursive definitions. “Closed” means that we have a fixed set of rules, which we can introduce from the beginning, which don’t depend on previous proofs, and which allow to introduce all inductive-recursive definitions. The formalisation taken makes use of ideas used in the definition of the Mahlo universe. In fact, the resulting theory reaches the strength of a slightly weakened version of Mahlo type theory.

We will in the following only consider the non-indexed case. We will make use of the logical framework. We used as logical framework operations the dependent function-type with η-rule (written as (x : A) → B – we reserve the notation Πx : A.B(x) for the definition of a set having essentially the same rules, but no η-rule) the dependent product with η-rule (written as (x : A) × B – again, Σx : A.B(x) is reserved for a corresponding set, which has no η-rule), and the types having zero, one and two elements, written as 0, 1, 2. The canonical element of 1 is ∗ and the canonical elements of 2 are ∗_{0} and ∗_{1}. We add the η-rule for 1, which expresses that for x : 1, x = ∗ : 1 We have as well case distinction case_{2} : 2 → A → A → A for any type A, with the equalities case_{2}(∗_{0}, a, b) = a, case_{2}(∗_{1}, a, b) = b. Furthermore, we have Set : Type, containing inductive-recursively defined sets. All sets are types. Both Set and Type are closed under the operations of the logical framework.^{1}

In the following, we will uncurry the arguments of the constructors, so we have C_{i} : ((x_{1} : B_{1}) × ⋯ × (x_{n} : B_{n})) → A instead of C_{i} : (x_{1} : B_{1}) → ⋯ → (x_{n} : B_{n}) → A. We can code several constructors into one by having one additional argument, which is an element of a finite set and indicates, which constructor was chosen. Depending on this argument, the types for the other arguments of the constructors are taken. Therefore, our inductive-recursively defined sets will have only one constructor.

Rules for inductive-recursive definitions. In the new type theory, we will replace the notion of dependency of a type B on x : A, as it occurred in P. Dybjer’s original schema by a judgement Γ, x : A, Δ ⇒ B : Type. In order to able to derive that something is an inductive recursive definition, we need a corresponding judgement, and therefore we will introduce a type OP_{D} of codes for inductiverecursive definitions, depending on a type D (the meaning of D will be explained later on). To derive an inductive recursive definition means to derive an element γ : OP_{D}. For every inductive recursive definition γ : OP_{D} we introduce the inductive recursively defined set U_{γ} introduced by it together with its decoding function T_{γ}, having typing rule a : U_{γ} ⇒ T_{γ}(a) : D. This explains now the meaning of the parameter D in OP_{D}: D is the codomain of the recursively defined functions T_{γ} for γ : OP_{D}. For instance, if we take D = Set, then (U_{γ}, T_{γ}) will be a universe, but not necessarily closed under type theoretic operations. If we take D = 1, then we have T_{γ}(a) = ∗, so T_{γ} doesn’t carry any information – this is nothing but an ordinary inductive definition (as opposed to an inductive-recursive definition). If we take D = ((X : Set) × (X → Set)) → ((X : Set) × (X → Set)), U_{γ} will be a universe of operations, where an operation maps families of sets to families of sets. In general D can be any type. In the following, D will be kept fixed, and we assume globally D : Type. When fully spelled out, all rules will have an additional premise D : Type.

1In our original articles besides Set an additional type stype was used. Set contained only sets introduced inductive-recursively, whereas stype contained all elements of Set, but not Set itself, and was closed under the operation of the logical framework. This distinction is not really necessary, and we omit it in this article.

Note that OP_{D} is therefore some kind of big universe, having two decoding functions, namely λγ.U_{γ} : OP_{D} → Set and λγ.λx.T_{γ}(x) : (γ : OP_{D}) → (U_{γ} → Set). OP_{D} itself cannot be defined inductive-recursively.

The argument type of the constructor is given by 𝔽_{γ}^{U}, having the formation rule

\frac{γ : OP_{D}  U : Set  T : U → Set}{𝔽_{γ}^{U}(U, T) : Set}

The result of T_{γ} applied to a constructor element, is given by 𝔽_{γ}^{T}, having the formation rule

\frac{γ : OP_{D}  U : Set  T : U → Set  a : 𝔽_{γ}^{U}(U, T)}{𝔽_{γ}^{T}(U, T, a) : D}

So when introducing γ : OP_{D} we have to define 𝔽_{γ}^{U} and 𝔽_{γ}^{T}.

Once this is defined we have the following formation and equality rules for inductive-recursively defined sets:

U_{γ} : Set T_{γ} : U_{γ} → D

The introduction rules for U_{γ} and equality rules for T_{γ} are

intro_{γ} : 𝔽_{γ}^{U}(U_{γ}, T_{γ}) → U_{γ} T_{γ}(intro_{γ}(a)) = 𝔽_{γ}^{T}(U_{γ}, T_{γ}, a)

We have the following rules for generating elements of OP_{D}:

• Addition of a non-inductive argument: Assume A : Set and γ : A → OP_{D}. Then we can form a new code σ(A, γ) : OP_{D} for the inductive-recursive definition, having a first non-inductive argument a : A, and depending on it, the other arguments taken from γ(a). So we have

𝔽_{σ(A,γ)}^{U}(U, T) = (a : A) × 𝔽_{γ(a)}^{U}(U, T)

The result of T_{γ} for an element intro_{γ}(a) is the result obtained for the remaining arguments with respect to γ(a). Therefore we have:

𝔽_{σ(A,γ)}^{T}(U, T, ⟨a, b⟩) = 𝔽_{γ(a)}^{T}(U, T, b)

• Addition of an inductive argument: Assume A : Set and γ : (A → D) → OP_{D}. Then we can form a new code δ(A, γ) for the inductive-recursive definition, having a first inductive argument indexed over A, i.e. f : A → U_{γ}. The further arguments depend on T_{γ} applied to the elements of U_{γ}, to which f is referring, i.e. on T_{γ} ∘ f, and are therefore taken from γ(T_{γ} ∘ f). So we have

𝔽 _{δ(A,γ)}^{U}(U, T) = (f : A → U) × 𝔽 _{γ(T ∘f)}^{U}(U, T)

The result of T_{γ} for an element intro_{γ}(a) is the result obtained for the remaining arguments with respect to γ(T_{γ} ∘ f). Therefore we have:

𝔽 _{δ(A,γ)}^{T}(U, T, ⟨f, b⟩) = 𝔽 _{γ(T ∘f)}^{T}(U, T, b)

• Base case: This corresponds to the inductive-recursive definition with no arguments. We only have to determine the result of T, which is an element of type D. Assuming ψ : D, we have therefore ι(ψ) : OP_{D} and the rules

𝔽 _{ι(ψ)}^{U}(U, T) = 1 ,
𝔽 _{ι(ψ)}^{T}(U, T, ∗) = ψ .

Elimination and equality rules. In order to define the elimination and equality rules, one has to define first for every γ : OP_{D} two more types:

\frac{γ : OP_{D}  U : Set  T : U → D u : 𝔽 _{γ}^{U}(U, T)  x : U ⇒ E[x] : Type}{𝔽 _{γ}^{IH}(U, T, E, u) : Type}

\frac{γ : OP_{D}  U : Set  T : U → Set x : U ⇒ E[x] : Type  h : (x : U) → E[x]}{𝔽 _{γ}^{map}(U, T, E, h) : (u : 𝔽 _{γ}^{U}(U, T)) → 𝔽 _{γ}^{IH}(U, T, E, u)}

Then the elimination rule for U_{γ} is as follows:

\frac{x : U_{γ} ⇒ E[x] : Type g : (u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ}), 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u)) → E[intro_{γ}(u)]}{R_{γ,E}(g) : (u : U_{γ}) → E[u]}

The equality rule is as follows:

\frac{x : U_{γ} ⇒ E[x] : Type g : (u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ}), 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u)) → E[intro_{γ}(u)] u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ})}{R_{γ,E}(g, intro_{γ}(u)) = g(u, 𝔽 _{γ}^{map}(U_{γ}, T_{γ}, E, R_{γ,E}(g), u)) : E[intro_{γ}(u)]}

We won’t give the equality rules for 𝔽_{γ}^{IH} and 𝔽_{γ}^{map} here, the straighforward and boring details can be found in [Dybjer and Setzer, 2003b].

Examples. The first examples will be inductive definitions, so in this case D := 1. Let ι_{∗} := ι(∗) : OP_{1}. The finite sets are defined by

γ_{N_{0}} := σ(0, λx.ι_{∗}) : OP_{1} .
γ_{N_{1}} := ι_{∗} : OP_{1} ,
γ_{N_{n+2}} := σ(2, λx.case_{2}(x, γ_{N_{n+1}}, ι_{∗})) : OP_{1} .

A + B and Σx : A.B(x) have codes

γ_{A+B} := σ(2, λx.case_{2}(x, σ(A, λy.ι_{∗}), σ(B, λy.ι_{∗}))) ,
γ_{Σx:A.B(x)} := σ(A, λx.σ(B(x), λy.ι_{∗})) .

N has code

γ_{N} := σ(2, λx.case_{2}(x, ι_{∗}, δ(1, λy.ι_{∗}))) .

Zero is here intro_{γ_{N}}(⟨∗_{0}, ∗⟩), and the successor of n is intro_{γ_{N}}(⟨∗_{1}, ⟨n, ∗⟩⟩). Wx : A.B(x) has code

γ_{Wx:A.B(x)} := σ(A, λx.δ(B(x), λy.ι_{∗})) .

Finally, the first universe (consisting of U_{0} : Set and T_{0} : U_{0} → Set and for simplicity closed under N and Σ only) has code

γ_{U_{0},T_{0}} := σ(2, λx.case_{2}(x, ι(N), δ(1, λA.δ(A(∗), λB.ι(Σx : A(∗), B x))) : OP_{Set} .

Application in generic programming. The theory developed has a data type for inductive-recursive definitions. If one considers this type theory as a functional programming language, it is possible to write programs, which have a higher degree of polymorphism, and take as input a data type (an element of OP_{D}), analyse it and generate a new data type (a new element of OP_{D}). Such kind of programming is called generic programming. Examples for its use are: a function, which takes an inductive recursive definition and adds one constructor to it, together with an embedding of the original one into the new one; and the definition of a defined equality relation on a data type. This is an area of ongoing research; see [Dybjer and Setzer, 1998, Benke et al., 2003, 3] for details.

Inductive-recursive definitions and the Mahlo universe. The constructor δ of OP_{D} has type δ : (A : Set, γ : (A → D) → OP_{D}) → OP_{D} and refers therefore negatively to D. Note that D can be Set, and that from elements of OP_{D} we introduce new elements of Set. Therefore elements of Set can be introduced by referring negatively to Set.

In fact, Set is essentially a weak variant of the Mahlo universe (the strength of a type theory with a weak Mahlo universe is only slightly below that of the type theory with a full Mahlo universe): Assume f_{0} : (A : Set, B : A → Set) → Set and f_{1} : (A : Set, B : A → Set, f_{0}(A, B)) → Set. Let

γ_{0}(f⃗) := δ(1, λA′.δ(A′(∗), λB′.ι(f_{0}(A′(∗), B′)))) : OP_{Set} ,
γ_{1}(f⃗) := δ(1, λA′.δ(A′(∗), λB′.σ(f_{0}(A′(∗), B′), λC.ι(f_{1}(A′(∗), B′, C))))) : OP_{Set} ,
γ(f⃗) := σ(2, λx.case_{2}(x, γ_{0}(f⃗), γ_{1}(f⃗))

Then U_{γ(f⃗)} will be, similar to Uf⃗ in case of the Mahlo universe, a universe closed under f_{0}, f_{1}. Here intro_{γ(f⃗)}(⟨∗_{0}, ⋯⟩) and intro_{γ(f⃗)}(⟨∗_{1}, ⋯⟩) will play the rôle of Res_{0}, Res_{1}, respectively, in the Mahlo universe. In this form, the universe U_{γ(f⃗)} will

be empty, but one can easily expand γ(f⃗) and guarantee that U_{γ(f⃗)} is closed under the standard universe constructions as well. Therefore, for every pair of functions f⃗ from families of elements of Set into families of elements of Set there exists a universe in Set closed under f⃗. Note that, in the presence of the logical framework, it is possible to have f⃗ as elements of the context.

In appendix D we will show, using this observation, that the theory of inductiverecursive definitions reaches the strength of KPM, Kripke-Platek set theory with Mahloness of the universe.

Model. In [Dybjer and Setzer, 1999], a model of the theory of inductive-recursive definitions was developed in set theory plus the existence of one strongly Mahlo cardinal. There we interpreted Set as V_{M}, where (V_{α})_{α∈Ord} is the commulative hierarchy of sets and M is one strongly Mahlo cardinal. The usual set constructions were interpreted by their naïve interpretation, e.g. [[ A → B]] was interpreted as the set theoretic function space [[ A]] → [[ B]]. OP_{D} was interpreted as an appropriate inductive definition. We defined approximations of U_{γ}^{α}, T_{γ}^{α} of the interpretation of U_{γ}, T_{γ}, and interpreted U_{γ} as U_{γ}^{M}, T_{γ} as T_{γ}^{M}. The definition of U_{γ}^{α} was based on the interpretation of λU, T.⟨𝔽_{γ}^{U}(U, T), 𝔽_{γ}^{T}(U, T)⟩. For every α < M there exists a β < M s.t. if U ∈ V_{α}, T ∈ U → [[ D]], then [[ 𝔽_{γ}^{U}(U, T) ]]_{U↦U,T ↦T} ∈ V_{β}. By the Mahlo property one obtained a κ < M recursively inaccessible, s.t. if α < κ, then the β as above is < κ. Using the recursive inaccessibility of κ it followed then that U_{γ}^{κ} = U_{γ}^{M} and therefore [[ U_{γ} ]] ∈ [[ Set ]].

Upper Bound. We introduced the above mentioned model, because it is rather natural. Using this model one obtains an upper bound, which is far too big, namely that of ZF plus the existence of one strongly Mahlo cardinal. We have not yet spelled out a model, which uses only the strength of KPM^{+}. In order to define such a model, one would have to interpret Set as the iteration of an operator up to the first recursively Mahlo ordinal M in a similar way as the interpretation of the Mahlo universe. The interpretation of OP_{D} would require in such a model finitely many admissibles above the recursively Mahlo ordinal. We do not expect any major difficulties in carrying this out in detail.

Precise strength. Assuming the model in KPM^{+} has been developed, we obtain an interval for the strength of the theory, namely [|KPM|, |KPM^{+}|]. We do not know yet currently, what the exact strength is. This depends on, whether the types OP_{D} actually contribute to the strength of the theory of inductive-recursive definitions.

Appendix A: Direct Well-Foundedness Proof of the Ordinal Notation System of Strength ϵ_{0}

We sketch here a direct well-ordering proof for the ordinal notation system of strength ϵ_{0}, developed in Sect. 2. This argument doesn’t refer to ordinals, and can be formalised, restricted to ordinals < ϵ_{0}, in Peano Arithmetic.

The argument proceeds as follows: First one shows that, if (A, <_{A}), (B, <_{B}) are well-founded linear orderings, so are (A × B, <_{A×B}) and (A_{dec}, <_{lex}). Here <_{A×B} is the lexicographic ordering on pairs ⟨a, b⟩, where a ∈ A and b ∈ B, A_{dec} is the set of w.r.t. < descending sequences of A (i.e. the set of sequences ⟨a_{0}, …, a_{n−1}⟩ s.t. a_{0} > ⋯ > a_{n−1}), and <_{lex} is the lexicographic ordering on these sequences (we suppress the dependencies of A_{dec} on <). Define for orderings (X, <) on ℕ the operation Γ(X, <) := ((X × ℕ)_{dec}, (<_{X×ℕ})_{lex}) as defined before. Then (OT_{ϵ_{0}}, <_{ϵ_{0}} ) = (⋃_{n∈ω} A_{n}, ⋃_{n∈ω} <_{n}) with (A_{n}, <_{n}) := Γ^{n}((∅, ∅)). Observe that (A_{n}, <_{n})

is the set of ordinal notations < \underbrace{ω^{ω^{·^{·^{·^{1}}}}}}_{n times}. (∅, ∅) is trivially well-founded, therefore

each (A_{n}, <_{n}) are well-founded. Furthermore, one can easily see that (A_{n}, <_{n}) ⊑ (A_{n+1}, <_{n+1}) where ⊑ means “initial segment” defined as (A, <) ⊑ (B, <′) :⇔ A ⊆ B∧ <′↾ A × A =< ∧∀a ∈ A.∀b ∈ B.b <′ a → b ∈ A. It is easy to see that if (B_{n}, <_{n}) are well-founded and transitive, (B_{n}, <_{n}) ⊑ (B_{n+1}, <_{n+1}) for all n, then (⋃_{n∈ω} B_{n}, ⋃_{n∈ω} <_{n}) is well-founded. Therefore it follows that (OT_{ϵ_{0}}, <_{ϵ_{0}}) is well-founded.

From the above argument one can develop in Peano Arithmetic a proof of the principle of transfinite induction for formulae of PA over (A_{n}, <_{n}) for Meta-each n, and therefore for OT_{ϵ_{0}} restricted to any ordinal b < ϵ_{0}.

Appendix B: Determination of the Strength of Type Theory with one Universe and the W-Type

Upper bound for the proof theoretic strength of ML_{1}W. We will in the following construct a model of ML_{1}W with extensional equality in a theory of the same strength, namely KPI^{+}, and use therefore KPI^{+} as Meta-theory.

We form a simple PER (= partial equivalence relation) model: every type expression A in dependent type theory is modelled as a set [[ A]]_{ρ} of pairs of terms, namely those terms which are considered to be equal, and, if ML_{1}W proves A : Type, then [[ A]]_{ρ} will be a partial equivalence relation, i.e. transitive and symmetric. In the model, we identify terms with their Gödel-numbers. ρ is an environment, i.e. a finite map from variables to closed terms, s.t. all free variables of A are in the domain of ρ. Let for sets of pairs of terms A, B A → B := {⟨s, s′⟩ | ∀⟨r, r′⟩ ∈ A.⟨s(r), s′(r′)⟩ ∈ B}. We form the model for the restriction of type theory, where the W-rank of type expressions is ≤ n for some n ∈ ℕ. Here the W-rank of A is 0, if A does not contain U. Otherwise, the rank of U is 1, the rank of Wx : A.B(x) is the maximum of the W-rank of A, B(x) incremented by 1, and the rank of all other type expression is the maximum of the W-rank of its immediate subterms which are subtypes (e.g. the W-rank of Πx : A.B(x) is the maximum of the W-rank of A and B(x)).

We introduce some notations: x_{1} ↦ r_{1}, …, x_{n} ↦ r_{n} denotes the environment, mapping x_{i} to r_{i}. If ρ is an environment, ρ(x ↦ r) is the environment, mapping x to ρ and y ≠ x to ρ(y), provided y is in the domain of ρ. We write [x_{1} := r_{1}, …, x_{n} := r_{n}] for the simultaneous substitution of x_{i} by r_{i}. If Γ = x_{1} : A_{1}, …, x_{n} : A_{n}, we write ∀⟨r⃗, r′⟩ ∈ [[ Γ ]] for ∀⟨r_{1}, r′_{1}⟩ ∈ [[ A_{1} ]], ∀⟨r_{2}, r′_{2}⟩ ∈ [[ A_{2} ]]_{x_{1}↦r_{1}}, …, ∀⟨r_{n}, r′_{n}⟩ ∈ [[ A_{n}]]_{x_{1}↦r_{1},...,x_{n−1}↦r_{n−1}}. Furthermore, we write x⃗ ↦ r⃗ for the environment x_{1} ↦ r_{1}, …, x_{n} ↦ r_{n} and [x⃗ := r⃗] for [x_{1} := r_{1}, …, x_{n} := r_{n}], assuming that the choice of x_{i}, r_{i} is obvious from the context.

We first state what it means for a derived judgement to be correct in this model. We define the set of immediate presuppositions (ips) of a judgement as follows:

• ∅ ⇒ Context has no ips.

• The ips of Γ, x : A ⇒ Context is Γ ⇒ A : Type.

• The ips of Γ ⇒ A : Type is Γ ⇒ Context.

• The ips of Γ ⇒ A = B are Γ ⇒ A : Type and Γ ⇒ B : Type.

• The ips of Γ ⇒ s : A is Γ ⇒ A : Type.

• The ips of Γ ⇒ r = s : A are Γ ⇒ r : A and Γ ⇒ s : A.

Then one defines the presuppositions of a judgement as follows:

• The ips of a judgement are presuppositions of it.

• The ips of a presupposition of a judgement are as well presuppositions of that judgement.

The correctness condition for Γ ⇒ θ is defined as the conjunction of the immediate correctness conditions (icc) of all its presuppositions and of the judgement itself, where the icc of a judgement Γ ⇒ θ is defined as follows:

• If θ = Context, then the icc is the true formula.

• If θ is A = B : Type, then the icc is ∀⟨r⃗, r′⟩ ∈ [[ Γ ]].[[ A]]_{x⃗↦r⃗} = [[ B]]_{x⃗↦r′} ∧ Equiv([[ A]]_{x⃗↦r⃗}), where Equiv(X) means that A is a partial equivalence relation on terms.

• If θ = A : Type, then the icc is the same as that of Γ ⇒ A = A : Type.

• If θ is r = s : A, the icc is ∀⟨r⃗, r′⟩ ∈ [[ Γ ]].⟨r[x⃗ := r⃗], s[x⃗ := r′]⟩ ∈ [[ A]]_{x⃗↦r⃗}.

• If θ is r : A, the icc is the same as that of Γ ⇒ r = r : A.

Standard types are modelled in a straightforward way, e.g.

\begin{matrix}[[ Πx : A.B]]_{ρ} := \{⟨r, r′⟩ | & ∀⟨s, s′⟩ ∈ [[ A]]_{ρ}([[ B]]_{ρ[x↦s]} = [[ B]]_{ρ[x↦s′]} \\ ∧⟨r(s), r′(s′)⟩ ∈ [[ B]]_{ρ[x↦s]})\} \end{matrix}

Interpretation of the W-type. The W-type corresponds in Kripke-Platek set theory to the step to the next admissible. In order to interpret this type, we will introduce for every type A, when defining [[ A]]_{ρ}, additionally an α ∈ Ord s.t. [[ A]]_{ρ} ∈ L_{α} for any environment ρ. This will be done in such a way that α < κ_{n}(= ℵ_{I^{δ}+n}^{rec}), if the W-rank of A is n. The definition of α is straightforward, except in case of Wx : A.B(x):

Assume [[ A]]_{ρ′} and [[ B]]_{ρ′} have already been defined for environments ρ′. Then we define [[ Wx : A.B(x) ]]_{ρ} as follows: First, we define for environments ρ an operator Γ_{ρ} on sets of pairs of terms by

Γ_{ρ}(X) := Cl({⟨sup(r, s), sup(r′, s′)⟩ |

⟨r, r′⟩ ∈ [[ A]]_{ρ} ∧ [[ B]]_{ρ(x↦r)} = [[ B]]_{ρ(x↦r′)} ∧ ⟨s, s′⟩ ∈ [[ B]]_{ρ(x↦r)} → X})

Here Cl(X) is the closure of X under reductions, i.e.

Cl(X) := {⟨r, r′⟩ | ∃⟨s, s′⟩ ∈ X.(r ⟶ s ∧ r′ ⟶ s′)}

If α is s.t. for all ρ [[ A]]_{ρ}, [[ B]]_{ρ} ∈ L_{α} and α^{+} is the least admissible above α, we can define the least fixed point of Γ_{ρ} as the iteration Γ_{ρ}^{α^{+}} of Γ_{ρ} α^{+}-times (starting with the empty set and taking at limit points the union), and therefore define

[[ Wx : A.B(x) ]]_{ρ} := Γ_{ρ}^{α^{+}} .

It is easy to see that if ⟨r, r′⟩ ∈ [[ A]]_{ρ}, and ⟨s, s′⟩ ∈ [[ B]]_{ρ(x↦r)} → [[ Wx : A.B(x) ]]_{ρ}, then ⟨sup(r, s), sup(r′, s′)⟩ ∈ [[ Wx : A.B(x) ]]_{ρ}: We have [[ B]]_{ρ(x↦r)} ∈ L_{α^{+}}, and for

all t, t′ s.t. ⟨t, t′⟩ ∈ [[ B]]_{ρ(x↦r)} it follows ⟨s(t), s′(t′)⟩ ∈ Γ_{ρ}^{α^{+}}, therefore there exists by the admissibility of κ a γ < α^{+} s.t. for all such t, t′ we have ⟨s(t), s′(t′)⟩ ∈ Γ_{ρ}^{γ}, and therefore ⟨sup(r, s), sup(r′, s′)⟩ ∈ Γ_{ρ}^{γ+1} ⊆ Γ_{ρ}^{α^{+}}.

It is easy to show that [[ Wx : A.B(x) ]]_{ρ} is a partial equivalence relation. In order to show that the correctness condition w.r.t. the induction rule is fulfilled, one shows first, assuming the correctness of the premises of the induction rule, by induction over γ the correctness of the conclusion for elements of Γ_{ρ}^{γ} instead of [[ Wx : A.B(x) ]]_{ρ}. Then the correctness of the conclusion without this replacement follows.

Interpretation of the universe. In order to interpret the universe, we define simultaneously a set of pairs of terms U^{α}, and for r, r′ s.t. ⟨r, r′⟩ ∈ U^{α} a set of pairs of terms T^{α}(r), s.t. U^{α} and T^{α}(r) are partial equivalence relations, U^{α} ⊆ U^{β} and T^{β}(r) = T^{α}(r) for α < β and r s.t. ⟨r, r⟩ ∈ U^{α}, and s.t. U^{α} and T^{α}(r) are in L_{ℵ_{α+2}^{rec}}. Then we interpret [[ U ]]_{ρ} := U^{I} and [[ T(r) ]]_{ρ} := T^{I}(r_{ρ}) (which is empty for ⟨r_{ρ}, r_{ρ}⟩ ∉ U^{I}), where I is the first recursively inaccessible ordinal, and r_{ρ} is the result of substituting in r free variables according to ρ.

The inductive definition is straightforward. E.g. if ⟨r, r′⟩ ∈ U^{<α} (where U^{<α} = ⋃_{β<α} U^{β}) and for ⟨t, t′⟩ ∈ T^{<α}(r), ⟨s[x := t], s′[x′ := t′]⟩ ∈ U^{<α}, then ⟨Ŵx : r.s, Ŵx′ : r′.s′⟩ ∈ U^{α} and T^{α}(Ŵx : r.s) = [[ Wx : T(r).T(s) ]]′, where [[ Wx : T(r).T(s) ]]′ is defined as above, but interpreting [[ T(r) ]] as T^{<α}(r), similarly for [[ T(s) ]]_{x↦t}. Furthermore, U is closed under reductions.

We have to show U^{α}, T^{α}(r) ∈ ℵ_{α+2}^{rec}. The crucial part of the proof is when we add Ŵx : a.b to U^{α}. By IH T^{<α}(r) and T^{<α}(s[x := t]) are in L_{β} for β := sup_{α′<α} ℵ_{α′+2}^{rec}. We have β ≤ κ := ℵ_{α+1}^{rec} < ℵ_{α+2}^{rec} and κ is admissible. By the admissibility of κ and L_{κ} = ⋃_{γ<κ} L_{γ}, there exists a γ < κ s.t. T^{<α}(r) ∈ L_{γ}, and for ⟨t, t⟩ ∈ T^{<α}(r), T^{<α}(s[x := t]) ∈ L_{γ}. Therefore the fixed point of the operator defining [[ Wx : T(r).T(s) ]] can be obtained by iterating the operator up to κ, and therefore [[ Wx : T(r).T(s) ]] ∈ L_{ℵ_{α+2}^{rec}}.

We show now that U^{<I} is closed under the introduction rules for the universe. In case of the W-type, this is done as follows: Assume ⟨r, r′⟩ ∈ U^{<I} and for ⟨t, t′⟩ ∈ T^{<I}(r), ⟨s[x := t], s′[x′ := t′]⟩ ∈ U^{<I}. Then T^{<I}(r) ∈ L_{I}, and therefore there exists an α < I s.t. for all t, t′ as above ⟨s[x := t], s′[x′ := t′]⟩ ∈ U^{α}. Here we used that I is an admissible closed under λα.ℵ_{α}^{rec}. Now it follows that ⟨Ŵx : r.s, Ŵx′ : r′.s′⟩ ∈ U^{α+1}.

Completion of the proof of the upper bound. Now one shows that every arithmetic statement provable in ML_{1}W can be shown in KPI^{+}. Let ψ be any arithmetic formula. We extend the set of terms by additional terms C_{φ,x⃗} for all subformulae φ of ψ and variables x⃗ = x_{1}, …, x_{k} containing the free variables of φ, together with reduction rules for C_{φ,x⃗}. This will be done in such a way that in the model we have provable in KPI^{+} ∀n_{1}, …, n_{k} ∈ ω.⟨C_{φ,x⃗}(n_{1}, …, n_{k}), C_{φ,x⃗}(n_{1}, …, n_{k})⟩ ∈ [[ φ]]_{x⃗↦n⃗} ⇔ [[ φ]]_{x⃗↦n⃗} ≠ ∅ ⇔ φ[x_{1} := n_{1}, …, x_{k} := n_{k}]. Especially, if ML_{1}W proves φ, then for all n⃗ [[ φ]]_{x⃗↦n⃗} is inhabited and therefore φ[x⃗ := n⃗] holds in KPI^{+}. If φ ≡ r = s then C_{φ,x⃗}(n⃗) ⟶ refl, if r[x⃗ := n⃗] = s[x⃗ := n⃗] is true, otherwise the term does not reduce. Here refl is the canonical element of the identity type r =_{N} s between r and s. If φ ≡ φ_{0} ∧ φ_{1}, C_{φ,x⃗}(n⃗) ⟶ ⟨C_{φ_{0},x⃗}(n⃗), C_{φ_{1},x⃗}(n⃗)⟩, if φ ≡ φ_{0} ∨ φ_{1} then C_{φ,x⃗}(n⃗) ⟶ inl(C_{φ_{0},x⃗}(n⃗)) if φ_{0}[x⃗ := n⃗] holds, and C_{φ,x⃗}(n⃗) ⟶ inr(C_{φ_{1},x⃗}(n⃗)) otherwise. If φ ≡ φ_{0} → φ_{1} then C_{φ,x⃗}(n⃗) ⟶ λx.C_{φ_{1},x⃗}(n⃗). if φ ≡ ∀x.ψ, C_{φ,x⃗}(n⃗) ⟶ λy.C_{ψ,x⃗,x}(n⃗, y), and if φ ≡ ∃x.ψ, then C_{φ,x⃗}(n⃗) ⟶ ⟨n, C_{ψ,x⃗,x}(n⃗, n)⟩, if n is minimal s.t. ψ[x⃗ := n⃗, x := n] holds; if there is no such n, there is no reduction for C_{φ,x⃗}(n⃗).

It follows that, if an arithmetic sentence ψ is provable in ML_{1}W, then by forming the above model w.r.t. ψ it follows that ψ holds in KPI^{+}. Therefore the limit of transfinite induction provable for all arithmetic formulae in ML_{1}W is less than or equal that for KPI^{+}, therefore |ML_{1}W| ≤ |KPI^{+}|.

Ordinal notation system. Whereas for the upper bound one is relying on the proof theoretic analysis of KPI^{+}, the lower bound will be carried out explicitly, and we need first to set up an ordinal notation system of appropriate strength.

The ordinal notation system will have as basic constants 0 and I, where I is the first strongly inaccessible cardinal.^{2} One takes as basic functions addition of ordinals, the Veblen function φ (where φ0β = ω^{β} and for α > 0 φαβ is the βth common fixed point of λβ′.φα′β′ for α′ < α) and λα.Ω_{α} (where Ω_{0} = 0 and Ω_{α} = ℵ_{α}^{rec} otherwise). Furthermore, one adds the collapsing function ψ. Here one defines simultaneously for κ ∈ R (where R is the set of regular cardinals) by recursion on α

2One could replace all cardinals in the following by their recursive analogues (admissibles), but setting up an ordinal notation system like this is much more complicated. What eventually matters is only the resulting ordinal notation system, which is primitive recursive and w.r.t. which we prove upper and lower bounds for the proof theoretic strength of corresponding theories. The set theoretic development can be considered as mere heuristic. It is a however a very valuable heuristic, since it has contributed to a much better understanding of the ordinal notation systems

ψ_{κ}α := min{β | κ ∈ C(α, β) ∧ C(α, β) ∩ κ ⊆ β} ,
C(α, β) := Closure of β under 0, I, +, φ, λα.Ω_{α}, λπ ∈ R.λξ < α.ψ_{π}ξ .

It is outside the scope of this article to give a detailed explanation of the ψ-function, here we give only a few remarks. If κ = Ω_{β+1}, then ψ_{κ}α is the least ordinal ≥ Ω_{α}, s.t., if we form the closure under basic constants, basic functions and all collapsing functions we have defined before, i.e. with arguments < α, we do not get any new ordinals < κ. In case of κ = I, I is automatically contained in the closure and we need only that the same closure as before does not contain any new ordinals < I. Let Γ_{α} the αth fixed point of λα.φα0, i.e. the αth ordinal, which cannot be defined from smaller ones using 0, + and the Veblen function. Let β be the first fixed point of λα.Γ_{α}. For α < β, ψ_{Ω_{1}}α = Γ_{α}, and β = ψ_{Ω_{1}}(Ω_{1}). Let I_{α} be the αth (not necessary regular) fixed point of λα.Ω_{α} and γ be the first (non-regular) fixed point of λα.I_{α}. For α < γ, ψ_{I}(α) = I_{α} and ψ_{I}(I) = γ.

If one adapts the analysis of KPI in [Buchholz, 1992] to an analysis of KPI^{+}, one can see that |KPI^{+}| = ψ_{Ω_{1}}(Ω_{I+ω}).

Lower bound for the strength of ML_{1}W. The lower bound is obtained by proving directly in ML_{1}W transfinite induction up to ψ_{Ω_{1}}(Ω_{I+n}) for (Meta-)every n < ω. Then it follows |ML_{1}W| ≥ sup_{n∈ω} ψ_{Ω_{1}}(Ω_{I+n}) = ψ_{Ω_{1}}Ω_{I+ω} = |KPI^{+}|. We will use the technique of distinguished sets, which is due to Buchholz. Before introducing it, we start with some basic definitions.

An expression C[x] is a type expression possibly depending on a free variable x, and we write C[t] for C[x := t] (possibly applying some α-conversion to C first in order to avoid clashes of bound and free variables). A subset B of a set A is a function B : A → U, and a subclass is an expression B[x] s.t. x : A ⇒ B[x] : Type. In case of subsets we write x ∈ B for T(B(x)) and in case of subclasses x ∈ B for B[x]. ∀x ∈ B.C[x] := ∀x : A.x ∈ B → C[x], similarly for ∃x ∈ B.C[x]. The following definitions can be carried out both for sets and for classes, although we we will explicitly only define them for sets. If B, C are subsets of A, then B ⊆ C :⇔ ∀x ∈ B.x ∈ C, B ≅ C :⇔ B ⊆ C ∧ C ⊆ B. A partially ordered set (class) (A, <) is a type A together with a binary relation < on A, i.e. a type expression x < y s.t. x : A, y : A ⇒ x < y : Type. For partially ordered sets A and a, b ∈ A, a ≤ b :⇔ a = b ∨ a < b. For a ∈ A, B, C ⊆ A, a ≤ B :⇔ ∃b ∈ B.a ≤ b, C ≤ B :⇔ ∀c ∈ C.c ≤ B. For partially ordered sets (A, <) we identify a ∈ A with {b ∈ A | b < a} and write a + 1 for {b ∈ A | b ≤ a}; this explains for instance notions like A ∩ (a + 1). If B, C ⊆ A, B ⊑ C (“B is an initial segment of C”) iff ∀b ∈ B.B ∩ (b + 1) ≅ C ∩ (b + 1). If (A, <) is a partially ordered set (i.e. < is a binary relation on a set A), we can form the accessible part Acc(A) as the largest well-founded segment of A.

Let (OT, <) be the ordinal notation system constructed from the above mentioned functions. We define for A ⊆ OT the set C^{a}(A) as the closure of A ∩ a under 0, I, +, φ, λγ.Ω_{γ} and λκ > a.λγ.ψ_{κ}γ. Let M(A) := {α | α ∈ C^{α}(A)}. So the elements of M(A) are those, which can be formed from A ∩ α from basic functions and collapsing functions ψ_{κ} with κ > α.

developed.

Distinguished sets. In order to get an idea of what a distinguished set is, we will give first some examples of distinguished sets, as they were introduced originally. Later we will slightly change this definition.

The first one A_{0} is the accessible part of the ordinals below Ω_{1}. The next one, A_{1} is the union of A_{0} with the accessible part of the ordinals α ∈ [Ω_{1}, Ω_{2}[ s.t. their components below Ω_{1} are in A_{0}, i.e. s.t. α ∈ C^{Ω_{1}}(A_{0}). The next one, A_{2} is the union of A_{1} with the accessible part of the ordinals α ∈ [Ω_{2}, Ω_{3}[ having components below Ω_{2} in A_{1}, i.e. s.t. α ∈ C^{Ω_{2}}(A_{1}). This series can be iterated transfinitely in an obvious way. Sets A introduced in this way can be characterised as having the following property: for all α s.t. Ω_{α} ≤ A we have that A ∩ [Ω_{α}, Ω_{α+1}[ is the accessible part of C^{Ω_{α}}(A)∩[Ω_{α}, Ω_{α+1}[. This was essentially the original definition of a distinguished set. In order to avoid the jumps at Ω_{α}, we introduce the following variations of this definition: first one replaces β ∈ C^{Ω_{α}}(A) by β ∈ C^{β}(A), i.e. β ∈ M(A) – this has only a minor effect on the definition. Furthermore, one consideres the definition of the accessible part: This is an inductive definition of the form: “if β ∈ M(A) ∩ [Ω_{α}, Ω_{α+1}[ and β ∩ M(A) ∩ [Ω_{α}, β[ is a subset of the accessible part, then β is in the accessible part”. This definition, in which one examines A in slices of the form [Ω_{α}, Ω_{α+1}[ , will now replaced by the following inductive definition of an unsliced set W(A): W(A) is the least set Y s.t., if α ∈ C^{α}(A) and C^{α}(A) ∩ α ⊆ Y, then α ∈ Y. Our final definition of distinquished is now as follows:

A is distinguished ⇔ A ⊑ W(A)

Assuming that A ∩ Ω_{α} ≅ W(A) ∩ Ω_{α} (therefore A ∩ Ω_{α} is distinguished) and A ∩ Ω_{α+1} ≅ M(A) ∩ Ω_{α+1} (i.e. A ∩ Ω_{α+1} is sufficiently closed), it follows that W(A) ∩ [Ω_{α}, Ω_{α+1}[ is the accessible part of the set [Ω_{α}, Ω_{α+1}[∩M(A), therefore the new definition is essentially the same as the original definition of distinguished sets. We will below show how to introduce W(A) and therefore as well the notion of “A is distinguished” in ML_{1}W.

Distinguished sets are well-ordered (since, if A is distinguished, α, β ∈ A, α < β, then α ∈ C^{β}(A) ∩ β). Now one can show using transfinite induction over distinguished sets that distinguished sets are essentially approximations of the same class: If A, B are distinguished sets, α ∈ A and α ≤ B, then A ∩ (α + 1) ≅ B ∩ (α + 1). In type theory, we take now P(N) := N → U as the notion of the powerset of N and form the union of all distinguished sets. This union will be a class W. W is a distinguished class, i.e. if we define W for classes, we obtain W ⊑ W(W).

If one forms by Meta-induction on n the classes W_{0} := (W ∩ I) ∪ {I}, W_{n+1} := (W(W_{n}) ∩ Ω_{I+n+1}) ∪ {Ω_{I+n+1}}, one obtains as well distinguished classes. It can be shown, using induction over distinguished sets, that distinguished sets and classes A are closed under 0, I, +, the step to the next cardinal, the Veblen function, the collapsing functions and λα.Ω_{α} bounded by A, i.e. if the result of applying of these operations is ≤ A, then it is in A. It follows that Ω_{1}, Ω_{I+n} ∈ W_{n}, therefore ψ_{Ω_{1}}(Ω_{I+n}) ∈ W_{n} ∩ Ω_{1}. Furthermore, W_{n} ∩ Ω_{1} is an initial segment of OT which is well-ordered, and therefore we obtain transfinite induction up to ψ_{Ω_{1}}(Ω_{I+n}), provable in ML_{1}W.

Definition of W(A). First we define C^{a}(A) in type theory. We have that b ∈ C^{a}(A), if b ∈ A ∩ a or b can be formed by one of the operations from other elements of C^{a}(A), where the latter terms are smaller. When we unfold this, we get a finite formula of the shape b ∈ C^{a}(A) ⇔ b ∈ A∩a∨((c_{0} ∈ A∩a∨⋯)∧(c_{1} ∈ A∩a∨⋯)). This formula can be transformed into disjunctive normal form with atomic formulae of the form c ∈ A ∩ a and therefore one can define for b ∈ OT a finite set K_{a}(b) of finite sets of elements of OT s.t. b ∈ C^{a}(A) ⇔ ∃C ∈ K_{a}(b).C ⊆ A ∩ a. K_{a}(b) can be introduced in type theory directly by induction over OT. This way we obtain a formalisation of C^{a}(A) in type theory.

W(A) itself can be defined using the W-type as follows: First a system of rules for deriving statements of the form a ∈ W(A) for a : N can be given by having for each a ∈ C^{a}(A) one rule

\begin{aligned}⋯ & a′ ∈ W(A) & ⋯ (a′ ∈ C^{a}(A) ∩ a) \\ & a ∈ W(A) \end{aligned}

In type theory we can represent such derivations as elements of Wb : B.C(b), where B := Σa : N.a ∈ C^{a}(A) and C(⟨a, p⟩) := Σa′ : N.a′ ∈ C^{a}(A) ∩ a. An element w := sup(⟨a, p⟩, q) derives a ∈ W(A) from subderivations q(c) (c : C(⟨a, p⟩)), provided at each subtree of w (including w) the labels of the trees are respected: Define label : (Wb : B.C(b)) → N, label(sup(⟨a, p⟩, q)) = a. Then the local correctness needed at each subtree w′ is: If w′ = sup(⟨a′, p′⟩, q′), then the ⟨a′′, q′′⟩th subtree of w′ has label a′′, i.e. label(q′(⟨a′′, q′′⟩)) =_{N} a′′. This local property for subtree w′ will be called LocCor(w′). In order to define the notion of a subtree, we first define the notion w ≺_{Tree}^{1} w′, “w is an immediate subtree of w′” recursively as w ≺_{Tree}^{1} sup(b, p) := ∃c : C(b).w =_{Wb:B.C(b)} p(c). Here a =_{D} b denotes the intensional equality type for a, b : D. Now we define w ⪯_{Tree} w′, “w is a subtree of w′ or equal to w′”, as “there exists a sequence of trees (w_{0}, …, w_{n}) s.t. n ≥ 0, w_{0} =_{Wb:B.C(b)} w′, w_{n} =_{Wb:B.C(b)} w and for k = 0, …, n − 1 w_{k+1} ≺_{Tree}^{1} w_{k}. We define Cor(w) := ∀w′ : (Wb : B.C(b)).w′ ⪯_{Tree} w → LocCor(w′) and

a ∈ W(A) :⇔ ∃w : (Wb : B.C(b)).Cor(w) ∧ label(w) =_{A} a .

It is an easy exercise to verify that a ∈ C^{a}(A) → (∀a′ ∈ C^{a}(A) ∩ a.a′ ∈ W(A)) → a ∈ W(A) holds and that we obtain the least such set. The latter can be expressed by the following induction principle (assuming a : N ⇒ D(a) : Type): (∀a ∈ W(A).(∀a′ ∈ C^{a}(A) ∩ a.D(a′)) → D(a)) → ∀a ∈ W(A).D(a). This completes the well-ordering proof.

Appendix C: A Model for Type Theory with W-Type and one Mahlo Universe

We will in the following give the details of the model of MLM in KPM^{+}. The main construction is as for KPI^{+}, the only difference is of course how to interpret the Mahlo universe itself. This is done as follows:

Similarly as when interpreting the universe of ML_{1}W, one defines simultaneously sets of pairs of terms V^{α} together with a set of pairs of terms T^{α}(r) for r s.t. ⟨r, r⟩ ∈ V_{α}, with similar conditions as before. We identify in the following the names of the constructors for sets in V and in Uf⃗, i.e. we identify Ñ with N̂, Σ̃ with Σ̂ etc.

The inductive definition is for standard universe constructors as for an ordinary universe. Assume now terms f⃗, g⃗, and an α is s.t. V^{α} is closed under the standard universe constructions, and s.t. if a ∈ V^{α}, b ∈ T^{α}(a) → V^{α}, then ⟨f_{0}(a, b), g_{0}(a, b)⟩ ∈ V^{α} and for c : T^{α}(f_{0}(a, b)), ⟨f_{1}(a, b, c), g_{1}(a, b, c)⟩ ∈ V^{α}. Then ⟨Ûf⃗, Ûg⃗⟩ ∈ V^{α+1} and T(Ûf⃗) = V^{β} for the minimal β ≤ α, s.t. the above conditions hold with α replaced by β.

Now let M := ⋃{α | α ∈ Ad_{M}} be the recursively Mahlo ordinal corresponding to Ad_{M} and introduce a model with [[ V ]] := V^{M}. Since M is recursively inaccessible, it follows as before that V^{M} is closed under the usual universe constructions. We verify now that V^{M} is closed under the introduction rule for Û. For simplicity, we work as if the interpretation of sets were a set of terms rather than a set of pairs of terms considered to be equal, and we assume that we do not have any context. Assume f_{0} ∈ [[ (a : V, b : T(a) → V) → V ]] and f_{1} ∈ [[ (a : V, b : T(a) → V, T(f′_{0}(a, b))) → V ]]_{f′_{0}↦f_{0}}. This means that for a ∈ V^{M}, b ∈ T^{M}(a) → V^{M}, f_{0}(a, b) ∈ V^{M} and for c ∈ T^{M}(f_{0}(a, b)), f_{1}(a, b, c) ∈ V^{M}. Assume now α < M. For every a ∈ V^{α} and b ∈ T^{α}(a) → V^{α} there exists a β < M s.t. f_{0}(a, b) ∈ V^{β}. For every c ∈ T^{β}(f_{0}(a, b)) there exists a γ < M s.t. f_{1}(a, b, c) ∈ V^{γ}. Using admissibility of M it follows that there exists a β < M s.t. f_{0}(a, b) ∈ V^{β} and for c ∈ T^{β}(a, b), f_{1}(a, b, c) ∈ V^{β}. Let φ(α, β) := ∀a ∈ V^{α}.∀b ∈ T^{α}(a) → V^{α}.f_{0}(a, b) ∈ V^{β} ∧ ∀c ∈ T^{α}(f_{0}(a, b)).f_{1}(a, b, c) ∈ V^{β}. Then ∀α < M.∃β < M.φ(α, β), where φ(α, β) is Δ_{0}. Furthermore, we have ∀α < M.∃β < M.β = ℵ_{α}^{rec} which is as well a Δ_{0}-formula. By the Mahlo axiom there exists a κ < M, which is admissible, s.t. ∀α < κ.∃β < κ.β = ℵ_{α}^{rec}, i.e. s.t. κ is recursively inaccessible, and s.t. ∀α < κ.∃β < κ.φ(α, β). Since we have demanded T^{α}(a) ∈ L_{ℵ_{α}^{rec}} it follows T^{κ}(a) ∈ L_{κ} for a ∈ V^{κ}. Using admissibility of κ it follows from the above that if a ∈ V^{κ}, b ∈ T^{κ}(a) → V^{κ} then f_{0}(a, b) ∈ V^{κ} and for c ∈ T^{κ}(f_{0}(a, b)), f_{1}(a, b, c) ∈ V^{κ}, and therefore Ûf⃗ ∈ V^{κ+1} ⊆ V^{M}.

Appendix D: Proof that Inductive-Recursive Definitions Reach the Strength of KPM

We show here how to adapt the well-ordering proof for the Mahlo universe in order to show that the theory of inductive-recursive definitions reaches the strength of KPM, Kripke-Platek set theory plus recursive Mahloness of the set-theoretic universe. We make use of the fact that Set is a weak variant of the Mahlo universe, as described in Sect. 7. In the well-ordering proof for type theory with one Mahlo universe, similarly as in that for ML_{1}W, one introduces the union of distinguished sets W, where sets were elements of N → V and V is the Mahlo universe. Then one introduces finitely many distinguished classes on top of W, which corresponds to the step to finitely many admissibles above the recursively Mahlo ordinal. The formation of those sets makes use of the W-type, formed using sets depending on V. In the theory of inductive-recursive definitions, we can from W as union of all distinguished sets as elements of N → Set, but we cannot form the nth admissible set above W. We cannot express that W is distinguished, however W will inherit the closure properties of distinguished sets. One can show transfinite induction over W′ := (W ∩M)∪{M}. Using induction into types one can then show transfinite induction up to the ntimes nested Cantor Normal Form over elements in

W′, which is essentially transfinite induction up to \underbrace{ω^{·^{·^{·^{ω^{M+1}}}}}}_{n times} This allows then show

that α_{n} := ψ_{Ω_{1}}(\underbrace{ω^{·^{·^{·^{ω^{M+1}}}}}}_{n times}) is in W, and, since W ∩ (α_{n} + 1) is a segment of OT,

transfinite induction up to α_{n}. Since ψ_{Ω_{1}}(ϵ_{M+1}) = sup_{n∈ω} α_{n}, it follows that the strength of the type theory of inductive-recursive definitions is at least ψ_{Ω_{1}}(ϵ_{M+1}), which is the proof theoretic ordinal of KPM. The strength of KPM is only slightly below that of KPM^{+}, the strength of type theory with one Mahlo universe.

References

AUGUSTSSON, L., “Cayenne - a language with dependent types”. In “International Conference on Functional Programming”, 1998, p. 239–250.

BARWISE, J., “Admissible Sets and Structures. An Approach to Definability Theory”, Omega-series, Springer, 1975.

BENKE, M., “Towards generic programming in type theory”. Presentation at Annual ESPRIT BRA TYPES Meeting, Berg en Dal, submitted for publication, 2002. Available via http://www.cs.chalmers.se/

~marcin/Papers/Notes/nijmegen.ps.gz.

BENKE, M., DYBJER, P., and JANSSON, P., “Universes for generic programs and proofs in dependent type theory”, submitted, 2003.

BUCHHOLZ, W., “Notation systems for infinitary derivations”, Arch. Math. Logic 30, 1991, p. 277 – 296.

BUCHHOLZ, W., “A simplified version of local predicativity”. In Aczel, P., Simmons, H., and Wainer, S. S., editors, “Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990”, Cambridge University Press, 1992, p. 115 – 147.

DYBJER, P., “A general formulation of simultaneous inductive-recursive definitions in type theory”, J.Sym.Log. 65(2), 2000, p. 525 – 549.

DYBJER, P. and SETZER, A., “Finite axiomatizations of inductive and inductiverecursive definitions”. In “Workshop on Generic Programming, Marstrand, Sweden, 18 June 1998”, http://www.cs.ruu.nl/people/johanj/programme wgp98.html, 1998.

DYBJER, P. and SETZER, A., “A finite axiomatization of inductive-recursive definitions”. In Girard, J.-Y., editor, “Typed Lambda Calculi and Applications”, volume 1581 of Springer Lecture Notes in Computer Science, p. 129–146, 1999.

DYBJER, P. and SETZER, A., “Indexed induction-recursion”. In Kahle, R., Schroeder-Heister, P., and Stärk, R., editors, “Proof Theory in Computer Science”, LNCS 2183, 2001, p. 93 – 113.

DYBJER, P. and SETZER, A. (2003a), “Indexed induction-recursion”, long version, submitted, 2003.

DYBJER, P. and SETZER, A. (2003b), “Induction-recursion and initial algebras”, Annals of Pure and Applied Logic 124, 2003, p. 1 – 47.

GENTZEN, G., “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Mathematische Annalen 112, 1936, p. 493 – 565.

GÖDEL, K., “Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik 38, 1931, p. 173 – 198.

GOODSTEIN, R. L., “Recursive Number Theory”, North-Holland, 1964.

GRIFFOR, E. and RATHJEN, M., “The strength of some Martin-Löf type theories”, Arch. math. Log. 33, 1994, p. 347 – 385.

HEIJENOORT, J. v., “From Frege to Gödel”, Harward University Press, 1967.

HILBERT, D., “Mathematische probleme”, Gött. Nachr., 1900, p. 253–297.

HILBERT, D. and BERNAYS, P., “Grundlagen der Mathematik. Zweiter Band”, Julius Springer, Berlin, 1939.

HINMAN, P. G., “Recursion-Theoretic Hierarchies”, Springer, 1978.

JÄGER, G., “Theories for Admissible Sets: A Unifying Approach to Proof Theory”, Bibliopolis, Naples, 1986.

KRIPKE, S., “Transfinite recursion on admissible ordinals, I, II (abstracts)”, J. Symbolic Logic 29, 1964, p. 161 – 162.

MICHELBRINK, M., “Zur endlichen Behandlung der Beweistheorie schwacher Fragmente der Mengenlehre: KP + Π_{3}-Reflexion”, PhD thesis, Fachbereich Mathematik und Informatik, Hannover, 2000.

MINTS, G. and TUPAILO, S., “Epsilon-substitution method for the ramified language and Δ_{1}^{1}-comprehension rule”. In Cantini, A., editor, “Logic and foundations of mathematics. Proceedings of the congress of logic, methodology and philosophy of science, Florence, 1995”, Synthese Library 280, Kluwer, 1999, p. 107 – 130.

MINTS, G., TUPAILO, S., and BUCHHOLZ, W., “Epsilon substitution method for elementary analysis”, Arch. Math. Logic 35(2), 1996, p. 103 – 130.

PALMGREN, E., “On universes in type theory”, In Sambin, G. and Smith, J., editors, “Twenty five years of constructive type theory”, Oxford University Press, 1998, p. 191 – 204.

PLATEK, R., “Foundations of recursion theory”, Doctorial Dissertation and Supplement, Stanford, CA: Stanford University, 1966.

RATHJEN, M., “Proof-theoretical analysis of KPM”, Arch. math. Logic 30, 1991, p. 377 – 403.

SCHLÜTER, A., “On provability in set theories with reflection,” preprint.

SETZER, A., “Proof theoretical strength of Martin-Löf Type Theory with Wtype and one universe”, PhD thesis, Universität München, 1993. Available via http://www.cs.swan.ac.uk/∼csetzer.

SETZER, A., “A type theory for iterated inductive definitions”, draft, 14 pp., 1994. Available via http://www.cs.swan.ac.uk/∼csetzer.

SETZER, A., “A model for a type theory with one Mahlo Universe,” preprint, 10pp, 1996. Available via http://www.cs.swan.ac.uk/∼setzer/articles/uppermahlo.pdf.

SETZER, A., “Well-ordering proofs for Martin-Löf type theory”, Annals of Pure and Applied Logic 92, 1998, p. 113 – 159.

SETZER, A., “Extending Martin-Löf type theory by one Mahlo-universe”, Arch. Math. Log. 39, 2000, p. 155 – 181.

SKOLEM, T., “Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich”, Videnskapsselskapets skripfter, I. Matematisknaturvidenskabelig klasse 6, 1923. See as well [Heijenoort, 1967], p. 302 – 333.

TAIT, W., “Normal derivability in classical logic”. In Barwise, J., editor, “The syntax and semantics of infinitary languages”, Springer Lecture Notes in Mathematics 72, 1968, p. 204 – 236.