Universes in Type Theory Part I – Inaccessibles and Mahlo

Anton Setzer^{∗}

November 9, 2005

Abstract

We give an overview over universes in Martin-Löf type theory and consider the following universe constructions: a simple universe, E. Palmgren’s super-universe and the Mahlo universe. We then introduce models for these theories in extensions of Kripke-Platek set theory having the same proof theoretic strength. The extensions of Kripke-Platek set theory used formalise the existence of a recursively inaccessible ordinal, a recursively hyper-inaccessible ordinal, and a recursively Mahlo ordinal. Using these models we determine upper bounds for the proof theoretic strength of the theories in questions. In case of simple universes and the Mahlo universe, these bounds have been shown by the author to be sharp. This article is an overview of the main techniques in developing these models. Full details will be presented in a series of future articles.

1 Introduction

This article presents some results of a research program with the goal of formulating extensions of Martin-Löf type theory (MLTT) that are proof-theoretically as strong as possible while remaining predicatively justified, and of determining their precise proof theoretic strength. We see three main reasons for following this research program:

1. The goal is to develop type theoretic analogues of the theories analysed in proof theory. In this way we hope to make the rather abstract and technically difficult results from proof theory more accessible to the general audience, and we hope as well to give some computational meaning to those results. This will be particularly important in case of the Π_{3}-reflecting universe (to be presented in the follow-up article [37]), which was developed from Rathjen’s ordinal notation system ([26]) for KP + (Π_{3} − refl) (Kripke-Platek set theory extended by the principle of Π_{3}-reflection).

∗Department of Computer Science, University of Wales Swansea, Singleton Park, Swansea SA2 8PP, UK, Email: a.g.setzer@swan.ac.uk, http://www.cs.swan.ac.uk/∼csetzer/, Tel:

+44 1792 513368, Fax: +44 1792 295651. Supported by Nuffield Foundation, grant ref.

NAL/00303/G and EPSRC grant GR/S30450/01.

2. One can consider predicatively justified extensions of MLTT as safe theories, more precisely theories for which there is a philosophical argument which justifies the validity of everything shown in those theories. This philosophical argument is given by Martin-Löf’s meaning explanations. The proofs of the lower bounds show that these extensions of MLTT show the consistency of corresponding extensions of Kripke-Platek set theory, or more precisely of any approximations of those extensions. If one accepts meaning explanations as a philosophical argument for the validity of statements shown in MLTT, one obtains in this way consistency proofs for extensions of Kripke-Platek set theory, which are strong enough to prove a large portion of mathematical theorems (see the results in reverse mathematics, e.g. Simpson’s book [38], which show that rarely more than the strength of (Π_{1}^{1} −CA)_{0} is needed; one exception seems to be the graph minor theorem). These results are in line with a revised Hilbert’s program. Hilbert’s original program was to prove the consistency of axiom systems for formalising mathematical proofs by finitary arguments. By Gödel’s incompleteness theorem we know that this program cannot be carried out. MLTT can be considered as one replacement for finitary methods in a revised Hilbert’s program, and our research demonstrates that MLTT can indeed be used for this purpose.

We should note however that meaning explanations haven’t been worked out yet in the case of the Mahlo universe – the author himself doesn’t have a sufficient background in philosophy to fill in this gap.

3. We hope as well that the new sets developed can be used as data structures in general computing. This hope has been fulfilled in case of the Mahlo universe. The data type of inductive-recursive definitions used in the closed formalisation of inductive-recursive definitions developed by P. Dybjer and the author (see [13, 14, 15, 16]) has a similar character to the Mahlo universe. Variants of this data type have been used in [10, 12] in the area of generic or generative programming.

In generative programming one aims at writing programs with a higher degree of polymorphism. Ordinary programs have as input elements of certain fixed data structures and compute from it elements of other fixed data structures. Polymorphic programs allow both the input and output data structures to be extended by certain type parameters, for instance both the input and output data structure can be List(X) (the type of lists of type X) depending on a type parameter X. Generative programs have as input data structures and elements of these data structures, and compute new data structures and elements of these. The computation can make use of the data and the build-up of the data structures. An example is the function, which takes as input an inductive data type and computes from it an inductive data type with one more constructor, and embeds the original data type into the extended one.

We hope that the Π_{3}-reflecting universe, which will be developed in the follow-up article [37], will give rise to data structures which have similar interesting applications in computer science.

We should note that whether the Mahlo universe and extensions of it presented in the follow-up article [37] are actually predicatively justifiable is still a matter of debate. However, even if there is a debate on this, it seems at least at the moment to be unlikely that a better construction can be found which avoids the problem in this case. For instance Erik Palmgren’s higher order universes [23] look at first sight more directly predicatively justifiable – but a closer look (it took the author a long time to actually discover this) reveals that in Palmgren’s construction Set has a similar character as a Mahlo universe. The introduction rule allows to introduce new elements of Set assuming an arbitrary function from families of Set into families of Set (the new element will be a universe closed under this function). This is essentially the same as the introduction rule for the Mahlo universe. Despite this criticism the author wants to express his strong admiration for Palmgren’s higher order universes – its a fascinating construction which doesn’t seem to have been fully understood yet. Especially its precise proof-theoretical strength still remains an open problem (to obtain as upper bound the strength of KPM by using techniques used in this article shouldn’t be a big problem – the real difficulty is to show that this is a lower bound as well).

Follow up articles. The original goal when writing this article was to present the Π_{3}-reflecting universe. It turned out that much more space is needed to present it, and therefore the presentation of the Π_{3}-reflecting universe will be given in a planned follow-up article [37]. Even so the current article is rather long, we won’t have room to present the models in full detail. We plan to write a series of articles, in which the models will be fully worked out. These future articles will then set up a better infrastructure for developing model constructions for extensions of MLTT. So the current article serves as an overview article, presenting the basic techniques for developing models of type theory suitable for determining upper bounds for the proof theoretic strength. It might be that this article is more accessible than the more detailed technical articles to follow.

Content. The structure of this article is as follows: In Sect. 2 we briefly develop the small and full logical framework and the basic set constructions (i.e. the sets N_{n}, N, and the sets formed using +, Σ, Π, W, Id). We then briefly introduce Kripke-Platek set theory. Then we develop the basic principles for defining models of type theory for the basic set constructions and the small logical framework. In Sect. 3 we introduce the rules for universes and the theory ML_{W}U. Furthermore we determine the principles for introducing nested universes. We will see that there are two ways of defining subuniverses, namely recursively and inductively. We then develop the main concepts for introducing models for universes and develop in particular a model of ML_{W}U. In Sect. 4 we introduce Erik Palmgren’s super-universe and develop a model of it in a corresponding extension of Kripke-Platek set theory. Finally, in Sect. 5 we introduce the Mahlo universe and determine a model of it. For all three universe constructions mentioned we obtain proof theoretic upper bounds for the strength of the theories in question.

Related results. The first model of MLTT developed for proof theoretic purposes seems to have been the model of MLTT with one universe but no W-type, developed by P. Aczel ([1]). Rathjen and Griffor have analysed the strength of MLTT with finitely many universes, W-type, and of several variants of it in [17] (where by finitely many universes we mean that one has universes U_{n} indexed over Meta-natural numbers n; so one cannot form for instance Σn : N.U_{n}). Erik Palmgren has introduced the super-universe and later higher order universes (the latter are conjectured to reach the strength of KPM), which are best presented in [23]. There is an extensive literature on PER models of MLTT – an overview of the techniques is given in M. Hofmann’s article [18]. Note that the emphasis of this article is in developing models in order to determine upper bounds for the proof-theoretic strength of those theories, which means as well to develop models using minimal strength in the Meta-theory. In this research programme we are following the steps of ordinal theoretic proof theory, where the major recent steps have been carried out by M. Rathjen, who analysed the theories KPM ([26]), KP + (Π_{3} − refl) [27] and (Π_{2}^{1} − CA) + (BI) ([28]; see [29] for a full version for the theory of parameter free Π_{2}^{1}-comprehension). Independently, similar steps have been taken by T. Arai ([5, 6, 7, 8]; there are as well preprints of Arai [2, 3, 4] covering Π_{n}-reflection, Σ_{1}-stability and Π_{1}- collection. This research benefitted very much from intensive discussions with T. Arai, U. Berger, P. Martin-Löf, E. Palmgren, and M. Rathjen.

2 Basic Martin-Löf Type Theory

In this section we will briefly introduce the version of Martin-Löf type theory (MLTT) used in this article. We will require some knowledge about MLTT. The reader not familiar with it might refer to [20, 21, 22, 25] or Chapter 11 of [39] (the latter deviates in its description of intensional type theory from the standard versions of MLTT).

2.1 The Small Logical Framework

The role of the logical framework in this article. In this article we will, when formally introducing theories and analysing them, not make use of the full logical framework. (We call the logical framework as it is used usually the full logical framework as opposed to the small logical framework, which is introduced in this subsection.) There are two reasons for this:

On one hand, the author has at the moment conceptual problems with the full logical framework. The problem manifests itself particularly when considering meaning explanations. Meaning explanations for the full logical framework don’t seem to have been worked out fully at present, whereas the concept of meaning explanations for type theory without the full logical framework seems to be well understood. One should note however that Per Martin-Löf seems to have a clear understanding of meaning explanations for the full logical framework, and has given talks on this topic.

On the other hand, a treatment of the full logical framework causes at the moment still problems when determining proof theoretic bounds. Our techniques for modelling type theories at present don’t allow to model the full logical framework directly without using more strength than is actually needed. Therefore, with our techniques we won’t be able to obtain precise proof theoretic bounds. In order to avoid this, it seems to be necessary to first eliminate the use of the full logical framework, and then to use the techniques used in this article. Martin Hofmann has shown in Sect. 4.3 of [18] that type theory with the full logical framework is conservative over type theory without it, which would give the desired reduction. However, we haven’t had time yet to study this result in detail in order to be sure that it can be applied to our setting.

For these two reasons all theories presented in the following will only make use of the restriction of the logical framework to Set, which we call the small logical framework. However, in order to explain the heuristics of our constructions, it is sometimes useful to make use of the full logical framework. We will do so for heuristic purposes only – when the formal theories are introduced, we will only make use of the small logical framework.

Judgements. The judgements of MLTT will be written as x_{1} : A_{1}, …, x_{n} : A_{n} ⇒ θ, where x_{1} : A_{1}, …, x_{n} : A_{n} is the context, often abbreviated as Γ or Δ, and θ is of the form A : Set, A = B : Set, a : A or a = b : A. In case of the empty context ∅, we write θ instead of ∅ ⇒ θ. In the presence of the full logical framework, A : Set, A = B : Set are replaced by A : Type, A = B : Type, respectively. (Note that A : Set and A = B : Set are in the presence of the full logical framework instances of the judgements a′ : A′ and a′ = b′ : A′ with A′ := Set, since Set : Type.)

The small logical framework. The small logical framework contains the dependent function set and product as in the full logical framework, but limited to sets. So we have, under the assumptions A : Set, x : A ⇒ B : Set, the following set constructions:

• The dependent function set (x : A) → B : Set.

– The formation rule allows to form (x : A) → B : Set from A : Set and x : A ⇒ B : Set.

– The introduction rule expresses that we can form (x : A)t : (x : A) → B provided x : A ⇒ t : B.

– The elimination rule expresses that we can apply f : (x : A) → B to a : A and obtain f(a) : B[x := a].

– We have as equality rule β-equality, i.e. ((x : A)t)(s) = t[x := s].

– Additionally we have the η-rule (which doesn’t fall under the general principle of having formation, introduction, elimination and equality rules): if f : (x : A) → B then f = (x : A)f(x).

– Furthermore we have equality versions of the formation, introduction, and elimination rule:

∗ The equality version of the formation rule expresses that if A = A′ : Set, x : A ⇒ B = B′ : Set, then (x : A) → B = (x : A′) → B′ : Set.

∗ The equality version of the introduction rule expresses that if x : A ⇒ t = t′ : B then (x : A)t = (x : A)t′ : (x : A) → B (that’s the ξ-rule).

∗ The equality version of the elimination rule expresses that if s = s′ : (x : A) → B and t = t′ : A then s(t) = s′(t′) : B[x := t].

∗ The principle of forming the equality versions of the formation, introduction and elimination rules from the standard (nonequality) rules is a straightforward principle. Therefore the convention is that whenever we introduce in the following formation, introduction and elimination rules, we silently introduce as well their equality versions. Note that there is no equality version of an equality rule.

∗ α-equivalent terms are considered to be identical, therefore there is no explicit rule for α-equality. This extends to judgements as well, i.e. x : A, y : B ⇒ C : Set and u : A, v : B[x := u] ⇒ C[x := u, y := v] : Set are considered as the same judgement.

– We mention the following abbreviations:

∗ We write f(a, b) instead of f(a)(b), similarly for longer applications.

∗ We usually omit the type A in (x : A)t and write (x)t instead.

∗ (x, y)t := (x)(y)t, similarly for longer expressions.

∗ We write A → B for (x : A) → B for a fresh variable x, (x, y : A) → B for (x : A) → (y : A) → B, (x : A, y : B) → C for (x : A) → (y : B) → C. Similar abbreviations are to be understood in the same way.

∗ If f : A → B and g : B → C, then g ∘ f := (x)g(f(x)).

• The dependent product (x : A) × B : Set.

– The introduction rule allows to form ⟨a, b⟩ for a : A and b : B[x := a].

– The elimination rule forms the projections of an element c : (x : A) × B : Set, written as π_{0}(c) : A and π_{1}(c) : B[x := π_{0}(c)].

– The equality rule expresses that π_{0}(⟨a, b⟩) = a and π_{1}(⟨a, b⟩) = b.

– We have as well the η-rule associated with it, so if c : (x : A) × B then c = ⟨π_{0}(c), π_{1}(c)⟩.

– We have similar abbreviations for the product as for the function set, especially A × B := (x : A) × B for some fresh variable x.

Definition 2.1. By the rules of the small logical framework we mean the structural rules of type theory and the rules for the dependent function set and the dependent product restricted to Set.

2.2 The Full Logical Framework

The full logical framework (which is not part of any of the type theories in this article unless explicitly stated), is obtained in the following way: In the small logical framework we were introducing sets, and elements of such sets. These sets are small types. In the full logical framework we have as well large types. There is a judgement A : Type for A is a large type. We have Set : Type, and if A : Set then A : Type. So we have the rules

Set : Type  \begin{matrix}A : Set \\ A : Type \end{matrix}  \begin{matrix}A = B : Set \\ A = B : Type \end{matrix}

If A : Type, then A can occur on the right hand side of the colon, especially we can conclude from Γ ⇒ A : Type that Γ, x : A is a context and Γ, x : A ⇒ x : A. Apart from Set, Type will as well be closed under the dependent function type and the dependent product. So if A : Type and x : A ⇒ B : Type, then

• (x : A) → B : Type,

• (x : A) × B : Type.

These types have essentially the same rules as the corresponding sets of the small logical framework, except that one refers to Type instead of Set.

2.3 The Basic Set Constructions

The basic set constructions are the following sets (or more precisely principles for forming sets) and their corresponding rules:

• The finite sets N_{n} : Set, where n ∈ {0, 1, …}. Note that here n is not an internal natural number inside type theory, but exists on the Meta-level. The introduction rules are A_{i}^{n} : N_{n} for i = 0, …, n − 1 (where i are again natural numbers on the Meta-level).

• The set N of natural numbers. The introduction rules are 0 : N and S : N → N.

• The disjoint union A + B of two sets A, B, with introduction rules inl : A → (A + B) and inr : B → (A + B).

• For A : Set and x : A ⇒ B : Set we have the following sets:

– The Π-set Πx : A.B. The introduction rule is λ : ((x : A) → B) → Πx : A.B. One writes λx : A.t for λ((x : A)t).

– The Σ-set Σx : A.B. The introduction rule is p : (a : A) → (b : B[x := a]) → Σx : A.B. (The differences between Πx : A.B, Σx : A.B, and (x : A) → B, (x : A) × B, respectively, will be explained below).

– The W set Wx : A.B, which is the set of well-founded trees with branching degrees B[x := a] for a : A. The introduction rule is sup : (a : A, b : B[x := a] → Wx : A.B) → Wx : A.B.

• The intensional identity set Id(A, a, b) for A : Set, a : A, b : A. The introduction rule is refl_{A} : (a : A) → Id(A, a, a).

• For all of the above set constructions, the elimination rules express that the above sets are the least sets introduced by these constructors. This will be for instance in case of N primitive recursion into arbitrary sets (which may depend on the element n : N we are eliminating), in case of W induction over those trees, and in case of A + B case distinction on whether ab : A + B is of the form inl(a) or inr(b).

• Furthermore, we have the standard equality rules for the above mentioned sets.

The main difference between the dependent function set and product and the sets Πx : A.B, Σx : A.B is that we have the η-rule for the constructions of the logical framework, but not for Π and Σ. The conceptual reason for this becomes clear when considering inductive-recursive definitions. All the basic set constructions are instances of inductive-recursive definitions (in case of Id(A, a, b) general indexed inductive-recursive definitions) as introduced originally by P. Dybjer with a formalisation using finitely many rules by P. Dybjer and the author; see [11, 12, 13, 14, 15, 16]). Indexed inductive-recursive definitions allow to introduce all sets in MLTT by determining their introduction rules (there are of course restrictions on which introduction rules are allowed). The elimination and equality rules are then derived automatically. There is no η-rule involved in this schema, which would be unnatural in general. For instance, it does not make much sense to consider an η-rule for N. Therefore it is natural to exclude the η-rule from Π and Σ, and to have separate logical framework versions which contain the η-rule. In this article, the difference between the constructions of the small logical framework and the Π- and Σ-set won’t play a big rôle.

Our models will admit as well the addition of an extensional equality set to the type theory. Since lower bounds will be obtained using intensional equality only, it will follow that the proof theoretic strength of the type theories under consideration with intensional equality and with extensional equality coincides.

Definition 2.2. (a) By the basic set constructions in type theory we mean the above mentioned constructions N_{n}, N, +, Σ, Π, W, Id for forming sets, and the corresponding formation/introduction/elimination/equality rules.

(b) Basic MLTT is the type theory consisting of the rules of the small logical framework and of the basic set constructions.

2.4 Kripke-Platek Set Theory

In this article, we will develop models of the type theories considered in extensions of Kripke-Platek set theory. This will allow us to determine upper bounds for the proof theoretic strength of the theories in question.

Kripke-Platek set theory (KP) is a weak version of set theory, based on classical logic. The “bible” of KP is the book by Barwise [9]. KP can be used in order to develop most concepts in generalised recursion theory, as demonstrated in that book. KP has been pioneered by Jäger [19] as a reference theory for proof theoretic studies (see as well the handbook article by Pohlers [24], which contains an overview over proof theoretic results up to the strength of KPI in this area). For many theories, there exists a variant of KP of equal strength, and often one can determine upper bounds for theories by first determining upper bounds for the variant for KP of equal strength, and then by modelling the original theory in that variant. This is as well the approach taken in this article.

We don’t have room to introduce KP in full (we highly recommend the reader not familiar with it to study the first chapters of [9]). We briefly repeat here its axioms (see p. 10 of [9]; the theory presented in [9] adds to KP as well urelements, and is therefore called KPU for KP plus urelements; the variants of KP used in this article don’t have urelements; Δ_{0}-formulae are formulae containing only bounded quantifiers, FV(φ) are the free variables of φ):

(Extensionality) ∀x, y.(∀z.z ∈ x ↔ z ∈ y) → x = y .
(Foundation)  ∀z⃗.(∀x.(∀y ∈ x.φ(y, z⃗)) → φ(x, z⃗)) → ∀x.φ(x, z⃗) ,
where FV(φ(x, z⃗)) ⊆ {x, z⃗}.
(Pair)  ∀x, y.∃z.x ∈ z ∧ y ∈ z .
(Union)  ∀x.∃y.∀z ∈ x.∀u ∈ z.u ∈ y .
(Δ_{0}-Separation) ∀u⃗, x.∃y.∀z.(z ∈ y ↔ (z ∈ x ∧ φ(z, u⃗))) ,
where φ(z, u⃗) is Δ_{0}, FV(φ(z, u⃗)) ⊆ {z, u⃗}.
(Δ_{0}-Collection) ∀u⃗, x.(∀y ∈ x.∃z.φ(y, z, u⃗)) → ∃v.∀y ∈ x.∃z ∈ v.φ(y, z, u⃗) ,
where φ(y, z, u⃗) is Δ_{0}, FV(φ(y, z, u⃗)) ⊆ {y, z, u⃗}.

The variants of KP used in this article will always be augmented by the axiom of infinity

(Infinity) ∃x.∅ ∈ x ∧ ∀y ∈ x.y ∪ {y} ∈ x ,

where ∅ ∈ x and y ∪ {y} ∈ x are to be understood in the usual way as Δ_{0}- formulae. Let KPω be the theory KP plus the axiom of infinity.

When forming extensions of KPω, one adds a predicate Ad(x) for “x is an admissible containing ω”, following the approach taken by Jäger (e.g. [19]; see as well Pohlers’ survey article [24]). Here an admissible is a transitive inner model of KP, and by an admissible > ω we mean an admissible containing ω, i.e. a transitive inner model of KPω. So one has the following additional axioms (trans(x) expresses that x transitive):

(Ad.1) ∀x.Ad(x) → trans(x) .
(Ad.2) ∀x, y.Ad(x) ∧ Ad(y) → (x ∈ y ∨ x = y ∨ y ∈ x) .
(Ad.3) ∀x.Ad(x) → ψ^{x} ,

for every instance ψ of (Pair), (Union), (Δ_{0}-Separation), (Δ_{0}-Collection), (Infinity).

ψ^{x} is obtained by replacing all unbounded quantifiers ∀y, ∃y occurring in ψ by ∀y ∈ x, ∃y ∈ x respectively, but leaving bounded quantifiers as they are (where a bounded quantifier is a quantifier of the form ∀y ∈ z, ∃y ∈ z). The extensions of KPω are then obtained by adding to KPω the above axioms for Ad and axioms expressing that there exists an admissible with sufficiently strong closure properties. The convention in this article is that whenever we introduce an extension of KP, we always add as well the infinity axiom and, if Ad is involved in any of the additional axioms, the axioms (Ad.1-3).

