Non-deterministic semantics for cocanonical and semi-cocanonical deduction systems

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 paper, we focus on a different kind of calculi that we dub cocanonical, i.e. 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 three- or four-valued non-deterministic matrices.