Neighbourhood semantics for graded modal logic

We introduce a class of neighbourhood frames for graded modal logic using an operation from Kripke frames to neighbourhood frames. This class of neighbourhood frames is shown to be first-order definable but not modally definable. We also obtain a new definition of graded bisimulation by modifying the definition of monotonic bisimulation.

Some Interrelations between Geometry and Modal Logic

This is a reprinting of Ken Pledger’s PhD thesis, submitted to the University of Warsaw in 1980 with the degree awarded in 1981. It develops a one-sorted approach to the theory of plane geometry, based on the idea that the usually two-sorted theory “can be made one-sorted by keeping careful account of whether the incidence relation is iterated an even or odd number of times”.The one-sorted structures can also serve as Kripke frames for modal logics, and the thesis defines and studies two such logics that are validated by projective planes and elliptic planes respectively. It raises questions of logical completeness for these systems that are addressed in the first article of this journal issue.

On the Logic of Belief and Propositional Quantification

We consider extending the modal logic KD45, commonly taken as the baseline system for belief, with propositional quantifiers that can be used to formalize natural language sentences such as “everything I believe is true” or “there is something that I neither believe nor disbelieve.” Our main results are axiomatizations of the logics with propositional quantifiers of natural classes of complete Boolean algebras with an operator (BAOs) validating KD45. Among them is the class of complete, atomic, and completely multiplicative BAOs validating KD45. Hence, by duality, we also cover the usual method of adding propositional quantifiers to normal modal logics by considering their classes of Kripke frames. In addition, we obtain decidability for all the concrete logics we discuss.

Fine’s Theorem on First-Order Complete Modal Logics

Fine’s influential Canonicity Theorem states that if a modal logic is determined by a first-order definable class of Kripke frames, then it is valid in its canonical frames. This article reviews the background and context of this result, and the history of its impact on further research. It then develops a new characterization of when a logic is canonically valid, providing a precise point of distinction with the property of first-order completeness. The ultimate point is that the construction of the canonical frame of a modal algebra does not commute with the ultrapower construction.

Algorithmic properties of first-order modal logics of finite Kripke frames in restricted languages

We study the effect of restricting the number of individual variables, as well as the number and arity of predicate letters, in languages of first-order predicate modal logics of finite Kripke frames on the logics’ algorithmic properties. A finite frame is a frame with a finite set of possible worlds. The languages we consider have no constants, function symbols or the equality symbol. We show that most predicate modal logics of natural classes of finite Kripke frames are not recursively enumerable—more precisely, $\varPi ^0_1$-hard—in languages with three individual variables and a single monadic predicate letter. This applies to the logics of finite frames of the predicate extensions of the sublogics of propositional modal logics $\textbf{GL}$, $\textbf{Grz}$ and $\textbf{KTB}$—among them, $\textbf{K}$, $\textbf{T}$, $\textbf{D}$, $\textbf{KB}$, $\textbf{K4}$ and $\textbf{S4}$.

Recursive enumerability and elementary frame definability in predicate modal logic

We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On one hand, it is well known that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e. a class of frames definable by a classical first-order formula, is recursively enumerable. On the other, numerous examples are known of predicate modal logics, based on ‘natural’ propositional modal logics with essentially second-order Kripke semantics, that are either not recursively enumerable or Kripke incomplete. This raises the question of whether every Kripke complete, recursively enumerable predicate modal logic can be characterized by an elementary class of Kripke frames. We answer this question in the negative, by constructing a normal predicate modal logic which is Kripke complete, recursively enumerable, but not complete with respect to an elementary class of frames. We also present an example of a normal predicate modal logic that is recursively enumerable, Kripke complete, and not complete with respect to an elementary class of rooted frames, but is complete with respect to an elementary class of frames that are not rooted.

KRIPKE COMPLETENESS OF STRICTLY POSITIVE MODAL LOGICS OVER MEET-SEMILATTICES WITH OPERATORS

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.

A Finite Model Property for Gödel Modal Logics

A new semantics with the finite model property is provided and used to establish decidability for Gödel modal logics based on (crisp or fuzzy) Kripke frames combined locally with Gödel logic. A similar methodology is also used to establish decidability, indeed co-NP-completeness, for a Gödel S5 logic that coincides with the one-variable fragment of first-order Gödel logic.

Four-valued modal logic: Kripke semantics and duality

Along the lines of recent investigations combining many-valued and modal systems, we address the problem of defining and axiomatizing the least modal logic over the four-element Belnap lattice. By this we mean the logic determined by the class of all Kripke frames where the accessibility relation as well as semantic valuations are four-valued. Our main result is the introduction of two Hilbert-style calculi that provide complete axiomatizations for, respectively, the local and the global consequence relations associated to the class of all four-valued Kripke models. Our completeness proofs make an extensive and profitable use of algebraic and topological techniques; in fact, our algebraic and topological analyses of the logic have, in our opinion, an independent interest and contribute to the appeal of our approach.