Page 130 - Textos de Matemática Vol. 40

118 Chapter 3. Truth Theories
Since univ δ is a universe for all δ less than α, for β less than α the expression ∀γ ≺ β.univ γ ` univ β is equivalent to a T-positive formula. So we can prove also the second assertion by transfinite induction on β.
The zero and successor cases are obvious. The limit case follows from the closure conditions of universes. Let γ ≺ Λ. Then we have:
(x∈˙ univγ)∈univ(γ+1)
˙
x∈univγ →
→ ∃δ ≺ Λ.(x ∈˙ univγ) ∈ univδ
→ ∃δ ≺ Λ.(x ∈˙ univγ) ∈ univδ ∈ univΛ
→ ∃δ ≺ Λ.((x ∈˙ univγ) ∈˙ univδ) ∈ univΛ
→ ∃δ ≺ Λ.(x ∈˙ univγ) ∈ univΛ
→ (x∈˙ univγ)∈univΛ,
(x̸∈˙ univγ)∈univ(γ+1)
˙
x̸∈univγ →
→ ∃δ ≺ Λ.(x ̸∈˙ univγ) ∈ univδ
→ ∃δ ≺ Λ.(x ̸∈˙ univγ) ∈ univδ ∈ univΛ
→ ∃δ ≺ Λ.((x ̸∈˙ univγ) ∈˙ univδ) ∈ univΛ
→ ∃δ ≺ Λ.(x ̸∈˙ univγ) ∈ univΛ
→ (x̸∈˙ univγ)∈univΛ. ⊣
¿From Proposition 3.4.10 and the trivial fact that TI(k, T(f ·)) is provable in FON + (C-IN) for every k < ω, we get:
Proposition 3.4.12. 1. FSU+(C-IN) proves the existence of hierarchies of uni- verses of length < ω.
2. FSU + (T-IN) proves the existence of hierarchies of universes of length < ωω.
3. FSU + (LU -IN) proves the existence of hierarchies of universes of length < ε0.
3.4.4 Fixed points
In the following, we show that hierarchies of universes allow us to define iterated fixed points. These fixed points will be used for the embedding of the the theories IDα within Frege structures with universes. This fact shows the close relation-
ship between universes and fixed points. We call an LU formula φ(P, Q, x, y) an inductive operator form if it is T-positive and contains the relation variable P only positively (whereas Q may occur positively and/or negatively). To state