1.4 The Lambda Calculus
Towards the end of the last section we saw how to transfer as much information as possible about the syntactic structure of a sentence into a kind of proto-semantic representation. But we still completely lack a uniform way of combining the collected semantic material into well-formed first order formulas.
In this section we will dicuss a mechanism that fits perfectly for this task. It will allow us to explicitly mark gaps in first-order formulas and give them names. This way we can state precisely how to build a complete first order formula out of separate parts. The mechanism we're talking about is called 
-calculus. For present purposes we shall view it as a notational extension of first order logic that allows us to bind variables using a new variable binding operator . Here is a simple -expression:
The prefix 
binds the occurrence of 
in 
. That way it gives us a handle on this variable, which we can use to state how and when other symbols should be inserted for it.