Proof theory for sequent-style tableaux: G0- and G3-style sequent calculi and full normalization

Abstract

Sequent-style tableaux are a one-sided refutation calculus for classical propositional logic, in which each node of the refutation tree carries a finite block of formulae and the structural rules are absorbed into the data structure and the closure criterion. Building on the correspondence between this block calculus and the cut-free sequent calculus, and following the programme of Kamide and Negri, we recast the calculus as a structural-rule-free G3-style sequent calculus $\mathbf{G}_t$ with shared contexts, and we introduce a G0-style sequent calculus $\mathbf{G}_0$ with independent contexts, explicit weakening and contraction, generalized initial sequents, and a primitive explosion rule. A theorem establishing the equivalence between $\mathbf{G}_0$ and $\mathbf{G}_t$ is proved, and the cut-elimination theorem for $\mathbf{G}_0$ is obtained as a consequence. We then introduce a natural deduction system $\mathbf{N}_g$ with general elimination rules matching the left rules of $\mathbf{G}_0$, and we prove a full normalization theorem for $\mathbf{N}_g$. The proof is achieved by means of bidirectional translations between $\mathbf{G}_0$ and $\mathbf{N}_g$: normal derivations correspond to cut-free derivations, and full normal form to the discipline in which every major premiss of an elimination rule is an assumption. We also determine the reach of the formula-succedent fragment, which is shown to have no theorems, so that the equivalence of the three systems is one of consequence and not of theoremhood, and we show that classical logic is recovered on the succedent side, and recovered exactly, by adjoining the rule of indirect proof.