Page 52 - Textos de Matemática Vol. 40

40 Chapter 1. Applicative theories
Theorem 1.7.24. We have the following proof-theoretic equivalences:
1. BON(μ) + (S-IN) ≡ BON(E0) + (S-IN) ≡ BON(E#0 ) + (S-IN) ≡ PA,
2. BON(μ) + (N-IN) ≡ BON(E0) + (N-IN) ≡ BON(E#0 ) + (N-Str) + (N-IN) ≡ ID#1 ,
3. BON(μ) + (O-IN) ≡ BON(E0) + (O-IN) ≡ BON(E#0 ) + (N-Str) + (O-IN) ≡ ID#1 ,
4. BON(μ) + (F-IN) ≡ BON(E0) + (F-IN) ≡ BON(E#0 ) + (F-IN) ≡ ID1.
The corresponding proof-theoretic ordinals are ε0 , φ ω 0, and φ ε0 0, respectively.
The lower bounds for BON(μ) + (S-IN) and BON(μ) + (F-IN) are proven by Feferman and Ja¨ger in [FJ93, Section 6] and make essential use of a Representation Lemma of arithmetical formulae in BON(μ) + (S-IN). Since this Lemma also holds for the corresponding theories over E0 and E#0 , the proofs can be directly applied to these operators. The lower bound for BON(μ) + (N-IN) is proven by a wellordering proof by Ja¨ger and Strahm, cf. [JS96, Section 3.3]. It uses the possibility to test the totality of a function by use of μ. But μ is never used in this proof to determine a particular zero of a function. Therefore, exactly the same proof works for BON(E0)+(N-IN). The equivalence of operation induction and N-induction over μ and E0 carry it over to operation induction. Finally, in the presence of (N-Str) we get the lower bound — with the definability of E0 — also for BON(E#0 ) with (N-IN) or (O-IN).
All these operators can be modeled by use of theories with ordinals over PA, introduced by Ja¨ger in [J¨ag93]. Feferman, Ja¨ger, and Strahm have done this for the μ operator in [FJ93] and [JS96]. It is an easy exercise to modify the construction for E0 and E#0 , cf. [Kah97a, Section 1.3.2]. (N-Str) is trivially satisfied in these models, because the universes consist of the natural numbers. Moreover, the modifications do not affect the proofs of the upper bounds in the presence of each form of induction as carried out in [FJ93] and [JS96]. Therfore, all bounds are sharp.
1.7.4 The missing N-strictness in BON
In this Section we provide the proof of Proposition 1.7.5. As mentioned, we will define an extension CNT⋆ which is still a model of BON, but which does not allow to define non-trivial N-strict functions.
Therefore we extend the closed normal term model CNT by so-called pseudo numerals n, n ∈ IN. n is not in the interpretation of N, but the mathe- matical constants of Lp, sN,pN,dN, and rN, operate on the pseudo numerals like on the “real” numerals.