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)

In the following we will use the well-known correspondence between modal logics and varieties of modal algebras in our investigation of the function which assigns to a modal logic its degree of incompleteness. A modal algebra is an algebra A = where is a Boolean algebra and is a unary operation satisfying 1 = 1 and = x y ; is called a modal operator. A variety of algebras is a class of algebras closed under the operations of forming homomorphic (...) images, subalgebras as and direct products, and if K is a class of algebras then V denotes the smallest variety containing K. The variety of modal algebras is denoted by M, the subvariety of M dened by the equation x x = x by MR and the subvariety of M dened by the equation x n = x n1 , n a natural number, by Mn . Here x 0 = x, x n = , n a natural number. We write for the lattice of subvarieties of a variety K. If K, K 0 are varieties such that K $ K 0 but for no variety K 00 K $ K 00 $ K 0 then we say that K 0 is a cover of K. The smallest normal modal logic { containing the axiom ! and closed under the inference rules of modus ponens, substitution and necessitation { will be denoted by K; the lattice of modal logics which are extensions of K by. (shrink)

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.

Some results on the upper end of the lattice of all modal propositional logics.

This paper concerns modal logics appearing from the temporal ordering of domains in two-dimensional Minkowski spacetime. As R. Goldblatt has proved recently, the logic of the whole plane isS4.2. We consider closed or open convex polygons and closed or open domains bounded by simple differentiable curves; this leads to the logics:S4,S4.1,S4.2 orS4.1.2.

We give a sound and complete axiomatization for the full computation tree logic, CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.

We prove a finite model theorem and infinitary completeness result for the propositional -calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.

We present two finitely axiomatized modal propositional logics, one betweenTandS4 and the other an extension ofS4, which are incomplete with respect to the neighbourhood or Scott-Montague semantics.Throughout this paper we are referring to logics which contain all the classical connectives and only one modal connective □ (unary), no propositional constants, all classical tautologies, and which are closed under the rules of modus ponens (MP), substitution, and the rule RE (fromA↔Binfer αA↔ □B). Such logics are calledclassicalby Segerberg [6]. Classical logics which (...) contain the formula □p∧ □q→ □(p∧q) (denoted byK) and its “converse,” □{p∧q)→ □p∧ □q(denoted byR) are called regular;regularlogics which are closed under the rule of necessitation, RN (fromAinfer □A), are callednormal. The logics that we are particularly concerned with are all normal, although some of our results will be true for all regular or all classical logics. It is well known thatKandRand closure under RN imply closure under RE and also that normal logics are also those logics closed under RN and containing □{p→q) → {□p→ □q). (shrink)

Modal logics are studied in their algebraic disguise of varieties of so-called modal algebras. This enables us to apply strong results of a universal algebraic nature, notably those obtained by B. Jonsson. It is shown that the degree of incompleteness with respect to Kripke semantics of any modal logic containing the axiom □ p → p or containing an axiom of the form $\square^mp \leftrightarrow\square^{m + 1}p$ for some natural number m is 2 ℵ 0 . Furthermore, we show that (...) there exists an immediate predecessor of classical logic (axiomatized by $p \leftrightarrow \square p$ ) which is not characterized by any finite algebra. The existence of modal logics having 2 ℵ 0 immediate predecessors is established. In contrast with these results we prove that the lattice of extensions of S4 behaves much better: a logic extending S4 is characterized by a finite algebra iff it has finitely many extensions and any such logic has only finitely many immediate predecessors, all of which are characterized by a finite algebra. (shrink)

Some philosophers, for example Quine, doubt the possibility of jointly using modalities and quantification. Simple model-theoretic considerations, however, lead to a reconciliation of quantifiers with such modal concepts as logical, physical, and ethical necessity, and suggest a general class of modalities of which these are instances. A simple axiom system, analogous to the Lewis systems S1 —S5, is considered in connection with this class of modalities. The system proves to be complete, and its class of theorems decidable.

A first-order sentence is quasi-modal if its class of models is closed under the modal validity preserving constructions of disjoint unions, inner substructures and bounded epimorphic images. It is shown that all members of the proper class of canonical structures of a modal logic Λ have the same quasi-modal first-order theory Ψ Λ . The models of this theory determine a modal logic Λ e which is the largest sublogic of Λ to be determined by an elementary class. The canonical (...) structures of Λ e also have Ψ Λ as their quasi-modal theory. In addition there is a largest sublogic Λ c of Λ that is determined by its canonical structures, and again the canonical structures of Λ c have Ψ Λ are their quasi-modal theory. Thus Ψ Λ = Ψ Λ c = Ψ Λ e . Finally, we show that all finite structures validating Λ are models of Ψ Λ , and that if Λ is determined by its finite structures, then Ψ Λ is equal to the quasi-modal theory of these structures. (shrink)

This paper presents duality results between categories of neighbourhood frames for modal logic and categories of modal algebras (i.e. Boolean algebras with an additional unary operation). These results extend results of Goldblatt and Thomason about categories of relational frames for modal logic.