Timeline for Translations between S4 and S5 modal logics
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13, 2018 at 17:56 | comment | added | user65526 | Ah, I get it. We just preface any S5 formula A with $\Diamond \Box$ | |
| Apr 13, 2018 at 17:39 | comment | added | user65526 | Ok, but say I have $S5⊢A \circ B$,for $\{\land, \lor, \rightarrow \} \in \circ$ and $S5 ⊢\neg A$. Would these be expressed in S4 as $\Diamond \Box A \circ \Diamond \Box B$ and $\neg \Diamond \Box A$? | |
| Apr 13, 2018 at 17:34 | comment | added | Emil Jeřábek | The translation is $A'=\Diamond\Box A$ for every formula $A$. It does not analyze the formula by connectives. | |
| Apr 13, 2018 at 17:12 | comment | added | user65526 | How does the translation you provided above work for the connectives? Is it simply $S5⊢A \circ B \Rightarrow S4 ⊢\Diamond \Box A \circ \Diamond \Box B$, for binary connectives $\{\land, \lor, \rightarrow \} \in \circ$ and $S5⊢\neg A \Rightarrow S4 ⊢\neg \Diamond \Box A$? | |
| Apr 13, 2018 at 17:07 | comment | added | user65526 | 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. | |
| Apr 13, 2018 at 17:04 | comment | added | Emil Jeřábek | 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. | |
| Apr 13, 2018 at 16:58 | vote | accept | user65526 | ||
| Apr 13, 2018 at 16:47 | comment | added | user65526 | 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. | |
| Apr 13, 2018 at 16:44 | comment | added | Emil Jeřábek | 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$? | |
| Apr 13, 2018 at 16:41 | comment | added | user65526 | 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$. | |
| Apr 13, 2018 at 16:32 | history | answered | Emil Jeřábek | CC BY-SA 3.0 |