The paper studies many-dimensional modal logics corresponding to products of Kripke frames. It proves results on axiomatisability, the finite model property and decidability for product logics, by applying a rather elaborated modal logic technique: p-morphisms, the finite depth method, normal forms, filtrations. Applications to first order predicate logics are considered too. The introduction and the conclusion contain a discussion of many related results and open problems in the area.

In the first part of this paper we introduced products of modal logics and proved basic results on their axiomatisability and the f.m.p. In this continuation paper we prove a stronger result - the product f.m.p. holds for products of modal logics in which some of the modalities are reflexive or serial. This theorem is applied in classical first-order logic, we identify a new Square Fragment of the classical logic, where the basic predicates are (...) binary and all quantifiers are relativised, and for which we show the f.m.p. in the classical sense. Also we prove that SF not included in Guarded Fragment and that it can be embedded into the equational theory of relational algebras. (shrink)

In this paper we improve the results of [2] by proving the product f.m.p. for the product of minimal n-modal and minimal n-temporal logic. For this case we modify the finite depth method introduced in [1]. The main result is applied to identify new fragments of classical first-order logic and of the equational theory of relation algebras, that are decidable and have the finite model property.

The simplest bimodal combination of unimodal logics \ and \ is their fusion, \, axiomatized by the theorems of \ for \ and of \ for \, and the rules of modus ponens, necessitation for \ and for \, and substitution. Shehtman introduced the frame product \, as the logic of the products of certain Kripke frames: these logics are two-dimensional as well as bimodal. Van Benthem, Bezhanishvili, ten Cate and Sarenac transposed Shehtman’s idea to the topological (...) semantics and introduced the topological product \, as the logic of the products of certain topological spaces. For almost all well-studies logics, we have \, for example, \. Van Benthem et al. show, by contrast, that \. It is straightforward to define the product of a topological space and a frame: the result is a topologized frame, i.e., a set together with a topology and a binary relation. In this paper, we introduce topological-frame products \ of modal logics, providing a complete axiomatization of \, whenever \ is a Kripke complete Horn axiomatizable extension of the modal logic D: these extensions include \ and \, but not \ or \. We leave open the problem of axiomatizing \, \, and other related logics. When \, our result confirms a conjecture of van Benthem et al. concerning the logic of products of Alexandrov spaces with arbitrary topological spaces. (shrink)

The simplest combination of unimodal logics \ into a bimodal logic is their fusion, \, axiomatized by the theorems of \. Shehtman introduced combinations that are not only bimodal, but two-dimensional: he defined 2-d Cartesian products of 1-d Kripke frames, using these Cartesian products to define the frame product \. Van Benthem, Bezhanishvili, ten Cate and Sarenac generalized Shehtman’s idea and introduced the topological product \, using Cartesian products of topological spaces rather than of Kripke frames. (...) Frame products have been extensively studied, but much less is known about topological products. The goal of the current paper is to give necessary and sufficient conditions for the topological product to match the frame product, for Kripke complete extensions of \. (shrink)

We show that—unlike products of ‘transitive’ modal logics which are usually undecidable—their ‘expanding domain’ relativisations can be decidable, though not in primitive recursive time. In particular, we prove the decidability and the finite expanding product model property of bimodal logics interpreted in two-dimensional structures where one component—call it the ‘flow of time’—is • a finite linear order or a finite transitive tree and the other is composed of structures like • transitive trees/partial orders/quasi-orders/linear orders or only (...) finite such structures expanding over time. The decidability proof is based on Kruskal’s tree theorem, and the proof of non-primitive recursiveness is by reduction of the reachability problem for lossy channel systems. The result is used to show that the dynamic topological logic interpreted in topological spaces with continuous functions is decidable if the number of function iterations is assumed to be finite. (shrink)

