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 swoop1 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 sweep2 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:
\begin{equation} \label{eq:6} ((A \lor B) \to C) \leftrightarrow ((A \to C) \land (B \to C)) \end{equation}| \(((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,
\begin{equation} \label{eq:7} ((A \lor B) \to C) \leftrightarrow ((A \to C) \lor (B \to C)) \end{equation}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:
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”.
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”.
