Some better-known facts

Let me begin this article like a good book on mathematical logic: with Kurt Gödel and a definition. In a short paper from 1933 titled “Eine Interpretation des intuitionistischen Aussagenkalküls” (An interpretation of the intuitionistic propositional calculus), Gödel came up with the following translation from intuitionistic propositional logic ($\mathsf{IPL}$) into modal logic (Gödel 1933a).¹

The motivation behind this interpretation was to capture the constructive meaning of intuitionistic logic, which Heyting had introduced as a complete formal system only three years earlier (Heyting 1930). Gödel added the $\Box$ modality to classical logic as a rather informal operator, for which he came up with a somewhat reasonable axiomatisation:

As readers familiar with modal logic will have recognised, this logic is nowadays known as the classical modal logic $\mathsf{S4}$. In the same paper, Gödel shows that this interpretation of intuitionistic logic inside classical modal logic is sound, i.e.: if $\mathsf{IPL} \vdash A$ then $\mathsf{S4} \vdash tr^G(A)$. This was rather easy and could be done using only the axiomatic Hilbert systems of intuitionistic propositional logic and $\mathsf{S4}$. However, the question of completeness – while conjectured to be true – was left open, until proved in 1948 by McKinsey and Tarski (McKinsey and Tarski 1948). This is also why the following is known as the Gödel-McKinsey-Tarski Theorem (GMTT):

Theorem 1. $\mathsf{IPL} \vdash A$ iff $\mathsf{S4} \vdash tr^G(A)$.

This still left the question about first-order intuitionistic logic open, which was proved a good few years later in 1963 by Rasiowa and Sikorski (Rasiowa and Sikorski 1963) who proved full faithfulness of an embedding from first-order intuitionistic logic into first-order modal logic.

Modalities as provability predicates

It is not clear from where exactly Gödel had the idea to use a modal operator to express an informal notion of provability of a sentence. But just as many other ideas throughout scientific history, it seems to me as if using a modality to denote provability was somewhat of a folklore idea among modal logicians the early 20th century.

One obvious candidate for furthering this idea and making it formal is Gödel himself and his incompleteness theorems, the first of which he had published in 1931 (Gödel 1931), two years prior to his interpretation. For proving incompleteness of set theory² he constructed a formal provability predicate enabling set theory to talk about its own provability. This is also what later lead to the development of modal provability logic, where $\square$ is interpreted as precisely such a formal provability predicate. However, the basic modal provability logic, known as Gödel-Löb logic, turned out to be inconsistent with $\mathsf{S4}$.³ Still, one can directly connect the two notions of informal and formal provability in two ways. One approach is to interpret $\square$ as ‘‘provable and true’’ leading to an extension of $\mathsf{S4}$ known as Grzegorczyk logic ($\mathsf{Grz}$).⁴ The completeness of $\mathsf{Grz}$ with respect to this provability interpretation was proved independently by Rob Goldblatt (Goldblatt 1978), as well as Alexander Kuznetsov and Alexei Muravitsky (Kuznetsov and Muravitsky 1976). Another approach is to have indexed modalities by terms that carry explicit information about the proofs which leads to an $\mathsf{S4}$-like justification logic known as Logic of Proof (Artemov and Fitting 2019). Notably, it was proved by Andrzej Grzegorczyk (Grzegorczyk 1967) in 1967 that the faithfulness of the Gödel embedding also holds for his logic:

Theorem 2. $\mathsf{IPL} \vdash A$ iff $\mathsf{Grz} \vdash tr^G(A)$.

Remarkably, this gives us two ways in which we can explicitly connect formal mathematical provability to intuitionistic logic. Either via the Logic of Proof and Theorem 1, or via the provability interpretation of $\mathsf{Grz}$ and Theorem 2.

What you might not know about the GMTT

These results are all well and nice, and this is usually where the main story ends. But it is notable that all commonly known proofs of the previous two theorems rely on topological and algebraic ideas. This is in contrast to my own research interests. Thus, enter Proof Theory.

It was while I was doing research for my Master of Logic thesis (Becker 2024) that I was lead down a rabbit hole. This rabbit hole began with a proof system of a certain Maehara-style found in (Kuznets and Straßburger 2019), a central system in my master’s thesis. The style of the calculus is attributed to Shôji Maehara who introduced it in his paper titled “Eine Darstellung der Intuitionistiuschen Logik in der Klassischen” (A representation of intuitionistic logic inside classical logic) from 1954 (Maehara 1954) for which no English translation exists.

As the keen reader might guess by the title of this paper, I noticed that there could be a more groundbreaking result that Maehara had presented there. Clearly, the title suggests that one might find a result similar to the GMTT. So I started reading that paper out of curiosity. Let me highlight the main points that I have found.

