Generalises the concept of a relational model for modal logic, due to Kripke, so as to obtain a closer correspondence between relational and algebraic models. The generalisation obtained is essentially equivalent to the notion of a "first-order" model that was defined independently by S.K.Thomason.

Given a class $$\mathcal {C}$$ of models, a binary relation $$\mathcal {R}$$ between models, and a model-theoretic language L, we consider the modal logic and the modal algebra of the theory of $$\mathcal {C}$$ in L where the modal operator is interpreted via $$\mathcal {R}$$. We discuss how modal theories of $$\mathcal {C}$$ and $$\mathcal {R}$$ depend on the model-theoretic language, their Kripke completeness, and expressibility of the modality inside L. We calculate such (...) theories for the submodel and the quotient relations. We prove a downward Löwenheim–Skolem theorem for first-order language expanded with the modal operator for the extension relation between models. (shrink)

The positive fragment of the local modal consequence relation defined by the class of all Kripke frames is studied in the context ofAlgebraic Logic. It is shown that this fragment is non-protoalgebraic and that its class of canonically associated algebras according to the criteria set up in [7] is the class of positive modal algebras. Moreover its full models are characterized as the models of the Gentzen calculus introduced in [3].

Hyperboolean algebras are Boolean algebras with operators, constructed as algebras of complexes (or, power structures) of Boolean algebras. They provide an algebraic semantics for a modal logic (called here a {\em hyperboolean modal logic}) with a Kripke semantics accordingly based on frames in which the worlds are elements of Boolean algebras and the relations correspond to the Boolean operations. We introduce the hyperboolean modal logic, give a complete axiomatization of it, and show that it lacks (...) the finite model property. The method of axiomatization hinges upon the fact that a "difference" operator is definable in hyperboolean algebras, and makes use of additional non-Hilbert-style rules. Finally, we discuss a number of open questions and directions for further research. (shrink)

We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic (...) class='Hi'>models and these in turn to the appropriate categorical models for these logics. (shrink)

Quasi-Boolean modal algebras are quasi-Boolean algebras with a modal operator satisfying the interaction axiom. Sequential quasi-Boolean modal logics and the relational semantics are introduced. Kripke-completeness for some quasi-Boolean modal logics is shown by the canonical model method. We show that every descriptive persistent quasi-Boolean modal logic is canonical. The finite model property of some quasi-Boolean modal logics is proved. A cut-free Gentzen sequent calculus for the minimal quasi-Boolean logic is developed and we (...) show that it has the Craig interpolation property. (shrink)

This paper presents an algebraic approach of some many-valued generalizations of modal logic. The starting point is the definition of the [0, 1]-valued Kripke models, where [0, 1] denotes the well known MV-algebra. Two types of structures are used to define validity of formulas: the class of frames and the class of Ł n -valued frames. The latter structures are frames in which we specify in each world u the set (a subalgebra of Ł n ) (...) of the allowed truth values of the formulas in u. We apply and develop algebraic tools (namely, canonical and strong canonical extensions) to generate complete modal n + 1-valued logics and we obtain many-valued counterparts of Shalqvist canonicity result. (shrink)

Quasi-Boolean modal algebras are quasi-Boolean algebras with a modal operator satisfying the interaction axiom. Sequential quasi-Boolean modal logics and the relational semantics are introduced. Kripke-completeness for some quasi-Boolean modal logics is shown by the canonical model method. We show that every descriptive persistent quasi-Boolean modal logic is canonical. The finite model property of some quasi-Boolean modal logics is proved. A cut-free Gentzen sequent calculus for the minimal quasi-Boolean logic is developed and we (...) show that it has the Craig interpolation property. (shrink)

We prove strong completeness of the □-version and the ◊-version of a Gödel modal logic based on Kripke models where propositions at each world and the accessibility relation are both infinitely valued in the standard Gödel algebra [0,1]. Some asymmetries are revealed: validity in the first logic is reducible to the class of frames having two-valued accessibility relation and this logic does not enjoy the finite model property, while validity in the second logic requires truly fuzzy accessibility (...) relations and this logic has the finite model property. Analogues of the classical modal systems D, T, S4 and S5 are considered also, and the completeness results are extended to languages enriched with a discrete well ordered set of truth constants. (shrink)

