Page 51 - Textos de Matemática Vol. 40

1.7. N-strictness 39 1. BON(E#0 )+(N-Str)⊢(f :N→N)↔N(E0E#0 f),
2. BON(E#0 )+(N-Str)⊢(f :N→N)→((∃x∈N.fx=0)↔E0E#0 f =0). Proof. We define
E0E#0 := λf.ifN (E#0 (λx.ifN (f x)(sN (f x))))(E#0 f).
1. ←: It follows from N(E0E#0 f) that E#0 (λx.ifN (f x)(sN (f x))) belongs to N. First let us assume E#0 (λx.ifN (f x) (sN (f x)))) = 0. So there is an x belonging to N such that ifN(fx)(sN(fx)) = 0, and we get N(fx) and sN(fx) = 0, a contradiction. So E#0 (λx.if N (f x) (sN (f x)))) = 1, that means this function is total, and especially for all x belonging to N, f x belongs to N, so f is total.
1. → and 2.: Assuming (f : N → N) we get by definition of ifN that, for N(x), ifN (f x)(sN (f x)) equals sN (f x). So E#0 (λx.ifN (f x)(sN (f x))) = 1, and we get ifN (E#0 (λx.ifN (f x)(sN (f x))))(E#0 f) = E#0 f. But the equality of E0E#0 f and E#0 f yields the required properties. ⊣
Combining the last two Propositions, we get:
Corollary 1.7.21. μ is definable in BON(E#0 ) + (N-Str) + (F-IN).
Now we show that the totality test of E0 already contains enough N- strictness to define sdN and andN.
Proposition 1.7.22. There exists terms sdN and andN of LE0 such that 1. BON(E0) ⊢ ∀x.sdN x = 0 ↔ N(x),
2. BON(E0) ⊢ ∀x, y.N(andN x y) ↔ N(x) ∧ N(y).
Proof. We can define the term sdN by λx.E0 (λy.dN x 0 y 0) and the term andN by λx, y.E0 (λz.dN x y z 0). So the Proposition is a straightforward consequence of the axioms of E0. ⊣
Analogous to BON + (N-Str) we get the equivalence of operation and N- induction in BON(E0) and BON(μ).
Corollary 1.7.23. (O-IN) and (N-IN) are equivalent over BON(E0) and over BON(μ).
Note that the totality test is essential for this argument. So it is not transferable to BON(E#0 ). On the other hand we have to point out that this test is the main problem in the logical relation between the different operators. Giving up the direction from the right to the left in the first axiom of E0 and μ the logical relation becomes much easier. Nevertheless, this totality test is needed to get appropriate proof-theoretic results for the theories containing (N-IN ).