Discussing "The Proof Theory and Semantics of Intuitionistic Modal Logic"

(Link)

Author: Alex K. Simpson (University of Edinburgh)

Reference: Simpson, Alex K. "The proof theory and semantics of intuitionistic modal logic.", PhD dissertation, University of Edinburgh (1994).

Why this paper? Cited by When programs have to watch paint dry, Wijesekera-style constructive modal logics, and Nested Sequents for First-Order Modal Logics via Reachability Rules

Computer science PhD dissertations, despite being an important part of academic life, are seldom widely read – the work is usually split into more digestible publications in journals and conference proceedings. There are exceptions, however, where the dissertation transcends merely being a stapled-together collection of papers to instead provide a comprehensive overview of a subject at a point of time. This dissertation, with its 557 citations as measured by (the sometimes slightly inaccurate) Google Scholar, is certainly an example of such.

The topic of the dissertation is the merge of intuitionistic logic and modal logic. Intuitionistic logic arose from the constructive mathematics of Brouwer, in which the notion of proof is elevated above the more mysterious notion of mathematical truth. Taking this as our basic logic requires a more restricted logic than is usually accepted, as we reject e.g. double negation elimination, as demonstrating the absence of a disproof does not entail the existence of a proof. Constructivism has become an important topic in computer science because the central concern of our discipline is that which can be constructed (via algorithm). Modal logic is the logic of possibility, necessity, and similar logical connectives. After Kripke (who recently passed away) we think of them as connectives which allow us to discuss `possible worlds’ – a certain thing may be true, but it is only necessarily true if it holds at all possible worlds.

Combining these two logics is a natural thing to do to allow modal connectives to be used in an intuitionistic setting, and has a number of computer science applications, including some that I have published on. The sticking point turns out not to be the ‘box’ operator for necessity (regarding all possible worlds), which has been translated to the intuitionistic setting without controversy many times, but rather the ‘diamond’ operator of possibility (regarding the existence of at least one possible world). Simpson’s first order of business is to survey the literature and make an argument for a particular approach to diamond, which has a range of desirable properties such as distribution over disjunction (if it is possible that A or B holds, then either it is possible that A holds, or possible that B holds).

The bulk of the dissertation revolves around structural proof theory, with natural deduction emphasised. Simpson builds the notion of possible worlds into his proof theory, with explicit requirements to show that certain worlds are possible (more technically, that one world is ‘reachable’ from another). The proof theory is shown to have good properties such as (various notions of) soundness and completeness, and strong normalisation (one can define a proof simplification procedure that is guaranteed to terminate). Most interestingly the proof theory is highly flexible, as a variety of modal logics, differentiated by different notions of the structure of possible worlds, can fit into Simpson’s framework via certain rules that reflect the semantic structure into the proof theory.