This paper deals with Kripke-style semantics for many-valued logics. We introduce various types of Kripke semantics, and we connect them with algebraic semantics. As for modal logics, we relate the axioms of logics extending MTL to properties of the Kripke frames in which they are valid. We show that in the propositional case most logics are complete but not strongly complete with respect to the corresponding class of complete Kripke frames, whereas in the predicate (...) case there are important many-valued logics like BL, Ł and Π, which are not even complete with respect to the class of all predicate Kripke frames in which they are valid. Thus although very natural, Kripke semantics seems to be slightly less powerful than algebraic semantics. (shrink)

This paper develops the model theory of normal modal logics based on partial “possibilities” instead of total “worlds,” following Humberstone [1981] instead of Kripke [1963]. Possibility semantics can be seen as extending to modal logic the semantics for classical logic used in weak forcing in set theory, or as semanticizing a negative translation of classical modal logic into intuitionistic modal logic. Thus, possibility frames are based on posets with accessibility relations, like intuitionistic modal frames, (...) but with the constraint that the interpretation of every formula is a regular open set in the Alexandrov topology on the poset. The standard world frames for modal logic are the special case of possibility frames wherein the poset is discrete. The analogues of classical Kripke frames, i.e., full world frames, are full possibility frames, in which propositional variables may be interpreted as any regular open sets. We develop the beginnings of duality theory, definability/correspondence theory, and completeness theory for possibility frames. The duality theory, relating possibility frames to Boolean algebras with operators (BAOs), shows the way in which full possibility frames are a generalization of Kripke frames. Whereas Thomason [1975a] established a duality between the category of Kripke frames with p-morphisms and the category of complete (C), atomic (A), and completely additive (V) BAOs with complete BAO-homomorphisms (these categories being dually equivalent), we establish a duality between the category of full possibility frames with possibility morphisms and the category of CV-BAOs, i.e., allowing non-atomic BAOs, with complete BAO-homomorphisms (the latter category being dually equivalent to a reflective subcategory of the former). This parallels the connection between forcing posets and Boolean-valued models in set theory, but now with accessibility relations and modal operators involved. Generalizing further, we introduce a class of principal possibility frames that capture the generality of V-BAOs. If we do not require a full or principal frame, then every BAO has an equivalent possibility frame, whose possibilities are proper filters in the BAO. With this filter representation, which does not require the ultrafilter axiom, we are lead to a notion of filter-descriptive possibility frames. Whereas Goldblatt [1974] showed that the category of BAOs with BAO-homomorphisms is dually equivalent to the category of descriptive world frames with p-morphisms, we show that the category of BAOs with BAO-homomorphisms is dually equivalent to the category of filter-descriptive possibility frames with p-morphisms. Applying our duality theory to definability theory, we prove analogues for possibility semantics of theorems of Goldblatt [1974] and Goldblatt and Thomason [1975] characterizing modally definable classes of frames. In addition, we discuss analogues for possibility semantics of first-order correspondence results in the style of Lemmon and Scott [1977], Sahlqvist [1975], and van Benthem [1976a]. Finally, applying our duality theory to completeness theory, we show that there are continuum many normal modal logics that can be characterized by full possibility frames but not by Kripke frames, that all Sahlqvist logics can be characterized by full possibility frames that contain no worlds, and that all normal modal logics can be characterized by filter-descriptive possibility frames. (shrink)

We define the notion of a model of higher-order modal logic in an arbitrary elementary topos E. In contrast to the well-known interpretation of higher-order logic, the type of propositions is not interpreted by the subobject classifier ΩE, but rather by a suitable complete Heyting algebra H. The canonical map relating H and ΩE both serves to interpret equality and provides a modal operator on H in the form of a comonad. Examples of such structures arise from surjective (...) geometric morphisms f : F → E, where H = f∗ΩF. The logic differs from non-modal higher-order logic in that the principles of functional and propositional extensionality are not longer valid but may be replaced by modalized versions. The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion. (shrink)

