Page 47 - Textos de Matemática Vol. 40

1.7. N-strictness 35
It is easy to see that the axiom (N-Str) is satisfied (or can be satisfied by slight modifications) in all usual models of BON and hence the proof-theoretic results are preserved.
Now we will show that in the presence of (N-Str), (O-IN) and (N-IN) are equivalent over BON:
Lemma 1.7.8. There exists a term sdN of Lp such that BON + (N-Str) ⊢ ∀x.sdN x = 0 ↔ N(x).
Proof. Define sdN := λx.dN 0 1 x x. ⊣ So we can replace N(f x) by (λy.sdN (f y)) x = 0, such that (N-IN) becomes
an instance of (O-IN).
Proposition 1.7.9. BON + (N-Str) + (O-IN) ⊢ (N-IN) .
To establish the converse we use Lemma 1.7.1 which allows to replace t = 0 by a conjunction of expressions over N. To integrate these two expressions we use the following Lemma:
Lemma 1.7.10. There exists a term andN of Lp such that
BON + (N-Str) ⊢ ∀x, y.N(andN x y) ↔ N(x) ∧ N(y).
Proof. Define andN := λx, y.dN 0 0 x y. ⊣ Replacing fx = 0 by N((λy.andN(fy)(dN(λz.0)(λz.notN)(fy)00))x),
(O-IN) becomes an instance of (N-IN).
Proposition 1.7.11. BON + (N-Str) + (N-IN) ⊢ (O-IN) .
Together both Propositions yield:
Theorem 1.7.12. BON + (N-Str) proves that (O-IN) and (N-IN) are equivalent.
Remark 1.7.13. This Theorem allows to dispense with the constant rN without any loss in BON+(N-Str)+(O-IN). It is well-known that the primitive recursive functions are provably representable in BON + (N-IN) without using rN. In BON + (O-IN), however, we do not know how to establish such a result. Thus we still need the explicit axiomatization of rN. With the equivalence of (N-IN) and (O-IN) this is no longer necessary in the presence of (N-Str).
A further application of (N-Str) is a strengthened representability of number- theoretic functions. To this end, we extend the notion of N-strictness to k-ary functions in a straightforward way, and say that a closed term t is k-N-strict (in atheoryT)ifT proves∀x1,...,xk.N(tx1 ...xk)→N(x1)∧...∧N(xk).
Definition 1.7.14. A closed term tF strongly represents a number-theoretic func- tionF :INk →IN (inthetheoryT),if