SWI-Tinker for G4+: A SWI-Prolog F.O.L. Prover with nanoCop Cross-Validation

G4+ is an automated prover for minimal, intuitionistic and classical First Order Logic written in SWI-Prolog. G4+ is mainly based on rules for direct syntactic deduction which are the rules of sequent calculus G4 and their translation in natural deduction (in tree style and Fitch style).

(Let us recall that sequent calculus G4 was not classical: when it was defined by Dyckhoff [1] (who called it LJT to stress the terminating property which was lacking in sequent calculus LJ), it was not classical, but intuitionistic. By adding rules IP and CQ_c, this F.O.L. prover becomes classical, while remaining single-conclusion.)

1. G4+ provides \(\LaTeX\) proofs in these three formats, which you can share via URL addresses (like with Wolfgang Schwartz’s Tree Proof Generator). For example, the solution to exercise i given by Lepage [2, p. 146] finds another proof in minimal logic via this link.
2. Note that, if your formula is provable, G4+ tells you the logic level that is at least required to prove it, i.e. either minimal, intuitionistic or classical logic.

This prover was formerly called “G4-mic” (minimal-intuitionistic-classical). The name change to “G4+” reflects the addition of nanoCop 2.0 [3] cross-validation, symbolized by the “+” for this dual-prover verification, ensuring correctness and reliability . For technical reasons, URLs g4-mic.vidal-rosset.net and https://github.com/joseph-vidal-rosset/G4-mic remain unchanged.

Both provers work independently on each formula, allowing systematic cross-checking:

• G4+ uses G4 sequent calculus (based on Dyckhoff’s LJT [1])
• nanoCop uses connection tableau with prefix unification

The test suite validates 134 formulas including:

• 107 numbered tests (propositional and first-order logic)
• 27 Pelletier problems and additional challenging theorems

Users can verify agreement between both provers by searching for “Disagreement” in the browser console after running tests with run_all_test_files. command.

I thank Jens Otten for developing nanoCop and making it freely available, enabling the cross-validation feature of this prover.

• The code of the proof engine has been inspired by Jens Otten’s leanseq.
• On this basis, the driver and the printers have been written with the help of A.I., mainly Claude, without which I would not have succeeded in completing this work.
• Finally, the web page dedicated to G4+ is also a SWI-Tinker that you can use to test your Prolog programs online, with other SWI-Prolog provers in the Demos library, thanks to the generous work of Jan Wielemaker given to people for free. My warmest thanks to Jens, Jan and Claude, and my apologies to those I have forgotten.

The source code of G4+ is on Github under the GPL v3 license.

