Originally invented by Roy Dyckhoff in Contraction-free sequent calculi for intuitionistic logic. G4ip is the sequent calculus derived from G3ip.
Also see an implementation by 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 , where
Given a w.f.f. , decide whether . Usually initially .
Also give a witness if it is derivable.
Remark: modus ponens always holds by structural induction on .
Remark: after this stage, can only be , an atom, or a disjunction.
If either step is not derivable, pattern match and rewrite accordingly,Why? It resembles MP, but I cannot find a term to describe this process.
Remark: By the disjunction property, a disjunction is derivable if and only if either branch is derivable.
Remark: it is already not the case that .
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 and formula.
The original algorithm describes everything as multisets for proving total correctness, but it seems that ordinary sets or lists suffices in practice.
There are 8 proof rules in LJ. They are , , , , , , , .
The 4 rules replacing the problematic are as follows:
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:
Questions: