Canonical propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules which have the subformula property, introduce exactly one occurrence of a connective in their conclusion, and no other occurrence of any connective is mentioned anywhere else in their formulation. We provide a constructive coherence criterion for the non-triviality of such systems, and show that a system of this kind admits cut elimination iff it is coherent. We show also that the semantics of such systems is provided by non-deterministic two-valued matrices (2-Nmatrices). 2-Nmatrices form a natural generalization of the classical two-valued matrix, and every coherent canonical system is sound and complete for one of them. Conversely, with any 2-Nmatrix it is possible to associate a coherent canonical Gentzen-type system which has for each connective at most one introduction rule for each side, and is sound and complete for that 2-Nmatrix. We show also that every coherent canonical Gentzen-type system either defines a fragment of the classical two-valued logic, or a logic which has no finite characteristic matrix. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Avron, A., & Lev, I. (2001). Canonical propositional Gentzen-type systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2083 LNAI, pp. 529–544). Springer Verlag. https://doi.org/10.1007/3-540-45744-5_45
Mendeley helps you to discover research relevant for your work.