Page 87 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 75 Theorem 2.3.8. 1. In EETJ, one can prove that
(U-Con) → (U-Tran).
2. In EETJ + (Lim) + (LEM-UG), one can prove that ¬(U-Lin) ∧ ¬(U-Tran) ∧ ¬(U-Con).
Proof. For the proof of the first assertion, take two universes S and T with S ∈ T. Then T ̸⊂ S since T contains a name of S which cannot be an element of S by Lemma 2.3.3. Therefore, (U-Con) implies S ⊂ T, completing the proof of the first assertion.
Now we work in the theory EETJ + (Lim) + (LEM-UG). In order to show ¬(U-Lin), we let S be the universe named by l (l nat) and T the type S \ {l nat}. Then T is properly contained in S. Moreover, because of the uniqueness of generators, T is a universe. Now we apply Lemma 2.3.3 and derive S ̸∈ T from T ⊂ S. It only remains to check that T ̸∈ S, or equivalently,
∀x ∈ S.¬R(x, T ).
If a is in S, then co(co(a)) is also an element of S and a =˙ co(co(a)). The uniqueness of generators and the definition of T therefore yield co (co(a)) ∈ T . We apply Lemma 2.3.3 again and conclude that co (co(a)) is not a name of T . But a and co(co(a)) name the same type so that a cannot be a name of T. Hence we have T ̸∈ S and therefore also ¬(U-Lin).
The proof of ¬(U-Tran) follows the same pattern. In this case we choose R to be the universe named by l (l nat), S to be the universe named by l (l (l nat)) and T to be the type S \{l nat}. It is l nat ̸= l (l nat) according to Lemma 2.3.6. Hence l(lnat) ∈ T. Therefore R ∈ T. In addition, we have lnat ∈ R which implies R ̸⊂ T . Therefore, ¬(U-Tran) is proven. Owing to the first assertion of this Theorem, we also have ¬(U-Con). ⊣
This Lemma makes clear that there are too many universes—universes that are not generated by l—which violate linearity, transitivity and connectivity. As a consequence, we claim linearity, transitivity and connectivity only for normal (names of) universes. These restricted versions are natural, sufficient for all practical purposes and justified by the standard model construction of Ja¨ger and Studer [JS02b]. Therefore our “official” formulations are:
(Ul-Lin) (Ul-Tran) (Ul-Con)
∀x,y.Ul(x)∧Ul(y)→x∈˙ y∨x=˙ y∨y∈˙ x, ∀x,y.Ul(x)∧Ul(y)∧x∈˙ y→x⊂˙ y, ∀x,y.Ul(x) ∧ Ul(y) → x ⊂˙ y ∨ y ⊂˙ x.