Canonical Gentzen-type calculi with (n,k)-ary quantifiers

Propositional canonical Gentzen-type systems, introduced by Avron&Lev,
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. Avron&Lev 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. The semantics of such
systems is provided using two-valued non-deterministic matrices
(2Nmatrices). These results were then extended to systems with unary
quantifiers of a very restricted form.

In this talk we 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 is coherent, then it admits
cut-elimination.