Universes in Type Theory Part II – Autonomous Mahlo and Π_{3}-Reflection

Anton Setzer^{∗}

22 December 2005

Abstract

We introduce an extension of Martin-Löf type theory, which we conjecture to have the same proof theoretic strength as Kripke-Platek set theory (KP) extended by one Π_{3}-reflecting ordinal and finitely many admissibles above it. That would mean that the proof theoretic strength of this type theory is substantially bigger than that of any previous predicatively justified extensions of Martin-Löf type theory, including the Mahlo universe. The universe is constructed following the principles of ordinal notation systems of strength KP plus one Π_{3}-reflecting ordinal, therefore extracting key ideas of these notation systems. We introduce a model for this type theory, and determine an upper bound for its proof theoretic strength. This article only presents the main ideas of this model construction, full details will be given in a future article.

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. (However, because of our lack of expertise in philosophy, we refrain from giving any meaning explanations.) 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, University of Wales Swansea, Singleton Park, Swansea SA2 8PP, UK, Email: a.g.setzer@swan.ac.uk, http://www.cs.swan.ac.uk/∼csetzer/, Tel:

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

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

(2) 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 of this 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]).

In the article [50], 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 tries to use as little strength of the theory, in which the models are developed, as possible.) Lower bounds for the proof theoretic strength of these theories have been shown in [39, 43, 46].

In this article we introduce a new universe construction into Martin-Löf type theory of expected strength Kripke-Platek set theory plus one Π_{3}-reflecting ordinal and finitely many admissibles above it. At the time of writing we have a sketch of a well-ordering proof, full details have still to be worked out. If this result is proven this will show that the strength of this universe goes substantially beyond that of the Mahlo universe. The step from Mahlo to Π_{3}-reflection is very natural and follows recent developments in proof theory.

After an analysis of (Δ_{2}^{1} − CA) + (BI) and, 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 independently by Rathjen and Arai (see [31, 32, 34] and [2, 3, 7, 9])^{1}. Then both researchers analysed Kripke-Platek set theory plus one Π_{3}-reflecting ordinal ([33, 35] and [2, 3, 6, 10]), and in this article we develop a type theory which we expect to have essentially the same strength. Then later in proof theory theories of strength Π_{N}-reflection (Arai only), Π_{1}^{1}-reflection (Arai only), stability, (Π_{2}^{1}−CA)+(BI) and (Δ_{3}^{1}−CA)−(BI) (Arai only) were analysed (see [30, 36, 37] and [2, 4, 5]; one should note that at present Rathjen’s analysis of full (Π_{2}^{1} − CA) + (BI) and Arai’s analysis of theories beyond Π_{3}-reflection exist only in draft form or got stuck in the referee process). We hope to present soon extensions of Martin-Löf type theory which follow further steps in the development of proof theory (although at present (Π_{2}^{1} − CA) is out of reach).

Relationship to the article [50]. This article is a follow-up article of the article [50], in which we introduced type theories with one universe, one super universe, and one Mahlo universe. We gave there as well the basic model constructions, without carrying out all details. Similarly, in this article we will not carry out the model construction in full detail. The main goal of this article is to introduce the Π_{3}-reflecting universe and give a sketch of the model construction – full details will follow in a future 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 Π_{3}- reflecting 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 ([44, 47, 49]) to Π_{3}-reflection, which can then be carried out using the Π_{3}- reflecting universe.

Notations. We will frequently make use of notations and some basic lemmata introduced in [50], 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 [50] first.

Content. The structure of this article is as follows: In Section 2 we start by discussing in Subsection 2.1, why a naïve approach for developing a Π_{3}- reflecting universe doesn’t work. One is tempted to suggest such an approach since the previous universe constructions were based on reflections of type-0 and type-1 functionals, therefore one expects that Π_{3}-reflection should be based on reflections of type-2 functionals – we show why this approach doesn’t work out.

1Both researchers have quite independent approaches and have achieved their results at different times. If one takes the dates of publication, Rathjen’s results were obtained much earlier – however many results of Arai have been around for long time in the form of notes, which makes it difficult to determine who obtained which results first.

Then we introduce in Subsect. 2.2 the autonomous Mahlo universe which corresponds to the existence of an admissible α which is hyper-α-Mahlo. We first introduce hyper-Mahlo and hyper^{α}-Mahlo universes and discuss how to overcome the minor complications arising there. Then we introduce the autonomous Mahlo universe, which is the main intermediate step towards the Π_{3}-reflecting universe.

In Section 3 we first motivate the Π_{3}-reflecting universe (Subsect. 3.1), and then introduce in Subsect. 3.2 the Π_{3}-reflecting universe in detail.

Finally, in Sect. 4 we introduce a model for the Π_{3}-reflecting universe and give a sketch of its correctness. This way we determine an upper bound for its proof-theoretic strength. We hope to be able soon to present the corresponding well-ordering proof, which shows that this bound is sharp.

Related work. As pointed out in Subsect. 2.1, G. Jäger and T. Strahm have introduced in [23] a Π_{3}-reflecting universe in the context of Feferman’s systems of explicit mathematics. Because this is a theory which allows partial applications, they can develop their approach by using reflection of type-2 functionals, which is much simpler than the present construction, but – as we will demonstrate – not possible in a type theoretic setting. They considered only a proof theoretic analysis in a Meta-predicative setting (translated to type theory this means that the W-type is omitted), so the proof theoretic ordinal is well below the Bachmann-Howard ordinal.

This work is heavily inspired by M. Rathjen’s and T. Arai’s proof theoretic analysis of Π_{3}-reflection ([33, 35] and [2, 3, 6, 10]) – the Π_{3}-reflecting universe mimics the ordinal notation systems of that strength. Without their work it would have been difficult to discover this model construction.

Acknowledgements. This research benefited very much from intensive discussions with both T. Arai and M. Rathjen, whose research we deeply admire.

2 The Autonomous Mahlo Universe

2.1 Problems with a Naïve Approach Towards Π_{3}-Reflection

If one considers the steps taking from the simple universe (corresponding to one recursively inaccessible) via a super universe to the Mahlo universe, one observes that a simple universe is a universe closed only under the universe constructions; a super universe (V, T_{V}) contains additionally for every a : IFam(V, T_{V})^{2} a universe containing a; a Mahlo universe (V, T_{V}) contains additionally for every f : IFam(V, T_{V}) → IFam(V, T_{V}) a subuniverse closed under f. If we consider no reflection as reflection of type-(−1) functionals, we see that we have introduced universes reflecting type-(−1), type-0 and type-1 functionals.

2IFam(U, T) := (x : U) × (T (x) → U), the set of internal families of sets in (V, T_{V}); see Def. 4.1 (b) of [50].

One might expect that the next step is to form a universe (V, T_{V}) which reflects type-2 functionals, i.e. a universe such that for every

F : (IFam(V, T_{V}) → IFam(V, T_{V})) → IFam(V, T_{V})

there is a subuniverse closed under F. One might experiment with the precise type of F, e.g. replacing it by the type of functions, mapping families of functions from IFam(V, T_{V}) into itself to other such families, i.e.

IFam′(V, T_{V}, IFam(V, T_{V}) → IFam(V, T_{V}))
→ IFam′(V, T_{V}, IFam(V, T_{V}) → IFam(V, T_{V})) ,

