3.4.1 Lambda-Abstraction

Introduction of -expressions and related concepts.

-expressions are formed out of ordinary first order formulae using the -operator. We can prefix the -operator, followed by a variable, to any first order formula or -expression. We call expressions with such prefixes -abstraction s (or, more simply, abstractions). We say that the variable following a -operator is abstracted over . The variable abstracted over is (-)bound by its respective -operator within an abstraction, just as a quantified variable is bound by its quantifier inside a quantification.

Abstractions

So the following two are examples of -abstractions:

In the first example, we have abstracted over . Thus the in the argument slot of is bound by the in the prefix. In the second example, we have abstracted twice: Once over and once over . So the in the first argument slot of is bound by the first , and the is bound by the second one.

Missing Information

We will think of occurrences of variables bound by as placeholders for missing information: They will serve us to mark explicitly where we should substitute the various bits and pieces obtained in the course of semantic construction. Let us look at our first example -expression again. Here the prefix states that there is information missing in the formula following it (a one-place predication), and it gives this ``information gap'' the name . The same way in our second example, the two prefixes and give us separate handles on each of the two information gaps in the following two-place predication.

While the -bound variables in our two examples act as placeholders for missing constant symbols, we will also use -prefixes to mark other kinds of missing information. For instance we will use -prefixes and variables to mark the gaps where information is missing in the template associated with the indefinite article ``a'' (don't care about the @-symbol for now. We'll explain what it means in a minute):

Here, and stand for missing predicate symbols. The version of -calculus introduced here does not distinguish variables that stand for different kinds of missing information. Nevertheless we will stick to a convention of using lower case letters for variables that stand for missing constant symbols, and capital letters otherwise.