pp 1–19 | Cite as

Quasi-canonical systems and their semantics

  • Arnon AvronEmail author
S.I.: Varieties of Entailment


A canonical (propositional) 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 \(\lnot \) of the language (usually, but not necessarily, interpreted as negation). Accordingly, each application of a logical rule in such systems introduces either a formula of the form \(\diamond (\psi _1,\ldots ,\psi _n)\), or of the form \(\lnot \diamond (\psi _1,\ldots ,\psi _n)\), and all the active formulas of its premises belong to the set \(\{\psi _1,\ldots ,\psi _n,\lnot \psi _1,\ldots ,\lnot \psi _n\}\). 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 (Nmatrix) which is based on some subset of the set of the four truth-values which are used in the famous Dunn–Belnap four-valued (deterministic) matrix for information processing. In addition, we determine when a quasi-canonical system admits (strong) cut-elimination.


Gentzen-type systems Quasi-canonical systems Non-deterministic matrices Coherence Negation 



This research was supported by The Israel Science Foundation (Grant No. 817-15).


  1. Anderson, A. R., & Belnap, N. D. (1975). Entailment: The logic of relevance and necessity (Vol. I). Princeton: Princeton University Press.Google Scholar
  2. Avron, A. (2014). Paraconsistency, paracompleteness, Gentzen systems, and trivalent semantics. Journal of Applied Non-Classical Logics, 24(1–2), 12–34.CrossRefGoogle Scholar
  3. Avron, A., Arieli, O. & Zamansky, A. (2018). Theory of Effective Propositional Paraconsitent Logics, volume 75 of Studies in logic mathematical logic and foundations. College PublicationsGoogle Scholar
  4. Avron, A., & Konikowska, B. (2005). Multi-valued calculi for logics based on non-determinism. Journal of the Interest Group in Pure and Applied Logic, 10, 365–387.Google Scholar
  5. Avron, A., Konikowska, B., & Zamansky, A. (2013). Cut-free sequent calculi for C-systems with generalized finite-valued semantics. Journal of Logic and Computation, 23(3), 517–540.CrossRefGoogle Scholar
  6. Avron, A., & Lev, I. (2001). Canonical propositional gentzen-type systems. In: Proceedings of the 1st international joint conference on automated reasoning (IJCAR 2001), LNAI 2083. SpringerGoogle Scholar
  7. Avron, A., & Lev, I. (2005). Non-deterministic multi-valued structures. Journal of Logic and Computation, 15, 241–261.CrossRefGoogle Scholar
  8. Avron, A., & Zamansky, A. (2011). Non-deterministic semantics for logical systems—A survey. In D. Gabbay & F. Guenther (Eds.), Handbook of philosophical logic (Vol. 16, pp. 227–304). Berlin: Springer.CrossRefGoogle Scholar
  9. Belnap, N. D. (1977). A useful four-valued logic. In J. M. Dunn & G. Epstein (Eds.), Modern uses of multiple-valued logics (pp. 7–37). Dordrecht: Reidel Publishing Company.Google Scholar
  10. Ciabattoni, A., Lahav, O., Spendier, L., & Zamansky, A. (2013). Automated support for the investigation of paraconsistent and other logics. In S. Artemov & A. Nerode (Eds.), Logical Foundations of Computer Science, number 7734 in Lecture Notes in Computer Science (pp. 119–133). Berlin: Springer.Google Scholar
  11. Dunn, J. M. (1976). Intuitive semantics for first-degree entailments and ‘coupled trees’. Philosophical Studies, 29, 149–168.CrossRefGoogle Scholar

Copyright information

© Springer Nature B.V. 2018

Authors and Affiliations

  1. 1.School of Computer ScienceTel Aviv UniversityTel AvivIsrael

Personalised recommendations