I have what I would call a philosophical question about λ-calculus.

When you explore λ-calculus you will be surprised to see all the things that you can do there.  You can define integers, arithmetic operations, booleans, if-then-else statements, loops, recursive functions, etc.  I believe it has been proven computationally complete.

But on the other side, if you consider what you can do with functions in λ-calculus, you realize that the only thing you can do is to feed it a function and it returns another function.  And that process never ends.

So how can you extract a result from a computation?

Suppose the result of an expression is function `f`.  You want to check whether `f` is what you expected.  You can test it, take a function you know, apply `f` to it and receive `g`.  But to check `g` is correct, you now need to verify what `g` does.  And you start all over.  So how can you tell anything about `f`?

It seems to me that you can replace all functions in λ-calculus by a single function, the identity function `I = λx.x`, and everything still works as described in λ-calculus.  The Church numeral `3` when given `f` and `x` returns `f(f(f(x)))`.  But since `f` and `x` can only be `I`, it returns `I`.  `I` applied to `I` and `I` also returns `I`.  So `I` satisfies the definition of `3`.  The “booleans” `(λxy.x)` and `(λxy.y)` need 2 arguments, which will be `I` and `I` so both booleans will return `I`.  Each is equivalent to the identity, even though they behave exactly according to their definitions.

So how do you make the difference?  How do you show that λ-calculus deals with more than just a single function?

Is there a concept of identity?  Can you identify a function immediately without evaluating it?  I believe it was proven that there is no way to test 2 functions for equality.

Or is λ-calculus not about functions, but about the formal description of what they do?  That would mean that λ expressions not only define what the functions do but are also the data that the functions manipulates.  So when you write `A B`, you don't apply `A` to `B`, but you apply the function described by the string `A` to formal definition of a function contained in `B` returning another formal definition.

What is actually going on in λ-calculus?  What is the mathematical objects it deals with?

EDIT: OK, from the answer below it seems that λ-calculus is not so much about functions in the mathematical sense, but about the subset of functions that can be expressed as λ expressions.  Or even more about the manipulation of λ expresssions.