arXiv 2103.114802021-03-21math.LO

一元直觉主义和模态逻辑承认可证性解释

Monadic Intuitionistic and Modal Logics Admitting Provability Interpretations

Guram Bezhanishvili, Kristina Brantley, Julia Ilin

摘要：

哥德尔翻译提供了一种将直觉主义逻辑$\mathsf{IPC}$嵌入模态逻辑$\mathsf{Grz}$的方法，然后模态逻辑通过分裂翻译嵌入模态逻辑$\mathsf{GL}$。结合Solovay定理，$\mathsf{GL}$是Peano算术$\mathsf{PA}$的可证性谓词的模态逻辑，$\mathsf{IPC}$和$\mathsf{Grz}$都允许算术解释。当试图将这些结果“提升”到这些逻辑的一元扩展$\mathsf{MIPC}$、$\mathsf{MGrz}$和$\mathsf{MGL}$时，相同的技术不再起作用。根据Esakia的猜想，我们将Casari公式的适当版本添加到这些一元扩展中（用"+“表示），得到哥德尔翻译将$\mathsf{M^{+}IPC}$嵌入$\mathsf{M^{+}Grz}$，分裂翻译将$\mathsf{M^{+}Grz}$嵌入$\mathsf{MGL}$。正如Japaridze所证明的那样，Solovay的结果扩展到一元系统$\mathsf{MGL}$，这使我们对$\mathsf{M^{+}IPC}$和$\mathsf{M^{+}Grz}$都有了算术解释。

英文摘要：

The Gödel translation provides an embedding of the intuitionistic logic $\mathsf{IPC}$ into the modal logic $\mathsf{Grz}$, which then embeds into the modal logic $\mathsf{GL}$ via the splitting translation. Combined with Solovay's theorem that $\mathsf{GL}$ is the modal logic of the provability predicate of Peano Arithmetic $\mathsf{PA}$, both $\mathsf{IPC}$ and $\mathsf{Grz}$ admit arithmetical interpretations. When attempting to 'lift' these results to the monadic extensions $\mathsf{MIPC}$, $\mathsf{MGrz}$, and $\mathsf{MGL}$ of these logics, the same techniques no longer work. Following a conjecture made by Esakia, we add an appropriate version of Casari's formula to these monadic extensions (denoted by a '+'), obtaining that the Gödel translation embeds $\mathsf{M^{+}IPC}$ into $\mathsf{M^{+}Grz}$ and the splitting translation embeds $\mathsf{M^{+}Grz}$ into $\mathsf{MGL}$. As proven by Japaridze, Solovay's result extends to the monadic system $\mathsf{MGL}$, which leads us to an arithmetical interpretation of both $\mathsf{M^{+}IPC}$ and $\mathsf{M^{+}Grz}$.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

摘要：

英文摘要：

相关论文