Universes in Type Theory Part II – Autonomous Mahlo

Anton Setzer^{∗}

20 December 2009

Abstract

We introduce the autonomous Mahlo universe which is an extension of Martin-Löf type theory which we consider as predicatively justified and which has a strength which goes substantially beyond that of the Mahlo universe, which is before writing this paper the strongest predicatively justified published extension of Martin-Löf type theory. We conjecture it to have the same proof theoretic strength as Kripke-Platek set theory extended by one recursively autonomous Mahlo ordinal and finitely many admissibles above it. Here a recursively autonomous Mahlo universe ordinal is an ordinal κ which is recursively hyper^{α}-Mahlo for all α < κ. We introduce as well as intermediate steps the hyper-Mahlo and hyper^{α}-Mahlo universes, and give meaning explanations for these theories as well as for the super and the Mahlo universe. We introduce a model for the autonomous Mahlo universe, and determine an upper bound for its proof theoretic strength, therefore establishing one half of the conjecture mentioned before. The autonomous Mahlo universe is the crucial intermediate step for understanding the Π_{3}-reflecting universe, which will be published in a successor of this article and which is even stronger and will slightly exceed the strength of Kripke-Platek set theory plus the principle of Π_{3}-reflection.

1 Introduction

This article is a step in a research programme of the author with the goal of introducing proof theoretically as strong as possible extensions of Martin-Löf type theory, which still can be regarded as predicatively justified. We have three main reasons for following such a research programme:

(1) We hope that this approach gives more insights into the development of ordinal theoretic proof theory. Results in the area of proof theory of impredicative theories are often regarded as very difficult to understand by non-specialists. The theories developed in this programme use crucial ideas from proof theory, while – as we hope – being much easier understandable by a more general audience. We hope this allows more researchers to understand the insights gained by recent proof theoretic developments.

∗Department of Computer Science, Swansea University, 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 EPSRC grant EP/G033374/1.

(2) This research can be seen as part of a revised Hilbert’s programme. The goal of Hilbert’s original programme was to prove the consistency of theories for formalising mathematical proofs using finitary methods. By Gödel’s second incompleteness theorem we know that such a programme cannot be carried out, except for very weak theories. In ordinal theoretic proof theory the consistency of theories of increasing strength is reduced to the well-foundedness of ordinal notation systems. Using strong extensions of Martin-Löf type theory one is able to prove the well-foundedness of such ordinal notation systems and therefore the consistency of the original theories. This provides a reduction of the consistency of classical theories (mainly fragments of second order logic and fragments of set theory) to constructive theories, which have a philosophical argument for the validity of their theorems. Therefore extensions of Martin-Löf type theory can be regarded as a substitute for Hilbert’s finitary methods.

(3) We hope that by developing such extensions we will discover new data structures. One example where this program has been successful was the discovery of the data type of inductive-recursive definitions ([16, 17, 18, 19]), which was strongly influenced by the Mahlo universe, a first step in this proof theoretic programme. Variants of this data type can be used in the area of generic programming ([12, 15]) and it has similarities with (and possibly influenced) the development of generic extensions of Haskell (polytypic programming, e.g. [25]).

In the article [53], we have introduced type theories of strength Kripke-Platek set theory extended by one recursively inaccessible, one recursively hyperinaccessible and one recursively Mahlo ordinal, respectively, and finitely many admissibles above those ordinals. The type theories considered were Martin-Löf type theory with W-type and one universe, one super universe and one Mahlo universe, respectively. We have as well given basic model constructions in the corresponding extensions of Kripke-Platek set theory, in order to obtain an upper bound for their proof theoretic strength. (For the reader not familiar with Kripke-Platek set theory it suffices to understand these constructions as model constructions in which one uses as little strength as possible from the set theory, in which the models are developed.) Lower bounds for the proof theoretic strength of these theories have been shown in [42, 46, 49].

In this article we introduce a new universe construction into Martin-Löf type theory of expected strength Kripke-Platek set theory plus one recursively autonomous Mahlo ordinal and finitely many admissibles above it. Here a recursively autonomous Mahlo ordinal is an ordinal κ which is recursively hyper^{κ}- Mahlo, or, equivalently, which is recursively hyper^{α}-Mahlo for all α < κ. (See Subsect. 5.2 for details.)

The step from the Mahlo universe to the autonomous Mahlo universe is a very natural step, in which we move from the Mahlo universe to the hyper-Mahlo universe, then to the hyper^{α}-Mahlo universe and then to an autonomous iteration of such universes. It is an important intermediate step before introducing the Π_{3}-reflecting universe, in which the iteration of Mahlo degrees (the Mahlo degree of a hyper^{α}-Mahlo universe would be α) is carried out even further. We plan to introduce the Π_{3}-reflecting universe in a follow up paper.

The step from Mahlo to Π_{3}-reflection follows recent developments in proof theory. After an analysis of (Δ_{2}^{1} − CA) + (BI) or, equivalently, Kripke Platek set theory plus one recursively inaccessible had been carried out, the next step in the development of proof theory was an analysis of Kripke-Platek set theory plus one Mahlo ordinal, carried out independently by Rathjen and Arai (see [33, 34, 36] and [3, 4, 8, 9]). Then both researchers analysed Kripke-Platek set theory plus one Π_{3}-reflecting ordinal ([35, 37] and [3, 4, 7, 10]), which was the crucial stepping stone before analysing theories of strength (Π_{2}^{1} − CA) + (BI) and beyond [38, 39, 40] and [3, 5, 6]. Relationship to the article [53]. This article is a follow-up article of the article [53], in which we introduced type theories with one universe, one super universe, and one Mahlo universe. There, we also gave the basic model construction and a proof of its correctness. However, since the author hasn’t published yet an article laying out the basic infrastructure for forming models of this kind, details about the basic setting (how to form a model for a type theory in Kripke-Platek set theory in general including terms and their reduction rules, and how to interpret the basic set constructions) have not been carried out yet. (They have been carried out in [42] for a type theory with one universe, however that setting, while based on the same principles, was not generic enough to be directly extensible.) The main goal of this article is to introduce the autonomous Mahlo universe and give a model construction with the same level of detail. Full details of the model will be introduced in a follow up article. This article might in fact be more accessible to a general audience than the more detailed model construction to be introduced later.

The model will be carried out in Kripke-Platek set theory plus one recursively autonomous Mahlo ordinal and finitely many admissibles above it. Therefore we obtain an upper bound for the proof-theoretic strength of this universe construction. In order to obtain a lower bound for its strength, we plan to extend our approach to well-ordering proofs for ordinal notation systems based on ordinal systems ([47, 50, 52]) to Kripke-Platek set theory extended by a recursively autonomous Mahlo set. Content. The structure of this article is as follows: In Sect. 2 we repeat the basic notations used in this article. In Sect. 3 we briefly revisit the super universe and the Mahlo universe, and develop meaning explanations for these theories. We will discuss as well the relationship between recursive and inductive subuniverses in this setting. In Sect. 4 we introduce the steps towards the autonomous Mahlo universe as follows: After a short motivation we introduce in Subsect. 4.1 the hyper-Mahlo universe, in Subsect. 4.2 the hyper-n-Mahlo and the hyper^{α}-Mahlo universes, and in Subsect. 4.3 the autonomous Mahlo universe itself. For each of these theories we will develop meaning explanations. We regard these meaning explanation as a predicative justification for the theories introduced. Finally, in Sect. 5 we introduce a model for the autonomous Mahlo universe and give the main proof ideas of its correctness. This way we determine an upper bound for its proof-theoretic strength. Related work. G. Jäger and T. Strahm have introduced in [24] a Π_{3}-reflecting universe in the context of Feferman’s systems of explicit mathematics, which doesn’t require to define an autonomous Mahlo universe first. Because they rely on partial application, their setting is much simpler, but because of its heavy reliance on partial application it is not possible to mimic this in type theory. Their theory seems as well to introduce elements which have no canonical counterpart, so it is not as explicit as demanded in type theory. We will discuss details about this in the follow up paper on the Π_{3}-reflecting universe. Jäger and Strahm carried out as well a full proof theoretic analysis. Since they are working in a Meta-predicative setting (translated to type theory this means that the W-type is omitted), the proof theoretic ordinal they obtained is well below the Bachmann-Howard ordinal, and well below the strength of type theory with the W-type and no universes except for atom.

This work is heavily inspired by M. Rathjen’s and T. Arai’s proof theoretic analysis of Π_{3}-reflection ([35, 37] and [3, 4, 7, 10]) – the Π_{3}-reflecting universe will mimic the ordinal notation systems of that strength. Without their work it would have been difficult to discover the Π_{3}-reflecting universe. Acknowledgements. This research benefited very much from intensive discussions with both T. Arai and M. Rathjen, whose research we deeply admire. It was as well inspired by intensive discussions with Peter Dybjer on inductiverecursive definitions. We would like as well to thank the anonymous referee of a previous version of this article for valuable comments, and my PhD student Frederik Forsberg for careful proof reading.

2 Notations

We will frequently make use of notations and some basic lemmata introduced in [53], but will repeat the most important ones briefly, so that the reader, who is not interested in all details, can read it without having to go through the article [53] first.

• We use mathematical style for application, so we write f(a) for the application of f to a. We write f(a, b) instead of f(a)(b), similarly for longer sequences of applications.

• We will omit equality versions of rules. For instance when we write the rule for the Π-type

A : Set  x : A ⇒ B : Set
(Πx : A.B) : Set

we implicitly introduce as well the rule

A = A′ : Set  x : A ⇒ B = B′ : Set
(Πx : A.B) = (Πx : A′.B′) : Set

The reason that we sometimes need such proper rules is that we for foundational reasons will use only the small logical framework (see below).

• When expressing equality rules, we will usually omit premises. For instance, a rule T(Π̂(a, b)) = Πx : T(a).T(b(x)) needs to be read as

a : U  b : T(a) → U
T(Π̂(a, b)) = Πx : T(a).T(b(x)) : Set

where the premises are what is needed in order to derive T(Π̂(a, b)) : Set and Πx : T(a).T(b(x)) : Set.

• The basic set constructions are the rules for forming the finite sets N_{n}, the set of natural numbers N, the disjoint union A + B, the Π-sets Πx : A.B, the Sigma set Σx : A.B, the W-sets Wx : A.B, and the intensional equality Id(A, a, b). Codes for these constructions as elements of a universe will usually have the form N̂_{i}, N̂, aˆ+b etc.. More details can be found in Sect. 2.3 of [53].

• The elements of N_{n} are denoted by A_{i}^{n} (i = 0, …, n − 1). We write ⊥ for N_{0} (the empty set, which represents the false proposition), ⊤ for N_{1} (which represents the true proposition), triv for A_{0}^{1} (the trivial proof of ⊤), Bool for N_{2}, ff for A_{0}^{2}, tt for A_{1}^{2} (and when using universes write sometimes ˆ⊥, ˆ⊤, { \atop Bool} for N̂_{0}, N̂_{1}, N̂_{2}, respectively).

• The rules for atom consist of the rules x : N_{2} ⇒ atom(x) : Set, atom(tt) = ⊥, atom(ff) = ⊤. Therefore, atom translates a Boolean value into an atomic formula which is provable iff the Boolean value is true, therefore the name atom.

• The small logical framework consists of the dependent function type (x : A) → B and the dependent product (x : A) × B, restricted to Set. λ-abstraction is denoted by (x : A)b or shorter (x)b, and application by f(a). The canonical elements of (x : A) × B are denoted by ⟨a, b⟩ and the projections of these elements are denoted by π_{0}(c), π_{1}(c). See Sect. 2.1 of [53] for details.

• The full logical framework, which is not part of any of the type theories in this article unless stated explicitly, adds a type level Type on top of set.

We have Set : Type and Type contains all elements of Set. Furthermore both Set and Type are closed under the dependent function type and dependent product. See Sect. 2.2 of [53] for details.

• The type of families of sets is defined (using the full logical framework) as Fam(Set) := (X : Set) × (X → Set). (See Def. 4.1 (b) of [53].) If we don’t have the logical framework, then we write

(U, T) : Fam(Set)

for the following rules:

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

• An operator on families of sets is a function h : Oper(Set), where Oper(Set) := Fam(Set) → Fam(Set). (See Def. 5.1 (a) of [53].) By uncurrying it and splitting it into two functions, such an h can be replaced by two functions

f : (X : Set, Y : X → Set) → Set ,
g : (X : Set, Y : X → Set, Z : f(X, Y)) → Set .