We introduce as well the theory KPl^{r} which expresses that there are finitely many admissibles (i.e. for Meta-each n we have a chain of n admissibles a_{0} ∈ a_{1} ∈ ⋯ ∈ a_{n−1}) but that the set theoretic universe itself is not necessarily a model of KP. The standard model of KPl^{r} is a := ⋃_{n∈ω} b_{n}, where b_{n} is the nth admissible (n ∈ ω). Note that a is not an admissible. Formally, KPl^{r} is obtained by taking KPω without (Δ_{0}-Collection), with (Foundation) restricted to Δ_{0}-formulae φ(x, z⃗). and by adding the axioms (Ad.1 -3) and the following axiom (Lim):

(Lim) ∀x.∃y.Ad(y) ∧ x ∈ y

The theory KPl is defined as KPl^{r}, but with (Foundation) for all formulae φ(x, z⃗).

When working in extensions of KPω, we will frequently make use of the constructible hierarchy, and refer to the definition of L_{α} in [9]. We define as well the following:

Definition 2.3. (a) L_{<α} := ⋃_{β<α} L_{β},

(b) L′_{α} := L_{ω·α},

(c) L′_{<α} := ⋃_{β<α} L′_{β}.

(d) An admissible ordinal is an ordinal α such that L_{α} is admissible.

We will often make use of the following essentially trivial remark:

Remark 2.4. (a) If c = {x ∈ a | φ(x, b⃗)}, where φ(x, y⃗) is Δ_{0}, FV(φ(x, y⃗)) ⊆ {x, y⃗}, and a, b⃗ ∈ L′_{α} ∪ {L′_{α}}, then c ∈ L′_{α+1}.

(b) α ∈ L′_{α+1}.

(c) ω ∈ L′_{2}.

(d) L′_{β} = L_{β}, if β is a multiplicative principal number, e.g. an admissible ordinal > ω.

Proof. Let Ord be the class of ordinals. (a): Assumption II.5.2 and Theorem II.6.4 of [9]. (b): One easily can show that L_{α} ∩ Ord ∈ Ord. We show the assertion by induction on α. The cases α = 0 and α → α + 1 follow easily or by induction hypothesis (IH). In case α being a limit ordinal we have by IH α ⊆ L′_{<α} ∩ Ord =: β ∈ L′_{α+1}, and therefore α ∈ L′_{α+1}. (c): ω ⊆ L_{<ω}, L_{<ω} ∩ Ord ⊆ ω, therefore ω := {x ∈ L_{<ω} | Ord(x)} ∈ L_{ω+ω} = L′_{2}. (d): ω · β = β.

2.5 Models of Basic MLTT

As said before, we will develop models of the type theories in question in extensions of KPω. These models will extend the model of MLTT with one universe and the W-type, as worked out in the author’s PhD thesis [30]. (See as well [32] for a draft version of an article on it, and [31] for an article containing a basic model construction for MLTT with one Mahlo universe.) We will first start to explain how to model basic MLTT.

Basic principles of the model construction. The basic idea of all our models is that we define a PER model, i.e. a model in which sets are interpreted as partial equivalence relations on a set of basic objects, where in this article the set of basic objects will be a set of terms, which is a slightly simplified version of the set of terms occurring in the type theory. Let ML′ denote the type theory for which we want to determine an upper bound for its proof theoretic strength. We will model ML′ in an extension KP′ of KPω. KP′ will be defined in such a way that it has the same expected proof theoretic strength. Once we have modelled ML′ in KP′ one will be able to conclude (this step requires some techniques which can be found in [30]) that the proof theoretic strength |ML′| of ML′ is less than or equal to the proof theoretic strength |KP′| of KP′, i.e. |ML′| ≤ |KP′|.

The soundness theorem for the model of type theory will be a Meta-theorem (otherwise we would obtain |ML′| < |KP′|): For Meta-every judgement Γ ⇒ θ such that ML′ ⊢ Γ ⇒ θ we have that KP′ proves the correctness statement associated with Γ ⇒ θ. But ML′ doesn’t prove that for all Γ ⇒ θ the correctness statement holds. In fact, ML′ cannot even express such a general correctness statement.

Let Term be the underlying set of terms occurring in ML′. We will introduce in the model a set of closed terms [[ Term ]] using essentially the same term and type constructors and destructors as in the type theory. α-equivalent terms (as well sets, context, judgements) will always be identified. However, we will, when introducing the models of the universes below occasionally throw away arguments needed for type checking purposes only (this is not really necessary, but simplifies matters).

One introduces as well a deterministic reduction relation ⟶ on [[ Term ]] corresponding to weak head reductions following the equality rules of the type theory. ⟶^{∗} is the reflexive and transitive closure of ⟶.

Definition 2.5. (Environments)

(a) An environment relative to a sequence of variables x_{1}, …, x_{n} is an expression [x_{1} = s_{1}, …, x_{n} = s_{n}], where x_{i} are distinct variables and s_{i} ∈ [[ Term ]].

(b) ∅ stands for the empty environment [].

(c) [x_{1} = s_{1}, …, x_{n} = s_{n}], y = t := [x_{1} = s_{1}, …, x_{n} = s_{n}, y = t], where we assume that after some renaming of variables corresponding to α-conversion in the situation used, y is different from x_{i}.

(d) FV([x_{1} = s_{1}, …, x_{n} = s_{n}]) := {x_{1}, …, x_{n}}.

(e) [x_{1} = s_{1}, …, x_{n} = s_{n}](x_{i}) := s_{i}.

(f) Env(x_{1}, …, x_{n}) := {[x_{1} = s_{1}, …, x_{n} = s_{n}] | s_{1}, …, s_{n} ∈ [[ Term ]]}.

The interpretation [[ t]]_{ρ} ∈ [[ Term ]] for environments ρ and terms t ∈ Term such that FV(t) ⊆ FV(ρ) is the result of omitting in t the arguments of constructors/destructors to be thrown away (as indicated when introducing the constants) and substituting free variables x in t by ρ(x).

We write [[ t]] for [[ t]]_{∅}.

Then one defines the interpretation [[ A]]_{ρ} of sets A relative to environments ρ such that FV(A) ⊆ FV(ρ) as a set of pairs ⟨s, t⟩ of closed terms. The intended meaning for ⟨s, t⟩ ∈ [[ A]]_{ρ} is that s and t are equal elements of the interpretation of A. We write [[ A]] for [[ A]]_{∅}.

We define some basic operations on sets X ⊆ [[ Term ]]^{2}:

Definition 2.6. Let X ⊆ [[ Term ]]^{2}.

(a) The closure of X under reductions is defined as

Clos_{→}(X) := {⟨s, t⟩ | ∃⟨s′, t′⟩ ∈ X | s ⟶^{∗} s′ ∧ t ⟶^{∗} t′} .

(b) Flat(X) := {a ∈ [[ Term ]] | ∃b ∈ [[ Term ]].⟨a, b⟩ ∈ X ∨ ⟨b, a⟩ ∈ X}.

(c) PER(X) iff X is a partial equivalence relation (i.e. symmetric and transitive) and X is closed upwards under ⟶, i.e. Clos_{→}(X) ⊆ X.

Flat([[ A]]_{ρ}) is the set of elements of the interpretation of A, and ⟨a, b⟩ ∈ [[ A]]_{ρ} means that a and b are equal elements of [[ A]]_{ρ}. This is meaningful if PER([[ A]]_{ρ}) holds, which we will show for all derivable sets A as expressed by the correctness statement below.

In the models for the type theories considered in this article, we can as well assign to every set A with FV(A) ⊆ {x_{1}, …, x_{n}} an ordinal o(A) ≥ 3 such that for all ρ ∈ Env(x_{1}, …, x_{n}) we have [[ A]]_{ρ} ∈ L′_{o(A)}, independent of ρ. Note that [[ Term ]] is a Δ_{0}-definable subset of ω and therefore [[ Term ]] ∈ L′_{3}.

The definition of [[ A]]_{ρ} and o(A) for A formed by one of the basic set constructions or constructions of the small logical framework is as follows:

• [[ N ]]_{ρ} := [[ N ]] := Clos_{→}({⟨S^{n}(0), S^{n}(0)⟩ | n ∈ ω}).

o(N) := 3 (this is probably not the minimal ordinal one can associate with it, similarly for the later ordinals, but this bound suffices for our proofs).

• [[ Σx : A.B]]_{ρ} := [[ Σ ]]([[ A]]_{ρ}, λs ∈ Flat([[ A]]_{ρ}).[[ B]]_{ρ,x=s}), where, if A ⊆ [[ Term ]]^{2}, and for a ∈ Flat(A) we have B(a) ⊆ [[ Term ]]^{2}, then

[[ Σ ]](A, B) := Clos_{→}(\begin{cases}⟨p(a, b), p(a′, b′)⟩ \\ | ⟨a, a′⟩ ∈ A ∧ (B(a) = B(a′)) ∧ ⟨b, b′⟩ ∈ B(a)\}) . \end{cases}

(Here λx ∈ A.s(x) := {⟨x, s(x)⟩ | x ∈ A}; note that p is the constructor of Σ as defined in Subsect. 2.3, and that according to our convention f(a, b) is an abbreviation for f(a)(b), therefore p(a, b) stands for p(a)(b)).

o(Σx : A.B) := max{o(A), o(B)} + 2.

• Similarly one defines the semantics and the ordinals of N_{n}, Πx : A.B, Wx : A.B, A + B, Id(A, a, b), (x : A) → B, (x : A) × B, making use of suitable definitions of [[ N_{n}]], [[ Π ]], [[ W ]], [[ + ]], [[ Id ]], [[ →]] and [[ ×]], and incrementing the ordinals as for Σ by 2 (except for W, see below; o(N_{n}) := 2).

We introduce here as well the following notations to be used later:

– (x ∈ A) [[ →]] B := [[ →]](A, λx ∈ Flat(A).B),

– A [[ →]] B := (x ∈ A) [[ →]] B where x is fresh,

– (x ∈ A) [[ ×]] B := [[ ×]](A, λx ∈ Flat(A).B),

– A [[ ×]] B := (x ∈ A) [[ ×]] B where x is fresh.

– We can omit brackets in the above, using for [[ →]], [[ ×]] the same conventions as we have for →, ×.

In the case of W only, one defines o(Wx : A.B) := (max{o(A), o(B)})^{+}+1, where α^{+} is the next admissible ordinal above α. The reason for using α^{+} +1 in case of [[ W ]] is that [[ W ]](A, B) is defined by iterating α^{+}-times an operator Φ. Here Φ(A) is the set of trees with immediate subtrees in A.

We interpret contexts as sets of environments as follows:

