Every first order logic formula can be written in disjunctive normal form

Question

How can i prove that: Every first-order logic formula can be written in disjunctive normal form? It is easy if the formula does't contain any quantifiers. i think i have to use induction on formulas but again i'm stuck in the non-quantifier-free formulas...

Answer 1

First, let's get clear on what we mean by a first-order logic formula that is in disjunctive normal form (DNF). This means that the formula is of the form

$$Q_1 x_1 Q_2 x_2 .... Q_n x_n \ \varphi(x_1, x_2, ..., x_n)$$

where each $Q_i$ is either $\forall$ or $\exists$, and where $\varphi(x_1, x_2, ..., x_n)$ is a quantifier-free truth-functional formula in DNF (I assume it is well-known what it means for a truth-functional formula to be in DNF).

In this form, all the quantifiers are said to be 'in front of' the statement, though note that an individual quantifier may appear after other quantifiers. So this is what I mean when below I talk about 'pulling quantifiers out in front of the statement'.

Now, you can take any first-order logic formula, and go through four steps to get it into disjunctive normal form:

1. Rewrite all truth-functional operators other than $\land$, $\lor$, and $\neg$ in terms of $\land$, $\lor$, and $\neg$

2. Change variables in such a way that each different quantifier quantifies a different variable. For example, change

$$\forall x P(x) \lor \exists x Q(x)$$

to

$$\forall x P(x) \lor \exists y Q(y)$$

3. Use the Quantifier Negation Laws and Prenex Laws to pull any quantifiers to the front:

Quantifier Negation Laws

Where $\varphi$ is any formula:

$\neg \exists x \ \varphi \Leftrightarrow \forall x \ \neg \varphi$

$\neg \forall x \ \varphi \Leftrightarrow \exists x \ \neg \varphi$

Prenex Laws

Where $\varphi$ is any formula and where $x$ is not a free variable in $\psi$:

$ \forall x \ \varphi \land \psi \Leftrightarrow \forall x (\varphi \land \psi)$

$ \psi \land \forall x \ \varphi \Leftrightarrow \forall x (\psi \land \varphi)$

$ \exists x \ \varphi \land \psi \Leftrightarrow \exists x (\varphi \land \psi)$

$ \psi \land \exists x \ \varphi \Leftrightarrow \exists x (\psi \land \varphi)$

$ \forall x \ \varphi \lor \psi \Leftrightarrow \forall x (\varphi \lor \psi)$

$ \psi \lor \forall x \ \varphi \Leftrightarrow \forall x (\psi \lor \varphi)$

$ \exists x \ \varphi \lor \psi \Leftrightarrow \exists x (\varphi \lor \psi)$

$ \psi \lor \exists x \ \varphi \Leftrightarrow \exists x (\psi \lor \varphi)$

Notice that because of step 1 the only truth-functional operators left are $\land$, $\lor$, and $\neg$, so there are only three possibilities if a quantifier is not yet in front of the statement:

A. It is being negated ... ok, so apply Quantifier Negation

B. It is a conjunct of a conjunction... ok, so pull it outside the conjunction using Prenex Laws .. which we are guaranteed to be able to apply since we renamed variables, so the variable quantified by the quantifier cannot occur in the other conjunct(s)

C. It is a disjunct of a disjunction: similar to B

This means that if we keep applying these rules, all quantifiers are guaranteed to end up in front of the statement.

4. Now that all quantifiers are in front, the body is a truth-functional formula, which we know can be put into DNF