Unifiability of terms (and formulas) and structural completeness in the variety of relation algebras RA and in the products of modal logic S5 is investigated. Nonunifiable terms (formulas) which are satisfiable in varieties (in logics) are exhibited. Consequently, RA and products of S5 as well as representable diagonal-free n-dimensional cylindric algebras, RDfn, are almost structurally complete but not structurally complete. In case of S5n a basis for admissible rules and the form of all passive rules are (...) provided. (shrink)

This work introduces a two-dimensional modal logic to represent agents' Concurrent Common Knowledge in distributed systems. Unlike Common Knowledge, Concurrent Common Knowledge is a kind of agreement reachable in asynchronous environments. The formalization of such type of knowledge is based on a model for asynchronous systems and on the definition of Concurrent Knowledge introduced before in paper [5]. As a proper semantics, we review our concept of closed sub-product of modal logics which is based on the product (...) of modal logics. The key idea is to reason about Concurrent Knowledge under a two-dimensional approach, regarding asynchronous runs and consistent global states as dimensions. We present an axiomatic system for the logic and issue the corresponding soundness and completeness proofs. (shrink)

This paper sets out a new way of combining Kripke-complete modal logics: lexicographic product. It discusses some basic properties of the lexicographic product construction and proves axiomatization/completeness results.

We solve a major open problem concerning algorithmic properties of products of ‘transitive’ modal logics by showing that products and commutators of such standard logics as K4, S4, S4.1, K4.3, GL, or Grz are undecidable and do not have the finite model property. More generally, we prove that no Kripke complete extension of the commutator [K4,K4] with product frames of arbitrary finite or infinite depth (with respect to both accessibility relations) can be decidable. In particular, (...) if. (shrink)

We solve a major open problem concerning algorithmic properties of products of ‘transitive’ modal logics by showing that products and commutators of such standard logics asK4,S4,S4.1,K4.3,GL, orGrzare undecidable and do not have the finite model property. More generally, we prove that no Kripke complete extension of the commutator [K4, K4] with product frames of arbitrary finite or infinite depth (with respect to both accessibility relations) can be decidable. In particular, ifl1andl2are classes of transitive frames such (...) that their depth cannot be bounded by any fixedn< ω, then the logic of the class {5ℑ1× ℑ2∣ ℑ1∈l1, ℑ2, ∈l2} is undecidable. (On the contrary, the product of, say,K4and the logic of all transitive Kripke frames of depth ≤n, for some fixedn< ω, is decidable.) The complexity of these undecidable logics ranges from r.e. to co-r.e. and Π11-complete. As a consequence, we give the first known examples of Kripke incomplete commutators of Kripke complete logics. (shrink)

In the propositional modal treatment of two-variable first-order logic equality is modelled by a ‘diagonal’ constant, interpreted in square products of universal frames as the identity relation. Here we study the decision problem of products of two arbitrary modal logics equipped with such a diagonal. As the presence or absence of equality in two-variable first-order logic does not influence the complexity of its satisfiability problem, one might expect that adding a diagonal to product logics (...) in general is similarly harmless. We show that this is far from being the case, and there can be quite a big jump in complexity, even from decidable to the highly undecidable. Our undecidable logics can also be viewed as new fragments of first-order logic where adding equality changes a decidable fragment to undecidable. We prove our results by a novel application of counter machine problems. While our formalism apparently cannot force reliable counter machine computations directly, the presence of a unique diagonal in the models makes it possible to encode both lossy and insertion-error computations, for the same sequence of instructions. We show that, given such a pair of faulty computations, it is then possible to reconstruct a reliable run from them. (shrink)

We introduce the horizontal and vertical topologies on the product of topological spaces, and study their relationship with the standard product topology. We show that the modal logic of products of topological spaces with horizontal and vertical topologies is the fusion S4 ⊕ S4. We axiomatize the modal logic of products of spaces with horizontal, vertical, and standard product topologies.We prove that both of these logics are complete for the product of rational numbers ℚ × (...) ℚ with the appropriate topologies. (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)

