In many logics dealing with information one needs to make statements not only about cognitive states, but also about transitions between them. In this paper we analyze a dynamic modal logic that has been designed with this purpose in mind. On top of an abstract information ordering on states it has instructions to move forward or backward along this ordering, to states where a certain assertion holds or fails, while it also allows combinations of such instructions by (...) means of operations from relation algebra. In addition, the logic has devices for expressing whether in a given state a certain instruction can be carried out, and whether that state can be arrived at by carrying out a certain instruction. This paper deals mainly with technical aspects of our dynamic modal logic. It gives an exact description of the expressive power of this language; it also contains results on decidability for the language with 'arbitrary' structures and for the special case with a restricted class of admissible structures. In addition, a complete axiomatization is given. The paper concludes with a remark about the modal algebras appropriate for our dynamic modal logic, and some questions for further work. The paper only contains some sketchy examples showing how the logic can be used to capture situations of dynamic interest, far more detailed applications are given in a companion to this paper (De Rijke [33]). (shrink)

In this dissertation we present proof systems for several modal logics. These proof systems are based on analytic (or semantic) tableaux. -/- Modal logics are logics for reasoning about possibility, knowledge, beliefs, preferences, and other modalities. Their semantics are almost always based on Saul Kripke’s possible world semantics. In Kripke semantics, models are represented by relational structures or, equivalently, labeled graphs. Syntactic formulas that express statements about knowledge and other modalities are evaluated in terms of such models. -/- (...) This dissertation focuses on modal logics with dynamic operators for public announcements, belief revision, preference upgrades, and so on. These operators are defined in terms of mathematical operations on Kripke models. Thus, for example, a belief revision operator in the syntax would correspond to a belief revision operation on models. -/- The ‘dynamic’ semantics of dynamic modal logics are a clever way of extending languages without compromising on intuitiveness. We present ‘dynamic’ tableau proof systems for these dynamic semantics, with the express aim to make them conceptually simple, easy to use, modular, and extensible. This we do by reflecting the semantics as closely as possible in the components of our tableau system. For instance, dynamic operations on Kripke models have counterpart dynamic relations between tableaux. -/- Soundness, completeness, and decidability are three of the most important properties that a proof system may have. A proof system is sound if and only if any formula for which a proof exists, is true in every model. A proof system is complete if and only if for any formula that is true in all models, a proof exists. A proof system is decidable if and only if any formula can be proved to be a theorem or not a theorem in a finite number of steps. All proof systems in this dissertation are sound, complete, and decidable. -/- Part of our strategy to create modular tableau systems is to delay concerns over decidability until after soundness and completeness have been established. Decidability is attained through the operations of folding and through operations on ‘tableau cascades’, which are graphs of tableaux. -/- Finally, we provide a proof-of-concept implementation of our dynamic tableau system for public announcement logic in the Clojure programming language. (shrink)

In many logics dealing with information one needs to make statements not only about cognitive states, but also about transitions between them. In this paper we analyze a dynamic modal logic that has been designed with this purpose in mind. On top of an abstract information ordering on states it has instructions to move forward or backward along this ordering, to states where a certain assertion holds or fails, while it also allows combinations of such instructions by (...) means of operations from relation algebra. In addition, the logic has devices for expressing whether in a given state a certain instruction can be carried out, and whether that state can be arrived at by carrying out a certain instruction.This paper deals mainly with technical aspects of our dynamic modal logic. It gives an exact description of the expressive power of this language; it also contains results on decidability for the language with arbitrary structures and for the special case with a restricted class of admissible structures. In addition, a complete axiomatization is given. The paper concludes with a remark about the modal algebras appropriate for our dynamic modal logic, and some questions for further work. (shrink)

In many logics dealing with information one needs to make statements not only about cognitive states, but also about transitions between them. In this paper we analyze a dynamic modal logic that has been designed with this purpose in mind. On top of an abstract information ordering on states it has instructions to move forward or backward along this ordering, to states where a certain assertion holds or fails, while it also allows combinations of such instructions by (...) means of operations from relation algebra. In addition, the logic has devices for expressing whether in a given state a certain instruction can be carried out, and whether that state can be arrived at by carrying out a certain instruction. (shrink)