We write

f, g : Oper(Set)

for f, g having the types just mentioned. We sometimes abbreviate f, g by h⃗ and write then

h⃗ = f, g : Oper(Set) .

• Assume (U, T) : Fam(Set). The set of internal families of sets in (U, T) is defined as IFam(U, T) := (x : U) × (T (x) → U). (See Def. 4.1 (b) of [53].)

• Assume (U, T) : Fam(Set). An operator on families of sets internal to (U, T) is a function h : IOper(U, T), where IOper(U, T) := IFam(U, T) → IFam(U, T). (See Def. 5.1 (a) of [53].) Such functions can be split into two components and uncurried, then we obtain functions

\begin{aligned}f & : & (a : U, b : T (a) → U) → U , \\ g & : & (a : U, b : T (a) → U, c : T (f(a, b))) → U . \end{aligned}

We write

f, g : IOper(U, T)

for f, g having the type just mentioned. We sometimes abbreviate f, g by h⃗ and write then

h⃗ = f, g : IOper(U, T) .

• A universe is a pair (U, T), where (U, T) : Fam(Set), such that U is closed under the basic set constructions. For instance, closure under Π means that for a : U, b : T(a) → U we have Π̂(a, b) : U, and T(Π̂(a, b)) = Πx : T(a).T(b(x)). For each universe different names for the constructor will be chosen. We will indicate the names if they are used later, otherwise leave those names implicit.

So the rules for a universe are as follows:

rules expressing (U, T) : Fam(Set) ,

Π̂ : (a : U, b : T(a) → U) → U ,

T(Π̂(a, b)) = Πx : T(a).T(b(x)) ,

similarly for the other basic set constructions.

• When defining nested universes, we consider both recursive subuniverses and inductive subuniverses.

– A recursive subuniverse of a universe (V, T_{V}) is given by a set U together with a recursively defined function T̂_{U} : U → V, which determines for every a : U the element in V it corresponds to. Then one defines T_{U}(a) := T_{V}(T̂_{U}(a)). So for every element a : U an element of V corresponding to it needs to have been defined using other rules. We have always closure of (U, T̂_{U}) under the basic set constructions, with constructors named in a usual way e.g. N̂_{U}, Π̂_{U} etc. We will indicate the names of those constructors, if they are used in the following, and indicate the name of T_{U} by saying “(U, T̂_{U}) is a recursive subuniverse of (V, T_{V}) with full decoding T_{U}.” So the rules expressing that (U, T̂_{U}) is a recursive subuniverse of (V, T_{V}) with full decoding T_{U} are as follows (assuming that the constructors for the basic set constructions in V are denoted by N̂_{V}, Π̂_{V} etc.)

U : Set ,  T̂_{U} : U → V ,

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

Π̂_{U} : (a : U, b : T_{U}(a) → U) → U ,

T̂_{U}(Π̂_{U}(a, b)) = Π̂_{V}(T̂_{U}(a), T̂_{U} ∘ b) , rules for the other basic set constructions.

– In an inductive subuniverse, U is defined together with recursively defined function T_{U} : U → Set. Then we define the embedding of U into V, namely T̂_{U} : U → V, as a constructor of V with equality rule T_{V}(T̂_{U}(x)) = T_{U}(x). So when we define an element a of U, we don’t need to have an element in V corresponding to it which is defined using other rules. All we need is to have a way of defining T_{U}(a).

So the rules for (U, T_{U}) being an inductive subuniverse of (V, T_{V}) with embedding T̂_{U} are as follows:

Rules expressing that (U, T_{U}) is a universe,

T̂_{U} : U → V , T_{V}(T̂_{U}(x)) = T_{U}(x) .

A universe (U, T_{U}) can be an inductive subuniverse of several universes, in which case the rules expressing that (U, T_{U}) is a universe occur only once.

– A more detailed discussion on inductive vs. recursive subuniverses can be found in paragraph “Type theories with several universes” in Subsect. 3.1 of [53]. Note that inductive subuniverses result in doubling of codes, for instance T̂_{U}(N̂_{U}) and N̂_{V} are two different codes for the natural numbers, although without universe elimination rules we cannot prove in type theory that they are different. This is the reason why we regard recursive subuniverses as more aesthetic, as long as they don’t create a substantial overhead.

• By “the inductive subuniverse (U, T_{U}) of (V, T_{V}) is represented in V by Û” we mean the following rules

Û : V , T_{V}(Û) = U .

3 The Super Universe and the Mahlo Universe Revisited

In this section we repeat briefly the super universe and the Mahlo universe, which were discussed in more detail in [53].

3.1 Super Universe

The super universe was introduced by Palmgren (see e.g. [30], Sect. 3.) In our setting, a super universe (V, T_{V}) is a universe which contains additionally for every ⟨a, b⟩ : IFam(V, T_{V}), a universe containing ⟨a, b⟩. This means that for every ⟨a, b⟩ : IFam(V, T_{V}), there exists a recursive subuniverse (U_{a,b}, T̂_{U,a,b}) with full decoding T_{U,a,b}, and a code Û_{a,b} : V for it. U_{a,b} is closed under a, b, which means that there are codes â_{a,b} : U_{a,b} for a, and b̂_{a,b} : T_{V}(a) → U_{a,b} for b.

Definition 3.1 The rules for the super universe are as follows:

• Rules for the basic set constructions and the small logical framework.

• Rules expressing that (V, T_{V}) is universe.

Assume in the following a : V, b : T_{V}(a) → V. Then we have the following rules:

• Rules expressing that (U_{a,b}, T̂_{U,a,b}) is a recursive subuniverse of V with full decoding T_{U,a,b}.

• Closure of (U_{a,b}, T_{U,a,b}) under a, b as expressed by 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}(x)) = b(x) .

• U_{a,b} is represented in V:

Û_{a,b} : V , T(Û_{a,b}) = U_{a,b} .

See Subsect. 4.1 of [53] for details.

As I learned from Peter Hancock, who has worked a lot on families of sets (see e.g. [20]), the rules for T̂_{U,a,b}, Û_{a,b} express that the successor of (U_{a,b}, T_{U,a,b}) is a subfamily of (V, T_{V}), where the successor of a family of sets (A, B) is the family of sets (A + ⊤, B′) where B′(inl(a)) = B(a), B′(inr(triv)) = A. Remember that ⊤ is another name for N_{1}.

We note the differences with Palmgren’s original formulation in [30], Sect. 3, p. 194 - 195. He introduces first using the full logical framework a universe operator U(A, B), which forms for arbitrary ⟨A, B⟩ : Fam(Set) a universe U(A, B) (so it is closed under the basic set constructions) containing codes for A and B, together with decoding T(A, B, x) : Set for x : U(A, B). Then the superuniverse is a universe (V, S) containing for every ⟨a, b⟩ : IFam(V, S) with A := S(a) and B(x) := S(b(x)) an inductive subuniverse u(a, b) representing U(A, B). So we have u(a, b) : V, S(u(a, b)) = U(A, B), and for x : T(a) we have t(a, b, x) : V, S(t(a, b, x)) = T(A, B, x). So u, t are additional constructors of V. In this article we want to avoid the full logical framework. Therefore, we have restricted the super universe operator to elements of IFam(V, T). The reason for using a recursive subuniverse rather than an inductive one is essentially a matter of taste, we prefer to use recursive subuniverses as long as this does not lead to any complications.

We can say that without introducing U(A, B) we get an external super universe, similar to the external Mahlo universe introduced in the next subsection: Here Set plays the rôle of the super universe, since Set is closed under the universe operator. When introducing (V, S), Palmgren makes the step towards an internal super universe, i.e. of forming a universe which reflects the closure of Set under the universe operator. Relationship to inductive-recursive definitions. U(A, B) is an instance of an inductive-recursive definition [14, 15, 16, 17, 18, 19] with parameters A, B. Then one can see that Palmgren’s super universe is as well an instance of an inductive-recursive definition. The formulation of the super universe in Def. 3.1 is not directly an instance of an inductive-recursive definition. Note that the formulation of inductive-recursive definitions makes heavily use of the full logical framework, so it is no surprise that a definition which avoids it is no longer an instance of that particular schema. However we can still observe an inductive-recursive nature in it (and might consider it as an instance of a suitable extension of inductive-recursive definitions): V, U_{a,b} are defined simultaneously inductively, while T_{V}, T̂_{U,a,b} are defined recursively. The constructors for the inductive definitions are the constructors for the codes for the basic set constructions, â, b̂ and Û. Meaning explanations for the super universe. We will give meaning explanations for our formulation of the super universe in order to justify its constructive validity. We are giving them on request of the referee of a previous version of this article. We are giving them quite reluctantly, since we lack a philosophical education in order to have a proper understanding of meaning theory. We hope that researchers with a proper background in this area will be able to transform them into proper meaning explanations. The basic concept of meaning explanations and meaning explanations for the basic set constructions are as in Martin-Löf’s article and book [27, 26].

So it suffices to give meaning explanations for V and for U_{a,b} for each element a of V and each function b mapping elements of T_{V}(a) to elements of V. These meaning explanations are given simultaneously. Whenever we introduce a canonical element c of V, we determine the set T_{V}(c), and for each canonical element d of U_{a,b} we determine the element T̂_{U,a,b}(d) of V. This is done in such a way that if c, c′ are equal canonical elements of V, we have that T_{V}(c) and T_{V}(c′) are equal sets, and if c, c′ are equal canonical elements of U_{a,b}, then T̂_{U,a,b}(c) and T̂_{U,a,b}(c′) are equal elements of V. A non-canonical element c of V is equal to a canonical element c′ of V′ and then we define T_{V}(c) as T_{V}(c′). The same applies to T̂_{U,a,b} and all other recursive functions defined in this article.

The canonical elements of V are those given by the fact that V is closed under the basic set constructions, and closure under Û. Regarding closure under the basic set constructions, we only treat the case of Π: If c is an element of V and d a function mapping elements of T_{V}(c) to V, then Π̂_{V}(c, d) is a canonical element of V, and T_{V}(Π̂_{V}(c, d)) is the set Πx : T_{V}(c).T_{V}(d(x)). Π̂_{V}(c, d) and Π̂_{V}(c′, d′) are equal canonical elements of V, if c, c′ are equal elements of V and for x in T_{V}(c) d(x) and d′(x) are equal elements of V. One observes now that if Π̂_{V}(c, d) and Π̂_{V}(c′, d′) are equal canonical elements, then T_{V}(Π̂_{V}(c, d)) and T_{V}(Π̂_{V}(c′, d′)) are equal sets: we assume that T_{V}(c) and T_{V}(c′) are equal sets, and for x in T_{V}(c) that T_{V}(d(x)) and T_{V}(d′(x)) are equal sets. Then T_{V}(Π̂(c, d)) and T_{V}(Π̂(c′, d′)) are equal sets as well. By saying in future meaning explanations that a universe V, T_{V} is closed under the basic set constructions we mean the explanations given before (using appropriate names for the constructors).

The definition of when two canonical elements are equal and an argument why this implies that recursively defined functions applied to them give the same result have to be carried out for all future canonical elements, a task we usually leave to the reader.

Closure of V under Û is given as follows: If a is an element of V, and b is a function mapping elements of T_{V}(a) to V, then Û_{a,b} is a canonical element of V, and we define T_{V}(Û_{a,b}) = U_{a,b}, where U_{a,b} will be explained later, where we will only use the fact that V contains a and b(x) for x in T_{V}(a), and that V is closed under the basic set constructions (so we don’t use closure of V under Û). This concludes the meaning explanations for V.

For elements a of V and functions c mapping elements of T_{V}(a) to V we explain the meaning of U_{a,b}. Since U_{a,b} is a recursive subuniverse of V, we define T_{U,a,b}(c) as T_{V}(T̂_{U,a,b}(c)).

U_{a,b} is closed under the basic set constructions, and again we explain only closure under Π: If c is an element of U_{a,b} and d is a function mapping elements of T_{U,a,b}(c) to U_{a,b}, then Π̂_{U,a,b}(c, d) is a canonical element of U_{a,b}, and we define T̂_{V}(Π̂_{U,a,b}(c, d)) as Π̂_{V}(T̂_{V}(c), (x)T̂_{V}(d(x))), which one verifies is a (canonical) element of V. (Note that we have to define, when two canonical elements Π̂_{U,a,b}(c, d) and Π̂_{U,a,b}(c′, d′) are equal and see, why in this case T̂_{V}(Π̂_{U,a,b}(c, d)) and T̂_{V}(Π̂_{U,a,b}(c′, d′)) are equal.) By saying in future that a recursive subuniverse (U_{a,b}, T̂_{a,b}) of a universe (V, T_{V}) is closed under the basic set constructions we mean the explanations given before (using appropriate names for the constructors).

Furthermore U_{a,b} is closed under â_{a,b}, b̂_{a,b}: â_{a,b} is a canonical element of U_{a,b}, and we define T̂_{U,a,b}(â_{a,b}) to be a. If x : T_{U,a,b}(a), then b̂_{a,b}(x) is a canonical element of U_{a,b}, and we define T̂_{U,a,b}(b̂_{a,b}(x)) to be b(x).

3.2 The External Mahlo Universe

The super universe is a universe (V, T_{V}) which is closed under one operator on families of sets, namely the universe operator U. We obtain the external Mahlo universe (see [18], Sect. 6) by assuming that for any operator on families of sets there exist a universe closed under it. As indicated in the introduction, we will split such an operator into two components and introduce the following abbreviation (see the introduction for what is meant by notations like f, g : Oper(U, T)).

Definition 3.2 (Assuming the full logical framework.) Assume

h⃗ = f, g : Oper(Set)

and ⟨U, T ⟩ : Fam(Set).

By f̂, ĝ : IOper(U, T) reflect f, g we mean the following rules:

f̂, ĝ : IOper(U, T)

(which form constructors of U) and

\begin{aligned}T (f̂(a, b)) & = & f(T (a), T ∘ b) , \\ T (ĝ(a, b, c)) & = & g(T (a), T ∘ b, c) . \end{aligned}

Definition 3.3 The rules for the external Mahlo universe are as follows:

• We have the full logical framework and the rules for the basic set constructions.

Assume in the following

h⃗ = f, g : Oper(Set) .

Then we have the following:

• We have

Uh⃗ : Set , T_{U,h⃗} : Uh⃗ → Set .

• We have the rules expressing that (Uh⃗, T_{U,h⃗}) is a universe.

• We have the rules expressing that

f̂, ĝ : IOper(Uh⃗, Th⃗)

reflect h⃗.

Relationship to inductive-recursive definitions and meaning explanations. The external Mahlo universe is directly an instance of an inductiverecursive definition with parameter h⃗. We are at the moment not able to give meaning explanations for the external Mahlo universe, since we don’t have yet a sufficient understanding of meaning explanations for the full logical framework.

3.3 The (Internal) Mahlo Universe

The internal Mahlo universe is the Mahlo universe as originally formulated by the author in [48], and we usually refer to it as the Mahlo universe. The internal Mahlo universe avoids the logical framework, which means that we don’t refer to Fam(Set). Instead we form a universe (V, T_{V}), which is called the Mahlo universe, such that for any operator on families of sets internal to (V, T_{V}) there exists a recursive subuniverse in V closed under this operator. Note that in case of the external Mahlo universe, Set plays the rôle which is played by V in the internal Mahlo universe. We will below introduce as well the notion of an internal inductive Mahlo universe, where we replace the recursive subuniverse by an inductive one.

As for the external Mahlo universe, we will split these operators into its two components, and introduce the following abbreviation (see the introduction for what is meant by notations like f, g : IOper(U, T)):

Definition 3.4 Assume (U, T) : Fam(Set),

h⃗ = f, g : IOper(U, T) .

Assume (U′, T′) was declared to be an inductive subuniverse of (U, T) with embedding T̂ : U → U′, or (U′, T̂) was declared to be a recursive subuniverse of (U, T) with full decoding T′.

By

f̂, ĝ : IOper(U′, T′) reflect f, g ,

we mean the following rules:

f̂, ĝ : IOper(U′, T′)

(which form constructors of U) and

(a) in case of (U′, T′) being a recursive subuniverse of (U, T)

\begin{aligned}T̂(f̂(a, b)) & = & f(T̂(a), T̂ ∘ b) , \\ T̂(ĝ(a, b, c)) & = & g(T̂(a), T̂ ∘ b, c) ; \end{aligned}

(b) and in case (U′, T′) being an inductive subuniverse of (U, T)

\begin{aligned}T′(f̂(a, b)) & = & T (f(T̂(a), T̂ ∘ b)) , \\ T′(ĝ(a, b, c)) & = & T (g(T̂(a), T̂ ∘ b, c)) . \end{aligned}

Definition 3.5 (a) The rules for the internal Mahlo universe (also called simply the Mahlo universe or the internal recursive Mahlo universe) are as follows:

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

Assume in the following

h⃗ = f, g : IOper(V, T_{V}) .

• We have rules expressing that (Uh⃗, T̂_{U,h⃗}) is a recursive subuniverse of (V, T_{V}) with full decoding T_{U,h⃗}.

• We have rules expressing

f̂h⃗, ĝh⃗ : IOper(Uh⃗, T_{U,h⃗}) reflect h⃗ .

• We have the rule that V contains a code for Uh⃗.

Ûh⃗ : V , T_{V}(Ûh⃗) = Uh⃗ .

(b) The rules for the internal inductive Mahlo universe are obtained by replacing in (a) “recursive subuniverse” by “inductive subuniverse”.

Inductive-recursive nature of the construction. The Mahlo universe and all universe constructions defined later in this article are no longer instances of inductive-recursive definitions, since Û is a constructor which is no longer strictly positive (Note that Û : IOper(V, T_{V}) → V, where IOper(V, T_{V}) forms the two components of IFam(V, T_{V}) → IFam(V, T_{V})). However, we can still see some inductive-recursive nature in it, by some sets being defined inductively, and some functions recursively. In case of the Mahlo universe, V, Uh⃗ are defined simultaneously inductively, while T_{V}, T̂_{U,h⃗} are defined recursively. The constructors for the inductively defined sets are the constructors for the codes for the basic set constructions, f̂, ĝ and Û. Meaning explanations for the internal Mahlo universe. As for the super universe we give simultaneously the meaning of V and of U_{f,g}. Here f, g are such that from the understanding of the meaning of the sets and elements introduced before we can conclude that for every element a of V and every element b mapping elements of T_{V}(a) to V we have that f(a, b) is in V, and for every element c of T_{V}(f(a, b)) we have g(a, b, c) is in V. We say in the following “(V, T_{V}) is closed under (f, g)” for the condition on f, g just stated (which includes the proviso “from the understanding of the meaning of the sets and elements introduced before we can conclude that”).

As for the super universe, T_{V}(c) and T̂_{U,f,g}(c) will be defined for any canonical element of V and U_{f,g}, respectively, and then defined for arbitrary elements in the same way, and we define T_{U,f,g}(c) as T_{V}(T̂_{U,f,g}(c)).

We first explain V. (V, T_{V}) is closed under the basic set constructions. Assume now that (V, T_{V}) is closed under f, g (as stated before). Then Û_{f,g} is a canonical element of V and we define T_{V}(Û_{f,g}) = U_{f,g}, where U_{f,g} will be explained below while referring only to the closure of V under the basic set constructions and under f, g, not to the closure under Û. If f, f′ and g, g′ are equal functions of their respective types, than Û_{f,g} and Û_{f′,g′} are equal canonical elements of V. Since equal elements of V are mapped by T_{V} to equal sets we get that in this case U_{f,g} and U_{f′,g′} are equal since the elements introduced and T̂_{U,f,g} and T̂_{U,f′,g′} applied to them give the same results in V. This concludes the meaning explanations for V.

We now explain U_{f,g}. (U_{f,g}, T̂_{f,g}) is closed under the basic set constructions. U_{f,g} is closed under f, g using constructors f̂_{f,g}, ĝ_{f,g}, which means the following (this notion will be used in future meaning explanations): Assume a is an element of U_{f,g}, and b is a function, mapping elements x of T_{U,f,g}(a) to U_{f,g}. Then a′ := T̂_{U,f,g}(a) is an element of V and b′ := (x)T̂_{U,f,g}(b(x)) is a function mapping elements of T_{V}(a′) to V. Since we know that V is closed under f, g, we know that f(a′, b′) is an element of V and for c an element of T_{V}(f(a′, b′)) we have that g(a′, b′, c) is an element of V. Now f̂_{f,g}(a, b) and for c in T_{U,f,g}(f(a, b)) ĝ_{f,g}(a, b, c) are canonical elements of U_{f,g}, and we define T̂_{U,f,g}(f̂_{f,g}(a, b)) = f(a′, b′) and T̂_{U,f,g}(ĝ_{f,g}(a, b, c)) = g(a′, b′, c). f̂_{f,g}(a, b) is equal to f̂_{f,g}(a′, b′), if a, a′ are equal elements of U_{f,g} and b, b′ are equal functions from T_{U,f,g}(a) to U_{f,g}. Equality for elements ĝ_{f,g}(a, b, c) is defined similarly. This concludes the meaning explanation for U_{f,g}.

4 The Autonomous Mahlo Universe

We are now going to carry out steps towards the autonomous Mahlo universe. The first step is to iterate the Mahlo construction and to form in Subsect. 4.1 the hyper Mahlo universe and in Subsect. 4.2 the hyper^{n} and hyper^{α}-Mahlo universes. Then we will describe how to iterate the degrees of Mahloness autonomously, and obtain in Subsect. 4.3 the full formulation of the autonomous Mahlo universe. In the followup paper the Π_{3}-reflecting universe will be obtained by iterating the formation of higher degrees of Mahloness even further.

4.1 The hyper-Mahlo universe.

The step from a Mahlo universe to a hyper-Mahlo universe is similar to the step from a super universe to a hyper-super-universe (see the beginning of Sect. 5.1 of [53]): A hyper-Mahlo universe is a universe (U_{2}, T_{2}) such that for every h⃗_{2} : IOper(U_{2}, T_{2}) there exists a subuniverse U_{1,h⃗_{2}} represented in U_{2} such that U_{1,h⃗_{2}} is a Mahlo universe closed under h⃗_{2}. That U_{1,h⃗_{2}} with its decoding function T_{1,h⃗_{2}} is a Mahlo universe means that for every h⃗_{1} : IOper(U_{1,h⃗_{2}}, T_{1,h⃗_{2}}) there exists a subuniverse U_{0,h⃗_{2},h⃗_{1}} of U_{1,h⃗_{2}} closed under h⃗_{1} and represented in U_{1,h⃗_{2}}. If one wants to define U_{1,h⃗_{2}} as a recursive subuniverse of U_{2}, one has one small problem, namely that one needs to have a code for U_{0,h⃗_{2},h⃗_{1}} in U_{2}. But it is straightforward to introduce such a code.

As before we split operators on families of sets internal to a universe into its two components, and we obtain the following rules:

Definition 4.1 The rules for the hyper-Mahlo universe are as follows:

• Rules for the basic set constructions and the small logical framework.

• Rules expressing that (U_{2}, T_{2}) is universe.

Assume in the following

h⃗_{2} = f_{2}, g_{2} : IOper(U_{2}, T_{2}) .

• We have rules expressing that (U_{1,h⃗_{2}}, T̂_{1,h⃗_{2}}) is a recursive subuniverse of (U_{2}, T_{2}) with full decoding T_{1,h⃗_{2}}.

• We have rules expressing that

f̂_{1,h⃗_{2}}, ĝ_{1,h⃗_{2}} : IOper(U_{1,h⃗_{2}}, T_{1,h⃗_{2}}) reflect h⃗_{2} .

• We have the rule that U_{2} contains a code for U_{1,h⃗_{2}}:

Û_{2,1,h⃗_{2}} : U_{2} , T_{2}(Û_{2,1,h⃗_{2}}) = U_{1,h⃗_{2}} .

Assume in the following in addition

h⃗_{1} = f_{1}, g_{1} : IOper(U_{1,h⃗_{2}}, T_{1,h⃗_{2}}) .

• We have rules expressing that (U_{0,h⃗_{2},h⃗_{1}}, T̂_{0,h⃗_{2},h⃗_{1}}) is a recursive subuniverse of (U_{1,h⃗_{2}}, T_{1,h⃗_{2}}) with full decoding T_{0,h⃗_{2},h⃗_{1}}.

• We have rules expressing that

f̂_{0,h⃗_{2},h⃗_{1}}, ĝ_{0,h⃗_{2},h⃗_{1}} : IOper(U_{0,h⃗_{2},h⃗_{1}}, T_{0,h⃗_{2},h⃗_{1}}) reflect h⃗_{1} .

• We have the rule that U_{2} contains a code for U_{0,h⃗_{2},h⃗_{1}}:

Û_{2,0,h⃗_{2},h⃗_{1}} : U_{2} , T_{2}(Û_{2,0,h⃗_{2},h⃗_{1}}) = U_{0,h⃗_{2},h⃗_{1}} .

• We have the rule that U_{1,h⃗_{2}} contains a code for U_{0,h⃗_{2},h⃗_{1}}:

Û_{1,0,h⃗_{2},h⃗_{1}} : U_{1,h⃗_{2}} ,  T̂_{1,h⃗_{2}}(Û_{1,0,h⃗_{2},h⃗_{1}}) = Û_{2,0,h⃗_{2},h⃗_{1}} .

Inductive-recursive nature of the construction. In the above U_{2}, U_{1,h⃗_{2}}, U_{0,h⃗_{2},h⃗_{1}} are defined simultaneously inductively, while T_{2}, T̂_{1,h⃗_{2}}, T̂_{0,h⃗_{2},h⃗_{1}} are defined recursively. The constructors for the inductively defined sets are the constructors for the codes for the basic set constructions, f̂_{1}, ĝ_{1}, Û_{2,1}, f̂_{0}, ĝ_{0}, Û_{2,0}, Û_{1,0}. Meaning explanations for the hyper-Mahlo universe. As for the Mahlo universe we give simultaneously the meaning of

• U_{2},

• of U_{1,h⃗_{2}} for every h⃗_{2} = f_{2}, g_{2} such that (U_{2}, T_{2}) is closed under h⃗_{2} (note that this was introduced as an abbreviation in the meaning explanations for the Mahlo universe with a special proviso),

• and of U_{0,h⃗_{2},h⃗_{1}} for every h⃗_{2} as before and every h⃗_{1} = f_{1}, g_{1} such that (U_{1,h⃗_{2}}, T_{1,h⃗_{2}}) is closed under h⃗_{1}.

As for the super universe, T_{2}(a), T̂_{1,h⃗_{2}}(a), and T̂_{0,h⃗_{2},h⃗_{1}}(a) will be defined for any canonical elements of U_{2}, U_{1,h⃗_{2}}, U_{0,h⃗_{2},h⃗_{1}} respectively, and then defined for arbitrary elements in the same way. Furthermore T_{1,h⃗_{2}} and T_{0,h⃗_{2},h⃗_{1}} are defined as before. In addition to the explanations given below, (U_{2}, T_{2}), (U_{1,h⃗_{2}}, T̂_{1,h⃗_{2}}), (U_{0,h⃗_{2},h⃗_{1}}, T̂_{0,h⃗_{2},h⃗_{1}}) will be closed under the basic set constructions.

We explain U_{2}: Assume U_{2} is closed under h⃗_{2}. Then Û_{2,1,h⃗_{2}} is a canonical element of U_{2}, and we define T_{2}(Û_{2,1,h⃗_{2}}) to be U_{1,h⃗_{2}}, which will be explained below while only referring to the closure of U_{2} under the basic set constructions and under h⃗_{2}. Furthermore, if U_{1,h⃗_{2}} is closed under h⃗_{1}, then Û_{2,0,h⃗_{2},h⃗_{1}} is a canonical element of U_{2} and we define T_{2}(Û_{2,0,h⃗_{2},h⃗_{1}}) = U_{0,h⃗_{2},h⃗_{1}}, where U_{0,h⃗_{2},h⃗_{1}} will be explained below, while only referring to the closure of U_{2} and U_{1,h⃗_{2}} under the basic set constructions and under h⃗_{2} and h⃗_{1} respectively. If h⃗_{2}, h⃗′_{2} and h⃗_{1}, h⃗′_{1} are equal functions of their respective types, then Û_{2,0,h⃗_{2},h⃗_{1}} and Û_{2,0,h⃗′_{2},h⃗′_{1}} are

equal canonical elements of U_{2}, similar for Û_{1,h⃗_{2}} and Û_{1,h⃗′_{2}}. We can observe, when looking at their explanations below, that they are mapped by T_{2} to equal sets. This concludes the explanations of U_{2}.

We explain U_{1,h⃗_{2}}: (U_{1,h⃗_{2}}, T̂_{1,h⃗_{2}}) is closed under h⃗_{2} using constructors f̂_{1,h⃗_{2}}, ĝ_{1,h⃗_{2}}. Furthermore, if U_{1,h⃗_{2}} is closed under h⃗_{1}, then Û_{1,0,h⃗_{2},h⃗_{1}} is a canonical element of U_{1,h⃗_{2}} and we define T̂_{1,h⃗_{2}}(Û_{1,0,h⃗_{2},h⃗_{1}}) = Û_{2,0,h⃗_{2},h⃗_{1}}. If h⃗_{1}, h⃗′_{1} are equal functions of their types then Û_{2,0,h⃗_{2},h⃗_{1}} and Û_{2,0,h⃗_{2},h⃗′_{1}} are equal canonical

elements of U_{1,h⃗_{2}} which are mapped by T̂_{1,h⃗_{2}} to equal elements of U_{2}. We explain U_{0,h⃗_{2},h⃗_{1}}: (U_{0,h⃗_{2},h⃗_{1}}, T_{0,h⃗_{2},h⃗_{1}}) is closed under h⃗_{1} using constructors

f̂_{2,h⃗_{2},h⃗_{1}}, ĝ_{2,h⃗_{2},h⃗_{1}}, which finishes the explanation of it.

4.2 The hyper^{n}- and Hyper^{α}-Mahlo universe.

The hyper-Mahlo universe can easily be generalised to a hyper^{n}-Mahlo universe, which consists of n + 1 nested Mahlo universes (so the hyper^{0}-Mahlo universe is a Mahlo universe.)

We give now a generalisation to a hyper^{α}-Mahlo universe. For this we need first to introduce a set the ordinals α are elements of. Assume some ordinal notation system, for which we have proved in some other type theory that it is well-founded (e.g. an ordinal notation system of order type ϵ_{0}). Let the set of notations be given by a Boolean valued function ÔT : N → Bool which decides whether a natural number denotes an ordinal notation or not, and the less-than relation be given by a Boolean valued function ˆ≺′ : N → N → Bool, which is written infix, which are definable in Peano Arithmetic, and therefore definable using the basic set constructions plus the rules for atom (needed in order to obtain Peano’s fourth axiom).

In our type theory we use the rules for the basic set constructions, the small logical framework, and atom, and define using them ÔT, ˆ≺′. Then let OT(x) := atom(ÔT(x)), x ≺′ y := atom(x ˆ≺′ y), and write x ∈ OT for OT(x). We define now the set of ordinals as Ord := (n : N) × (n ∈ OT), and ⟨n, p⟩ ≺ ⟨m, q⟩ := n ≺′ m.

A hyper^{α}-universe is a universe (U^{α}, T^{α}), such that for every β ≺ α and h⃗ : IOper(U^{α}, T^{α}) there exists a hyper^{β}-sub-universe of (U^{α}, T^{α}), closed under h⃗ and represented in U^{α}. In order to formulate it one defines for α : Ord a set of universes Univ_{α} of universes of Mahlo degree α, i.e. of hyper^{−1+α}- Mahlo universes. (Univ_{0} contains universes which are not Mahlo at all, Univ_{1} contains the Mahlo-universes, which one might call hyper^{0}-Mahlo universes, Univ_{2} contains hyper-Mahlo or hyper^{1}-Mahlo universes, etc.; so the “Mahlo degree” determines “how much hyper^{α}-Mahlo” a universe is). For u : Univ_{α} we have (U_{α,u}, T_{U,α,u}) : Fam(Set) (note that this is an abbreviation introduced in the introduction which does not refer to the logical framework).

When defining it, one faces the problem that it is possible, but cumbersome, to use recursive subuniverses. The reason is that we get chains of subuniverses: If α_{0} ≻ α_{1} ≻ ⋯ ≻ α_{n}, we get chains of subuniverses u_{i} : U_{α_{i}} such that (U_{α_{i+1}u_{i+1}}, T_{U,α_{i+1},u_{i+1}}) is a subuniverse of (U_{α_{i}u_{i}}, T_{U,α_{i},u_{i}}). When using recursive subuniverses, we need to have codes for U_{i} in every universe U_{j} for j > i since the code for it will be recursively handed upwards until we reach the uppermost universe for which this code is mapped to the set U_{i}. This can be seen already for the hyper-Mahlo universe, where we first needed to introduce Û_{2,0,h⃗_{2},h⃗_{1}} : U_{2} before we were able to define Û_{1,0,h⃗_{2},h⃗_{1}} : U_{1,h⃗_{2}}, otherwise we couldn’t define an equality rule for T̂_{1,h⃗_{2}}(Û_{1,0,h⃗_{2},h⃗_{1}}). (See the end of Def. 4.1.) This is possible, but notationally complicated.^{1}

It is much easier to work instead with inductive subuniverses. Then elements created in subuniverses are automatically passed on to higher universes containing it. We will follow this approach in the following.

Definition 4.2 The rules for the hyper^{α}-Mahlo universe are as follows:

• Rules for the basic set constructions, the small logical framework, and atom.

• The definition equations for ÔT, ˆ≺′, OT, ≺′, Ord, ≺, as given above. The order type of the ordinal notation system is supposed to be 1 + α.

• Rules expressing that (V, T_{V}) is universe.

• Defining rules for Univ_{β}: Assume β : Ord.

– Univ_{β} : Set.

– Rules expressing that for β : Ord, u : Univ_{β} we have (U_{β,u}, T_{U,β,u}) is an inductive subuniverse of (V, T_{V}) with embedding T̂_{U,β,u}, which is represented in V by Û_{U,β,u}.

• Assume β : Ord,

h⃗ = f, g : IOper(V, T_{V}) .

– We have

v_{β,h⃗} : Univ_{β} .

Let locally in this item only v_{−} := v_{β,h⃗} : Univ_{β}.

– We have rules expressing that

f̂_{v,β,h⃗}, ĝ_{v,β,h⃗} : IOper(U_{β,v_{−}}, T_{U,β,v_{−}}) reflect h⃗ .

1In [53] we assumed that this is not possible because we expected to get infinite chains of universes. But in fact we never get such infinite chains: when going upwards in the Mahlo degrees, we will always in finitely many steps reach a top level. However the number of steps is different for universes having the same Mahlo degree.

• Assume β : Ord, u : Univ_{β}, γ : Ord, p : γ ≺ β, and

h⃗ = f, g : IOper(U_{β,u}, T_{U,β,u}) .

– We have

u_{β,u,γ,p,h⃗} : Univ_{γ} .

Let locally in this item only

U_{+}  := U_{β,u}  : Set ,
T_{+}(a) := T_{U,β,u}(a) : Set  (where a : U_{+}) ,
u_{−}  := u_{β,u,γ,p,h⃗} : Univ_{γ} ,
U_{−} := U_{γ,u_{−}} : Set ,
T_{−}(a) := T_{U,γ,u_{−}}(a) : Set  (where a : U_{−}) .

– (U_{−}, T_{−}) is an inductive subuniverse of (U_{+}, T_{+}) with embedding T̂_{u,β,u,γ,p,h⃗} : U_{−} → U_{+}, which is represented in U_{+} by Û_{u,β,u,γ,p,h⃗}.

– We have rules expressing that

f̂_{u,β,u,γ,p,h⃗}, ĝ_{u,β,u,γ,p,h⃗} : IOper(U_{−}, T_{−}) reflect h⃗ .

Note that in case of α = 0 we have that the ordinal notation system has one element and we obtain essentially the rules for the internal inductive Mahlo universe.

We leave it to the reader to model a hyper^{α}-Mahlo universe in Kripke-Platek set theory plus one recursively hyper^{α}-Mahlo ordinal and finitely many admissibles above it. (This model can as well be obtained by cutting down the model of the autonomous Mahlo universe below). Inductive-recursive nature of the construction. In the above V, U_{β,u}, Univ_{β} are defined simultaneously inductively, while T_{V}, T_{U,β,u} are defined recursively. The constructors for the inductively defined sets are the constructors for the codes for the basic set constructions, T̂_{U}, Û_{U}, v, f̂_{v}, ĝ_{v}, u, T̂_{u}, Û_{u}, f̂_{u}, ĝ_{u}. Meaning explanations for the hyper^{α}-Mahlo universe. For the hyper^{α}- Mahlo universe we assume that we have already shown without using the Mahlo universe that OT is well-founded, and therefore validated the principle of transfinite induction over Ord. The meaning explanations for the basic set constructions, ÔT, ˆ≺′, OT, ≺′, Ord, ≺ are standard. We will now give simultaneously the meaning of

