双直觉主义逻辑的无切割矢列演算：扩展版
计算机科学中的逻辑
2007-05-23 v2
摘要
双直觉主义逻辑是直觉主义逻辑通过添加一个与蕴含对偶的联结词而得到的扩展。双直觉主义逻辑由 Rauszer 作为一个具有代数和 Kripke 语义的希尔伯特演算引入。但她随后为 BiInt 提出的“无切割”矢列演算，最近被 Uustalu 证明切割消去失败。我们为 BiInt 提出了一种新的无切割矢列演算，并证明了其相对于 Kripke 语义的可靠性和完备性。由于蕴含及其对偶联结词之间的相互作用，确保完备性变得复杂，这类似于时态逻辑中将来和过去模态词的情况。我们的演算通过使用扩展矢列来处理这种相互作用，这些矢列利用在失败推导树的叶节点处实例化的变量，将信息从前提出传递到结论。我们简单的终止性论证使得该演算可用于自动演绎，尽管这不是其主要目的。
引用
@article{arxiv.0704.1707,
title = {A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version},
author = {Linda Buisman and Rajeev Goré},
journal= {arXiv preprint arXiv:0704.1707},
year = {2007}
}