In his famous Semantical Analysis of Intuitionistic Logic, S. Kripke speaks of the "well-known mappings of intuitionistic logic into the modal system S4". I'm not sure which mappings Kripke means. One guess would be K. Gödel's "Eine Interpretation des Intuitionistischen Aussagenkalküls" (translated into English as "An Interpretation of the Intuitionistic Propositional Calculus". I don't have access to either.)

Could somebody please point me towards a text that details these translations?

  • 1
    $\begingroup$ By the way, while this is 100% on topic here, you'd probably get a better answer on the cstheory stack exchange. $\endgroup$
    – Pseudonym
    Commented Mar 4, 2014 at 11:41
  • 1
    $\begingroup$ Yes, I was torn where to ask the question. I guess it's really well-known and trivial. So I went for cs.stackexchange. $\endgroup$ Commented Mar 4, 2014 at 11:59

2 Answers 2


That is the right paper, but there are actually several equivalent embeddings.

The book Basic Proof Theory by Troelstra and Schwichtenberg gives two such embeddings. Here's one. If $P$ is atomic but not $\bot$:

$$P^\circ := P$$ $$\bot^\circ := \bot$$ $$(A \wedge B)^\circ := A^\circ \wedge B^\circ$$ $$(A \vee B)^\circ := \square A^\circ \vee \square B^\circ$$ $$(A \rightarrow B)^\circ := \square A^\circ \rightarrow B^\circ$$ $$(\exists x A)^\circ := \exists x \square A^\circ$$ $$(\forall x A)^\circ := \forall x A^\circ$$

Here's the other:

$$P^\square := \square P$$ $$\bot^\square := \bot$$ $$(A \wedge B)^\square := A^\square \wedge B^\square$$ $$(A \vee B)^\square := A^\square \vee B^\square$$ $$(A \rightarrow B)^\square := \square (A^\square \rightarrow B^\square)$$ $$(\exists x A)^\square := \exists x A^\square$$ $$(\forall x A)^\square := \square \forall x A^\square$$

They are equivalent in the sense that $S4 \vdash \square A^\circ \leftrightarrow A^\square$, and the embeddings are sound and faithful. The proofs are left as an exercise, or you can dig out the book.

  • $\begingroup$ I have that book, and I even looked at its index before I asked my question, but the entry "intuistic logic" does not point towards anything useful. I should have looked at the table of content instead. $\endgroup$ Commented Mar 4, 2014 at 12:01
  • 2
    $\begingroup$ Correction (comparing the above answer to §9.2.1 and §9.2.2 on page 288 of the second edition of Troelstra&Schwhichtenberg): $P^□$ is defined as $□P$ for atomic $P$, and the equivalence is that $S4⊢□A^∘↔A^□$. $\endgroup$
    – Gro-Tsen
    Commented Mar 19, 2019 at 23:35

In addition to the two translations Pseudonym mentions in his/her reply, I found another one here: It's from intuitionistic propositional logic to GL, the logic of provability. GL is characterised by the following axioms.

  • $\square(A \rightarrow B) \rightarrow \square A \rightarrow \square B$.
  • $\square A \rightarrow A$.
  • $\square A \rightarrow \square \square A$.
  • $\square (\square A \rightarrow A) \rightarrow \square A$.

Now the embedding is given by the following clauses.

  • $p^{\triangle} := p \wedge \square p$.
  • $\bot^{\triangle} := \bot$.
  • $(A \wedge B)^{\triangle} := A^{\triangle} \wedge B^{\triangle}$.
  • $(A \vee B)^{\triangle} := A^{\triangle} \vee B^{\triangle}$.
  • $(A \rightarrow B)^{\triangle} := ( A^{\triangle} \rightarrow B^{\triangle}) \wedge \square ( A^{\triangle} \rightarrow B\ ^{\triangle})$.

We can show that $\vdash A$ in intuitionistic propositional logic iff $\vdash_{GL} A^{\triangle}$ in GL.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.