The paper begins by remarking on the well known double negation translation. More specifically, Maehara mentions the interpretation of classical logic inside intuitionistic logic by Sigekatu Kuroda using a double negation translation (Kuroda 1951). Similar results have also been independently discovered by Kolmogorov (Kolmogorov 1925), Gödel(Gödel 1933b) and Gentzen (Gentzen 1974). The paper then motivates itself by considering a reverse interpretation of intuitionistic logic in classical logic. The idea is very similar to the one of Gödel, however it seems as if Maehara was not aware of the previous developments in modal logic. Note also, that Maehara considers not a translation from intuitionistic propositional logic to its classical relative, but instead from intuitionistic first-order logic to classical first-order logic.

Maehara introduces a new connective Bew which stands for Beweis or beweisbar (proof or provability), essentially a unary modality expressing informal provability. Thus, let us identify $\textnormal{Bew} = \square$ to make the connection to the previous sections explicit. After recalling Gerhard Gentzen’s sequent calculi for classical and intuitionistic logic (Gentzen 1935), he introduces his own Hilfskalkül (helping calculus) which is the previously mentioned Maehara calculus. He shows that his calculus is equivalent to intuitionistic logic. The motivation for this calculus is to use it as a tool to show for his main theorem.

He then goes about introducing two sequent rules for his provability operator. As is usual in sequent calculus, there is a left rule and a right rule:

$\Gamma$ and $\Theta$ are lists of formulas (or sequences of formulas, which is why it’s called the sequent calculus).⁵ Maehara remarks, almost coincidentally, that these sequent rules are equivalent to the following:

It is now a very easy exercise to show that this logic is a first-order version of $\mathsf{S4}$ which we call $\mathsf{QS4}$. Moreover, we can actually derive the converse Barcan formula $\square \forall x A \to \forall x \square A$ which can be a desired feature of a first-order modal logic (see (Cresswell and Hughes 1996) p. 245). As is natural in sequent calculus, Maehara shows consistency and closure under modus ponens for $\mathsf{QS4}$ by proving cut-elimination.

Formulas of the form $\square A$ should now be read as “$A$ is provable”. Thus, he makes the connection between the classical reading of a formula $A$ as ‘’$A$ is true’’ and its intuitionistic reading as ‘‘it is provable that $A$ is true’’ explicit via the following translation:

Simply put, this translations just puts a $\square$ in front of every subformula. It is a nice exercise to show that, in the propositional case, this translation is actually equivalent to $tr^G(\cdot)$ from before. Thus, it almost seems unsurprising to find a theorem similar to the GMTT. However, here we connect first-order intuitionistic logic ($\mathsf{IFOL}$) with the first-order modal logic $\mathsf{QS4}$.

Theorem 3. $\mathsf{IFOL} \vdash A$ iff $\mathsf{QS4} \vdash tr^M(A)$.

Showing the left-to-right direction is rather straightforward, indeed Gödel could prove it axiomatically for the propositional case. The converse is quite involved and makes use of the Maehara calculus from before. In essence, a classical proof of $tr^M(A)$ gets non-locally transformed into an intuitionistic Maehara-style proof such that all occurrences of $\square$ are removed. We might therefore rightfully claim that this is the first GMTT for first-order intuitionistic logic preceding the result of Rasiowa and Sikorski by about a decade.

But wait, there is more! This is merely the Hauptsatz (main theorem) of the paper. There is one additional theorem in the paper which is not there to derive the main theorem, connecting to intuitionistic first-order modal logic $\mathsf{IQS4}$:⁶

Theorem 4. $\mathsf{IFOL} \vdash A$ iff $\mathsf{IQS4} \vdash tr^M(A)$.

Thus, we have even another variant of a GMT-like theorem. Initially, it seemed that this would have been an unknown result, as I did not know anyone who knew about this. But then I realised that I only know proof theorists, and after some digging found that algebraicists of course also found this out (Wolter and Zakharyaschev 2014). But the story does not even end there: it was rather recently found by Jan von Plato (Plato 2025), who translated handwritten notes by Gödel, that he had also obtained a completeness result in 1941, although he never published it. The proof by Gödel also uses sequents, however his method differs from the one Maehara used.

I do not claim that Maehara’s result has been a “forgotten gem” that no one knew about. To the contrary, there are multiple sources I could find from the recent decades which explicitly cited this result (see (Inoué 2023; Yamasaki and Sano 2017) for the most recent ones). It still seems remarkable though that a result of such a scale has received so little attention; and that the vast majority of citations of Maehara’s Darstellung is only due to his proof system. Thus, the story about “Maehara’s Gödel-McKinsey-Tarski Theorem” can also be seen as a story about the sociology of mathematics. Especially deep results have a tendency to be discovered more than once, almost as if they want to be discovered. At the same time, some discoveries may lie dormant for decades, either because they sit unpublished in some handwritten notebook, or they must be read by the right person to be appreciated. Thus, one may only wonder how many more such theorems are quietly sitting in the literature, only waiting for someone curious enough to follow a rabbit hole.

