Page 53 - Textos de Matemática Vol. 40

1.7. N-strictness 41 Definition 1.7.25. Let L the language L extended by the new individual con-
pp
stants 0 and s . (We use n, in the same way as n, as the canonical abbreviation N
of n applications of s to 0.) We extend ρ (and analogously ρ +) to L and Np
add the following clauses for all terms t and s of L and natural numbers n and p
m, n ̸= m.
sN n ρ n + 1, (5a)
pNn+1 ρ n, (5b) dNtsnn ρ t, (6a) dNtsnn ρ t, (6b) dNtsnn ρ t, (6c)
dNtsnm ρ s, (7a) dNtsnm ρ s, (7b) dNtsnm ρ s, (7c)
rNtsr0 ρ tr, (8a)
rN tsrn+1 ρ sr(rN tsrn). (9a) Let CNT ⋆ be defined like CNT , but be aware that the terms n are not
elements of the interpretation of N.
Since BON has no special axioms about the pseudo numerals, we get in
the same way as for CNT : Proposition 1.7.26. CN T ⋆ |= BON.
By construction of CN T ⋆ it follows, that every N-strict function has to be the identity, since the mathematical constants of Lp cannot distinguish between “real” and pseudo numerals. So we can prove Proposition 1.7.5 in the following formulation:
Proposition 1.7.27. For every closed term t of Lp and every natural number m for which CNT⋆ |=N(tm)∧tm̸=m we have:
CNT⋆ |=tm=tm.
Proof. In this proof we use the notation t →i s, if the term t can be reduced in CNT⋆ tosmodulo ρ inisteps,i∈IN. t{s/r}iscalledavariantoft,ifsome occurrences of the subterm r are replaced by s (not necessary all occurrences, maybe no one). t{s/r} is called a proper variant of t if it is different from t.
Let us assume CNT ⋆ |= N(tm) ∧ tm ̸= m. Then there exists a natural number k, k ̸= m, such that
C N T ⋆ |= t m = k .