Canonical calculi with (n,k)-ary quantifiers

Propositional canonical Gentzen-type systems, introduced in [2], 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. [2] 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 using two-valued non-deterministic matrices (2Nmatrices). [23] 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, and show that the coherence criterion remains constructive for such systems. Then we focus on the case of k {0, 1} and show that the following statements concerning a canonical calculus G are equivalent: (i) G is coher...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Arnon Avron, Anna Zamansky
• Keywords: Canonical Gentzen-type Systems, Coherence Criterion, CORR 2008, Education, Systems