Event Detail

I will explain the background of my recent collaboration with Wes Holliday. It is well known among modal logicians that while “naturally” obtained modal logics tend to be Kripke complete, things look very differently when one looks at the class of all modal logics. In the 1970’s, S.K. Thomason found a fundamental reason why this phenomenon is unavoidable: modal consequence over Kripke frames is every bit as complex as full second-order consequence. Shortly afterward, Wim Blok proved another amazing result: even those logics that are complete tend to be surrounded by uncountably many incomplete ones, which are sound wrt precisely the same class of Kripke structures. Kripke incompleteness turned out to be much more of a norm than anybody had expected; and in a very precise sense, the problem is irreparable, at least as long as the notion of proof remains decidable.

A question then arises if some sensible generalization of Kripke semantics would make the phenomenon of incompleteness disappear. In a way, the answer was known even before Kripke frames dominated the picture: every modal logic is complete wrt Boolean Algebras with Operators (BAOs). As it turns out, this is the best general completeness result we can hope for. It is possible to find naturally motivated semantics properly contained between Kripke semantics and algebraic semantics which do not suffer from the “Thomason effect”: the induced notion of consequence can be axiomatized. However, as soon as these notions nontrivially depart from the full generality of algebraic semantics and try to capture at least some of the defining properties of Kripke frames, not only can one still find examples of incomplete logics, but the limitative result of Blok survives.

These questions were investigated in my PhD dissertation a decade ago, building on several decades of work in the modal community. By the time the dissertation was completed, there was still one possible escape route left: one of the three defining properties of (dual algebras of) Kripke frames could perhaps allow a general completeness result. More recently, Wes Holliday’s work on “possibility semantics” for modal logic rekindled the interest in that particular notion of completeness. Now we have found that even this escape route is blocked. Furthermore, the story turns out to involve an unjustly forgotten example, paper and program of Johan van Benthem.