This paper presents the algebraic and Kripke modelsoundness and completeness ofa logic over Boolean monoids. An additional axiom added to thelogic will cause the resulting monoid models to be representable as monoidsof relations. A star operator, interpreted as reflexive, transitiveclosure, is conservatively added to the logic. The star operator isa relative modal operator, i.e., one that is defined in terms ofanother modal operator. A further example, relative possibility,of this type of operator is given. A separate (...) axiom,antilogism, added to the logic causes the Kripke models to support acollection of abstract topological uniformities which become concretewhen the Kripke models are dual to monoids of relations. The machineryfor the star operator is shownto be a recasting of Scott-Montague neighborhood models. An interpretationof the Kripke frames and properties thereof is presented in terms ofcertain CMOS transister networks and some circuit transformation equivalences.The worlds of the Kripke frame are wires and the Kripke relation is a specializedCMOS pass transistor network. (shrink)

This work is divided in two papers (Part I and Part II). In Part I, we study a class of polymodal logics (herein called the class of "Rare-logics") for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability are established by (...) faithfully translating the Rare-logics into more standard modal logics. The main idea of the translation consists in eliminating the Boolean terms by taking advantage of the components construction and in using various properties of the classes of semilattices involved in the semantics. The novelty of our approach allows us to prove new decidability results (presented in Part II), in particular for information logics derived from rough set theory and we open new perspectives to define proof systems for such logics (presented also in Part II). (shrink)

This work is divided in two papers (Part I and Part II). In Part I, we introduced the class of Rare-logics for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability were established by faithfully translating the Rare-logics into more standard (...) modal logics (some of them contain the universal modal operator).In Part II, we push forward the results from Part I. For Rare-logics with nominals (present at the level of formulae and at the level of modal expressions), we show that the constructions from Part I can be extended although it is technically more involved. We also characterize a class of standard modal logics for which the universal modal operator can be eliminated as far as satifiability is concerned. Although the previous results have a semantic flavour, we are also able to define proof systems for Rare-logics from existing proof systems for the corresponding standard modal logics. Last, but not least, decidability results for Rare-logics are established uniformly, in particular for information logics derived from rough set theory. (shrink)

This is a review of those aspects of the theory of varieties of Boolean algebras with operators that emphasise connections with modal logic and structural properties that are related to natural properties of logical systems.It begins with a survey of the duality that exists between BAO's and relational structures, focusing on the notions of bounded morphisms, inner substructures, disjoint and bounded unions, and canonical extensions of structures that originate in the study of validity-preserving operations on Kripke frames. (...) This duality is then applied to polymodal propositional logics having finitary intensional connectives that generalise the Box and Diamond connectives of unary modal logic. Issues discussed include validity in canonical structures, completeness under the relational semantics, and characterisations of logics by elementary classes of structures and by finite structures.It turns out that a logic is strongly complete for the relational semantics if the variety of algebras it defines is complex, which means that every algebra in the variety is embeddable into a full powerset algebras that is also in the variety. A hitherto unpublished formulation and proof of this is given that applies to quasi-varieties. This is followed by an algebraic demonstration that the temporal logic of Dedekind complete linear orderings defines a complex variety, adapting Gabbay's model-theoretic proof that this logic is strongly complete. (shrink)

Gives the first published adaptation of the Lindenbaum/Henkin method of maximal consistent sets for establishing the completeness of modal propositional logics with respect to the relational models of Kripke.

This paper, a sequel to Models for normal intuitionistic modal logics by M. Boi and the author, which dealt with intuitionistic analogues of the modal system K, deals similarly with intuitionistic analogues of systems stronger than K, and, in particular, analogues of S4 and S5. For these prepositional logics Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given, and soundness and completeness are proved with respect to these models. (...) It is shown how the holding of formulae characteristic for particular logics is equivalent to conditions for the relations of the models. Modalities in these logics are also investigated. (shrink)

