5.2.10 Sidetrack: Predicates versus Functions

A somewhat deeper motivation.

When we introduced our tree notation for formulas (in Section 5.2.5) we also said that we use the application symbol @ in atomic formulas of first order logic and their tree representations. So we write for instance the application instead of and the two nested applications instead of . We've introduced this as a simple change of notation, but in fact there's a somewhat deeper motivation behind it.

Using function symbols

As you may remember from the sidetrack on typed -calculus, the semantics of -expressions is generally defined in terms of functions, and the symbol @ is understood as functional application of the functor (to the left of the @) to the argument (to the right). Thus the semantics of an application is the result of applying the function denoted by to whatever is denoted by . Now with our new notation (which is quite common for -based formalisms), this ``function-and-application perspective'' on the syntax and semantics is extended to atomic formulas.

What exactly does this mean?

  1. Syntactically, what used to be predicate and relation symbols are treated alike, as one-place function symbols that are combined with other symbols using the application symbol @. n-ary predications are written as n nested applications.

  2. This means that the semantics of our (former) predicate and relation symbols has to be given in terms of unary functions if we want to interpret the @-symbol as functional application consistently. In short, we have to re-define models such that they interpret predicate symbols (which are by definition unary) as the characteristic function of the set that we used to assign to the respective symbol. The characteristic function of a set is the function that assigns to all entities in that set, and to all other entities. Unary predications can then be stated equivalently as application of such a function to the argument of the predication. On this basis, n-ary predicates are interpreted as complex functions, allowing us to express n-ary predications as a series of nested functional applications. This series has to end with the application of the characteristic function of some set, resulting in a truth value.

Examples: Expressing predicates by functions

This was a bit abstract, so here are two examples. First let's look at the predicate symbol . Here, the situation is easy: A predicate symbol used to be interpreted as the set of things in the extension of the respective predicate in the model under consideration. In our example that's the set of all men, (assuming that we're looking at a model that really interprets the symbol as counterpart of the word ``man''). Now, we will simply use the characteristic function of that same set instead, hence in our example the function that yields if its argument is a man (and thus would have been in the extension of in our old model), and false otherwise.

But what can we do for relation symbols? How do we give an interpretation in terms of a unary function that corresponds in the right way to an n-ary relation? The solution is to use functions that yield functions as a result. We can do this in such a way that we finally arrive at the characteristic function of some set. Let us look at the example of the (former) relation symbol . We used to interpret this symbol as the set of ordered pairs such that the first element loves the second. Instead we will now interpret it as a unary function that takes each entity to the characteristic function of the set of all things that love that entity.

Let's see how we interpret

versus

We shall assume that we are looking at a model where is assigned Mary and is assigned John. The first formula is true if the pair is in the set assigned to by our model. For the second formula, we will proceed in two steps. First we apply the function that our model assigns to the symbol to John. This yields the characteristic function of the set of ``john-lovers'', which we apply in turn to Mary. This final application gives us the result in case Mary loves John in our model, and otherwise.

All other n-ary relations are treated analogously to our example: As functions that yield the characteristic function of some set after n-1 applications. Clearly we can characterize situations just as well using this functional way of speaking as we could with our familiar relational approach.

Connection to lambda-calculus

What's the great advantage of all this? As we've mentioned above, our new notation and interpretation fit in well with -calculus. And now that we know something about the interpretation of atomic formulas, we can see why this is so. If you recall what we've said about the interpretation of -expressions in Section 3.4.4, you will realize that the functional interpretations we've just discussed for our former predicate and relation symbols are constructed exactly along the lines of the semantics for -expressions such as and . In fact for any of our unary function symbols ``written on its own'', there's an equivalent -expression where the functional character has been made explicit. We say that the function symbol is -equivalent to its explicit -counterpart (and the other way round). Strictly speaking, there are always many -expressions that are -equivalent to one function symbol, because (as usual) -equivalence doesn't make a difference. Here's an example: and are -equivalent, and so are and , etc.

A simplification

For practical purposes this means that we can use the (shorter) function symbols for common nouns directly in semantic construction, instead of their -equivalent (long) -terms. For example we used to write (or, lately, ) as the translation of ``man'', and translated the NP ``a man'' as:

But now we know the functional semantics of on its own, and so we know that we can apply the determiner to that function directly, to the same effect:

We will make use of this simplification in our implementation of CLLS (see in particular Section 6.3.1).


Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)