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