A Finite Axiomatization of Inductive-Recursive Definitions

Peter Dybjer^{∗}and Anton Setzer^{†}

May 16, 2005

Abstract

Induction-recursion is a schema which formalizes the principles for introducing new sets in Martin-Löf’s type theory. It states that we may inductively define a set while simultaneously defining a function from this set into an arbitrary type by structural recursion. This extends the notion of an inductively defined set substantially and allows us to introduce universes and higher order universes (but not a Mahlo universe). In this article we give a finite axiomatization of inductive-recursive definitions. We prove consistency by constructing a set-theoretic model which makes use of one Mahlo cardinal.

1 Introduction

In this article we present an elegant, uniform method for introducing large sets in type theory. We draw on experience from proof theory, category theory, and set theory to formulate a compact, completely formal theory of inductive-recursive definitions, and to prove its consistency.

Induction-recursion is a schema for introducing new sets in type theory developed by Dybjer [7]. All the usual sets in Martin-Löf’s type theory and practically all sets (data types), which are defined in analogy with it, are instances of this schema. Applications of induction-recursion include not only a variety of type-theoretic analogues of large cardinals (inaccessible cardinals, hyper-inaccessible cardinals, etc) but also various powerful notions needed for the type-theoretic formalization of metamathematics (such as reducibility predicates and logical relations for dependent types). Induction-recursion can also provide novel ways to formalize simple concepts such as the set of lists with distinct elements [7].

The original presentation of induction-recursion was as an external schema [7]. In this article we internalize this concept. The new theory has a special type of codes for inductive-recursive definitions. New sets defined by induction-recursion are introduced by deriving codes in this type. Therefore we achieve full precision of the concept of an inductive-recursive definition. The meta-theory becomes easier, as will be demonstrated by building a full function space model.

Ordinary dependent type theory with generalized inductive definitions (that is, Martin-Löf’s type theory without universes) has a natural full function space interpretation in classical set theory [1, 8]. As shown by our construction of a set-theoretic model the step from inductive to inductive-recursive definitions in type theory is roughly analogous to moving from ordinary ZF set theory to ZF set theory with a Mahlo cardinal. The proof-theoretic strength of type theory increases accordingly when inductive-recursive definitions are added. The consistency of the theory is shown without assuming the positivity restriction on parameters needed for Dybjer’s original realizability model of inductive-recursive definitions [7].

∗Department of Mathematics and Computing Science, Chalmers University of Technology.

Email: peterd@cs.chalmers.se

†Department of Mathematics, Uppsala University. Email: setzer@math.uu.se

The new theory explains that induction-recursion can be viewed as a very general reflection principle: given finitely many (possibly infinitary) operations on a type D, we can construct by simultaneous induction-recursion a universe U with decoding function T : U → D, which reflects each of the D-operations. This reflection principle can be expressed formally by a diagram which extends the initial algebra diagram used for categorical semantics of inductively defined sets. The resulting theory has been implemented in the Half system, a proof assistant for Martin-Löf’s type theory developed by Coquand and Synek, see Cederquist [4].

Plan of the paper. In Section 2 we present Martin-Löf’s Logical Framework. In Section 3 we recall how to use initial algebras for giving categorical semantics of inductive types in the simply typed lambda calculus. In Section 4 we discuss the step from induction to induction-recursion and how we need to modify the notion of an endofunctor Φ and of an initial Φ-algebra in order to capture the formal rules for induction-recursion. We then show how to give a finite axiomatization of inductiverecursive definitions by introducing a type of codes for such modified endofunctors. In Section 5 we show how to recover some well-known set constructors by giving appropriate codes. In Section 6 we build a set-theoretic model. In Section 7 we mention some related work.

2 An Extension of the Logical Framework

The Logical Framework (see [15]) has the following forms of judgements: Γ context, and A : type, A = B : type, a : A, a = b : A, depending on contexts Γ (written as Γ ⇒ A : type, etc.). We have set : type and if A : set, then A : type. The collection of types is closed under the formation of dependent function types written as (x : A) → B, with elements formed by abstraction (x : A)a, application written in the form a(b) and which has the η-rule. Types are also closed under the formation of dependent products written as (x : A) × B, with elements ⟨a, b⟩, projections π_{0} and π_{1} and again the η-rule (surjective pairing). There is also the type 1, with unique element ⟨⟩ : 1 and η-rule expressing, that if a : 1, then a = ⟨⟩ : 1.

We will add a level between set and type, which we call stype for small types: stype : type. (The reason for the need for stype is discussed in [7].) If a : set then a : stype. Moreover, stype is also closed under dependent function types, dependent products and includes the one-element type. However, set itself will not be in stype.

Finally, in order to make it possible to code all constructors into one (see the remark on page 4), we add the set 𝔹 of booleans with elements tt for true and ff for false and as elimination rule case distinction if a then b else c : D for a : 𝔹, D : type and b, c : D.

We also use some abbreviations, such as omitting the type in an abstraction, that is, writing (x)a instead of (x : A)a, and writing repeated application as a(b_{1}, …, b_{n}) instead of a(b_{1}) ⋯ (b_{n}) and repeated abstraction as (x_{1} : A_{1}, …, x_{n} : A_{n})a instead of (x_{1} : A_{1}) ⋯ (x_{n} : A_{n})a.

3 Inductive Types as Initial Algebras

Let us first consider the question of how to formalize inductive types in the setting of the simply typed λ-calculus. We shall consider generalized inductive definitions of types given by a finite number of constructors

intro_{i} : Φ_{i}(U) → U ,

where Φ_{i} are strictly positive in the following restricted sense:

• The constant functor Φ(D) = 1 is strictly positive. This is the base case corresponding to an introduction rule with no premises.

• If Ψ is strictly positive and A is an stype, then Φ(D) = A × Ψ(D) is strictly positive. This corresponds to the addition of a non-inductive^{1} premise.

• If Ψ is strictly positive and A is an stype, then Φ(D) = (A → D) × Ψ(D) is strictly positive. This corresponds to the addition of an inductive premise, where A corresponds to the hypotheses of this premise in a generalized inductive definition (and when A = 1 we have the special case of an ordinary inductive definition).

Note that all occurrences of U in Φ(U) are strictly positive in the standard sense that U does not occur to the left of an arrow in Φ(U).