This contribution is an essay of formal philosophy—and more specifically of formal ontology and formal epistemology—applied, respectively, to the philosophy of nature and to the philosophy of sciences, interpreted the former as the ontology and the latter as the epistemology of the modern mathematical, natural, and artificial sciences, the theoretical computer science included. I present the formal philosophy in the framework of the category theory (CT) as an axiomatic metalanguage—in many senses “wider” than set theory (ST)—of mathematics and logic, both (...) of the “extensional” logics of the pure and applied mathematical sciences (=mathematical logic), and the “intensional” modal logics of the philosophical disciplines (=philosophical logic). It is particularly significant in this categorical framework the possibility of extending the operator algebra formalism from (quantum and classical) physics to logic, via the so-called “Boolean algebras with operators” (BAOs), with this extension being the core of our formal ontology. In this context, I discuss the relevance of the algebraic Hopf coproduct and colimit operations, and then of the category of coalgebras in the computations over lattices of quantum numbers in the quantum field theory (QFT), interpreted as the fundamental physics. This coalgebraic formalism is particularly relevant for modeling the notion of the “quantum vacuum foliation” in QFT of dissipative systems, as a foundation of the notion of “complexity” in physics, and “memory” in biological and neural systems, using the powerful “colimit” operators. Finally, I suggest that in the CT logic, the relational semantics of BAOs, applied to the modal coalgebraic relational logic of the “possible worlds” in Kripke’s model theory, is the proper logic of the formal ontology and epistemology of the natural realism, as a formalized philosophy of nature and sciences. (shrink)

We present a Kripke model for Girard's Linear Logic (without exponentials) in a conservative fashion where the logical functors beyond the basic lattice operations may be added one by one without recourse to such things as negation. You can either have some logical functors or not as you choose. Commutatively and associatively are isolated in such a way that the base Kripke model is a model for noncommutative, nonassociative Linear Logic. We also extend the logic by adding a (...) coimplication operator, similar to Curry's subtraction operator, which is resituated with Linear Logic's contensor product. And we can add contraction to get nondistributive Relevance Logic. The model rests heavily on Urquhart's representation of nondistributive lattices and also on Dunn's Gaggle Theory. Indeed, the paper may be viewed as an investigation into nondistributive Gaggle Theory restricted to binary operations. The valuations on the Kripke model are three valued: true, false, and indifferent. The lattice representation theorem of Urquhart has the nice feature of yielding Priestley's representation theorem for distributive lattices if the original lattice happens to be distributive. Hence the representation is consistent with Stone's representation of distributive and Boolean lattices, and our semantics is consistent with the Lemmon-Scott representation of modal algebras and the Routley-Meyer semantics for Relevance Logic. (shrink)

Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given for analogues of the modal systemK based on Heyting's prepositional logic. It is shown that these two relations can combine with each other in various ways. Soundness and completeness are proved for systems with only the necessity operator, or only the possibility operator, or both. Embeddings in modal systems with several modal operators, based on classical propositional logic, are also considered. (...) This paper lays the ground for an investigation of intuitionistic analogues of systems stronger thanK. A brief survey is given of the existing literature on intuitionistic modal logic. (shrink)

Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics (...) define the same consequence relations for a given spi-logic. (shrink)

