|  | |||||||||
Relations between propositional normal modal logics:
an overview
Rajeev Gor?e ? Wolfgang Heinle y Alain Heuerding y
?Automated Reasoning Project yInstitut fur Informatik
Australian National University und angewandte Mathemetik
Canberra, Australia University of Bern
[email protected] Bern, Switzerland
fheinle, [email protected]
Abstract
The modal logic literature is notorious for multiple axiomatisations of the same logic and
for conflicting overloading of axiom names. Many of the interesting interderivability results
are still scattered over the often hard to obtain classics. We catalogue the most interesting
axioms, their numerous variants, and explore the relationships between them in terms of
interderivability as both axiom (schema) and as simple formulae. In doing so we introduce
the Logics Workbench (LWB, see http://lwbwww.unibe.ch:8080/LWBinfo.html), a versatile
tool for proving theorems in numerous propositional (nonclassical) logics. As a side effect we
fulfill a call from the modal theorem proving community for a database of known theorems.
1 Introduction
The modal logic literature is quite diverse but most beginners turn to the introductory works by Hughes and Cresswell [HC68, HC84], Bull and Segerberg [BS86], Lemmon and Scott [LS77], or Chellas [Che80]. The classic by Segerberg [Seg71] is indispensable but is probably the hardest to get hold of (legally). Unfortunately the nomenclature used in these works is not uniform, and the proof techniques range from semantic, to proof-theoretic, to algebraic. Consequently, it is difficult to form a clear picture of the many interesting results contained in these works, and even harder to keep track of the many different versions of the basic axioms, their different names, and even the overloading of names. In what follows we try to give a general picture of this nomenclature, the interesting interconnections between some of these logics, and the interderivability of different axiomatisations of the same logic.
Our basic tool is the Logics Work Bench (LWB) [HJSS95], a program developed at the University of Bern that contains automated proof procedures based on modal Gentzen systems for numerous propositional (nonclassical) logics. Although the class of modal logics which have been automated in the LWB is relatively small, namely K, KT, KT4, KT45 and KW, we can work with extensions of these logics by using a finite number of appropriate formula instances of the desired axioms, as explained below.
2 Definitions and Notational Conventions
We assume that formulae are built as usual from the classical connectives ^, _, !, :, >, ? and the modal connectives ? and ?. The binding strengths of the connectives from strongest to weakest is: :, ?, ?, ^, _, !. Hence :A_B ! C is read as ((:A)_B) ! C. We also assume that ! associates so that A ! B ! C is to be read as A ! (B ! C). We use ` to denote derivability in a Hilbert system for a particular modal logic. This notation has been chosen carefully to avoid
?Work supported by a visiting fellowship from the IAM. Tableaux-96 version: October 18, 1995