Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5

(Link).

Authors: Björn Lellmann (Imperial College London) and Dirk Pattinson (Imperial College London / Australian National University).

Conference: Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013), Nancy, France, 16-19 September, 2013.

Journal reference: Lecture Notes in Computer Science, to appear.

Comments: This is a paper that Google Scholar Updates surely wouldn't have recommended to me a couple of weeks ago; recall that Updates uses one's papers as 'search terms' to direct its recommendations of new work to you. This paper has little in common with most of my existing papers, but it has clear (albeit somewhat shallow) similarities with my brand new paper 'Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic' (pdf), co-authored with Jeremy Dawson, Rajeev Goré, and Alwen Tiu, which I will be presenting at the conference CSL 2013 in September. I also must note that one of the authors of this paper, Dirk Pattinson, has an office in the same corridor as me at Australian National University; in this new world we apparently need big data algorithms to tell us to read the work of our colleagues next door!

A mathematical proof involves starting with agreed-upon axioms, applying agreed-upon inference rules, and reaching a conclusion; this is a rather basic definition, but leads us to the really important questions for a logician - what axioms? And what inference rules? One broad approach, called Hilbert calculi, require that only an extremely small and fixed set of inference rules be used: in the simplest systems the single rule Modus Ponens alone suffices, although with modal logic, the topic of this week's paper, a couple more are needed. All the action with Hilbert calculi is in their axioms, in the sense that many different logics developed for all sorts of different purposes may have the same inference rule(s) but very different axioms. Hilbert calculi have their charms - they can be a very concise way to present a logic, for example - but they are not much fun to construct actual proofs with, as proofs of even apparently simple tautologies can be lengthy and highly unintuitive.

To get a more structured proof system that helps both humans and machines to generate proofs, the opposite approach tends to be more helpful: more structured proof systems tend to have very few axioms - often the fact that every proposition entails itself is enough - but many inference rules. Such structured proof systems come in various styles, including natural deduction, tableau, and sequent calculus, the topic of this paper, and also of my CSL paper which has surely prompted this recommendation (broadly, these proof systems differ in the style in which the inference rules are designed and organised).

One last piece of preamble is needed before we consider this week's paper; modal logic refers to any logic involving 'modalities' that modify propositions. For example, if 'p' is a statement that might be true or false ("it is raining"), we can preface it with a range of modalities: "it is possible that", "I believe that", "I know that", "in the future it will hold that", and so on. If such modalities have any plausible logical content - e.g. you can form a deductive argument in which "it is possible that" forms an important part - then we can design a modal logic that captures this logical content, via Hilbert axioms, sequent calculus, or whatever other proof style appears most suited.

This paper concerns the translation back and forth between Hilbert calculi axioms and sequent calculi rules for modal logic. The details of this translation are far too involved to summarise adequately in this blog post, but a key wrinkle in the development is to precisely identify certain classes of axioms with certain classes of rules; these classes relate to how many modalities must be piled up on top of one proposition to describe the logic. These distinctions support the 'limitative' results of the final section of the paper, which uses the translation to show that certain modal logics (defined via Hilbert calculi) cannot be captured by certain types of sequent calculus.