Mapping intuitionistic logic to the modal logic S4

Question

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?

Answer 1

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.

Answer 2

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.