Step-by-step explanation:
I do not know how to solve this incredibly difficult question. The complexity rivals those of the millennial problems. Instead, I’ll let reddit user u/sellopou speak his words.
Take a computational approach to the problem. Specifically, consider the encoding of natural numbers in the simply-typed lambda calculus called Church numerals. In this encoding, the number 2 is represented by a function that looks like this:
2 ≡ λf.λx.f (f x) Â
In other words, the number two is a function that takes a function and some value (let's assume that we're comfortable with currying here), and applies the function twice to the value. In general, a number n is represented by a function that takes a function and some value and applies f to the value n times.
Using the Church encoding, you can define operations on the numbers as well. In this case, you're interested in plus, which takes two numbers and returns a number
plus ≡ λm.λn.λf.λx.??? Â
So what's in the body? Well, the body has to be n + m applications of f to the value x. If we pass f and x to n, we get n applications–call that r, and if we apply m to f and r, that'll be m + n applications of f:
plus ≡ λm.λn.λf.λx.m f (n f x) Â
So the expression 2 + 2 using this encoding is:
plus 2 2 ≡ (λm.λn.λf.λx.m f (n f x)) (λf.λx.f (f x)) (λf.λx.f (f x)) Â
Now β-reduce until you get the result:
plus 2 2 ≡ (λm.λn.λf.λx.m f (n f x)) (λf.λx.f (f x)) (λf.λx.f (f x)) Â
    ↦ (λn.λf.λx.(λf.λx.f (f x)) f (n f x)) (λf.λx.f (f x)) Â
    ↦ (λf.λx.(λf.λx.f (f x)) f ((λf.λx.f (f x)) f x)) Â
    ↦ (λf.λx.(λx.f (f x)) ((λf.λx.f (f x)) f x)) Â
    ↦ (λf.λx.(λx.f (f x)) ((λx.f (f x)) x)) Â
    ↦ (λf.λx.(λx.f (f x)) (f (f x))) Â
    ↦ (λf.λx.f (f (f (f x Â
    ≡ 4. Â
But now, let's bust out of this theoretical prison and say we have a number 0 in some representation that we can actually work with, as well as a function add1 that knows how to increment a number in that representation. Well, then we can get a useable representation out of our church numeral, by applying to the numeral to add1 and the value:
4 add1 0 = 4
Then you remove 1 for the sake of simplicity.
3.