14. Deduction for First-Order Logic

The fundamental difference between propositional logic and first-order logic is that in first-order logic there are variables and terms that stand for objects, and we can form atomic propositions that depend on those objects. Within the framework, the two key ingredients are equality and the quantifiers. Deduction systems for first-order logic have to extend those for propositional logic by providing rules for these.

As was the case for propositional logic, all the deductive systems we describe in this section are sound and complete for first-order logic, though we do not provide detailed proofs here.

14.1. Axiomatic systems

We have already discussed equational reasoning in Section 12.3. We have seen that the natural rules for equality are given by reflexivity, symmetry, transitivity, and congruence with respect to functions and relations. These can be expressed as rules, but also as first-order axioms:

  • \(\fa x x = x\)

  • \(\fa {x, y} x = y \limplies y = x\)

  • \(\fa {x, y, z} x = y \land y = z \limplies x = z\)

  • \(\fa {x_1, \ldots, x_n, y_1, \ldots, y_n} x_1 = y_1 \land \cdots x_n = y_n \limplies f(x_1, \ldots, x_n) = f(y_1, \ldots, y_n)\)

  • \(\fa {x_1, \ldots, x_n, y_1, \ldots, y_n} x_1 = y_1 \land \cdots x_n = y_n \land R(x_1, \ldots, x_n) \limplies R(y_1, \ldots, y_n)\).

From these, we can derive substitution for terms and formulas:

  • \(\fa {x, y} x = y \limplies t(x) = t(y)\)

  • \(\fa {x, y} x = y \land A(x) \limplies A(y)\)

Sometimes these are taken as axioms instead of congruence. Remember that we are adopting the convention what when we use notation like \(t(x)\), we have in mind a certain variable \(z\) that \(t\) might depend on and we take \(t(x)\) to stand for \(t[x/z]\) and \(t(y)\) to stand for \(t[y/z]\). Similar conventions hold for formula \(A(x)\).

The axioms for the quantifiers follow naturally from their meanings:

  • \((\fa x A) \limplies A[t/x]\)

  • \(A[t/x] \limplies \ex x A\).

The first says that if \(A\) holds of everything, then it holds of any particular thing, and the second says that if \(A\) holds of any particular thing, then it holds of something.

These axioms are only half the story, though. The first axiom tells us how to use a statement that starts with a universal quantifier but not how to prove it, and the second one tells us how to prove a statement with an existential quantifier but not how to use it. How do we prove \(\fa x A\)? Establishing \(\fa x A\) involves showing that \(A\) holds of an arbitrary value of \(x\). To do that, we let \(x\) be arbitrary, and prove \(A\). This suggests the following rule of generalization:

From \(A\), conclude \(\fa x A\).

The actual rule we use is a generalization of this: if we have shown that \(A\) follows from \(B\), and \(B\) doesn’t say anything about \(x\), then we have shown that \(B\) implies that \(A\) holds for any \(x\) at all.

  • From \(B \limplies A\) conclude \(B \limplies \fa x A\), assuming \(x\) is not free in \(B\).

The dual rule for the existential quantifier says that if \(B\) follows from the assumption that \(A\) holds of some \(x\), then \(B\) follows from the assumption that there exists an \(x\) satisfying \(B\).

  • From \(A \limplies B\) conclude \((\ex x A) \limplies B\), assuming \(x\) is not free in \(B\).

14.2. A sequent calculus

We can also extend the cut-free sequent calculus described in Section 8.2 to first-order logic. Remember that the system derives sets of formulas \(\Gamma\) in negation-normal form. We interpret a proof as telling us that in any model, and with any assignment to the free variables, at least one of the formula in \(\Gamma\) is true. In the case of propositional logic, we took the axioms to be finite sets \(\Gamma\) that contain a complementary pair of atoms \(P\) and \(\lnot P\). In the presence of equality, we now take the axioms to be sets \(\Gamma\) such that the set of negations of those formulas can be refuted using equational reasoning. For example, \(\lnot P(a), a \ne b, P(b)\) is an axiom, because equational reasoning refutes the set \(P(a), a = b, \lnot P(b)\). We can determine whether a finite set of formulas is an axiom using congruence closure.

The other rules of the system are as follows:

