Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library

Abstract

The present dissertation introduces the research project on HOLMS (\textbf{HOL} Light Library for \textbf{M}odal \textbf{S}ystems), a growing modular framework for modal reasoning within the HOL Light proof assistant. To provide an accessible introduction to the library, the fundamentals of modal logic are outlined first, followed by a concise manual for the proof assistant itself. The core contribution of this work on HOLMS is the development of a unified and modular strategy for proving adequacy theorems with respect to relational semantics directly within HOL Light for several normal modal systems, currently including K, T, K4, and GL. Adequacy theorems establish a formal connection between syntactic proof systems and their intended relational models, ensuring that derivable statements align with valid ones. This approach extends previous research on Gödel-Löb logic (GL) by two HOLMS developers. It also assesses the generality and compositionality of the completeness proofs in George Boolos' monograph \textit{The logic of provability}. Beyond theoretical contributions, HOLMS incorporates automated decision procedures and a countermodel constructor for K, T, K4, and GL, illustrating how general-purpose proof assistants can be effectively combined with research on labelled sequent calculi and key insights from correspondence and bisimulation theories. The implementation in HOL Light demonstrates the feasibility of mechanising modal reasoning in a flexible and robust manner, paving the way for further developments of the HOLMS framework.