where IFam′(A, B, C) := (a : A) × (B(a) → C). However, the general form of being essentially a type-2 functional remains the same. The problem is that it is not possible to define what it means to form a universe closed under F. When forming a universe, containing a family of sets, we simply add codes for those elements to it. When forming a recursive subuniverse (U, T_{U})^{3} of a universe (V, T_{V}) closed under a function f : IFam(V, T_{V}) → IFam(V, T_{V}), one uses the fact that every element a : IFam(U, T_{U}) can be lifted to an element of IFam(V, T_{V}). Then f can be applied, and all one needs is to form codes for the resulting elements in U. If one however takes an F : (IFam(V, T_{V}) → IFam(V, T_{V})) → IFam(V, T_{V}), we have the problem that we can no longer in general lift a function f : IFam(U, T_{U}) → IFam(U, T_{U}) to a function f′ : IFam(V, T_{V}) → IFam(V, T_{V}). But such an f′ would be needed in order to be able to apply F to it and to obtain therefore an element of IFam(V, T_{V}), for which we then introduce a code in IFam(U, T_{U}).

In a setting with partiality such as Feferman’s theory of explicit mathematics G. Jäger and T. Strahm have shown in [23] how to overcome this problem. There one uses the fact that the F as above can always be applied to f. (One should note that the type of F used in [23] is slightly different – we try to stay in this discussion as close as possible to type theory.) The result might be defined or not. Now for the Π_{3}-reflecting universe one demands that F (f) is a defined element of IFam(V, T_{V}) for any f : IFam(U, T_{U}) → IFam(U, T_{U}). The resulting elements of V are then added to U. This gives a very short formulation of a Π_{3}-reflecting universe.

There is a drawback, namely that one needs to assume that certain “ghost” elements enter U, which makes the theory not as explicit as one would like to have it in a constructive framework. What happens is that if one looks at F as being a continuous function, one finds out that in order to evaluate F on a given function f, f is not used as a whole, but needs to be evaluated only for certain elements of V (the choice of values depends on f). Indirectly the reflection of F demands now that if we have f : IFam(U, T_{U}) → IFam(U, T_{U}), all elements needed in order to obtain a defined value for F (f) must have already been elements of U. So when defining a Π_{3}-reflecting universe, these elements need to be elements of U, but are not constructed explicitly.

3See Subsect. 2.5 of [50], paragraph “Type theories with several universes” for details on the notions of recursive vs. inductive subuniverses. We repeat this briefly: 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 we need to have an element of V already defined. In an inductive universe, one has a recursively defined function T_{U} : U → Set. T̂_{U} : U → V is a constructor of V, with equality rule T_{V}(T̂_{U}(x)) = T_{U}(x).

So one can define new elements a of U, whether they already correspond to elements in V or not, as long as one defines T_{U}(a).

We consider here an example: Consider for a fixed element a : IFam(V, T_{V}) the functional F := λf.⟨π_{0}(f(a)), (y)N̂_{1}⟩ : (IFam(V, T_{V}) → IFam(V, T_{V})) → IFam(V, T_{V}). That (U, T_{U}) is closed under F means that any function f : IFam(U, T_{U}) → IFam(U, T_{U}) can be applied to a as well. Now, assume a is not an element of IFam(U, T_{U}). Then define f which checks whether the argument is equal to a. If yes it returns an element which doesn’t belong to any universe, say 17. Otherwise it returns ⟨N̂_{1}, (x)N̂_{1}⟩.^{4} f : IFam(U, T_{U}) → IFam(U, T_{U}), but F (f) returns an element which cannot be in U. So we are forced to add a to IFam(U, T_{U}).

It turns out that in proof theory there is a similar problem as in type theory: the collapsing technique allows only to deal with Π_{2}-reflections, or more generally with Π_{2}-statements. When M. Rathjen in his famous paper [35] (see as well [33]) analysed Π_{3}-reflection^{5}, he had to decompose Π_{3}-reflection into a sequence of Π_{2}-steps. This paper was the main inspiration for our Π_{3}-reflecting universe, which we will present in the following – what we will do is to replace type-2 functionals (as the F above) by a combination of type-1 functionals.

2.2 Steps Towards the Autonomous Mahlo Universe

We will introduce the Π_{3}-reflecting universe in several steps: First we consider the formulation of a hyper-Mahlo universe. Then we consider hyper^{α}-Mahlo universes. Next we consider an autonomous Mahlo universe, corresponding to an ordinal κ which is recursively hyper^{κ}-Mahlo. And finally we will introduce in Sect. 3 the Π_{3}-reflecting universe.

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 [50]): A hyper-Mahlo universe is a universe (U_{2}, T_{2}) such that for ever f : IFam(U_{2}, T_{2}) → IFam(U_{2}, T_{2}) there exists a subuniverse U_{1,f} represented in U_{2} such that U_{1,f} is a Mahlo universe closed under f. That U_{1,f} with its decoding function T_{1,f} is a Mahlo universe means that for every g : IFam(U_{1,f}, T_{1,f}) → IFam(U_{1,f}, T_{1,f}) there exists a subuniverse U_{0,f,g} of U_{1,f} closed under g and represented in U_{1,f}. If one wants to define U_{1,f} as a recursive subuniverse of U_{2}, one has one small problem, that one needs to have a code for U_{0,f,g} in U_{2}. But it is straightforward to introduce such a code there (in the final version one would do a similar step as for the Mahlo universe and uncurry f and g and split each of them into two functions^{6}).

4Here we of course assume that our language is strong enough to define such a function and one might argue that one shouldn’t be able to define such functions. (Note that such functions are very natural in the framework of explicit mathematics, which is different from type theory, where elimination rules for the Mahlo universe already result in an inconsistency – when adding such constants to explicit mathematics one doesn’t make any assumptions about their definedness as a function, so they shouldn’t carry any ontological meaning.) But this means that one has a restriction on the language, and a theory should allow for extensions of the language by new constants. Even if one says that such extensions are forbidden, one sees here the high dependency of the theory on the function space.

5The same step was taken by Arai in his analysis of Π_{3}-reflection.

f : IFam(U_{2}, T_{2}) → IFam(U_{2}, T_{2})  g : IFam(U_{1,f}, T_{1,f}) → IFam(U_{1,f}, T_{1,f})
Û_{0,2,f,g} : U_{2}
T_{2}(Û_{0,2,f,g}) = U_{0,f,g}

We leave it to the reader to spell out the rules for such a universe in detail and to model it in Kripke-Platek set theory, extended by one recursively hyper-Mahlo ordinal and finitely many admissibles above it.

The hyper^{α}-Mahlo universe. A hyper^{α}-universe is a universe (U^{α}, T^{α}), such that for every β < α and f : IFam(U^{α}, T^{α}) → IFam(U^{α}, T^{α}) there exists a hyper^{β}-sub-universe of (U^{α}, T^{α}), closed under f and represented in U^{α}. It is again straightforward to formulate a type theory with one hyper^{α}-Mahlo universe in detail. The only difference is that we get the problem of having chains of universes of unbounded depth, which causes problems when using recursive subuniverses.^{7} The solution is to introduce U^{β} as an inductive rather than recursive subuniverse of U^{α} (β < α). A similar construction would be done if one would like to formulate hyper^{α}-super universes (see the beginning of Subsect. 5.1 of [50]). 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.

2.3 The Autonomous Mahlo Universe

The next step is to define a universe (V, T_{V}) which has strength (KPω + (Aut − Mahlo))^{+}. Here (KPω + (Aut − Mahlo))^{+} 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. We can replace the ordinals α < κ needed in order to form hyper^{α}-Mahlo universes by elements of Deg = Wv : V.T_{V}(v). This means that we have for every w : Deg a set of inductive subuniverses Univ_{w} of V of that degree. For every f : IFam(V, T_{V}) → IFam(V, T_{V}) and every degree w there exists a universe in Univ_{w} closed under f. Furthermore, if w = sup(a, b), where a : V and b : T_{V}(a) → Deg, c : T_{V}(a), and w′ := b(c), then any universe in Univ_{w} is Mahlo reflecting in Univ_{w′}: If (U, T_{U}) is a universe in Univ_{w}, f : IFam(U, T_{U}) → IFam(U, T_{U}), then there exists an inductive subuniverse of (U, T_{U}) in Univ_{w′} closed under f and represented in U.

