Canonical Propositional Gentzen-Type Systems

Canonical propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the subformula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a "canonical system" to first-order languages and beyond. We extend the propositional coherence criterion for the non-triviality of such systems to rules with unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Arnon Avron, Iddo Lev
• Keywords: 2-valued Non-deterministic Matrices, Automated Reasoning, CADE 2001, Propositional Coherence Criterion, Pure Logical Rules