Page 85 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 73 Proof. Let S be a universe and choose a name a of S. Then j(a, λx.x) is a name
of the type
U = {(x, y) : x ∈ S ∧ y ∈˙ x}. (1) The next step is to prove the equivalence
R(b,T)↔∀x.x∈˙ b↔x∈T (2)
for all b ∈ S. The direction from left to right is obvious. To establish the converse direction, let b be an element of S. Then b is a name of a type V since all elements of universes are names. Hence we have R(b, V ), and the right hand side of (2) yields T = V . Thus we conclude R(b, T ).
For all b ∈ S, we derive from (1) and (2) that R(b,T)↔∀x.(b,x)∈U ↔x∈T.
Since the right hand side of this equivalence is elementary, elementary compre- hension gives the type
W ={x:x∈S∧R(x,T)}.
If all names of T were contained in S, then W would be the type of all names
of T. But, in view of the remark above, this is not possible. ⊣
The Limit axiom. The theory EETJ does not prove the existence of uni- verses. However, as in the case of theories for admissible sets (cf. e.g., Ja¨ger [J¨ag84, J¨ag86]), a so-called limit axiom can easily be added. By making use of the generator l, one assigns to each name x the name l x of a universe containing x, i.e.,
(Lim) ∀x.R(x)→U(lx)∧x∈˙ lx.
The standard model constructions of Ja¨ger and Strahm [JS01] for metapred- icative and Ja¨ger and Studer [JS02b] for impredicative Mahlo provide natural models for (Lim). The proof-theoretic strengths of (Lim) in the context of EETJ plus (T-IN) or (LEM-IN) have been analyzed in Kahle [Kah97b] and Strahm [Str99].
Originally, a limit axiom was introduced by Marzetta in [Mar94] as the obvious nonuniform version of (Lim):
(nu-Lim) ∀X.∃Y.U(Y ) ∧ X ∈ Y.
The uniform version was first considered in Kahle [Kah97b]. Although, in many situations, (Lim) is proof-theoretically equivalent to the nonuniform ver- sion as studied in Marzetta [Mar94] and Marzetta and Strahm [MS98], one has to be aware that sometimes there are subtle differences between (Lim) and its nonuniform version.
There are, of course, many universes which contain a given name a. The universe named by l a may be regarded as the standard or normal universe and l a as its normal name.