We introduce the horizontal and vertical topologies on the product of topological spaces, and study their relationship with the standard product topology. We show that the modal logic of products of topological spaces with horizontal and vertical topologies is the fusion ${\bf S4}\oplus {\bf S4}$ . We axiomatize the modal logic of products of spaces with horizontal, vertical, and standard product topologies. We prove that both of these logics are complete for the product of rational (...) numbers ${\Bbb Q}\times {\Bbb Q}$ with the appropriate topologies. (shrink)

We introduce the horizontal and vertical topologies on the product of topological spaces, and study their relationship with the standard product topology. We show that the modal logic of products of topological spaces with horizontal and vertical topologies is the fusion S4 ⊕ S4. We axiomatize the modal logic of products of spaces with horizontal, vertical, and standard product topologies.We prove that both of these logics are complete for the product of rational numbers ℚ × (...) ℚ with the appropriate topologies. (shrink)

We prove that everyn-modal logic betweenKnandS5nis undecidable, whenever n ≥ 3. We also show that each of these logics is non-finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic. These results answer several questions of Gabbay and Shehtman. The proofs combine the modal logic technique of Yankov–Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, and give a reduction of the representation problem (...) of finite relation algebras. (shrink)

In this work we study the decidability of a class of global modal logics arising from Kripke frames evaluated over certain residuated lattices, known in the literature as modal many-valued logics. We exhibit a large family of these modal logics which are undecidable, in contrast with classical modal logic and propositional logics defined over the same classes of algebras. This family includes the global modal logics arising from Kripke frames evaluated (...) over the standard Łukasiewicz and Product algebras. We later refine the previous result, and prove that global modal Łukasiewicz and Product logics are not even recursively axiomatizable. We conclude by closing negatively the open question of whether each global modal logic coincides with its local modal logic closed under the unrestricted necessitation rule. (shrink)

We prove that everyn-modal logic betweenKnandS5nis undecidable, whenever n ≥ 3. We also show that each of these logics is non-finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic. These results answer several questions of Gabbay and Shehtman. The proofs combine the modal logic technique of Yankov–Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, and give a reduction of the representation problem (...) of finite relation algebras. (shrink)

We prove that everyn-modal logic betweenKnandS5nis undecidable, whenever n ≥ 3. We also show that each of these logics is non-finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic. These results answer several questions of Gabbay and Shehtman. The proofs combine the modal logic technique of Yankov–Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, and give a reduction of the (undecidable) representation (...) problem of finite relation algebras. (shrink)

We prove that every n-modal logic between K n and S5 n is undecidable, whenever n ≥ 3. We also show that each of these logics is non- finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic. These results answer several questions of Gabbay and Shehtman. The proofs combine the modal logic technique of Yankov-Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, (...) and give a reduction of the (undecidable) representation problem of finite relation algebras. (shrink)

We introduce the horizontal and vertical topologies on the product of topological spaces, and study their relationship with the standard product topology. We show that the modal logic of products of topological spaces with horizontal and vertical topologies is the fusion S4 ⊕ S4. We axiomatize the modal logic of products of spaces with horizontal, vertical, and standard product topologies.We prove that both of these logics are complete for the product of rational numbers ℚ × (...) ℚ with the appropriate topologies. (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)

We investigate the expressivity of many-valued modal logics based on an algebraic structure with a complete linearly ordered lattice reduct. Necessary and sufficient algebraic conditions for admitting a suitable Hennessy–Milner property are established for classes of image-finite and modally saturated models. Full characterizations are obtained for many-valued modal logics based on complete BL-chains that are finite or have the real unit interval [0, 1] as a lattice reduct, including Łukasiewicz, Gödel, and product modal logics.

The paper generalises Goldblatt's completeness proof for Lemmon–Scott formulas to various modal propositional logics without classical negation and without ex falso, up to positive modal logic, where conjunction and disjunction, andwhere necessity and possibility are respectively independent.Further the paper proves definability theorems for Lemmon–Scottformulas, which hold even in modal propositional languages without negation and without falsum. Both, the completeness theorem and the definability theoremmake use only of special constructions of relations,like relation products. No second order (...) logic, no general frames are involved. (shrink)

