The variety MBA of monadic bounded algebras consists of Boolean algebras with a distinguished element E, thought of as an existence predicate, and an operator ∃ reflecting the properties of the existential quantifier in free logic. This variety is generated by a certain class FMBA of algebras isomorphic to ones whose elements are propositional functions. We show that FMBA is characterised by the disjunction of the equations ∃E = 1 and ∃E = 0. We also define a weaker notion of (...) "relatively functional" algebra, and show that every member of MBA is isomorphic to a relatively functional one. (shrink)

Sets out the basic theory of normal modal and temporal propositional logics; applies this theory to logics of discrete (integer), dense (rational), and continuous (real) time, to the temporal logic of henceforth, next, and until, and to the propositional dynamic logic of regular programs.

Modal logic is the study of modalities - expressions that qualify assertions about the truth of statements - like the ordinary language phrases necessarily, possibly, it is known/believed/ought to be, etc., and computationally or mathematically motivated expressions like provably, at the next state, or after the computation terminates. The study of modalities dates from antiquity, but has been most actively pursued in the last three decades, since the introduction of the methods of Kripke semantics, and now impacts on a wide (...) range of disciplines, including the philosophy of language and linguistics ('possible words' semantics for natural language), constructive mathematics (intuitionistic logic), theoretical computer science (dynamic logic, temporal and other logics for concurrency), and category theory (sheaf semantics). This volume collects together a number of the author's papers on modal logic, beginning with his work on the duality between algebraic and set-theoretic modals, and including two new articles, one on infinitary rules of inference, and the other about recent results on the relationship between modal logic and first-order logic. Another paper on the 'Henkin method' in completeness proofs has been substantially extended to give new applications. Additional articles are concerned with quantum logic, provability logic, the temporal logic of relativistic spacetime, modalities in topos theory, and the logic of programs. (shrink)

Many systems of quantified modal logic cannot be characterised by Kripke's well-known possible worlds semantic analysis. This book shows how they can be characterised by a more general 'admissible semantics', using models in which there is a restriction on which sets of worlds count as propositions. This requires a new interpretation of quantifiers that takes into account the admissibility of propositions. The author sheds new light on the celebrated Barcan Formula, whose role becomes that of legitimising the Kripkean interpretation of (...) quantification. The theory is worked out for systems with quantifiers ranging over actual objects, and over all possibilia, and for logics with existence and identity predicates and definite descriptions. The final chapter develops a new admissible 'cover semantics' for propositional and quantified relevant logic, adapting ideas from the Kripke-Joyal semantics for intuitionistic logic in topos theory. This book is for mathematical or philosophical logicians, computer scientists and linguists. (shrink)

The Diodorean interpretation of modality reads the operator as it is now and always will be the case that. In this paper time is modelled by the four-dimensional Minkowskian geometry that forms the basis of Einstein's special theory of relativity, with event y coming after event x just in case a signal can be sent from x to y at a speed at most that of the speed of light (so that y is in the causal future of x).It is (...) shown that the modal sentences valid in this structure are precisely the theorems of the well-known logic S4.2, and that this system axiomatises the logics of two and three dimensional spacetimes as well. (shrink)

We introduce the equational notion of a monadic bounded algebra (MBA), intended to capture algebraic properties of bounded quantification. The variety of all MBA's is shown to be generated by certain algebras of two-valued propositional functions that correspond to models of monadic free logic with an existence predicate. Every MBA is a subdirect product of such functional algebras, a fact that can be seen as an algebraic counterpart to semantic completeness for monadic free logic. The analysis involves the representation of (...) MBA's as powerset algebras of certain directed graphs with a set of "marked" points. It is shown that there are only countably many varieties of MBA's, all are generated by their finite members, and all have finite equational axiomatisations classifying them into fourteen kinds of variety. The universal theory of each variety is decidable. Finitely generated MBA's are shown to be finite, with the free algebra on r generators having exactly $2^{3.2^{r.} } ^{2^{{\rm{2}}^{{\rm{r - 1}}} } } $ elements. An explicit procedure is given for constructing this freely generated algebra as the powerset algebra of a certain marked graph determined by the number r. (shrink)

The quantified relevant logic RQ is given a new semantics in which a formula for all xA is true when there is some true proposition that implies all x-instantiations of A. Formulae are modelled as functions from variable-assignments to propositions, where a proposition is a set of worlds in a relevant model structure. A completeness proof is given for a basic quantificational system QR from which RQ is obtained by adding the axiom EC of 'extensional confinement': for all x(A V (...) B) -> (A V for all xB). with x not free in A. Validity of EC requires an additional model condition involving the boolean difference of propositions. A QR-model falsifying EC is constructed by forming the disjoint union of two natural arithmetical structures in which negation is interpreted by the minus operation. (shrink)

Monomodal logic has exactly two maximally normal logics, which are also the only quasi-normal logics that are Post complete, and they are complete for validity in Kripke frames. Here we show that addition of a propositional constant to monomodal logic allows the construction of continuum many maximally normal logics that are not valid in any Kripke frame, or even in any complete modal algebra. We also construct continuum many quasi-normal Post complete logics that are not normal. The set of extensions (...) of S4.3 is radically altered by the addition of a constant: we use it to construct continuum many such normal extensions of S4.3, and continuum many non-normal ones, none of which have the finite model property. But for logics with weakly transitive frames there are only eight maximally normal ones, of which five extend K4 and three extend S4. (shrink)

The tangle modality is a propositional connective that extends basic modal logic to a language that is expressively equivalent over certain classes of finite frames to the bisimulation-invariant fragments of both first-order and monadic second-order logic. This paper axiomatises several logics with tangle, including some that have the universal modality, and shows that they have the finite model property for Kripke frame semantics. The logics are specified by a variety of conditions on their validating frames, including local and global connectedness (...) properties. Some of the results have been used to obtain completeness theorems for interpretations of tangled modal logics in topological spaces. (shrink)

Monomodal logic has exactly two maximally normal logics, which are also the only quasi-normal logics that are Post complete, and they are complete for validity in Kripke frames. Here we show that addition of a propositional constant to monomodal logic allows the construction of continuum many maximally normal logics that are not valid in any Kripke frame, or even in any complete modal algebra. We also construct continuum many quasi-normal Post complete logics that are not normal. The set of extensions (...) of S4.3 is radically altered by the addition of a constant: we use it to construct continuum many such normal extensions of S4.3, and continuum many non-normal ones, none of which have the finite model property. But for logics with weakly transitive frames there are only eight maximally normal ones, of which five extend K4 and three extend S4. (shrink)

A variety V of Boolean algebras with operators is singleton-persistent if it contains a complex algebra whenever it contains the subalgebra generated by the singletons. V is atom-canonical if it contains the complex algebra of the atom structure of any of the atomic members of V.This paper explores relationships between these "persistence" properties and questions of whether V is generated by its complex algebras or its atomic members, or is closed under canonical embedding algebras or completions. It also develops a (...) general theory of when operations involving complex algebras lead to the construction of elementary classes of relational structures. (shrink)

The Routley-Meyer relational semantics for relevant logics is extended to give a sound and complete model theory for many propositionally quantified relevant logics (and some non-relevant ones). This involves a restriction on which sets of worlds are admissible as propositions, and an interpretation of propositional quantification that makes ∀ pA true when there is some true admissible proposition that entails all p -instantiations of A . It is also shown that without the admissibility qualification many of the systems considered are (...) semantically incomplete, including all those that are sub-logics of the quantified version of Anderson and Belnap’s system E of entailment, extended by the mingle axiom and the Ackermann constant t . The incompleteness proof involves an algebraic semantics based on atomless complete Boolean algebras. (shrink)

A general result is proved about the existence of maximally consistent theories satisfying prescribed closure conditions. The principle is then used to give streamlined proofs of completeness and omitting-types theorems, in which inductive Henkin-style constructions are replaced by a demonstration that a certain theory respects a certain class of inference rules.

The Principle of Dependent Choice is shown to be equivalent to: the Baire Category Theorem for Čech-complete spaces (or for complete metric spaces); the existence theorem for generic sets of forcing conditions; and a proof-theoretic principle that abstracts the "Henkin method" of proving deductive completeness of logical systems. The Rasiowa-Sikorski Lemma is shown to be equivalent to the conjunction of the Ultrafilter Theorem and the Baire Category Theorem for compact Hausdorff spaces.

This paper uses an "admissible set semantics" to treat quantification in quantified modal logics. The truth condition for the universal quantifier states that a universally quantified statement (x)A(x) is true at a world w if and only if there is some proposition true at that world that entails every instance of A(x). It is shown that, for any canonical propositional modal logic the corresponding admissible set semantics characterises the quantified version of that modal logic.

We study a canonical modal logic introduced by Lemmon, and axiomatised by an infinite sequence of axioms generalising McKinsey’s formula. We prove that the class of all frames for this logic is not closed under elementary equivalence, and so is non-elementary. We also show that any axiomatisation of the logic involves infinitely many non-canonical formulas.

We show that there exist 2 ℵ 0 equational classes of Boolean algebras with operators that are not generated by the complex algebras of any first-order definable class of relational structures. Using a variant of this construction, we resolve a long-standing question of Fine, by exhibiting a bimodal logic that is valid in its canonical frames, but is not sound and complete for any first-order definable class of Kripke frames (a monomodal example can then be obtained using simulation results of (...) Thomason). The constructions use the result of Erd $\H{o}$ s that there are finite graphs with arbitrarily large chromatic number and girth. (shrink)

