Page 125 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures 113 3.4.2 Properties of FSU
As a first consequence we get that in global truth is equivalent to “truth in a universe” or “elementhood in a universe”.
Lemma 3.4.2. FSU ⊢ T(x) ↔ ∃u.U(u) ∧ x ∈ u.
Proof. The direction from right to left is axiom I.(2). For the converse, it follows from T(x) that the constant function λy.x is a class. By applying the limit axiom we get ∃u.U(u) ∧ λy.x ` u. Assuming U(u) the definition of ` this yields ∀z.T((λy.x) z) → T(u ((λy.x) z)), i.e., T(x) → x ∈ u. But T(x) was the premiss, so x ∈ u. ⊣
The global consistency of T follows from local consistency.
Lemma 3.4.3. FSU ⊢ ∀x.¬(T(x) ∧ T(¬˙ x)).
Proof. Assume T(x) ∧ T(¬˙ x). Thus, λy.x is a class, and we can apply limit which yields: U(l (λy.x)) ∧ (λy.x) ` l (λy.x). Now, the assumption together with the definition of ` implies x ∈ (l (λy.x)) ∧ ¬˙ x ∈ (l (λy.x)) in contradiction to local consistency. ⊣
By use of these two Lemmas we easily can embed FON within FSU, cf. [Can96, Lemma 37.7.(i)].
Proposition 3.4.4. Let φ be a LFt formula. Then we have FON⊢φ ⇒ FSU⊢φ.
Proof. The proof is by induction on the length of the derivation of φ in FON. The verification of the groups I. and II. of axioms of FON follows from Lemma 3.4.2. Only the verification of closure for universal quantification needs an extra application of the limit axiom in the direction from left to right:
(∀x.T(f x))
→ C(λx.f x) ∧ ∀x.T(f x)
→ ∃u.U(u) ∧ (λx.f x) ` u ∧ ∀x.T(f x)
→ ∃u.U(u)∧(∀x.x∈f →fx∈u)∧∀x.x∈f → ∃u.U(u)∧∀x.fx∈u
→ ∃u.U(u)∧∀˙f∈u
→ T(∀˙f).
The axiom III.(10) of consistency follows from local consistency as shown in the previous Lemma. ⊣
The order relation ` is an unbounded strict partial order on universes. In addition the relation is persistent (or transitive with respect to the defined element relation).