LARA

Normal Forms for First-Order Logic

Example Formula

We will look at the language ${\cal L} = \{P, R, a, f\}$ where

  • $P$ is relation symbol of arity one
  • $R$ is relation symbol of arity two
  • $a$ is a constant
  • $f$ is a function symbol of two arguments

Consider this formula in ${\cal L}$:

\begin{equation*} \begin{array}{l@{}l} & (\forall x. \exists y.\ R(x,y))\ \land \\ & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\ & (\forall x.\ P(x) \lor P(f(x,a)))\ \\ & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \end{array} \end{equation*}

We are interested in checking the validity of this formula (is it true in all interpretations). We will check the satisfiability of the negation of this formula (does it have a model):

\begin{equation*} \begin{array}{l@{}l} \lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\ & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\ & (\forall x.\ P(x) \lor P(f(x,a)))\ \big)\\ & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg) \end{array} \end{equation*}

We will first consider a range of techniques that allow us to convert such formula to simpler normal forms.

Negation Normal Form

In negation normal form of formula the negation applies only to atomic formulas.

Every FOL formula can be transformed in NNF using the formulas used for the same purpose in PL extended by two new ones :

  • $\neg \neg F \Leftrightarrow F$
  • $\neg \bot \Leftrightarrow \top$
  • $\neg \top \Leftrightarrow \bot$
  • $\neg (F_1 \wedge F_2) \Leftrightarrow \neg F1 \vee \neg F2$
  • $\neg (F_1 \vee F_2) \Leftrightarrow \neg F1 \wedge \neg F2$
  • $F1 \rightarrow F2 \Leftrightarrow \neg F1 \vee F2$
  • $F1 \leftrightarrow F2 \Leftrightarrow (F1 \rightarrow F2) \wedge (F2 \rightarrow F1)$
  • $\neg \forall x.F[x] \Leftrightarrow \exists x. \neg F[x]$
  • $\neg \exists x.F[x] \Leftrightarrow \forall x. \neg F[x]$

NNF of Example

\begin{equation*} \begin{array}{l@{}l} & (\forall x. \exists y.\ R(x,y))\ \land \\ & (\exists x. \exists y.\ \neg R(x,y) \lor \forall z.\ R(x,f(y,z)))\ \land \\ & (\forall x.\ P(x) \lor P(f(x,a)))\ \land \\ & (\exists x. \forall y.\ \neg R(x,y) \vee \neg P(y)) \end{array} \end{equation*}

Prenex Normal Form

Prenex normal form has all quantifiers in front.

Prenex normal form (PNF) is a formula of the form

\begin{equation*} Q_1 x_1. Q_2 x_2. \ldots Q_n x_n. G \end{equation*}

where $Q_i \in \{\forall, \exists\}$ and $G$ has no quantifiers.

Any FOL formula can be transformed to PNF. First convert it to NNF, then if several quantified variables or free variables have the same name rename them to fresh names, and finaly use the following formulas :

  • $(\forall x.F) \lor G \Leftrightarrow \forall x.(F \lor G)$
  • $(\forall x.F) \land G \Leftrightarrow \forall x.(F \land G)$
  • $(\exists x.F) \lor G \Leftrightarrow \exists x.(F \lor G)$
  • $(\exists x.F) \land G \Leftrightarrow \exists x.(F \land G)$

PNF of Example

\begin{equation*} \begin{array}{l@{}l} & (\forall x_1. \exists y_1.\ R(x_1,y_1))\ \land \\ & (\exists x_2. \exists y_2.\ \forall z.\ \neg R(x_2,y_2) \lor R(x_2,f(y_2,z)))\ \land \\ & (\forall x_3.\ P(x_3) \lor P(f(x_3,a)))\ \land \\ & (\exists x_4. \forall y_4.\ \neg R(x_4,y_4) \vee \neg P(y_4)) \end{array} \end{equation*}

Skolem Normal Form

Let $P : D \times D \rightarrow \{{\it true},{\it false}\}$ be a predicate with two arguments.

Note that

\begin{equation*} \exists x. \forall y. P(y,x) \to \forall u. \exists v. P(u,v) \end{equation*}

but converse implication does not hold (take as $P$ relation $\le$ or $>$ on natural numbers).

