about possibly nonterminating general recursive programs are given in Sect. \[sec\_partiality\].

We may define a recursor $R$ for natural numbers in the following way: $$\begin{aligned}
  R &=& \lambda g h x y \,.\, {\ensuremath{\mathrm{Cond}\,({\ensuremath{\mathfrak{0}}}y)\,(g x)\,(h\, x\, ({\ensuremath{\mathfrak{p}}}y)\,
    (R\, g\, h\, x\, ({\ensuremath{\mathfrak{p}}}y)))\,}}.\end{aligned}$$ Note that we need the predecessor as a primitive, because otherwise a recursor would not be definable.

Now $+$, $-$, ${\ensuremath{\cdot}}$, $<$ and $\le$, usually used in infix notation, are defined as follows. $$\begin{aligned}
  x + y &=& R (\lambda x \,.\, x) (\lambda x y z \,.\, {\ensuremath{\mathfrak{s}}}z) x y \\
  x - y &=& R (\lambda x \,.\, x) (\lambda x y z \,.\, {\ensuremath{\mathfrak{p}}}z) x y \\
  x {\ensuremath{\cdot}}y &=& R (\lambda x \,.\, 0) (\lambda x y z \,.\, x + z) x y \\
  x \le y &=& {\ensuremath{\mathfrak{0}}}(x - y) \\
  x < y &=& ({\ensuremath{\mathfrak{s}}}x) \le y\end{aligned}$$

\[lem\_nat\_op\_well\_defined\] The following terms are derivable in the system ${\ensuremath{{\cal I}}}_s$:

-   $\forall x, y : {\ensuremath{\mathrm{Nat}}}\,.\, (x + y) : {\ensuremath{\mathrm{Nat}}}$, $\forall x, y :
        {\ensuremath{\mathrm{Nat}}}\,.\, (x - y) : {\ensuremath{\mathrm{Nat}}}$, $\forall x, y : {\ensuremath{\mathrm{Nat}}}\,.\, (x {\ensuremath{\cdot}}y)
        : {\ensuremath{\mathrm{Nat}}}$,

-   $\forall x, y : {\ensuremath{\mathrm{Nat}}}\,.\, (x \le y) : {\ensuremath{\mathrm{Prop}}}$, $\forall x, 