arithmetic definition in lambda calculus

Question

As the lambda calculus wiki said:

There are several possible ways to define the natural numbers in lambda calculus, but by far the most common are the Church numerals, which can be defined as follows:

0 := λf.λx.x
1 := λf.λx.f x
2 := λf.λx.f (f x)
3 := λf.λx.f (f (f x))

I just know the part λx.x in 0 definition is identity function and the numerals is related to how many times f repeated(in 0 f repeated 0 time), but why defined like this, how to explain λf.λx.x(0) and λf.λx.f (f x)(2) in a sentence that can be easily understand(especially what f stand for).

---

Add: Is there anything worth being explained about the definition?

Answer 1

Since everything is a lambda term, in lambda calculus you can only define lambda terms (functions) that “operates” on other lambda terms (the only “values” allowed, that are written with the λ notation).

So, if we want to show, from a theoretical point of view, that the lambda calculus allows one to write any computable function, we need to find a suitable representation (encoding, in technical terms) of natural numbers, over which to define computable functions (note that with the Church encoding, you are representing through lambda terms numbers, and not numerals !).

Having encoded the numbers as lambda terms, one can define all the usual functions on “numbers”. For instance, the successor function can be defined as:

SUCC := λn.λf.λx.f (n f x)

that takes a “number” (that is, a lambda term which encodes a number) and returns its successor (that is, the lambda term which encodes the successor of that number). So that, for instance, ((SUCC) 0) β-reduces to 1 (that is ((λn.λf.λx.f (n f x)) λf.λx.x) is β-equivalent to λf.λx.f x), and so on. And starting from this, one can define all the other functions on “numbers”, like sum, multiplication, exponentiation, etc.

What is the use of such encoding? Of course, it is not useful to give a practical programming language to perform the sum of two numbers. But it allows the study of this formalism in the field of computability theory, for instance, to provide a way of expressing the Church-Turing thesis, that asserts that any computable operator (and its operands) can be represented under Church encoding.