# zbMATH — the first resource for mathematics

A triple correspondence in canonical calculi: Strong cut-elimination, coherence, and non-deterministic semantics. (English) Zbl 1143.03028
Hirsch, Edward A. (ed.) et al., Computer science – theory and applications. Third international computer science symposium in Russia, CSR 2008 Moscow, Russia, June 7–12, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79708-1/pbk). Lecture Notes in Computer Science 5010, 52-63 (2008).
Summary: An $$(n,k)$$-ary quantifier is a generalized logical connective, binding $$k$$ variables and connecting $$n$$ formulas. Canonical systems with $$(n,k)$$-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence to characterize strong cut-elimination in such systems. We show that the following properties of a canonical system $$G$$ with arbitrary $$(n,k)$$-ary quantifiers are equivalent: (i) $$G$$ is coherent, (ii) $$G$$ admits strong cut-elimination, and (iii) $$G$$ has a strongly characteristic two-valued generalized non-deterministic matrix.
For the entire collection see [Zbl 1136.68005].
##### MSC:
 03F05 Cut-elimination and normal-form theorems 03C80 Logic with extra quantifiers and operators
Full Text: