Page 41 - Textos de Matemática Vol. 40

1.5. Proof theory 29
The theory ID#1 . Occasionally we will consider the theory ID#1 which is defined like ID1 but restricts the induction on the natural numbers to formulae which have only positive occurrences of the new fixed point constants. This theory was introduced and analyzed in [JS96]:
Proposition 1.5.4. |ID#1 | = φ ω 0.
Iterated fixed-point theories. Finitely iterated fixed point theories were introduced and studied by Feferman in [Fef82]. The transfinite case is ana- lyzed by Ja¨ger, Kahle, Setzer, and Strahm in [JKSS99].
The theories IDα up to α < ε0 are formulated in the language Lfix. This language extends the language LPA of Peano arithmetic by predicate constants Pφ for each inductive operator form φ(P,Q,x,y), i.e., a formula of LPA con- taining P(t) at most positively, while Q(s) is allowed to occur positively and negatively. Here, P and Q have to be fresh (unary) relation variables. For the formal definition, we need a primitive recursive pairing operation ⟨·, ·⟩ with projections (·)0 and (·)1. Then, we write Psφ(t) for Pφ(⟨t,s⟩) and P≺φs(t) for t = ⟨(t)0, (t)1⟩ ∧ (t)1 ≺ s ∧ Pφ(t). Here, ≺ denotes a primitive recursive well- ordering of order type ε0. One may understand the parameter s in Psφ(t) as the level of the fixed point definition. With P≺φs(t), it is expressed that t belongs to the disjoint union of fixed points with levels less than s.
The axioms of IDα, for α an ordinal less than ε0, are those of PA, together with induction on the natural numbers for all Lfix formulae, plus the following fixed point axiom for each inductive operator form φ(P, Q, x, y):
∀β ≺ α.∀x.Pφ(x) ↔ φ(Pφ, Pφ , x, β). β β≺β
ID<α is the union of the theories IDβ, β < α ≤ ε0.
The theories IDα are defined as the metapredicative counterparts to the well-known impredicative theories of inductive definitions IDα which contain, additionally, the leastness of the fixed points.
The proof-theoretic analysis of IDα in [JKSS99] yields the following Theo- rem about the proof-theoretic strength, in terms of the ternary Veblen function φ. cf. [JKSS99]. The first assertion of the Theorem was proven by Feferman in [Fef82].
Proposition 1.5.5. 1. |ID<ω| = φ100 = Γ0, 2. |ID<ωω|=φ1ω0,
3. |ID<ε0| = φ1ε0 0.
1.5.4 Kripke-Platek set theory
Within set theory, it turned out that Kripke-Platek set theory, KP, is an ex- tremely fruitful framework for proof theoretic investigations. It was investigated