Lambda calculus is for functional computation so there is nothing in it as numbers but we can somehow have definitions like what we had for True or False and other logical elements, for natural numbers too. The way we are going to introduce the natural numbers is called Church numbers because he was the one who first introduced this in Lambda calculus.
In this definition a higher order function represents a natural number, depending on what number we are showing we need to use n times composition of a function (any function) on itself to show the number n, look at the bellow:
0 : x → λf.λx.x // applying 0 times to the given input
1 : f ( x ) → λf.λx.f x // applying 1 times to the given input
2 : f ( f ( x ) ) → λf.λx.f ( f x ) // applying 2 times to the given input
3 : f ( f ( f ( x ) ) ) → λf.λx.f ( f ( f x ) ) // applying 3 times to the given input
4 : f ( f ( f ( f ( x ) ) ) ) → λf.λx.f ( f ( f ( f x ) ) ) // applying 4 times to the given input
n : f ( f ( ... f ( f ( x ) ) ... ) ) → λf.λx.f^n x // f^n means applying n times ...
As you see depending on what number we are going to represent, we composite n times the function on a given single argument.
You really want numbers?
The way church defines numbers is a general solution and if you want you still can drive mathematical numbers too. For example, in a very special situation when x equals to 0 and the function is like successor operator, then these compositions really return the n-th natural number.
Successor function
If you look deeply on the number representations above, you'll find we can define general form of successor operator for church numbers as bellow:
λn.λf.λx. f (n f x)
For example if you pass number 2 or λf.λx.f (f x) to this abstraction you'll get number 3, see:
(λn.λf.λx. f (n f x)) λf.λx.f (f x) → λf.λx.f (f(f x))
Addition
It is not difficult to find out how easy we can define other basic operators like add, multiply, power and ... look at the bellow:
m + n : λm. λn. λf. λx.m f (n f x)
For example, if you want to add 1 to 2 we have:
(λm. λn. λf. λx.m f (n f x)) λf.λx.f x λf.λx.f ( f x ) →
→ λf.λx.λf.λx.f x f (λf.λx.f ( f x ) f x) → λf.λx.λf.λx.f x f (f ( f x )) → λf.λx.f (f ( f x )) // which is 3
Multiplication
And you know multiplication is not anything but repeated adding so we can have:
m * n : λm.λn.λf.λx.m (nf) x
Let us just, for example, show how the above formula leads to m * n abstraction, if you have trouble to understand it, just forget about it, you can still verify the abstraction by passing some Church number to it, we are going to use some conversions and reductions to proof this:
(λm.λn.λf.λx.m (nf) x) M N → (λmnfx.m(nf) x) M N → (λnfx. M (nf) x) N  → λfx. M (N f) x
We replace M with λgx.g^m x so we have:
→ λfx.(λgx.g^m x) (n f) → λfx.(n f)^m x
Now we replace N with λhx.h^n x so we have:
→ λfx.((λhx.hn x) f)^m x → λfx.(f n)m x → λfx.(f^m)^n x → λfx.f^(m+n) x → λf.λx.f^(m+n) x
So that is it. Again if it was a bit difficult to understand, forget about it, we are programmers, not mathematicians. But if you just simply take a look at the results you see the similarities we have here with what we have in logarithm, I mean using power operator in place of add or multiply.
