Canonical signed calculi with multi-ary quantifiers

详细信息	查看全文 | 推荐本文 |

• 作者：Anna Zamansky^a ; ^{annazam@gmail.com} ; Arnon Avron^b
• 关键词：03F03 ; 03B22
• 刊名：Annals of Pure and Applied Logic
• 出版年：2012
• 期刊代码：4_01680072
• 类别：cp
• 出版时间：July, 2012
• 卷：163
• 期：7
• 页码：951-960
• 文件大小：269 K

摘要

Canonical Gentzen-type calculi are a natural class of systems, which in addition to the standard axioms and structural rules have only logical rules introducing exactly one connective. There is a strong connection in such systems between a syntactic constructive criterion of coherence, the existence of a two-valued non-deterministic semantics for them and strong cut-elimination. In this paper we extend the theory of canonical systems to signed calculi with multi-ary quantifiers. We show that the extended criterion of coherence fully characterizes strong analytic cut-elimination in such calculi, and use finite non-deterministic matrices to provide modular semantics for every coherent canonical signed calculus.