Sequent Calculus Prover with Antisequents for Classical Propositional Logic
2021-12-16, updated 2024-03-01 next - previous
A Tau Prolog prover, from Philip Zucker’s and Jens Otten’s works.
This Tau Prolog prover for classical propositional logic is an implementation of 12 rules which are the rules for the connectives in \(\mathbf{LK}\) [1, p. 187], and three additional rules: two rules (left and right) for the biconditional [2, p. 5], and an initial rule to prove falsifiability, which is the axiom of LK, a refutation system based on antisequents [3, p. 20].
Last, note, about the rules below, that the Weakening rules are built in the initial rule Ax., that there is no Contraction neither Cut, and that falsity constant \(\bot\) is not used in this system.
| Initial rule for provability | Initial rule for unprovability |
|---|---|
| \begin{prooftree} \AxiomC{}\RightLabel{\(\scriptsize{Ax.}\)}\UnaryInfC{$\Gamma, A \vdash A, \Delta$}\end{prooftree} | \begin{prooftree} \AxiomC{}\RightLabel{\(\scriptsize{Asq.}\)}\UnaryInfC{$\Gamma \nvdash \Delta$}\noLine\UnaryInfC{$\Gamma \cap \Delta = \emptyset$}\end{prooftree} |
| Left rules | Right rules |
|---|---|
| \begin{prooftree} \AxiomC{$\Gamma, A, B \vdash \Delta$}\RightLabel{\(\scriptsize{L\land}\)}\UnaryInfC{$\Gamma, A \land B \vdash \Delta$}\end{prooftree} | \begin{prooftree}\AxiomC{$\Gamma \vdash A, \Delta$} \AxiomC{$\Gamma \vdash B, \Delta$}\RightLabel{\(\scriptsize{R\land}\)}\BinaryInfC{$\Gamma \vdash A \land B, \Delta$} \end{prooftree} |
| \begin{prooftree}\AxiomC{$\Gamma, A \vdash \Delta$} \AxiomC{$\Gamma, B \vdash \Delta$}\RightLabel{\(\scriptsize{L\lor}\)}\BinaryInfC{$\Gamma, A \lor B \vdash \Delta$} \end{prooftree} | \begin{prooftree} \AxiomC{$\Gamma \vdash A, B, \Delta$}\RightLabel{\(\scriptsize{R\lor}\)}\UnaryInfC{$\Gamma \vdash A \lor B, \Delta$}\end{prooftree} |
| \begin{prooftree}\AxiomC{$\Gamma \vdash A, \Delta$} \AxiomC{$\Gamma, B \vdash \Delta$}\RightLabel{\(\scriptsize{L\to}\)}\BinaryInfC{$\Gamma, A \to B \vdash \Delta$} \end{prooftree} | \begin{prooftree} \AxiomC{$\Gamma, A \vdash B, \Delta$}\RightLabel{\(\scriptsize{R\to}\)}\UnaryInfC{$\Gamma \vdash A \to B, \Delta$}\end{prooftree} |
| \begin{prooftree} \AxiomC{$\Gamma \vdash A, \Delta$}\RightLabel{\(\scriptsize{L\lnot}\)}\UnaryInfC{$\Gamma, \lnot A \vdash \Delta$}\end{prooftree} | \begin{prooftree} \AxiomC{$\Gamma, A \vdash \Delta$}\RightLabel{\(\scriptsize{R\lnot}\)}\UnaryInfC{$\Gamma \vdash \lnot A, \Delta$}\end{prooftree} |
| \begin{prooftree}\AxiomC{$\Gamma, A, B \vdash \Delta$} \AxiomC{$\Gamma \vdash A, B, \Delta$}\RightLabel{\(\scriptsize{L\leftrightarrow}\)}\BinaryInfC{$\Gamma, A \leftrightarrow B \vdash \Delta$} \end{prooftree} | \begin{prooftree}\AxiomC{$\Gamma, A \vdash B, \Delta$} \AxiomC{$\Gamma, B \vdash A, \Delta$}\RightLabel{\(\scriptsize{R\leftrightarrow}\)}\BinaryInfC{$\Gamma \vdash A \leftrightarrow B, \Delta$} \end{prooftree} |
1. HOWTO
Select a query in section D- Examples of Queries, or write a Prolog query like:
provable((your_formula), Proof).
“your_formula” must a propositional formula respecting the syntax for the connectives given at the beginning of the Prolog file below.
- If your formula is provable in classical propositional logic, all paths of the proof provided by the prover end on a sequent which is a logical axiom (label Ax.).
- If your formula is unprovable in classical propositional logic, there is at least one path of the refutation provided by the prover which ends on one antisequent (label Asq, antisequents outputs are red), that is a sequent which is unprovable because no atomic formula occurs on both sides of the derivation symbol i.e. \(\vdash\). Note that each antisequent provides a countermodel. For example, formula 11 has two countermodels: \(\{A = true, B = false\}\) and \(\{A = false, B = true\}\). To the syntactical non-derivability expressed by \(A \nvdash B\) and \(B \nvdash A\) on which ends the refutation of \((A \lor B) \to (A \land B)\) provided by the prover, corresponds, by completeness, implications \(A \Rightarrow B\) and \(B \Rightarrow A\), whose the truth value is false when the truth values of the antecedent and the consequent are respectively true and false.
It is sometimes necessary to click twice on Prove button.
Enjoy !
A - Prolog Code:
D - Examples of Queries:
- Excluded Middle: a | ~ a
- Dilemma : ((~ a => b) & (a => b)) => b
- Double Negation: ~(~a) <=> a
- Peirce’s Law: ((a => b) => a) => a
- Dummett Formula : (a => b)| (b => a)
- Classical equivalence for negation : (~a => a) <=> a
- Classical De Morgan's Law : ~((a & b)) => (~ a | ~b)
- Pelletier Problem 17 : ( ( ( p & ( q => r ) ) => s ) <=> ( ( ~ p | q | s ) & ( ~ p | ~ r | s ) ) )
- a
- a => b
- (a | b) => (a & b)
- a & b | a & ~b | ~a & b | ~a & ~c