Prof. Ruth Barcan Marcus created quantified modal logic in 1946. She extended the Lewis calculus S2 to cover quantification. Quantified modal logic became an essential tool for the rigorous study of natural language in the hands of R. Montague in the late sixties. Some complex phenomena cannot be properly handled at the level of sentences. Recent researches in formal semantics have concentrated on discourse and led to a rich amount of results. Logical theories introduced for the (...) logical study of programs play an important role in these developments. We shall present a detailed account of the connection between dynamic logic and “static” logic. The core of the paper will be the translation of dynamic logic into S5. Developping an insight due to Prof. J. van Eijck, We shall offer a simplified version of the latter translation. The paper also relates to P. Gärdenfors' Knowledge in Flux. (shrink)

abstract. A first-order dynamic epistemic logic is developed where the names of the agents are also terms in the sense of first-order logic. Consequently one can quantify over epistemic modalities. Us- ing constructs from dynamic logic one can express many interesting concepts. First-order update models are developed and added to the language as modalities.

A new modal logic containing four dynamic modalities with the following informal reading is introduced: $${\square^\forall}$$ – always necessary , $${\square^\exists}$$ – sometimes necessary , and their duals – $${\diamondsuit^\forall}$$ – always possibly , and $${\diamondsuit^\exists}$$ – sometimes possibly . We present a complete axiomatization with respect to the intended formal semantics and prove decidability via fmp.

van Bentham et al. (Merging frameworks for interaction: DEL and ETL, 2007) provides a framework for generating the models of Epistemic Temporal Logic ( ETL : Fagin et al., Reasoning about knowledge, 1995; Parikh and Ramanujam, Journal of Logic, Language, and Information, 2003) from the models of Dynamic Epistemic Logic ( DEL : Baltag et al., in: Gilboa (ed.) Tark 1998, 1998; Gerbrandy, Bisimulations on Planet Kripke, 1999). We consider the logic TDEL on the merged (...) semantic framework, and its extension with the labeled past-operator “ P ϵ ” (“The event ϵ has happened before which. . .”). To axiomatize the extension, we introduce a method for transforming a given model into a normal form in a suitable sense. These logics suggest further applications of DEL in the theory of agency, the theory of learning, etc. (shrink)

We prove completeness and decidability results for a family of combinations of propositional dynamic logic and unimodal doxastic logics in which the modalities may interact. The kind of interactions we consider include three forms of commuting axioms, namely, axioms similar to the axiom of perfect recall and the axiom of no learning from temporal logic, and a Church–Rosser axiom. We investigate the influence of the substitution rule on the properties of these logics and propose a new semantics (...) for the test operator to avoid unwanted side effects caused by the interaction of the classic test operator with the extra interaction axioms. (shrink)

A modal logic for translating a sequence of English sentences to a sequence of logical forms is presented, characterized by Kripke models with points formed from input/output sequences, and valuations determined by entailment relations. Previous approaches based (to one degree or another) on Quantified Dynamic Logic are embeddable within it. Applications to presupposition and ambiguity are described, and decision procedures and axiomatizations supplied.

Dynamic Topological Logic ( ) is a modal logic which combines spatial and temporal modalities for reasoning about dynamic topological systems , which are pairs consisting of a topological space X and a continuous function f : X → X . The function f is seen as a change in one unit of time; within one can model the long-term behavior of such systems as f is iterated. One class of dynamic topological systems where (...) the long-term behavior of f is particularly interesting is that of minimal systems ; these are dynamic topological systems which admit no proper, closed, f -invariant subsystems. In such systems the orbit of every point is dense, which within translates into a non-trivial interaction between spatial and temporal modalities. This interaction, however, turns out to make the logic simpler, and while s in general tend to be undecidable, interpreted over minimal systems we obtain decidability, although not in primitive recursive time; this is the main result that we prove in this paper. We also show that interpreted over minimal systems is incomplete for interpretations on relational Kripke frames and hence does not have the finite model property; however it does have a finite non-deterministic quasimodel property. Finally, we give a set of formulas of which characterizes the class of minimal systems within the class of dynamic topological systems, although we do not offer a full axiomatization for the logic. (shrink)

Modal logics, originally conceived in philosophy, have recently found many applications in computer science, artificial intelligence, the foundations of mathematics, linguistics and other disciplines. Celebrated for their good computational behaviour, modal logics are used as effective formalisms for talking about time, space, knowledge, beliefs, actions, obligations, provability, etc. However, the nice computational properties can drastically change if we combine some of these formalisms into a many-dimensional system, say, to reason about knowledge bases developing in time or moving objects. (...) To study the computational behaviour of many-dimensional modal logics is the main aim of this book. On the one hand, it is concerned with providing a solid mathematical foundation for this discipline, while on the other hand, it shows that many seemingly different applied many-dimensional systems (e.g., multi-agent systems, description logics with epistemic, temporal and dynamic operators, spatio-temporal logics, etc.) fit in perfectly with this theoretical framework, and so their computational behaviour can be analyzed using the developed machinery. We start with concrete examples of applied one- and many-dimensional modal logics such as temporal, epistemic, dynamic, description, spatial logics, and various combinations of these. Then we develop a mathematical theory for handling a spectrum of 'abstract' combinations of modal logics - fusions and products of modal logics, fragments of first-order modal and temporal logics - focusing on three major problems: decidability, axiomatizability, and computational complexity. Besides the standard methods of modal logic, the technical toolkit includes the method of quasimodels, mosaics, tilings, reductions to monadic second-order logic, algebraic logic techniques. Finally, we apply the developed machinery and obtained results to three case studies from the field of knowledge representation and reasoning: temporal epistemic logics for reasoning about multi-agent systems, modalized description logics for dynamic ontologies, and spatio-temporal logics. The genre of the book can be defined as a research monograph. It brings the reader to the front line of current research in the field by showing both recent achievements and directions of future investigations (in particular, multiple open problems). On the other hand, well-known results from modal and first-order logic are formulated without proofs and supplied with references to accessible sources. The intended audience of this book is logicians as well as those researchers who use logic in computer science and artificial intelligence. More specific application areas are, e.g., knowledge representation and reasoning, in particular, terminological, temporal and spatial reasoning, or reasoning about agents. And we also believe that researchers from certain other disciplines, say, temporal and spatial databases or geographical information systems, will benefit from this book as well. Key Features: Integrated approach to modern modal and temporal logics and their applications in artificial intelligence and computer science Written by internationally leading researchers in the field of pure and applied logic Combines mathematical theory of modal logic and applications in artificial intelligence and computer science Numerous open problems for further research Well illustrated with pictures and tables. (shrink)

Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let (...) a dynamic topological system be a topological space X together with a continuous function f. f can be thought of in temporal terms, moving the points of the topological space from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality □, and two temporal modalities, ○ and *, both interpreted using the continuous function f. In particular, ○ expresses f’s action on X from one moment to the next, and * expresses the asymptotic behaviour of f. (shrink)

Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let (...) a dynamic topological system be a topological space X together with a continuous function f. f can be thought of in temporal terms, moving the points of the topological space from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality □ , and two temporal modalities, ○ and * , both interpreted using the continuous function f. In particular, ○ expresses f’s action on X from one moment to the next, and * expresses the asymptotic behaviour of f. (shrink)

