# Boolean normal form (first-order logic)

### From Learning Logic for Computer Science

Every first-order formula is equivalent to a formula where the only connectives are 'or', 'and', and 'not'.

A first-order formula is in **boolean normal form (BNF)** if it is built from atomic formulas using the unary connective $\neg$, the binary connectives $\wedge$ and $\vee$, and existential and universal quantifiers.

**Example**
The formula $\exists x_0 (R(x_0) \rightarrow Q(x_0, x_1))$ is not in BNF, but $\exists x_0 (\neg R(x_0) \vee Q(x_0, x_1))$ is and is equivalent to the first formula.

**Theorem**
Every first-order formula can be converted into an equivalent first-order formula in BNF.

An inductive proof, which rewrites every other connective in a straightforward fashion using the rewrite rules for them, can be carried out easily.