Reasoning: An Introduction to Logic, Sets, and Functions

Subsection 5.1.15 Skolem Functions

But first, before we introduce our last new rule, let’s explain the second restriction on the use of this instantiation rule. Suppose that we began with the following expression, with respect to the universe of bears:

[1] ∀x (∃y (MotherOf(y, x)))

If we wish to use the instantiation rules, we must begin at the outside (in other words, with the entire statement). So we first instantiate x. If we do that for a specific value, say Smokey, then we get:

[2] ∃y (MotherOf(y, Smokey))

Now we can give a name to the particular individual who is Smokey’s mother. We can write:

[3] MotherOf(c*, Smokey)

We haven’t gotten into any trouble (yet).

But now suppose that we begin by instantiating x with an arbitrary element. Recall that we do this when we want to reason about that arbitrary element, typically with the intent of generalizing it later. When we do this, we can make no specific claims about the value that we choose. So, in particular, we can’t claim that there’s any one c* who is the mother of any arbitrary bear. Clearly different bears can have different mothers.

We can still apply the Existential Instantiation rule. But we must make clear that the value we’re asserting the existence of depends on the value that is chosen for x. To do that we’ll use the notation:

f(x),

which we’ll read as, “f of x”, meaning “a value that depends on x”.

So, suppose that we’d used Universal Instantiation on [1] to produce:

[4] ∃y (MotherOf(y, a))

Then we can use Existential Instantiation to produce:

[5] MotherOf(f(a), a)

So we have that, no matter who a is, there’s something, whose value depends on a, who is a’s mother.

What if the original existentially quantified expression occurred inside the scope of two or more universal quantifiers? Easy. We simply make the instantiated value depend on all of them.

Suppose for example, that we want to claim that, for every pair of Facebook users, there’s a definition of their Facebook relationship. (This definition includes whether they are friends, whether one has hidden the other, etc.) Then (assuming a universe of Facebook users) we could write:

[6] x (y (z (FBRelDef(z, x, y))))

After applying Universal Instantiation twice, we will have:

[7] z (FBRelDef(z, a, b))

Then we apply Existential Instantiation and we get the fact that the Facebook relationship that exists for a and b depends on who a and b are:

[8] FBRelDef(f(a, b), a, b)

Nifty Aside

Objects such as c*, are sometimes called Skolem constants. Objects such as f(a) and f(a, b) are sometimes called Skolem functions. While it’s true that these objects are clunky for us to reason with, they play a very important role in some computational logic systems (i.e., programs that produce proofs).