Library-Grade Modal Logic

Abstract

Modal logic comprises a broad family of logics to reason about relational structures. The literature presents many such logics, displaying diverse operators, semantics, and applications. This plurality is reflected in a zoo of mechanised modal logics, which often duplicate syntax, semantics, metatheory, and reasoning infrastructure. We present a library-grade formalisation of modal logic in Lean, developed as part of CSLib (the Lean Computer Science Library) and designed around two complementary forms of reuse: vertical reuse, whereby specialised logics inherit from common abstractions, and horizontal reuse, whereby modal logic becomes a reasoning tool for independently formalised domains. Our development provides a generic framework for polyadic modal languages, reusable metatheory and proof automation, and derived interfaces for specialised modal logics. We exemplify our infrastructure by deriving basic modal logic, basic temporal logic, and Hennessy-Milner Logic; the latter subsumes and extends CSLib's previous implementation while reducing its logic-specific code by 67%. We further apply the same modal infrastructure to reasoning about mathematics (radicals of ideals), theory of programming languages (the type safety strategy for the simply typed $λ$-calculus), and concurrency theory (reasoning about processes in the Calculus of Communicating Systems). Our experience suggests that reuse, automation, and integration with the strong Lean ecosystem should be treated as first-class design concerns when formalising theories for shared libraries.