[Gajurgensen]

The encoding of natural numbers in lambda calculus can be mysterious at first glance. I'm surprised the author didn't spend more time on it. No need to be so hostile about it though.

Essentially, we represent numbers as functions that will call a function a number of times on a base value. So for `zero = λs. λz. z`, we can see if we gave it a function `s`, and a value `z`, it would apply `s` zero times to `z`. For `one = λs. λz. s z`, clearly `s` is applied once to `z`. I think you can see the rest of the pattern. Its really as simple as that.

We can then define the successor function as `suc = λn. λs. λz. s (n s z)` (I'm not sure why the author doesn't write this out. Instead he confuses the successor function with the `s` argument). We can see `suc` behaves as expected with examples. `suc one = (λn. λs. λz. s (n s z)) one = λs. λz. s (one s z) = λs. λz. s ((λs. λz. s z) s z) = λs. λz. s (s z) = two`. All we need is our definition of `zero` and `suc`, and we can define any natural number.

Now go back and look at the definition of `plus` and it should make a lot more sense.