Rules for the Π_{3}-reflecting Universe

Anton Setzer^{∗}

February 15, 1999

Abstract We introduce a universe, which yields the strength of KP + Π_{3}-

reflection + ω admissibles above it.

1 Rules for the Π_{3}-reflecting unverse

The basic structure

𝕌 is a universe, with decoding function S(x). Univ is a subset of 𝕌, each element u of it is a subuniverses of it 𝕌 with decoding function T̂_{u}. M is the set of Mahlo-degrees, and m(u) is the Mahlo-degree of a universe u. If u is a universe then it will be Mahlo with respect to every m(u)^{a,b}[i] for i : τ^{a,b}(m(u)) for every family of sets a, b in u. So the degree of Mahloness depends on m(u) and the universe u.

In order to distinguish recursive and inductive definitions we underline all constructors when they are introduced the first time (afterwards we don’t underline them, to reduce the amount of syntax). So, whenever we have a rule which yields a set or an element of a set and have an expression which does not start with an underlined constructor, this is a recursive definition, and whenever we introduce a new element of the set by recursion on which it is defined (and introducing means, that the element starts with a constructor), we have to tell, how to evaluate it. For instance, S(a) is defined recursively by recursion on a : 𝕌, and it is defined by S(univ(u)) = U_{u}, S(Σ̂(a, b)) = Σ(S(a), S ∘ b), where univ and Σ̂ are the constructors of 𝕌.

\underline{𝕌} : Set  \underline{Univ} : Set
\frac{u : Univ}{\underline{univ}(u) : 𝕌}  \frac{a : 𝕌}{S(a) : Set}
\frac{u : Univ}{\underline{U}_{u} : Set}  \frac{u : Univ}{S(univ(u)) = U_{u} : Set}

\frac{u : Univ a : U_{u}}{T̂_{u}(a) : 𝕌}

If u : Univ, a : U_{u} then T_{u}(a) := S(T̂_{u}(a)) : Set.

∗Anton Setzer, Dept. of Mathematics, Uppsala University. Email: setzer@math.uu.se

\underline{M} : Set  \frac{u : Univ}{m(u) : M}
\frac{a : 𝕌  b : S(a) → 𝕌  m : M}{τ^{a,b}(m) : 𝕌} τ^{a,b}(m) := S(τ^{a,b}(m))
\frac{m : M  a : 𝕌  b : S(a) → 𝕌  i : τ^{a,b}(m)}{m^{a,b}[i] : M}

𝕌 is a universe

\frac{a : 𝕌 b : S(a) → 𝕌}{\underline{Σ̃}(a, b) : 𝕌} \frac{a : 𝕌 b : S(a) → 𝕌}{S(Σ̃(a, b)) = Σ(S(a), S ∘ b)}

Similarly closure under N_{0}, N_{1}, N_{2}, N, +, Π, W, I.

The elements of Univ are universes

\frac{u : Univ  a : U_{u}  b : T_{u}(a) → U_{u}}{\underline{Σ̂}(a, b) : U_{u}}
\frac{u : Univ  a : U_{u}  b : T_{u}(a) → U_{u}}{T̂_{u}(Σ̂(a, b)) = Σ̃(T̂_{u}(a), T̂_{u} ∘ b) : 𝕌}

Similarly closure under Ñ_{0}, Ñ_{1}, Ñ_{2}, Ñ, ˜+, Π̃, W̃, Ĩ.

Universes are Mahlo with respect to ·^{·}[·]

u : Univ  r : U_{u}
s : T_{u}(r) → U_{u}  i : τ^{T̂_{u}(r),T̂_{u}∘s}(m(u))
f : (x : U_{u}, y : T_{u}(x) → U_{u}) → U_{u} g : (x : U_{u}, y : T_{u}(x) → U_{u}, T_{u}(f(x, y))) → U_{u}
\underline{su}_{u,r,s,i,f,g} : Univ

