Page 46 - Textos de Matemática Vol. 40

34 Chapter 1. Applicative theories
Proposition 1.7.5. There exists a model M of BON such that for every closed term t of Lp and every natural number m for which M |= N(tm)∧tm ̸= m we have:
M |= ∃x.¬N(x) ∧ t m = t x.
We will give the (longish but not very complicated) proof of this Propo- sition in Section 1.7.4. The main idea is to extend a term model by so-called pseudo numerals such that all combinators which operate on numerals reduce pseudo numerals also to numerals. Thus it is impossible to distinguish whether the argument of a function was a numeral or a pseudo numeral except for the identity function. In this specific model M every N-strict function has to be the identity on the natural numbers. We use it to prove that andN and sdN are undefinable in BON:
Proposition 1.7.6. There is no Lp term sdN such that BON proves ∀x.sdN x = 0 ↔ N(x).
Proof. Assume sdN exists. Then we get in BON in particular sdN 1 = 0. By the previous Proposition we get for the specific model M: ∃x.¬N(x)∧sdN 1 = sdN x. This contradicts N(x) which follows from the assumption. ⊣
Proposition 1.7.7. There is no Lp term andN such that BON proves ∀x, y.N(andN x y) ↔ N(x) ∧ N(y).
Proof. Assume andN exists. From Proposition 1.7.5 it follows in M that the terms λx.andN 0 x as well as λx.andN x 1 have to be the identity function on N. So we get the contradiction 1 = (λx.andN 0x)1 = andN 01 = (λx.andN x1)0 = 0.
⊣
Now we will propose a very natural extension of BON which allows to define N-strict functions. Understanding dN as a definition by cases on N, this can be formalized in the following way:
Axiom of N-strictness
(N-Str) ∀x,y,v,w.N(dNxyvw)→N(v)∧N(w).
The axiom expresses that dN is N-strict in its two last arguments. Its meaning can be illustrated, if we consider its contraposition: As a definition by cases on N, dN should be a term without a specific meaning whenever v or w does not belong to N. With respect to the total version of BON it is impossible to express this fact by ¬ dN x y v w ↓. Moreover, in the total models we have no possibility to distinguish any term not belonging to N, thus the statement ¬N(dN x y v w) is the only way to express “meaninglessness”.