A translation of Maehara's "Eine Darstellung der Intuitionistischen Logik in der Klassischen"
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.
Related
- Approximate Transitivity of Young Translation on Rough Paths
- A Finite-Range, Translation-Invariant Counterexample to Weak Gibbsianity
- Translation of Dolbeault Representations
- Scalar curvature, volume, and Weil-Petersson translation length
- Reverse Translation and Convolution Estimates in the Framework of the Mehler-Fock Transform
BibTeX
@misc{becker2026translation,
title = {{A translation of Maehara's "Eine Darstellung der Intuitionistischen Logik in der Klassischen"}},
author = {Justus Becker},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.24673},
eprint = {2609.24673},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.24673},
}
RIS
TY - UNPB
TI - A translation of Maehara's "Eine Darstellung der Intuitionistischen Logik in der Klassischen"
AU - Justus Becker
PY - 2026
DA - 2026/09/23
PB - arXiv
DO - 10.48550/arxiv.2609.24673
UR - https://arxiv.org/abs/2609.24673
AB - 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.
ER -