Contraction-free sequent calculi for intuitionistic logic

Gentzen's sequent calculus LJ, and its variants such as G3 21, are (as is well known) convenient as a basis for automating proof search for IPC (intuitionistic propositional calculus). But a problem arises: that of detecting loops, arising from the use (in reverse) of the rule ⊃⇒ for implication introduction on the left. We describe below an equivalent calculus, yet another variant on these systems, where the problem no longer arises: this gives a simple but effective decision procedure for IPC. The underlying method can be traced back forty years to Vorob′ev 33, 34. It has been rediscovered recently by several authors (the present author in August 1990, Hudelmaier 18, 19, Paulson 27, and Lincoln et al. 23). Since the main idea is not plainly apparent in Vorob′ev's work, and there are mathematical applications 28, it is desirable to have a simple proof. We present such a proof, exploiting the Dershowtiz-Manna theorem 4 on multiset orderings. Consider the task of constructing proofs in Gentzen's sequent calculus LJ of intuitionistic sequents Γ⇒ G , where Γ is a set of assumption formulae and G is a formula (in the language of zero-order logic, using the nullary constant f absurdity, the unary constant ¬ negation, with ¬ A = def A ⊃ f and the binary constants &, ∨, and ⊃ conjunction, disjunction, and implication respectively). By the Hauptsatz 15, there is an apparently simple algorithm which breaks up the sequent, growing the proof tree until one reaches axioms (of the form Γ⇒ A where A is in Γ), or can make no further progress and must backtrack or even abandon the search. (Gentzen's argument in fact was to use the subformula property derived from the Hauptsatz to limit the size of the search tree. Došen 5 improves on this argument.)