SWI-Tinker for G4-mic F.O.L. Prover
G4-mic is an automated prover for classical, intuitionistic and minimal First Order Logic written in SWI-Prolog and based on G4 which is an intuitionistic system of sequent calculus, defined by Roy Dyckhoff [1] [2, p. 122]. Dyckhoff initially named it LJT, to emphasize the termination property that G4 adds to LJ. G4 is therefore a good choice for an automated prover, because it terminates the proof of any valid propositional formula while avoiding the risk of looping associated with blindly applying the usual rule \(L\to\). This latter is replaced in G4 by two rules for the conditional on the left, to which we must add rules \(L\land\to\) and \(L\lor\to\), in order to get the complete list of rules specific to G4:
| \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, 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), \Gamma \vdash D$}\RightLabel{\(\scriptsize{L\land\to}\)}\UnaryInfC{$(A \land B) \to C,\Gamma \vdash D$}\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} |
These four rules are sometimes sequents to prove in exercises of good logic textbooks (see for example [3]). All of them are derivable in minimal logic and, rule \(L\to\to\) apart, they are all invertible. The links below lead to the automated quick proofs of their invertibility:
- Quick proof that \(L0\to\) is invertible, where \(L0\to\) and \(L\land\to\) are used.
- Quick proof that \(L\land \to\) is invertible, where \(L0\to\) and \(L\land\to\) are used.
- Quick proof that \(L\lor\to\) is invertible, where where \(L0\to\) and \(L\lor\to\) are used.
With these proofs, the reader can see that G4-mic prover provides \(\LaTeX\) proofs in sequent calculus and in natural deduction, both in “flag style” and “tree style”. In G4-mic prover, there is only one proof engine for proofs, which is the sequent calculus prover for G4-mic, inspired by Jens Otten’s Prolog code for leanseq. It means that, in this code, proofs natural deduction are only translations of their respective proofs in sequent calculus G4, and, in this translation process, the tree style translates the flag style, not the other way around. To sum up, G4-mic prover has the same goal that GAPT,
In contrast to automated and interactive theorem provers whose focus is the construction of proofs, GAPT concentrates on the transformation and further processing of proofs.
and, by contrast with GAPT, aims at proving in F.O.L. at the weakest strength that is required to prove a formula F: there is no need to use intuitionistic logic nor a fortiori classical logic, if F is provable in minimal logic, and G4-mic informs the user about the logic that is used in the given proof.
In this translation work, the delicate part was the translation of \(L\to \to\). It is difficult to deny that Negri and von Plato were right to explain this rule [2, p. 122], because it is not intuitive. Their explanation was very helpful to translate \(L\to \to\) in natural deduction, where, surprisingly, this rule is far simpler than in sequent calculus, here it is:
\begin{prooftree} \AxiomC{$(A \to B) \to C$} \RightLabel{\scriptsize{$L\to\to$}} \UnaryInfC{$B \to C$} \end{prooftree}This translation is a provable sequent, crucial to the proof that \(L\to\to\) is derivable in minimal logic:
\begin{prooftree} \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$B, A \vdash B$} \RightLabel{$\scriptsize{L \to}$} \UnaryInfC{$B \vdash A \to B$} \AxiomC{} \RightLabel{$\scriptsize{Ax.}$} \UnaryInfC{$B, C \vdash C$} \RightLabel{$\scriptsize{R \to}$} \BinaryInfC{$B, (A \to B) \to C \vdash C$} \UnaryInfC{$(A \to B) \to C \vdash B \to C$} \AxiomC{$A, B \to C, \Gamma \vdash B$} \RightLabel{$\scriptsize{R \to}$} \UnaryInfC{$B \to C, \Gamma \vdash A \to B$} \RightLabel{$\scriptsize{Cut}$} \BinaryInfC{$(A \to B) \to C, \Gamma \vdash A \to B$} \AxiomC{$C,\Gamma \vdash D$} \RightLabel{$\scriptsize{L\to}$} \BinaryInfC{$(A \to B) \to C, \Gamma \vdash D$} \end{prooftree}It is interesting to note that, once correctly translate in natural deduction, \(L\to\to\) is not only rather simple, but useful to get automated proof that would be more complex without this rule. Take for example the proof of the double negation of the classical law of contrapositive i.e.
\begin{equation} \label{eq:1} \lnot \lnot ((\lnot B \to \lnot A) \to (A \to B)) \end{equation}As any double negation of theorem of classical logic, \eqref{eq:1} is provable in intuitionistic logic (Glivenko theorem). The proofs in natural deduction given by G4-mic prover are interesting to compare. First, in flag style
second, in tree style:
We see that rule \(L\to\to\) is applied only one time in the proof in tree style while it is applied three times in the proof in flag style, which translates faithfully the sequent proof. Therefore, the former in this prover is an optimization of the latter.