Page 30 - Textos de Matemática Vol. 40

18 Chapter 1. Applicative theories 1.3.3 Primitive recursion
To use set induction, it is necessary that BON contains already some function in P(N). Therefore, the variants of BON which consider this form of induction have built in the primitive recursive functions. Most notable, this is the case for the original formulation of BON by Feferman and Ja¨ger in [FJ93]. In this case, the language BON is extended by the constant rN and one has the following two additional axioms:
V. Primitive recursion on N.
(10) (f :N→N)∧(g:N3 →N)→(rNfg:N2 →N),
(11) (f :N→N)∧(g:N3 →N)∧N(x)∧N(y)∧h=rNfg→
h x 0 = f x ∧ h x (y′) = g x y (h x y).
However, as soon as at least (O-IN) or (N-IN) are added to BON the prim- itive recursive functions may be defined by use of the applicative language. Therefore, one can usually dispense with the constant rN and the two axioms if one is not considering especially (S-IN).
As a consequence we can use in BON in the presence of any of the forms of induction all the primitive recursive functions and relations. Later on, we will make freely use of addition + and multiplication ∗ of natural numbers (for which we will use infix notation) as well as the usual “less than” relation <, “less or equal than” relation ≤, and the dual forms for “greater”.
1.3.4 Some results and comments
The recursion-theoretic μ operator. In the presence of (Lp-IN), we can define a least number operator μrec so that the following holds, cf. [TvD88a, Chapter 9, 3.10]:
Proposition 1.3.1. There exists a term μrec of Lp such that:
BON + (Lp-IN) ⊢
∀f.((f : N → N) ∨ (∃y : N.f y = 0 ∧ ∀z : N.z < y → N(f z))) →
∀x:N.μrecf =x↔fx=0∧∀v:N.v<x→fv>0.
Proof. Define μrec := rec (λh, f.dN (k 0) (λg.(h g)′) (f 0) 0 (λx.f (x′))). The Propo- sition is proven by induction on x. We need full formulae induction, because the induction formula has to contain the quantification over f . In the induction step we have to use λx.f (x′) as instantiation for f in the induction hypothesis. ⊣
A term not belonging to N. As a useful Corollary of Proposition 1.2.3 we get the fact that there is a term which does not belong to N, provable in BON. Discussing the different standard models of BON below, one observes that in