Abstract

A canonical Gentzen-type system is a system in which every rule has the subformula property, it introduces exactly one occurrence of a connective, and it imposes no restrictions on the contexts of its applications. A larger class of Gentzen-type systems which is also extensively in use is that of quasi-canonical systems. In such systems a special role is given to a unary connective \ of the language. Accordingly, each application of a logical rule in such systems introduces either a formula of the form \\), or of the form \\), and all the active formulas of its premises belong to the set \. In this paper we investigate the whole class of quasi-canonical systems. We provide a constructive coherence criterion for such systems, and show that a quasi-canonical system is coherent iff it is analytic iff it has a characteristic non-deterministic matrix which is based on some subset of the set of the four truth-values which are used in the famous Dunn–Belnap four-valued matrix for information processing. In addition, we determine when a quasi-canonical system admits cut-elimination.