Conjunctive normal form (first-order logic)

The notion of conjunctive normal form (CNF) known from propositional logic can be adapted to first-order logic. There are, however, some caveats.

Formal definition and conversion theorem

Definition A first-order literal is an atomic or a negated atomic formula. A first-order formula is in conjunctive normal form (CNF) if it is a conjunction of universally closed disjunctions of literals.

Note that this means that a formula in CNF has no free variables.

Example The formula $\forall x_0\forall x_1 (R(x_0) \vee \neg Q(x_0, x_1)) \wedge \forall x_0\forall x_1 (\neg R(f(x_0)) \vee R(x_1)))$ is a first-order formula in CNF, but, strictly speaking, $\forall x_0\forall x_1 \forall x_2(R(x_0) \vee \neg Q(x_0, x_1)) \wedge \forall x_0\forall x_1 (\neg R(f(x_0)) \vee R(x_1)))$ is not, because $x_2$ does not occur free in $R(x_0) \vee \neg Q(x_0, x_1)$.

Theorem

1. Every universal formula without free variables is equivalent to a formula in CNF.
2. There are first-order formulas without free variables which are not equivalent to any first-order formula in CNF.

To prove the first part first observe that every universal formula is equivalent to a universal formula with a matrix in the form $B \bigwedge(\bigvee(L_0^0, \dots, L_{n_0-1}^0), \dots, \bigvee(L_0^{k-1}, \dots, L_{n_0-1}^{k-1}))$, where $B$ is a block of universal quantifications. This can be shown by applying the laws of propositional logic. Using the quantifier laws (distribution), this formula is equivalent to $\bigwedge(B \bigvee(L_0^0, \dots, L_{n_0-1}^0), \dots, B \bigvee(L_0^{k-1}, \dots, L_{n_0-1}^{k-1}))$. Removing all the unnecessary quantifiers yields a formula in CNF.

An example for the second part is $\exists x_0 R(x_0)$.

Clausal notation

The fact that formulas in CNF have a very rigid syntax suggests a simpler notation, the so-called clausal notation.

A finite set of literals is called a clause. When $K$ is a clause, then $\forall\bigvee K$ stands for any formula \begin{align} \forall \bigvee(L_0, \dots, L_{n-1}) \end{align} where $K = \{L_0, \dots, L_{n-1}\}$.

When $M$ is a finite set of clauses, then $\bigwedge \forall \bigvee M$ stands for any formula \begin{align} \bigwedge \{\forall \bigvee K \colon K \in M\} \enspace. \end{align}

Example The formula $\forall x_0 \forall x_1 (P(x_0) \wedge (R(x_0, x_1) \vee \neg R(f(x_0), g(x_1)))$ is equivalent to the formula $\forall x_0 P(x_0) \wedge \forall x_0 \forall x_1 (R(x_0, x_1) \vee \neg R(f(x_0), g(x_1)))$, which can be written as \begin{align} \bigwedge \forall \bigvee \{\{P(x_0)\}, \{R(x_0, x_1), \neg R(f(x_0), g(x_1))\}\} \enspace. \end{align}