These questions concern concern issues with substitution and Skolemization.

a. Given the premise ∀ x ∃y P(x, y), it is not valid to conclude that ∃q P(q, q). Give an example of a predicate P where the first is true but the second is false.

b. Suppose that an inference engine is incorrectly written with the occurs check omitted, so that it allows a literal like P(x, F(x)) to be unified with P(q, q). (As mentioned, most standard implementations of Prolog actually do allow this.) Show that such an inference engine will allow the conclusion ∃y P(q, q) to be inferred from the premise ∀ x ∃y P(x, y).

c. Suppose that a procedure that converts first-order logic to clausal form incorrectly Skolemizes ∀ x ∃y P(x, y) to P(x, Sk0)—that is, it replaces y by a Skolem constant rather than by a Skolem function of x. Show that an inference engine that uses such a procedure will likewise allow ∃q P(q, q) to be inferred from the premise ∀ x ∃y P(x, y).

d. A common error among students is to suppose that, in unification, one is allowed to substitute a term for a Skolem constant instead of for a variable. For instance, they will say that the formulas P(Sk1) and P(A) can be unified under the substitution {Sk1/A}. Give an example where this leads to an invalid inference.