Saul Kripke has made fundamental contributions to a variety of areas of logic, and his name is attached to a corresponding variety of objects and results. 1 For philosophers, by far the most important examples are ‘Kripke models’, which have been adopted as the standard type of models for modal and related non-classical logics. What follows is an elementary introduction to Kripke’s contributions in this area, intended to prepare the reader to tackle more formal (...) treatments elsewhere.2 2. WHAT IS A MODEL THEORY? Traditionally, a statement is regarded as logically valid if it is an instance of a logically valid form, where a form is regarded as logically valid if every instance is true. In modern logic, forms are represented by formulas involving letters and special symbols, and logicians seek therefore to define a notion of model and a notion of a formula’s truth in a model in such a way that every instance of a form will be true if and only if a formula representing that form is true in every model. Thus the unsurveyably vast range of instances can be replaced for purposes of logical evaluation by the range of models, which may be more tractable theoretically and perhaps practically. Consideration of the familiar case of classical sentential logic should make these ideas clear. Here a formula, say (p & q) ∨ ¬p ∨ ¬q, will be valid if for all statements P.. (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.

The formula A (it is noncontingent whether A) is true at a point in a Kripke model just in case all points accessible to that point agree on the truth-value of A. We can think of -based modal logic as a special case of what we call the general modal logic of agreement, interpreted with the aid of models supporting a ternary relation, S, say, with OA (which we write instead of A to emphasize the generalization (...) involved) true at a point w just in case for all points x, y, with Swxy, x and y agree on the truth-value of A. The noncontingency interpretation is the special case in which Swxy if and only if Rwx and Rwy, where R is a traditional binary accessibility relation. Another application, related to work of Lewis and von Kutschera, allows us to think of OA as saying that A is entirely about a certain subject matter. (shrink)

The paper presents a semantics for quantified modal logic which has a weaker axiomatization than the usual Kripke semantics. In particular, the Barcan Formula and its converse are not valid with the proposed semantics. Subclasses of models which validate BF and other interesting formulas are presented. A completeness theorem is proved, and the relation between this result and completeness with respect to Kripke models is investigated.

Various four- and three-valued modal propositional logics are studied. The basic systems are modal extensions BK and BS4 of Belnap and Dunn's four-valued logic of firstdegree entailment. Three-valued extensions of BK and BS4 are considered as well. These logics are introduced semantically by means of relational models with two distinct evaluation relations, one for verification and the other for falsification. Axiom systems are defined and shown to be sound and complete with respect to the relational (...) semantics and with respect to twist structures over modal algebras. Sound and complete tableau calculi are presented as well. Moreover, a number of constructive non-modal logics with strong negation are faithfully embedded into BS4, into its three-valued extension B3S4, or into temporal BS4, BtS4. These logics include David Nelson's three-valued logic N3, the four-valued logic N4 bottom, the connexive logic C, and several extensions of bi-intuitionistic logic by strong negation. (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)

We characterize all finitary consequence relations over S4.3, both syntactically, by exhibiting so-called passive rules that extend the given logic, and semantically, by providing suitable strongly adequate classes of algebras. This is achieved by applying an earlier result stating that a modal logic L extending S4 has projective unification if and only if L contains S4.3. In particular, we show that these consequence relations enjoy the strong finite model property, and are finitely based. In this way, we extend the (...) known results by Bull and Fine, from logics, to consequence relations. We also show that the lattice of consequence relations over S4.3 is countable and distributive and it forms a Heyting algebra. (shrink)

Modal logic with counting is obtained from basic modal logic by adding cardinality comparison formulas of the form $ \#\varphi \succsim \#\psi $, stating that the cardinality of successors satisfying $ \varphi $ is larger than or equal to the cardinality of successors satisfying $ \psi $. It is different from graded modal logic where basic modal logic is extended with formulas of the form $ \Diamond _{k}\varphi $ stating that there are at least $ k$-many (...) different successors satisfying $ \varphi $. In this paper, we investigate the axiomatization of ML(#) with respect to different frame classes, such as image-finite frames and arbitrary frames. Drawing inspiration from existing works, we employ a similar proof strategy that uses the characterization of binary relations on finite Boolean algebras capable of representing generalized probability measures or finite (respectively arbitrary) cardinality measures. Our main result shows that any formula not provable in the Hilbert system can be refuted within a finite (respectively arbitrary) cardinality measure Kripke frame with a finite domain. We then transform this finite (respectively arbitrary) cardinality measure Kripke frame into a Kripke frame in the corresponding class, refuting the unprovable formula. (shrink)

The relationships between various modal logics based on Belnap and Dunn’s paraconsistent four-valued logic FDE are investigated. It is shown that the paraconsistent modal logic \, which lacks a primitive possibility operator \, is definitionally equivalent with the logic \, which has both \ and \ as primitive modalities. Next, a tableau calculus for the paraconsistent modal logic KN4 introduced by L. Goble is defined and used to show that KN4 is definitionally equivalent with \ without the (...) absurdity constant. Moreover, a tableau calculus is defined for the modal bilattice logic MBL introduced and investigated by A. Jung, U. Rivieccio, and R. Jansana. MBL is a generalization of BK that in its Kripke semantics makes use of a four-valued accessibility relation. It is shown that MBL can be faithfully embedded into the bimodal logic \ over the non-modal vocabulary of MBL. On the way from \ to MBL, the Fischer Servi-style modal logic \ is defined as the set of all modal formulas valid under a modified standard translation into first-order FDE, and \ is shown to be characterized by the class of all models for \. Moreover, \ is axiomatized and this axiom system is proved to be strongly sound and complete with respect to the class of models for \. Moreover, the notion of definitional equivalence is suitably weakened, so as to show that \ and \ are weakly definitionally equivalent. (shrink)

For each natural number n we study the modal logic determined by the class of transitive Kripke frames in which there are no cycles of length greater than n and no strictly ascending chains. The case n=0\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$n=0$$\end{document} is the Gödel-Löb provability logic. Each logic is axiomatised by adding a single axiom to K4, and is shown to have the finite model property and be decidable. We then consider a number (...) of extensions of these logics, including restricting to reflexive frames to obtain a corresponding sequence of extensions of S4. When n=1\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$n=1$$\end{document}, this gives the famous logic of Grzegorczyk, known as S4Grz, which is the strongest modal companion to intuitionistic propositional logic. A topological semantic analysis shows that the n-th member of the sequence of extensions of S4 is the logic of hereditarily n+1\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$n+1$$\end{document}-irresolvable spaces when the modality ◊\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Diamond $$\end{document} is interpreted as the topological closure operation. We also study the definability of this class of spaces under the interpretation of ◊\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Diamond $$\end{document} as the derived set operation. The variety of modal algebras validating the n-th logic is shown to be generated by the powerset algebras of the finite frames with cycle length bounded by n. Moreover each algebra in the variety is a model of the universal theory of the finite ones, and so is embeddable into an ultraproduct of them. (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)

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 classical modal semantics, a binary accessibility relation connects worlds. In this paper, we present a uniform and systematic treatment of modal semantics with a continuous accessibility relation alongside the continuous accessibility modal logics that they model. We develop several such logics for a variety of philosophical applications. Our main conclusions are as follows. Modal logics with a continuous accessibility relation are sound and complete in their natural classes of models. The class of Kripke (...) frames where a continuous accessibility relation has a magnitude characterizing its degree of accessibility is not modally definable, and this has unappreciated significance to completeness proofs for such logics, revealing a methodological advantage of using classical multimodal semantics over fuzzy modal semantics. There is a pseudometric space modal logic that is complete in the class of pseudometric spaces, a natural semantic setting for quantitative modal reasoning about similarity. There is a metric space modal logic that is complete in the class of metric spaces, a natural semantic setting for quantitative modal reasoning about neighborhoods and counterfactual stability. There is a real line continuous temporal logic that is canonical for real lines, a natural semantic setting for quantitative modal reasoning about time. (shrink)

We present a framework for understanding abduction within modal logic and Kripke semantics; worlds of a Kripke frame will represent possible theories, and a change in theory will be understood as a passage from one world to an adjacent possible world. Further, these steps may agree with the accessibility relation or may ‘backtrack’, accordingly as new information refutes or reinforces our present theory. Our formalism can be used to model not only abduction, but also to talk about (...) the inner structure of theories as well as relations between them, allowing us to interpret many ideas from philosophy of science within the well-understood framework of modal logic. (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)

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)