Rules for Sequent Calculus G4	Natural Deduction Rules in Tree Style	Natural Deduction Rules in Flag Style
\begin{prooftree}\AxiomC{}\RightLabel{\scriptsize{$Ax.$}}\UnaryInfC{$A, \Gamma \vdash A$} \end{prooftree}	\begin{prooftree}\AxiomC{$A$}\RightLabel{\scriptsize{$R$}}\UnaryInfC{$A$} \end{prooftree}
\begin{prooftree}\AxiomC{$A, B, \Gamma \vdash C$} \RightLabel{\(\scriptsize{L0\to}\)} \UnaryInfC{$A \to B, A, \Gamma \vdash C$}\end{prooftree}	\begin{prooftree}\AxiomC{$A \to B$} \AxiomC{$A$} \RightLabel{\scriptsize{$\to E$}}\BinaryInfC{$B$}\end{prooftree}
\begin{prooftree}\AxiomC{$A \to (B \to C), \Gamma \vdash D$}\RightLabel{\(\scriptsize{L\land\to}\)}\UnaryInfC{$(A \land B) \to C,\Gamma \vdash D$}\end{prooftree}	\begin{prooftree}\AxiomC{$(A \land B) \to C$}\RightLabel{\scriptsize{$\land\to E$}}\UnaryInfC{$A \to (B \to C)$}\end{prooftree}
\begin{prooftree}\AxiomC{$A \to C, B \to C, \Gamma \vdash D$}\RightLabel{\(\scriptsize{L\lor\to}\)}\UnaryInfC{$(A \lor B) \to C, \Gamma \vdash D$}\end{prooftree}	\begin{prooftree}\AxiomC{$(A \lor B) \to C$}\RightLabel{\scriptsize{$\lor\to E$}}\UnaryInfC{$(A \to C)$}\end{prooftree} \begin{prooftree}\AxiomC{$(A \lor B) \to C$}\RightLabel{\scriptsize{$\lor\to E$}}\UnaryInfC{$(B\to C)$}\end{prooftree}
\begin{prooftree}\AxiomC{$A, B \to C,\Gamma \vdash B$}\AxiomC{$C,\Gamma \vdash D$}\RightLabel{\(\scriptsize{L\to\to}\)}\BinaryInfC{$(A \to B) \to C, \Gamma \vdash D$}\end{prooftree}	\begin{prooftree}\AxiomC{$(A \to B) \to C$}\RightLabel{\scriptsize{$\to\to E$}}\UnaryInfC{$B \to C$}\end{prooftree}
\begin{prooftree}\AxiomC{$(A \to B) \to B, \Gamma \vdash B$}\RightLabel{\scriptsize{\(DNE_{m}\)}}\UnaryInfC{$A , \Gamma \vdash B$}\end{prooftree}	\begin{prooftree}\AxiomC{\scriptsize{$i$}}\noLine \UnaryInfC{$(A \to B) \to B$}\noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{$B$}\RightLabel{\scriptsize{\(DNE_{m}\)}~\(i\)}\UnaryInfC{$A \to B$}\end{prooftree}
\begin{prooftree}\AxiomC{$A, B, \Gamma \vdash C$}\RightLabel{\scriptsize{$L\land$}} \UnaryInfC{$A \land B, \Gamma \vdash C$}\end{prooftree}	\begin{prooftree}\AxiomC{$A \land B$}\RightLabel{\scriptsize{$\land E$}} \UnaryInfC{$A$} \end{prooftree} \begin{prooftree}\AxiomC{$A \land B$}\RightLabel{\scriptsize{$\land E$}} \UnaryInfC{$B$}\end{prooftree}
\begin{prooftree}\AxiomC{$A, \Gamma \vdash C$}\AxiomC{$B, \Gamma \vdash C$}\RightLabel{\scriptsize{$L\lor$}}\BinaryInfC{$A \lor B, \Gamma \vdash C$}\end{prooftree}	\begin{prooftree}\AxiomC{$A \lor B$}\AxiomC{\scriptsize{1}}\noLine\UnaryInfC{$A$}\noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{$C$}\AxiomC{\scriptsize{2}}\noLine\UnaryInfC{$B$}\noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{$C$}\RightLabel{\scriptsize{$\lor E$ 1,2}}\TrinaryInfC{$C$}\end{prooftree}
\begin{prooftree}\AxiomC{$A, \Gamma \vdash B$}\RightLabel{\scriptsize{$R\to$}}\UnaryInfC{$\Gamma \vdash A \to B$}\end{prooftree}	\begin{prooftree}\AxiomC{\scriptsize{1}}\noLine\UnaryInfC{$A$} \noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{$B$}\RightLabel{\scriptsize{$\to I$ 1}}\UnaryInfC{$A \to B$}\end{prooftree}
\begin{prooftree}\AxiomC{$\Gamma \vdash A$}\AxiomC{$\Gamma \vdash B$}\RightLabel{\scriptsize{$R\land$}}\BinaryInfC{$\Gamma \vdash A \land B$}\end{prooftree}	\begin{prooftree}\AxiomC{$A$}\AxiomC{$B$}\RightLabel{\scriptsize{$\land I$}}\BinaryInfC{$A \land B$}\end{prooftree}
\begin{prooftree}\AxiomC{$\Gamma \vdash A$}\RightLabel{\scriptsize{$R\lor$}}\UnaryInfC{$\Gamma \vdash A \lor B$}\end{prooftree}\begin{prooftree} \AxiomC{$\Gamma \vdash B$}\RightLabel{\scriptsize{$R\lor$}}\UnaryInfC{$\Gamma \vdash A \lor B$}\end{prooftree}	\begin{prooftree}\AxiomC{$A$}\RightLabel{\scriptsize{$\lor I$}}\UnaryInfC{$A \lor B$}\end{prooftree} \begin{prooftree}\AxiomC{$B$}\RightLabel{\scriptsize{$\lor I$}}\UnaryInfC{$A \lor B$}\end{prooftree}
\begin{prooftree}\AxiomC{}\RightLabel{\scriptsize{$L\bot$}}\UnaryInfC{$\bot, \Gamma \vdash C$}\end{prooftree}	\begin{prooftree}\AxiomC{$\bot$}\RightLabel{\scriptsize{$\bot E$}}\UnaryInfC{$C$}\end{prooftree}
\begin{prooftree}\AxiomC{$\lnot A, \Gamma \vdash \bot$}\RightLabel{\scriptsize{$IP$}}\UnaryInfC{$\Gamma \vdash A$}\end{prooftree}	\begin{prooftree}\AxiomC{\scriptsize{1}}\noLine\UnaryInfC{$\lnot A$}\noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{$\bot$}\RightLabel{\scriptsize{$IP$ 1}}\UnaryInfC{$A$}\end{prooftree}
\begin{prooftree} \AxiomC{$ Ftt, \forall x Fxx ,\Gamma \vdash C $}\RightLabel{\scriptsize{$ L\forall $}}\UnaryInfC{$ \forall x Fxx, \Gamma \vdash C$}\end{prooftree}	\begin{prooftree}\AxiomC{$\forall x Fxx$}\RightLabel{\scriptsize{$\forall E$}}\UnaryInfC{$Ftt$}\end{prooftree}
\begin{prooftree}\AxiomC{$ \Gamma \vdash Ftt $}\RightLabel{\scriptsize{$ R\exists $}}\UnaryInfC{$\Gamma \vdash \exists y Fyt$}\end{prooftree}	\begin{prooftree}\AxiomC{$ Ftt $}\RightLabel{\scriptsize{$\exists I$}}\UnaryInfC{$\exists y Fyt$}\end{prooftree}
\begin{prooftree}\AxiomC{$ \Gamma \vdash Fa $}\RightLabel{\scriptsize{$ R \forall $}}\UnaryInfC{$ \Gamma \vdash \forall x Fx $}\noLine\UnaryInfC{\(a\) = \textit{eigenvariable}} \end{prooftree}	\begin{prooftree}\AxiomC{$Fa$} \RightLabel{\scriptsize{$ \forall I $}}\UnaryInfC{$ \forall x Fx $}\noLine\UnaryInfC{\(a\) = \textit{eigenvariable}}\end{prooftree}
\begin{prooftree}\AxiomC{$ Fa, \Gamma \vdash C$}\RightLabel{\scriptsize{$ L \exists $}}\UnaryInfC{$ \exists x Ax, \Gamma \vdash C $} \noLine\UnaryInfC{\(a\) = \textit{eigenvariable}}\end{prooftree}	\begin{prooftree}\AxiomC{$ \exists x Fx $}\AxiomC{\scriptsize{$ i $}} \noLine \UnaryInfC{$ Fa $} \noLine \UnaryInfC{$ \vdots $} \noLine \UnaryInfC{$ G $} \RightLabel{\scriptsize{$ \exists E ~ i $}} \BinaryInfC{$ G $} \noLine\UnaryInfC{\(a\) = \textit{eigenvariable}}\end{prooftree}
\begin{prooftree}\AxiomC{$ \exists x (Fx \to P), \Gamma \vdash D $}\RightLabel{\scriptsize{\(CQ_{c}\)}}\UnaryInfC{$\forall x Fx \to P, \Gamma \vdash D $}\end{prooftree}	\begin{prooftree}\AxiomC{$ \forall x Fx \to P $} \RightLabel{\scriptsize{\(CQ_{c}\)}}\UnaryInfC{$ \exists x(Fx \to P) $}\end{prooftree}
\begin{prooftree}\AxiomC{$ \forall x (Fx \to P), \Gamma \vdash D $}\RightLabel{\scriptsize{\(CQ_{m}\)}}\UnaryInfC{$\exists x Fx \to P, \Gamma \vdash D $} \end{prooftree}	\begin{prooftree}\AxiomC{$ \exists x Fx \to P $} \RightLabel{\scriptsize{\(CQ_{m}\)}}\UnaryInfC{$ \forall x(Fx \to P) $}\end{prooftree}