Skip to main content

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:


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)

Video cover image

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).

Exercises Exercises



[1] ∀x (∃y (∀z (P(x, y, z))))

Which of the following statements could result from a correct application of the Instantiation rules that we have presented? Assume that all uses of Universal Instantiation derive arbitrary elements.

  1. P(a, b*, c)

  2. P(a, f(a), c)

  3. P(a, f*(a, ), c)

  4. P(a, b*, a)

Correct answer is B.

Explanation: P(a, f(a), c) is correct. We must instantiate from the outside in. So first we apply Universal instantiation to x. We choose the arbitrary element a and we get:

y (z (P(a, y, z)))

Next we apply Existential Instantiation to y. But y originally occurred inside the scope of x, which has now been instantiated as the arbitrary value a. So we must reflect the fact that y depends on a. So we write:

z (P(a, f(a), z))

Finally, we apply Universal Instantiation again, this time to z. We get:

P(a, f(a), c)

All the others are wrong because they do not handle the Existential Instantiation step correctly.