论文标题
用一种模态定量反射分积分
Quantified Reflection Calculus with one modality
论文作者
论文摘要
本文介绍了逻辑QRC $ _1 $，这是量化模态逻辑的严格正面片段。钻石方式的预期阅读是形式理论的一致性。谓词符号被解释为参数化的公理。我们证明了逻辑QRC $ _1 $相对于此算术解释的算术声音。 已知量化的可预致性逻辑是不可决定的。但是，无法在我们的签名和算术阅读中执行不可证明的证明。我们推测逻辑QRC $ _1 $要完成算术。本文通过提供相应的完整性证明的QRC $ _1 $的关系语义来迈出算术完整性的第一步。我们还显示有限模型属性，这意味着可决定性。
This paper presents the logic QRC$_1$, which is a strictly positive fragment of quantified modal logic. The intended reading of the diamond modality is that of consistency of a formal theory. Predicate symbols are interpreted as parametrized axiomatizations. We prove arithmetical soundness of the logic QRC$_1$ with respect to this arithmetical interpretation. Quantified provability logic is known to be undecidable. However, the undecidability proof cannot be performed in our signature and arithmetical reading. We conjecture the logic QRC$_1$ to be arithmetically complete. This paper takes the first steps towards arithmetical completeness by providing relational semantics for QRC$_1$ with a corresponding completeness proof. We also show the finite model property, which implies decidability.