\begin{matrix}[[ x_{1} : A_{1}, …, x_{n} : A_{n}]] := \\ \{⟨[x_{1} = s_{1}, …, x_{n} = s_{n}], \begin{matrix}[x_{1} = t_{1}, …, x_{n} = t_{n}]⟩ | \\ ⟨s_{1}, t_{1}⟩ ∈ [[ A_{1} ]]_{∅}∧ \\ ⟨s_{2}, t_{2}⟩ ∈ [[ A_{2} ]]_{[x_{1}=s_{1}]} ∧ ⋯ ∧ \\ ⟨s_{n}, t_{n}⟩ ∈ [[ A_{n}]]_{[x_{1}=s_{1},...,x_{n−1}=s_{n−1}]}\} . \end{matrix} \end{matrix}

Definition 2.7. The correctness of a judgement is defined as follows by induction on the length:

(a) Correct(∅ ⇒ Context) (where ∅ is the empty context) is defined as a true formula, e.g. ∀x.x = x.

(b)

Correct(Γ ⇒ A = B : Set)

:= Correct(Γ ⇒ Context) ∧ ∀⟨ρ, ρ′⟩ ∈ [[ Γ ]].PER([[ A]]_{ρ}) ∧ [[ A]]_{ρ} = [[ B]]_{ρ′} .

(c)

Correct(Γ, y : A ⇒ Context) := Correct(Γ ⇒ A : Set) := Correct(Γ ⇒ A = A : Set) ,

as just defined.

(d)

Correct(Γ ⇒ a = b : A)

:= Correct(Γ ⇒ A : Set) ∧ ∀⟨ρ, ρ′⟩ ∈ [[ Γ ]].⟨[[ a]]_{ρ}, [[ b]]_{ρ′}⟩ ∈ [[ A]]_{ρ} .

(e) Correct(Γ ⇒ a : A) := Correct(Γ ⇒ a = a : A) as just defined.

The correctness statement to be shown by induction on the derivations in ML′ is as follows: For Meta-every judgement Γ ⇒ θ we have

(ML′ ⊢ Γ ⇒ θ) → KP′ ⊢ Correct(Γ ⇒ θ) .

3 Universes and Recursively Inaccessibles

3.1 Rules for Universes

A universe (à la Tarski) in MLTT (Martin-Löf type theory) is given by a set U : Set of codes for sets together with a decoding function T : U → Set, which without the full logical framework is given by the following rule:

\begin{matrix}u : U \\ T(u) : Set \end{matrix}

All universes in the following will be closed under the basic set constructions (i.e. N_{n}, N, Σ, Π, W, +, Id). This means that we have in case of N and Σ the rules:

N̂ : U  T(N̂) = N

\begin{aligned}a : U & b : T(a) → U \\ & Σ̂(a, b) : U \end{aligned} T(Σ̂(a, b)) = Σx : T(a).T(b(x))

(The codes for N_{n}, Π, W, +, Id will be called N̂_{n}, Π̂, Ŵ, ˆ+, Îd respectively.)

In particular we consider the theory ML_{W}U consisting of the small logical framework, the basic set constructions and one universe (which is by our convention closed under the standard set constructors including the W-set, but not under U itself; the subscript W stands for the closure under the W-set).

We will not add any elimination rules for universes. In case of the theory ML_{W}U and of the super-universe (as introduced in Sect. 4), they could be added without any problems, but won’t add in the presence of the W-set any strength.^{1} In case of the Mahlo universe (Sect. 5) and stronger universes, such elimination rules result in inconsistencies (see Theorem 6.1 in [23]).

Type theories with several universes. We will already here look at how to extend this approach to type theories having several universes. In this case, the codes N̂, Σ̂ etc. have special names and additional parameters so that we can distinguish them from each other. These parameters will always be omitted when moving to [[ Term ]]. E.g. if we have universes V and U_{a,b}, we have in Term codes N̂_{V} and N̂_{U,a,b}, whereas in [[ Term ]] we have only one code N̂ and define [[ N̂_{V} ]]_{ρ} := [[ N̂_{U,a,b}]]_{ρ} := N̂.

By a recursive subuniverse (U, T̂_{U}) of a universe (V, T_{V}) we mean that we have U : Set, but, instead of having T_{U} : U → Set (or, if one avoids the full logical framework, the rule stating that if a : U then T_{U}(a) : Set), we have the rule formulating the existence of a function T̂_{U} : U → V, which recursively decodes codes by their corresponding codes in the other set. If we for a : U define T_{U}(a) := T_{V}(T̂_{U}(a)) : Set, we have therefore the rules

1One can show this by extending the model given in the following to include the elimination rules for the universe while still using the same Meta theory for modelling it. Therefore the upper bound for the proof theoretic strength of the type theory with elimination rules coincides with the upper bound for the theory without elimination rules which in turn coincides with the lower bound for the theory without elimination rules obtained using a well-ordering proof.

The idea for a more direct proof – we haven’t carried out the details yet – is to use the W-set in order to select out of the ordinary universe a subuniverse which is the least universe closed under the basic set constructions. That would show that a type theory with elimination rules for the universe could be interpreted in the type theory without those rules. Both techniques wouldn’t work for constructions like the Mahlo universe.

N̂_{U} : U  T̂_{U}(N̂_{U}) = N̂_{V}

\begin{aligned}a : U & b : T_{U}(a) → U \\ & Σ̂_{U}(a, b) : U \end{aligned} T̂_{U}(Σ̂_{U}(a, b)) = Σ̂_{V}(T̂_{U}(a), T̂_{U} ∘ b)

similarly for the other basic set constructions.

Sometimes it will not be possible to develop the subuniverses introduced in this article as recursive subuniverses. The problem occurs as soon as we have infinite chains of universes. Consider for instance a sequence of universes (U_{α})_{α≤β} such that U_{α} is a subuniverse of U_{α′} for α < α′. There is no problem of using recursive subuniverses, if we have a finite sequence of such universes (i.e. β < ω): Then we can consider for α < β the universe U_{α} as a recursive subuniverse of U_{α+1}, whereas the universe U_{β} itself is defined as a standard universe. The set corresponding to a : U_{α} is then T_{β}(T̂_{β−1}(⋯ (T̂_{α}(a)) ⋯)). If β = ω, we would however with this approach end up with a nonterminating chain

U_{0} \underrightarrow{T̂_{0}} U_{1} \underrightarrow{T̂_{1}} U_{2} \underrightarrow{T̂_{2}} ⋯

and we cannot determine a set corresponding to a : U_{0}.

The way around this is to follow Per Martin-Löf’s approach, by forming inductive subuniverses. An inductive subuniverse U of a universe (V, T_{V}) is given by

• a set U,

• a recursively defined decoding function T_{U} : U → Set, and

• a constructor T̂_{U} : U → V.

So T̂_{U} : U → V forms an additional introduction rule for V.

If we avoid the full logical framework, we get the following rules for an inductive subuniverse (U, T_{U}) of (V, T_{V}):

U : Set  \begin{matrix}a : U \\ T_{U}(a) : Set \end{matrix}
\begin{matrix}a : U \\ T̂_{U}(a) : V \end{matrix}  T_{V}(T̂_{U}(a)) = T_{U}(a)
N̂_{U} : U  T_{U}(N̂_{U}) = N

\begin{aligned}a : U & b : T_{U}(a) → U \\ & Σ̂_{U}(a, b) : U \end{aligned} T_{U}(Σ̂_{U}(a, b)) = Σx : T_{U}(a).T_{U}(b(x))

Similarly for the other basic set constructions.

The reason why we prefer recursive subuniverses to inductive ones is that we obtain in inductive subuniverses many copies of the same element. In the simple situation, we have for instance two codes for N in V, namely N̂_{V} and T̂_{V}(N̂_{U}). This is not very aesthetic (it doesn’t cause many problems when actually making use of such universes). However, one should be aware that we anyway get often doubling of codes. For instance, if in case of the super-universe to be introduced in Sect. 4 we form a recursive subuniverse (U, T̂_{U}) of (V, T_{V}) containing the family ⟨N̂_{V}, (x)N̂_{V}⟩, then U will have infinitely many codes for N, namely N̂_{U}, â and b̂(n) for n : N.

When modelling subuniverses, we will treat them as mere subsets of the interpretation of the original universe. T̂_{U} will for both the recursive and inductive subuniverses be essentially the identity function, expressed by the reduction rule T̂_{U}(a) ⟶ a. This means that in the model we will identify codes coming from the same element in U, so for instance all the codes for N in the above example will be equal in the model.

3.2 Modelling Universes

For modelling universes closed under the W-set in extensions of KPω one needs the notion of a recursively inaccessible ordinal. A recursively inaccessible ordinal I is an admissible ordinal I such that for every β ∈ I there exists a γ ∈ I such that β ∈ γ and γ is an admissible ordinal. If one refers to admissible sets rather than admissible ordinals, then a recursively inaccessible set is a set a such that

Ad(a) ∧ ∀y ∈ a.∃z ∈ a.y ∈ z ∧ Ad(z) .

Let KPI^{+} be the theory of KPω extended by the existence of one recursively inaccessible set and finitely many admissibles (i.e. for Meta-each n we have n admissibles) above it. So KPI^{+} has constants a_{I,k} for Meta k ∈ ω, axioms expressing that a_{I,0} is a recursively inaccessible set, and for Meta k ∈ ω the axioms

Ad(a_{I,k}) ∧ a_{I,k} ∈ a_{I,k+1} .

Proof theoretically equivalent is the theory KPl^{r} plus the existence of one recursively inaccessible set.

A universe is a family of sets, and therefore it will be modelled by a family of terms, i.e. an element of [[ Fam ]](Set), as given by the following definition (dom(f) is the domain of the function f):

Definition 3.1. (in the language of Kripke-Platek set theory).

(a) By Set we mean the class of all sets.

(b) [[ Fam ]](Set) := \{(A, B)\begin{matrix}∈ Set^{2} | A ⊆ [[ Term ]]^{2} \\ ∧B is a function \\ ∧dom(B) = Flat(A) \\ ∧∀x ∈ Flat(A).B(x) ⊆ [[ Term ]]^{2} \\ ∧∀⟨x, x′⟩ ∈ A.B(x) = B(x′)\} . \end{matrix}

(c) Assume (A, B) ∈ [[ Fam ]](Set). Then the set [[ IFam ]](A, B) of families of sets internal to (A, B) ([[ IFam ]] stands for internal family) is defined as

[[ IFam ]](A, B) := (x ∈ A) [[ ×]] (B(x) [[ →]] A) ,

(which is

Clos_{→}(\{⟨c, c′⟩ ∈ [[ Term ]]^{2} | \begin{matrix}⟨π_{0}(c), π_{0}(c′)⟩ ∈ A \\ ∧ (B(π_{0}(c)) [[ →]] A) = (B(π_{0}(c′)) [[ →]] A) \\ ∧ ∀⟨x, x′⟩ ∈ B(π_{0}(c)).⟨π_{1}(c)(x), π_{1}(c′)(x′)⟩ ∈ A\}) ) . \end{matrix}

(Note that π_{i} are the projections of pairs ⟨a, b⟩, which are part of the small logical framework, see Subsect. 2.1.)

(d) Assume (A, B), (A′, B′) ∈ [[ Fam ]](Set). Then

(A, B) ≤ (A′, B′) :⇔ A ⊆ A′ ∧ B ⊆ B′ .