This essay aims to provide a modal logic for rational intuition. Similarly to treatments of the property of knowledge in epistemic logic, I argue that rational intuition can be codified by a modal operator governed by the modal $\mu$-calculus. Via correspondence results between fixed point modal propositional logic and the bisimulation-invariant fragment of monadic second-order logic, a precise translation can then be provided between the notion of 'intuition-of', i.e., the cognitive phenomenal properties (...) of thoughts, and the modal operators regimenting the notion of 'intuition-that'. I argue that intuition-that can further be shown to entrain conceptual elucidation, by way of figuring as a dynamic-interpretational modality which induces the reinterpretation of both domains of quantification and the intensions and hyperintensions of mathematical concepts that are formalizable in monadic first- and second-order formal languages. Hyperintensionality is countenanced via a topic-sensitive epistemic two-dimensional truthmaker semantics. (shrink)

We investigate the modal logic of stepwise removal of objects, both for its intrinsic interest as a logic of quantification without replacement, and as a pilot study to better understand the complexity jumps between dynamic epistemic logics of model transformations and logics of freely chosen graph changes that get registered in a growing memory. After introducing this logic (MLSR) and its corresponding removal modality, we analyze its expressive power and prove a bisimulation characterization theorem. We (...) then provide a complete Hillbert-style axiomatization for the logic of stepwise removal in a hybrid language enriched with nominals and public announcement operators. Next, we show that model-checking for MLSR is PSPACE-complete, while its satisfiability problem is undecidable. Lastly, we consider an issue of fine-structure: the expressive power gained by adding the stepwise removal modality to fragments of first-order logic. (shrink)

The purpose of this paper is to suggest a formal modelling of metaphors as a lingustic tool capable of conveying meanings from one conceptual space to another. This modelling is done within DDL (dynamic doxastic logic).

We consider modal epistemic and doxastic logics as intuitively inadequate logics of information, and we outline a modal system of the operator being informed that which avoids inconsistency with our intuitive concept of information. The system has modal structure of the normal modal logic K4, and is sound and complete on the class of all transitive frames. We compare this logic with Floridi’s KTB information logic, and we consider a possibility of extending our (...) system to a dynamic logic. (shrink)

Dynamic Topological Logic ( $\mathcal{DTL}$ ) is a modal framework for reasoning about dynamical systems, that is, pairs 〈X, f〉 where X is a topological space and f: X → X a continuous function. In this paper we consider the case where X is a metric space. We first show that any formula which can be satisfied on an arbitrary dynamic topological system can be satisfied on one based on a metric space; in fact, this space (...) can be taken to be countable and have no isolated points. Since any metric space with these properties is homeomorphic to the set of rational numbers, it follows that any satisfiable formula can be satisfied on a system based on $\mathbb{Q}$ . We then show that the situation changes when considering complete metric spaces, by exhibiting a formula which is not valid in general but is valid on the class of systems based on a complete metric space. While we do not attempt to give a full characterization of the set of valid formulas on this class we do give a relative completeness result; any formula which is satisfiable on a dynamical system based on a complete metric space is also satisfied on one based on the Cantor space. (shrink)

A reactive graph generalizes the concept of a graph by making it dynamic, in the sense that the arrows coming out from a point depend on how we got there. This idea was first applied to Kripke semantics of modal logic in [2]. In this paper we strengthen that unimodal language by adding a second operator. One operator corresponds to the dynamics relation and the other one relates paths with the same endpoint. We explore the expressivity of (...) this interpretation by axiomatizing some natural subclasses of reactive frames. The main objective of this paper is to present a methodology to study reactive logics using the existent classic techniques. (shrink)

Transition systems can be viewed either as process diagrams or as Kripke structures. The rst perspective is that of process theory, the second that of modal logic. This paper shows how various formalisms of modal logic can be brought to bear on processes. Notions of bisimulation can not only be motivated by operations on transition systems, but they can also be suggested by investigations of modal formalisms. To show that the equational view of processes from (...) process algebra is closely related to modal logic, we consider various ways of looking at the relation between the calculus of basic process algebra and propositional dynamic logic. More concretely, the paper contains preservation results for various bisimulation notions, a result on the expressive power of propositional dynamic logic, and a de nition of bisimulation which is the proper notion of invariance for concurrent propositional dynamic logic. (shrink)

Let ${{\mathcal L}^{\square\circ}}$ be a propositional language with standard Boolean connectives plus two modalities: an S4-ish topological modality □ and a temporal modality ◦, understood as ‘next’. We extend the topological semantic for S4 to a semantics for the language ${{\mathcal L}^{\square\circ}}$ by interpreting ${{\mathcal L}^{\square\circ}}$ in dynamic topological systems, i.e., ordered pairs 〈X, f〉, where X is a topological space and f is a continuous function on X. Artemov, Davoren and Nerode have axiomatized a logic S4C, and (...) have shown that S4C is sound and complete for this semantics. S4C is also complete for continuous functions on Cantor space (Mints and Zhang, Kremer), and on the real plane (Fernández Duque); but incomplete for continuous functions on the real line (Kremer and Mints, Slavnov). Here we show that S4C is complete for continuous functions on the rational numbers. (shrink)

This book offers a state-of-the-art introduction to the basic techniques and results of neighborhood semantics for modal logic. In addition to presenting the relevant technical background, it highlights both the pitfalls and potential uses of neighborhood models – an interesting class of mathematical structures that were originally introduced to provide a semantics for weak systems of modal logic. In addition, the book discusses a broad range of topics, including standard modal logic results ; bisimulations (...) for neighborhood models and other model-theoretic constructions; comparisons with other semantics for modal logic ; neighborhood semantics for first-order modal logic, applications in game theory ; applications in epistemic logic ; and non-normal modal logics with dynamic modalities. The book can be used as the primary text for seminars on philosophical logic focused on non-normal modal logics; as a supplemental text for courses on modal logic, logic in AI, or philosophical logic ; or as the primary source for researchers interested in learning about the uses of neighborhood semantics in philosophical logic and game theory. (shrink)

The main purpose of the paper is to introduce philosophers and philosophical logicians to dynamic logic, a subject which promises to be of interest also to philosophy. A new completeness result involving both after — and during — operators is announced.

Consider any logical system, what is its natural repertoire of logical operations? This question has been raised in particular for first-order logic and its extensions with generalized quantifiers, and various characterizations in terms of semantic invariance have been proposed. In this paper, our main concern is with modal and dynamic logics. Drawing on previous work on invariance for first-order operations, we find an abstract connection between the kind of logical operations a system uses and the kind of (...) invariance conditions the system respects. This analysis yields (a) a characterization of invariance and safety under bisimulation as natural conditions for logical operations in modal and dynamic logics, and (b) some new transfer results between first-order logic and modal logic. (shrink)

We often have to draw conclusions about states of machines in computer science and about states of knowledge and belief in artificial intelligence based on partial information. Nerode suggested using constructive logic as the language to express such deductions and also suggested designing appropriate intuitionistic Kripke frames to express the partial information. Following this program, Nerode and Wijesekera developed syntax, semantics and completeness for a system of intuitionistic dynamic logic for proving properties of concurrent programs. Like all (...) dynamics logics, this was a logic of many modalities, each expressing a program, but in intuitionistic rather than in classical logic. In that logic, both box and diamond are needed, but these two are not intuitionistically interdefinable and, worse, diamond does not distribute over ‘or’, except for sequential programs. This also happens in other contemplated computer science and AI applications, and leads outside the class of constructive logics investigated in the literature. The present paper fills this gap. We provide intuitionistic logics with independent box and diamond without assuming distribution of diamond over ‘or’. The completeness theorem is based on intuitionistic Kripke frames , but equipped with an additional, quite separate accessibility relation between worlds. In the interpretation of Nerode and Wijesekera , worlds under the partial order represent states of partial knowledge, the accessibility represents change in state of partial knowledge resulting from executing a specific program. But there are many other computer science interpretations. This formalism covers all computer science applications of which we are aware. We also give a cut elimination theorem and algebraic and topological formulations, since these present some new difficulties. Finally, these results were obtained prior to those in Nerode and Wijesekera. (shrink)

This paper is a continuation of the authors' attempts to deal with the notion of indistinguishability (or indiscernibility) from a logical point of view. Now we introduce a two-sorted first-order modal logic to enable us to deal with objects of two different species. The intended interpretation is that objects of one of the species obey the rules of standard S5, while the objects of the other species obey only the rules of a weaker notion of indiscernibility. Quantum mechanics (...) motivates the development. The basic idea is that in the ‘actual’ world things may be indiscernible but in another accessible world they may be distinguished in some way. That is, indistinguishability needs not be seen as a necessary relation. Contrariwise, things might be distinguished in the ‘actual’ world, but they may be indiscernible in another world. So, while two quantum systems may be entangled in the actual world, in some accessible world, due to a measurement, they can be discerned, and on the other hand, two initially separated quantum systems may enter in a state of superposition, losing their individualities. Two semantics are sketched for our system. The first is constructed within a standard set theory (the ZFC system is assumed at the metamathematics). The second one is constructed within the theory of quasi-sets, which we believe suits better the purposes of our logic and the mathematical treatment of certain situations in quantum mechanics. Some further philosophically related topics are considered. (shrink)

Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a (...) class='Hi'>dynamic topological system be a topological space X together wError: Corrupted memory profileError: read ICCBased color space profile errorith a continuous function f. f can be thought of in temporal terms, moving the points of the topological space from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality, and two temporal modalities, and ∗, both interpreted using the continuous function. (shrink)

This paper aims to extend in two directions the probabilistic dynamic epistemic logic provided in Kooi’s paper (J Logic Lang Inform 12(4):381–408, 2003) and to relate these extensions to ones made in van Benthem et al. (Proceedings of LOFT’06. Liverpool, 2006). Kooi’s probabilistic dynamic epistemic logic adds to probabilistic epistemic logic sentences that express consequences of public announcements. The paper (van Benthem et al., Proceedings of LOFT’06. Liverpool, 2006) extends (Kooi, J Logic Lang (...) Inform 12(4):381–408, 2003) to using action models, but in both papers, the probabilities are discrete, and are defined on trivial σ -algebras over finite sample spaces. The first extension offered in this paper is to add a previous-time operator to a probabilistic dynamic epistemic logic similar to Kooi’s in (J Logic Lang Inform 12(4):381–408, 2003). The other is to involve non-trivial σ -algebras and continuous probabilities in probabilistic dynamic epistemic logic. (shrink)

The theories of belief change developed within the AGM-tradition are not logics in the proper sense, but rather informal axiomatic theories of belief change. Instead of characterizing the models of belief and belief change in a formalized object language, the AGM-approach uses a natural language — ordinary mathematical English — to characterize the mathematical structures that are under study. Recently, however, various authors such as Johan van Benthem and Maarten de Rijke have suggested representing doxastic change within a formal logical (...) language: a dynamic modal logic. Inspired by these suggestions Krister Segerberg has developed a very general logical framework for reasoning about doxastic change: dynamic doxastic logic (DDL). This framework may be seen as an extension of standard Hintikka-style doxastic logic with dynamic operators representing various kinds of transformations of the agent's doxastic state. Basic DDL describes an agent that has opinions about the external world and an ability to change these opinions in the light of new information. Such an agent is non-introspective in the sense that he lacks opinions about his own belief states. Here we are going to discuss various possibilities for developing a dynamic doxastic logic for introspective agents: full DDL or DDL unlimited. The project of constructing such a logic is faced with difficulties due to the fact that the agent’s own doxastic state now becomes a part of the reality that he is trying to explore: when an introspective agent learns more about the world, then the reality he holds beliefs about undergoes a change. But then his introspective (higher-order) beliefs have to be adjusted accordingly. In the paper we shall consider various ways of solving this problem. (shrink)

This paper introduces Agreement Theorems to dynamic-epistemic logic. We show first that common belief of posteriors is sufficient for agreement in epistemic-plausibility models, under common and well-founded priors. We do not restrict ourselves to the finite case, showing that in countable structures the results hold if and only if the underlying plausibility ordering is well-founded. We then show that neither well-foundedness nor common priors are expressible in the language commonly used to describe and reason about epistemic-plausibility models. The (...) static agreement result is, however, finitely derivable in an extended modal logic. We provide the full derivation. We finally consider dynamic agreement results. We show they have a counterpart in epistemic-plausibility models, and provide a new form of agreements via public announcements. (shrink)

We introduce quantificational modal operators as dynamic modalities with (extensions of) Henkin quantifiers as indices. The adoption of matrices of indices (with action identifiers, variables and/or quantified variables as entries) gives an expressive formalism which is here motivated with examples from the area of multi-agent systems. We study the formal properties of the resulting logic which, formally speaking, does not satisfy the normality condition. However, the logic admits a semantics in terms of (an extension of) Kripke (...) structures. As a consequence, standard techniques for normal modal logic become available. We apply these to prove completeness and decidability, and to extend some standard frame results to this logic. (shrink)

This paper brings together Dana Scottʼs measure-based semantics for the propositional modal logic S4, and recent work in Dynamic Topological Logic. In a series of recent talks, Scott showed that the language of S4 can be interpreted in the Lebesgue measure algebra, M, or algebra of Borel subsets of the real interval, [0,1], modulo sets of measure zero. Conjunctions, disjunctions and negations are interpreted via the Boolean structure of the algebra, and we add an interior operator (...) on M that interprets the □-modality. In this paper we show how to extend this measure-based semantics to the bimodal logic S4C. S4C is interpreted in ‘dynamic topological systems,’ or topological spaces together with a continuous function acting on the space. We extend Scottʼs measure based semantics to this bimodal logic by defining a class of operators on the algebra M, which we call O-operators and which take the place of continuous functions in the topological semantics for S4C. The main result of the paper is that S4C is complete for the Lebesgue measure algebra. A strengthening of this result, also proved here, is that there is a single measure-based model in which all non-theorems of S4C are refuted. (shrink)

Let $\mathcal{L}$ be a propositional language with standard Boolean connectives plus two modalities: an S4-ish topological modality $\square$ and a temporal modality $\bigcirc$ , understood as ‘next’. We extend the topological semantic for S4 to a semantics for the language $\mathcal{L}$ by interpreting $\mathcal{L}$ in dynamic topological systems, i.e. ordered pairs $\langle X, f\rangle$ , where X is a topological space and f is a continuous function on X. Artemov, Davoren and Nerode have axiomatized a logic S4C, and (...) have shown that S4C is sound and complete for this semantics. Zhang and Mints have shown that S4C is complete relative to a particular topological space, Cantor space. The current paper produces an alternate proof of the Zhang-Mints result. (shrink)

We consider a syntax and semantics of modal logics based on parametrized modal connectives with \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\exists \forall $$\end{document}-satisfaction definitions, we axiomatically introduce different parametrized modal logics, we prove their completeness with respect to appropriate classes of parametrized relational structures and we show the decidability of some related satisfiability problems.

We define a family of intuitionistic non-normal modal logics; they can be seen as intuitionistic counterparts of classical ones. We first consider monomodal logics, which contain only Necessity or Possibility. We then consider the more important case of bimodal logics, which contain both modal operators. In this case we define several interactions between Necessity and Possibility of increasing strength, although weaker than duality. We thereby obtain a lattice of 24 distinct bimodal logics. For all logics we provide both (...) a Hilbert axiomatisation and a cut-free sequent calculus, on its basis we also prove their decidability. We then define a semantic characterisation of our logics in terms of neighbourhood models containing two distinct neighbourhood functions corresponding to the two modalities. Our semantic framework captures modularly not only our systems but also already known intuitionistic non-normal modal logics such as Constructive K and the propositional fragment of Wijesekera’s Constructive Concurrent Dynamic Logic. (shrink)