# Translations between S4 and S5 modal logics

$\textbf{Question}$: Is there a translation from $\textbf{S5}$ modal logic to $\textbf{S4}$ such that

$$\text{If} \hspace{0.3cm} \textbf{S5} \vdash F \hspace{0.3cm} \text{then } \hspace{0.3cm} \textbf{S4} \vdash F'$$

where $F'$ is formed from $F$ by applying a suitable translation $\hspace{0.2cm}'$?

I take it that every theorem of $\textbf{S4}$ is a theorem of $\textbf{S5}$, the former being a sublogic of the latter, the translation of $\textbf{S4}$ into $\textbf{S5}$ thereby being trivial.

My interest in this question comes from considering Goedel's translation of Intuitionistic propositional logic into $S4$, and how that translation would look in $S5$, but since $S4$ is a sublogic of $\textbf{S5}$, there would be only a trivial translation. However, I don't know of a translation of $\textbf{S5}$ into $\textbf{S4}$. If there is a particular reason why such a translation does not or could not exist, I would be interested to know.

$\textbf{S5}$ is characterised by the axioms for classical propositional logic alongside the $\textbf{Necessitation Rule}$: If $A$ is a theorem, then so is $□A$), plus the axioms below. $\textbf{S4}$ is characterised by the axioms for classical propositional logic plus the the Necessitation Rule and the $\textbf{K,T, 4}$ axioms below (as usual, $\Diamond A := \neg \thinspace\Box \neg A$):

$$\textbf{K}: \Box(A\to B)\to(\Box A\to\Box B);$$ $$\textbf{T}: \Box A \to A$$,

and either:

$$\textbf{5}: \Diamond A\to \Box\Diamond A;$$ or both: $$\textbf{4}: \Box A\to\Box\Box A,$$ and $$\textbf{B}: A\to\Box\Diamond A.$$

As written, there is a trivial such translation: just put $F'=\top$ for all formulas $F$.
Assuming you actually wanted to formulate the condition as “if and only if” rather than just “if”, a simple such translation is provided by $$\mathrm{S5}\vdash A\iff\mathrm{S4}\vdash\Diamond\Box A.$$
• I don't understand why a formula $A$ of $S4$ does not simply translate as $A$ in $S5$, given that $S4$ is a sublogic of $S5$, so that $S4 \vdash \Diamond \Box A$ translates as $S5 \vdash \Diamond \Box A$. – user65526 Apr 13 '18 at 16:41
• I don’t understand the point of your comment. As it happens, $\mathrm{S4}\vdash\Diamond\Box A$ if and only if $\mathrm{S5}\vdash\Diamond\Box A$, but the question asks for a translation of S5 into S4, not for a translation of S5 into S5, so why would I mention $\mathrm{S5}\vdash\Diamond\Box A$? – Emil Jeřábek Apr 13 '18 at 16:44
• I thought a translation of $S5$ into $S4$ would mean only $S5 ⊢ A\Rightarrow S4 ⊢ A'$, for some translation function $'$, and not the converse, as you stated. – user65526 Apr 13 '18 at 16:47
• I wasn't taking into account trivial translation functions. What I meant to say is that I thought a non-trivial translation of S5 into S4 would mean only$S5⊢A⇒S4⊢A′$, for some non-trivial translation function $′$, and not the converse, as you stated. – user65526 Apr 13 '18 at 17:07