Page 43 - Textos de Matemática Vol. 40

1.6. Quantification operators 31 The unbounded μ operator.
(μ.1) (f :N→N)↔N(μf),
(μ.2) (f :N→N)∧(∃x:N.fx=0)→f(μf)=0.
In order to define the standard recursion-theoretic model of BON which satisfies the axioms of μ, Π1 recursion theory is required. Sets in the sense of P(N) as defined above then correspond exactly to the hyperarithmetic sets.
¿From a recursion-theoretic point of view, recursion in μ is equivalent to recursion in the functional E0 for quantification over the natural numbers. E0 differs from μ in the way that it tests for a zero without returning one. This kind of test was used by Feferman for his theory T1 in [Fef75].
The quantification functional E0 (E0.1) (f :N→N)↔N(E0f),
(E0.2) (f :N→N)→((∃x:N.fx=0)↔E0f =0).
A further step consists in replacing E0 by the functional E#0 which acts on partial type 1 objects, cf. Hinman [Hin78]. For the operator E#0 we omit the totality of the argument in the test of a zero. But if there is no zero E#0 returns only a value in N if the function was total. Note that E#0 does not allow a direct test for totality of functions which have a zero.
The quantification functional E#0
(E#0 .1) E#0 f =0↔∃x:N.fx=0,
(E#0 .2) E#0 f =1↔∀x:N.N(fx)∧fx̸=0,
(E#0 .3) ¬N(E#0 f)↔(∀x:N.¬fx=0)∧∃x:N.¬N(fx).
We write BON(μ) and BON(E0), and BON(E#0 ) for the theory BON ex- tended by (μ.1) + (μ.2) and (E0.1) + (E0.2), and (E#0 .1) + (E#0 .2) + (E#0 .3), respectively.
It is obvious that all three operators provide for the elimination of quan- tifiers ranging over N.
For the proof-theoretic strength we refer to Theorem 1.7.24 in the next Section about N strictness. There, we also prove that (O-IN) and (N-IN) are equivalent over BON(E0) and over BON(μ), cf. Corollary 1.7.23. However, for the relation of E#0 to the other operators and its proof-theoretic strength in the presence of (O-IN) and (N-IN) it turns out that an additional axiom about N strictness is useful.