Assume now in the following the assumptions of the last rule. We write f⃗g for u, r, s, i, f, g.

m(suf⃗g) = (m(u))^{T̂_{u}(r),T̂_{u}∘s}[i] : M  SUf⃗g := U^{su}f⃗g : Set

SUf⃗g is a subuniverse of u:

\frac{a : SUf⃗g}{\underline{s}f⃗g(a) : U_{u}}  \frac{a : SUf⃗g}{T̂_{u}(sf⃗g(a)) = T̂_{suf⃗g}(a) : 𝕌}

SUf⃗g is closed under f, g:

\frac{a : SUf⃗g b : T_{suf⃗g}(a) → SUf⃗g}{\underline{appf}f⃗g(a, b) : SUf⃗g}
\frac{a : SUf⃗g b : T_{suf⃗g}(a) → SUf⃗g}{T̂_{suf⃗g}(appff⃗g(a, b)) = T̂_{u}(f(sf⃗g(a), sf⃗g ∘ b)) : 𝕌}

a : SUf⃗g

b : T_{suf⃗g}(a) → SUf⃗g c : T_{u}(f(sf⃗g(a), sf⃗g ∘ b))
\underline{appg}f⃗g(a, b, c) : SUf⃗g
a : SUf⃗g
b : T_{suf⃗g}(a) → SUf⃗g  c : T_{u}(f(sf⃗g(a), sf⃗g ∘ b))

T̂_{suf⃗g}(appgf⃗g(a, b, c)) = T̂_{u}(g(sf⃗g(a), sf⃗g ∘ b, c)) : 𝕌 Introduction rules for M

\frac{F : (a : 𝕌, b : S(a) → 𝕌) → 𝕌 G : (a : 𝕌, b : S(a) → 𝕌, U_{F (a,b)}) → M}{\underline{mahlo}(F, G) : M}

And under the assumptions of the last rule we have:

τ^{a,b}(mahlo(F, G)) = F (a, b) : 𝕌  mahlo(F, G)^{a,b}[c] = G(a, b, c) : M

Existence of Mahlo universe

For every Mahlo-degree we have universe of its degree:

\frac{m : M, f : (x : 𝕌, y : S(x) → 𝕌) → 𝕌 g : (x : 𝕌, y : S(x) → 𝕌, z : S(f(x, y))) → 𝕌}{\underline{v}_{m,f,g} : Univ}

Assume now in the following the assumptions of the last rule. m(v_{m,f,g}) = m : M V_{m,f,g} := U_{v_{m,f,g}} : Set V_{m,f,g} is closed under f, g:

\frac{a : V_{m,f,g} b : T_{v_{m,f,g}}(a) → V_{m,f,g}}{\underline{Appf}_{m,f,g}(a, b) : V_{m,f,g}}

\frac{a : V_{m,f,g} b : T_{v_{m,f,g}}(a) → V_{m,f,g}}{T̂_{v_{m,f,g}}(Appf_{m,f,g}(a, b)) = f(T̂_{v_{m,f,g}}(a), T̂_{v_{m,f,g}} ∘ b) : 𝕌}

a : V_{m,f,g}

b : T_{v_{m,f,g}}(a) → V_{m,f,g} c : T_{u}(f(T̂_{v_{m,f,g}}(a), T̂_{v_{m,f,g}} ∘ b))
\underline{Appg}_{m,f,g}(a, b, c) : V_{m,f,g}
a : V_{m,f,g}
b : T_{v_{m,f,g}}(a) → V_{m,f,g} c : T_{u}(f(T̂_{v_{m,f,g}}(a), T̂_{v_{m,f,g}} ∘ b))

T̂_{v_{m,f,g}}(Appg_{m,f,g}(a, b, c)) = g(T̂_{v_{m,f,g}}(a), T̂_{v_{m,f,g}} ∘ b), c) : 𝕌

Elimination rules for the universe

non applicable