6See the formation rule for U_{f,g} in Subsect. 5.1 of [50]. What one does is to replace f : IFam(U_{2}, T_{2}) → IFam(U_{2}, T_{2}) by two functions f_{1} : (x : U_{2}, T_{2}(x) → U_{2}) → U_{2} and f_{2} : (x : U_{2}, y : T_{2}(x) → U_{2}, T_{2}(f_{1}(x, y))) → U_{2}, similarly for g.

7See Subsect. 2.5 of [50] for a discussion on why recursive subuniverse cause problems when forming unbounded chains of subuniverses. In short, the problem is that when using chains of recursive subuniverses, one needs to add to the uppermost universe codes for all nested subuniverses, which is technically difficult to achieve.

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 seen 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 f : (Wx : T_{V}(a).T_{V}(b(x))) → Wx : V.T_{V}(x), f(sup(r, s)) = sup(b(r), (y)f(s(y))). Then d = f(d′) for some d′ : (Wx : T_{V}(a).T_{V}(b(x))).

Therefore the set of degrees depend 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.

It turns out that we don’t need any elimination rules for Deg. This is 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 of Wx : V.T_{V}(x).

We therefore obtain now the following rules for the type theory with one autonomous Mahlo universe:

• Preliminaries. We will always determine, which sets are defined inductively, and which sets are defined recursively. So elements of the inductively defined sets are given by constructors, and whenever we introduce a new element we have to determine the values of the recursively defined functions. This notion is inspired by the notion of inductive-recursive definitions ([14, 16, 17, 18, 19]), although this construction is not an inductiverecursive definition. (Already the Mahlo universe construction, which is one of the main ingredients of this construction, goes beyond inductionrecursion.)

• Basic type theory. We have the rules for the small logical framework and for the basic set constructions.^{8} In the following we introduce the rules for the sets specific to the autonomous Mahlo universe.

• Formation rules.

8The basic set constructions are N, N_{k}, +, Π, Σ, W, Id, and their rules. The small logical framework consists of the dependent function type (x : A) → B and the dependent product (x : A) × B, restricted to Set. See Sect. 2.1 of [50] for details.

– Formation rules for V, T_{V} (V is defined inductively, T_{V} recursively):

V : Set  \begin{matrix}a : V \\ T_{V}(a) : Set \end{matrix}

– Formation rule for Deg. Every d : Deg has a branching degree bdeg(d) : V and for every a : T_{V}(bdeg(d)) subdegrees subdeg(d, a), which are both defined recursively:

Deg : Set
bdeg : Deg → V
subdeg : (d : Deg, a : T_{V}(bdeg(d)) → Deg

– Formation rule for Univ, and for the universes (U_{d,u}, T_{U,d,u}) in Univ_{d}. Univ_{d} and U_{d,u} are defined inductively, T_{U,d,u} is defined recursively:

d : Deg ; Univ_{d} : Set
d : Deg  u : Univ_{d}
U_{d,u} : Set
d : Deg u : Univ_{d} a : U_{d,u}
T_{U,d,u}(a) : Set

• Introduction rules and equality rules for the recursively defined functions:

– We have standard rules expressing that (V, T_{V}) is a universe.

– We have standard rules expressing that (U_{d,u}, T_{U,d,u}) is a universe.

– Introduction rule for Deg:

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

– (U_{d,u}, T_{U,d,u}) is an inductive subuniverse of V. These rules form introduction rules for V. Assume d : Deg, u : Univ_{d}.

\begin{matrix}a : U_{d,u} \\ T̂_{U,d,u}(a) : V \end{matrix}

T_{V}(T̂_{U,d,u}(a)) = T_{U,d,u}(a)

– U_{d,u} is represented in V.^{9} Assume d : Deg, u : Univ_{d}.

Û_{U,d,u} : V  T_{V}(Û_{U,d,u}) = U_{d,u}

9As I learned from Peter Hancock, who has worked a lot on families of sets (see e.g. [21]), the above means that the successor of (U_{d,u}, T_{U,d,u}) is a subfamily of (V, T_{V}), where the successor of a family of sets (A, B) is the family of sets (A + N_{1}, B′) where B′(inl(a)) = B(a), B′(inr(A_{0}^{1})) = A.

– Every function in IFam(V, T_{V}) → IFam(V, T_{V}) is reflected in a universe in Univ_{d} for every d : Deg. (f will as usual be split into two functions).

∗ We obtain the following introduction rule for Univ_{d}:

d : Deg
f : (a : V, T_{V}(a) → V) → V
g : (a : V, T_{V}(a) → V, T_{V}(f(a, b)) → V
v_{d,f,g} : Univ_{d}

∗ Assume d, f, g as in the premises for that rule. Let temporarily in this item only

v_{−} := v_{d,f,g}  : Univ_{d} ,
U_{−} := U_{d,v_{−}}  : Set ,
T_{−}(a) := T_{U,d,v_{−}}(a) : Set  (where a : U_{−}) ,
T̂_{−}(a) := T̂_{U,d,v_{−}}(a) : V  (where a : U_{−}) .

The closure of (U_{−}, T_{−}) under f, g is given by the following introduction rules for U_{−}:

f̂_{v,d,f,g} : (a : U_{−}, b : T_{−}(a) → U_{−}) → U_{−}
T_{−}(f̂_{v,d,f,g}(a, b)) = T_{V}(f(T̂_{−}(a), T̂_{−} ∘ b))

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

→ U_{−}
T_{−}(ĝ_{v,d,f,g}(a, b, c)) = T_{V}(g(T̂_{−}(a), T̂_{−} ∘ b, c))

– Assume d : Deg, u : Univ_{d}, c : T_{V}(bdeg(d)). Let temporarily in this item only

U_{+} := U_{d,u}  : Set ,
T_{+}(a) := T_{U,d,u}(a) : Set (where a : U_{+}) ,
d_{−} := subdeg(d, c) : Deg .

Then every function f : IFam(U_{+}, T_{+}) → IFam(U_{+}, T_{+}) is reflected in an inductive subuniverse of (U_{+}, T_{+}) which is in Univ_{d_{−}}. As usual f will be split into two functions. So assume

f : (a : U_{+}, b : T_{+}(a) → U_{+}) → U_{+} ,
g : (a : U_{+}, b : T_{+}(a) → U_{+}, T_{+}(f(a, b))) → U_{+} .

∗ We have the following introduction rule for Univ_{d_{−}}:

u_{d,u,c,f,g} : Univ_{d_{−}} Let

u_{−} := u_{d,u,c,f,g}  : 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_{+}), as expressed by the following introduction and equality rule for U_{+}:

\begin{matrix}a : U_{−} \\ T̂_{u,d,u,c,f,g}(a) : U_{+} \end{matrix}  T_{+}(T̂_{u,d,u,c,f,g}(a)) = T_{−}(a)

Let for a : U_{−}

T̂_{−}(a) := T̂_{u,d,u,c,f,g}(a) : U_{+} .

∗ (U_{+}, T_{+}) is closed under f, g as expressed by the following introduction rules for U_{−}:

f̂_{u,d,u,c,f,g} : (a : U_{−}, b : T_{−}(a) → U_{−}) → U_{−}
T_{−}(f̂_{u,d,u,c,f,g}(a, b)) = T_{+}(f(T̂_{−}(a), T̂_{−} ∘ b))
ĝ_{u,d,u,c,f,g} : \begin{matrix}(\begin{matrix}a : U_{−}, \\ b : T_{−}(a) → U_{−}, \\ T_{+}(f(T̂_{−}(a), T̂_{−} ∘ b))) \end{matrix} \\ → U_{−} \end{matrix}

T_{−}(ĝ_{u,d,u,c,f,g}(a, b, d)) = T_{+}(g(T̂_{−}(a), T̂_{−} ∘ b, d))

∗ Finally U_{−} is represented in U_{+}. So we have the following introduction and equality rule for U_{+}:

Û_{u,d,u,c,f,g} : U_{+}  T_{+}(Û_{u,d,u,c,f,g}) = U_{−}

We will not spell out a model for the autonomous Mahlo universe in Kripke-Platek set theory plus the existence of a κ which is recursively hyper^{κ}-Mahlo and finitely many admissibles above it. The details will be carried out in a future paper.

3 The Π_{3}-Reflecting Universe

3.1 Motivation

When defining the autonomous Mahlo universe, the notion of a Mahlo degree (the set Deg) emerged. The set of subdegrees (given by bdeg(d) and subdeg(d, b)) do not depend on a universe in Univ_{d}.

We want to extend the degree structure (Deg, bdeg, subdeg) to a new structure, in which we can associate a degree to the autonomous Mahlo universe itself. We want to use the same names Deg, bdeg, subdeg as before, but now with different types which reflect the new dependencies.

If we want to associate with the autonomous Mahlo universe (V, T_{V}) a degree d, we see that the set of subdegrees of d should be Wx : V.T_{V}(x) or a set related to this. This is problematic since it is a set which depends on the whole universe (V, T_{V}).

We have however seen already that any w : (Wx : V.T_{V}(x)) depends only on a small subset of V, i.e. a subset of V indexed by an element of V. Therefore the set of subdegrees of d can be approximated fully by referring to restrictions of Wx : V.T_{V}(x) to the set of trees over a small subset ⟨a, b⟩ : IFam(V, T_{V}), i.e. to Wx : T_{V}(a).T_{V}(b(x)). This makes this a “good” set of subdegrees: the set of subdegrees depends only locally on V. So every subdegree will be available at some point during the construction of V – we don’t have to wait until all of V is constructed.

We want to generalise this notion of a local dependency to our new set of degrees Deg. Then the set of subdegrees of elements of Deg depends on a family of elements of (V, T_{V}). So the index set for the subdegrees bdeg and the subdegrees subdeg of an element Deg have types

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

We will (once we have defined the introduction rules for Deg) be able to determine for every element w : (Wx : V.T_{V}(x)) a Mahlo degree f(w) : Deg such that

bdeg(f(sup(a, b)), c, d) = a ,
subdeg(f(sup(a, b)), c, d, e) = f(b(e)) .

So the old degrees are specific in the sense that bdeg and subdeg do not depend on c, d. With the autonomous Mahlo universe we associate the Mahlo degree m : Deg such that

bdeg(m, c, d) = Ŵ_{V}x : c.d(x) ,
subdeg(m, c, d, e) = f(g(c, d, e)) ,

where

g : (c : V, d : T_{V}(c) → V) → (Wx : T_{V}(c).T_{V}(d(x))) → (Wx : V.T_{V}(x))

is the embedding defined recursively by

g(c, d, sup(a, b)) = sup(d(a), (x)g(c, d, b(x)) ,

and f is as before the embedding of Wx : V.T_{V}(x) into Deg. The remaining structure is essentially the same as for the autonomous Mahlo universe, except that we need, when forming subdegrees, to refer to a family of elements of the subuniverse one is constructing.

The main other difference is the introduction rule for Deg. This rule says now that everything, for which we can define bdeg and subdeg is an element of Deg. In full this means:

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

Define for A : Set, B : A → Set, C : Set^{10}

IFam′(A, B, C) := (a : A) × (B(a) → C) : Set .

Then we see that the above means essentially that for every

f : IFam(V, T_{V}) → IFam′(V, T_{V}, Deg)

we get a new element of Deg. The constructor deg depends negatively on V, which is defined simultaneously with Deg. We have here a similar principle as the Mahlo principle, which allows to introduce subuniverses of a Mahlo universe (V, T_{V}) closed under f : IFam(V, T_{V}) → IFam(V, T_{V}). Here we use the Mahlo principle in order to introduce new Mahlo degrees, i.e. new elements of Deg.

3.2 Rules for the Π_{3}-reflecting universe.

Since this is the main type theory introduced in this article, we will spell out the rules of the Π_{3}-reflecting universe in detail:

• Basic type theory: We have the rules for the small logical framework and for the basic set constructions. In the following we introduce the rules for the sets specific to the Π_{3}- reflecting universe.

• Formation rules.

– Formation rules for V, T_{V} (V is defined inductively, T_{V} recursively):

V : Set  \begin{matrix}a : V \\ T_{V}(a) : Set \end{matrix}

– Formation rule for Deg. Deg is defined inductively, bdeg and subdeg are defined recursively:

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

– Formation rule for Univ, and for the universes (U_{d,u}, T_{U,d,u}) in Univ_{d}. Univ_{d} and U_{d,u} are defined inductively, T_{U,d,u} is defined recursively:

10The following definition was already introduced in Subsect. 2.1.

d : Deg ; Univ_{d} : Set
d : Deg  u : Univ_{d}
U_{d,u} : Set

d : Deg  u : Univ_{d}  a : U_{d,u}
T_{U,d,u}(a) : Set

• Introduction rules and equality rules for the recursively defined functions:

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

N̂_{V} : V  T_{V}(N̂_{V}) = N

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

Similarly for the other basic set constructions N_{n}, +, Π, W, Id.

– Rules expressing that (U_{d,u}, T_{U,d,u}) is a universe: Assume d : Deg, u : Univ_{u}:

N̂_{U,d,u} : U_{d,u}  T_{U,d,u}(N̂_{U,d,u}) = N

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

T_{U,d,u}(Σ̂_{U,d,u}(a, b)) = Σx : T_{U,d,u}(a).T_{U,d,u}(b(x))

Similarly for the other basic set constructions N_{n}, +, Π, W, Id.

– Introduction rule for Deg:

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

– (U_{d,u}, T_{U,d,u}) is an inductive subuniverse of V. These rules form introduction rules for V. Assume d : Deg, u : Univ_{d}.

\begin{matrix}a : U_{d,u} \\ T̂_{U,d,u}(a) : V \end{matrix}  T_{V}(T̂_{U,d,u}(a)) = T_{U,d,u}(a)

– U_{d,u} is represented in V. Assume d : Deg, u : Univ_{d}.

Û_{U,d,u} : V  T_{V}(Û_{U,d,u}) = U_{d,u}

– Every function IFam(V, T_{V}) → IFam(V, T_{V}) is reflected in a universe in Univ_{d} for every d : Deg (as usual f will be split into two functions):

∗ We obtain the following introduction rule for Univ_{d}:

d : Deg
f : (a : V, T_{V}(a) → V) → V
g : (a : V, T_{V}(a) → V, T_{V}(f(a, b)) → V
v_{d,f,g} : Univ_{d}

∗ Assume d, f, g as in the premises for the previous rule. Let temporarily in the definition of the rules for v_{d,f,g} only

v_{−} := v_{d,f,g}  : Univ_{d} ,
U_{−} := U_{d,v_{−}}  : Set ,
T_{−}(a) := T_{U,d,v_{−}}(a) : Set  (where a : U_{−}) ,
T̂_{−}(a) := T̂_{U,d,v_{−}}(a) : V  (where a : U_{−}) .

The closure of (U_{−}, T_{−}) under f, g is given by the following introduction rules for U_{−}:

f̂_{U,d,f,g} : (x : U_{−}, y : T_{−}(x) → U_{−}) → U_{−}
T_{−}(f̂_{U,d,f,g}(x, y)) = T_{V}(f(T̂_{−}(x), T̂_{−} ∘ y))

ĝ_{U,d,f,g} : (\begin{matrix}x : U_{−}, \\ y : T_{−}(x) → U_{−}, \\ T_{V}(f(T̂_{−}(x), T̂_{−} ∘ y))) \end{matrix}

→ U_{−}
T_{−}(ĝ_{U,d,f,g}(x, y, z)) = T_{V}(g(T̂_{−}(x), T̂_{−} ∘ y, z))

– Assume d : Deg, u : Univ_{d}. Let temporarily in this item only

U_{+} := U_{d,u}  : Set ,
T_{+}(a) := T_{U,d,u}(a) : Set (where a : U_{+}) ,
T̂_{+}(a) := T̂_{U,d,u}(a) : V  (where a : U_{+}) .

Assume a : U_{+} b : T_{+}(a) → U_{+}. Let

a_{V} := T̂_{+}(a)  : V ,
b_{V} := (x)T̂_{+}(b(x)) : T_{V}(a_{V}) → V .

Assume c : T_{V}(bdeg(d, a_{V}, b_{V})). Let temporarily in this item only

d_{−} := subdeg(d, a_{V}, b_{V}, c) : Deg .

Then every function f : IFam(U_{+}, T_{+}) → IFam(U_{+}, T_{+}) is reflected in an inductive subuniverse of (U_{+}, T_{+}) which is in Univ_{d_{−}} (as usual f will be split into two functions). So assume

f : (a : U_{+}, b : T_{+}(a) → U_{+}) → U_{+} ,
g : (a : U_{+}, b : T_{+}(a) → U_{+}, T_{+}(f(a, b))) → U_{+} .

∗ We have the following introduction rule for Univ_{d_{−}}:

u_{d,u,a,b,c,f,g} : Univ_{d_{−}}

∗ Let

u_{−} := u_{d,u,a,b,c,f,g} : 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_{+}), as expressed by the following introduction and equality rule for U_{+}:

\begin{matrix}a : U_{−} \\ T̂_{u,d,u,a,b,c,f,g}(a) : U_{+} \end{matrix}  T_{+}(T̂_{u,d,u,a,b,c,f,g}(a)) = T_{−}(a)

Let for a : U_{−}

T̂_{−}(a) := T̂_{u,d,u,a,b,c,f,g}(a) : U_{+} .

∗ That (U_{+}, T_{+}) is closed under f, g is expressed by the following introduction rules for U_{−}:

f̂_{u,d,u,a,b,c,f,g} : (x : U_{−}, y : T_{−}(x) → U_{−}) → U_{−}
T_{−}(f̂_{u,d,u,a,b,c,f,g}(x, y)) = T_{+}(f(T̂_{−}(x), T̂_{−} ∘ y))
ĝ_{u,d,u,a,b,c,f,g} : \begin{matrix}(\begin{matrix}x : U_{−}, \\ y : T_{−}(x) → U_{−}, \\ T_{+}(f(T̂_{−}(x), T̂_{−} ∘ y))) \end{matrix} \\ → U_{−} \end{matrix}

T_{−}(ĝ_{u,d,u,a,b,c,f,g}(x, y, z)) = T_{+}(g(T̂_{−}(x), T̂_{−} ∘ y, z))

∗ Finally U_{−} is represented in U_{+}. So we have the following introduction and equality rule for U_{+}:

Û_{u,d,u,a,b,c,f,g} : U_{+}  T_{+}(Û_{u,d,u,a,b,c,f,g}) = U_{−}

We call the resulting type theory ML_{W} + (Π_{3} − refl).

4 A Model of the Π_{3}-Reflecting Universe

4.1 The Basic Idea of the Model

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 [50]. We repeat here the most important ones:

• Terms are interpreted as slightly reduced 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 [50]) [[ A]]_{ρ}, where ⟨a, b⟩ ∈ [[ A]]_{ρ} means that a and b are equal elements of [[ A]]_{ρ}. Flat([[ A]]_{ρ}) is the underlying set of terms, i.e. since [[ A]]_{ρ} is a PER, Flat([[ A]]_{ρ}) = {a | ⟨a, a⟩ ∈ [[ 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 ∈ Flat(A) to Flat(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 ∈ Flat(A) and b ∈ Flat(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 ∈ Flat(U) and b ∈ Flat(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 .

These two sets form the two components of the set of functions

[[ IFam ]](U, T) [[ →]] [[ IFam ]](U, T) .

Π_{N}-reflecting ordinals (see [35]). A transitive and non-empty set a is Π_{N}- reflecting, if for any Π_{N}-formula φ in the language of Kripke-Platek set theory with parameters in a we have

a ⊧ φ → ∃z(trans(z) ∧ z ≠ ∅ ∧ φ^{z}) (∗)

where φ^{z} is the result of replacing in φ any unbounded quantifier ∃y, ∀y by ∃y ∈ z, ∀y ∈ z respectively, and trans(z) is the formula expressing that z is transitive. An ordinal α > 0 is Π_{N}-reflecting if L_{α} is Π_{N}-reflecting.

(KPω + (Π_{3} − refl))^{+} is the theory consisting of the axioms of Kripke-Platek set theory with infinity, and axioms expressing that there exists a constant a_{P} s.t. a_{P} is Π_{3}-reflecting, and constants b_{n} for Meta-natural numbers n and axioms Ad(b_{n}), a_{P} ∈ b_{0} and b_{n} ∈ b_{n+1}.

As shown in [38], Theorem 1.9. (iv), the z, which reflects a Π_{N}-formula in (∗), can, in case of N ≥ 3, be chosen to be admissible, and for a Π_{N}-reflecting ordinal P for N ≥ 2 we have that P is admissible. We cannot show Ad(z) and Ad(L_{P}), since the axioms of our formulation of Kripke-Platek set theory state only that, if Ad(u) holds, then u fulfils the axioms of being admissible, not the other way around. However, as stated in [38], Theorem 2.4, there exists a Π_{3}-formula Ãd(x) such that a transitive set x ≠ 0 is admissible, if Ãd(x) holds, and we can guarantee z to fulfil Ãd(z), and P always fulfils Ãd(L_{P}). One easily sees that Theorem 3.3^{11} and Lemma 3.4^{12} of [50] hold, if one replaces Ad by Ãd.

Basic Ideas. The general idea for constructing models is as in Subsect. 3.2 of [50]: One defines by recursion on α (V^{α}, T^{α}) ∈ [[ Fam ]](Set) fulfilling Assumption 3.2. of [50] by closing V^{α} under the basic set constructions and adding codes for universes, 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^{P} and [[ T(a) ]]_{ρ} := T^{P}([[ a]]_{ρ}) for a Π_{3}-reflecting ordinal P.

Therefore the main task is to define when (V^{β}, T^{β}) is sufficiently closed so that it can be used as an interpretation of a subuniverse of (V, T_{V}) of appropriate Mahlo degree.

A problem when dealing with the Π_{3}-reflecting universe is that the set Deg depends on the whole universe, so [[ Deg ]] can be defined only when [[ V ]] is complete. This is similar to the initial problem we had with modelling the Mahlo universe in [50], namely 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 Π_{3}-reflecting universe codes v_{d,f,g} to our universe, using only the fact that f, g are locally defined and that d is a local degree. 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}. For instance, we will have the reduction rule u_{d,u,a,b,c,f,g} ⟶ v_{d_{−},f,g} where d_{−} = subdeg(d, a, b, c). This means of course that when we derive in the type theory u : Univ_{d} and have [[ u]] = v_{d′,f,g}, it is not necessarily the case that f, g are total on V: if u = u_{d′′,u,a,b,c,f,g}, 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_{V}, b_{V}, c) : Deg, therefore in the model d′ is an element of [[ Deg ]] – roughly speaking d′ is a “total degree”.

As for the model of the super and the Mahlo universe in [50], we will not start defining at each stage α the least subuniverse of V^{<α} closed under the constructions needed but only check whether for some β < α V^{<β} is sufficiently closed. This reduces the technical work to be carried out.

11Which says essentially that under [50], Assumption 3.2, if κ is recursively inaccessible, then U^{<κ} is closed under the basic set constructions. Here Assumption 3.2 expresses roughly that (V^{α}, T^{α}) are increasing, PERs, closed under reductions, well-behaved w.r.t. definability, and contain at least the one step application of basic set operations to previously defined sets.

12Which says that under [50], Assumption 3.2, if κ is admissible, then a family of sets internal to U^{<κ} is already a family in U^{<α} for some α < κ.

We could define now at each stage α first the set of local degrees on V^{<α}. We could do so by defining the least set Deg^{<α} such that, if

f : IFam(V^{<α}, T^{<α}) → IFam′(V^{<α}, T^{<α}, Deg^{<α}) ,

then deg(f) ∈ Deg^{<α} (or more precisely the corresponding statement in the model; see Subsect. 2.1 for the definition of IFam′(A, B, C)). More precisely we would have to divide f into its two components.

But this would create a lot of overhead. All we need is that V^{<α} is closed under all subuniverses which we can define from v_{d,f,g}. This means that for ⟨a, b⟩ ∈ [[ IFam ]](V^{<α}, T^{<α}) we have that bdeg(d, a, b) ∈ V^{<α} and that for all c ∈ T^{<α}(bdeg(d, a, b)), which gives us a subdegree d_{−} := subdeg(d, a, b, c) of d, and for all functions f′, g′ from families of elements in V^{<α} to families of elements in V^{<α} we have that v_{d_{−},f′,g′} is in V^{<α}.

This gives us the inductive definition of V^{α}, T^{α}, and, as stated above, we define [[ V ]] := V^{<P}, [[ T_{V} ]] := T^{<P}, where P is a Π_{3}-reflecting ordinal.

[[ 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.) We will not define Flat([[ Deg ]]) as the least set closed under deg. Instead we define Flat([[ Deg ]]) as the set of d such that for all functions f, g from families of [[ V ]] into families of [[ V ]] we have v_{d,f,g} is in [[ V ]]. Therefore we have trivially the closure of V under the formation of v_{d,f,g}, but have to show that Deg is closed under its introduction rule, given by the constructor deg. This will require the use of the fact that P is Π_{3}-reflecting.

4.2 Formal Definition of the Model

We will work in (KPω + (Π_{3} − refl))^{+} which is, as stated above, Kripke-Platek set theory plus the existence of one Π_{3}-reflecting ordinal and finitely many admissibles above it. Proof-theoretically equivalent is the theory KPl^{r} plus the existence of one Π_{3}-reflecting ordinal. Let P be the Π_{3}-reflecting ordinal which we know does exist.

The set of terms in the model. As for all models of type theory in [50], 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 subsets. Therefore Û_{U,d}, T̂_{U,d,u}, T̂_{u,d,u,a,b,c,f,g} will be treated as if they were identity functions, and Û_{u,d,u,a,b,c,f,g} will be identified with u_{d,u,a,b,c,f,g} So we have the following reduction rules:

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

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

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

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

f̂_{U,d,f,g}(x, y) ⟶ f(x, y) ,
f̂_{u,d,u,a,b,c,f,g}(x, y) ⟶ f(x, y) ,
ĝ_{U,d,f,g}(x, y, z) ⟶ g(x, y, z) ,
ĝ_{u,d,u,a,b,c,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,b,c,f,g}, but one sees immediately that there are indeed no problems.)

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

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

Definition of V^{α}, T^{α}. As for the super and Mahlo universe in [50], we define (V^{α}, T^{α}) ∈ [[ Fam ]](Set) by closing it under the standard set constructions. We will then interpret [[ V ]] = V^{<P}, [[ T_{V} ]] = T^{<P}.

Instead of closing it under Û_{f,g} – as for the model for the Mahlo universe – we close it now under v_{d,f,g} as follows. We first introduce what it means for a family of sets to be closed under d:

Definition 4.1 (a) 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′)⟩:

⟨(x, y)bdeg(d, x, y), (x, y)bdeg(d′, x, y)⟩ ∈ [[ IFamOper ]]_{0}(U, T)

(2) U is closed under the formation of subuniverses for subdegrees of d, d′: Assume a, b, a′, b′, c, c′, f̃, f̃, g̃, g′ ∈ [[ Term ]] such that the following holds:

– ⟨⟨a, b⟩, ⟨a′, b′⟩⟩ ∈ [[ IFam ]](U, T),

– ⟨c, c′⟩ ∈ T (bdeg(d, a, b)), – d_{−} := subdeg(d, a, b, c), d_{−}′ := subdeg(d′, a′, b′, c′),

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

(b) Assume (U, T) ∈ [[ Fam ]](Set), and that U is closed under N_{1} and +, i.e. that the following following holds: We have N̂_{1} ∈ U and T (N̂_{1}) = [[ N_{1} ]]; for a, b ∈ Flat(U) we have aˆ+b ∈ Flat(U) and T (aˆ+b) = T (a)[[ + ]]T (b); we have that if ⟨a, a′⟩, ⟨b, b′⟩ ∈ U then ⟨aˆ+b, a′ ˆ+b′⟩ ∈ U. Furthermore, assume ⟨a, b⟩, ⟨c, d⟩ ∈ Flat([[ IFam ]](U, T)). Then we define

• S_{[[ IFam ]](U,T)}(⟨a, b⟩) := ⟨aˆ+N̂_{1}, b′⟩ ∈ Flat([[ IFam ]](U, T)).

Here b′(inl(x)) = b(x), b′(inr(A_{0}^{1})) = a. Remember that A_{0}^{1} is the canonical element of N_{1}. So S_{[[ IFam ]](U,T)}(⟨a, b⟩) is the successor of ⟨a, b⟩, which contains both all sets b(x) for x ∈ T (a), and a code for a itself.

• ⟨a, b⟩ ∪_{[[ IFam ]](U,T)} ⟨c, d⟩ := ⟨aˆ+c, e⟩ ∈ Flat([[ IFam ]](U, T)). Here e(inl(x)) = b(x), e(inr(x)) = d(x). So ⟨a, b⟩ ∪_{[[ IFam ]](U,T)} ⟨c, d⟩ is the union of the two families of sets ⟨a, b⟩ and ⟨c, d⟩.

• ⟨a, b⟩ ∪_{[[ IFam ]](U,T)}^{S} ⟨c, d⟩ :=

S_{[[ IFam ]](U,T)}(⟨a, b⟩) ∪_{[[ IFam ]](U,T)} S_{[[ IFam ]](U,T)}(⟨c, d⟩) .

So ⟨a, b⟩ ∪_{[[ IFam ]](U,T)}^{S} ⟨c, d⟩ is the family of set containing a, c, b(x)

for x ∈ T (a), and d(x) for x ∈ T (c).^{13}

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^{<β})

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

Let β be minimal such that the above holds. Then

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

13P. Hancock suggested to split the notion ∪_{[[ IFam ]](U,T)}^{S} into two operations, first the successor operation and the union operation. In [50], Def. 5.1.(c) a similar definition for Fam(U, T) was introduced, which could in the light of P. Hancock’s comment as well be split up into the two operations.

Interpretation of the other sets. We define now for a Π_{3}-reflecting ordinal P

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

and then

[[ Deg ]]_{ρ} := \begin{cases}⟨d, d′⟩ ∈ [[ Term ]]^{2} | \\ ∀⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]]([[ V ]], [[ T_{V} ]]). \\ ⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ [[ V ]]\} . \end{cases}

