Any one of a family of translations from the language of intuitionistic logic into the modal language of $\text{S}4$. A very simple version can be given recursively:

• • $p^{\tau }=\square p$ when $p$ is an atomic formula

• • ${\left(\neg \phi \right)}^{\tau }=\square \neg \left({\phi }^{\tau }\right)$ where $\neg$ is a negation

• • ${\left(\phi \circ \psi \right)}^{\tau }=\square \left({\left(\phi \right)}^{\tau }\circ \left({\psi }^{\tau }\right)\right)$ where $\circ$ is a conjunction $\wedge$, disjunction $\vee$, or conditional $\to$

These translations are notable for showing a particular correspondence between intuitionistic logic and $\text{S}4$, such that a formula is valid intuitionistically if and only if its translation is valid in $\text{S}4$. Although the original translation of mathematician Kurt Gödel (1906–1978) only preserves validity or theoremhood, the later translations of J. C. C. McKinsey (1908–1953) and Alfred Tarski (1901–1983) preserve validity in general, so that:

${\phi }_0,\mathrm{\dots },{\phi }_{n-1}{\models }_{\text{Int}}\psi$ iff ${\phi }_0^{\tau },\mathrm{\dots },{\phi }_{n-1}^{\tau }{\models }_{\text{Int}}{\psi }^{\tau }$

Gödel interpreted the $\square$ operator of $\text{S}4$ as a provability operator, so that intuitionistic logic becomes an implicit provability logic.