Overview
The classical Modal Logic Cube compares extensions of normal propositional modal logic K by combinations of the axioms D, T, B, 4, and 5. Of the 32 formal subsets of five axioms, 15 give distinct logics; the rest collapse to equivalent axiomatizations. Benzmüller, Claus and Sultana mechanised correspondence, inclusion, properness and small countermodels in Isabelle/HOL.
Five Frame Correspondences
| Axiom | Modal principle | Accessibility property |
|---|---|---|
| D | \Box p\to\Diamond p | Serial: \forall x\exists y\,Rxy |
| T | \Box p\to p | Reflexive: \forall x\,Rxx |
| B | p\to\Box\Diamond p | Symmetric: \forall x,y\,(Rxy\to Ryx) |
| 4 | \Box p\to\Box\Box p | Transitive: \forall x,y,z\,((Rxy\land Ryz)\to Rxz) |
| 5 | \Diamond p\to\Box\Diamond p | Euclidean: \forall x,y,z\,((Rxy\land Rxz)\to Ryz) |
Catalogue
| Logic | Defining extra axiom(s) | Local satisfiability |
|---|---|---|
| [[k | K]] | K only |
| [[kd | KD]] | D |
| [[kt | KT]] | T |
| [[kb | KB]] | B |
| [[kdb | KDB]] | D+B |
| [[b | B]] | T+B |
| [[k4 | K4]] | 4 |
| [[kd4 | KD4]] | D+4 |
| [[s4 | S4]] | T+4 |
| [[k5 | K5]] | 5 |
| [[kd5 | KD5]] | D+5 |
| [[k45 | K45]] | 4+5 |
| [[kd45 | KD45]] | D+4+5 |
| [[kb5 | KB5]] | B+5 |
| [[s5 | S5]] | T+5 |
Names and equivalences: KT is often called T; KTB is commonly called B; KT4 is S4; KT5 is S5; KB4 and KB5 are equivalent. SDL is a deontic reading of KD, not a new point of the cube.
Semantics and Metalogic
A model is M=(W,R,V) and M,w\models\Box\varphi iff \varphi holds at all R-successors of w. The cube compares logics by inclusion of their theorem sets, in the opposite direction to inclusion of their frame classes. Every cube logic has a finite model property. Complexity bounds here concern monomodal propositional local satisfiability and should not be transported automatically to quantified or multimodal variants.
Relation to Embedded Logics
Benzmüller et al. use a shallow embedding of modal formulas as predicates on worlds in classical higher-order logic. The embedding is a metalogical verification technique; it does not redefine K, T, S4 or S5 as higher-order modal languages.
References
- Christoph Benzmüller, Maximilian Claus, and Nik Sultana (2015). Systematic Verification of the Modal Logic Cube in Isabelle/HOL. PxTP 2015, EPTCS 186, 27–41. arXiv.
- Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, and Clare Dixon (2022). Local Reductions for the Modal Cube. IJCAR 2022. DOI.
- Richard E. Ladner (1977). The Computational Complexity of Provability in Systems of Modal Propositional Logic. SIAM J. Comput. 6(3), 467–480. DOI.
- Patrick Blackburn, Maarten de Rijke, and Yde Venema (2001). Modal Logic. Cambridge University Press.