Note that by (A, B), (A′, B′) ∈ [[ Fam ]](Set), B ⊆ B′ is equivalent to

B ↾ Flat(A) = B′ ↾ Flat(A) .

(e) Assume (U^{α}, T^{α}) ∈ [[ Fam ]](Set) for α < β such that

∀α < α′ < β.(U^{α}, T^{α}) ≤ (U^{α′}, T^{α′}) .

Then we define

(U^{<β}, T^{<β}) := ( ⋃_{α<β} U^{α}, ⋃_{α<β} T^{α}) ∈ [[ Fam ]](Set) .

Note that, if x ∈ Flat(U^{α}), α < β, then

T^{<β}(x) = T^{α}(x) .

A model of a universe (U, T) can be obtained by defining sets [[ U ]] and [[ T ]] such that

([[ U ]], [[ T ]]) ∈ [[ Fam ]](Set) .

Then

[[ T(s) ]]_{ρ} := [[ T ]]([[ s]]_{ρ}) .

We will introduce first by induction on α sets

(U^{α}, T^{α}) ∈ [[ Fam ]](Set)

and define (assuming the existence of a recursively inaccessible ordinal I)

[[ U ]] = U^{<I} , [[ T ]] = T^{<I}

for the least recursively inaccessible ordinal I. (When we later in this article consider universes closed under additional constructions, the ordinal I will be replaced by a recursively inaccessible ordinal, which has some additional closure properties.)

We will guarantee that the following assumptions are fulfilled:

Assumption 3.2. (U^{α}, T^{α}) ∈ [[ Fam ]](Set) are defined in such a way that the following holds:

(a) α < β → (U^{α}, T^{α}) ≤ (U^{β}, T^{β}).

(b) PER(U^{α}) ∧ ∀x ∈ Flat(U^{α}).PER(T^{α}(x)).

(c) U^{α} ∈ L′_{α+1} ∧ ∀x ∈ Flat(U^{α}).T^{α}(x) ∈ L′_{α}.

(d) (λβ < α.U^{β}) ∈ L′_{α+1} ∧ (λβ < α.λx ∈ U^{β}.T^{β}(x)) ∈ L′_{α+1}.

(e) “x ∈ U^{β}” and “x ∈ T^{β}(y)” are Σ_{1}-formulae, and the unbounded existential quantifiers in those Σ_{1}-formulae can be, if we restrict β to ordinals less than α (where α ≥ 2), restricted to L′_{α}.

Here (e) follows from the fact that the unbounded existential quantifiers in the definition of U^{β} and T^{β}(x), restricted to β < α, are of the form ∃f, where f is λδ < β.U^{δ}, λδ < β.λx ∈ U^{δ}.T^{δ}(x), λδ < β.L′_{δ}, ω or a primitive recursive function on ω, and therefore f is an element of L′_{β+1} ⊆ L′_{α}. (Here λδ < β.U^{δ} stands for the set theoretic function with domain β mapping δ to U^{δ}.) More precisely, when showing that this assumption is fulfilled one shows simultaneously (c) - (e) by induction on α.

Because of PER(U^{α}), U^{α} needs to be closed under reductions. This is more formally obtained as follows: When defining U^{α} below, what we actually define are sets U′^{α} and functions T′^{α} (while still referring to U^{<α} and T^{<α}). Then one defines (U^{α}, T^{α}) itself as the closure of (U′^{α}, T′^{α}) under reductions (note that ⟶ is a deterministic reduction relation):

U^{α} := Clos_{→}(U′^{α}) ,
T^{α}(a) := T′^{α}(a′) if a ⟶^{∗} a′ ∈ U′^{α} .

We will however in the following not explicitly mention U′^{α}, T′^{α} in this article, assuming that the reader can adapt the model correspondingly.

U^{α} is the closure of U^{<α} under one application of each basic set construction of type theory, provided the results are in L′_{α}, as expressed by the following:

• [[ N ]] ∈ L′_{α} → ⟨N̂, N̂⟩ ∈ U^{α}, T^{α}(N̂) = [[ N ]].

• Assume ⟨⟨a, b⟩, ⟨a′b′⟩⟩ ∈ [[ IFam ]](U^{<α}, T^{<α}), and

A := [[ Σ ]](T^{<α}(a), λx ∈ T^{<α}(a).T^{<α}(b(x))) ∈ L′_{α} .

Then ⟨Σ̂(a, b), Σ̂(a′, b′)⟩ ∈ U^{α} and T^{α}(Σ̂(a, b)) = A.

• Similarly for the other basic set constructions.

In order to obtain a model of a universe closed under some other principles, we will in later sections of this article add to U^{α} additional elements. In this article, these closure principles will always be the closure under certain universe constructions.

We show that (U^{<I}, T^{<I}) is a model of the standard universe. In fact we show a more general theorem:

Theorem 3.3. Assume (U^{α}, T^{α}) is defined as above, except that one adds possibly additional elements to U^{α} and defines T^{α}(s) for each such additional element s, and that this is done in such a way that Assumption 3.2 is fulfilled. Let κ be a recursively inaccessible ordinal. Then (U^{<κ}, T^{<κ}) is closed under the basic set constructions.

Proof: First one observes that if (A, B) ∈ [[ Fam ]](Set) and A, B ∈ L′_{α}, then [[ Σ ]](A, B), [[ Π ]](A, B) ∈ L′_{α+2} and [[ W ]](A, B) ∈ L′_{α^{+}+1}. Similar properties hold for [[ + ]] and [[ Id ]] (making use of α + 2).

Now, if I is a recursively inaccessible ordinal, then (U^{<I}, T^{<I}) is closed under N̂_{n}, N̂, Σ̂, Π̂, Ŵ, ˆ+, Îd: We consider only the most difficult case Ŵ. First we show a small Lemma:

Lemma 3.4. Assume Assumption 3.2 is fulfilled. Let κ be an admissible ordinal and

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](U^{<κ}, T^{<κ}) .

Then there exists an α < κ such that

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](U^{<α}, T^{<α}) .

Proof of the Lemma: We have ⟨a, a′⟩ ∈ U^{<κ}, and since κ is a limit ordinal, it follows ⟨a, a′⟩ ∈ U^{<α_{0}} for some α_{0} < κ. Furthermore, T^{<α_{0}}(a) ∈ L′_{α_{0}}, and for all ⟨x, x′⟩ ∈ T^{<α_{0}}(a) there exists α_{1} < κ such that ⟨b(x), b′(x′)⟩ ∈ U^{<α_{1}}. Since “u ∈ U^{β}” is Σ_{1}, the unbounded quantifier in this Σ_{1}-formula can be relativised to L_{κ} for β < κ (by Assumption 3.2 (e)), T^{<α_{0}}(a) ∈ L′_{α_{0}}, and κ is admissible, we can find a uniform α_{1} for this. Now let α := max{α_{0}, α_{1}}.

We continue with the main proof. Assume ⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](U^{<I}, T^{<I}). Then by Lemma 3.4 we find a β such that ⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](U^{<β}, T^{<β}). We have T^{<I}(a) = T^{<β}(a) ∈ L′_{β}, T^{<I}(b(x)) = T^{<β}(b(x)), therefore (λx ∈ T^{<I}(a).T^{<I}(b(x))) ∈ L′_{β+1}, therefore [[ W ]](T^{<I}(a), λx ∈ T^{<I}(a).T^{<I}(b(x))) ∈ L′_{β^{+}+1}. Therefore ⟨Ŵ(a, b), Ŵ(a′, b′)⟩ ∈ U^{β^{+}+2} ⊆ U^{<I}.

One obtains a model of the type theory ML_{W}U in KPI^{+} as follows. We have modelled all the ingredients already, and need only to make sure that the constructions can be carried out in KPI^{+}. Let κ_{n} be the nth admissible above I. First, one observes, that [[ U ]] ∈ L′_{I+1}, for x ∈ Flat([[ U ]]) we have [[ T_{U} ]](x) ∈ L′_{I}, and for ⟨x, x′⟩ ∈ [[ U ]] we have [[ T_{U} ]](x) = [[ T_{U} ]](x′). Therefore one defines o(U) := I + 1, o(T_{U}(s)) := I. For all other set constructions we have seen that if the maximum of the ordinals of the subterms is α, then the ordinal of the term itself is α + 2 or α^{+} + 1. Therefore we obtain that for any set term A there exists an n such that o(A) ≤ κ_{n} and therefore for all ρ [[ A]]_{ρ} ∈ L′_{κ_{n}}. One sees now that we can interpret all sets in KPI^{+}, and can show that this model is sound with respect to the above mentioned correctness conditions. So we have given a sketch of the following theorem of which a detailed proof can be found in [30]; see as well [32]; Griffor and Rathjen have shown related results in [17]:

Theorem 3.5.

(a) ML_{W}U can be modelled in KPI^{+}.

(b) |ML_{W}U| ≤ |KPI^{+}|.

(c) The previous statements hold as well if we replace intensional by extensional equality.

In the other direction, we have developed in [34] (see as well our PhD thesis [30], and the overview articles [33, 36]; Rathjen and Griffor have obtained related results in [17]) a well-ordering proof which shows the other direction, namely:

Theorem 3.6. (a) |ML_{W}U| = |KPI^{+}|

(b) The previous statements hold as well if we replace intensional by extensional equality.

4 Palmgren’s Super-Universe and Recursively Hyperinaccessibles

4.1 Definition of the Super-Universe

The first substantial step beyond the type theory ML_{W}U was the introduction of a hierarchy of finitely many universes by Per Martin-Löf. We won’t cover this extension in this article, and will instead move to the next step, namely the super-universe, as introduced by Erik Palmgren. He introduced a superuniverse operator which takes as arguments a family of sets, and forms a universe containing this family of sets. (More precisely, since we are using universes à la Tarski, the resulting universe contains a code for the index set and codes for each element of the family. The decoding function maps these codes to the corresponding sets.) The super-universe is defined as a universe closed under this operator.

In order to introduce this in detail, let us first introduce some notions:

Definition 4.1. (Refers to the full logical framework).

(a) The type of families of sets is defined (using the full logical framework) as

Fam(Set) := (X : Set) × (X → Set) .

(b) Let ⟨U, T⟩ ∈ Fam(Set). The family of sets internal to (U, T) (or internal family of sets in (U, T)) is the set of families of sets in U, indexed over elements of U:

IFam(U, T) := (x : U) × (T(x) → U) .

(c) Let ⟨U, T⟩ ∈ Fam(Set). The lifting of an element a : IFam(U, T) to an element of Fam(Set) is defined as

T[a] := ⟨T(π_{0}(a)), (x)T(π_{1}(a)(x))⟩ : Fam(Set) .

Palmgren first introduced the super-universe operator

SU : Fam(Set) → Fam(Set) .

SU(C) is a universe (U′, T′) closed under the standard set constructions and containing C. This means that if C = ⟨A, B⟩, then U′ contains

• a code â for A, i.e. T′(â) = A,

• and for a : A a code b̂(a) for B(a), i.e. T′(b̂(a)) = B(a).