Assume Φ_{1}, …, Φ_{n} are strictly positive functors, and let Φ⃗ := (Φ_{1}, …, Φ_{n}). Then the inductive type generated by Φ⃗ can be captured categorically as an initial Φ⃗-algebra, that is, a sequence of arrows (i = 1, …, n)

Φ_{i}(U) \overline{^{intro_{i}}} U

such that for any other Φ⃗-algebra

Φ_{i}(D) \overline{d_{i}} D

there is a unique arrow T : U ⟶ D, such that the following diagrams commute

Φ_{i}(U) \overline{^{intro_{i}}} U

[figure: Φ_{i}(D); Φ_{i}(T); d_{i}; D; T]

4 Inductive-Recursive Definitions

4.1 From Inductive to Inductive-Recursive Definitions

In the presence of dependent types more inductive definitions become possible. Let us look at some examples:

The set Σ(A, B) has one constructor p : (x : A) → (y : B(x)) → Σ(A, B). It has two non-inductive arguments, where the type B(x) of the second argument depends on the first premise x : A.

The well-ordering set W(A, B) has one constructor sup : (x : A) → (y : B(x) → W(A, B)) → W(A, B). It has a first non-inductive argument x and a second B(x)- indexed inductive argument y. So the second argument depends on the first noninductive argument.

Both are examples of inductive definitions (no simultaneously defined function participates in the definition yet). For this case later premises can only depend on earlier non-inductive premises, but not on earlier inductive premises. We cannot make use of inductive premises, because they only give information about the set we are currently defining.

To capture inductive definitions of sets in the presence of dependent types [8, 9], we thus only need to change the notion of a strictly positive functor Φ above by replacing the non-inductive case by:

1In [7] the terminology “non-recursive premise” was used, but “non-inductive premise” seems better in connection with induction-recursion, since it primarily has to do with the inductively defined set and not with the recursively defined function. Similarly we will use “inductive premise”

instead of “recursive premise”.

• If A is an stype, and Ψ_{x} is a strictly positive functor depending on x : A, then Φ(D) = (x : A) × Ψ_{x}(D) is strictly positive.

We shall now replace the sequence of functors (Φ_{1}, …, Φ_{n}) by a single functor by defining Φ(D) := (x : N_{n}) × Φ_{x}(D). In order to make this possible we need the existence of finite sets with n elements N_{n}. An easy observation shows that 𝔹 and the empty set N_{0} suffice. (It will however be possible to define N_{0}, see section 5).

In the case of inductive-recursive definitions however, a later premise may also depend on an earlier inductive premise. We consider the key example, the ordinary first universe U à la Tarski [12], which is defined inductively, while simultaneously defining the decoding function T : U → set recursively. Consider one of its constructors, Σ̂ : (x : U) → (y : T(x) → U) → U with the defining equality T(Σ̂(a, b)) = Σ(T(a), T ∘ b) : set. Here we have two inductive premises: x : U (implicitly indexed by the one-element type 1) and y : U indexed by T(x). The second argument depends on the first inductive argument via T.

Is U inductively generated by a strictly positive functor Φ as was the case for inductively defined sets? If this is the case, Φ must depend on the recursively defined function T as well: we need something like Φ : (U : set) → (T : U → set) → set defined by Φ(U, T) = (x : U) × (T (x) → U)!

In general, induction-recursion allows that a simultaneously defined function T : U → D for an arbitrary fixed type D may participate in the inductive generation of the set U.

• The modified non-inductive case thus becomes: if A is an stype, and Ψ_{x} is a strictly positive functor depending on x : A, then Φ(U, T) = (x : A)×Ψ_{x}(U, T) is strictly positive.

• The modified inductive case becomes: if A is an stype, and Ψ_{g} is a strictly positive functor depending on g : A → D, then Φ(U, T) = (f : A → U) × Ψ_{T ∘f}(U, T) is strictly positive.

We see that the Φ which generates U (as defined above), is isomorphic to the following strictly positive functor: Φ(U, T) = (f : 1 → U) × (T (f(⟨⟩)) → U) ^{2}.

Furthermore, T is defined by T(Σ̂(a, b)) = Σ(T(a), T ∘ b), i.e. T(Σ̂(a, b)) = d(T(a), T ∘ b) with d : (A : set) → (A → set) → set and d(A, B) := Σ(A, B).

In general, we need an additional component Φ^{Arg} which specifies the domain of d. (Note that this domain only depends on D and not on U and T!). Finally, we need a third component Φ^{map}(U, T) : Φ^{arg}(U, T) → Φ^{Arg} and then we can draw a diagram

Φ^{arg}(U, T) \overline{intro} U

[figure: Φ^{Arg}; Φ^{map}(U, T); d; D; T]

which summarizes the inductive definition of U and recursive definition of T. Think of D as a type of “semantic” objects and of d : Φ^{Arg} → D as a (possibly infinitary) “semantic” operation with Φ^{Arg} as the domain (or generalized arity) of d. U is a universe of codes for objects in D and T : U → D is the decoding function. The constructor intro is the syntactic reflection of d : Φ^{Arg} → D.^{3}

2As this example shows the term “strictly positive” may no longer be wholly appropriate, since the T -argument now can appear negatively. Allen [2] used the alternative term “half-positive” for this reason. U always appears strictly positively however.

3Recall that the term “universe à la Tarski” was chosen by Martin-Löf [12] because of the similarity between the definition of T (for the ordinary first universe) and Tarski’s definition of truth.

Note the similarity between the above diagram for induction-recursion and the ordinary diagram for an initial algebra of an endofunctor which was displayed in Section 2! The key difference is that here Φ is no longer a functor in the ordinary sense, but consists of three components: Φ^{Arg}, Φ^{arg}, and Φ^{map}. These will be axiomatized below.

4.2 A Finite Axiomatization

We shall now give the formal rules for the inductive-recursive definition of a set U and a function T : U → D. Such a definition is always parameterized with respect to the target type D of T, since a particular inductive-recursive definition generates a universe for a finite number of D-operations.

The main step is to introduce a new type SP_{D}, the objects of which are representatives of strictly positive “functors” Φ as above:

\frac{D : type}{SP_{D} : type}

(There is also a rule, which lets us infer that SP_{D} = SP_{D′} if D = D′, but we will omit all such equality preservation rules.)

SP_{D} has three associated operations corresponding to Φ^{Arg}, Φ^{arg}, and Φ^{map} in the informal exposition above:

