ABSTRACT George Gargov was an active pioneer in the ‘Sofia School’ of modal logicians. Starting in the 1970s, he and his colleagues expanded the scope of the subject by introducing new modal expressive power, of various innovative kinds. The aim of this paper is to show some general patterns behind such extensions, and review some very general results that we know by now, 20 years later. We concentrate on simulation invariance, decidability, and correspondence. What seems clear is that ‘modal logic’ (...) as a genre of logical systems has a much wider scope than originally conceived, and that we have not reached its limits yet. (shrink)

This paper deals with two main topics: One is a semantical investigation for a bimodal language with a modal operator \blacksquare associated with the intersection of the accessibility relation R and the inequality ≠. The other is a generalization of some of the former results to general extended languages with modal operators. First, for our language L\sb{\square\blacksquare}, we prove that Segerberg's theorem (equivalence between finite frame property and finite model property) fails and establish both van Benthem-style and Goldblatt-Thomason-style characterizations. We (...) extract the notion of \blacksquare-realizer (a generalization of bulldozing) as an essence from the proofs of our results. Second, we generalize the notion of \blacksquare-realizer and prove quite general versions of these semantical characterization results. The known and previously unknown characterization results for almost all of the languages extended with modal operators already proposed will be immediate corollaries. (shrink)

We prove an existential analogue of the Goldblatt‐Thomason Theorem which characterizes modal definability of elementary classes of Kripke frames using closure under model theoretic constructions. The less known version of the Goldblatt‐Thomason Theorem gives general conditions, without the assumption of first‐order definability, but uses non‐standard constructions and algebraic semantics. We present a non‐algebraic proof of this result and we prove an analogous characterization for an alternative notion of modal definability, in which a class is defined by formulas which are satisfiable (...) under any valuation (the so‐called existential validity). Continuing previous work in which model theoretic characterization for this type of definability of elementary classes was proved, we give an analogous general result without the assumption of the first‐order definability. Furthermore, we outline relationships between sets of existentially valid formulas corresponding to several well‐known modal logics. (shrink)

Adam Brandenburger and H. Jerome Keisler have recently discovered a two person Russell-style paradox. They show that the following configurations of beliefs is impossible: Ann believes that Bob assumes that Ann believes that Bob’s assumption is wrong. In [7] a modal logic interpretation of this paradox is proposed. The idea is to introduce two modal operators intended to represent the agents’ beliefs and assumptions. The goal of this paper is to take this analysis further and study this paradox from the (...) point of view of a modal logician. In particular, we show that the paradox can be seen as a theorem of an appropriate hybrid logic. (shrink)

We investigate transfer of interpolation in such combinations of modal logic which lead to interaction of the modalities. Combining logics by taking products often blocks transfer of interpolation. The same holds for combinations by taking unions, a generalization of Humberstone's inaccessibility logic. Viewing first-order logic as a product of modal logics, we derive a strong counterexample for failure of interpolation in the finite variable fragments of first-order logic. We provide a simple condition stated only in terms of frames and bisimulations (...) which implies failure of interpolation. Its use is exemplified in a wide range of cases. (shrink)

Propositional dynamic logic (PDL) is one of the most successful variants of modal logic. To make it even more useful for applications, many extensions of PDL have been considered in the literature. A very natural and useful such extension is with negation of programs. Unfortunately, as long-known, reasoning with the resulting logic is undecidable. In this paper, we consider the extension of PDL with negation of atomic programs, only. We argue that this logic is still useful, e.g. in the context (...) of description logics, and prove that satisfiability is decidable and EXPTIME-complete using an approach based on Büchi tree automata. (shrink)

In this paper, using a propositional modal language extended with the window modality, we capture the first-order properties of various mereological theories. In this setting, $\Box \varphi $ reads all the parts (of the current object) are $\varphi $, interpreted on the models with a whole-part binary relation under various constraints. We show that all the usual mereological theories can be captured by modal formulas in our language via frame correspondence. We also correct a mistake in the existing completeness proof (...) for a basic system of mereology by providing a new construction of the canonical model. (shrink)

Viewing the language of modal logic as a language for describing directed graphs, a natural type of directed graph to study modally is one where the nodes are sets and the edge relation is the subset or superset relation. A well-known example from the literature on intuitionistic logic is the class of Medvedev frames $\langle W,R\rangle$ where $W$ is the set of nonempty subsets of some nonempty finite set $S$, and $xRy$ iff $x\supseteq y$, or more liberally, where $\langle W,R\rangle$ (...) is isomorphic as a directed graph to $\langle \wp(S)\setminus\{\emptyset\},\supseteq\rangle$. Prucnal [32] proved that the modal logic of Medvedev frames is not finitely axiomatizable. Here we continue the study of Medvedev frames with extended modal languages. Our results concern definability. We show that the class of Medvedev frames is definable by a formula in the language of tense logic, i.e., with a converse modality for quantifying over supersets in Medvedev frames, extended with any one of the following standard devices: nominals (for naming nodes), a difference modality (for quantifying over those $y$ such that $x\not= y$), or a complement modality (for quantifying over those $y$ such that $x\not\supseteq y$). It follows that either the logic of Medvedev frames in one of these tense languages is finitely axiomatizable---which would answer the open question of whether Medvedev's [31] "logic of finite problems'' is decidable---or else the minimal logics in these languages extended with our defining formulas are the beginnings of infinite sequences of frame-incomplete logics. (shrink)

We investigate an enrichment of the propositional modal language L with a "universal" modality ■ having semantics x ⊧ ■φ iff ∀y(y ⊧ φ), and a countable set of "names" - a special kind of propositional variables ranging over singleton sets of worlds. The obtained language ℒ $_{c}$ proves to have a great expressive power. It is equivalent with respect to modal definability to another enrichment ℒ(⍯) of ℒ, where ⍯ is an additional modality with the semantics x ⊧ ⍯φ (...) iff Vy(y ≠ x → y ⊧ φ). Model-theoretic characterizations of modal definability in these languages are obtained. Further we consider deductive systems in ℒ $_{c}$ . Strong completeness of the normal ℒ $_{c}$ logics is proved with respect to models in which all worlds are named. Every ℒ $_{c}$ -logic axiomatized by formulae containing only names (but not propositional variables) is proved to be strongly frame-complete. Problems concerning transfer of properties ([in]completeness, filtration, finite model property etc.) from ℒ to ℒ $_{c}$ are discussed. Finally, further perspectives for names in multimodal environment are briefly sketched. (shrink)

We describe a relational framework that uniformly supports formalization and automated reasoning in varied propositional modal logics. The proof system we propose is a relational variant of the classical Rasiowa-Sikorski proof system. We introduce a compact graph-based representation of formulae and proofs supporting an efficient implementation of the basic inference engine, as well as of a number of refinements. Completeness and soundness results are shown and a Prolog implementation is described.

Following the theory of Boolean algebras with modal operators , in this paper we investigate Boolean algebras with sufficiency operators and mixed operators . We present results concerning representability, generation by finite members, first order axiomatisability, possession of a discriminator term etc. We generalise the classes BAO, SUA, and MIA to classes of algebras with the families of relative operators. We present examples of the discussed classes of algebras that arise in connection with reasoning with incomplete information.

We consider some modal languages with a modal operator $D$ whose semantics is based on the relation of inequality. Basic logical properties such as definability, expressive power and completeness are studied. Also, some connections with a number of other recent proposals to extend the standard modal language are pointed at.

ABSTRACT George Gargov was an active pioneer in the ‘Sofia School’ of modal logicians. Starting in the 1970s, he and his colleagues expanded the scope of the subject by introducing new modal expressive power, of various innovative kinds. The aim of this paper is to show some general patterns behind such extensions, and review some very general results that we know by now, 20 years later. We concentrate on simulation invariance, decidability, and correspondence. What seems clear is that ‘modal logic’ (...) as a genre of logical systems has a much wider scope than originally conceived, and that we have not reached its limits yet. (shrink)

Over the last twenty years, in all of these neighbouring fields, modal systems have been developed that we call multi-dimensional. (Our definition of multi ...