AI 中文总结
本文翻译了Maehara 1954年关于直觉主义逻辑嵌入经典模态逻辑的论文，该工作独立于Gödel，使用证明论方法扩展了嵌入到一阶直觉主义模态逻辑。
AI 中文摘要
Heyting直觉主义逻辑的一个关键动机是获得Brouwer关于数学作为“心智构造”思想的正式概念。因此，有人可能会争辩说，Heyting的演算也应该对应于一种可证明性的概念。受这一想法的启发，Gödel通过嵌入到模态演算（现在称为模态逻辑S4）中形式化了这种联系。虽然在他最初的出版物中，他只证明了从直觉主义命题逻辑到S4的嵌入的可靠性，但逆命题在十五年后由McKinsey和Tarski证明。尽管后来发现，Gödel在1941年的未发表笔记中已经获得了其嵌入忠实性的证明。Rasioa和Sikorski后来将Gödel的嵌入扩展到一阶直觉主义逻辑。1954年，Maehara使用证明论方法独立获得了相同的结果，甚至将嵌入从直觉主义一阶逻辑扩展到直觉主义一阶模态逻辑。本文档提供了Maehara 1954年论文的忠实英文翻译。
英文摘要
A key motivation for Heyting's intuitionistic logic was to gain a formal notion of Brouwer's idea of mathematics as a "construction of the mind". One might thus argue that Heyting's Calculus should also correspond to a notion of provability. Inspired by this idea, Gödel formalised this connection via an embedding into a modal calculus, which is now known as the modal logic S4. While in his original publication, he only proved soundness for the embedding from intuitionistic propositional logic into S4, the converse was proved fifteen years later by McKinsey and Tarski. Although, it was later discovered that Gödel also had obtained a proof of the faithfulness of his embedding in unpublished notes in 1941. Rasioa and Sikorski later extended Gödel's embedding to first-order intuitionistic logic. In 1954, Maehara independently obtained the same results using proof-theoretic methods, even extending the embedding to one from intuitionistic first-order logic into intuitionistic first-order modal logic. This document presents a faithful English translation of Maehara's 1954 paper.
CommentsCorrected several typos
