双直觉时态逻辑的消割与证明搜索
计算机科学中的逻辑
2010-06-30 v2
摘要
我们考虑用经典时态逻辑Kt中的传统模态算子对双直觉逻辑进行扩展。从证明论角度看，这种扩展只需通过将用于显示逻辑的模态算子的典型推理规则添加到双直觉逻辑的现有矢列演算中即可获得。结果表明，由此产生的演算LBiKt似乎比文献中考虑的大多数直觉主义时态或模态逻辑（特别是Ewald和Simpson研究过的那些）更为基础，因为它没有假设菱形和方框模态算子之间存在任何先验关系。我们通过模块化地向LBiKt添加额外的结构规则，恢复了Ewald的直觉主义时态逻辑和Simpson的直觉主义模态逻辑。演算LBiKt采用一种显示演算的变体形式，使用一种称为嵌套矢列的矢列形式。我们使用类似于显示演算的技术证明了LBiKt的消割定理。与显示演算一样，LBiKt的推理规则是“浅层”规则，即它们作用于嵌套矢列中的顶层公式。由于存在某些称为“显示公设”的结构规则以及对任意结构的收缩规则，LBiKt演算不适合于反向证明搜索。我们展示了这些结构规则可以在另一个使用深层推理的演算DBiKt中变得冗余，该演算允许在嵌套矢列的任意深度应用推理规则。我们证明了LBiKt和DBiKt之间的等价性，并概述了DBiKt的证明搜索策略。我们还给出了一个克里普克语义，并证明了LBiKt相对于该语义是可靠的，但完备性仍是一个未解决的问题。最后，我们讨论了LBiKt的各种扩展。
引用
@article{arxiv.1006.4793,
title = {Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic},
author = {Rajeev Gore and Linda Postniece and Alwen Tiu},
journal= {arXiv preprint arXiv:1006.4793},
year = {2010}
}