# Definition of integers needs explaining

Zero and one are defined by the successor function.

\begin{align*} &0 ≡ λsz.z \\ &1 ≡ λsz.s(z) \end{align*}

But why? $λsz.z$ is irreducible to a value. If I call this function on some value, I get back $z$, which is merely a variable in itself. If I call the function on two values, I get back the second value, which is not necessarily zero.

And yet we're just assigning the function the value $0$? Why? Why not assign zero to say $λs.(λz.xyt)$. This seems arbitrary.

This is from the arithmetic section of: http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf

• If you apply $\lambda s z.z$ to a value you get back $\lambda z.z$. Note that $\lambda s z.z$ is shorthand for $\lambda s.\lambda z.z$. – Derek Elkins left SE Dec 4 '16 at 22:55

The natural numbers don't exist natively in the world of lambda calculus, and so if we want to use them, we have to define them somehow. You are describing the Church numerals, one possible definition which supports arithmetic. Church defines $n$ to be the function $(s,z) \mapsto s^{(n)}(z)$ that maps a pair $(s,z)$ into an $n$-fold application of $s$ to $z$. In particular, when $n = 0$ we get $(s,z) \mapsto z$.