• V,

• of Univ_{β} for β : Ord,

• and of U_{β,u} for β : Ord and u : Univ_{β}.

This will be done in such a way that U_{β,u} will not refer to V or U_{γ,u} for β ≺ γ except for the closure properties known at the time of introducing u, and by not referring to U_{β,u′} for other u′, except when defining it as equal to such a set because u and u′ are equal elements of Univ_{β}. So we only assume, when introducing U_{β,u} a complete understanding of U_{γ,u′} for γ ≺ β for certain u′ in Univ_{γ}.

Simultaneously recursively we define T_{V}(x) and T_{U,β,u}(x) for elements x of V and U_{β,u}, respectively. These operations will as before be first defined for canonical elements and then extended to arbitrary elements.

(V, T_{V}) and (U_{β,u}, T_{β,u}) will in addition to what is said below be closed under the basic set constructions.

Meaning of V: If β is in Ord, u is in Univ_{β}, then u′ := Û_{β,u} is a canonical element of V and T_{V}(u′) is defined as U_{β,u}. Furthermore, for a in U_{β,u} we have that a′ := T̂_{β,u}(a) is a canonical element of V and we define T_{V}(a′) = T_{β,u}(a).

Meaning of Univ_{β}: If (V, T_{V}) is closed under f, g, then v_{β,f,g} is a canonical element of Univ_{β}. Assume that (U_{γ,u}, T_{γ,u}) is closed under f, g. Assume p is an element of β ≺ γ. Then u_{γ,u,β,p,f,g} is a canonical element of Univ_{β}.

Meaning of U_{β,u}: We have closure properties applying to all u ∈ Univ_{β}: Assume that (U_{β,u}, T_{β,u}) is closed under f, g. Assume p is an element of γ ≺ β. Let u′ := u_{β,u,γ,p,f,g} which is a canonical element of Univ_{β}. Then u′′ := Û_{u,β,u,γ,p,f,g} is a canonical element of U_{β,u} with T_{β,u}(u′′) defined as U_{β,u′}. Furthermore for every a in U_{γ,u′} we have that a′ := T̂_{u,β,u,γ,p,f,g}(a) is a canonical element of U_{β,u} and we define T_{β,u}(a′) as T_{γ,u′}(a).

The additional closure properties for u′ := u_{β,u,γ,p,f,g} as defined before are: (U_{γ,u′}, T_{γ,u′}) is closed under f, g via T̂′ := T̂_{u,β,u,γ,p,f,g} using constructors f̂′ := f̂_{u,β,u,γ,p,f,g} and g′ := ĝ_{u,β,u,γ,p,f,g}. This means that if a is an element of U_{γ,u′} and b a function mapping T_{γ,u′}(a) to U_{γ,u′}, then a′ := f̂′(a, b) is a canonical element of U_{γ,u′} with T_{γ,u′}(a′) = A := T_{β,u}(f(T̂′(a), T̂′ ∘ b)). Furthermore, if c is an element of A, then c′ := g′(a, b, c) is a canonical element of U_{γ,u′} with T_{γ,u′}(c′) = T_{β,u}(g(T̂′(a), T̂′ ∘ b, c)).

The additional closure properties for v′ := v_{β,f,g} as defined before are: (U_{β,v′}, T_{β,v′}) is closed under f, g via T̂_{β,v′} using constructors f̂_{v,β,f,g}, ĝ_{v,β,f,g}.

4.3 The Autonomous Mahlo Universe

The next step is to define a universe (V, T_{V}) which has strength (KPω + (AutMahlo))^{+}. Here (KPω + (AutMahlo))^{+} means that there exists an ordinal κ which is recursively hyper^{κ}-Mahlo plus finitely many admissibles above it. We will call this universe the autonomous Mahlo universe.

(Recursively) inaccessible sets (and hyper^{κ}-Mahlo sets are inaccessible sets) correspond in type theory to universes, so we introduce in type theory a universe (V, T_{V}) which correspond to an autonomous Mahlo set. Ordinals can be modelled in type theory by elements of a W-type. The set of ordinals in a universe (V, T_{V}) are the elements of the W-type having as branching types all sets in V, which means that it can be represented by Wx : V.T_{V}(x)^{2}. We define the set Deg of degrees preliminarily as this set.

So we need to formulate that (V, T_{V}) is hyper^{d}-Mahlo for any d : Deg. In order to define this, we introduce for d : Deg the set Univ_{d} of codes for universes which are hyper^{d}-Mahlo. For each u : Univ_{d} we introduce the actual universe given by it as U_{d,u} : Set and T_{d,u} : U_{d,u} → Set.

That the autonomous Mahlo ordinal κ is hyper^{α}-Mahlo for any α < κ will be expressed by rules stating that for every h⃗ : IOper(V, T_{V}) and every degree d : Deg there exists a universe u : Univ_{d} s.t. U_{d,u} is closed under h⃗.

That a universe u : Univ_{d} is hyper^{d}-Mahlo will be expressed by rules stating that any h⃗ : IOper(U_{d,u}, T_{d,u}) can be reflected into smaller degrees d′. If d = sup(r, s), where r : V and s : T_{V}(a) → Deg, then the degrees d′ smaller than d are the degrees d′ := s(a) for a : T_{V}(a). Then we demand that any universe u : Univ_{d} is Mahlo reflecting in Univ_{d′} for any d′ smaller than d: If h⃗ : IOper(U_{d,u}, T_{d,u}), then there exists an inductive subuniverse of (U_{d,u}, T_{d,u}) in Univ_{d′} which is closed under h⃗ and represented in U_{d,u}.

(The reader might suggest that one should close “smaller” transitively, but that won’t result in introducing new universes: in order for instance to reflect h⃗ as above into a u′′ : Univ_{d′′}, where d′′ is smaller than d′ which is again smaller than d, we can first reflect h⃗ into some u′ : Univ_{d′} and reflect the function reflecting h⃗ in U_{d′,u′} into some u′′ : Univ_{d′′}.)

One problem seems to be that Deg depends on all of V, T_{V} – therefore Deg is only available once the construction of V, T_{V} is complete. But when constructing V one needs to know Deg in order to be able to introduce new universes for appropriate Mahlo degrees.

However, one can easily see that for every d : (Wx : V.T_{V}(x)) there exists an ⟨a, b⟩ : IFam(V, T_{V}) such that d and its subtrees only refer to elements of V in (b(x))_{x:a} (collect all branching degrees of d and its subtrees into one family of sets in V). More precisely, the situation is as follows: Define for ⟨a, b⟩ as above f_{a,b} : (Wx : T_{V}(a).T_{V}(b(x))) → Wx : V.T_{V}(x), f_{a,b}(sup(r, s)) = sup(b(r), (y)f_{a,b}(s(y))). Then for every d : Deg there exist some a, b, d′ s.t. d = f_{a,b}(d′) for some ⟨a, b⟩ and d′ : (Wx : T_{V}(a).T_{V}(b(x))).

Therefore the set of degrees depends only locally on V and one can construct Deg simultaneously while constructing V – whenever one constructs new elements of V one obtains new elements of Deg, which allow to construct new elements of V, namely subuniverses of V having the new degrees. The existence of an autonomous Mahlo universe means that we claim that this process eventually stops after transfinitely many steps. We distinguish now Deg, which is defined simultaneously with V from Wx : V.T_{V}(x) (which can fully only be defined after the definition of (V, T_{V}) is complete) and give the constructor introducing elements of Deg the name deg rather than sup.

It turns out that we don’t need any elimination rules for Deg, except for rules decomposing deg(r, s) into r and s. Full elimination rules are unnecessary, since there exists an obvious embedding g : (Wx : V.T_{V}(x)) → Deg. So if one wanted to refer to the least set of degrees introduced like this, one could refer to g(w) for w : (Wx : V.T_{V}(x)) and use the elimination rule for Wx : V.T_{V}(x).

2Note that this type is the same as Peter Aczel’s type V of iterative sets [1].

We therefore obtain now the following rules for the type theory with one autonomous Mahlo universe: Definition 4.3 The rules for the autonomous Mahlo universe are as follows:

• Rules for the basic set constructions and the small logical framework.

• Rules expressing that (V, T_{V}) is universe.

• Formation rule for Deg:

Deg : Set ,

• Introduction rule for Deg and elimination rules (referring to bdeg, subdeg): deg : (a : V, b : T_{V}(a) → Deg) → Deg ,

bdeg : Deg → V ,  subdeg : (d : Deg, a : T_{V}(bdeg(d))) → Deg .
bdeg(deg(a, b)) = a , subdeg(deg(a, b), c) = b(c) .

• Defining rules for Univ_{d}: Assume d : Deg.

– Univ_{d} : Set.

– Rules expressing that for d : Deg, u : Univ_{d} we have (U_{d,u}, T_{U,d,u}) is an inductive subuniverse of (V, T_{V}) with embedding T̂_{U,d,u}, which is represented in V as Û_{U,d,u}.

• Assume d : Deg,

h⃗ = f, g : IOper(V, T_{V}) .

– We have

v_{d,h⃗} : Univ_{d} .

Let locally in this item only v_{−} := v_{d,h⃗} : Univ_{d}.

– We have rules expressing that

f̂_{v,d,h⃗}, ĝ_{v,d,h⃗} : IOper(U_{d,v_{−}}, T_{U,d,v_{−}}) reflect h⃗ .

• Assume now d : Deg, u : Univ_{d}, a : T_{V}(bdeg(d)),

h⃗ = f, g : IOper(U_{d,u}, T_{U,d,u}) .

Let locally in this item only d_{−} := subdeg(d, a) : Deg.

– We have u_{d,u,a,h⃗} : Univ_{d_{−}} .

Let additionally locally in this item only

U_{+}  := U_{d,u}  : Set ,
T_{+}(a) := T_{U,d,u}(a)  : Set  (where a : U_{+}) ,
u_{−}  := u_{d,u,a,h⃗}  : Univ_{d_{−}} ,
U_{−}  := U_{d_{−},u_{−}}  : Set ,
T_{−}(a) := T_{U,d_{−},u_{−}}(a) : Set  (where a : U_{−}) .

– (U_{−}, T_{−}) is an inductive subuniverse of (U_{+}, T_{+}) with embedding T̂_{u,d,u,a,h⃗} : U_{−} → U_{+}, which is represented in U_{+} by Û_{u,d,u,a,h⃗}.

– We have rules expressing that

f̂_{u,d,u,a,h⃗}, ĝ_{u,d,u,a,h⃗} : IOper(U_{−}, T_{−}) reflect h⃗ .

Inductive-recursive nature of the construction. In the above V, Deg, Univ_{d}, U_{d,u} are defined simultaneously inductively, while T_{V}, bdeg, subdeg, T_{U,d,u} are defined recursively. The constructors for the inductively defined sets are the constructors for the codes for the basic set constructions, deg, T̂_{U}, Û_{U}, v, f̂_{v}, ĝ_{v}, u, T̂_{u}, Û_{u}, f̂_{u}, ĝ_{u}. Meaning explanations for the autonomous Mahlo universe. These meaning explanations will serve as a predicative justification of its constructive validity. We give simultaneously the meaning of Deg, V, Univ_{d} (for d in Deg) and U_{d,u} (for d in Deg and u in Univ_{d}). We will as well define simultaneously sets T_{V}(x) for x in V, and T_{d,u}(a) for a in U_{d,u}, and elements bdeg(d) in V for d in Deg and subdeg(d, a) for d in Deg and a in T_{V}(bdeg(d)). Here U_{d,u} will refer only to a complete understanding of U_{d′,u′} for some u′ in Univ_{d′} and degrees d′ introduced before introducing d. Otherwise it will only refer to U_{d′,u′} for other degrees d′ and to V by using closure properties known when introducing u.

(V, T_{V}) and (U_{d,u}, T_{d,u}) will in addition to what is said below be closed under the basic set constructions.

Explanation of V: If d is in Deg, u is in Univ_{d}, then Û_{U,d,u} is a canonical element of V and we define T_{V}(Û_{U,d,u}) as U_{d,u}. Furthermore, if a is in U_{d,u}, then T̂_{U,d,u}(a) is a canonical element of V and we define T_{V}(T̂_{U,d,u}(a)) as T_{U,d,u}(a).

