Page 109 - Textos de Matemática Vol. 40

3.1. Truth theories in the total setting 97 It contains new constants PΓ for each positive operator form Γ(P, x) and
axioms of the form
where σ is an ordinal variable and Pσ(t) stands for PΓ(σ,t) and P<σ(t)
∀x.Pσ(x) ↔ Γ(P<σ,x) ΓΓ
ΓwΩΓ
for ∃ξ < σ.PΓ(ξ, t). Moreover, in ω-PAΩ we have ∆0 -induction on the
ordinals, i.e., induction on the ordinals for formulae which do not contain unrestricted ordinal quantifiers.
3. Interprete Γ-ID1 in ω-PAwΩ. In this interpretation, PΓ(t) will be translated by ∃ξ.PΓξ(t). Now, we can prove
∀σ.∀x.¬(PΓσ (x) ∧ PΓσ (¬˙ x))
by use of ∆Ω0 -induction and the axiom for positive operator forms in
ω-PAwΩ. This, of course, verifies the translation of the consistency axiom.
4. Proceed with the usual proof-theoretic methods for the analysis of ω-PAwΩ: Partial cut elimination up to ΣΩ/ΠΩ formulae; introduce a suitable in- finitary system T∞ which allows full cut-elimination and an asymmetric interpretation of ω-PAwΩ.
The consistency was already treated in the third step by use of ∆Ω0 -
induction on the ordinals in ω-PAwΩ. Therefore, we will not exceed the proof- theoretic bounds, as they are computed along the same lines as for an analysis of ID1. The procedure described here is paradigmatic for the treatment of con- sistency as it can be done for the theories with universes later on.
An analogous procedure in the context of fixed point theories with ordinals is worked out in detail in [Str00b] where Strahm analyzes theories called PAwΩ + (Subst) and PA+Ω + (Subst). By replacing the ΣΩ-induction by ∆Ω0 -induction in the semi-formal system T which corresponds to PA+Ω one gets exactly the theory we call ω-PAwΩ. For the forth step one may actually use the semi-formal system T∞, defined by Strahm, replacing the bounds (β, φ α (β+β)) in the asymmetric interpretation by (β, β + 2α), cf. [Str00b, Theorem 13].
3.1.5 Proof theory
As proof-theoretic results we get:
Theorem 3.1.10. 1. FON + (C-IN) ≡ PA,
2. FON+(T-IN)≡ID#1 , 3. FON + (LFt -IN) ≡ ID1.
The lower bounds follow from Proposition 3.1.9. The upper bounds are proven directly by Cantini [Can96, §57] or may be carried out following the description above in analogy to the results of Strahm in [Str00b].