SKEDSOFT

First-order Logic (FOL) and Validity: Below, we will introduce many notions of first-order logic intuitively, through examples. We refer the reader to one of many excellent books in first-order logic for details. One step called skolemization merits some explanation. Basically, skolemization finds a witness to model the existential variable. In general, from a formula of the form ∃X.P(X), we can infer P(c) where c is a constant in the domain. Likewise, from P(c), we can infer ∃X.P(X); in other words, for an unspecified constant c in the domain,
∃X.P(X) ⇔ P(c).
We will use this equivalence in the following proofs. There is another use of skolemization illustrated by the following theorem (which we won’t have occasion to use):
∀X.∃Y.P(X, Y ) ⇔ P(X, f(X)).
Here, f is an unspecified (but fixed) function. This equivalence is valid because of two reasons:

• The right-hand side leaves X as a free variable, achieving the same effect as ∀X goes, as far as validity goes (must be true for all X).
• The right-hand side employs f(X) to model the fact that the selection of ∃Y may depend on X.

A warm-up exercise: Suppose we are given the following proof challenge: Some patients like every doctor. No patient likes a quack. Therefore, prove that no doctor is a quack. It is best to approach problems such as this using predicates to model the various classes of individuals2 instead of employing ‘arbitrary constants’ such as p and d to denote patients, doctors, etc. Introduce predicate p to carve out a subset of people (P) to be patients, and similarly d for doctors. Let l (for “likes”) be a binary relation over P. Our proof will consist of instantiation of formulas, followed by Modus ponens, and finally proof by contradiction.

A1: The statement, “Some patients like every doctor:”
∃x ∈ P : (p(x) ∧ ∀y : (d(y) ⇒ l(x, y))).
A2: The statement, “No patient likes a quack:”
∀x, y ∈ P : (p(x) ∧ q(y)⇒ ¬l(x, y)).
Proof goal: “No doctor is a quack.”
∀x ∈ P : (d(x) ⇒¬q(x)).
Negate the proof goal: ∃x ∈ P : (d(x) ∧ q(x)).
Skolemize negated proof goal: (x0 ∈ P ∧ d(x0) ∧ q(x0).
Skolemize A1: c ∈ P ∧ (p(c) ∧ ∀y : (d(y) ⇒ l(c, y))) (we will suppress domain membership assertions such as c ∈ P from now on).
Specialize: From A1, we specialize y to x0 to get: p(c) ∧ (d(x0) ⇒ l(c, x0)). But since d(x0) is true in the negated proof goal, we get: p(c) ∧ l(c, x0) (more irrelevant facts suppressed). Since q(x0) is true in the negated proof goal, we also get: p(c) ∧ l(c, x0) ∧ q(x0). Use A2 and specialize x to c and y to x0 to get ¬l(c, x0).
Contradiction: Since we have l(c, x0) and ¬l(c, x0), we get a contradiction.