具有（n，k）元量词的典范演算
Canonical calculi with (n,k)-ary quantifiers
摘要：
2001年由Avron和Lev提出的命题规范Gentzen型系统，除了标准公理和结构规则外，只有逻辑规则，其中只有一个连接词被引入，而没有其他连接词被提及。定义了这类系统的非平凡性的构造性凝聚准则，并证明了这类系统允许割消当且仅当它是凝聚的。这种系统的语义是使用二值非确定性矩阵（2N矩阵）。在2005年，Zamansky和Avron将这些结果扩展到了一元量词的严格形式。在本文中，我们大大扩展的典型系统的特征（n，k）-ary量词，绑定k个不同的变量和连接n个公式，并表明，一致性标准仍然是建设性的，这样的系统。然后，我们讨论了k {0，1}的情形，证明了当正则演算G具有强特征2N矩阵时，G是相干的，这就等价于允许强割消.
英文摘要：
Propositional canonical Gentzen-type systems, introduced in 2001 by Avron and 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. A constructive coherence criterion for the non-triviality of such systems was defined and it was shown 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). In 2005 Zamansky and Avron extended these results to systems with unary quantifiers of a very restricted form. In this paper we substantially extend the characterization of canonical systems to (n,k)-ary quantifiers, which bind k distinct variables and connect n formulas, and show that the coherence criterion remains constructive for such systems. Then we focus on the case of k∈{0,1} and for a canonical calculus G show that it is coherent precisely when it has a strongly characteristic 2Nmatrix, which in turn is equivalent to admitting strong cut-elimination.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