[[ Univ_{d}]]_{ρ} := Closure(\begin{matrix}\{⟨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{matrix}
where d′ = [[ d]]_{ρ}.
[[ U_{d,u}]]_{ρ} := [[ T_{V} ]]([[ u]]_{ρ})
[[ T_{U,d,u}(a) ]]_{ρ} := [[ T_{V} ]]([[ a]]_{ρ})

We will need below as well the relativisation of [[ Deg ]] with (V^{<P}, T^{<P}) replaced by (V^{<α}, T^{<α}) and define therefore

[[ Deg ]]^{<α} := \begin{cases}⟨d, d′⟩ ∈ [[ Term ]]^{2} | \\ ∀⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]](V^{<α}, T^{<α}). \\ ⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ V^{<α}\} . \end{cases}

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

o(U) := P + 1 o(T_{V}(a)) := P

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

4.3 Correctness of the Model

Basic correctness. The difficult part of the model is to show that [[ Deg ]] is closed under the introduction rule for Deg. 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 these, we show the correctness of the other rules (full details will be presented in a future article, here we give only the main proof ideas):

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

• We have

[[ bdeg ]] ∈ [[ Deg ]] [[ →]] [[ IFamOper ]]_{0}([[ V ]], [[ T_{V} ]]) :

Let ⟨d, d′⟩ ∈ [[ Deg ]], ⟨a, a′⟩ ∈ [[ V ]], ⟨b, b′⟩ ∈ [[ T_{V} ]](a) → [[ V ]]. Let