The next step was to introduce the super-universe as a universe (V, T_{V}), which is as usual closed under the standard set constructions and which reflects the super-universe operator: if a : IFam(V, T_{V}), then V contains codes ⟨Û_{a}, (x)T̂_{a}(x)⟩ for SU(T_{V}[a]), which means

⟨Û_{a}, (x)T̂_{a}(x)⟩ : IFam(V, T_{V}) , T_{V}[⟨Û_{a}, (x)T̂_{a}(x)⟩] = SU(T_{V}[a]) .

We will in the following present a version, in which (T(Û_{a}), T̂_{a}) is a recursive subuniverse of (V, T_{V}). Furthermore, we will define the universe operator only restricted to elements of IFam(V, T_{V}) (which will be written as U_{a,b} for ⟨a, b⟩ : IFam(V, T_{V})). We uncurry SU and obtain the following rules:

V : Set  \begin{matrix}a : V \\ T_{V}(a) : Set \end{matrix}
a : V  b : T_{V}(a) → V
U_{a,b} : Set
\begin{aligned}a : V & b : T_{V}(a) → V \\ & Û_{a,b} : V \end{aligned}  T_{V}(Û_{a,b}) = U_{a,b}
a : V  b : T_{V}(a) → V  c : U_{a,b}
T̂_{U,a,b}(c) : V

Let T_{U,a,b}(x) := T_{V}(T̂_{U,a,b}(x)) : Set.

(V, T_{V}) is a universe, which means it is closed under the basic set constructions. The codes are written as N̂_{V}, Σ̂_{V}, etc.

One demands for a : V, b : T_{V}(a) → V that (U_{a,b}, T̂_{U,a,b}) is a recursive subuniverse of (V, T_{V}), which means as indicated in Sect. 3 that U_{a,b} is closed under constructors for forming codes for the standard set constructions like N̂_{U,a,b}, Σ̂_{U,a,b}, etc., and that T̂_{U,a,b} decodes them as the corresponding codes in V, e.g. T̂_{U,a,b}(N̂_{U,a,b}) = N̂_{V}.

Furthermore, U_{a,b} contains codes for a, b, which means that one has the following rules:

â_{a,b} : U_{a,b}  T̂_{U,a,b}(â_{a,b}) = a
b̂_{a,b} : T_{V}(a) → U_{a,b}  T̂_{U,a,b}(b̂_{a,b}(c)) = b(c)

Let ML_{W} + (Superuniv) be the type theory consisting of the rules of the small logical framework, the basic set constructions, and the rules for V, T_{V}, U_{a,b}, Û_{a,b}, T̂_{U,a,b} as above.

In this type theory, one can define using the elimination rules for N a hierarchy of universes Û′_{n} : V by

Û′_{0} = Û_{N̂_{0},(x)N̂_{0}}  Û′_{S(n)} = Û_{N̂_{1},(n)Û′_{n}} .

In a next step one can define a universe containing this hierarchy of universes, namely U_{N̂,(n)Û′_{n}}.

This is the first step towards forming a transfinite hierarchy of universes: Assume any well-founded relation (R, ≺) such that (R, ≺) can be represented in (V, T_{V}), i.e. such that there exist R̂ : V and ˆ≺ : R → R → U such that T_{V}(R̂) = R and T_{V}(ˆ≺(r, r′)) =≺ (r, r′). Assume the well-foundedness of (R, ≺) can be shown in this type theory. Then we can define a hierarchy of universes Û′′_{α} for α ∈ R such that Û′′_{α} contains codes for Û′′_{β} for β ≺ α.

4.2 A Model of the Super-Universe

ML_{W} + (Superuniv) has strength (KP + (hyper − inacc))^{+}, where (KP + (hyper − inacc))^{+} is Kripke-Platek set theory plus the existence of a recursively hyper-inaccessible set plus finitely many admissibles (i.e. for Metaeach n we have n admissibles) above it, which is proof theoretically equivalent to KPl^{r} plus the existence of a recursively hyper-inaccessible set.

Here a recursively hyper-inaccessible set is an admissible set a such that for all x ∈ a there exists a y ∈ a such that x ∈ y and y is recursively inaccessible. A recursively hyper-inaccessible ordinal is an admissible ordinal HI such that

∀α ∈ HI.∃β ∈ HI.α ∈ β ∧ Inacc(β) ,

where Inacc(β) means that β is a recursively inaccessible ordinal.

The precise formulation of (KP + (hyper − inacc))^{+} is similar to KPI^{+}, except that one replaces “inaccessible” by “hyper-inaccessible”.

An upper bound for the strength of ML_{W} + (Superuniv) can be obtained by modelling it in (KP + (hyper − inacc))^{+}. We will give in the following a sketch of the model, full details will be presented in a future paper.

The basic construction is as in Sect. 2. As pointed out there, in [[ Term ]] we omit arguments of the constructors of V, U_{a,b} used for type checking only, except in â, b̂. (By “used for type checking only” we mean that they have no computational content – in an equality rule of the form T̃(c) = d, where T̃ = T_{V} or T̃ = T̂_{U,a,b}, d will not depend on those parameters.) For instance, we have a constant N̂ ∈ [[ Term ]] and interpret

[[ N̂_{V} ]]_{ρ} = [[ N̂_{U,a,b}]]_{ρ} = N̂ ,

similarly for N̂_{n}, Σ̂, Π̂, ˆ+, Îd, Ŵ. Û, T̂_{U}, â and b̂ will depend on a, b. We will in the model identify â_{a,b} with a, b̂_{a,b} with b, and T̂_{U,a,b}(c) with c as expressed by the reduction rules

\begin{matrix}â_{a,b} & ⟶ & a \\ b̂_{a,b}(c) & ⟶ & b(c) \\ T̂_{U,a,b}(c) & ⟶ & c \end{matrix}

As for standard universes, the super-universe is interpreted, by defining first by induction on α sets

(V^{α}, T^{α}) ∈ [[ Fam ]](Set)

such that

α < β → (V^{α}, T^{α}) ≤ (V^{β}, T^{β}) .

As for all models of universes in this article, we add to V^{α} the codes for standard set constructors applied to arguments, if the elements of the universe they refer to are already in V^{<α} and the sets added are in L′_{α}. Additionally, whenever there exists a β such that β + 1 < α and V^{<β} is closed under all universe constructions, and such that

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](V^{<β}, T^{<β}) ,

then

⟨Û_{a,b}, Û_{a′,b′}⟩ ∈ V^{α}

and we define

T^{α}(Û_{a,b}) := V^{<β}

for the minimal β, which has the mentioned closure properties. The construction fulfils Assumption 3.2 with U replaced by V.

Let HI be the least recursively hyper-inaccessible ordinal. Then one interprets

[[ V ]] := V^{<HI} ,
[[ T_{V} ]] := T^{<HI} ,
[[ U_{a,b}]]_{ρ} := T^{<HI}([[ Û_{a,b}]]_{ρ}) .

Note that this model construction won’t admit elimination rules for U_{a,b}, since it is not interpreted as the least set closed under a, b and the basic set constructions – the V^{β′} chosen above might contain elements of the form Û_{a′,b′}, which have been added, since the model of V needs to be closed under Û, but which are not elements of the least subuniverse closed under a, b and the standard set constructions. One could modify the above model in order to admit elimination rules: Then one would try to form at each stage α the least subset of V^{<α} closed under the universe constructions and containing a and b(x) for x ∈ Flat(T^{<α}(a)). If this definition succeeds and the least such set is A, one would add Û_{a,b} to V^{α} and define T^{α}(Û_{a,b}) := A.

We have to verify that V^{<HI} has the necessary closure properties of the super-universe. Since HI is a recursively inaccessible, V^{<HI} will be closed under universe constructions as before. V^{<HI} is as well closed under (a, b)Û_{a,b}: Assume

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](V^{<HI}, T^{<HI}) .

By the admissibility of HI it follows using Lemma 3.4 (note that we observed above that Assumption 3.2 is fulfilled)

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](V^{<α}, T^{<α})

for some α < HI. Since HI is a recursively hyper inaccessible, there exists a recursively inaccessible ordinal α < κ < HI. V^{<κ} will be closed under the universe constructions and

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](V^{<κ}, T^{<κ}) ,

therefore

⟨Û_{a,b}, Û_{a′,b′}⟩ ∈ V^{κ+2} ⊆ V^{<HI} .

That [[ U_{a,b}]]_{ρ} has the closure properties needed in order to interpret U_{a,b} follows by the construction.

The remaining construction is as for any standard model of type theory, i.e. we interpret the constructions of the small logical framework and the basic set constructions on top of U. As for ML_{W}U, we need < ω many admissibles in order to interpret W-types built on top of V^{<HI}, therefore finite approximations of the type theory can be interpreted into Kripke Platek set theory plus one recursively hyper-inaccessible and finitely many admissibles (i.e. for Meta-each n we have n admissibles) above it. So we have given the essence of a proof of the following theorem:

Theorem 4.2.

(a) We can model ML_{W} + (Superuniv) in (KP + (hyper − inacc))^{+}.

(b) |ML_{W} + (Superuniv)| ≤ |(KP + (hyper − inacc))^{+}|

(c) The previous statements hold as well if we replace intensional by extensional equality.

In order to obtain the precise proof theoretic strength, one has to carry out a well-ordering proof in order to obtain

|ML_{W} + (Superuniv)| ≥ |(KP + (hyper − inacc))^{+}| .

We note that if one adds as in Palmgren’s original type theory the full universe operator SU : Fam(Set) → Fam(Set), one obtains a slightly stronger theory.

Formulated without the full logical framework, in this type theory one has depending on A : Set and x : A ⇒ B : Set the set U(A, (x)B) : Set and decoding function

u : U(A, (x)B) ⇒ T(A, (x)B, u) : Set .

(U(A, (x)B), T(A, (x)B)) is a universe containing codes for A and B[x := a]. Now one can replace in the type theory for the super universe the rules for U_{a,b}, T_{U,a,b} and defines

U_{a,b} := U(T_{V}(a), (x)T_{V}(b(x))) ,
T_{U,a,b}(c) := T(T_{V}(a), (x)T_{V}(b(x)), c) .

U_{a,b} is now an inductive subuniverse of V, so T̂_{U,a,b} is a constructor of V with equality rule T_{V}(T̂_{U,a,b}(c)) = T_{U,a,b}(c). In this theory one can apply the superuniverse operator as well to V itself, and to elements formed from it. However, only finite nestings of the super-universe operator are possible. The modelling of one application of the super-universe to arguments (A, B) requires one recursively inaccessible above max{o(A), o(B)}. The modelling of V requires one recursively hyper-inaccessible, so in total one needs for Palmgren’s original type theory one recursively hyper-inaccessible ordinal and finitely many recursively inaccessible ordinals (i.e. for Meta-each n we have n recursively inaccessible ordinals) above it.

5 The Mahlo Universe

5.1 Definition of the Mahlo Universe

