Page 140 - Textos de Matemática Vol. 40

128 Chapter 3. Truth Theories
Let l < m be minimal such that Ul+1(s) and Tl+1(st). Thus, we have Tl(t), i.e., t ∈ Xl. Assume Tl+1(s(¬˙ t)). This would imply Tl(¬˙ t), i.e., ¬˙ t ∈ Xl. But this contradicts the consistency of Xl.
(14a) Γ, (∃x.T(t x) ∧ T(¬˙ (t x))), U(l t).
Let l < m be minimal such that ∀x.Tl(tx)∨Tl(¬˙ (tx)), i.e., Cl(t). There-
fore, we have Ul+1(l t) and by persistence, Um+1(l t). (14b) Γ, (∃x.T(t x) ∧ T(¬˙ (t x))), T(t s), T(l t (t s)).
Let l < m be minimal such that Cl(t) and Tl(t s). Thus we have Ul+1(l t) and by clause 11 we get Tl+1(lt(ts)). Again, by persistence we obtain Tm+1(l t (t s)).
(14c) Follows analogously to (14b).
Induction step. We need to check the cut rule and class induction.
(Cut) If Γ is the conclusion of a cut rule, there is a T+ formula φ and a natural number l < k such that
FSUT +(C-IN)T l Γ,φ, ⋆
FSUT +(C-IN)T l Γ,¬φ. ⋆
By the induction hypothesis used with m in the first case and m + 2l in the second, we have
M(m,m+2l) |= Γ,φ, M(m+2l,m+2l +2l) |= Γ,¬φ.
Forl<k,m+2l+2l ≤m+2k,wehavebypersistence: M(m,m+2k) |= Γ,φ,
M(m,m+2k) |= Γ,¬φ, which yields the conclusion.
(C-IN)T ¿From the premiss of class induction, we know that there is a l < k such that:
FSUT +(C-IN)T FSUT +(C-IN)T FSUT +(C-IN)T
l Γ, C(t), ⋆
l Γ, T(t 0), ⋆
l Γ, ∀x : N.T(¬˙ (t x)) ∨ T(t (sN x)). ⋆