Page 126 - Textos de Matemática Vol. 40

114 Chapter 3. Truth Theories
Lemma3.4.5. 1. FSU⊢U(u)∧U(v)∧u`v∧x∈u→x∈v, 2. FSU⊢U(u)→∃v.U(v)∧u`v,
3. FSU⊢U(u)→¬u`u,
4. FSU⊢U(u)∧U(v)∧U(w)∧u`v∧v`w→u`w.
Proof. 1. By definition of ` we get from the premiss (x ∈˙ u) ∈ v which implies x ∈ v by axiom IV.(12).
2. Since universes are classes, the assertion is a direct consequence of the limit axiom.
3. Let us define r := rec(λx.x ̸∈˙ u), i.e., r = r ̸∈˙ u. Assuming U(u)∧u ` u, we get the following contradiction:
T(ur) ↔ r∈u
↔ (r̸∈˙u)∈u
↔ r̸∈u
↔ ¬T(u r).
4. Transitivity follows again from axiom IV.(12). Assume U(u) ∧ U(v) ∧ U(w)∧u`v∧v`w. Sowehave
x∈u → (x∈˙u)∈v
→ ((x∈˙u)∈˙v)∈w
→ (x∈˙u)∈w.
x̸∈u → (x̸∈˙u)∈v
→ ((x̸∈˙u)∈˙v)∈w
→ (x̸∈˙u)∈w. ⊣
Let us give some remarks about FSU and related theories.
In view of the upper bounds we could strengthen the theories by adding
directedness:
(U-Dir) U(u) ∧ U(v) → ∃w.U(w) ∧ w ` u ∧ v ` w
or linearity of ` :
(U-Lin) U(u) ∧ U(v) ∧ U(w) → w ` u ∨ u ≡ w ∨ u ` w.
Here, u ≡ w stands for ∀x.x ∈ u ↔ x ∈ w. However, for our purposes both are not needed. For instance, in Cantini’s theory TLR, which is closely re- lated to FSU, directedness was used to prove global consistency, cf. [Can96,
Remarks.