Discussing "A Framework for Intuitionistic Modal Logics (Extended Abstract)"

(Link)

Authors: Gordon Plotkin and Colin Stirling (Edinburgh University)

Reference: Plotkin, Gordon, and Colin Stirling. "A framework for intuitionistic modal logics (Extended abstract)". Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pp. 399-406. 1986.

Why this paper? Cited by A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals, Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement, and Intuitionistic versions of modal fixed point logics

Eight years before Alex Simpson’s thesis, which I discussed on this blog just four weeks ago, comes this extremely short (8 pages in a fairly large font!) but groundbreaking paper on intuitionistic modal logics. This paper is specifically the first to look at possible world semantics, also called Kripke semantics after its inventor Saul Kripke, for such logics. I will not repeat the things I said about intuitionistic modal logics in my previous post, but rather focus on this topic of possible worlds semantics.

Classically the truth of a proposition can be calculated based on ‘truth tables’, through which logical connectives can be seen as functions from the propositions they apply to. For example, negation is the function mapping True to False and False to True. The modal connectives Box and Diamond, for necessity and possibility respectively, are not truth-functional in this way. Instead we give meaning to our new connectives by relativising truth to a set of possible worlds, in which a certain proposition might be true in some, but false in others. In fact, a mere set of worlds is not enough; in order to talk sensibly about applying modalities on top of each other, we need to know how the worlds are arranged with respect to relative notions of possibility. For example, if the world Earth-One can be imagined as possible from the world Earth-Prime, does it follow that the inhabitants of Earth-One can imagine the world Earth-Prime? If all worlds have this symmetry, this corresponds to the axiom ‘B’, which states that if a proposition holds, then it necessarily possibly holds. Piling up modalities in this style can, frankly, strain our intuitions, but possible worlds semantics makes things transparent by asking to define the relationship between worlds as part of our definition.

One cool thing about possible worlds semantics is that intuitionistic logic, the logic of constructive reasoning, can also be seen through this lens. Worlds are now viewed as ‘states of knowledge’ and moving from one world to another corresponds to gaining knowledge, for example by discovering a proof of a new mathematical theorem. This setup allows us to give sound and complete semantics for intuitionistic logic (and in particular, its implication connective) within normal mathematics.

What if we wanted to combine the two flavours of logic? Plotkin and Sterling quite correctly predicted that this could have computational significance, an ongoing subject of my own (and others’) work to this day. The aim of this paper was to work out some details of how the Kripke semantics should work for this combination, with an emphasis more on working out a technically reasonable suggestion than on making a philosophical argument. Their suggestion is to have one set of worlds with two relations, one for the modal connectives and one for intuitionistic implication. However possible worlds semantics for intuitionistic logic have the crucial property that moving between worlds cannot falsify previously established truths, but only introduce new ones. If the two relations on worlds are unrelated, this property fails, and so work needs to be done to make them harmonise. A minimal logic (Intuitionistic K, where the K stands for Kripke) is established for these semantics, and some axiomatic extensions such as the B axiom are considered.