Treating the existential quantification ∃ν i as a diamond $\diamond_i$ and the identity ν i = ν j as a constant δ ij , we study restricted versions of first order logic as if they were modal formalisms. This approach is closely related to algebraic logic, as the Kripke frames of our system have the type of the atom structures of cylindric algebras; the full cylindric set algebras are the complex algebras of the intended multidimensional frames called (...) cubes. The main contribution of the paper is a characterization of these cube frames for the finite-dimensional case and, as a consequence of the special form of this characterization, a completeness theorem for this class. These results lead to finite, though unorthodox, derivation systems for several related formalisms, e.g. for the valid n-variable first order formulas, for type-free valid formulas and for the equational theory of representable cylindric algebras. The result for type-free valid formulas indicates a positive solution to Problem 4.16 of Henkin, Monk and Tarski [16]. (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)

We prove that each intermediate or normal modal logic is strongly complete with respect to a class of finite Kripke frames iff it is tabular, i.e. the respective variety of pseudo-Boolean or modal algebras, corresponding to it, is generated by a finite algebra.

Various connexive FDE-based modal logics are studied. Some of these logics contain a conditional that is both connexive and strict, thereby highlighting that strictness and connexivity of a conditional do not exclude each other. In particular, the connexive modal logics cBK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^{-}$$\end{document}, cKN4, scBK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^{-}$$\end{document}, scKN4, cMBL, and scMBL are introduced semantically by means of classes of Kripke models. The logics (...) cBK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^{-}$$\end{document} and cKN4 are connexive variants of the FDE-based modal logics BK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^{-}$$\end{document} and KN4 with a weak and a strong implication, respectively. The system cMBL is a connexive variant of the modal bilattice logic MBL. The latter is a modal extension of Arieli and Avron’s logic of logical bilattices and is characterized by a class of Kripke models with a four-valued accessibility relation. In the systems scBK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^{-}$$\end{document}, scKN4, and scMBL, the conditional is both connexive and strict. Sound and complete tableau calculi for all these logics are presented and used to show that the entailment relations of the systems under consideration are decidable for finite premise set. Moreover, the logics cBK-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {cBK}^-$$\end{document} and cMBL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {cMBL}$$\end{document} are shown to be algebraizable. The algebraizability of cMBL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {cMBL}$$\end{document} is derived from proving cMBL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {cMBL}$$\end{document} to be definitionally equivalent to MBL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {MBL}$$\end{document}. All connexive modal logics studied in this paper are decidable, paraconsistent, and inconsistent but non-trivial logics. (shrink)

