Page 143 - Textos de Matemática Vol. 40

3.4. Universes over Frege structures 131
points of Φ. This theory is as IDα formulated in the language Lfix. We there- fore use the same abbreviations. In this case we have to consider only the one particular operator form Φ given above (and not arbitrary ones, like for IDα). We define Φ-IDα as the extension of PA, together with induction on the natural numbers for all Lfix formulae, by the following axioms for the new constant PΦ:
∀β ≺ α.∀x.PβΦ(x) ↔ Φ(PβΦ,P≺Φβ,x,β), ∀β ≺ α.∀x.¬(PβΦ(x) ∧ PβΦ(¬˙ x)).
With the usual proof-theoretic machinery, we can formalize the asymmetric interpretation in Φ-IDα to obtain the following results.
Proposition 3.4.21. 1. FSU + (C-IN) can be embedded within Φ-ID<ω. 2. FSU + (T-IN) can be embedded within Φ-ID<ωω .

By a slight modification of the proof-theoretic analysis of the theories IDα given in [JKSS99] one can check that the theories Φ-IDα have the same strength. The analysis of IDα uses auxiliary semi-formal systems Hα. They are essentially Tait-style calculi for IDα including an ω rule for the natural numbers. For our purpose we extend Hα to H+α by additional axioms stating the consistency of the fixed points of the particular operator form Φ, i.e., we have to add axioms of the form
¬(PβΦ(s) ∧ PβΦ(¬˙ s))
for all β < α. These axioms do not affect the partial cut elimination as it is done for Hα. However, in the proof of the so-called Main Lemma II, [JKSS99, Lemma 13], one has to carry through “the standard elimination procedure of finitely many fixed points (say, by asymmetric interpretation, cf. e.g., [Can85, JS96, MS98])”. This elimination procedure for the highest leveled fixed point has to be adjusted in a similar way to the analysis of FON + (LFt -IN), described above. This means we have to add an intermediate step where we remove the consistency axiom for the highest leveled fixed point, by use of an auxiliary system providing ordinals and ∆Ω0 -induction on these ordinals, which can be added without “proof-theoretic costs”. Hence, partial cut-elimination followed by an asymmetric interpretation in the lower semi-formal system will still yield the appropriate bounds.
Putting all together, taking into account these final considerations along with Proposition 3.4.15 and Theorem 1.5.5, we get the final result about the proof-theoretic strength of our theories:
3. FSU + (LU -IN) can be embedded within Φ-ID<ε0 .
All three embeddings preserve (the translations of) the arithmetical theo-
rems.