Page 84 - Textos de Matemática Vol. 40

72 Chapter 2. Explicit Mathematics
Thus the formula ∀x.C(S,x) → x ∈ S) describes that S is a type which is closed under the type constructions of EETJ, i.e., elementary comprehension and join. A universe is a type which consists of names only and satisfies this closure condition.
Definition 2.3.1. 1. We write U(S) to express that the type S is a universe, U(S) := (∀x.C(S, x) → x ∈ S) ∧ ∀x ∈ S.R(x).
2. U(t) means that the individual t is a name of a universe, U(t) := ∃X.R(t, X) ∧ U(X).
It follows immediately from this definition that one can work within uni- verses as in EETJ; in particular, there is an analog of Lemma 2.1.2 relativized to all universes.
Lemma 2.3.2 (Modified elementary comprehension in universes). Let φ be an elementary LEM formula with no individual variables other than z1, . . . , zm+1 and no (distinct) type variables other than Z1,...,Zn, and let ⃗s = s1,...,sn be a sequence of closed individual terms of LEM. Then there exists a closed individual term t of LEM, depending on φ and ⃗s, so that EETJ proves for all ⃗a = a1,...,am:
1. U(S)∧⃗s(⃗a)∈S→t(⃗a)∈S,
2. R(⃗s(⃗a)) → ∀x.x ∈˙ t(⃗a) ↔ φ[x,⃗a,⃗s(⃗a)].
We now observe that universes do not contain their names; for a proof see Marzetta [Mar94]. This property of universes corresponds in a certain sense to the set-theoretic fact that admissibles do not contain themselves, even if ∈ foundation is not available.
Lemma 2.3.3. In EETJ, one can prove that
U(S) ∧ R(a, S) → a ∈/ S.
Note that in explicit mathematics, the names of a type do not form a type. This is proven in various places, for example in Cantini and Minari [CM99], Ja¨ger [J¨ag97] and Jansen [Jan97]; join is not needed for this argument. In connection with universes, a stronger result is possible: each type has so many names that not all of them can be contained in a single universe, or, in other words, no universe is large enough to contain all names of a given type (see also Minari [Min]).
Lemma 2.3.4. In EETJ, one can prove that
U(S) → ∃x.R(x, T ) ∧ x ∈/ S.