Grishin algebras are a generalisation of Boolean algebras that provide algebraic models for classical bilinear logic with two mutually cancelling negation connectives. We show how to build complete Grishin algebras as algebras of certain subsets (“propositions”) of cover systems that use an orthogonality relation to interpret the negations. The variety of Grishin algebras is shown to be closed under MacNeille completion, and this is applied to embed an arbitrary Grishin algebra into the algebra of all propositions of some (...) cover system, by a map that preserves all existing joins and meets. This representation is then used to give a cover system semantics for a version of classical bilinear logic that has first-order quantifiers and infinitary conjunctions and disjunctions. (shrink)

We give an extension of the Jónsson‐Tarski representation theorem for both normal and non‐normal modal algebras so that it preserves countably many infinite meets and joins. In order to extend the Jónsson‐Tarski representation to non‐normal modal algebras we consider neighborhood frames instead of Kripke frames just as Došen's duality theorem for modal algebras, and to deal with infinite meets and joins, we make use of Q‐filters, which were introduced by Rasiowa and Sikorski, instead of prime filters. (...) By means of the extended representation theorem, we show that every predicate modal logic, whether it is normal or non‐normal, has a model defined on a neighborhood frame with constant domains, and we give a completeness theorem for some predicate modal logics with respect to classes of neighborhood frames with constant domains. Similarly, we show a model existence theorem and a completeness theorem for infinitary modal logics which allow conjunctions of countably many formulas. (shrink)

The chapter is divided in two parts. The first part gives an introduction to issues in quantified modal logic. We provide an overview of recent work in QML and we presuppose the use of a relational semantics. We discuss models for constant domains, increasing domains and varying domains and present axiomatizations for the corresponding logics. We also discuss philosophical issues related to the interpretation of the quantifiers, terms and identity and we present a first-order quantified intensional logic. (...) A crucial issue in QML is to provide a unified semantic framework capable of accommodating a large class of logical systems including both normal and non-normal systems. The second part of the article focuses on alternatives to the standard relational semantics for modalities deriving from the work of Kripke. In particular we give an overview of recent work in neighborhood semantics and we offer a general completeness result for the class of first order classical modal logics in terms of general frames with constant domains. We also consider some extensions of current work dealing with identity. (shrink)

