Dynamic topological S5 (Q1024554)

Phil Kremer has a very elegant and succinct style of presentation. In this paper, he presents four temporal extensions of the modal logic S5 interpreted on topological spaces. In this setting, the interpretation of a formula is a subset of a topological space. In particular, the interpretation of \(\square \phi\) is the \textit{interior} of the interpretation of \(\phi\). The \textit{almost discrete} and the trivial topological space both satisfy the S5 validities; in topological terms they both satisfy that every open set is closed. So far, S5 in topological semantics. In \textit{dynamic topological logic}, the language with the \(\square\) modality is extended with the temporal modalities \(\bigcirc\) and \(\star\), for, respectively, next and (henceforth/always in the future). The temporal \textit{next} modality \(\bigcirc\) is interpreted by applying a function \(f\) on the topology: the interpretation of \(\bigcirc \phi\) is the \(f\)-inverse of the interpretation of \(\phi\). The four considered topologies-cum-functions considered are: \(\bullet\) continuous functions on almost discrete spaces; \(\bullet\) homeomorphisms on almost discrete spaces; \(\bullet\) continuous functions on trivial spaces; \(\bullet\) homeomorphisms on trivial spaces. These are axiomatized by four logics. Given the already mentioned well-known epistemic logic S5 and given the well-known temporal logic LTL, the elegant way to see these logics is as follows (in order of correspondence): \(\bullet\) S5C = S5 + LTL + \((\bigcirc\square \phi \rightarrow \square \bigcirc \phi)\); \(\bullet\) S5Ct = S5 + LTL + \((\square \phi \rightarrow \square \bigcirc \phi)\); \(\bullet\) S5Ht = S5 + LTL + \((\square \phi \leftrightarrow \square \bigcirc \phi)\); \(\bullet\) S5H = S5 + LTL + \((\bigcirc\square \phi \leftrightarrow \square \bigcirc \phi)\) + \(\bigcirc \phi / \phi\). It is observed -- and it seems worthwhile to repeat this observation -- that there is a strong relation to many-dimensional modal logics: the logic S5C can alternatively be seen as the product of LTL and S5. The continuation and core of the contribution now consists of the completeness proofs for these logics, preceded and interleaved with useful other results: Theorem 2.4.3 shows that \(\text{S5C} \subset \text{S5Ct} \subset \text{S5Ht}\) and \(\text{S5C} \subset \text{S5H} \subset \text{S5Ht}\), and that S5Ct and S5H are incomparable; all four logics are decidable. Looking at Kremer's work from a perspective of dynamic epistemic logic, I am wondering what would happen if we replaced the temporal modalities by dynamic modalities, so that instead of assuming an underlying functional structure interpreting the temporal modalities, such functionality is induced by dynamic operators with internal structure (preconditions or postconditions in terms of open sets), as in, e.g., public announcement logic. I recall ongoing work by \textit{C. Başkent} based on his ILLC MSc in Logic thesis [Topics in subset space logic (2007)], and also recently at AiML 2010 presented ongoing work by \textit{P. Balbiani} and \textit{A. Kudinov}, entitled ``A topological interpretation of public announcement logic'', that may shed some more light on this matter.