Page 135 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures 123
(T-IN )T
Γ,C(t) Γ,T(t0) Γ,∀x:N.T(¬˙(tx))∨T(t(sNx)) Γ, ∀x : N.T(t x)
(C-IN )T
where the assumption C(t) allows us to write the induction step as a T-
positive formula, and
Γ,T(t0) Γ,∀x : N.T(tx) → T(t(sN x)) Γ, ∀x : N.T(t x)
The main formula of both rules is ∀x : N.T(t x).
The semi-formal system FSU∞ is defined as usual. (For detailed definitions
of semi-formal systems in the context of explicit mathematics, cf. [GS96, MS98], or for truth theories [Can96].) We can bring over all axioms and rules from FSUT into the formalism of FSU∞, and add the following ω rule to deal with formula induction (here, n denotes the n-th numeral):
<ω
derivable with length α and k as a strict upper bound for the cut-rank (defined in the usual way, starting with 0 for T+ and T− formulae).
Let φT be the canonical translation of a LU formula φ into the Tait cal- culus. Then, we have:
Proposition 3.4.17. 1. FSU + (C-IN) ⊢ φ ⇒ FSUT + (C-IN)T φT ,
2. FSU+(T-IN)⊢φ ⇒ FSUT +(T-IN)T φT,
3. FSU+(LU-IN)⊢φ ⇒ FSU∞ <ω+ω φT. <ω
We say that a derivation of Γ is quasi-normal if each cut formula in the
derivation is either a T+ or T− formula. For a quasi-normal derivation of Γ
Γ,n=t foralln<ω Γ , N ( t )
(ω)
WewriteFSU∞ <ω+ω Γifthereareα<ω+ωandk<ωsuchthatΓis
with length k < ω in FSUT we write k Γ (or <ω Γ) and, correspondingly, for ∞ ⋆ α ⋆ <ε0
onewithlengthα<ε0 inFSU wewrite ⋆ Γ(or ⋆ Γ). Becauseallmainformulaeofthenon-logicalaxiomsandrulesofFSUT and FSU∞ are either T+ or T− formulae, we can prove partial cut elimination by
use of the usual methods of proof theory, cf. e.g., [Sch77] or [Mar94]. Proposition 3.4.18. For every finite set Γ of LTU formulae, it holds that:
1. FSUT + (C-IN)T Γ ⇒ FSUT + (C-IN)T
2. FSUT + (T-IN)T Γ ⇒ FSUT + (T-IN)T
3.FSU∞ <ω+ω Γ ⇒ FSU∞ <ε0 Γ. <ω ⋆
<ω Γ, ⋆
<ω Γ, ⋆