Shehtman introduced bimodal logics of the products of Kripke frames, thereby introducing frame products of unimodal logics. Van Benthem, Bezhanishvili, ten Cate and Sarenac generalize this idea to the bimodal logics of the products of topological spaces, thereby introducing topological products of unimodal logics. In particular, they show that the topological product of S4 and S4 is S4 ⊗ S4, i.e., the fusion of S4 and S4: this logic is strictly weaker than (...) the frame product S4 × S4. In this paper, we axiomatize the topological product of S4 and S5, which is strictly between S4 ⊗ S5 and S4 × S5. We also apply our techniques to (1) proving a conjecture of van Benthem et al concerning the logic of products of Alexandrov spaces with arbitrary topological spaces; and (2) solving a problem in quantified modal logic: in particular, it is known that standard quantified S4 without identity, QS4, is complete in Kripke semantics with expanding domains; we show that QS4 is complete not only in topological semantics with constant domains (which was already shown by Rasiowa and Sikorski), but wrt the topological space Q with a constant countable domain. (shrink)

It is shown that the many-dimensional modal logic K n , determined by products of n-many Kripke frames, is not finitely axiomatisable in the n-modal language, for any $n > 2$ . On the other hand, K n is determined by a class of frames satisfying a single first-order sentence.

We show the first examples of recursively enumerable (even decidable) two-dimensional products of finitely axiomatisable modal logics that are not finitely axiomatisable. In particular, we show that any axiomatisation of some bimodal logics that are determined by classes of product frames with linearly ordered first components must be infinite in two senses: It should contain infinitely many propositional variables, and formulas of arbitrarily large modal nesting-depth.

Our concern is the axiomatisation problem for modal and algebraic logics that correspond to various fragments of two-variable first-order logic with counting quantifiers. In particular, we consider modal products with Diff, the propositional unimodal logic of the difference operator. We show that the two-dimensional product logic $Diff \times Diff$ is non-finitely axiomatisable, but can be axiomatised by infinitely many Sahlqvist axioms. We also show that its ‘square’ version (the modal counterpart of the substitution and equality (...) free fragment of two-variable first-order logic with counting to two) is non-finitely axiomatisable over $Diff \times Diff$ , but can be axiomatised by adding infinitely many Sahlqvist axioms. These are the first examples of products of finitely axiomatisable modal logics that are not finitely axiomatisable, but axiomatisable by explicit infinite sets of canonical axioms. (shrink)

Future Logic is an original, and wide-ranging treatise of formal logic. It deals with deduction and induction, of categorical and conditional propositions, involving the natural, temporal, extensional, and logical modalities. Traditional and Modern logic have covered in detail only formal deduction from actual categoricals, or from logical conditionals (conjunctives, hypotheticals, and disjunctives). Deduction from modal categoricals has also been considered, though very vaguely and roughly; whereas deduction from natural, temporal and extensional forms of conditioning has been all but totally (...) ignored. As for induction, apart from the elucidation of adductive processes (the scientific method), almost no formal work has been done. This is the first work ever to strictly formalize the inductive processes of generalization and particularization, through the novel methods of factorial analysis, factor selection and formula revision. This is the first work ever to develop a formal logic of the natural, temporal and extensional types of conditioning (as distinct from logical conditioning), including their production from modal categorical premises. Future Logic contains a great many other new discoveries, organized into a unified, consistent and empirical system, with precise definitions of the various categories and types of modality (including logical modality), and full awareness of the epistemological and ontological issues involved. Though strictly formal, it uses ordinary language, wherever symbols can be avoided. Among its other contributions: a full list of the valid modal syllogisms (which is more restrictive than previous lists); the main formalities of the logic of change (which introduces a dynamic instead of merely static approach to classification); the first formal definitions of the modal types of causality; a new theory of class logic, free of the Russell Paradox; as well as a critical review of modern metalogic. But it is impossible to list briefly all the innovations in logical science — and therefore, epistemology and ontology — this book presents; it has to be read for its scope to be appreciated. (shrink)