In this paper we consider the modal logic with both $$\Box $$ and $$\Diamond $$ arising from Kripke models with a crisp accessibility and whose propositions are valued over the standard Gödel algebra $$[0,1]_G$$. We provide an axiomatic system extending the one from Caicedo and Rodriguez (J Logic Comput 25(1):37–55, 2015) for models with a valued accessibility with Dunn axiom from positive modal logics, and show it is strongly complete with respect to the intended semantics. (...) The axiomatizations of the most usual frame restrictions are given too. We also prove that in the studied logic it is not possible to get $$\Diamond $$ as an abbreviation of $$\Box $$, nor vice-versa, showing that indeed the axiomatic system we present does not coincide with any of the mono-modal fragments previously axiomatized in the literature. (shrink)

Suppose there are several experts, with some dominating others (expert A dominates expert B if B says something is true whenever A says it is). Suppose, further, that each of the experts has his or her own view of what is possible — in other words each of the experts has their own Kripke model in mind (subject, of course, to the dominance relation that may hold between experts). How will they assign truth values to sentences in a common (...) modal language, and on what sentences will they agree? This problem can be reformulated as one about many-valued Kripke models, allowing many-valued accessibility relations. This is a natural generalization of conventional Kripke models that has only recently been looked at. The equivalence between the many-valued version and the multiple expert one will be formally established. Finally we will axiomatize many-valued modal logics, and sketch a proof of completeness. (shrink)

A new deduction system for deciding validity for the minimal decidable normal modal logic K is presented in this article. Modal logics could be very helpful in modelling dynamic and reactive systems such as bio-inspired systems and process algebras. In fact, recently the Connectionist Modal Logics has been presented, which combines the strengths of modal logics and neural networks. Thus, modal logic K is the basis for these approaches. Soundness, completeness and the fact that the (...) system itself is a decision procedure are proved in this article. The main advantages of this approach are: first, the system is deterministic, i.e. it generates one proof tree for a given formula; second, the system is a validity-checker, hence it generates a proof of a formula ; and third, the language of deduction and the language of a logic coincide. Some of these advantages are compared with other classical approaches. (shrink)

In this paper we consider distributive modal logic, a setting in which we may add modalities, such as classical types of modalities as well as weak forms of negation, to the fragment of classical propositional logic given by conjunction, disjunction, true, and false. For these logics we define both algebraic semantics, in the form of distributive modal algebras, and relational semantics, in the form of ordered Kripke structures. The main contributions of this paper lie in (...) extending the notion of Sahlqvist axioms to our generalized setting and proving both a correspondence and a canonicity result for distributive modal logics axiomatized by Sahlqvist axioms. Our proof of the correspondence result relies on a reduction to the classical case, but our canonicity proof departs from the traditional style and uses the newly extended algebraic theory of canonical extensions. (shrink)

In the present paper, we start studying epistemic updates using the standard toolkit of duality theory. We focus on public announcements, which are the simplest epistemic actions, and hence on Public Announcement Logic without the common knowledge operator. As is well known, the epistemic action of publicly announcing a given proposition is semantically represented as a transformation of the model encoding the current epistemic setup of the given agents; the given current model being replaced with its submodel relativized to the (...) announced proposition. We dually characterize the associated submodel-injection map as a certain pseudo-quotient map between the complex algebras respectively associated with the given model and with its relativized submodel. As is well known, these complex algebras are complete atomic BAOs . The dual characterization we provide naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras . Thanks to this construction, the benefits and the wider scope of applications given by a point-free, intuitionistic theory of epistemic updates are made available. As an application of this dual characterization, we axiomatize the intuitionistic analogue of PAL, which we refer to as IPAL, prove soundness and completeness of IPAL w.r.t. both algebraic and relational models, and show that the well known Muddy Children Puzzle can be formalized in IPAL. (shrink)