$\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.$$



Translations between S4 and S5 modal logics
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.$$


