经典非单调交互式证明的逻辑：否定完全与析取性质

"否定完全交互式证明的逻辑" 这篇论文探讨的是经典正规模态逻辑的一个特殊领域，重点关注否定完全交互式证明的逻辑（LDiiP）和即时交互式证明的逻辑（LiiP）。这两个概念是理论计算机科学中的形式逻辑分支，涉及到证明理论和多代理系统的证明检查过程。 在LiiP的基础上，作者西蒙·克雷默发展出一个内在否定完备的经典正规模态逻辑——LDiiP。这个新的逻辑系统内化了以代理为中心的证明理论，其中的证明目标可以在证明或证伪的意义上被定义，这得益于反言内在化证明的概念，也被称为认知决策者。值得注意的是，尽管LDiiP是经典的、单调的，但它是负不完全的，不具备析取性质，即它不能确保所有合取公式都能被分解为析取公式。 另一方面，LiiP是非单调的，不构造性的，并且具有析取性质，类似于直觉逻辑。然而，它并不具有否定完备性，这意味着不是所有的陈述都可以被证明或证伪。在LiiP的语境中，证明是基于代理的交互，这些代理在资源无限的假设下进行证明检查。 论文通过引入LiiP的选择公理，并利用特定的预言机可计算函数，为LDiiP提供了标准的Kripke语义。这种语义允许对逻辑系统进行形式化的理解和分析。此外，作者还强调了交互式证明的非单调性和非公共性，这是针对单例代理社区的特性。 关键词如“代理作为证明检查器”、“建设性Kripke语义”、“认知决策者作为决定性证据”等，揭示了研究的焦点在于理解证明过程如何在多代理环境中运作，以及如何通过代理的交互来确定认知状态和决策。 在介绍部分，作者指出他们的工作受到了之前研究的影响，如[20, 19, 17]，并且他们的交互式证明模型依然假定证明检查代理具有无限的预期资源。此外，研究得到了卢森堡国家研究基金的支持，并在开放获取许可下发表，这表明其结果可以被广泛访问和使用。 这篇论文深入研究了交互式证明逻辑的否定完备性，提出了一种新的经典正规模态逻辑，它结合了证明理论、多代理系统和形式逻辑的元素，为理解和构建非单调和交互式的证明环境提供了新的视角。