Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers

Propositional canonical Gentzen-type systems, introduced in [1], are systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a connective is introduced and no other connective is mentioned. [1] provides a constructive coherence criterion for the non-triviality of such systems and shows that a system of this kind admits cut-elimination iff it is coherent. The semantics of such systems is provided by two-valued nondeterministic matrices (2Nmatrices). [3] extends these results to systems with unary quantifiers of a very restricted form. In this paper we substantially extend the characterization of canonical systems to (n, k)-ary quantifiers, which bind k distinct variables and connect n formulas. We show that the coherence criterion remains constructive for such systems, and that for the case of k {0, 1}: (i) a canonical system is coherent iff it has a strongly characteristic 2Nmatrix, and (ii) if a canonical system...

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Anna Zamansky, Arnon Avron
• Keywords: Automated Reasoning, CADE 2006, Coherence Criterion, Constructive Coherence Criterion, Two-valued Nondeterministic Matrices