Page 128 - Textos de Matemática Vol. 40

116 Chapter 3. Truth Theories However, in a universe v which reflects u the term ru ru becomes true (cf.
Cantini’s Lemma 37.5 [Can96]):
Proposition3.4.7. FSU⊢U(u)∧U(v)∧u`v→ruru ∈v.
Proof. ¿From the previous Lemma we get ¬(ru ru ∈ u). Since u is a universe we have ru ru ̸∈ u. Thus, the definition of ` yields (ru ru ̸∈˙ u) ∈ v. From the definition of ru we finally get ru ru ∈ v. ⊣
For the “liar” let us consider two different relativizations: l is defined as rec(λx.¬˙ (ux)). So we have lu := lu = ¬˙ (ulu). It may be read as “I’m false in u”. The alternative is to define m := rec (λx.u (¬˙ x)). Here, we have mu := mu = u(¬˙ mu) which may be read as “My negation is true in u”. Both cannot be propositions relativized to a universe u, and while lu is true in universes reflecting u, for mu it is its negation.
Proposition 3.4.8. 1. FSU ⊢ U(u)∧U(v)∧v ` u → ¬(lu ∈ u∨¬˙ lu ∈ u)∧lu ∈ v,
2. FSU⊢U(u)∧U(v)∧v`u→¬(mu ∈u∨¬˙mu ∈u)∧¬˙mu ∈v. The proof is straightforward, similar to the relativized Russell set.
3.4.3 Hierarchies of universes
In the following, we will investigate up to which length, depending on the in- duction principle, we can define hierarchies of universes in our theory. For it, we assume that ≺ represents a primitive recursive well-ordering of ordertype ε0 in FSU. We will use small Greek letter as variables ranging over the field of ≺, and Λ for limit ordinals. As abbreviations we use:
∀α≺β.φ := ∃α≺β.φ := Prog(φ) := TI(α, φ) :=
∀α.α≺β→φ, ∃α.α≺β∧φ,
∀γ.(∀β ≺ γ.φ(β)) → φ(γ), Prog(φ) → ∀β ≺ α.φ(β).
Definition 3.4.9. A theory T proves the existence of a hierarchy of universes of length α, if there is a term t such that:
T ⊢∀β≺α.U(tβ)∧∀γ≺β.tγ`tβ.
We say that T proves the existence of hierarchies of universes of length < α, if it proves the existence of hierarchies of universes of length β for every β less than α.