Bibliography

Artemov, Sergei, and Melvin Fitting. 2019. Justification Logic: Reasoning with Reasons. Vol. 216. Cambridge University Press.

Becker, Justus. 2024. “Proof Translations for Intuitionistic Modal Logic.” MSc, ILLC, University of Amsterdam. https://eprints.illc.uva.nl/id/eprint/2325/1/MoL-2024-08.text.pdf .

Cresswell, Maxwell John, and George Edward Hughes. 1996. A New Introduction to Modal Logic. Routledge.

Gentzen, Gerhard. 1935. “Untersuchungen [ü]{.nocase}ber Das Logische Schließen. i.” Mathematische Zeitschrift 39:176–210.

———. 1974. “Über Das [Verh[ä]{.nocase}ltnis]{.nocase} Zwischen Intuitionistischer Und Klassischer Arithmetik.” Archiv für Mathematische Logik Und Grundlagenforschung 16:119–32. https://doi.org/10.1007/BF02015371 .

Gödel, Kurt. 1931. “Über Formal Unentscheidbare sätze Der Principia Mathematica Und Verwandter Systeme i.” Monatshefte für Mathematik Und Physik 38 (1): 173–98.

———. 1933a. “Eine Interpretation Des Intuitionistischen Aussagenkalküls.” Ergebnisse Eines Mathematischen Kolloquiums 4:39–40.

———. 1933b. “Zur Intuitionistischen Arithmetik Und Zahlentheorie.” Ergebnisse Eines Mathematischen Kolloquiums 4:34–38.

Goldblatt, Rob. 1978. “Arithmetical Necessity, Provability and Intuitionistic Logic.” Theoria 44 (1): 38–46. https://doi.org/ https://doi.org/10.1111/j.1755-2567.1978.tb00831.x .

Grzegorczyk, Andrzej. 1967. “Some Relational Systems and the Associated Topological Spaces.” Fundamenta Mathematicae 60 (3): 223–31.

Heyting, A. 1930. Die Formalen Regeln Der Intuitionistischen Logik i. Sitzungsberichte der Preussischen Akademie der Wissenschaften zu Berlin.

Inoué, Takao. 2023. “Epistemic Systems and Flagg and Friedman’s Translation.” https://arxiv.org/abs/2307.02688 .

Kolmogorov, Andrei Nikolaevich. 1925. “O Principe Tertium Non Datur.” Matematicheskij Sbornik 32:646–67.

Kuroda, Sigekatu. 1951. “Intuitionistische Untersuchungen Der Formalistischen Logik.” Nagoya Mathematical Journal 2:35–47. https://doi.org/10.1017/S0027763000010023 .

Kuznets, Roman, and Lutz Straßburger. 2019. “Maehara-Style Modal Nested Calculi.” Archive for Mathematical Logic 58 (May):359–85. https://doi.org/10.1007/s00153-018-0636-1 .

Kuznetsov, A. V., and A. Yu. Muravitsky. 1976. “The Logic of Provability.” In Abstracts of the 4th All-Union Conference on Mathematical Logi, 73.

Maehara, Shôji. 1954. “Eine Darstellung Der Intuitionistischen Logik in Der Klassischen.” Nagoya Mathematical Journal 7:45–64. https://doi.org/10.1017/S0027763000018055 .

McKinsey, J. C. C., and Alfred Tarski. 1948. “Some Theorems about the Sentential Calculi of Lewis and Heyting.” The Journal of Symbolic Logic 13 (1): 1–15.

Plato, Jan von. 2025. “Gödel’s Modal Interpretation of Intuitionistic Logic and Its Proof Theory.” Monatshefte Für Mathematik 208 (4): 791–817. https://doi.org/10.1007/s00605-025-02083-0 .

Rasiowa, H., and R. Sikorski. 1963. The Mathematics of Metamathematics. Monografie Matematyczne. PWN-Polish Scientific Publishers.

Wolter, Frank, and Michael Zakharyaschev. 2014. “On the Blok-Esakia Theorem.” In Leo Esakia on Duality in Modal and Intuitionistic Logics, edited by Guram Bezhanishvili, 99–118. Dordrecht: Springer Netherlands. https://doi.org/10.1007/978-94-017-8860-1_5 .

Yamasaki, Sakiko, and Katsuhiko Sano. 2017. “Proof-Theoretic Embedding from Visser’s Basic Propositional Logic to Modal Logic K4 via Non-Labelled Sequent Calculi.” In Philosophical Logic: Current Trends in Asia, edited by Syraya Chin-Mu Yang, Kok Yong Lee, and Hiroakira Ono, 233–57. Singapore: Springer Singapore.