Page 38 - Textos de Matemática Vol. 40

26 Chapter 1. Applicative theories
In the following, we usually determine the proof-theoretic strength of the theories under consideration by proof-theoretic reductions, i.e., interpretations in other theories. So, direct well-ordering and cut-elimination proofs are not needed. Only for the upper bounds of truth theories with universes we will sketch a cut-eliminiation procedure, cf. Section 3.4.6.
As ordinal notation we will use the binary and ternary Veblen function. The ternary Veblen function extends the standard notation system for ordinals up to the Feferman-Schu¨tte ordinal Γ0 which is based on the well-known binary Veblen function φ, cf. [Poh89] and [Sch77]. Its definition may be found, for instance, in [JKSS99, §2].
For the impredicative theories we use the notation system of Pohlers
[Poh98]. In this notation, for instance, the proof-theoretic ordinal of the theory
T (see Section 2.3.2) reads Ψ (ε ) where Ω stands for ωck, the first nonre- 0 Ω I0+1 1
cursive ordinal (which is the recursive counterpart of ω1, the first uncountable ordinal) and I0 has its origin in the first weakly inaccessible cardinal.
1.5.2 Subsystems of analysis
The most important framework in proof theory is formed by the subsystems of analysis. With respect to mathematical practice, it was shown that full analysis Z2 is sufficient to formalize nearly all mathematics, cf. [HB34, HB39]. The crucial axiom is comprehension for arbitrary second order formulae, i.e., those which may contain second order quantifiers without any restriction:
∃X.∀y.y ∈ X ↔ φ(X, y).
An ordinal analysis of Z2 is still out of reach, however, one nay obtain treatable theories by restricting the comprehension axiom. Therefore, if C is a class of formulae, we denote by C-CA the axiom scheme:
∃X.∀y.y ∈ X ↔ φ(y)
with φ ∈ C and X not occurring in φ. The class of arithmetical formulae, i.e., formulae without bound set variables, is called Π0∞. Thus, the axiom of arithmetical comprehension is denoted by Π0∞-CA. In general, given a com- prehension axiom Ax we denote by (Ax) the corresponding theory containing the basic arithmetical axioms plus Ax as well as the induction scheme for the full language; (Ax)0 is the theory where the induction scheme is replaced by an induction axiom for elementhood in a set.6 Thus, (Π0∞-CA) is the theory of arithmetical comprehension. By defining a jump hierarchy along a primitive recursive well-ordering ≺ of order type α, cf. [Fef77], we can iterate the com- prehension for arithmetical formulae along such a hierarchy and get the theory (Π0∞-CA)α. The union of all (Π0∞-CA)β for β < α is called (Π0∞-CA)<α.
6In the literature, sometimes the symbol is used instead of the index 0, i.e., a theory Th0 is also designated Th.