# Boole-Quine Prover for Classical Propositional Logic

2021-01-28, updated 2024-03-01 next - previous

A Boole-Quine prover in Prolog, online thanks to Carlo Capelli

Quine’s algorithm for classical propositional logic
[1] consists in reducing any propositional
formula *F* either to at least one propositional variable or to one of
the constants that are the truth constant and falsity constant: if
this reduction ends on a propositional variable, then *F* is neither a
tautology nor an antilogy. *F* is a tautology if and only if all
reductions end on the truth constant. *F* is an antilogy (i.e. a
contradiction) if and only if all reductions end on the falsity
constant. Here are the reduction rules of Quine’s algorithm:

\(\Large{\frac{A \land \top}{A}}\) | \(\Large{\frac{A \land \bot}{\bot}}\) | \(\Large{\frac{A \lor \top}{\top}}\) | \(\Large{\frac{A \lor \bot}{A}}\) | \(\Large{\frac{A \to \top}{\top}}\) | \(\Large{\frac{A \to \bot}{\lnot A}}\) | \(\Large{\frac{\top \to A}{A}}\) | \(\Large{\frac{\bot \to A}{\top}}\) | \(\Large{\frac{A \leftrightarrow \top}{A}}\) | \(\Large{\frac{A \leftrightarrow \bot}{\lnot A}}\) |

One of the most interesting point of this algorithm is what Quine
called the *fell swoop*^{1} that consists in trying to provide a
counter-model of *F* in one and only one reduction path: choose the
most common variable in *F*, replace it by \(\bot\), apply the
reduction rules step by step and stop this test as soon as you end
on a literal (i.e. an atom or the negation an atom). It is therefore
proved that *F* is neither a tautology nor an antilogy.

Note that *fell swoops* are always insufficient to prove that *F* is a
tautology (or an antilogy): a *full sweep*^{2} is needed to prove
that formula is a tautology. Here is an example of *full sweep* that
proves that the following formula is a tautology:

\(((A \lor B) \to \top) \leftrightarrow ((A \to \top) \land (B \to \top))\) | \(((A \lor B) \to \bot) \leftrightarrow ((A \to \bot) \land (B \to \bot))\) |

\(\top \leftrightarrow (\top \land \top)\) | \(\lnot (A \lor B) \leftrightarrow (\lnot A \land \lnot B)\) |

\(\top \leftrightarrow \top\) | |

\(\top\) |

On the right, \(\lnot (A \lor B) \leftrightarrow (\lnot A \land \lnot B)\) contains neither \(\top\) nor \(\bot\), therefore this sub-formula requires a second division:

\(\lnot (A \lor \top) \leftrightarrow (\lnot A \land \bot) \) | \(\lnot (A \lor \bot) \leftrightarrow (\lnot A \land \top)\) |

\(\lnot \top \leftrightarrow \bot\) | \(\lnot A \leftrightarrow \lnot A \) |

\(\bot \leftrightarrow \bot\) | \(\top\) |

\(\top\) |

Here is a *fell swoop* that proves that, by contrast,

is *neither* a tautology nor an antilogy:

\(((A \lor B) \to \bot) \leftrightarrow ((A \to \bot) \lor (B \to \bot))\) |

\(\lnot (A \lor B) \leftrightarrow (\lnot A \lor \lnot B)\) |

\(\lnot (A \lor \top) \leftrightarrow (\lnot A \lor \bot)\) |

\(\lnot \top \leftrightarrow \lnot A\) |

\(\bot \leftrightarrow \lnot A\) |

\(\lnot \lnot A\) |

\(A\) |

## Footnotes:

^{1}

In French, Clavelin translated this expression by “l’attaque sélective”, but it could be also translated by “le coup de balai”, “in one fell swoop” meaning “d’un seul coup”.

^{2}

Clavelin translated “full sweep” by “attaque complète”. The English pun “the full sweep as opposed to the fell swoop” is untranslatable in French. “Full sweep” meaning “balayage complet”, it could have been translated by “grand ménage”, in French, “le grand ménage” is clearly more than “un coup de balai”.