Regular dynamic logic is extended by the program construct, meaning and executed in parallel. In a semantics due to Peleg, each command is interpreted as a set of pairs (s,T), withT being the set of states reachable froms by a single execution of, possibly involving several processes acting in parallel. The modalities ] are given the interpretations>A is true ats iff there existsT withsRT andA true throughoutT, and.

A foundational algebra ( , f, ) consists of a hemimorphism f on a Boolean algebra with a greatest solution to the condition f(x). The quasi-variety of foundational algebras has a decidable equational theory, and generates the same variety as the complex algebras of structures (X, R), where f is given by R-images and is the non-wellfounded part of binary relation R.The corresponding results hold for algebras satisfying =0, with respect to complex algebras of wellfounded binary relations. These algebras, however, (...) generate the variety of all ( ,f) with f a hemimorphism on ). (shrink)

It is known that propositional relevant logics can be conservatively extended by the addition of a Heyting (intuitionistic) implication connective. We show that this same conservativity holds for a range of first-order relevant logics with strong identity axioms, using an adaptation of Fine’s stratified model theory. For systems without identity, the question of conservatively adding Heyting implication is thereby reduced to the question of conservatively adding the axioms for identity. Some results in this direction are also obtained. The conservative presence (...) of Heyting implication allows the development of an alternative model theory for quantified relevant logics. (shrink)

The existence of a final coalgebra is equivalent to the existence of a formal logic with a set of formulas that has the Hennessy–Milner property of distinguishing coalgebraic states up to bisimilarity. This applies to coalgebras of any functor on the category of sets for which the bisimilarity relation is transitive. There are cases of functors that do have logics with the Hennessy–Milner property, but the only such logics have a proper class of formulas. The main theorem gives a representation (...) of states of the final coalgebra as certain satisfiable sets of formulas. The key technical fact used is that any function between coalgebras that is truth-preserving and has a simple codomain must be a coalgebraic morphism. (shrink)

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)

Coalgebras of polynomial functors constructed from sets of observable elements have been found useful in modelling various kinds of data types and state-transition systems. This paper continues the study of equational logic and model theory for polynomial coalgebras begun in Goldblatt , where it was shown that Boolean combinations of equations between terms of observable type form a natural language of observable formulas for specifying properties of polynomial coalgebras, and for giving a Hennessy–Milner style logical characterisation of observational indistinguishability (...) of states.Here we give a structural characterisation of classes of coalgebras definable by observable formulas. This is an analogue for polynomial coalgebras of Birkhoff's celebrated characterisation of equationally definable classes of abstract algebras as being those closed under homomorphic images, subalgebras, and direct products. The coalgebraic characterisation involves new notions of observational ultraproduct and ultrapower of coalgebras, obtained from the classical construction of ultraproducts by deleting states that assign “nonstandard” values to terms of observable type. A class of polynomial coalgebras is shown to be the class of all models of a set of observable formulas if, and only if, it is closed under images of bisimulation relations, disjoint unions and observational ultrapowers.Observational ultraproducts are also used to discuss compactness—which holds only under limited conditions; to characterise finitely, axiomatisable classes of polynomial coalgebras; and to show that there are axiomatisable classes that are not finitely axiomatisable. (shrink)

In "An Alternative Semantics for Quantified Relevant Logic" (JSL 71 (2006)) we developed a semantics for quantified relevant logic that uses general frames. In this paper, we adapt that model theory to treat quantified modal logics, giving a complete semantics to the quantified extensions, both with and without the Barcan formula, of every proposi- tional modal logic S. If S is canonical our models are based on propositional frames that validate S. We employ frames in which not every set of (...) worlds is an admissible proposition, and an alternative interpretation of the uni- versal quantifier using greatest lower bounds in the lattice of admissible propositions. Our models have a fixed domain of individuals, even in the absence of the Barcan formula. For systems with the Barcan formula it is possible to preserve the usual Tarskian reading of the quantifier, at the expensive of sometimes losing va- lidity of S in the underlying propositional frames. We apply our results to a number of logics, including S4.2, S4M and KW, whose quantified extensions are incomplete for the standard semantics. (shrink)

We develop a method for showing that various modal logics that are valid in their countably generated canonical Kripke frames must also be valid in their uncountably generated ones. This is applied to many systems, including the logics of finite width, and a broader class of multimodal logics of ‘finite achronal width’ that are introduced here.

A fundamental result from Boolean modal logic states that a first-order definable class of Kripke frames defines a logic that is validated by all of its canonical frames. We generalise this to the level of non-distributive logics that have a relational semantics provided by structures based on polarities. Such structures have associated complete lattices of stable subsets, and these have been used to construct canonical extensions of lattice-based algebras. We study classes of structures that are closed under ultraproducts and whose (...) stable set lattices have additional operators that are first-order definable in the underlying structure. We show that such classes generate varieties of algebras that are closed under canonical extensions. The proof makes use of a relationship between canonical extensions and MacNeille completions. (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)