\[\begin{prooftree} \AXC{$\Gamma, A$} \AXC{$\Gamma, B$} \BIC{$\Gamma, A \land B$} \end{prooftree} \quad\quad \begin{prooftree} \AXC{$\Gamma, A, B$} \UIC{$\Gamma, A \lor B$} \end{prooftree} \] \[\begin{prooftree} \AXC{$\Gamma, A$} \UIC{$\Gamma, \fa x A$} \end{prooftree} \quad\quad \begin{prooftree} \AXC{$\Gamma, A[t/x]$} \UIC{$\Gamma, \ex x A$} \end{prooftree} \]

In the rule for the universal quantifier, we require that \(x\) is not free in any formula in \(\Gamma\). This is analogous to the requirement in the previous section that \(x\) is not free in the formula \(B\) in the generalization rule. You can think of it as saying that \(x\) is really arbitrary.

As in Section 8.2, we can add the cut rule, which represents a form of modus ponens. In class, we will sketch a proof that this system is complete even without the cut rule.

14.3. Resolution

We now explain how to extend propositional resolution to the first-order setting. As with propositional resolution, first-order resolution is a refutational proof system: to prove \(A\), we assume \(\lnot A\) and derive a contradiction. Remember that propositional resolution required us to put formulas in conjunctive normal form. Having quantifiers complicates things. One option is to put \(\lnot A\) in prenex form, with all the quantifiers in front, and then put the quantifier-free part of the formula in CNF. This is a step in the right direction, but the presence of existential quantifiers makes automated reasoning more difficult, so we introduce a method, Skolemization, to get rid of them.

Here is the idea. Suppose we are trying to refute a formula of the form \(\fa x \ex y A(x, y)\). From a semantic point of view, we are trying to show that this formula is unsatisfiable. Let \(f(x)\) be a new function symbol. We claim that \(\fa x \ex y A(x, y)\) is equisatisfiable with \(\fa x A(x, f(x))\). As a result, we can refute \(\fa x \ex y A(x, y)\) by refuting \(\fa x A(x, f(x))\). One direction of the claim is easy: any model of \(\fa x A(x, f(x))\) is a model of \(\fa x \ex y A(x, y)\). To see this, notice that if \(\mdl M\) satisfies \(\fa x A(x, f(x))\), then it also satisfies \(\fa x \ex y A(x, y)\): given any value \(a\) in the universe of \(\mdl M\), if we set \(b\) equal to \(f^{\mdl M}(a)\), then \(A\) holds of \(a\) and b in \(\mdl M\). For the other direction, suppose \(\mdl M\) is a model of \(\fa x \ex y A(x, y)\). That means that for every value \(a\) in the universe of \(\mdl M\), there is a value \(b\) such that \(A\) holds of \(a\) and b. We can then interpret \(f\) as any function that, for any \(a\), returns such a value \(b\).

More generally, given any formula \(A(x, y)\) and a new function symbol \(f(x)\), we can expand any model for the language of \(A\) with an interpretation of \(f(x)\) satisfying \(\fa x (\ex y A(x, y)) \liff A(x, f(x))\). We simply interpret \(f(x)\) as a function that, whenever there is a \(y\) in the model satisfying \(A(x, y)\), returns such a \(y\). Such a function is known as a Skolem function for \(\ex y A(x, y)\), and the process of replacing \(\fa x \ex y A(x, y)\) by \(\fa x A(x, f(x))\) is known as Skolemization. The equivalence \(\fa x (\ex y A(x, y)) \liff A(x, f(x))\) is known as the corresponding Skolem axiom. Because we can always choose \(f\) to satisfy the Skolem axiom, we can replace \(\ex y A(x, y)\) with \(A(x, f(x))\) in a set of hypotheses and preserve satisfiability. In general, a formula \(\ex y A(y)\) may have more than one free variable, in which case they should all be arguments to \(f\).

Iteratively eliminating all the existential quantifiers in this way results in a formula in Skolem normal form. It helps to put the sentence in negation-normal form first, because existential quantifiers under negations or on the left side of an implication act like universal quantifiers and vice versa. For example, suppose we are given the sentence

\[\fa {u, x} \ex y (\fa v Q(x, y, u, v)) \to \fa z \ex w R(x, y, z, w)\]

where \(Q\) and \(R\) are relation symbols. First, we rewrite the sentence as

\[\fa {u, x} \ex y (\ex v \lnot Q(x, y, u, v)) \lor \fa z \ex w R(x, y, z, w).\]

First, we replace \(y\) by a Skolem function that depends on \(u\) and \(x\):

\[\fa {u, x} (\ex v \lnot Q(x, f(u, x), u, v)) \lor \fa z \ex w R(x, f(u, x), z, w).\]

Then we replace \(v\):