\frac{D : type ϕ : SP_{D}}{Arg_{D,ϕ} : type}

\frac{ϕ : SP_{D}  U : set  T : U → D}{arg_{ϕ}(U, T) : stype}

\frac{ϕ : SP_{D}  U : set  T : U → D}{map_{ϕ}(U, T) : (arg_{ϕ}(U, T)) → Arg_{D,ϕ}}

To simplify notation we have suppressed the parameter (the “global” premise) D : type and the argument D for the second and third operation^{4}. It should be emphasized that arg_{ϕ} and map_{ϕ} are only abbreviations of the proper formal expressions arg_{D,ϕ} and map_{D,ϕ}. Similarly, we will suppress the D in some later operations as well.

With this new notation the diagram for the inductive-recursive definition of U and T becomes:

arg_{ϕ}(U_{ϕ,d}, T_{ϕ,d}) \overline{\begin{matrix}intro & ϕ,d \\  \end{matrix}}U_{ϕ,d}

[figure: Arg_{D,ϕ}; map_{ϕ}(U_{ϕ,d}, T_{ϕ,d}); d; D; T_{ϕ,d}]

We have the following introduction rules for SP_{D} (again with D suppressed):

nil : SP_{D}

\frac{A stype ϕ : A → SP_{D}}{nonind(A, ϕ) : SP_{D}}

\frac{A stype ϕ : (A → D) → SP_{D}}{ind(A, ϕ) : SP_{D}}

4In Arg we have not suppressed it, since the equality rules for it will make use of D.

Arg_{D,nil} = 1
Arg_{D,nonind(A,ϕ)} = (x : A) × Arg_{D,ϕ(x)}
Arg_{D,ind(A,ϕ)} = (f : A → D) × Arg_{D,ϕ(f)}
arg_{nil}(U, T) = 1
arg_{nonind(A,ϕ)}(U, T) = (x : A) × (arg_{ϕ(x)}(U, T))
arg_{ind(A,ϕ)}(U, T) = (f : A → U) × (arg_{ϕ(T ∘f)}(U, T))
map_{nil}(U, T, ⟨⟩) = ⟨⟩
map_{nonind(A,ϕ)}(U, T, ⟨a, γ⟩) = ⟨a, map_{ϕ(a)}(U, T, γ)⟩
map_{ind(A,ϕ)}(U, T, ⟨f, γ⟩) = ⟨T ∘ f, map_{ϕ(T ∘f)}(U, T, γ)⟩

We are now ready to give the formal rules for U and T. These rules have the common premises D : type, ϕ : SP_{D} and d : Arg_{D,ϕ} → D which will be omitted.

Formation rules:

U_{ϕ,d} : set
T_{ϕ,d} : U_{ϕ,d} → D

Introduction rule:

\frac{a : arg_{ϕ}(U_{ϕ,d}, T_{ϕ,d})}{intro_{ϕ,d}(a) : U_{ϕ,d}}

Equality rule:

\frac{a : arg_{ϕ}(U_{ϕ,d}, T_{ϕ,d})}{T_{ϕ,d}(intro_{ϕ,d}(a)) = d(map_{ϕ}(U_{ϕ,d}, T_{ϕ,d}, a))}

Moreover, structural recursion on U into a type D′, that is, the analogue of universe elimination, is expressed by the following diagram (we omit the indices ϕ, d of U, T, intro, R, write D′[t] for the substitution of some fixed variable in D′ by t and, when used as an argument, D′ instead of (x)D′[x]; assume in the following x : U_{ϕ,d} ⇒ D′[x] : type as a global premise)

arg_{ϕ}(U, T)  \overline{intro} U

(γ : arg_{ϕ}(U, T)) × IH_{ϕ,U,T,D′}(γ)

⟨id, mapIH_{ϕ,U,T,D′}(R_{D′}(e))⟩

\begin{matrix}⟨intro ∘ π_{0}, e⟩ \\ \end{matrix} (x : U) × D′[x]

\begin{matrix}⟨id, R_{D′}(e)⟩ \\ \end{matrix}

where we have used the operation IH which generates the induction hypothesis and the operation mapIH which generates the recursive call:

\frac{U : set  T : (x : U) → D  x : U ⇒ D′[x] : type  γ : arg_{ϕ}(U, T)}{IH_{ϕ,U,T,D′}(γ) : type}

\frac{U : set  T : (x : U) → D  x : U ⇒ D′[x] : type  R : (x : U) → D′[x]}{mapIH_{ϕ,U,T,D′}(R) : (x : arg_{ϕ}(U, T)) → IH_{ϕ,U,T,D′}(x)}

IH_{nil,U,T,D′}(⟨⟩) = 1
IH_{nonind(A,ϕ),U,T,D′}(⟨a, γ⟩) = IH_{ϕ(a),U,T,D′}(γ)
IH_{ind(A,ϕ),U,T,D′}(⟨f, γ⟩) = ((y : A) → D′[f(y)]) × (IH_{ϕ(T ∘f),U,T,D′}(γ))
mapIH_{nil,U,T,D′}(R, ⟨⟩) = ⟨⟩

mapIH_{nonind(A,ϕ),U,T,D′}(R, ⟨a, γ⟩) = mapIH_{ϕ(a),U,T,D′}(R, γ)
mapIH_{ind(A,ϕ),U,T,D′}(R, ⟨f, γ⟩) = ⟨R ∘ f, mapIH_{ϕ(T ∘f),U,T,D′}(R, γ)⟩

Elimination rule (universe elimination):

\frac{e : (γ : arg_{ϕ}(U_{ϕ,d}, T_{ϕ,d})) → (IH_{ϕ,U_{ϕ,d},T_{ϕ,d},D′}(γ)) → (D′[intro_{ϕ,d}(γ)])}{R_{ϕ,d,D′}(e) : (a : U_{ϕ,d}) → D′[a]}

Equality rule (universe elimination, premises omitted):

R_{ϕ,d,D′}(e, intro_{ϕ,d}(γ)) = e(γ, mapIH_{ϕ,U_{ϕ,d},T_{ϕ,d},D′}(R_{ϕ,d,D′}(e), γ))

5 Examples

