(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.
Showing posts with label Intuitionistic Modal Logic. Show all posts
Showing posts with label Intuitionistic Modal Logic. Show all posts
Tuesday, 29 November 2022
Discussing "A Framework for Intuitionistic Modal Logics (Extended Abstract)"
Wednesday, 2 November 2022
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.
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.
Subscribe to:
Posts (Atom)