Page 44 - Textos de Matemática Vol. 40

32 Chapter 1. Applicative theories 1.6.2 The Suslin operator
The next (natural) step up in recursion-theoretic hierarchies is the well-known Suslin operator E1 which tests for wellfoundedness on total objects. The recur- sion theory of E1 is presented in detail for example in Hinman [Hin78].
There exists a close relationship between recursion in E1, subsystems of the theory KPi of iterated admissible sets (cf. e.g., Ja¨ger [Ja¨g86]) and ∆12 comprehension in second order arithmetic. The least ordinal not recursive in E1 is the first recursively inaccessible ordinal and the sets recursive in E1 form a model of ∆12 comprehension.
The study of the Suslin operator E1 in applicative theories is due to Ja¨ger and Strahm [JS02a]. It can be characterized by the following two axioms.
The wellfoundedness functional E1 (E1.1) (f :N2 →N)↔N(E1f),
(E1.2) (f : N2 → N) →
((∃g.(g:N→N)∧∀x:N.f(gx′)(gx)=0)↔E1f =0).
We write SUS for BON(μ) + (E1.1) + (E1.2).
In BON(μ,E1) every Π1 set of natural numbers can be represented by a set in the sense of P(N).
Proposition 1.6.1. We have the following proof-theoretic equivalences: 1. SUS + (S-IN) ≡ (Π1-CA)0.
2. SUS + (O-IN) ≡ SUS + (N-IN) ≡ (Π1-CA)<ωω .
3. SUS + (F-IN) ≡ (Π1-CA)<ε0 .
The corresponding proof-theoretic ordinals are ΨΩ(Ωω), ΨΩ(Ωωω ), and ΨΩ(Ωε0 ), respectively.
This Proposition is proven in Ja¨ger and Strahm [JS02a]. By known proof-theoretic results the paper also exhibits the proof-theoretic relationship between E1 and theories for iterated admissible sets.
1.7 N-strictness
In this Section we discuss the logical relationship of the different forms of induc- tion as well as quantification operators in applicative theories. In both cases an introduced notion of N-strictness allows to obtain the appropriate results. Note, that within this Section we assume that primitive recursion is implemented in BON by the axioms V.(10) and V.(11), see Section 1.3.3.
The Section on N-strictness is based on [Kah00] which is essentially a translation of [Kah97a, Section 1.2].