A cirquent calculus system with clustering and ranking

详细信息    查看全文

• 作者：Wenyan Xu ^{xwykiki@126.com" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Computability logic ; Cirquent calculus ; IF logic
• 刊名：Journal of Applied Logic
• 出版年：2016
• 出版时间：July 2016
• 年：2016
• 卷：16
• 期：Complete
• 页码：37-49
• 全文大小：375 K

文摘

Cirquent calculus is a new proof-theoretic and semantic approach introduced by G. Japaridze for the needs of his theory of computability logic (CoL). The earlier article “From formulas to cirquents in computability logic” by Japaridze generalized formulas in CoL to circuit-style structures termed cirquents. It showed that, through cirquents with what are termed clustering and ranking, one can capture, refine and generalize independence-friendly (IF) logic. Specifically, the approach allows us to account for independence from propositional connectives in the same spirit as IF logic accounts for independence from quantifiers. Japaridze's treatment of IF logic, however, was purely semantical, and no deductive system was proposed. The present paper syntactically constructs a cirquent calculus system with clustering and ranking, sound and complete w.r.t. the propositional fragment of cirquent-based semantics. Such a system captures the propositional version of what is called extended IF logic, thus being an axiomatization of a nontrivial fragment of that logic.