Page 45 - Textos de Matemática Vol. 40

1.7. N-strictness 33 1.7.1 Logical relations of the induction principles
It is trivial from the definitions of the different forms of induction that (S-IN) ⊂ (O-IN) ⊂ (Lp-IN) and (N-IN) ⊂ (Lp-IN) .
But the relation between (N-IN) and (S-IN) or (O-IN) is not as trivial. However, we can prove in BON that (N-IN) implies (S-IN). To express t = 0 by an expression about N, we can use notN and a non-strict case distinction to get the following Lemma:
Lemma 1.7.1. BON ⊢ t = 0 ↔ N(t) ∧ N(dN (λz.0) (λz.notN) t 0 0).
Proof. The direction from the left to the right is a trivial calculation. For the other direction we assume N(t), N(dN (λz.0) (λz.notN) t 0 0), and t ̸= 0. Now we get dN (λz.0) (λz.notN) t 0 0 ≃ (λz.notN) 0 ≃ notN, such that the second assump- tion contradicts ¬N(notN). ⊣
Proposition 1.7.2. BON + (N-IN) ⊢ (S-IN) .
Proof. From the premiss f ∈ P(N) of (S-IN) we can conclude N(f x) for all x belonging to N. With this we get from the previous lemma that the equality f x = 0 is equivalent to N(dN (λz.0) (λz.notN) (f x) 0 0). Using this equivalence (S-IN) follows from (N-IN). ⊣
Remark 1.7.3. If we want to use Lemma 1.7.1 to deduce (O-IN) from (N-IN), we need a possibility to integrate two expression about N to a single one. But we will show that a term andN with the property N(x) ∧ N(y) ↔ N(andN x y) is not definable in BON. We also show that there does not exist a so-called semidecider sdN for N. Such a term with the property sdN x = 0 ↔ N(x) would yield that (O-IN) implies (N-IN).
1.7.2 The axiom of N-strictness
In analogy to the usual notion of strictness we introduce the following notion of
N-strictness:
Definition 1.7.4. Let T be an extension of the theory BON. A closed term t (of
the language of T ) is called N-strict (in T ), if we have T ⊢ ∀x.N(t x) → N(x).
The crucial observation is that BON allows to define only trivial N-strict functions. From this it follows that terms like andN and sdN which would allow to translate (O-IN) and (N-IN) into each other—cf. remark 1.7.3—are undefinable in BON.