Canonical signed calculi with multi-ary quantifiers (Q408550)

Arnon Avron and his colaborators introduced both the notion of canonical sequent calculi and nondeterministic matrices. In particular, the relations between the criterion of coherence, cut elimination and characterization via nondeterministic matrices were investigated in earlier works. Nondeterministic matrices are meant as a generalization of standard matrices. The difference is that each \(n\)-ary operation is characterised as a function which selects a set of values instead of exactly one value for any \(n\)-tuple. Canonical sequent calculi are made of standard structural rules and logical rules which introduce exactly one occurrence of a logical constant in the conclusion. Finally, the notion of coherence provides a simple and effective criterion for rules in canonical calculi which allow for determination of the meanings of constants. In this paper the notion of canonicity is extended to one-sided sequent calculi built up from formulas signed with labels expressing truth values (with the special case of two labels corresponding to ordinary two-sided sequents). Moreover, only rules for multi-ary quantifiers, i.e. binding one variable in \(n\) formulas for some \(n > 1\), are considered. In the context of these calculi the criterion of coherence requires that for any set of (basic instances) of rules such that the intersection of sets of labels of the main formula is empty, the union of side formulas is inconsistent. Two notions of cut elimination are considered for derivability of a conclusion sequent from the set of premise sequents: strong, which admits only cuts made on (substitution of) elements of premise sequents, and strong analytic, which admits also cuts on subformulas of premise sequents and the conclusion sequent. Note that in case of an empty set of premise sequents (a proof of the conclusion sequent) in the first case we obtain ordinary cut elimination, whereas in the second, analytic cuts (on subformulas of the conclusion sequent) are not eliminable. The main result of the paper concerns the equivalence of three statements for any canonical signed calculus \(G\): (a) \(G\) is coherent; (b) \(G\) has strongly characteristic finite nondeterministic matrix; (c) \(G\) admits strong analytic cut elimination. It is interesting to note that although coherence is a sufficient condition for strong cut elimination in canonical standard sequent calculi (two-sided sequents or with two labels), it is insufficient for signed calculi with more than two labels.