Page 34 - Textos de Matemática Vol. 40

22 Chapter 1. Applicative theories
Due to the restricted form of the Recursion Theorem in PRON, in this theory it is not possible to define a term like notN which is provably not a natural number (cf. Corollary 1.3.2). In fact, this theory allows a model where the universe consists of the natural number, but also the axiom of totality (Tot) holds.
1.4 Models
There are a lot of models of BON which are extensively discussed in the litera- ture, cf. e.g., [Fef75, Fef79, Bee85, FJ93, JS95b, Str96a]. Two classes of models, which differ essentially in the central intention of the interpretation, are of spe- cial interest: the recursion theoretic models and the term models. Both models develop from the corresponding model constructions for combinatory logic and λ calculus.
1.4.1 Recursion theoretic models.
The standard recursion-theoretic model of BON is obtained by taking as domain the natural numbers and interpreting application as partial recursive function application so that t applied to s is {t∗}(s∗).
It is an easy exercise in elementary recursion theory to find appropriate natural numbers (depending on an underlying enumeration of the partial recur- sive functions) to interprete the individual constants k, s, etc. in this model.
However, one may also consider recursion theoretic models based on higher recursion theory. For example, for the interpretation of the quantification oper- ators, discussed in Section 1.6, one takes as a basis Π1 recursion theory.
It is trivial that the recursion theoretic models satisfy the possible axiom that everything is a natural number: ∀x.N(x) (we will consider this axiom in the treatment of least fixed point operators in applicative theories in Section 1.8). It also follows immediately that the models are partial, in the sense, that there is a term which cannot be interpreted in the domain. For instance, for the term notN in these models ¬ notN ↓ holds.
Therefore, (Tot) cannot hold in recursion theoretic models. Likewise, ex- tensionality, (Ext), cannot be verified in these models.
1.4.2 Term models
Besides the recursion theoretic models, the term models provide a second class of natural models, cf. [Bee85, JS95b, Can96, Str96a]. They can be divided in (at least) two forms: The normal term models and the total term models.
In both cases we start from a reduction relation defined on arbitrary closed terms of the language. For BON it reads as follows: