We consider second-order propositional modal logic (SOPML), an extension of the basic modal language with propositional quantifiers introduced by Kit Fine in 1970. We determine the precise expressive power of SOPML by giving analogues of the Van Benthem–Rosen theorem and the Goldblatt Thomason theorem. Furthermore, we show that the basic modal language is the bisimulation invariant fragment of SOPML, and we characterize the bounded fragment of first-order logic as being the intersection of first-order logic and SOPML.

We explore the finite model theory of the characterisation theorems for modal and guarded fragments of first-order logic over transition systems and relational structures of width two. A new construction of locally acyclic bisimilar covers provides a useful analogue of the well known tree-like unravellings that can be used for the purposes of finite model theory. Together with various other finitary bisimulation respecting model transformations, and Ehrenfeucht–Fraïssé game arguments, these covers allow us to upgrade finite approximations for full bisimulation equivalence (...) towards approximations for elementary equivalence. These techniques are used to prove several ramifications of the van Benthem–Rosen characterisation theorem of basic modal logic for refinements of ordinary bisimulation equivalence, both in the sense of classical and of finite model theory. (shrink)

We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem’s theorem, which says that a first-order formula is invariant under bisimulation if, and only if, it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes (...) that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes–for instance, rooted frames, finite rooted frames, finite transitive frames, well-founded transitive frames, finite equivalence frames–as these are not elementary. Instead we develop and extend the game-based analysis over such classes and provide bisimulation preserving model constructions within these classes. Over most of the classes considered, we obtain finite model theory analogues of the classically expected characterisations, with new proofs also for the classical setting. The class of transitive frames is a notable exception, with a marked difference between the classical and the finite model theory of bisimulation invariant first-order properties. Over the class of all finite transitive frames in particular, we find that monadic second-order logic is no more expressive than first-order as far as bisimulation invariant properties are concerned — though both are more expressive here than basic modal logic. We obtain ramifications of the de Jongh–Sambin theorem and a new and specific analogue of the Janin–Walukiewicz characterisation of bisimulation invariant monadic second-order for finite transitive frames. (shrink)

Inquisitive modal logic, InqML, is a generalisation of standard Kripke-style modal logic. In its epistemic incarnation, it extends standard epistemic logic to capture not just the information that agents have, but also the questions that they are interested in. Technically, InqML fits within the family of logics based on team semantics. From a model-theoretic perspective, it takes us a step in the direction of monadic second-order logic, as inquisitive modal operators involve quantification over sets of worlds. We introduce and investigate (...) the natural notion of bisimulation equivalence in the setting of InqML. We compare the expressiveness of InqML and first-order logic in the context of relational structures with two sorts, one for worlds and one for information states, and characterise inquisitive modal logic as the bisimulation invariant fragment of first-order logic over various natural classes of two-sorted structures. (shrink)

This book illustrates the program of Logical-Informational Dynamics. Rational agents exploit the information available in the world in delicate ways, adopt a wide range of epistemic attitudes, and in that process, constantly change the world itself. Logical-Informational Dynamics is about logical systems putting such activities at center stage, focusing on the events by which we acquire information and change attitudes. Its contributions show many current logics of information and change at work, often in multi-agent settings where social behavior is essential, (...) and often stressing Johan van Benthem's pioneering work in establishing this program. However, this is not a Festschrift, but a rich tapestry for a field with a wealth of strands of its own. The reader will see the state of the art in such topics as information update, belief change, preference, learning over time, and strategic interaction in games. Moreover, no tight boundary has been enforced, and some chapters add more general mathematical or philosophical foundations or links to current trends in computer science. The theme of this book lies at the interface of many disciplines. Logic is the main methodology, but the various chapters cross easily between mathematics, computer science, philosophy, linguistics, cognitive and social sciences, while also ranging from pure theory to empirical work. Accordingly, the authors of this book represent a wide variety of original thinkers from different research communities. And their interconnected themes challenge at the same time how we think of logic, philosophy and computation. Thus, very much in line with van Benthem's work over many decades, the volume shows how all these disciplines form a natural unity in the perspective of dynamic logicians (broadly conceived) exploring their new themes today. And at the same time, in doing so, it offers a broader conception of logic with a certain grandeur, moving its horizons beyond the traditional study of consequence relations. (shrink)

In this article, we present a modal logic that extends the basic modal logic with two dynamic operators: copy ( ), which replicates the current model, labelling each copy with a different propositional symbol and respecting accessibility relations even between distinct copies; and remove ( ), which deletes paths in the model that satisfy certain intermediate conditions. We call the resulting logic. We study its computational complexity, and its relative expressivity with respect to (static) modal logics and, and the dynamic (...) epistemic Action Model Logic,. (shrink)

How can we prove that some fragment of a given logic has the power to define precisely all structural properties that satisfy some characteristic semantic preservation condition? This issue is a fundamental one for classical model theory and applications in non-classical settings alike. While methods differ greatly, and while the classical methods can usually not be matched for instance in the setting of finite model theory, this note surveys some interesting commonality revolving around the use and availability of tractable representatives (...) in the relevant model classes. The construction of models in which simple invariants like partial types based on some weak fragment control all the relevant structural properties, may be seen at the heart of such questions. We highlight some constructions involving degrees of acyclicity and saturation that can be achieved in finite model constructions, and discuss their uses towards expressive completeness w.r.t. bisimulation based equivalences in hypergraphs and relational structures. The emphasis is on the combinatorial challenges in such more constructive approaches that work in non-classical settings and especially in finite model theory. One new result concerns expressive completeness w.r.t. guarded negation bisimulation, a back-and-forth equivalence involving local homomorphisms. (shrink)

The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this (...) article we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics. (shrink)