1
$\begingroup$

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

$\endgroup$
4
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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$. $\endgroup$ – user65526 Apr 13 '18 at 16:41
  • $\begingroup$ 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$? $\endgroup$ – Emil Jeřábek Apr 13 '18 at 16:44
  • $\begingroup$ 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. $\endgroup$ – user65526 Apr 13 '18 at 16:47
  • $\begingroup$ Well but then its existence would be trivial between any pair of logics, as I wrote in the beginning of my answer, hence it would not be a useful concept. $\endgroup$ – Emil Jeřábek Apr 13 '18 at 17:04
  • $\begingroup$ 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. $\endgroup$ – user65526 Apr 13 '18 at 17:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.