Page 40 - Textos de Matemática Vol. 40

28 Chapter 1. Applicative theories
positive arithmetical operator forms. A positive operator form φ(R,x) is a formula having only positive occurrences of the relation symbol R. For the definition of the theories we extend the language LPA of Peano arithmetic by new predicate symbols Pφ for each positive operator form φ(R,x). ID1 extends the axioms of PA, including formulae induction extended to the new language, by the following two principles for each new predicate symbol Pφ and arbitrary formulae ψ:
(ID1.1) ∀x.φ(Pφ, x) → Pφ(x)
(ID1.2) (∀x.φ(ψ/R, x) → ψ(x)) → ∀x.Pφ(x) → ψ(x)
Here φ(ψ/R,x) denotes the result of substituting any occurrence of R(t) in φ by ψ[t/x].
The proof-theoretic ordinal of ID1 is the Bachmann-Howard ordinal. In terms of the notation system used in [Poh98], we have:
Proposition 1.5.2. |ID1| = ΨΩ(εΩ+1).
The theory IDacc. Occasionally we will consider also a proof-theoretic
1 acc equivalent, by expressively slightly weaker variant of ID1 called ID1 . It is the
theory of accessibility elementary inductive definitions, introduced and studied
in [BFPS81] (see also [Can96]). In this case we extend the language LPA of
Peano arithmetic by new unary predicate symbols Pφ for every formula φ(x,y)
of L containing two distinct free variables. IDacc extends the axioms of PA, PA 1
including formulae induction extended to the new language, by the following two axioms:
(IDacc.1) ∀x.(∀y.φ(x, y) → Pφ(y)) → Pφ(x) 1
(IDacc.2) (∀x.(∀y.φ(x, y) → ψ(y)) → ψ(x)) → ∀x.Pφ(x) → ψ(x) 1
The theory ID1. For the fixed point theory ID1 we only postulate (not necessarily least) fixed points of positive arithmetical operator forms, cf. [Acz77]. The theory is formulated in the same language as ID1, but we drop the leastness condition (ID1.2) and, instead, state the first axiom as equivalence. Thus, ID1 extends Peano arithmetic by the following axiom for each new predicate symbol Pφ:
(ID1) ∀x.φ(Pφ, x) ↔ Pφ(x).
In view of the following definition we have to stress that ID1 contains formulae induction extended to the full new language. As ordinal strength we have, cf. e.g., [Fef82]:
Proposition 1.5.3. |ID1| = φ ε0 0.