Page 129 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures 117
By straightforward adaptation of the corresponding proofs in arithmetic, cf. e.g., [Sch77, Can89, JS96], we get the following results about transfinite induction in the presence of truth and formula induction (see also [Can96, §46] for corresponding proofs over FON).
Proposition 3.4.10. 1. For ordinals α less than ωω, we have: FSU + (T-IN ) ⊢ TI(α, T(f ·)).
2. For ordinals α less than ε0 and each LU formula φ, we have: FSU + (LU -IN) ⊢ TI(α, φ).
Now we show that FSU + (T-IN) proves the existence of hierarchies of universes of length < ωω, while FSU+(LU -IN) proves the existence of hierarchies of universes of length < ε0. For this aim, we define an appropriate operation univ. By using recursion on the ordinals less then ε0, we can define a term univ satisfying the following conditions:
1.univ0=l(λy.0=˙0),
2. univ(α+1)=l(univα),
˙
3. univΛ = l(λy.∃x ≺ Λ.y ∈ univx), Λ is a limit ordinal.
Lemma 3.4.11. 1. FSU + TI(α, T(f ·)) ⊢ ∀β ≺ α.U(univ β), 2. FSU+TI(α,T(f·))⊢∀β≺α.∀γ≺β.univγ`univβ.
Proof. We prove both assertions by transfinite induction on β.
For the first Claim, we need only check that the arguments of the universe operator are classes. Note that the formula C(t) can be rewritten as the T- positive formula T(∀˙ x.t x ∨˙ ¬˙ (t x)) such that transfinite induction for T formulae
is sufficient.
The zero and successor cases are trivial. For the limit case, we have by the
induction hypothesis ∀x ≺ Λ.U(univ x), thus
∀x ≺ Λ.U(univ x)
→ ∀x ≺ Λ.C(univ x)
→ ∀y.∀x≺Λ.y∈univx∨y̸∈univx
→ ∀y.(∃x≺Λ.y∈univx)∨(∀x≺Λ.y̸∈univx)
˙ ˙
→ ∀y.T(∃x≺Λ.y∈univx)∨T(∀x≺Λ.y̸∈univx)
˙ ˙
→ ∀y.T(∃x≺Λ.y∈univx)∨T(¬˙(∃x≺Λ.y∈univx))
˙ ˙ ˙ ˙
→ T(∀z.(λy.∃x ≺ Λ.y ∈ univ x) z ∨ ¬˙ ((λy.∃x ≺ Λ.y ∈ univ x) z))
˙
→ C(λy.∃x ≺ Λ.y ∈ univ x)