Explanation of Deg: If a is in V, b is a function mapping elements of T_{V}(a) to Deg, then deg(a, b) is a canonical element of Deg and we define bdeg(deg(a, b)) = a, subdeg(deg(a, b), x) = b(x). Note that as usual we leave it to the reader to explain when two canonical elements of Deg are equal and that bdeg and subdeg applied to equal canonical elements result in equal elements of V and Deg, respectively.

Explanation of Univ_{d}: Assume (V, T_{V}) is closed under f, g and d is an element of Deg. Then v_{d,f,g} is a canonical element of Univ_{d}. Assume d is in Deg, u in Univ_{d}. Assume (U_{d,u}, T_{d,u}) is closed under f, g, a is in T_{V}(bdeg(d)), and let d_{−} := subdeg(d, a). Then we have u_{d,u,a,f,g} is a canonical element of Univ_{d_{−}}.

Explanation of U_{d,u}: As for the hyper^{α}-Mahlo universe, we first give an explanation of the closure properties of U_{d,u} which apply to all elements u of Univ_{d}: If the conditions for forming u_{−} := u_{d,u,a,f,g} above are fulfilled, then Û_{u,d,u,a,f,g} is a canonical element of U_{d,u} and we define T_{d,u}(Û_{u,d,u,a,f,g}) as U_{d_{−},u_{−}}. Furthermore for a in U_{d_{−},u_{−}} we define T̂_{u,d,u,a,f,g}(a) as a canonical element of U_{d,u} and define T_{d,u}(T̂_{u,d,u,a,f,g}(a)) as T_{d_{−},u_{−}}(a).

Now we define the additional closure properties for specific elements U_{d,u}: In case of u = v_{d,f,g} for which the conditions for introducing it are fulfilled we have that U_{d,u} is closed under f, g via T̂_{U,d,u} using constructors f̂_{v,d,f,g}, ĝ_{v,d,f,g}. In case of u = u_{d,u,a,f,g} which is an element of Univ_{d_{−}} with d_{−} as stated above we have that U_{d_{−},u} is closed under f, g via T̂_{u,d,u,a,f,g} using constructors f̂_{u,d,u,a,f,g}, ĝ_{u,d,u,a,f,g}.

5 A Model of the Autonomous Mahlo Universe

5.1 Notations

We will in the following make use of the notations and basic principles for developing models as introduced in the sections on model constructions of [53]. We repeat here the most important ones:

• Terms are interpreted as simplified terms of the language (we throw away some typing information which is not relevant in the model). For a term r let [[ r]]_{ρ} be the result of substituting free variables x by ρ(x) in r and omitting the information to be thrown away. Let [[ Term ]] be the set of terms.

• A set A in an environment ρ is interpreted as a partial equivalence relation (PER; i.e. a symmetric and transitive relation; see Def. 2.6(c) of [53]) [[ A]]_{ρ}, where ⟨a, b⟩ ∈ [[ A]]_{ρ} means that a and b are equal elements of [[ A]]_{ρ}. Dom([[ A]]_{ρ}) is the underlying set of terms, i.e. since [[ A]]_{ρ} is a PER, Dom([[ A]]_{ρ}) = {a | ⟨a, a⟩ ∈ [[ A]]_{ρ}}. (In [53] we used Flat instead of Dom – we change the notation on suggestion by the referee, in order to be closer to standard notations for PER models.)

• We will sometimes for simplicity treat [[ A]]_{ρ} as if it were a set of terms rather than a set of pairs of terms, and therefore identify [[ A]]_{ρ} with Dom([[ A]]_{ρ}).

• We have a reduction relation on terms corresponding to the elimination rules of the type theory. All interpretations of sets will be in addition to what is stated in the following be closed under reductions.

• We have operations on PERs corresponding to the operations of the standard set constructions and of the small logical framework, where we write [[ →]], [[ ×]], [[ + ]] infix. Especially we write (x ∈ A) [[ →]] B(x) for the set of functions mapping a ∈ Dom(A) to Dom(B(a)), or more precisely the corresponding partial equivalence relation. (x ∈ A) [[ ×]] B(x) stands for the PER corresponding to the set of pairs ⟨a, b⟩ for a ∈ Dom(A) and b ∈ Dom(B(a)). A [[ + ]] B is to be understood in a similar way.

• [[ IFam ]](U, T) := (x ∈ U) [[ ×]] (T (x) [[ →]] U), which is the PER corresponding to the set of pairs ⟨a, b⟩ such that a ∈ Dom(U) and b ∈ Dom(T (a) [[ →]] U).

• [[ IFamOper ]]_{0}(U, T) := (x ∈ U) [[ →]] (T (x) [[ →]] U) [[ →]] U , [[ IFamOper ]]_{1}(U, T, f) :=

(x ∈ U) [[ →]] (y ∈ (T (x) [[ →]] U)) [[ →]] T (f(x, y)) [[ →]] U ,

[[ IFamOper ]](U, T) := (f ∈ [[ IFamOper ]]_{0}(U, T)) [[ ×]] [[ IFamOper ]]_{1}(U, T, f) .

[[ IFamOper ]]_{0}(U, T) and [[ IFamOper ]]_{1}(U, T, f) form the two components of the set of functions [[ IFam ]](U, T) [[ →]] [[ IFam ]](U, T).

• The closure of X under reductions is defined as

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

5.2 Autonomous Mahlo and Hyper^{α}-Mahlo Ordinals

In order to define what it means for an ordinal to be recursively autonomous hyper^{α}-Mahlo we first introduce the notion of an recursively hyper^{α}-Mahlo. We will in the following usually omit the adverb “recursively” (or put it in brackets) which has to be added to all occurrences of hyper^{α}-Mahlo and autonomous Mahlo sets and ordinals.

Remember the definition of a Mahlo ordinal from [53]: 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⃗} .

Here Ad(u) means that u is an admissible set. A (recursively) Mahlo ordinal is an ordinal M such that L_{M} is a (recursively) Mahlo set.

Recursively Mahlo ordinals can be defined purely recursion theoretically ([21] Definition VIII.6.7 p. 422) as the set of ordinals κ such that for any F : κ → κ which is κ-recursive in parameters there exist a recursively regular (or admissible) ordinal λ < κ s.t. ∀π < λ.F (π) < λ.

Recursively hyper^{α}-Mahlo ordinal are obtained by stating instead that for any β < α any F as above can be reflected into a recursively hyper^{β}-Mahlo ordinal κ′. Since we want recursively hyper^{α}-Mahlo ordinals to be Mahlo, we need to allow as well reflection into admissible sets.

(Note that we only demand κ′ to be recursively hyper^{β}-Mahlo for one β < α, not for all β < α simultaneously, which would give a slightly different notion – with that different notion a recursively autonomous Mahlo κ is not recursively hyper^{κ}-Mahlo, but only recursively hyper^{α}-Mahlo for all α < κ).

Moving back to the definitions in Kripke-Platek set theory, we define for ordinals α the collection of (recursively) hyper^{α}-Mahlo sets hyper^{α}MahloSet by recursion on α as follows: hyper^{α}MahloSet is defined by having the following property:

(HyperMahlo)^{α} a ∈ hyper^{α}MahloSet →

Ad(a)∧

(∀z⃗ ∈ a.(∀x ∈ a.∃y ∈ a.φ(x, y, z⃗)) → ((∀β < α.∃u ∈ a.u ∈ hyper^{β}MahloSet ∧ z⃗ ∈ u ∧(∀x ∈ u.∃y ∈ u.φ(x, y, z⃗))) ∧∃u ∈ a.\begin{matrix}Ad(u) ∧ z⃗ ∈ u \\ ∧(∀x ∈ u.∃y ∈ u.φ(x, y, z⃗)))) \end{matrix}

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

So a hyper^{α}-Mahlo means that a is admissible and any Π_{2}-property ∀x ∈ a.∃y ∈ a.φ(x, y, z⃗) can be reflected for any β < α into a hyper^{β}-Mahlo set in a and be reflected into an admissible set in a. Especially hyper^{0}MahloSet are the (recursively) Mahlo sets. A (recursively) Hyper^{α}-Mahlo-ordinal is an ordinal κ such that L_{κ} is a (recursively) Hyper^{α}-Mahlo set.

Now an ordinal κ is (recursively) autonomous Mahlo (we say in the following briefly autonomous Mahlo) if it is (recursively) hyper^{κ}-Mahlo.

The theory (KPω + (Aut − Mahlo))^{+} of Kripke Platek set theory plus one (recursively) autonomous Mahlo ordinal and finitely many admissibles above is defined as follows:

• The language is that of KPi as in [13], and in addition a binary predicate u ∈ hyper^{β}MahloSet (depending on u, β), a constant AutMahloSet for an admissible which is autonomous Mahlo and for n ∈ ℕ constants a_{n} for the nth admissible above AutMahlo.

• We have the axioms of KPi as in [13], p. 124, but excluding (Δ_{0} − Col) and (Lim).

• We have axioms (HyperMahlo)^{α} (uniform in α, for any formula φ stated there).

• We have axioms

Ad(AutMahloSet)∧∀α ∈ AutMahloSet.AutMahloSet ∈ hyper^{α}MahloSet .

• We have for n ∈ ℕ axioms

Ad(a_{n}) ∧ AutMahloSet ∈ a_{n} ∧ a_{n} ∈ a_{n+1} .

5.3 The Basic Idea of the Model

The general idea for constructing models is as in Subsect. 3.2 of [53]: One defines by recursion on α (V^{α}, T^{α}) ∈ [[ Fam ]](Set) fulfilling Assumption 3.2. of [53] by closing V^{α} under the basic set constructions and adding codes for universes (i.e. elements of Univ_{d}), whenever for some β < α we have that (V^{β}, T^{β}) is suitable as an interpretation for this universe. The added universe is then interpreted as V^{β} for the minimal such β. Then [[ V ]] := V^{<AutM} and [[ T(a) ]]_{ρ} := T^{<AutM}([[ a]]_{ρ}) for a (recursively) autonomous Mahlo ordinal AutM.

Therefore the main task is to define when (V^{β}, T^{β}) is sufficiently closed so that it can be used as an interpretation of an element of Univ_{d}.

One problem when dealing with the autonomous Mahlo universe is the fact that the set Deg seems to depend on the whole universe we are defining. But we have observed above that it only depends locally on it, so each element of Deg depends only on locally small set of elements of the autonomous Mahlo universe. So we will be able to define approximations Deg^{α} of [[ Deg ]] simultaneously while defining V^{α}, T^{α}, and define [[ Deg ]] := Deg^{<AutM} := ⋃_{α<AutM} Deg^{α}, and refer, when defining V^{α} only to elements of Deg^{<α}.

As for the Mahlo universe (defined in [53]) we have the problem that we know the set of functions from families of elements in [[ V ]] to families of elements in [[ V ]] only, when the definition of [[ V ]] is complete. The solution there was to add Û_{f,g} without knowing that f and g are defined on all of [[ V ]] – all we needed was that they are defined on U_{f,g}. Similarly, we will add in the construction of the autonomous Mahlo universe codes v_{d,f,g} to V^{α} using only the fact that f, g are locally defined and that d ∈ Deg^{<α}. In fact we will only consider codes for subuniverses of the form v_{d,f,g}.

All other occurring universes will be modelled in this universe by codes of the form v_{d,f,g}. Especially we will add a reduction rule u_{d,u,a,f,g} ⟶ v_{d_{−},f,g} where d_{−} = subdeg(d, a). This means of course that that if in the model we have u = v_{d′,f,g} ∈ V^{α}, it is not necessarily the case that f, g are total on V: if u represents an element u_{d′′,u,a,f,g} in the type theory, then we know only that f, g are total on U_{d′′,u}, not on V. However, the type theory guarantees that d′ = subdeg(d′′, a) : Deg, therefore in the model d′ is an element of [[ Deg ]] – roughly speaking d′ is a “total degree”.

One could have defined a more sophisticated model by defining at each stage α the least subuniverse of V^{<α} closed under the constructions needed as an interpretation of u := v_{d,f,g}, and, if this set is sufficiently closed, take this set as an interpretation of U_{d,u}. This would be technically more complicated and we use the current definition, since it is simpler and gives a model.

[[ Univ_{d}]]_{ρ} will be essentially the set of v_{d′,f,g} (where d′ = [[ d]]_{ρ}) occurring in [[ V ]]. (We have to vary this definition slightly in order to accommodate for the rule stating that d = d′ : Deg implies Univ_{d} = Univ_{d′} : Set.)