\[\fa {u, x} \lnot Q(x, f(u, x), u, g(u, x)) \lor \fa z \ex w R(x, f(u, x), z, w).\]

Finally, we replace \(w\):

\[\fa {u, x} \lnot Q(x, f(u, x), u, g(u, x)) \lor \fa z R(x, f(u, x), z, h(u, x, z)).\]

We are now left with only universal quantifiers.

In this example, if we bring \(z\) to the front, we get a universally quantified clause:

\[\fa {u, x, z} \lnot Q(x, f(u, x), u, g(u, x)) \lor R(x, f(u, x), z, h(u, x, z)).\]

More generally, we can always bring the universal quantifiers to the front and put the rest of the formula in conjunctive normal form. Using the identity \((\fa x A \land B) \liff (\fa x A) \land (\fa x B)\), we can then reduce the original sentence to a conjunction of universally quantified clauses.

A resolution proof is designed to refute a set of universally quantified clauses. The resolution rule from first-order logic is now generalized as follows: given two universally quantified clauses, instantiate the universal quantifiers to obtain a complementary literal, resolve, and then generalize. For example, given

  • \(\fa {x, y} A(f(x),y)\) and

  • \(\fa {w, z} \lnot A(w, g(z)) \lor B(w, z)\),

we can do the following:

  • instantiate \(x\) to \(u\) and \(y\) to \(g(v)\) in the first to get \(A(f(u),g(v))\),

  • instantiate \(w\) to \(f(u)\) and \(z\) to \(v\) in the second to get \(\lnot A(f(u), g(v)) \lor B(f(u), v)\),

  • resolve, to get \(B(f(u), v)\), and then

  • generalize, to get \(\fa {u, v} B(f(u), v)\).

We then say that \(\fa {u, v} B(f(u), v)\) has been obtained by resolution from the two hypotheses.

As with propositional logic, a first-order resolution refutation is a proof of the empty clause using the resolution rule. For example, suppose we have the following hypotheses:

  • Every smart and motivated student likes logic.

  • Every student at Carnegie Mellon is smart.

  • At least one student at Carnegie Mellon is motivated.

Let us show that someone likes logic. We introduce predicates \(S(x)\), \(M(x)\), \(L(x)\), and \(C(x)\) for “smart,” “motivated,” “likes logic”, and “is at Carnegie Mellon.” Negating the conclusion and expressing the statements as universally quantified clauses, we get:

  1. \(\fa x \lnot S(x) \lor \lnot M(x) \lor L(x)\).

  2. \(\fa x \lnot C(x) \lor S(x)\).

  3. \(C(a)\).

  4. \(M(a)\).

  5. \(\fa x \lnot L(x)\).

Notice that the existential quantifier in the third hypothesis has been Skolemized to produce the constant \(a\), and that we split the resulting conjunction into two singleton clauses. We now refute the hypotheses as follows:

  1. \(\fa x \lnot C(x) \lor \lnot M(x) \lor L(x)\), from 1 and 2.

  2. \(\lnot M(a) \lor L(a)\), from 6 and 3.

  3. \(L(a)\), from 7 and 4.

  4. \(\bot\) from 8 and 5.

Another example (stolen from John Harrison’s book) is the barber paradox. Suppose we are told that in a given town there is a male barber who shaves all and only those men who don’t shave themselves. We obtain a contradiction by asking who shaves the barber. Formally, this amounts to a refutation of the sentence \(\ex x \fa y S(x, y) \liff \lnot S(y, y)\). Skolemizing and expressing this as a conjunction of clauses, we get:

  • \(\fa y \lnot S(a, y) \lor \lnot S(y,y)\).

  • \(\fa y S(y, y) \lor S(a, y)\).

Instantiating \(y\) to \(a\) in both cases and resolving yields the empty clause.

As you might have guessed, this is where unification, discussed in Section 11.4, comes in handy. When looking for resolvents, though, it’s not always sufficient to look for most general unifiers of a literal from each clause; sometimes a resolution step has to unify two or more literals in the same clause as well. The example of the barber paradox illustrates this. You can check that in this case we are not forced to instantiate both instances of \(y\) to \(a\) unless we consider more than two literals, and anything short of that fails to produce a new clause.

The proof system we have just described is sound and complete for first-order logic without equality. The general method of proof search is implicit in the presentation: systematically searching for substitutions that yield complementary literals and resolving on them is guaranteed to find a refutation if one exists. In general, if there is no refutation, the search may continue forever. We can prove that the calculus is complete, as usual, by arguing that if the search fails to terminate, the failure points the way to the existence of a countermodel.

