AI 中文总结
本文修正彼得鲁欣的证明，将命题逻辑嵌入可证性逻辑的结果扩展至$\boldsymbol{D}$，提出可嵌入$\boldsymbol{D}$的命题逻辑$\boldsymbol{DPL}$。
AI 中文摘要
正如维瑟（Visser）证明形式命题逻辑$\boldsymbol{FPL}$可嵌入哥德尔-洛布可证性逻辑$\boldsymbol{GL}$，彼得鲁欣（Petrukhin）提出命题逻辑$\boldsymbol{SPL}$可嵌入索洛维（Solovay）的非正规可证性逻辑$\boldsymbol{S}$。本文修正彼得鲁欣的证明，将该结果扩展至亚帕里泽（Japaridze）的可证性逻辑$\boldsymbol{D}$，并提出可嵌入$\boldsymbol{D}$的命题逻辑$\boldsymbol{DPL}$。
英文摘要
Just as Visser showed that the formal propositional logic $\mathbf{FPL}$ can be embedded into Gödel-Löb provability logic $\mathbf{GL}$, Petrukhin proposed a propositional logic $\mathbf{SPL}$ that can be embedded into Solovay's non-normal provability logic $\mathbf{S}$. In this paper, we fix Petrukhin's proof and extend the result to Japaridze's provability logic $\mathbf{D}$, and propose a propositional logic $\mathbf{DPL}$ that can be embedded into $\mathbf{D}$.
Comments25 pages
