Maehara’s proof links intuitionistic logic to modal logic s4 faithfully
A translation of Maehara's "Eine Darstellung der Intuitionistischen Logik in der Klassischen"
Logic in Computer Science
Summary
Intuitionistic logic is a way to think about math that focuses on building proofs step-by-step. Maehara showed a careful translation from intuitionistic logic into a related system called modal logic S4. This translation lets mathematicians understand and check intuitionistic proofs using classical logic techniques. The paper translated here presents Maehara’s original detailed proof from 1954, helping readers see how these two logical systems connect.
What this means in practice
- •For formal methods engineers: Use Maehara’s embedding to verify intuitionistic proofs within modal logic frameworks, facilitating formal verification systems.
- •For automated theorem prover developers: Incorporate Maehara’s result to improve theorem provers that handle intuitionistic logic by translating problems into modal logic S4.
A theory result. No direct application yet.
Authors
Justus Becker
Abstract
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.