Abstract

In 1933, Gödel in a short paper titled "An Interpretation of the Intuitionistic Propositional Calculus" proposed a logical system by adding three axioms and one rule of inference to the classical logic, which is equivalent to the Lewis S4 modal system. He proposed two translations slightly different from the formulas of the intuitionistic logic to the S4, claiming: "A formula is provable in intuitionistic logic, if its translation is provable in this system," and conjectures that the converse of this relationship also holds. The Gödel's claim and conjecture was proved by McKinsey and Tarski in 1948 using topological semantics for modal logic and intuitionistic logic, and in 1959 Dummut and Lemon proved this correspondence between the entire superintuitionistic logics and modal logics above S4. In this paper, we describe the proofs presented in the 1948 and 1959 papers, and we will endorse the correctness of these translations with some proofs.