Example 10.1

For our first example we take the one that came up in Chapter 6, when we first introduced the topic of universally valid implications:

P1 ∀x (R(x)→H(x))
P2 R(t)
C ∃y H(y)

A possible interpretation is:

P1: All rich people are happy
P2: Tony is rich
C: Somebody is happy

Is it true that P1 and P2 imply C, in all models? The test is to see whether or not the conjunction W = P1∧P2∧¬C is satisfiable. To this end we first of all transcribe P1, P2 and ¬C into Laws of Form notation:

Then re-express ∀x and ∃y in terms of Πx and Πy:

Remove the Pi's (as they are already in the outermost space):

Perform two resolutions, as indicated in the diagram:

The substitution required for the first resolution is {t/x}; for the second, {t/y}. We have obtained the mark O, therefore W is unsatisfiable and the implication is proved valid. There is no way (no model in which) it couldn't be.

Example 10.2

For our second example we prove the universal validity not of an implication but of a simple statement S. (Actually this may be thought of as an implication but where the premise is simply: nothing - the void.)

S ∀x (Px→(∃y Py))

We consider the negation of S, transcribed:

Re-express ∀x and ∃y in terms of Πx and Πy:

Πx is stuck in level -1, calling for Skolemization: so we remove Πx and replace all occurrences of x by x, leading to

Remove the Πy, and resolve just once this time...

(with substitution {x/y} ). Thus the negation of S is impossible, which means that S itself is universally valid.


A good online source of problems in first order logic is Chapter 8 of the old edition of Symbolic Logic: A First Course by Gary Hardegree. This is Example 3 (page 424):

P (∀x Fx) → (∃y Gy)
C ∃x (Fx→Gx)

The task is to show that P implies C. Here are P and ¬C transcribed:



with resolution (using substitutions {x/z}, {y/w})



This is Example 28 from page 450 of Hardegree:

P1 ∀x (Fx → Gx)
P2 ¬∃x(Gx ∧ Hx)
C ∀x (Fx→¬Hx)

We have to show P1 and P2 imply C. We transcribe P1∧P2∧¬C, changing the 'bound' variables to make them all different:



resolving as



This is Example 66 from page 461 of Hardegree:

P ∃x (¬∃y (Fy ∧ Rxy))
C ∀x (Fx→(∃y ¬Ryx))

Our task is to show that P implies C. We transcribe P∧¬C, changing the 'bound' variables in C to make them different to the variables of P:


Skolemizing Πx, Πa, then discarding Πy, Πb, we obtain

resolving as



This is Example 67 from page 461 of Hardegree:

P1 ∀x (Fx → (∃y ¬Kxy))
P2 ∃x (Gx ∧ (∀y Kxy))
C ∃x (Gx ∧ ¬Fx))

Transcription of P1∧P2∧¬C:


Because Πy lies within the scope of Πx, Skolemization converts y into yx, with subscript x. The variable a, however, is converted into plain a. So we obtain

resolving as