# LJT (G4ip) proof search

Originally invented by Roy Dyckhoff in [Contraction-free sequent calculi for intuitionistic logic](https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/contractionfree-sequent-calculi-for-intuitionistic-logic/C7ABBFC63E74878E52FF4E624029503B). G4ip is the sequent calculus derived from G3ip.

Also see an implementation by [Michel Levy](https://lig-membres.imag.fr/michel.levy/): http://teachinglogic.liglab.fr/
I traced down the code from the file `preuve.ml` ("proof" in French) in the DN1 variant.

---

Let context $\Gamma = \Gamma_0 \cup \Gamma_1 \cup \Gamma_2 \cup \Gamma_3$, where

* $\Gamma_1$ is a set of atoms,
* $\Gamma_2$ is a set of clauses of the form $b \to c$ where $b$ is an atom,
* $\Gamma_3$ is a set of clauses of the form $(b \to d) \to c$,
* $\Gamma_0$ is a set of formula of no restrictions.

Given a w.f.f. $a$, decide whether $\Gamma \vdash_{\mathrm{NJ}} a$. Usually initially $\Gamma = \emptyset$.
Also give a witness if it is derivable.

## Algorithm

* If $a \in \Gamma$: **Conclude** "derivable" ($\mathrm{assum}$).
* If one of below conditions holds:
1. $\bot \in \Gamma_0$ ($L_\bot$), or
2. there is some $x \in \Gamma$ such that $x \to a \in \Gamma$, or
3. $\Gamma_0$ contains either $\_ \land a$ or $a \land \_$ ($L_{\land}; \mathrm{assum}$),
<!---->
**Conclude** "derivable".
> Remark: modus ponens always holds by structural induction on $x$.
* Else, Try to pattern match $(\Gamma_0, a)$:
* If $a$ is of the form $x \to y$, **apply** $R_\to$.
* If $a$ is of the form $x \land y$, **apply** $R_\land$.
> Remark: after this stage, $a$ can only be $\bot$, an atom, or a disjunction.
* If $\Gamma_0$ is non-empty, pick an element and pattern match:
* an atom: **Move** it to $\Gamma_1$ and recurse.
* a conjunction: **Apply** $L_\land$.
* a disjunction: **Apply** $L_\lor$.
* an implication $y = g \to b$:
Let $\Gamma_0' = (\Gamma_0 \setminus \{y\})$, prove $g \to b \vdash a$ as follows:
1. **Prove** $\Gamma_0' \cup \Gamma_{1..3} \vdash g$, and then
2. **Prove** ($\Gamma_0' \cup \{b\}) \cup \Gamma_{1..3} \vdash a$.
<!---->
> Why? It resembles MP, but I cannot find a term to describe this process.
<!---->
If either step is not derivable, pattern match $g$ and rewrite accordingly,
* an atom: **move** $y$ to $\Gamma_2$ and recurse.
* a conjunction: **apply** $L_{\land\to}$. ~Lemma\ p10~
* a disjunction: **apply** $L_{\lor\to}$. ~Lemma\ p11~
* an implication: **move** it to $\Gamma_3$ and recurse.
* $\bot$: **remove** $y$ and recurse. (why?)
* Else $\Gamma_0$ is empty. Try proceeding with the following steps in order.
* Collect $\{ p : p \in \Gamma_1, p \to b \in \Gamma_2 \}$. If it is non-empty, **apply** $L_{0\to}$ on an element. If a proof fails, repeat this step on the remaining of them.
* If $\Gamma_3$ is non-empty, pick an element in $\Gamma_3$ and **apply** $L_{\to\to}$. ~Lemma\ p13~
* If $a$ is a disjunction, **apply** $R_\lor$ on either side.
> Remark: By the [disjunction property](https://flolac.iis.sinica.edu.tw/2022/LOGIC_3.pdf#page=21), a disjunction is derivable if and only if either branch is derivable.
* None of the above applies ($a$ is $\bot$ or an atom).
**Conclude** "not derivable".
> Remark: it is already not the case that $a \in \Gamma$.

To **apply** a rule, to **prove** a statement, or to **move**/**remove** an element to a set means that to re-enter the procedure with the resulting context $\Gamma' = \cup_{i=0..3} \Gamma_i$ and formula.

The original algorithm describes everything as multisets for proving total correctness, but it seems that ordinary sets or lists suffices in practice.

## Appendix

There are 8 proof rules in LJ. They are $\mathrm{assum}$, $L_\bot$, $L_\land$, $R_\land$, $L_\lor$, $R_\lor$, $L_\to$, $R_\to$.

The 4 rules replacing the problematic $L_\to$ are as follows:

$$\frac
{\Gamma, P, B \vdash E}
{\Gamma, P, P \to B \vdash E}
\;\;\;(L_{0\to})\;\;\;\text{with $P$ atomic}$$

$$\frac
{\Gamma, D, B \vdash C \to D \hspace{3em}
\Gamma, B \vdash E}
{\Gamma, (C \to D) \to B \vdash E}
\;\;\;(L_{\to\to})$$

$$\frac
{\Gamma, C \to D \to B \vdash E}
{\Gamma, (C \land D) \to B \vdash E}
\;\;\;(L_{\land\to})$$

$$\frac
{\Gamma, C \to B, D \to B \vdash E}
{\Gamma, (C \lor D) \to B \vdash E}
\;\;\;(L_{\lor\to})$$

The witness can be collected from the path an input has undergone recursively.

Some lemmas are used to convert the sequent calculus back to natural deduction proofs. They are listed below, naming after variables found in the original code:

* p10: $(c \land d) \to b \vdash c \to (d \to b)$
* p11: $(c \lor d) \to b \vdash d \to b$ (only the second branch)
* p13: $(c \to d) \to b \vdash d \to b$ (only the second branch)

---

Questions:

1. Roy's paper did not give an explicit deciding procedure. Why this order of backtracking?
2. Will it always terminate?
3. When it rejects, how to prove that it has tried all paths?