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)

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