# zbMATH — the first resource for mathematics

Generalized non-deterministic matrices and $$(n,k)$$-ary quantifiers. (English) Zbl 1132.03342
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 26-40 (2007).
Summary: An $$(n,k)$$-ary quantifier is a generalized logical connective, binding $$k$$ variables and connecting $$n$$ formulas. Canonical Gentzen-type systems with $$(n,k)$$-ary quantifiers are systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of an $$(n,k)$$-ary quantifier is introduced. The semantics of such systems for the case of $$k \in {0,1}$$ are provided in [A. Zamansky and A. Avron, “Canonical Gentzen-type calculi with $$(n,k)$$-ary quantifiers”, Lect. Notes Comput. Sci. 4130, 251–265 (2005)] using two-valued non-deterministic matrices (2Nmatrices). A constructive syntactic coherence criterion for the existence of a 2Nmatrix for which a canonical system is strongly sound and complete, is formulated there. In this paper we extend these results from the case of $$k \in \{0,1\}$$ to the general case of $$k \geq 0$$. We show that the interpretation of quantifiers in the framework of Nmatrices is not sufficient for the case of $$k > 1$$ and introduce generalized Nmatrices which allow for a more complex treatment of quantifiers. Then we show that (i) a canonical calculus $$G$$ is coherent iff there is a 2GNmatrix, for which $$G$$ is strongly sound and complete, and (ii) any coherent canonical calculus admits cut-elimination.
For the entire collection see [Zbl 1121.03005].
Reviewer: Reviewer (Berlin)

##### MSC:
 03C80 Logic with extra quantifiers and operators 03F05 Cut-elimination and normal-form theorems
Full Text: