Abstract

This article aims to dualize several results concerning various types (including possibly Cut-free and Identity-free systems) of canonical multiple-conclusion sequent calculi, i.e. Gentzen-style deduction systems for sequents, equipped with well-behaved forms of left and right introduction rules for logical expressions. In this opportunity, we focus on a different kind of calculi that we dub cocanonical, that is, Gentzen-style deduction systems for sequents, equipped with well-behaved forms of left and right elimination rules for logical expressions. These systems, simply put, have rules that proceed from sequents featuring complex formulas to sequents featuring their component subformulas. Our main goals are to prove soundness and completeness results for the target systems’ consequence relations in terms of their characteristic 3- or 4-valued non-deterministic matrices.