Page 28 - Textos de Matemática Vol. 40

16 Chapter 1. Applicative theories
The language Lp of BON comprises, next to s and k, the following con- stants: p, p0, p1 (pairing and projection), 0, sN, pN (zero, successor, and pre- decessor), and dN (definition by cases on N). In very weak theories, we also assume the existence of a constant rN for primitive recursion (see Subsection 1.3.3 below).
We will use the following abbreviations concerning the natural numbers:
t′ := 1 := 0 :=
n+1 := ∀x:N.φ := (t:N→N) := (t:Nm+1 →N) := t∈P(N) :=
sNt,
0′,
0,
n′,
∀x.N(x) → φ, ∀x:N.N(tx), ∀x:N.(tx:Nm →N), ∀x:N.tx=0∨tx=1.
Terms of the form n are called numerals of Lp, and the elements of P(N) are sometimes called sets. We call terms t with (t : N → N) total functions.
As non-logical axioms of BON we have, in addition to the axioms for the partial combinatory algebra, the following ones:
II. Pairing and projection. (3) p0x↓∧p1x↓,
(4) p0(pxy)=x∧p1(pxy)=y. III. Natural numbers.
(5) N(0) ∧ ∀x : N.N(x′),
(6) ∀x:N.x′ ̸=0∧pN(x′)=x,
(7) ∀x:N.x̸=0→N(pNx)∧(pNx)′ =x.
IV. Definition by cases on N.
(8) N(v)∧N(w)∧v=w→dNxyvw=x,
(9) N(v)∧N(w)∧v̸=w→dNxyvw=y.
Sometimes, we will use the shorthand notation (s,t) instead of pst. In
general, we define n tupling by induction on n as follows:
(s1) := s1, (s1,...,sn+1) := ((s1,...,sn),sn+1).
Please note that pairing is introduced independently from the natural num- bers. Since we will consider models of applicative theories where not all defined