We shall show how to find ϕ : SP_{D} for some well-known set constructors. (Compare the informal discussion in Section 4.1.) We will write intro instead of intro_{ϕ,d}. Let in the first examples D := 1 and d := (x : C)⟨⟩ for some suitable type C, since this is how we obtain inductive definitions as degenerate cases of inductive-recursive definitions.

Σ-sets. Let

ϕ_{A,B} := nonind(A, (x)nonind(B(x), (y)nil))

in the context A : set, B : A → set. It follows that Σ(A, B) := U_{ϕ_{A,B},d} : set. This set has the constructor intro : ((x : A) × (B(x) × 1)) → Σ(A, B). If we define p := (A, B, x, y)intro(⟨x, ⟨y, ⟨⟩⟩⟩), then p : (A : set, B : A → set, x : A, y : B(x)) → Σ(A, B) and one can easily derive the ordinary elimination rules as if p were the constructor of Σ. Note that this illustrates that we get dependencies on parameters (in the sense of Dybjer [9, 7]) like A, B for free.

Natural numbers. Let

ϕ := nonind(𝔹, (x) if x then nil else ind(1, (y)nil)) ,
N := U_{ϕ,d} ,
0 := intro(⟨tt, ⟨⟩⟩) : N ,
S := (n)intro(⟨ff, ⟨(y)n, ⟨⟩⟩⟩) : N → N .

Although this definition is like the definition of N by the equation N = 1+(1 → N) × 1, because of the η-rule on 1 this is equivalent to the ordinary definition of N. The usual elimination rules for N can be derived.

The empty set. Let

ϕ := ind(1, (x)nil) ,

and define N_{0} := U_{ϕ,d}. Then we can show the elimination rule for the empty set N_{0}. Note that this corresponds to the definition of N_{0} by having one constructor intro : N_{0} → N_{0}. We can define now N′_{0} := U_{nonind(N_{0},(x)nil),d}, which can be regarded as the empty set with no constructors. However, one might prefer to add the set N_{0} like the set 𝔹 as a basic set.

Well-orderings. Let

ϕ_{A,B} := nonind(A, (x)ind(B(x), (y)nil)) ,

in the context A : set, B : (x : A) → set, and define W(A, B) := U_{ϕ_{A,B},d} : set with the constructor intro : ((x : A) × ((B(x) → W(A, B)) × 1)) → W(A, B). As before we can define the ordinary constructor sup with its elimination rules.

A universe closed under N and Σ. Let D := set,

ϕ := nonind(𝔹, (x) if x then nil else ind(1, (f)ind(f(⟨⟩), (y)nil))) .

Hence Arg_{D,ϕ} = (x : 𝔹) × E(x), with

E(tt) = 1 ,
E(ff) = (x : 1 → set) × (f : x(⟨⟩) → set) × 1 .

Moreover, let d : Arg_{D,ϕ} → set be defined such that

d(⟨tt, ⟨⟩⟩) = N ,
d(⟨ff, ⟨A, ⟨B, ⟨⟩⟩⟩⟩) = Σ(A(⟨⟩), (y)B(y)) ,

using the elimination rules for 𝔹 and product. Define U′ := U_{ϕ,d}, T′ := T_{ϕ,d}, and

N̂ := intro(⟨tt, ⟨⟩⟩) : U′ ,
Σ̂ := (a, b)intro(⟨ff, ⟨(x)a, ⟨b, ⟨⟩⟩⟩⟩) : (a : U′, b : T′(a) → U′) → U′ .

N̂ and Σ̂ are essentially the two constructors of the universe U′, T′ and we have T′(N̂) = N, T′(Σ̂(a, b)) = Σ(T′(a), T′ ∘ b).

Lists with distinct elements. Assume A : set and # : (A × A) → A, where # is an (infix) apartness relation on A. In [7] the set Dlist of lists with elements which are distinct with respect to the relation # is defined inductively together with the recursively defined relation (family of sets) Fresh : Dlist → A → set, where Fresh(l, a) expresses that a is distinct from all elements in l. (If we wish to make the dependence on the parameters A and # explicit, we may write Dlist(A, #) and Fresh(A, #).) Dlist has the constructors^{5}

empty : Dlist ,
cons : (a : A, u : Dlist, Fresh(u, a)) → Dlist ,

and Fresh(l, a) is defined such that

Fresh(empty) = (b)1 ,
Fresh(cons(a, u, p)) = (b)((b#a) ∧ Fresh(u, a)) .

Then Dlist = U_{ϕ_{A,#},d_{A,#}}, Fresh = T_{ϕ_{A,#},d_{A,#}}, where D := A → set,

ϕ_{A,#} := nonind(𝔹, (x) if x then nil
else nonind(A, (a)ind(1, (u)nonind(u(⟨⟩, a), nil)))) ,
d_{A,#}(⟨tt, ⟨⟩⟩) = (b)1 ,
d_{A,#}(⟨ff, ⟨a, ⟨u, ⟨p, ⟨⟩⟩⟩⟩⟩) = (b)((b#a) ∧ u(⟨⟩, a)) .

The above examples show that we can derive all inductive-recursive sets in a form, which is close to the way we would ordinarily like to write them down. We must for example write the arguments in list notation and, if we have a non-indexed inductive argument, write it as an argument depending on the type 1. In an implementation of the calculus one could of course easily avoid this administrative overhead.

6 Set-Theoretic Model

6.1 Interpretation of Expressions

The idea behind the model is simple: interpret all constructions in set theory in the obvious way! In particular, each type is interpreted as a set, equal types are interpreted as equal sets, a : A is interpreted as a ∈ A, and a = b : A is interpreted as a and b are equal elements of A. Moreover, A → B is interpreted as the set of all functions from A to B in the set-theoretic sense, and (x : A) → B as the set-theoretic cartesian product Π_{x∈A}B, etc.

5We have here renamed the constructor nil in [7] to empty.

The inductively defined type SP_{D} of codes for strictly positive operators is interpreted as an inductively defined set in the set-theoretic sense, that is, as a set generated by iterating a monotone operator up to a fixed point. Similarly, the inductive-recursively defined set U and function T : U → D, are also interpreted by iterating a monotone operator up to a fixed point.

In order to ensure that a fixed point indeed can be reached we postulate the existence of one Mahlo cardinal in addition to the ordinary axioms of ZF set theory.^{6} We also need the the axiom of choice to deal with cardinals, and for simplicity we assume the generalized continuum hypothesis.^{7}

Note, that a cardinal κ is inaccessible, iff it is regular and ℵ_{κ} = κ, where ℵ_{α} enumerates the infinite cardinals. An inaccessible cardinal κ is a Mahlo cardinal, iff every normal function f : κ → κ has a regular fixed point. (A normal function f is a (strictly) monotone function, which is continuous at limit ordinals λ, i.e. f(λ) = sup_{α<λ} f(α).) The standard model of our extension of ZF is V_{M^{+}}, where M^{+} is the first inaccessible above M, however all types will be interpreted as elements of V_{Λ}, where Λ is the first (non-regular) fixed point of λα.ℵ_{α} above M.

We will develop the semantics following the approach in [8]. Let λ_{0} := ℵ_{M+1}, λ_{n+1} := ℵ_{λ_{n}}, and Λ := sup_{n∈ω} λ_{n}.

If a, a_{1}, …, a_{n}, c are sets, and b is a function with domain a, let

Π_{x∈a}b(x) := {f | f function ∧ dom(f) = a ∧ ∀x ∈ a.f(x) ∈ b(x)} ,
λx ∈ a.b(x) := {⟨x, b(x)⟩ | x ∈ a} ,
Σ_{x∈a}b(x) := {⟨c, d⟩ | c ∈ a ∧ d ∈ b(c)} ,
a_{0} + ⋯ + a_{n} := Σ_{i∈{0,...,n}}a_{i} (if n ≥ 1) ,
(a → c) := Π_{x∈a}c .

Moreover, (a)_{i} := a_{i}, if a = ⟨a_{0}, …, a_{i}⟩ and undefined otherwise.

Whenever we introduce sets A^{α} indexed by ordinals α, let in the following

A^{<α} := ⋃_{β<α} A^{β} .

We shall use the set V_{Λ} as the set-theoretic universe for our interpretation. All types and objects of types will thus be interpreted as elements of V_{Λ} ^{8}. Terms which depend on free variables will be interpreted relative to an assignment ρ, that is, a function, which maps a finite set of variables to elements of V_{Λ}. In the following ρ (possibly with indices or accents) will always be an assignment. If a ∈ V_{Λ}, then ρ_{x}^{a} is the assignment with dom(ρ_{x}^{a}) := dom(ρ) ∪ {x}, such that

ρ_{x}^{a}(y) := \begin{cases}a & if x = y, \\ ρ(y) & otherwise. \end{cases}

Let terms be the set of expressions which possibly occur as elements of a type or as types: So variables are terms and if a, b, a_{1}, …, a_{n} are terms, x is a variable, and C is an n-ary constructor (including set, stype and constructors like ⟨·, ·⟩, π_{0} but excluding type) of the system, then (x : a) → b, (x : a)b, (x : a) × b and C(a_{1}, …, a_{n}) are terms.

6In Sect. 7 (“Constructive versions of the model”) we will discuss how to replace these strong set theoretic requirements by far weaker ones.

7Without the generalized continuum hypothesis one has to replace Mahlo and inaccessible by strongly Mahlo and strongly inaccessible, respectively, and ℵ_{α} by ℶ_{α}.

8We here use a notion of model which only requires all derivable types to be interpreted as elements of V_{Λ}. Note however that V_{Λ} is not closed under the formation of dependent function types. If we wish to satisfy this requirement we can either reinterpret type as the class of all sets or as V_{I} for some inaccessible cardinal I > M.

For terms t and assignments ρ we will determine, whether its interpretation t_{ρ}^{∗} is defined, and if it is defined, the value of t_{ρ}^{∗}. This will be done in such a way that for every term t and every n ∈ ω there exists an m ∈ ω such that, if rng(ρ) ⊆ V_{λ_{n}}, t_{ρ}^{∗} ∈ V_{λ_{m}}. For closed terms, t_{ρ}^{∗} will not depend on ρ and we therefore omit the subscript ρ. We will use ≃ for partial equality in the usual sense, and also let t_{ρ}^{∗} :≃ s mean that the interpretation of t under assignment ρ is defined to be s, provided s is defined, and is undefined otherwise. We extend this definition further by defining

type^{∗} := V_{Λ} .

The interpretation of terms is given by

x_{ρ}^{∗} :≃ ρ(x) ,  set^{∗} :≃ stype^{∗} :≃ V_{M} ,
((x : A) → B)_{ρ}^{∗} :≃ Π_{y∈A_{ρ}^{∗}}B_{ρ_{x}^{y}}^{∗} , ((x : A)a)_{ρ}^{∗} :≃ λy ∈ A_{ρ}^{∗}.a_{ρ_{x}^{y}}^{∗} ,
(a(b))_{ρ}^{∗} :≃ a_{ρ}^{∗}(b_{ρ}^{∗}) ,  ((x : A) × B)_{ρ}^{∗} :≃ Σ_{y∈A_{ρ}^{∗}}B_{ρ_{x}^{y}}^{∗} ,
⟨a, b⟩_{ρ}^{∗} :≃ ⟨a_{ρ}^{∗}, b_{ρ}^{∗}⟩ ,  (π_{0}(a))_{ρ}^{∗} :≃ (a)_{0} ,
(π_{1}(a))_{ρ}^{∗} :≃ (a)_{1} ,  1^{∗} :≃ 1 ,
⟨⟩^{∗} :≃ 0 ,  𝔹^{∗} :≃ {0, 1} ,
tt^{∗} :≃ 0 ,  ff^{∗} :≃ 1 ,

(if a then b else c)_{ρ}^{∗} :≃ \begin{cases}b_{ρ}^{∗} & if a_{ρ}^{∗} = 0 , \\ c_{ρ}^{∗} & if a_{ρ}^{∗} = 1 , \\ undefined & otherwise . \end{cases}

To interpret terms with constructors SP, nonind, ind, Arg, …, we first define SP^{∗}, nonind^{∗}, ind^{∗}, Arg^{∗}, arg^{∗}, map^{∗}, IH^{∗}, mapIH^{∗}, U^{∗}, T^{∗} and interpret

(SP_{D})_{ρ}^{∗} :≃ SP^{∗}(D_{ρ}^{∗}) ,
(nonind(a, b))_{ρ}^{∗} :≃ nonind^{∗}(a_{ρ}^{∗}, b_{ρ}^{∗}) ,
(Arg_{D,ϕ})_{ρ}^{∗} :≃ Arg^{∗}(D_{ρ}^{∗}, ϕ_{ρ}^{∗}) ,
(map_{D,ϕ}(U, T))_{ρ}^{∗} :≃ λx ∈ arg^{∗}(D_{ρ}^{∗}, ϕ_{ρ}^{∗}, U_{ρ}^{∗}, T_{ρ}^{∗}).map^{∗}(D_{ρ}^{∗}, ϕ_{ρ}^{∗}, U_{ρ}^{∗}, T_{ρ}^{∗}, x) ,

etc.

SP^{∗}(D) is defined for D ∈ type^{∗} as the least set such that

SP^{∗}(D) = 1 + Σ_{a∈set^{∗}}(a → SP^{∗}(D)) + Σ_{a∈set^{∗}}((a → D) → SP^{∗}(D)) ,

which we get by iterating the appropriate operator κ times, if for all a ∈ set^{∗} the cardinality of a and of a → D is less than κ. If D ∈ V_{λ_{n}}, therefore SP^{∗}(D) ∈ V_{λ_{n+1}}.

nil^{∗} :≃ ⟨0, 0⟩, nonind^{∗}(a, b) :≃ ⟨1, ⟨a, b⟩⟩, ind^{∗}(a, b) :≃ ⟨2, ⟨a, b⟩⟩ .

Arg^{∗}(D, ϕ) is defined, if ϕ ∈ SP^{∗}(D), and then defined in accordance with the equations for Arg, that is,

Arg^{∗}(D, nil^{∗}) :≃ 1 ,
Arg^{∗}(D, nonind^{∗}(A, ϕ)) :≃ Σ_{x∈A}Arg^{∗}(D, ϕ(x)) ,
Arg^{∗}(D, ind^{∗}(A, ϕ)) :≃ Σ_{f∈(A→D)}Arg^{∗}(D, ϕ(f)) .

Similarly, we define arg^{∗}(D, ϕ, U, T), map^{∗}(D, ϕ, U, T, a), and for D′ ∈ (U → type^{∗}), IH^{∗}(D, ϕ, U, T, D′, γ), mapIH^{∗}(D, ϕ, U, T, D′, R, a).

U^{∗}(D, ϕ, d) :≃ U^{M}(D, ϕ, d) ,
T^{∗}(D, ϕ, d) :≃ λx ∈ U^{M}(D, ϕ, d).T^{M}(D, ϕ, d, x) ,

where U^{α}(D, ϕ, d) and T^{α}(D, ϕ, d) or shorter U^{α} and T^{α} are simultaneously defined by recursion on α as

U^{α} :≃ arg^{∗}(D, ϕ, U^{<α}, T^{<α}) ,

T^{α}(a) :≃ d(map^{∗}(D, ϕ, U^{<α}, T^{<α}, a)) ,
intro(a)_{ρ}^{∗} :≃ a_{ρ}^{∗} ,
R^{∗}(D, ϕ, d, D′, e, a) :≃ R^{M}(D, ϕ, d, D′, e, a), where
R^{α}(D, ϕ, d, D′, e, a) :≃ e(a, mapIH^{∗}(D, ϕ, U^{∗}(D, ϕ, d), T^{∗}(D, ϕ, d) ,
D′, R^{<α}(D, ϕ, d, D′, e), a)) .

Contexts will be interpreted as sets of assignments:

∅^{∗} :≃ ∅ , (Γ, x : A)^{∗} :≃ {ρ_{x}^{a} | ρ ∈ Γ_{ρ}^{∗} ∧ a ∈ A_{ρ}^{∗}} .

6.2 Soundness of the Rules

Theorem 1 (Soundness theorem)

(a) If ⊢ Γ context, then Γ^{∗} is defined.

(b) If ⊢ Γ ⇒ A : E, where E ≡ type or E is a term, then Γ^{∗} is defined, ∀ρ ∈ Γ^{∗}.A_{ρ}^{∗} ∈ E_{ρ}^{∗}, and if E ≢ type, ∀ρ ∈ Γ^{∗}.E_{ρ}^{∗} ∈ type^{∗}.

(c) If ⊢ Γ ⇒ A = B : E, where E ≡ type or E is a term, then Γ^{∗} is defined, ∀ρ ∈ Γ^{∗}(A_{ρ}^{∗} ∈ E_{ρ}^{∗} ∧ B_{ρ}^{∗} = A_{ρ}^{∗}), and if E ≢ type, ∀ρ ∈ Γ^{∗}.E_{ρ}^{∗} ∈ type^{∗}.

(d) ⊬ a : N_{0}, where N_{0} is the empty set, for any of the possibilities mentioned in Section 5.

The proof of the Soundness theorem is more or less routine, except for the verification that U : set. In order to prove this we will need some lemmata.

First we need to verify that U^{α} is increasing with α and that for α < β T^{α} and T^{β} coincide on U^{α}. In order to prove this we need to verify that arg^{∗}(D, ϕ, U, T) and map^{∗}(D, ϕ, U, T) are monotone in U, T, as expressed by the following lemma:

Lemma 1 Assume D ∈ type^{∗}, ϕ ∈ SP^{∗}(D), U ⊆ U′ ∈ set^{∗}, T′ : U′ → D, T = T′ ↾ U. Then

(a) arg^{∗}(D, ϕ, U, T) ⊆ arg^{∗}(D, ϕ, U′, T′) and

(b) map^{∗}(D, ϕ, U′, T′) ↾ arg^{∗}(D, ϕ, U, T) = map^{∗}(D, ϕ, U, T).

We want to show that there is a κ < M such that U^{<κ} = U^{κ}. This is the case if κ is a limit ordinal such that arg^{∗}(D, ϕ, U, T) is κ-continuous in U and T, that is,

arg^{∗}(D, ϕ, U^{<κ}, T^{<κ}) = ⋃_{α<κ} arg^{∗}(D, ϕ, U^{α}, T^{α}) .  (1)

To obtain this we need that all index sets, which start an inductive argument, have cardinality less than κ. The set Aux(D, ϕ, U, T) ∈ set^{∗}, where D ∈ type^{∗}, ϕ ∈ SP^{∗}(D), U ∈ set^{∗}, T ∈ U → D, collects all possible such index sets. It is defined by induction on ϕ:

Aux(D, nil^{∗}, U, T) := 1 ,
Aux(D, nonind^{∗}(A, ϕ), U, T) := Π_{x∈A}Aux(D, ϕ(x), U, T) ,
Aux(D, ind^{∗}(A, ϕ), U, T) := A + Π_{f∈(A→U)}Aux(D, ϕ(T ∘ f), U, T) .

Lemma 2 Assume D ∈ type^{∗}, ϕ ∈ SP^{∗}(D). Let κ be inaccessible and let for α < κ U^{α} ∈ set^{∗}, T^{α} : U^{α} → D such that for α < β, U^{α} ⊆ U^{β}, T^{α} = T^{β} ↾ U^{α}. Assume also for some α_{0} < κ and for all α_{0} ≤ α < κ

Aux(D, ϕ, U^{α}, T^{α}) ∈ V_{κ} .  (2)

Then arg^{∗}(D, ϕ, U, T) is κ-continuous in U and T, that is, (1) holds.

Proof: “⊇” follows by Lemma 1b.

“⊆” follows by induction on ϕ. We treat only the main case ϕ = ind^{∗}(A, γ). Assume a ∈ arg^{∗}(D, ϕ, U^{<κ}, T^{<κ}), and show a ∈ arg^{∗}(D, ϕ, U^{α}, T^{α}) for some α < κ. We know a = ⟨f, c⟩ for some f : A → U^{<κ}, c ∈ arg^{∗}(D, γ(T^{<κ} ∘ f), U^{<κ}, T^{<κ}). By (2) it follows A ∈ V_{κ}, and by the inaccessibility of κ there exists a β < κ such that f : A → U^{<β}, especially f : A → U^{β}. W.l.o.g. α_{0} ≤ β. For β ≤ α < κ it follows Aux(D, γ(T^{α} ∘ f), U^{α}, T^{α}) ∈ V_{κ} and therefore by induction hypothesis there exists a β′ such that c ∈ arg^{∗}(D, γ(T^{β′} ∘ f), U^{β′}, T^{β′}). With α := max{β, β′} follows the assertion. ⊓ ⊔

Lemma 3 Assume ϕ ∈ SP^{∗}(D), s ∈ Arg^{∗}(D, ϕ) → D. Abbreviate U^{α} := U^{α}(D, ϕ, d), T^{α} := T^{α}(D, ϕ, d) and note that U^{∗}(D, ϕ, d) = U^{M}, T^{∗}(D, ϕ, d) = T^{M}.

(a) T^{α} : U^{α} → D, and if α < M, U^{α} ∈ V_{M}.

(b) If α < β then U^{α} ⊆ U^{β} and T^{β} ↾ U^{α} = T^{α}.

(c) There exists κ < M such that U^{α} = U^{κ} (and therefore T^{α} = T^{κ}) for all α > κ.

(d) U^{M} ∈ V_{M}, arg^{∗}(D, ϕ, U^{M}, T^{M}) ⊆ U^{M}.

Proof:

(a) Easy induction on α.

(b) Induction on α, β, by using Lemma 1(b).

(c) Define f : Ord → Ord by transfinite recursion:

f(β) = min{α | ∀β′ < β(f(β′) < α)∧

∀β′ < M(U^{β′} ⊆ V_{β} → U^{β′+1} ∪ Aux(D, ϕ, U^{β′}, T^{β′}) ⊆ V_{α}}

f : M → M follows immediately by M being inaccessible, since

{U^{β′} | β′ < M ∧ U^{β′} ⊆ V_{β}} ∈ V_{β+1} ⊆ V_{M} .

Let for α < M θ(α) := f^{α}(0). By the regularity of M we have θ : M → M. Since f is increasing, θ is normal. Hence, since M is Mahlo, θ has an inaccessible fixed point κ < M.

Therefore f : κ → κ: Assume α < κ. κ is a limit ordinal, therefore α < θ(β) for some β < κ, f(α) < f(θ(β)) = θ(β + 1) < θ(κ) = κ. By induction on α, using the regularity of κ, for α < κ U^{α} ∈ V_{κ}, Aux(D, ϕ, U^{α}, T^{α}) ∈ V_{κ}, and therefore by Lemma 2

U^{κ} = arg^{∗}(D, ϕ, U^{<κ}, T^{<κ})
= ⋃_{α<κ} arg^{∗}(D, ϕ, U^{α}, T^{α})
= ⋃_{α<κ} U^{α+1} = U^{<κ}.

By induction on α for all α ≥ κ U^{α} = U^{<κ} = U^{κ}.

(d) U^{M} = U^{κ} ∈ V_{M}, arg^{∗}(D, ϕ, U^{M}, T^{M}) = arg^{∗}(D, ϕ, U^{κ}, T^{κ}) ⊆ U^{κ+1} ⊆ U^{M}. ⊓ ⊔

7 Related and Future Work

Universes in type theory. The first example of an inductive-recursive definition in type theory was Martin-Löf’s universe à la Tarski [12]. ^{9} Then Palmgren [17] defined external and internal universe hierarchies and also a super universe. Rathjen, Griffor, and Palmgren [19] defined quantifier universes and Palmgren [16] defined higher order universe hierarchies. All these constructions use induction-recursion, whereas Setzer [20] defined a Mahlo universe, which goes beyond it.

9There are earlier examples of informal inductive-recursive definitions, for example, Martin-Löf’s simultaneous definition of the notions of computable type and term [13] from 1972. However, the explicitly inductive-recursive nature of type-theoretic universes was only brought out when they were formulated à la Tarski rather than à la Russell.

Inductive definitions in type theory. Previous work on formalization of inductive definitions in Martin-Löf’s type theory has mainly used external schemata in the style of Martin-Löf’s intuitionistic theory of iterated inductive definitions in predicate logic [11]. See for example Backhouse [3], Dybjer [9], and Paulin [18]. A schema for inductive-recursive definitions was introduced by Dybjer [7].

Categorical semantics of inductive types and of universes. The categorical semantics of inductively defined dependent types has been discussed for example by Coquand and Paulin [5] and Mendler [14]. The latter article also discusses categorical semantics of universes in type theory. In a future article we plan to extend Mendler’s work, by giving categorical semantics of inductive-recursive definitions in terms of initial algebras on endofunctors in slice categories. We will also show how such semantics suggest an alternative finite axiomatization of inductive-recursive definitions.

Set-theoretic semantics of type theory. It is well-known that Martin-Löf’s type theory has a “naive” full function-space model, see for example the introduction in Troelstra [26]. Dybjer [8] gives a full function space model of Martin-Löf’s type theory with an external schema for inductive definitions. Aczel’s recent article [1] contains further information about set-theoretic interpretations of type theory.

Large cardinals in set theory. Induction-recursion gives quite a general approach to type-theoretic analogues of large cardinals in set theory. See for example Drake [6] for an introduction to large cardinals. Induction-recursion gives rise to analogues of for example inaccessible, hyper-inaccessible cardinals, and more generally Mahlo’s π-numbers [19], but does not justify the definition of a set, which is an analogue of a Mahlo cardinal. However, the type of sets has closure properties similar to those of a Mahlo cardinal.

Constructive versions of the model. The current model requires much more proof theoretic power than is actually needed: the strength of the type theory considered is very weak relative to ZF, even without any addition of large cardinals. Aczel [1] shows that the set theoretic models interpret as well the principle of excluded middle of type theory, an enormous strengthening of the type theory. In order to get a model in a theory which has the same strength, Aczel modifies the model and replaces ZF by constructive set theory CZF. One can as well define a model in a theory of the same strength by giving a realizability interpretation in Kripke-Platek set theory extended by a recursive Mahlo ordinal and ω admissibles above, extending [21, 24, 23]. Both models require some extra work, which exceeds the space available in this article.^{10}

Proof-theoretic strength of type theory. It should be easy to develop a term model of the theory in KPM^{+} used in [23] for the interpretation of Mahlo type theory. Such a model, which will make use of a (countable) recursive Mahlo ordinal and ω admissibles above it only, would show that the strength of the current type theory is at most as big as the Mahlo universe. On the other hand, set can be seen as being almost a Mahlo-universe, since we have induction over arbitrary types. What is missing to get the full strength is the possibility of having the W-type on top of the universe. In [10] together with [22], [24], [25] it was shown that in case of one universe such a restriction reduces the strength from |KPI^{+}| to |KPI| and with a similar argument for the lower bound as in [10] it is very likely that using the Mahlo-feature of set we have a lower bound |KPM|. Therefore it seems that the strength of our theory lies in the interval [|KPM|, |KPM^{+}|].

10The interpretation in the extension of Kripke-Platek set theory will be presented in an extended version of this article.

Inductive-recursive definitions seem to cover what is by many (but not all) researchers considered at the moment as predicative type theory. Even if some extensions are not covered by our calculus, it seems unlikely that such extensions will get beyond the strength of the Mahlo universe. This indicates that Mahloness is a natural boundary in the world of predicativity, which can only be crossed by adding principles such as the existence of the Mahlo universe as a set. The second author regards such principles as predicatively justifiable.

Inductive-recursive definition of indexed families. The external schema by Dybjer [7] considers the more general case of the simultaneous inductive-recursive definition of a set-indexed family of sets and functions. The present finite axiomatization can be extended to this case too, but we postpone the presentation of this to a future article.

References

[1] P. Aczel. On relating type theories and set theories. Submitted to TYPES’ 98, LNCS, Springer-Verlag.

[2] S. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Department of Computer Science, Cornell University, 1987.

[3] R. Backhouse. On the meaning and construction of the rules in Martin-Löf’s theory of types. In A. Avron, B. Harper, F. Honsell, I. Mason, and G. Plotkin, editors, Proceedings of the Workshop on General Logic, Edinburgh, February 1987. Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1988. ECS-LFCS-88-52.

[4] J. Cederquist. Pointfree Approach to Constructive Analysis in Type Theory. PhD thesis, Department of Computing Science, Chalmers University of Technology and University of Göteborg, 1997.

[5] T. Coquand and C. Paulin. Inductively defined types, preliminary version. In LNCS 417, COLOG ’88, International Conference on Computer Logic. Springer-Verlag, 1990.

[6] F. R. Drake. Set Theory - an Introduction to Large Cardinals. North Holland, 1974.

[7] P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. To appear in Journal of Symbolic Logic.

[8] P. Dybjer. Inductive sets and families in Martin-Löf’s type theory and their settheoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 280–306. Cambridge University Press, 1991.

[9] P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440–465, 1994.

[10] E. Griffor and M. Rathjen. The strength of some Martin-Löf type theories. Archive for Mathematical Logic, 33:347 – 385, 1994.

[11] P. Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 179–216. North-Holland, 1971.

[12] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[13] P. Martin-Löf. An intuitionistic theory of types. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998. To appear. Reprinted version of an unpublished report from 1972.

[14] P. F. Mendler. Predicative type universes and primitive recursion. In Proceedings Sixth Annual Synposium on Logic in Computer Science. IEEE Computer Society Press, 1991.

[15] B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory: an Introduction. Oxford University Press, 1990.

[16] E. Palmgren. On universes in type theory. To appear in: G. Sambin, and J. Smith, editors: Twenty-Five Years of Constructive Type Theory.

[17] E. Palmgren. On Fixed Point Operators, Inductive Definitions and Universes in Martin-Löf’s Type Theory. PhD thesis, Uppsala University, 1991.

[18] C. Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In Proceedings Typed λ-Calculus and Applications, pages 328–245. Springer-Verlag, LNCS, March 1993.

[19] M. Rathjen, E. R. Griffor, and E. Palmgren. Inaccessibility in constructive set theory and type theory. Annals of Pure and Applied Logic, 94:181 – 200, 1998.

[20] A. Setzer. Extending Martin-Löf Type Theory by one Mahlo-universe. To appear in Archive for Mathematical Logic.

[21] A. Setzer. Proof theoretical strength of Martin-Löf Type Theory with Wtype and one universe. PhD thesis, Fakultät für Mathematik der Ludwig-Maximilians-Universität München, 1993.

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

[23] A. Setzer. A model for a type theory with Mahlo universe. Draft, 1996.

[24] A. Setzer. An upper bound for the proof theoretical strength of Martin-Löf Type Theory with W-type and one Universe. Draft, 1996.

[25] A. Setzer. Well-ordering proofs for Martin-Löf type theory. Annals of Pure and Applied Logic, 92:113 – 159, 1998.

[26] A. S. Troelstra. On the syntax of Martin-Löf’s type theories. Theoretical Computer Science, 51:1–26, 1987.