5.4 Formal Definition of the Model

We will work in (KPω + (Aut − Mahlo))^{+} as defined above. The set of terms in the model. As for all models of type theory in [53], we will omit in [[ Term ]] the dependency of N̂, Σ̂ on V, U, d, u, and have for instance [[ N̂_{V} ]]_{ρ} := [[ N̂_{U,d,u}]]_{ρ} := N̂.

Univ_{d}, U_{d,u} will be interpreted as subsets of [[ V ]], and in the model we treat inductive subuniverses as if they were recursive subuniverses and we could omit the recursive embedding altogether, i.e. as if they were subsets. Note that in the original type theory, the embedding T̂ of an inductive subuniverse (U, T_{U}) into its encompassing universe (V, T_{V}) is a constructor. For instance, let N̂_{U} and N̂_{V} be the codes for the natural numbers in U and V. Then in the type theory we don’t have T̂(N̂_{U}) = N̂_{V} (however, we cannot prove inside type theory that they are not equal). All we have is that the sets they denote are the same, i.e. T_{V}(N̂_{V}) = T_{V}(T̂(N̂_{U})). In the model we have instead that N̂_{V} and T̂(N̂_{U}) are equal, and we will in the model omit the embedding T̂ altogether. Therefore T̂_{U,d,u}, T̂_{u,d,u,a,f,g} will be treated as if they were identity functions, and Û_{U,d,u}, Û_{u,d,u,a,f,g} will be identified with u and u_{d,u,a,f,g}, respectively. So we have the following reduction rules:

T̂_{U,d,u}(a) ⟶ a ,
T̂_{u,d,u,a,f,g}(x) ⟶ x ,
Û_{U,d,u} ⟶ u ,
Û_{u,d,u,a,f,g} ⟶ u_{d,u,a,f,g} .

The reduction rules for bdeg and subdeg are as given by their equality rules, i.e.

bdeg(deg(r, s)) ⟶ r ,
subdeg(deg(r, s), a) ⟶ s(a) .

f̂ and ĝ will be interpreted by their underlying functions, i.e. we have

f̂_{v,d,f,g}(x, y) ⟶ f(x, y) ,
f̂_{u,d,u,a,f,g}(x, y) ⟶ f(x, y) ,
ĝ_{v,d,f,g}(x, y, z) ⟶ g(x, y, z) ,
ĝ_{u,d,u,a,f,g}(x, y, z) ⟶ g(x, y, z) .

(We have to be careful that this causes no problems with the equality rules for T_{U,d,u}, T_{u,d,a,f,g}, but one sees immediately that there are indeed no problems.)

Furthermore u_{d,u,a,f,g} will be identified with v_{subdeg(d,a),f,g}, so we have

u_{d,u,a,f,g} ⟶ v_{subdeg(d,a),f,g} .

Closure properties of V^{β}: The crucial closure property of V^{α} apart from closing V^{<α} under one step basic set constructions is when to add v_{d,f,g} to V^{α}: We add it, if d ∈ Deg^{<α} and we have at a previous stage β < α found that V^{<β} has the closure properties needed so that it can be used as an interpretation of v_{d,f,g}. This means that

• V^{<β} is closed under f, g.

• V^{<β} contains bdeg(d).

• V^{<β} is closed under subuniverses relative to the subdegrees formed from the branching degrees just mentioned. This means that for any operator f̃, g̃ on families of sets internal to V^{<β} and any a ∈ T^{<β}(bdeg(d)) we have with d_{−} := subdeg(d, a) that v_{d_{−},f̃,g̃} is in V^{<β}.

This means that V^{<β} is sufficiently closed to serve as an interpretation of v_{d,f,g}, and we interpret v_{d,f,g} as V^{<β} for the minimal such β.

Since we are working in a PER model, we have to replace in the definitions reference to terms as elements of the sets by pairs of terms as elements of those sets. Definition of V^{α}, T^{α}, Deg^{α}. As for the super and Mahlo universe in [53], we define (V^{α}, T^{α}) ∈ [[ Fam ]](Set) by closing it under the one step standard set constructions. We will then interpret [[ V ]] = V^{<AutM}, [[ T_{V} ]] = T^{<AutM}.

In order to define when to add v_{d,f,g} we first introduce what it means for a family of sets to be closed under d:

Definition 5.1 Let (U, T) ∈ [[ Fam ]](Set), ⟨d, d′⟩ ∈ [[ Term ]]^{2}. (U, T) is downward closed under d, d′, written as degClosure(U, T, d, d′), if the following holds:

(1) U is closed under ⟨bdeg(d), bdeg(d′)⟩, i.e.

⟨bdeg(d), bdeg(d′)⟩ ∈ U .

(2) U is closed under the formation of subuniverses for subdegrees of d, d′:

Assume a, a′, f̃, f̃′, g̃, g′ ∈ [[ Term ]] such that the following holds:

– ⟨a, a′⟩ ∈ T (bdeg(d)),

– d_{−} := subdeg(d, a), d_{−}′ := subdeg(d′, a′),

– U is closed under f̃, f̃′, g̃, g′, i.e.

⟨⟨f̃, g̃⟩, ⟨f̃′, g′⟩⟩ ∈ [[ IFamOper ]](U, T) .

Then

⟨v_{d_{−},f̃,g̃}, v_{d_{−}′,f̃′,g′}⟩ ∈ U .

Assume now an ordinal α and d, d,′ f, f′, g, g′ ∈ [[ Term ]]. Assume β s.t. β + 1 < α. Assume

• (V^{<β}, T^{<β}) is closed under the universe constructions.

• (V^{<β}, T^{<β}) is closed under f, f′, g, g′:

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

• ⟨d, d′⟩ ∈ Deg^{<α}.

• degClosure(V^{<β}, T^{<β}, d, d′).

We call the above conditions the “conditions for possibly interpreting [[ T ]](v_{d,f,g}) as V^{<β}.” Let β be minimal such that the above holds. Then

⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ V^{α} , T^{α}(v_{d,f,g}) := V^{<β} .

Furthermore Deg^{α}, Deg^{<α} are defined as follows simultaneously with defining V^{α}, T^{α}:

Deg^{<α} := ⋃_{β<α} Deg^{β} ,
Deg^{α} := Clos_{→}({⟨deg(r, s), deg(r′, s′)⟩ | ⟨r, r′⟩ ∈ V^{<α} ∧ ⟨s, s′⟩ ∈ T^{<α}(r) [[ →]] Deg^{<α}}) .

Interpretation of the other sets. We define now for an autonomous Mahlo ordinal AutM

[[ V ]]_{ρ} := V^{<AutM} ,
[[ T_{V}(a) ]]_{ρ} := [[ T_{V} ]]([[ a]]_{ρ}) := T^{<AutM}([[ a]]_{ρ}) ,
[[ Deg ]]_{ρ} := Deg^{<AutM} ,

and then

[[ Univ_{d}]]_{ρ} := Clos_{→}(\begin{cases}⟨v_{d′′,f,g}, v_{d′′′,f′,g′}⟩ ∈ [[ Term ]]^{2} | \\ ⟨v_{d′,f,g}, v_{d′′,f,g}⟩ ∈ [[ V ]] ∧ ⟨v_{d′′,f,g}, v_{d′′′,f′,g′}⟩ ∈ [[ V ]]\}) , \end{cases}
where d′ = [[ d]]_{ρ}.
[[ U_{d,u}]]_{ρ} := [[ T_{V} ]]([[ u]]_{ρ}) .
[[ T_{U,d,u}(a) ]]_{ρ} := [[ T_{V} ]]([[ a]]_{ρ}) .

As for all previous models we have [[ V ]] ∈ L_{AutM+1} and [[ T_{V} ]](a) ∈ L_{AutM} for a ∈ [[ V ]] and define therefore

o(U) := AutM + 1 , o(T_{V}(a)) := AutM .

The interpretation of the basic set constructions will be defined as in the previously introduced models of type theories, and this will require the use of finitely many admissibles on top of AutM.

We can easily see see that Assumption 3.2 of [53] holds.

5.5 Correctness of the Model

Basic correctness. The crucial part of the correctness proof for the model model will be to show that [[ Deg ]] is closed under the introduction rule for Deg

– this is where we use the fact that AutM is an autonomous Mahlo ordinal.

A minor complication arises as well when showing that, if d, d′ are equal elements of [[ Deg ]], then [[ Univ_{d}]] and [[ Univ_{d′} ]] are equal. Before verifying this, we show the correctness of the other rules:

• The correctness of all equality rules follow by the corresponding reduction rules.

• We have that [[ bdeg ]] ∈ [[ Deg ]] [[ →]] [[ V ]], and for ⟨d, d′⟩ ∈ [[ Deg ]] and ⟨a, a′⟩ ∈ [[ T ]](bdeg(d)) we have that ⟨subdeg(d, a), subdeg(d′, a′)⟩ ∈ [[ Deg ]]:

Assume ⟨d, d′⟩ ∈ [[ Deg ]]. Then ⟨d, d′⟩ ∈ Deg^{α} for some α. But then d ⟶ deg(r, s), d′ ⟶ deg(r′, s′) s.t. ⟨r, r′⟩ ∈ V^{<α} and ⟨s, s′⟩ ∈ T^{<α}(r) [[ →]] Deg^{<α}. bdeg(d) ⟶ r bdeg(d′) ⟶ r′, therefore ⟨bdeg(d), bdeg(d′)⟩ ∈ V^{<α} ⊆ [[ V ]]. Furthermore assume ⟨a, a⟩ ∈ [[ T ]](bdeg(d)) = T^{<α}(bdeg(d)). We have subdeg(d, a) ⟶ s(a), subdeg(d′, a′) ⟶ s′(a′), ⟨s(a), s′(a′)⟩ ∈ Deg^{<α} ⊆ [[ Deg ]], and therefore as well ⟨subdeg(d, a), subdeg(d′, a′)⟩ ∈ [[ Deg ]].

• We show that [[ Deg ]] is closed under the introduction rule. Assume ⟨r, r′⟩ ∈ [[ V ]], and ⟨s, s′⟩ ∈ [[ T ]](r) [[ →]] [[ Deg ]]. Then ⟨r, r′⟩ ∈ V^{<α} for some α < AutM. [[ T ]](r) = T^{<α}(r) ∈ L_{AutM}, ∀⟨a, a′⟩ ∈ T^{<α}(r).∃β < AutM.⟨s(a), s′(a′)⟩ ∈ Deg^{β}. By AutM admissible there exists γ < AutM s.t. α < γ and the β just given can always to be chosen < γ. But then it follows ⟨deg(r, s), deg(r′, s′)⟩ ∈ Deg^{γ} ⊆ [[ Deg ]].

• [[ V ]] is a universe: One easily verifies that Assumption 3.2 of [53] is fulfilled with U replaced by V. Therefore, by Theorem 3.3 of [53] and the fact that AutM is a recursively inaccessible we get that ([[ V ]], [[ T_{V} ]]) is closed under the universe constructions.

• That ([[ U_{d,u}]]_{ρ}, [[ T_{U,d,u}]]_{ρ}) are closed under the universe constructions follows by the construction. [[ U_{d,u}]]_{ρ} ⊆ [[ V ]], T̂_{U,d,u}(x) ⟶ x and Û_{d,y} ⟶ u ∈ [[ V ]], therefore ([[ U_{d,u}]]_{ρ}, [[ T_{U,d,u}]]_{ρ}) fulfils the rules for being an inductive subuniverse of V represented in V.

• We prove the correctness of the introduction rule introducing v_{d,f,g}. More generally we prove the following:

– Assume α ∈ Ord, ⟨d, d′⟩ ∈ Deg^{α}. Assume κ ∈ Ord, κ hyper^{α}-Mahlo, ⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]](V^{<κ}, T^{<κ}). Then ⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ V^{κ+2}.

If we have proved that statement above then the assertion follows: If ⟨d, d′⟩ ∈ [[ Deg ]], then ⟨d, d′⟩ ∈ Deg^{α} some α < AutM. AutM is hyper^{α+1}- Mahlo, so if ⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]]([[ V ]], [[ T ]]), then ⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]](V^{<κ}, T^{<κ}) for some κ which is hyper^{α}-Mahlo. Here we use the fact that ⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]]([[ V ]], [[ T ]]) can be expressed as a Π_{2}-formula in AutM (similarly as it was the case in case of the Mahlo universe). But then ⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ V^{κ+2} ⊆ [[ V ]].