In general, we have this theorem:

\begin{equation*} \forall u. \exists v. P(u,v) \leftrightarrow \exists g. \forall u. P(u,g(u)) \end{equation*}

where $g : D \to D$ is a function.

Proof:

($\leftarrow$): For each $u$ we take $f(u)$ as the witness $v$.

($\rightarrow$): We know there exists a witness $v$ for each $u$. We define $f$ to map $u$ to one such witness $v$. (To prove that this is possible requires axiom of choice from set theory.)

End Proof.

Note also that satisfiability of formula $F$ expresses existential quantification over function symbols and relation symbols.

Definition: Skolemization is the result of applying this transformation

\begin{equation*} \forall x_1,\ldots,x_n. \exists y. F \ \leadsto \forall x_1,\ldots,x_n. subst(\{y \mapsto g(x_1,\ldots,x_n)\})(F) \end{equation*}

to the entire PNF formula to eliminate all existential quantifiers. Above, $g$ is a fresh function symbol. Denote $snf(F)$ the result of applying skolemization to formula $F$.

Lemma: A set of formulas $S$ in prenex normal form is satisfiable iff the set $\{ snf(F) \mid F \in S\}$ is satisfiable.

SNF for Example

\begin{equation*} \begin{array}{l@{}l} & (\forall x. R(x,g(x)))\ \land \\ & (\forall x.\forall y. \forall z.\ \neg R(x,y) \lor R(x,f(y,z)))\ \land \\ & (\forall x.\ P(x) \lor P(f(x,a)))\ \land \\ & (\forall y.\ \neg R(c,y) \vee \neg P(y)) \end{array} \end{equation*}

Note: it is better to do PNF and SNF for each conjunct independently.

CNF and Sets of Clauses

Let $snf(F)$ be $\forall x_1,\ldots,x_n. F$. Convert $F$ to conjunctive normal form $C_1 \land \ldots \land C_m$. Then $snf(F)$ is equivalent to

\begin{equation*} (\forall x_1,\ldots,x_n. C_1) \land \ldots \land (\forall x_1,\ldots,x_n. C_m) \end{equation*}

where each $C_i$ is a disjunction of first-order literals. We call $C_i$ (first-order) clause. For a given formula $F$, denote the set of such clauses in conjunctive normal form of $snf(pnf(F))$ by $clauses(F)$.

We omit universal quantifiers because all variables are universally quantified. We use a convention to denote variables by $x,y,z,\ldots$ and constants by $a,b,c,\ldots$.

Theorem: The set $S$ is satisfiable iff the set

\begin{equation*} \bigcup_{F \in S} clauses(F) \end{equation*}

is satisfiable.

Clauses for Example

  • $C_1=R(x,g(x))$
  • $C_2=\neg R(x,y) \lor R(x,f(y,z)))$
  • $C_3=P(x) \lor P(f(x,a))$
  • $C_4=\neg R(c,y) \vee \neg P(y)$

Another Example: Irreflexive Dense Linear Orders

Let ${\cal L} = \{ less \}$ be binary relation (“strictly less”). We consider the following axioms for irreflexive partial order that is total and dense:

\begin{equation*}\begin{array}{rcl} IRef & \equiv & \forall x.\ \lnot less(x,x) \\ Tra & \equiv & \forall x.\ \forall y.\ \forall z.\ less(x,y) \land less(y,z) \rightarrow less(x,z) \\ Total & \equiv & \forall x. \forall y.\ x \neq y \rightarrow less(x,y) \lor less(y,x) \\ Dense & \equiv & \forall x. \forall y.\ less(x,y) \rightarrow \exists z.\ less(x,z) \land less(z,y) \end{array} \end{equation*}

Let us find clauses for these axioms :

\begin{equation*}\begin{array}{lcr} \lnot less(x_1,x_1) \\ \lnot less(x_2,y_2) \lor \lnot less(y_2,z_2) \lor less(x_2,z_2) \\ \lnot (x_3 \neq y_3) \lor less(x_3,y_3) \lor less(y_3,x_3) \\ \lnot less(x_4,y_4) \lor \ less(x_4,f(x_4,y_4))\\ \lnot less(x_4,y_4) \lor \ less(f(x_4, y_4),y_4) \end{array} \end{equation*}