Once one has defined the super-universe, one can move to a hyper-universe by forming a universe U^{2} with decoding function T^{2}, such that for any family of sets (a, b) internal to (U^{2}, T^{2}) there exists a super-universe U_{a,b}^{1} and an element Û_{a,b}^{1} in V, such that T_{V}(Û_{a,b}^{1}) = U_{a,b}^{1}, where U_{a,b}^{1} contains codes which decode as a, b as before. So we have a decoding function T̂_{a,b}^{1} : U_{a,b}^{1} → U^{2}, and define T_{a,b}^{1} := T^{2} ∘ T̂_{a,b}^{1}. U_{a,b}^{1} is closed under the standard universe constructions. That U_{a,b}^{1} is a super-universe means, that for any family of sets (c, d) internal to (U_{a,b}^{1}, T_{a,b}^{1}) there exists a subuniverse U_{a,b,c,d}^{0} of U_{a,b}^{1} which contains codes decoding as c, d, is closed under the standard universe constructions, and which is represented as a code in U_{a,b}^{1}.

One could define now hyper^{α}-super-universes, but we won’t spell this out in this article. The construction is similar to the step from a Mahlo-universe to a hyper^{α}-Mahlo universe, which will be discussed in the follow-up article [37].

We note that E. Palmgren [23] has introduced higher order universes. In those universes, the lowest level is a universe, the next level is a universe of universe operators, the next level is a universe of operators on universe operators, etc. E. Palmgren added rules expressing the closure of higher order universes under the application of a universe operator from the next level. It is conjectured that E. Palmgren’s universe reaches the strength of KPM, which is slightly below the strength of the Mahlo universe. We will not investigate this construction any further (see the remark in the introduction that Palmgren’s universe contains a Mahlo universe in disguise).

We will investigate in which sense the hyper^{α}-super-universes are universes which for specific operators f on families of sets internal to it contains a universe internal to it, which is closed under f, and in which sense the Mahlo universe to be introduced generalises this.

Definition 5.1. (Assuming the full logical framework).

(a) An operator on families of sets is a function f : Fam(Set) → Fam(Set).

(b) Let ⟨U, T⟩ : Fam(Set). An operator on families of sets internal to (U, T) is a function f : IFam(U, T) → IFam(U, T).

(c) Let ⟨A, B⟩, ⟨A′, B′⟩ : Fam(Set). Assume elimination of + into Set. Then

⟨A, B⟩ ∪_{Fam(Set)} ⟨A′, B′⟩ := ⟨C, D⟩

where

C := (A + N_{1}) + (A′ + N_{1})

and D is such that (remember that A_{0}^{1} is the canonical element of N_{1})

D(inl(inl(a))) = B(a) , D(inl(inr(A_{0}^{1}))) = A ,
D(inr(inl(a′))) = B′(a′) , D(inr(inr(A_{0}^{1}))) = A′ .

The super-universe operator SU takes A : Fam(Set) and forms a universe closed under the operator (X)A : Fam(Set) → Fam(Set). The super-universe is a universe which is closed under the super-universe operator SU. One can define now a hyper-universe operator HU, which takes A : Fam(Set) and forms a super-universe closed (X)A. One obtains essentially the same set by taking a universe closed under (X)SU(X) ∪_{Fam(Set)} A (assuming this is definable). Then one can form a hyper^{2}-universe operator, a universe closed under it etc.

The step towards the Mahlo universe is now to form a universe (V, T_{V}) such that for any operator on families of sets internal to (V, T_{V}) there exists a universe, which is closed under this operator and represented in (V, T_{V}). So for any f : IFam(V, T_{V}) → IFam(V, T_{V}) there exists a subuniverse (U_{f}, T_{U,f}) of V, closed under f and represented as an element Û_{f} in V.

Spelled out without using the full logical framework, we obtain the following rules:

• We have the rules of the small logical framework and of the basic set constructions.

• We have rules expressing that (V, T_{V}) is a universe closed under the basic set constructions. The constructors for the codes for these set constructions will be denoted by N̂_{V}, Σ̂_{V}, etc.

• We have that for every operator f on families of sets internal to (V, T_{V}) there is a subuniverse U_{f} closed under it. We split f into two components, uncurry it, and obtain the following rules:

f : (a : V, b : T_{V}(a) → V) → V  g : (a : V, b : T_{V}(a) → V, T_{V}(f(a, b)) → V
U_{f,g} : Set

• We have rules expressing that U_{f,g} is a recursive subuniverse closed under the standard set constructions. So we have the decoding function

T̂_{U,f,g} : U_{f,g} → V

and define

T_{U,f,g}(a) := T_{V}(T̂_{U,f,g}(a)) : Set .

The codes for the basic set constructions will be denoted by N̂_{U,f,g}, Σ̂_{U,f,g}, etc.

• We have rules expressing that (U_{f,g}, T_{U,f,g}) is closed under f and g:

f̂_{f,g} : (a : U_{f,g}, b : T_{U,f,g}(a) → U_{f,g}) → U_{f,g}
T̂_{U,f,g}(f̂_{f,g}(a, b)) = f(T̂_{U,f,g}(a), T̂_{U,f,g} ∘ b).

ĝ_{f,g} : (\begin{matrix}a : U_{f,g}, \\ b : T_{U,f,g}(a) → U_{f,g}, \\ T_{V}(f(T̂_{U,f,g}(a), T̂_{U,f,g} ∘ b))) \end{matrix}

→ U_{f,g}
T̂_{U,f,g}(ĝ_{f,g}(a, b, c)) = g(T̂_{U,f,g}(a), T̂_{U,f,g} ∘ b, c).

• And finally, we have the rule that V contains a code for U_{f,g}. As P. Martin-Löf observed this is the rule which makes the Mahlo universe so strong

– having just subuniverses closed under f, g doesn’t add any strength to ML_{W}U.

f : (a : V, b : T_{V}(a) → V) → V  g : (a : V, b : T_{V}(a) → V, T_{V}(f(a, b)) → V
Û_{f,g} : V
T_{V}(Û_{f,g}) = U_{f,g}

We call the resulting type theory ML_{W} + (Mahlo).

5.2 A Model of the Mahlo Universe

ML_{W} + (Mahlo) has strength (KPM)^{+}, where (KPM)^{+} is KPω plus the existence of one recursively Mahlo set plus finitely many admissibles above it (i.e. for Meta-each n we have a chain of n admissibles above it), which is equivalent to KPl^{r} plus the existence of one recursively Mahlo set.

Here a recursively Mahlo set is an admissible set a_{M} such that

(Mahlo) ∀z⃗ ∈ a_{M}.((∀x ∈ a_{M}.∃y ∈ a_{M}.φ(x, y, z⃗)) → ∃u ∈ a_{M}.Ad(u) ∧ z⃗ ∈ u ∧ (∀x ∈ u.∃y ∈ u.φ(x, y, z⃗)))

for any Δ_{0}-formula φ(x, y, z⃗) such that FV(φ(x, y, z⃗)) ⊆ {x, y, z⃗}

A recursively Mahlo ordinal is an ordinal M such that L_{M} is a recursively Mahlo set.

The basic construction of a model of the Mahlo universe is as for the superuniverse: We define by recursion over α approximations (V^{α}, T^{α}) of ([[ V ]], [[ T ]]) by closing it systematically under the basic set constructions, and by adding suitable codes Û_{f,g} to it.

The question is when to add codes Û_{f,g} to the Mahlo universe. In the introduction rule for Û_{f,g}, f, g need to be total functions from families of sets internal to (V, T) to the same kind of families. But we only know this type of total functions, once the definition of [[ V ]] is complete – so in the definition of V^{α} we cannot refer to these total functions. The trick to get around this problem is to add more elements Û_{f,g} to the universe than are actually justified by the introduction rules. We only demand that f, g are total on the subuniverse U_{f,g} itself. So we take f, g to be arbitrary terms. Then we try to form a subuniverse of the current approximation V^{α} of [[ V ]], which is closed under f and g. If we succeed, we add Û_{f,g} to [[ V ]] and define [[ T_{V} ]](Û_{f,g}) as the least such subuniverse.

If we assume now total functions f, g from families of sets internal to (V^{<M}, T^{<M}) into itself, then there is at least one subuniverse of (V^{<M}, T^{<M}) closed under f, g, namely V^{<M} itself. Then we will use the fact that M is recursively Mahlo in order to find such a subuniverse inside some (V^{<α}, T^{<α}) for some α < M, and that therefore Û_{f,g} is in V^{<α+1} ⊆ V^{<M}.

As for the super-universe, we simplify this construction slightly and don’t search for the least subuniverse closed under f and g, but only for the least β such that V^{β} is closed under f and g.

More precisely we proceed as follows: As in the model for the super-universe, we omit in the terms of the model the arguments needed in N̂, Σ̂, etc. (but not in f̂, ĝ) for type-checking purposes only, so for instance

[[ N̂_{V} ]]_{ρ} := [[ N̂_{U,f,g}]]_{ρ} := N̂ .

We obtain essentially the same reduction rules for T̂_{U,f,g} as the reduction rules for T̂_{U,a,b} in case of the super-universe. Furthermore, we have the reductions

\begin{matrix}f̂_{f,g}(a, b) & ⟶ & f(a, b) , \\ ĝ_{f,g}(a, b, c) & ⟶ & g(a, b, c) . \end{matrix}

As for the super-universe, we form (V^{α}, T^{α}) ∈ [[ Fam ]](Set) by closing it under the standard set constructions and by adding codes for suitable subuniverses as defined below. We will then interpret [[ V ]] = V^{<M}, [[ T_{V} ]] = T^{<M}.

Whereas the super-universe was closed under Û_{a,b} for ⟨a, b⟩ ∈ [[ IFam ]](V^{<α}, T^{<α}), we close the approximation V^{α} of the Mahlo universe under Û_{f,g}, where f, g form the two components of a function

[[ IFam ]](V^{<α}, T^{<α}) [[ →]] [[ IFam ]](V^{<α}, T^{<α}) .

We call such a pair ⟨f, g⟩ an operator on families of sets internal to (V^{<α}, T^{<α}). More precisely, we introduce the following definition, where we first define a notion for the two components of an operator on families of sets internal to (A, B), and then define what it means to be an operator on families of such sets as the conjunction of the two:

Definition 5.2. Let ⟨A, B⟩ ∈ [[ Fam ]](Set).

(a) [[ IFamOper ]]_{0}(A, B) := \begin{matrix}(x ∈ A) \\ [[ →]](B(x) [[ →]] A) \\ [[ →]]A . \end{matrix}

(b) Assume f ∈ Flat([[ IFamOper ]]_{0}(A, B)). Then

[[ IFamOper ]]_{1}(A, B, f) := \begin{matrix}(x ∈ A) \\ [[ →]](y ∈ (B(x) [[ →]] A)) \\ [[ →]]B(f(x, y)) \\ [[ →]]A . \end{matrix}

(c) The set of operators on families of sets internal to ⟨A, B⟩ is given as

[[ IFamOper ]](A, B) :=

\{⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ ([[ Term ]]^{2})^{2} | \begin{matrix}⟨f, f′⟩ ∈ [[ IFamOper ]]_{0}(A, B)∧ \\ ⟨g, g′⟩ ∈ [[ IFamOper ]]_{1}(A, B, f)\} . \end{matrix}

With this notation, the addition of Û_{f,g} to V^{α} is defined as follows:

Assume f, f′, g, g′ ∈ [[ Term ]]. Assume α < M and β such that β + 1 < α and such that V^{<β} is closed under all universe constructions. Assume that

⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]](V^{<β}, T^{<β})

