Non-deterministic matrices for combinations of canonical and cocanonical deduction systems

This article aims to study, proof-theoretically and semantically, Gentzen-style sequent calculi (including possibly Cut-free and Identity-free systems), containing combinations of canonical and cocanonical rules, i.e. Gentzen systems for sequents, with well-behaved forms of left and right introduction and elimination rules for logical expressions. Our main goals are to provide soundness and completeness results for the derivability relations of the target systems in terms of 2-, 3-, or 4-valued non-deterministic semantics, and to give sufficient conditions under which these calculi are prone to produce well-behaved normal derivations of a structurally-atomic analytic-synthetic kind.