# Boole-Quine Prover for Classical Propositional Logic

2020-11-08, updated 2020-11-08 next - previous

Jan Burse’s Prolog program, published online thanks to Carlo Capelli.

Prolog program: Jan Burse (Have a look on the reference given by Jan Burse on this web page, it explains why this prover must be called “Boole-Quine”, and not only Quine’s prover.)

PHP file: Carlo Capelli.

You can enjoy this program here.

Quine’s algorithm for classical propositional logic
[quine1966a][quine1984]
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”.