We consider two topological interpretations of the modal diamond—as the closure operator (C-semantics) and as the derived set operator (d-semantics). We call the logics arising from these interpretations C-logics and d-logics, respectively. We axiomatize a number of subclasses of the class of nodec spaces with respect to both semantics, and characterize exactly which of these classes are modally definable. It is demonstrated that the d-semantics is more expressive than the C-semantics. In particular, we show that the d-logics of the six (...) classes of spaces considered in the paper are pairwise distinct, while the C-logics of some of them coincide. (shrink)

We prove that each countable rooted K4 -frame is a d-morphic image of a subspace of the space $\mathbb{Q}$ of rational numbers. From this we derive that each modal logic over K4 axiomatizable by variable-free formulas is the d-logic of a subspace of $\mathbb{Q}$ . It follows that subspaces of $\mathbb{Q}$ give rise to continuum many d-logics over K4 , continuum many of which are neither finitely axiomatizable nor decidable. In addition, we exhibit several families of modal logics finitely axiomatizable (...) by variable-free formulas over K4 that d-define interesting classes of topological spaces. Each of these logics has the finite model property and is decidable. Finally, we introduce quasi-scattered and semi-scattered spaces as generalizations of scattered spaces, develop their basic properties, axiomatize their corresponding modal logics, and show that they also arise as the d-logics of some subspaces of $\mathbb{Q}$. (shrink)

ABSTRACT The paper studies propositional logics in a bimodal language, in which the first modality is interpreted as the local truth, and the second as the universal truth. The logic S4UC is introduced, which is finitely axiomatizable, has the f.m.p. and is determined by every connected separable metric space.

The completeness of the modal logic S4 for all topological spaces as well as for the real line, the n-dimensional Euclidean space and the segment etc. was proved by McKinsey and Tarski in 1944. Several simplified proofs contain gaps. A new proof presented here combines the ideas published later by G. Mints and M. Aiello, J. van Benthem, G. Bezhanishvili with a further simplification. The proof strategy is to embed a finite rooted Kripke structure for S4 into a subspace of (...) the Cantor space which in turn encodes. This provides an open and continuous map from onto the topological space corresponding to. The completeness follows as S4 is complete with respect to the class of all finite rooted Kripke structures. (shrink)

The completeness of the modal logic S4 for all topological spaces as well as for the real line , the n-dimensional Euclidean space and the segment etc. was proved by McKinsey and Tarski in 1944. Several simplified proofs contain gaps. A new proof presented here combines the ideas published later by G. Mints and M. Aiello, J. van Benthem, G. Bezhanishvili with a further simplification. The proof strategy is to embed a finite rooted Kripke structure for S4 into a subspace (...) of the Cantor space which in turn encodes . This provides an open and continuous map from onto the topological space corresponding to . The completeness follows as S4 is complete with respect to the class of all finite rooted Kripke structures. (shrink)

In the topological semantics for modal logic, S4 is well-known to be complete for the rational line, for the real line, and for Cantor space: these are special cases of S4’s completeness for any dense-in-itself metric space. The construction used to prove completeness can be slightly amended to show that S4 is not only complete, but also strongly complete, for the rational line. But no similarly easy amendment is available for the real line or for Cantor space and the question (...) of strong completeness for these spaces has remained open, together with the more general question of strong completeness for any dense-in-itself metric space. In this paper, we prove that S4 is strongly complete for any dense-in-itself metric space. (shrink)

The tangle modality is a propositional connective that extends basic modal logic to a language that is expressively equivalent over certain classes of finite frames to the bisimulation-invariant fragments of both first-order and monadic second-order logic. This paper axiomatises several logics with tangle, including some that have the universal modality, and shows that they have the finite model property for Kripke frame semantics. The logics are specified by a variety of conditions on their validating frames, including local and global connectedness (...) properties. Some of the results have been used to obtain completeness theorems for interpretations of tangled modal logics in topological spaces. (shrink)

We show that given a finite, transitive and reflexive Kripke model 〈 W , ≼, ⟦ ⋅ ⟧ 〉 and $${w \in W}$$ , the property of being simulated by w (i.e., lying on the image of a literalpreserving relation satisfying the ‘forth’ condition of bisimulation) is modally undefinable within the class of S4 Kripke models. Note the contrast to the fact that lying in the image of w under a bi simulation is definable in the standard modal language even (...) over the class of K4 models, a fairly standard result for which we also provide a proof. We then propose a minor extension of the language adding a sequent operator $${\natural}$$ (‘tangle’) which can be interpreted over Kripke models as well as over topological spaces. Over finite Kripke models it indicates the existence of clusters satisfying a specified set of formulas, very similar to an operator introduced by Dawar and Otto. In the extended language $${{\sf L}^+ = {\sf L}^{\square\natural}}$$ , being simulated by a point on a finite transitive Kripke model becomes definable, both over the class of (arbitrary) Kripke models and over the class of topological S4 models. As a consequence of this we obtain the result that any class of finite, transitive models over finitely many propositional variables which is closed under simulability is also definable in L + , as well as Boolean combinations of these classes. From this it follows that the μ -calculus interpreted over any such class of models is decidable. (shrink)

Dynamic Topological Logic (DFH) is a multimodal system for reasoning about dynamical systems. It is defined semantically and, as such, most of the work done in the field has been model-theoretic. In particular, the problem of finding a complete axiomatization for the full language of DFH over the class of all dynamical systems has proven to be quite elusive. Here we propose to enrich the language to include a polyadic topological modality, originally introduced by Dawar and Otto in a different (...) context. We then provide a sound axiomatization for DFH over this extended language, and prove that it is complete. The polyadic modality is used in an essential way in our proof. (shrink)

In the pioneering article and two papers, written jointly with McKinsey, Tarski developed the so-called algebraic and topological frameworks for the Intuitionistic Logic and the Lewis modal system. In this paper, we present an outline of modern systems with a topological tinge. We consider topological interpretation of basic systems GL and G of the provability logic in terms of the Cantor derivative and the Hausdorff residue.