We prove now the statement above by induction over α.

Let r := bdeg(d), r′ := bdeg(d′), s(x) := subdeg(d, x), s′(x) := subdeg(s′, x). We have ⟨r, r′⟩ ∈ U^{<α} ⊆ U^{<κ} since α ≤ κ, and for ⟨x, x′⟩ ∈ T^{<α}(r) we have that ⟨s(x), s′(x′)⟩ ∈ Deg^{<α}. In order to show that ⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ V^{κ+2} it suffices to show that the conditions for possibly interpreting [[ T ]](v_{d,f,g}) as V^{<κ} are fulfilled. Since κ is Mahlo, it is inaccessible and therefore (V^{<κ}, T^{<κ}) is closed under the universe constructions. It is by assumption closed under f, f′, g, g′. By α ≤ κ we get ⟨d, d′⟩ ∈ Deg^{<κ}. So we need to show degClosure(V^{<κ}, T^{<κ}, d, d′). ⟨r, r′⟩ ∈ U^{<κ}. Assume a, a′, f̃, f̃′, g̃, g′ s.t. ⟨a, a′⟩ ∈ T^{<κ}(r), d_{−} := subdeg(d, a), d′_{−} := subdeg(d′, a′), and ⟨⟨f̃, g̃⟩, ⟨f̃′, g′⟩⟩ ∈ [[ IFamOper ]](U^{<κ}, T^{<κ}). The above can be expressed as a Π_{2}-formula. ⟨d_{−}, d′_{−}⟩ ∈ Deg^{<α}. Let ⟨d_{−}, d′_{−}⟩ ∈ Deg^{β} for β < α. By κ being hyper^{α}-Mahlo there exists a κ′ < κ which is hyper^{β}-Mahlo, s.t. ⟨⟨f̃, g̃⟩, ⟨f̃′, g′⟩⟩ ∈ [[ IFamOper ]](U^{<κ′}, T^{<κ′}). By IH ⟨v_{d_{−},f̃,g̃}, v_{d′_{−},f̃′,g′}⟩ ∈ U^{κ′+2} ⊆ U^{<κ}.

• The closure of [[ U_{d,v_{d,f,g}} ]]_{ρ} under f̂_{v,d,f,g}, ĝ_{v,d,f,g}, follows by the construction and the reduction rules for f̂, ĝ.

• Similarly follows, with d_{−} := subdeg(d, a) the closure of [[ U_{d_{−},u_{d,u,a,f,g}} ]]_{ρ} under f̂_{u,d,u,a,f,g}, ĝ_{u,d,u,a,f,g}.

• The correctness of the introduction rule introducing u_{d,u,a,f,g} follows by the fact that u ∈ Dom([[ Univ_{d}]]_{ρ}) must reduce to v_{d′′,f̃,g̃} where ⟨v_{d′,f̃,g̃}, v_{d′′,f̃,g̃}⟩ ∈ [[ V ]] (d′ := [[ d]]_{ρ}), that therefore [[ U_{d,u}]]_{ρ} = [[ T_{V} ]](v_{d′,f̃,g̃}) = [[ T_{V} ]](v_{d′′,f̃,g̃}) is closed under the formation of subuniverses (interpreting v_{d_{−},f,g} for subdegrees d_{−} of d), and that u_{d,u,a,f,g} ⟶ v_{d_{−},f,g} for d_{−} = subdeg(d, a).

• That with u_{−} := u_{d,u,a,f,g} and d_{−} := subdeg(d, a) we have that (under the assumptions given by the rules) the correctness of the rules expressing that (U_{d_{−},u_{−}}, T_{d_{−},u_{−}}) is an inductive subuniverse of (U_{d,u}, T_{d,u}) holds follows since u must reduce to some v_{d,f̃,g̃}, and U_{d,u} was interpreted as some V^{<α} which contained [[ U_{d_{−},u_{−}} ]] as a subset and u_{−} as an element (the argument is essentially the same as verifying the correctness of U_{d,u} being an inductive subuniverse of V above).

Correctness of the equality rule for Univ_{d}. We show the correctness of the equality rule for Univ_{d}, which expresses that if d = d′ : Deg then Univ_{d} = Univ_{d′} : Set. First we see easily by main induction on α and side-induction on β that the following small lemma holds:

⟨a, b⟩ ∈ V^{α} → ∀β < α(⟨a, a⟩ ∈ V^{β} ∨ ⟨b, b⟩ ∈ V^{β}) → ⟨a, b⟩ ∈ V^{β} .

Now we show the following statement:

∀α < AutM.∀d, d′, f, g, a ∈ [[ Term ]].∀⟨d, d′⟩ ∈ [[ Deg ]].
(⟨v_{d,f,g}, a⟩ ∈ V^{α} → ⟨v_{d′,f,g}, a⟩ ∈ V^{α})∧
(⟨a, v_{d,f,g}⟩ ∈ V^{α} → ⟨a, v_{d′,f,g}⟩ ∈ V^{α}) .

Then, since [[ V ]] is symmetric and transitive, we obtain that ⟨d, d′⟩ ∈ [[ Deg ]] implies [[ Univ_{d}]] = [[ Univ_{d′} ]].

The statement is shown by induction on α. We need to show only the first half, the second half follows by the symmetry of V^{α} (the symmetry is part of Assumption 3.2 of [53]). Assume α, ⟨d, d′⟩ ∈ [[ Deg ]], ⟨v_{d,f,g}, a⟩ ∈ V^{α}, and that the assertion holds for β < α. Then a ⟶ v_{d′′,f′,g′} for some d′′, f′, g′. Let T^{α}(v_{d,f,g}) = V^{<β} with β + 1 < α.

Therefore V^{<β} is closed under the universe constructions,

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

and we have degClosure(V^{<β}, T^{<β}, d, d′′). We have that ⟨d, d′⟩ ∈ [[ Deg ]] implies ⟨bdeg(d), bdeg(d′)⟩ ∈ [[ V ]] and for ⟨a, a′⟩ ∈ [[ T_{V} ]](bdeg(d)) we have ⟨subdeg(d, a), subdeg(d′, a′)⟩ ∈ [[ Deg ]]. But then we obtain using the IH for ordinals < β that degClosure(V^{<β}, T^{<β}, d′, d′′) holds. Therefore ⟨v_{d′,f,g}, a⟩ ∈ V^{α}. Remaining construction of the model. The remaining steps are as for the other models of type theory with universes in [53]: We need finitely many admissibles above AutM in order to interpret the basic set constructions on top of V, T_{V} (each application of the W-type on top of V requires one more admissible). Therefore the type theory can be interpreted in Kripke Platek set theory plus one Π_{3}-reflecting 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.2

(a) We can model ML_{W} + (Aut − Mahlo) in (KPω + (Aut − Mahlo))^{+}.

(b) |ML_{W} + (Aut − Mahlo)| ≤ |(KPω + (Aut − Mahlo))^{+}|.

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

Remark 5.3 The status of the above theorem is as follows: Above we have developed the model and proved its correctness, including the details involving the autonomous Mahlo universe which go beyond standard Martin-Löf type theory. However, we are relying on the basic constructions of models of type theory in Kripke-Platek set theory, which includes how to interpret the basic set constructions, and the properties of the terms and reductions of terms used. In the author’s PhD thesis [42], these details have been worked out in full detail, but the setting there was not very generic to be adaptable to the current setting. The author would have liked to publish a modernised presentation of this model construction before publishing the current article, which would have enabled him to carry out the details in full. However, he felt that presenting the autonomous Mahlo and the Π_{3}-reflecting universes is more urgent, and therefore decided to present this universe with a sketch of the model, rather than waiting before the infrastructure article has gone through the publishing process. So what makes the current model constructions a sketch is the general setting common to all models of type theory (and one can refer to my PhD thesis for those details), the correctness of the model regarding the details of the autonomous Mahlo universe have been worked out in this article in detail.

6 Conclusion

We have shown how to develop an autonomous Mahlo universe. We have developed a model for the autonomous Mahlo universe and therefore determined an upper bound for its proof theoretic strength. Future research. Apart from introducing the Π_{3}-reflecting universe together with a proof theoretical analysis, the next steps will be to introduce stronger universes, for which we already have developed draft versions: the Π_{N}-reflecting universe and a Π_{1}^{1}-reflecting universe. We need to carry out as well well-ordering proofs for these extensions (at the moment there are only very rough sketches). Another line of research would be to explore, whether variants of these universe constructions can be used in programming, especially in generic programming.

References

[1] P. Aczel. The type theoretic interpretation of Constructive Set Ttheory: choice principles. In A. S. Troelstra and D. van Dalen, editors, The L.E.J¿ Brouwer Centenary Symposium, pages 1 – 40, Amsterdam, 1982. North Holland.

[2] P. Aczel and W. Richter. Inductive definitions and analogues of large cardinals. In W. Hodges, editor, Conference in Mathematical Logic, London ’70, Lecture Notes in Mathematics, Vol. 255, pages 1 – 9, Berlin, 1972. Springer.

[3] T. Arai. Proof theory of theories of ordinals I: Reflecting ordinals. Draft, 1996.

[4] T. Arai. Systems of ordinal diagrams. Draft, 1996.

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

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

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

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

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

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

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

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

[13] W. Buchholz. A simplified version of local predicativity. In P. Aczel, H. Simmons, and S. S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 115 – 147, Cambridge, 1992. Cambridge University Press.

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

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

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

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

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

[19] P. Dybjer and A. Setzer. Indexed induction-recursion. Journal of Logic and Algebraic Programming, 66:1 – 49, 2006.

[20] P. Hancock and P. Hyvernat. Programming interfaces and basic topology. Ann. Pure Appl. Logic, 137(1-3):189–239, 2006.

[21] P. Hinman. Recursion-Theoretic Hierarchies. Springer, Berlin, Heidelberg, New York, 1978.

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

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

[24] G. Jäger and T. Strahm. Reflections on reflections in explicit mathematics. Ann. Pure Appl. Logic, 136(1-2):116 – 133, 2005.

[25] P. Jansson. Functional Polytypic Programming: Use and Implementation. PhD thesis, Computing Science, Chalmers University of Technology, Gothenburg, Sweden, 1997.

[26] P. Martin-Löf. Constructive mathematics and computer programming. In L. Cohen, J. Los, H. Pfeiffer, and K.-P. Podewski, editors, Logic, Methodology and Philosophy of Science VI, pages 153–175, Amsterdam, 1982. North-Holland.

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

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

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

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

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

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

[33] M. Rathjen. Ordinal notations based on a weakly Mahlo cardinal. Arch. math. Logic, 29:249 – 263, 1990.

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

[35] M. Rathjen. Eine Ordinalzahlanalyse der Π_{3}–Reflexion. Habilitationsschrift, Westfälische Wilhelms–Universität Münster, 1992.

[36] M. Rathjen. Collapsing functions based on recursively large cardinals: A well-ordering proof for KPM. Arch. math. Logic, 33:35–55, 1994.

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

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

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

[40] M. Rathjen. An ordinal analysis of stability. Arch. Math. Logic, 44(1):1 – 62, January 2005.

[41] W. Richter and P. Aczel. Inductive definitions and reflecting properties of admissible ordinals. In J. E. Fenstad and P. G. Hinman, editors, Generalized recursion theory, pages 301 – 381, Amsterdam, 1973. North-Holland.

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

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

[44] 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 via http://www.cs.swan.ac.uk/∼sim/articles/1papdiss.dvi or .ps or .pdf, 1996.

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

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

[47] A. Setzer. Ordinal systems. In C. B. and J. Truss, editors, Sets and Proofs, pages 301 – 331, Cambridge, 1999. Cambridge University Press.

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

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

[50] A. Setzer. Ordinal systems part 2: One inaccessible. In S. Buss, P. Hajek, and P. Pudlak, editors, Logic Colloquium ’98, ASL Lecture Notes in Logic 13, pages 426 – 448, Massachusetts, 2000. Peters Ltd.

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

[52] A. Setzer. Ordinal systems part 3: Mahlo. In preparation, 2006.

[53] A. Setzer. Universes in type theory part I – Inaccessibles and Mahlo. In A. Andretta, K. Kearnes, and D. Zambella, editors, Logic Colloquium ’04, pages 123 – 156. Association of Symbolic Logic, Lecture Notes in Logic 29, Cambridge University Press, 2008.

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