Boolean normal form

A propositional formula is in boolean normal form if the connectives occurring in it are among $\neg$, $\vee$, and $\wedge$. Every propositional formula is equivalent to a formula in boolean normal form.

Formal definition

The set of propositional formulas in boolean normal form (BNF) is defined inductively as follows.

Base set.

• $\top$ and $\bot$ are in BNF.
• For every $i$, the formula $X_i$ is in BNF.

Inductive rules.

• If $\varphi$ is in BNF, then $\neg \varphi$ is in BNF.
• If $\varphi$ and $\psi$ are in BNF, then $\varphi \vee \psi$ and $\varphi \wedge \psi$ are in BNF.

In other words, the set of connectives is restricted to the ones which are typically used for calculating with truth values. More formally, the language of boolean algebra is used.

Example The formula $\neg (X_0 \vee X_1)$ is in boolean normal form, but neither $\neg \bigvee(X_0, X_1, X_2)$ nor $X_0 \rightarrow X_1$ are in BNF.

Conversion into boolean normal form

The following simple algorithm turns an arbitrary propositional formula into a formula in boolean normal form.

  PL2BNF($\phi$)
  Precondition: $\varphi$ is a propositional formula
  case $\varphi$ of
    $\top$: return $\top$
    $\bot$: return $\bot$
    $X_i$: return $X_i$
  else
    write $\varphi$ as $C(\varphi_0, \dots, \varphi_{n-1})$
    case $C$ of
      $\bigwedge$:
        if $n = 0$ then return $\top$
        if $n = 1$ then return PL2BNF($\varphi_0$)
        if $n \geq 2$
          let $\psi$ = PL2BNF($\varphi_0$) $\wedge$ PL2BNF($\varphi_1$)
          for $i = 2$ to $n-1$
            let $\psi$ = $\psi$ $\wedge$ PL2BNF($\varphi_i$)
          return $\psi$
      $\bigvee$:
        ...
      ...
      $\rightarrow$: return $\neg$ PL2BNF($\varphi_0$) $\vee$ PL2BNF($\varphi_1$)
      ...
      $\vee$: return PL2BNF($\varphi_0$) $\vee$ PL2BNF($\varphi_1$)
      $\wedge$: return PL2BNF($\varphi_0$) $\wedge$ PL2BNF($\varphi_1$)
      $\neg$: return $\neg$ PL2BFN($\varphi_0$)
  Postcondition: return is equivalent to $\varphi$ and in BNF

The idea is that for every connective which is *not* among the ones which are allowed one of the rewrite rules is applied.

Theorem Every propositional formula is equivalent to a formula in boolean normal form.

The proof is given by the above algorithm: this algorithm terminates for each input and it is correct, because of the congruence lemma and because in each step one of the laws of propositional logic is used.