To handle equality, one option is simply to add equality axioms to the hypotheses. This is inefficient, however. Modern first-order provers use techniques based on paramodulation and superposition.

It is worth mentioning that Skolemization can also be used for search in the cut-free sequent calculus described in the previous section, or, more or less equivalently, in a tableau search. In an ordinary proof system (rather than a refutation system), rather than an equisatisfiable formula, we want one that is equivalid. This requires replacing the universally quantified variables rather than the existentially quantified variables, resulting in Herbrand normal form instead of Skolem normal form. Tableau systems are usually presented, instead, as refutation calculi, in which case Skolem normal form is appropriate.

We close this section with one more example. Consider the following hypotheses:

  1. Every students owns either an iphone or a laptop.

  2. Every student who owns a laptop also owns a pair of bluetooth headphones.

  3. Every iphone is buggy.

  4. Every pair of bluetooth headphones is buggy.

  5. Every student who owns something buggy is sad.

From these we should be able to conclude that every student is sad. We can formalize the hypotheses as follows:

  1. \(\fa x \fn{Student}(x) \to \ex y \fn{Owns}(x, y) \land (\fn{Iphone}(y) \lor \fn{Laptop}(y))\)

  2. \(\fa {x, y} \fn{Student}(x) \land \fn{Owns}(x,y) \land \fn{Laptop}(y) \to \ex z \fn{Owns}(x, z) \land \fn{Headphones}(z)\)

  3. \(\fa y \fn{Iphone}(y) \to \fn{Buggy}(y)\)

  4. \(\fa y \fn{Headphones}(y) \to \fn{Buggy}(y)\)

  5. \(\fa {x, y} \fn{Student}(x) \land \fn{Owns}(x, y) \land \fn{Buggy}(y) \to \fn{Sad}(x)\)

The desired conclusion is \(\fa x \fn{Student}(x) \to \fn{Sad}(x)\). You can check that if we negate the conclusion, Skolemize, put the results in CNF, and move universal quantifiers through the hypotheses, we get the following:

  1. \(\fa x \lnot \fn{Student}(x) \lor \fn{Owns}(x, f(x))\)

  2. \(\fa x \lnot \fn{Student}(x) \lor \fn{Iphone}(f(x)) \lor \fn{Laptop}(f(x))\)

  3. \(\fa {x, y} \lnot \fn{Student}(x) \lor \lnot \fn{Owns}(x, y) \lor \lnot \fn{Laptop}(y) \lor \fn{Headphones}(g(x,y))\)

  4. \(\fa {x, y} \lnot \fn{Student}(x) \lor \lnot \fn{Owns}(x, y) \lor \lnot \fn{Laptop}(y) \lor \fn{Owns}(x,g(x,y))\)

  5. \(\fa y \lnot \fn{Iphone}(y) \lor \fn{Buggy}(y)\)

  6. \(\fa y \lnot \fn{Headphones}(y) \lor \fn{Buggy}(y)\)

  7. \(\fa {x, y} \lnot \fn{Student}(x) \lor \lnot \fn{Owns}(x, y) \lor \lnot \fn{Buggy}(y) \lor \fn{Sad}(x)\)

  8. \(\fn{Student}(a)\)

  9. \(\lnot \fn{Sad}(a)\)

We leave it to you to construct a resolution proof of the empty clause from these.

14.4. Natural deduction

Finally, we can extend the system of natural deduction of Section 8.4. The quantifier rules are as follows:

\[\begin{prooftree} \AXC{$\Gamma, A[t/x] \fCenter B$} \UIC{$\Gamma, \fa x A \fCenter B$} \end{prooftree} \quad \quad \begin{prooftree} \AXC{$\Gamma \fCenter A$} \UIC{$\Gamma \fCenter \fa x A$} \end{prooftree} \] \[\begin{prooftree} \AXC{$\Gamma, A \fCenter B$} \UIC{$\Gamma, \ex x A \fCenter B$} \end{prooftree} \quad \quad \begin{prooftree} \AXC{$\Gamma \fCenter A[t/x]$} \UIC{$\Gamma \fCenter \ex x A$} \end{prooftree} \]

In the right rule for \(\forall\) and the left rule for \(\exists\), the eigenvariable condition amounts to the requirement that \(x\) is not free in any formula other than \(A\). The rules for equality are the same as in Section 12.3, except that in all the rules, we allow a set \(\Gamma\) of formulas on the left side of the sequent.