10.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 explicitely 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
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.