The Handbook of Modal Logic contains 20 articles, which collectively introduce contemporary modal logic, survey current research, and indicate the way in which the field is developing. The articles survey the field from a wide variety of perspectives: the underling theory is explored in depth, modern computational approaches are treated, and six major applications areas of modal logic (in Mathematics, Computer Science, Artificial Intelligence, Linguistics, Game Theory, and Philosophy) are surveyed. The book contains both well-written expository articles, (...) suitable for beginners approaching the subject for the first time, and advanced articles, which will help those already familiar with the field to deepen their expertise. Please visit: http://people.uleth.ca/~woods/RedSeriesPromo_WP/PubSLPR.html - Compact modal logic reference - Computational approaches fully discussed - Contemporary applications of modal logic covered in depth. (shrink)

Apostoli and Brown have shown that the class of formulae valid with respect to the class of -ary relational frames is completely axiomatized by Kn: an n-place aggregative system which adjoins [RM], [RN], and a complete axiomatization of propositional logic, with [Kn]:□α1 ∧...∧□αn+1 → □2/ is the disjunction of all pairwise conjunctions αi∧αj )).Their proof exploits the chromatic indices of n-uncolourable hypergraphs, or n-traces. Here, we use the notion of the χ-product of a family of sets to formulate an alternative (...) definition of an n-trace, which in turn enables a new and simpler completeness proof. (shrink)

Does general validity or real world validity better represent the intuitive notion of logical truth for sentential modal languages with an actuality connective? In (Philosophical Studies 130:436–459, 2006) I argued in favor of general validity, and I criticized the arguments of Zalta (Journal of Philosophy 85:57–74, 1988) for real world validity. But in Nelson and Zalta (Philosophical Studies 157:153–162, 2012) Michael Nelson and Edward Zalta criticize my arguments and claim to have established the superiority of real world validity. Section (...) 1 of the present paper introduces the problem and sets out the basic issues. In Sect. 2 I consider three of Nelson and Zalta’s arguments and find all of them deficient. In Sect. 3 I note that Nelson and Zalta direct much of their criticism at a phrase (‘true at a world from the point of view of some distinct world as actual’) I used only inessentially in Hanson (Philosophical Studies 130:436–459, 2006), and that their account of the philosophical foundations of modal semantics leaves them ill equipped to account for the plausibility of modal logics weaker than S5. Along the way I make several general suggestions for ways in which philosophical discussions of logical matters–especially, but not limited to, discussions of truth and logical truth for languages containing modal and indexical terms–might be facilitated and made more productive. (shrink)

The modal logician's notion of possible world and the computer scientist's notion of state of a machine provide a point of commonality which can form the foundation of a logic of action. Extending ordinary modal logic with the calculus of binary relations leads to a very natural logic for describing the behavior of computer programs.

If deontic logic is to cast light on any of the normative sciences, such as legal reasoning, then certain problems regarding its logical constants must be faced. Recent studies in the area of deontic logic have tended to assume that it is our responses to the “paradoxes” of deontic implication which are fundamental to resolving problems with the use of deontic logic to investigate various branches of normative reasoning. In this paper I wish to show that the paradoxes are of (...) secondary importance; that they are merely by‐products of the central issue, namely the ability of certain syntactic forms to embody natural language structures used in reasoning about norms. An investigation of modal syntax is proffered as the best starting‐point from which to tackle the questions that still dog the legitimacy of deontic logic. Part I provides some philosophical background to the discussion of deontic logical constants. Part II addresses in greater detail issues concerning the representation of normative concepts; and Part III offers a few remarks on the general issue of deontic logic's fruitfulness as an analytical tool. (shrink)