Let β be minimal that this property holds. Then

⟨Û_{f,g}, Û_{f′,g′}⟩ ∈ V^{α} ,

and we define

T^{α}(Û_{f,g}) := V^{<β} .

The construction fulfils Assumption 3.2 with U replaced by V. Now define

[[ U ]]_{ρ} := V^{<M} ,
[[ T_{V}(c) ]]_{ρ} := T^{<M}([[ c]]_{ρ}) ,
[[ U_{f,g}]]_{ρ} := T^{<M}(Û_{[[ f]]_{ρ},[[ g]]_{ρ}}) .

where M is the least recursively Mahlo ordinal.

We note that T^{α}(Û_{f,g}) is not defined as a minimal set closed under universe constructions and under f and g. We could have done so by modifying the above definition and trying at stage α to define the least subset of V^{α} closed under f and g and the standard universe constructions. If this succeeds, this subset is independent of α (provided α is big enough so that this subset lies inside V^{α}) and we could have interpreted T^{α}(Û_{f,g}) as this set. This would interpret elimination rules for U_{f,g} as well. But since elimination rules for U_{f,g} don’t add any proof theoretic strength, and such a model construction would be more complicated, we use the original approach.

We have to verify that V^{<M} has the necessary closure properties of the Mahlo universe. Every recursively Mahlo ordinal is recursively inaccessible, therefore V^{<M} will be closed under universe constructions as before. V^{<M} is as well closed under (f, g)Û_{f,g}: Assume f, f′, g, g′ ∈ [[ Term ]]. Assume

⟨f, f′⟩ ∈ [[ (x : V, y : T_{V}(x) → V) → V ]] ,
⟨g, g′⟩ ∈ [[ (x : V, y : T_{V}(x) → V, T_{V}(z(x, y)) → V ]]_{[z=f]} .

This means

⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]](V^{<M}, T^{<M})

We need to find a κ < M such that V^{<κ} is closed under universe constructions and that the previous conditions hold with M replaced by κ. For being closed under universe constructions it suffices that κ is inaccessible.

We show the following statement (∗): For every β < M there exists a ρ < M such that ρ is admissible, β < ρ and such that

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](V^{<β}, T^{<β})

→ ⟨⟨f(a, b), g(a, b)⟩, ⟨f′(a′, b′), g′(a′, b′)⟩⟩ ∈ [[ IFam ]](V^{<ρ}, T^{<ρ}) .

So assume β < M and

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](V^{<β}, T^{<β}) .

Then

⟨⟨f(a, b), g(a, b)⟩, ⟨f′(a, b), g′(a, b)⟩⟩ ∈ [[ IFam ]](V^{<M}, T^{<M}) .

By Lemma 3.4 there exists a ρ < M such that

⟨⟨f(a, b), g(a, b)⟩, ⟨f′(a, b), g′(a, b)⟩⟩ ∈ [[ IFam ]](V^{<ρ}, T^{<ρ}) .

Furthermore, using the fact that every recursively Mahlo ordinal is recursively inaccessible, we can achieve β < ρ admissible. This shows (∗).

The statement (∗) can be expressed as a Π_{2}-formula, i.e. a formula of the form

∀β < M.∃ρ < M.φ(β, ρ) ,

where φ is Δ_{0}.

By M being recursively Mahlo we obtain the existence of an admissible κ < M such that

∀β < κ.∃ρ < κ.φ(β, ρ) .

Since ρ is an admissible > β, it follows that κ is recursively inaccessible, therefore (V^{<κ}, T^{<κ}) is closed under the basic set constructions. Furthermore if

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](V^{<κ}, T^{<κ}) ,

then by Lemma 3.4 there exists a β < κ such that

⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](V^{<β}, T^{<β}) .

Therefore there exists a ρ < κ such that

⟨⟨f(a, b), g(a, b)⟩, ⟨f′(a′, b′), g′(a′, b′)⟩⟩ ∈ [[ IFam ]](V^{<ρ}, T^{<ρ}) ⊆ [[ IFam ]](V^{<κ}, T^{<κ}) .

This means that V^{<κ} is a candidate for the interpretation of ⟨Û_{f,g}, Û_{f′,g′}⟩, and therefore

⟨Û_{f,g}, Û_{f′,g′}⟩ ∈ V^{κ+2} ⊆ V^{<M} .

That [[ U_{f,g}]]_{ρ} has the closure properties needed in order to interpret U_{f,g} follows by the construction.

The remaining steps are as for the model of simple ML_{W}U, i.e. we need < ω many admissibles in order to interpret the basic set constructions on top of V, T_{V}. Therefore the type theory can be interpreted in Kripke Platek set theory plus one recursively Mahlo ordinal and finitely many admissibles (i.e. for Meta-each n we have n admissibles ) above it. So we have given the essence of a proof of the following theorem:

Theorem 5.3.

(a) We can model ML_{W} + (Mahlo) in (KPM)^{+}.

(b) |ML_{W} + (Mahlo)| ≤ |(KPM)^{+}|

(c) The previous statements hold as well if we replace intensional by extensional equality.

By [35] we obtain the other direction and obtain therefore

Theorem 5.4. (a) |ML_{W} + (Mahlo)| = |(KPM)^{+}|

(b) The previous statements hold as well if we replace intensional by extensional equality.

References

[1] P. Aczel. The strength of Martin-Löf’s intuitionistic type theory with one universe. In S. Miettinen and J. Väänänen, editors, Proceedings of the symposium on Mathematical Logic (Oulu 1974). Report No. 2, Dept. of Philosophy, Univ of Helsinki, 1977.

[2] T. Arai. Proof theory of theories of ordinals I: Reflecting ordinals. Preprint, 1996.

[3] T. Arai. Proof theory of theories of ordinals II: Σ_{1} stability. Preprint, 1997.

[4] T. Arai. Proof theory of theories of ordinals III: Π_{1} collection. Preprint, 1997.

[5] T. Arai. Ordinal diagrams for Π_{3}-reflection. J. Symbolic Logic, 65(3):1375 – 1394, 2000.

[6] T. Arai. Ordinal diagrams for recursively Mahlo universes. Arch. Math. Logic, 39(5):353 – 391, 2000.

[7] T. Arai. Proof theory for theories of ordinals. I. Recursively Mahlo ordinals. Ann. Pure Appl. Logic, 122(1 – 3):1 – 85, 2003.

[8] T. Arai. Proof theory for theories of ordinals. II. Π_{3}-reflection. Ann. Pure Appl. Logic, 129(1 – 3):39 – 92, 2004.

[9] J. Barwise. Admissible Sets and Structures. An Approach to Definability Theory. Omega-series. Springer, 1975.

[10] M. Benke, P. Dybjer, and P. Jansson. Universes for generic programs and proofs in dependent type theory. Nordic J. of Computing, 10(4):265–289, 2003.

[11] P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525–549, June 2000.

[12] P. Dybjer and A. Setzer. Finite axiomatizations of inductive and inductive-recursive definitions. In Workshop on Generic Programming, Marstrand, Sweden, 18 June 1998. http://www.cs.ruu.nl/people/johanj/programme wgp98.html, 1998.

[13] P. Dybjer and A. Setzer. A finite axiomatization of inductive-recursive definitions. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129–146. Springer, April 1999.

[14] P. Dybjer and A. Setzer. Indexed induction-recursion. In R. Kahle, P. Schroeder-Heister, and R. Stärk, editors, Proof Theory in Computer Science, volume 2183 of Lecture Notes in Computer Science, pages 93 – 113. Springer, 2001.

[15] P. Dybjer and A. Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124:1–47, 2003.

[16] P. Dybjer and A. Setzer. Indexed induction-recursion. 65 pp. To appear in Journal of Logic and Algebraic Programming, 2006.

[17] E. Griffor and M. Rathjen. The strength of some Martin-Löf type theories. Arch. math. Logic, 33:347 – 385, 1994.

[18] M. Hofmann. Syntax and semantics of dependent types. In A. M. Pitts and P. Dybjer, editors, Semantics and logics of computation, pages 79 – 130, Cambridge, 1997. Cambridge University Press.

[19] G. Jäger. Theories for Admissible Sets: A Unifying Approach to Proof Theory. Bibliopolis, Naples, 1986.

[20] P. Martin-Löf. Intuitionistic type theory. Bibliopolis, Naples, 1984.

[21] B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s type theory. An Introduction. Oxford University-Press, Oxford, 1990.

[22] B. Nordström, K. Petersson, and J. M. Smith. Martin-löf’s type theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of logic in computer science, Vol. 5, pages 1 – 37. Oxford Univ. Press, 2000.

[23] E. Palmgren. On universes in type theory. In G. Sambin and J. Smith, editors, Twenty five years of constructive type theory, pages 191 – 204, Oxford, 1998. Oxford University Press.

[24] W. Pohlers. Subsystems of set theory and second order number theory. In S. R. Buss, editor, Handbook of Proof Theory, pages 209 – 335. Elsevier, 1998.

[25] A. Ranta. Type-theoretical Grammar. Clarendon Press, Oxford, 1995.

[26] M. Rathjen. Proof-theoretical analysis of KPM. Arch. math. Logic, 30:377 – 403, 1991.

[27] M. Rathjen. Proof theory of reflection. Ann. Pure Appl. Logic, 68:181 – 224, 1994.

[28] M. Rathjen. Recent advances in ordinal analysis: Π_{2}^{1}-CA and related systems. Bulletin of Symbolic Logic, 1:468 – 485, 1995.

[29] M. Rathjen. An ordinal analysis of parameter free Π_{2}^{1}-comprehension. Arch. Math. Log., 44(3):263 – 362, April 2005.

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

[31] A. Setzer. A model for a type theory with Mahlo Universe. 10pp. Draft, available at http://www.cs.swan.ac.uk/∼/articles/uppermahlo.pdf, 1996.

[32] A. Setzer. An upper bound for the proof theoretical strength of Martin-Löf Type Theory with W-type and one Universe. 33pp. Draft, available at http://www.cs.swan.ac.uk/∼/articles/1papdiss.dvi or .ps or .pdf, 1996.

[33] A. Setzer. An introduction to well-ordering proofs in Martin-Löf’s type theory. In G. Sambin and J. Smith, editors, Twenty-five years of constructive type theory, pages 245 – 263, Oxford, 1998. Clarendon Press.

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

[35] A. Setzer. Extending Martin-Löf type theory by one Mahlo-universe. Arch. Math. Log., 39:155 – 181, 2000.

[36] A. Setzer. Proof theory of Martin-Löf type theory – an overview. Mathematiques et Sciences Humaines, 42 année, n^{o}165:59 – 99, 2004.

[37] A. Setzer. Universes in type theory part II – Π_{3}-reflection. In preparation, 2005.

[38] S. G. Simpson. Subsystems of second-order arithmetic. Springer, 1999.

[39] A. Troelstra and D. v. Dalen. Constructivism in Mathematics. An Introduction, Vol. II. North-Holland, Amsterdam, 1988.