Page 86 - Textos de Matemática Vol. 40

74 Chapter 2. Explicit Mathematics Definition 2.3.5. We write Ul(t) to express that the individual t is a normal
name of a universe,
A first simple observation concerning the generator l says that for all
names a, the type named by a and the type named by l a have to be different. Lemma 2.3.6. In EETJ + (Lim), one can prove that
˙ ∀x.R(x) → x ̸= l x.
Proof. Let a be a name. Because of (Lim), we know that la is a name of a universe S which contains a. According to Lemma 2.3.3, this l a cannot be an
˙
element of S. Hence a ̸= la. ⊣
Simple generators like co and int are extensional in the sense that a =˙ b and u =˙ v imply co(a) =˙ co(b) and int(a, u) =˙ int(b, v). The following Lemma shows that such a form of extensionality is not the case for the generator l.
Lemma 2.3.7. In EETJ + (Lim), one can prove that ∃x,y.R(x)∧R(y)∧x=˙ y∧lx̸=ly.
Proof. Choose an arbitrary type T and a name a of T. Then la is a name of a
universe S which contains a. Because of Lemma 2.3.4, there exists a name b of
Ul(t) := ∃x.R(x) ∧ t = l x.
T which does not belong to S, i.e., b ∈/˙ la. Now consider la and lb. Both are ˙˙
names of universes, but since b ∈˙ lb and b ∈/ la we have la ̸= lb. On the other hand, a =˙ b since both are names of T. ⊣
Ordering principles. Now we turn to possible “ordering principles” for universes. Motivated by the familiar set-theoretic situation, we begin with con- sidering linearity, transitivity and connectivity of universes which are formulated in our context as follows:
(U-Lin) ∀X,Y.U(X)∧U(Y)→X∈Y ∨X=Y ∨Y ∈X, (U-Tran) ∀X,Y.U(X)∧U(Y)∧X∈Y →X⊂Y,
(U-Con) ∀X, Y.U(X) ∧ U(Y ) → X ⊂ Y ∨ Y ⊂ X.
Although these three assertions may appear natural, they are problematic in our context. For example, they are not valid in the standard model of Ja¨ger and Studer [JS02b] and incompatible, as we will see now, with uniqueness of generators.
In the proof of the following Theorem, we exploit the fact that suitably constructed universes remain universes if certain elements are taken out. For this sort of argument, it is important that we have a criterion for testing whether a type is a universe. If universes were introduced by an implicit definition, such an argument would hardly work.
˙