2026/07/31 by Simone Cuconato
Mathematics · #math.LO #msc:03F05 #msc:03B05 #msc:03F03
arxiv created 2026/07/31 · arxiv updated 2026/08/03
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 G3T with shared contexts, and we introduce a G0-style sequent calculus G0T with independent contexts, explicit weakening and contraction, generalized initial sequents, and a primitive explosion rule. A theorem establishing the equivalence between G0T and G3T is proved, and the cut-elimination theorem for G0T is obtained as a consequence. We then introduce a natural deduction system NgT with general elimination rules for the same logic, and we prove a full normalization theorem for NgT. The proof is achieved by means of bidirectional translations between G0T and NgT: 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.