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.

Discussing "The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics"

 (Link)

Author: Arnon Avron (Tel Aviv University)

Reference: Arnon Avron. The method of hypersequents in the proof theory of propositional non-classical logics. In Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss, editors, Logic: From Foundations to Applications: European Logic Colloquium, page 1–32. Clarendon Press, USA, 1996.

Why this paper? Cited by Nested Sequents for First-Order Modal Logics via Reachability Rules and Falsification-Aware Calculi and Semantics for Normal Modal Logics Including S4 and S5

This paper returns us to the world of structural proof theory, and in particular the sequent calculus, a formalism for organising and (often) generating proofs in various logics. The `various logics’ part of that phrase is very important here – there are a huge number of different logics out there, capturing different notions of truth and ways of combining propositions. Unfortunately many of these logics do not, in any obvious way, lend themselves to a well behaved sequent calculus. This paper reviews some work on a more flexible generalisation of sequent calculus based on hypersequents.

A sequent is simply a list of assumptions (or premises) and a list of conclusions. Working with a list of all current assumptions is very natural, but a list of conclusions may seem more unusual. The intuition is to view that list as disjunctive, i.e. proving any one of the conclusions will do. Working with a list of conclusions rather than a single one is not necessary for every logic, but turns out to be important for some. Similarly, hypersequents are simply a list of sequents, typically viewed as a disjunction. As for standard sequents, this is pointless for some logics but does allow other logics to be handled that would otherwise resist a nice structural treatment. The magic of this is that we can create new proof rules that allow sequents to communicate with each other within the hypersequent, for example by exchanging conclusions between them, in ways that allow the proof of new theorems.

Hypersequent calculi are shown to exist for a variety of interesting logics. We see Gödel–Dummett logic, also known as Dummett’s LC, a logic in which propositions can be assigned a position on an infinitely long truth spectrum, with one proposition implying another if the second proposition is ‘more true’ than the first; the relevance logic RM, which can be understood via the Sugihara matrix - truth values range across the integers, with the non-negative integers designated as ‘true’, and logical negation exactly matching the negation of integers; S5, a long established member of the family of modal logics that resisted the toolkit of standard proof theory; and a couple of three-valued logics which allow for a single intermediate position between absolute truth and falsity.

Discussing "Structural Proof Theory"

(Link)

Authors: Sara Negri and Jan von Plato (University of Helsinki)

Reference: Negri, Sara, and von Plato, Jan. Structural proof theory. Cambridge University Press, 2001.

Why this book? Cited by Two-sided Sequent Calculi for FDE-like Four-valued Logics and Proof Theory for Intuitionistic Temporal Logic

There has been an unplanned delay to the blog, as two weeks ago there were not enough new recommendations appearing in Google Scholar to recommend any ‘classic papers’ for me to review via their citations, and then one week ago we got this book, which took me a small while to track down. I therefore expect to post twice this week.

A `structural’ proof is one that proceeds via a set of inference rules that forces one to arrange one’s proof in a tree-like structure, using only a limited set of inference rules and axioms. These inference rules generally reflect the logical connectives used to state the proposition one is trying to prove.  For example, to prove a conjunction one `branches’ to prove each side of the conjunction separately. This may seem a mundane or obvious notion, but is actually very young with respect to the long history of logic, originating with Gerhard Gentzen in the 1930s. The structural approach allows one to study the space of proofs for a given logic as an object of mathematical interest in its own right (hence, proof theory) and can help with finding proofs.

The two important systems for structural proof are natural deduction and sequent calculus, both originating with Gentzen. Natural deduction is intended to reflect the natural way in which one reasons logically, and is an important concept in computer science due to its relationship with types: according to the Curry-Howard isomorphism, programs with a given type can be viewed as natural deduction proofs of a certain proposition, and vice versa. Sequent calculus is a slightly less natural notion where one works on `sequents’ which allow one to manipulate one’s premises as well as one’s conclusion(s). This turns out to be an ideal setting in which to study the space of all proofs for a logic, and can support automated proof search and help to demonstrate that non-theorems are not provable. While the two approaches differ, they also have many similarities; for example, both have a notion of an algorithm (called normalisation or reduction for natural deduction, and cut-elimination for sequent calculus) that automatically simplifies unnecessarily complex or indirect proofs.

This book is a careful development of various notions of natural deduction and sequent calculus for classical, intuitionistic, and intermediate logic, including propositions, predicates, equality, and ‘nonlogical rules’ that give one access to the axioms of various parts of logic. Full proof details are given throughout the book, a number of new results are presented alongside the classic results, and care is taken to place ideas in their historical context. The high level of detail make this a less breezy read than, say, Girard’s Proofs and Types, but it is in invaluable tool to anyone working in the area.