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.

Abstract A wide family of many-valued logics—for instance, those based on the weak Kleene algebra—includes a non-classical truth-value that is ‘contaminating’ in the sense that whenever the value is assigned to a formula $\varphi $, any complex formula in which $\varphi $ appears is assigned that value as well. In such systems, the contaminating value enjoys a wide range of interpretations, suggesting scenarios in which more than one of these interpretations are called for. This calls for an evaluation of systems with multiple contaminating values. In this paper, we consider the countably infinite family of multiple-conclusion consequence relations in which classical logic is enriched with one or more contaminating values whose behaviour is determined by a linear ordering between them. We consider some motivations and applications for such systems and provide general characterizations for all consequence relations in this family. Finally, we provide sequent calculi for a pair of four-valued logics including two linearly ordered contaminating values before defining two-sided sequent calculi corresponding to each of the infinite family of many-valued logics studied in this paper.