f := (x, y)a , f′ := (x, y)a′ , g := (x, y, z)b(z) , f′ := (x, y, z)b′(z)

Then

⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]]([[ V ]], [[ T_{V} ]]) ,

therefore

⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ [[ V ]] .

Let

[[ T_{V} ]](v_{d,f,g}) = V^{<β} .

Then

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

But then

⟨bdeg(d, a, b), bdeg(d′, a′, b′)⟩ ∈ V^{<β} ⊆ [[ V ]]

• We have

[[ subdeg ]] ∈ (d ∈ [[ Deg ]]) [[ →]](a ∈ [[ V ]]) [[ →]](b ∈ [[ T_{V} ]](a) → [[ V ]]) [[ →]][[ T_{V} ]](bdeg(d, a, b)) [[ →]][[ Deg ]] :

Assume ⟨d, d′⟩ ∈ [[ Deg ]], ⟨a, a′⟩ ∈ [[ V ]], ⟨b, b′⟩ ∈ [[ T_{V} ]](a) → [[ V ]], ⟨c, c′⟩ ∈ [[ T_{V} ]](bdeg(d, a, b)). Let d_{−} := subdeg(d, a, b, c), d_{−}′ := subdeg(d′, a′, b′, c′). We have to show

⟨d_{−}, d_{−}′⟩ ∈ [[ Deg ]] .

