Canonical calculi with (n,k)-ary quantifiers

Propositional canonical Gentzen-type systems, introduced in 2001 by Avron andLev, are systems which in addition to the standard axioms and structural ruleshave only logical rules in which exactly one occurrence of a connective isintroduced and no other connective is mentioned. A constructive coherencecriterion for the non-triviality of such systems was defined and it was shownthat a system of this kind admits cut-elimination iff it is coherent. Thesemantics of such systems is provided using two-valued non-deterministicmatrices (2Nmatrices). In 2005 Zamansky and Avron extended these results tosystems with unary quantifiers of a very restricted form. In this paper wesubstantially extend the characterization of canonical systems to (n,k)-aryquantifiers, which bind k distinct variables and connect n formulas, and showthat the coherence criterion remains constructive for such systems. Then wefocus on the case of k∈{0,1} and for a canonical calculus G show that itis coherent precisely when it has a strongly characteristic 2Nmatrix, which inturn is equivalent to admitting strong cut-elimination.Comment: Special Issue of IJCAR2006, edited by Prof. Natarajan Shankar, paper LMCS-2007-20