In order to show this we need to prove that whenever

⟨⟨f, g⟩, ⟨f′, g′⟩⟩ ∈ [[ IFamOper ]]([[ V ]], [[ T_{V} ]])

then

⟨v_{d_{−},f,g}, v_{d_{−}′,f′,g′}⟩ ∈ [[ V ]]

So assume f, g, f′, g′ as above. Let f̃, g̃, f̃′, g′ ∈ [[ Term ]] such that module reductions

⟨f̃(x, y), g̃(x, y)⟩ = ⟨f(x, y), g(x, y)⟩ ∪_{[[ IFam ]]([[ V ]],[[ T_{V} ]])}^{S} ⟨a, b⟩ ,
⟨f̃′(x, y), g′(x, y)⟩ = ⟨f′(x, y), g′(x, y)⟩ ∪_{[[ IFam ]]([[ V ]],[[ T_{V} ]])}^{S} ⟨a′, b′⟩ .

Then

⟨⟨f̃, g̃⟩, ⟨f̃′, g′⟩⟩ ∈ [[ IFamOper ]]([[ V ]], [[ T_{V} ]])

Therefore

⟨v_{d,f̃,g̃}, v_{d′,f̃′,g′}⟩ ∈ [[ V ]]

Let V^{<β} = [[ v_{d,f̃,g̃}]]. Then

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

and therefore

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

Since [[ IFamOper ]](V^{<β}, T^{<β}) is not empty (it contains for instance ⟨⟨N̂_{1}, (x)N̂_{1}⟩, ⟨N̂_{1}, (x)N̂_{1}⟩⟩), we obtain therefore

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

But then

⟨v_{subdeg(d,a,b,c),f,g}, v_{subdeg(d′,a′,b′,c′),f′,g′}⟩ ∈ V^{<β} ⊆ [[ V ]] .

• One easily verifies that Assumption 3.2 of [50] is fulfilled with U replaced by V. Therefore, by Theorem 3.3 of [50] and the fact that Ãd(L_{P}) holds ([[ 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.

• [[ T̂_{U,d,u}(a) ]]_{ρ} ∈ Flat([[ V ]]) follows since [[ U_{d,u}]]_{ρ} ⊆ [[ V ]], and T̂_{U,d,u}(a) ⟶ a.

• The correctness of the introduction rule introducing v_{d,f,g} follows by the definition of [[ Deg ]].

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

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

• The correctness of the introduction rule introducing u_{d,u,a,b,c,f,g} follows by the definition the fact that u ∈ Flat([[ Univ_{d}]]_{ρ}) must be of the form v_{d′′,f,g} where ⟨v_{d′,f,g}, v_{d′′,f,g}⟩ ∈ [[ V ]] (d′ := [[ d]]_{ρ}), and that therefore [[ U_{d,u}]]_{ρ} = [[ T_{V} ]](v_{d′,f,g}) = [[ T_{V} ]](v_{d′′,f,g}) is closed under the formation of subuniverses.

[[ Deg ]] is closed under the introduction rule for Deg. We show directly the correctness of the equality version of that rule, which implies the correctness of the non-equality version of the rule as well. So assume

(1) ⟨r, r′⟩ ∈ [[ IFamOper ]]_{0}(V^{<P}, T^{<P}) ,

(2) ⟨s, s′⟩ ∈ (a ∈ V^{<P})

[[ →]](b ∈ (T^{<P}(a) [[ →]] V^{<P}))
[[ →]]T^{<P}(r(a, b))
[[ →]][[ Deg ]]^{<P} .

Let d := deg(r, s), d′ := deg(r′, s′). Note that, since r(x, y) = bdeg(d, x, y), s(x, y, z) = subdeg(d, x, y, z), similarly for r′ and s′, the above means that we have

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

We have to show

⟨d, d′⟩ ∈ [[ Deg ]] .

For this assume

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

We have to show

⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ V^{<P} .

We have as well

(4) ∀α < P.∃β < P.α < β ∧ Ãd(L_{β}),
(5) Ãd(L_{P}).

We show that conditions (1) - (5) can be expressed as a Π_{3}-formula

∀α < P.∃β < P.∀γ < P.φ(α, β, γ) ,

such that, if 0 < δ < P and

∀α < δ.∃β < δ.∀γ < δ.φ(α, β, γ) ,

then (1) - (5) follow with P replaced by δ.

But then we have by Theorem 3.3. of [50] that V^{<δ} is closed under the universe constructions,

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

This will imply that

⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ V^{δ+2} ⊆ V^{<P} .

Before carrying this out, let us define the following asymmetric versions of [[ IFamOper ]]:

Definition 4.2 Let (A, B), (C, D) ∈ [[ Fam ]](Set).

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

(b) Assume ⟨f, f′⟩ ∈ [[ IFamOper′]]_{0}(A, B, C). Then

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

(c)

[[ IFamOper′]](A, B, C, D) :=

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

We will express (1) - (5) as Π_{2}- or Π_{3}-formulas (1’) - (5’), respectively, all with parameter δ, such that

• they hold for δ = P,

• if condition (i’) (where i ∈ {1, …, 5}) holds for 0 < δ, and in case of (1’) - (3’) as well (5’) holds and in case of (2’) as well (1’), then the condition (i) holds w.r.t. δ.

Then the conjunction of these formulae will be equivalent to a Π_{3}-formula as well, and we are done.

• (4) is already a Π_{2}-formula and (5) is already a Π_{3}-formula.

• (1) ⟨r, r′⟩ ∈ [[ IFamOper ]]_{0}(V^{<δ}, T^{<δ}).

Let φ(δ) be the following Π_{2}-formula:

∀α < δ.∃β < δ.⟨r, r′⟩ ∈ [[ IFamOper′]]_{0}(V^{<α}, T^{<α}, V^{<β}) .

This holds for δ = P, since, for each α < δ, ⟨x, x′⟩ ∈ V^{<α} and ⟨y, y′⟩ ∈ T^{<α}(x) → V^{<α} we can find a β such that ⟨r(x, y), r′(x′, y′)⟩ ∈ V^{<β}. By Ãd(L_{P}), we can find for every α one β such that for all x, x′, y, y′ this condition hold.

Furthermore, assume the formula holds for a δ which fulfils (5’). Assume

⟨x, x′⟩ ∈ V^{<δ} ∧ ⟨y, y′⟩ ∈ T^{<δ}(x) → V^{<δ} .

Then by (5’) and [50], Lemma 3.4 there exists an α < δ such that

⟨x, x′⟩ ∈ V^{<α} ∧ ⟨y, y′⟩ ∈ T^{<α}(x) → V^{<α} .

Therefore,

⟨r(x, y), r′(x′, y′)⟩ ∈ V^{<β} ⊆ V^{<δ}

for some β < δ.

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

Let φ(δ) be the following Π_{2}-formula:

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

The argument in this case is similar as for (1).

• (2) This is the most complicated case, where a real Π_{3}-formula emerges. If we replace P by δ we obtain the formula (2′):

⟨s, s′⟩ ∈ (a ∈ V^{<δ}) [[ →]] (b ∈ (T^{<δ}(a) [[ →]] V^{<δ})) [[ →]] T^{<δ}(r(a, b)) [[ →]] [[ Deg ]]^{<δ} .

First ⟨d, d′⟩ ∈ [[ Deg ]]^{<δ} is equivalent (provided δ fulfils (5’)) to an almost Σ_{2}-formula relative to δ

∀x ∈ ω.∃α < δ.∀β < δ.φ(α, β) .

namely the formula equivalent to the following

∀f, f′, g, g′ ∈ [[ Term ]].

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

→ ∃γ < δ.⟨v_{d,f,g}, v_{d′,f′,g′}⟩ ∈ V^{<γ} .

This is clear, since under the condition (5’)

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

is by Lemma 3.4 of [50] equivalent to

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

Now (2′) is therefore, assuming (1′), (5′), equivalent to

∀α < δ.∃β < δ.∀⟨a, a′⟩ ∈ V^{<α}. ∀⟨b, b′⟩ ∈ T^{<α}(a) [[ →]] V^{<α}. ⟨r(a, b), r′(a, b)⟩ ∈ V^{<β} ∧ \begin{matrix}∀⟨c, c′⟩ ∈ T^{<β}(r(a, b)). \\ ⟨s(a, b, c), s(a′, b′, c′)⟩ ∈ [[ Deg ]]^{<δ} . \end{matrix}

If we substitute for ⟨s(a, b, c), s(a′, b′, c′)⟩ ∈ [[ Deg ]]^{<δ} the above mentioned almost Σ_{2}-formula in δ, we obtain therefore that (2′) is equivalent (assuming (5’), which guarantees that we can move the quantifiers restricted only to δ to the front of the formula, and assuming (1’)) to a Π_{3}-formula.

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:

∀α < P.∀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 [50]). 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 for ⟨⟨x, y⟩, ⟨x′, y′⟩⟩ ∈ [[ IFam ]]([[ V ]], [[ T_{V} ]]) ⟨bdeg(d, x, y), bdeg(d′, x′, y′)⟩ ∈ [[ V ]] and for ⟨z, z′⟩ ∈ [[ T_{V} ]](bdeg(d, x, y)) we have ⟨subdeg(d, x, y, z), subdeg(d′, x′, y′, z′)⟩ ∈ [[ Deg ]]. But then we obtain using IH for ordinals < β that degClosure(V^{<β}, T^{<β}, d′, d′′). 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 [50]: We need finitely many admissibles above P 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 4.3

(a) We can model ML_{W} + (Π_{3} − refl) in (KPω + (Π_{3} − refl))^{+}.

(b) |ML_{W} + (Π_{3} − refl)| ≤ |(KPω + (Π_{3} − refl))^{+}|.

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

We have currently only a sketch of a well-ordering proof which shows that the above bound is sharp. We hope to soon be able to present it as a fully proven result.

5 Conclusion

We have indicated why a naïve approach for developing a Π_{3}-reflecting universe using reflection of type-2 functionals doesn’t work in type theory. We have then shown how to develop an autonomous Mahlo universe and a Π_{3}-reflecting universe. We have developed a model for the Π_{3}-reflecting universe and therefore determined an upper bound for its proof theoretic strength.

Future research. Apart from showing that this bound is sharp, 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. However, at the moment we haven’t yet gone through the pain of carrying out wellordering proofs (there are only rough sketches at present). Another line of research would be to explore, whether variants of these universe constructions can be used in general programming.

References

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

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

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

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

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

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

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

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

[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 inductive-recursive 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. 65 pp. To appear in Journal of Logic and Algebraic Programming, 2006.

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

[21] P. Hyvernat and P. Hancock. Programming interfaces and basic topology. To appear in Annals of Pure and Applied Logic, 2005.

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

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

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

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

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

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

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

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

[30] M. Rathjen. An ordinal analysis of stability. Available from http://www.amsta.leeds.ac.uk/Pure/staff/rathjen/preprints.html.

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

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

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

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

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

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

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

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

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

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

[41] 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/∼/articles/1papdiss.dvi or .ps or .pdf, 1996.

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

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

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

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

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

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

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

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

[50] A. Setzer. Universes in type theory part I – Inaccessibles and Mahlo. 35 pages. To appear in the proceedings of the Logic Colloquium 2004, Lecture Notes in Logic, A. K. Peters, 2006.

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