We communicate here the most recent extension of HOLMS, our library for modal logics aimed at introducing automated modal reasoning within the HOL Light proof assistant. Based on a uniform proof strategy, we present a more refined formal proof of completeness for systems within and beyond the S5-normal modal cube, notably Gödel-Löb logic. We report on our development by adopting a measure of its modularity based on Strachey's distinction between parametric and ad hoc polymorphic code.
5,
6, 7]; properties of program executions [
These and many other examples show that the interest of computer science in modal logic extends beyond the boundaries of the so-called 5-normal cube, i.e. the class of normal modal logics obtained from the minimal axiomatic system by combining the axioms among D, T, B, 4, and 5. The proper inclusions between these systems can be summarised graphically in the cube shown in Figure 1.
For each system in the modal cube, it is possible to provide a proof of adequacy (soundness and completeness) for the standard relational semantics – also known as “possible worlds” or “Kripke” semantics – by applying in a uniform and modular way the canonical model method, followed by appropriate filtration lemmas specific to each system under consideration [ Brogi) https://github.com/Antonella-Bilotta/ (A. Bilotta); https://sites.google.com/unifi.it/maggesi/ (M. Maggesi); https://sysma.
CEUR
ceur-ws.org
D ∶ □ → ♦ T ∶ □ → B ∶ → 4 ∶ □ → □ 5 ∶ ♦ → ♦□ ♦□ GL ∶ □ (□ → ) → □
T D K
S4=T4
D4 K4
D5 K5
D45 K45
B=TB DB KB =DB5=D4B5 KB5=K4B5 =K4B obtain adequacy and the finite model property for GL and the systems within the 5-normal cube, as documented in [22, Ch. 5].
In the present work, we report on the latest update of our implementation of that proof strategy for completeness within the more general HOLMS framework, which currently covers the systems K, T, K4, S4, B, S5 and GL.
The latest version of
HOLMS is freely accessible from our repository and is archived on Software Heritage . The readme file from the git repository and the project webpage
provide some pointers to the main contents of the library.
Our HOLMS framework (HOL Light Library for Modal Systems) [23, 24] has incorporated from its inception a formalisation of the aforementioned adequacy proof with respect to finite models. Initially, this formalisation addressed solely GL [25, 26]. Subsequently, we extended it to encompass three additional normal systems within the cube: K, T, and K4. In the present setting, we present a further extension of it, covering the adequacy proofs and the decision procedures for S4, B and S5.
Our research pursuits with HOLMS are twofold, addressing both practical implementation and theoretical foundations.
From the practical perspective, we aim to enhance HOL Light’s capabilities in automated modal reasoning. The current version of HOLMS extends the proof assistant’s deductive apparatus by introducing a novel inference rule of the proof assistant (HOLMS_RULE). This rule determines whether a given input modal formula constitutes a theorem within a specified modal logic selected from K, T, K4, S4, B, S5 and GL. When the formula fails to qualify as a theorem, the rule generates an appropriate countermodel tailored to the established logic.1 The automation process is grounded in a shallow embedding of root-first proof search within the labelled sequent calculus associated with each logic 1The general mechanism provides a semi-decision procedure for K4. However, the literature on labelled sequent calculi ofers uniform solutions to this issue [27], which may be incorporated in future versions of HOLMS. under consideration [28, 29]. Henceforth, in HOLMS we have three interconnected presentations of normal modal logics: (i) axiomatic calculi, (ii) relational semantics (both deeply embedded), and (iii) labelled sequent calculi, which we shallow embed in the goal-stack mechanism of HOL Light as a certificate of correctness of the decision procedure behind HOLMS_RULE.
From the theoretical standpoint, we intend to develop the library according to a precisely defined modular architecture. Following a compositional implementation methodology, this development generalises our previous library for HOL Light. This methodology centres upon the previously referenced scalable and uniform proof of semantic adequacy. To precisely measure the proof modularity – and the same property of the associated formalisation – we implemented a precise coding discipline, inspired by [30]. In developing HOLMS, we have distinguished between: parametric polymorphic code, fully independent of specific parameter instantiations; and ad-hoc polymorphic code, whose components are tailored to the modal logic under consideration. We use that colour convention consistently throughout the following pages.2 Figure 2 summarises the modularity of the current version of our code, together with the specific files where each component is implemented. Here, * ranges over the diferent modal logics considered, that is * ∈ { , , 4 , 4 , , 5 , }.
Syntax Semantics Correspondence Theory Soundness Completeness Shallow Embedding Decision Procedure modal.ml modal.ml Concepts parametric_correspondence.ml Lemmata ad_hoc_correspondence.ml
gen_completeness.ml “Standard” Model gen_completeness.ml Truth Lemma gen_completeness.ml Counteromodel Lemma gen_completeness.ml “Standard” Relation *_completeness.ml Identification of the “Standard” Model *_completeness.ml Type Generalisation *_completeness.ml gen_decid.ml and *_decid.ml gen_decid.ml and *_decid.ml
In our formalisation of modal systems, HOL Light serves as the metatheory, while modal logics are treated as object logics. This distinction requires the embedding of an object language within HOL Light—to explicitly diferentiate between formal statements of the modal language (e.g. □ → □ ) and statements about modal systems in the metatheory (e.g. |- ∀. ⊢ 4 □ → □ ).
First, we define a grammar for modal formulas by an inductive definition . Next, we uniformly introduce axiomatic proof systems. To avoid code duplication in the embeddings of Hilbert calculi for normal modal logics, we define a ternary deducibility relation .ℋ ⊢ that is parametric to a set of axiom schemata and considers a set of hypotheses ℋ. Such a formal predicate conceptualises the abstract notion of deducibility close to the one discussed in [31], based on a minimal deductive system which extends the calculus – by including the axiom schema K ∶ □ ( → ) → ( □ → □ ) – and is modularly extended by instantiating .
Definition 1 (Proof system). The ternary predicate .ℋ ⊢ , denoting the deducibility of a formula from a set of hypotheses ℋ in an axiomatic extension of logic K via schemas in the set , is inductively defined by the following conditions: 2Notice that, although HOL Light lacks explicit mechanisms to support parametric and/or ad hoc polymorphism (unlike e.g. Isabelle/HOL), this distinction remains helpful in presenting the abstract structure of our (formalised) proof and discussing the potential portability of our results to proof assistants that implement this distinction through specific mechanisms. • For every instance of axiom schemas for the calculus , .ℋ ⊢ ; • For every instance of schemas in , .ℋ ⊢ ; • For every ∈ ℋ , .ℋ ⊢ ; • If .ℋ ⊢ → • If .∅ ⊢
and .ℋ ⊢ , then .ℋ ⊢ ; , then .ℋ ⊢ □ for any set of formulas ℋ.
For that deducibility relation, we provide a formal proof of Theorem 1 (Deduction theorem). following equivalence holds: .ℋ ∪ {} ⊢ if .ℋ ⊢ →
.
For any modal formulas , and any sets of formulas , ℋ , the
Moving to the semantics side, the current version of HOLMS contains the formalisation of basic notions of frames, relational models and validity therein via a forcing relation . Furthermore, we formalise the notion of validity in a class of frames .3 Next, we formalise results from correspondence theory [32] collected in the table from Figure 1 by also defining a general predicate CHAR representing the class of frames characteristic to the schema(s) . We leverage it for stating and proving Theorem 2 (Soundness). for . For every ∈
Form□ , if .∅ ⊢ then ⊨
.
Let be a set of axiom schemata. Let be the characteristic class of frames
From those results, we can easily prove the consistency of the proof systems introduced by Def. 1.
The current version of HOLMS includes a refined formal proof of semantic completeness of any system ∈ { , , 4 , 4 , , 5 ,
}. The modularity of the strategy from [22] lets us avoid code duplication in several parts of the implementation. The following ad-hoc polymorphic theorem then condenses the resulting completeness statement: Theorem 3 (Completeness). Let be a set of axiom schemata. Let be the characteristic class of finite frames for . For every ∈
Form□ , if ⊨ , then .∅ ⊢ .
Proof Sketch. We proceed by contraposition, and prove that—given a generic modal formula —if .∅ ⊬ , then ⊭
.
This means that for each set of axioms and for each modal formula , we have to find a countermodel ℳ
inhabiting , and a ‘counterworld’ inhabiting ℳ the argument in [22, Ch. 5] and implement the following key strategy. such that ⊮ℳ . To do so, we formalise Parametric part of the proof : 1. We identify a parametric notion of (counter)model ℳ in having: maximal consistent lists of modal formulas as possible worlds; an accessibility relation that verifies two given constraints; a valuation such that (, )
if is a subformula of and ∈ . (GEN_STANDARD_MODEL ) 2. We prove a general truth-lemma independent from the considered and . This step allows the reduction of the notion of forcing ( ⊩ ℳ ) to membership ( ∈ ). (GEN_TRUTH_LEMMA ) 3. We identify a ‘counterworld’ in ℳ
(GEN_COUNTERMODEL_ALT ) Ad hoc polymorphic part of the proof : such that ∉ and thus ⊮ ℳ .
I. For each system , identification of its specific countermodel ℳ , and in particular of its accessi3We refer to our previous [23] for the details of the implementation.
bility relation ; II. Verification that this model satisfies the following two technical requirements for : a. ⟨ , ⟩ ∈
( _MAXIMAL_CONSISTENT); b. for all ∈ Form□ , if □ is a subformula of then, for every ∈ for all ∈ , implies ∈ ( _ACCESSIBILITY_LEMMA). , □ ∈ if and only if,
As a technical aside, we notice that for step 2, we work on worlds that are lists of formulas without repetitions for purely practical reasons. Because of that choice, the formal proof of Theorem 3 establishes completeness w.r.t. frames sitting on the type-theoretic domain of formula lists. We overcome that annoying consequence of our implementation choice by applying a type-theoretic version of the bisimulation invariance lemma [33] (BISIMILAR_VALID ) which allows us to prove completeness w.r.t. any infinite domain – including formula sets commonly used in this kind of constructions – thanks also to the auxiliary lemma GEN_LEMMA_FOR_GEN_COMPLETENESS .
By HOLMS, we aim to equip a proof assistant with a uniform and compositional mechanism for decision procedures for modal logics. To achieve that, the mechanisation of completeness results we have presented here is a key step, independently of the logic under consideration.
In our development, we have been inspired by independent works that individually present relevant aspects such as the natural extensibility of decision procedures of [34, 35, 36, 37, 38, 39] and the analogous generality of the formal proofs of completeness via canonical model constructions exhibited in [40, 41]. By merging those aspects in a uniform framework, we have managed to mechanise in a modular, uniform, and general way six central systems of the modal cube (K, T, K4, S4, B, S5) – already captured independently by those works – plus Gödel-Löb logic, which is one of the most important systems beyond the modal cube. At the current stage, the HOLMS library also contains a fully formalised uniform proof of adequacy for the seven normal modal systems w.r.t. relational semantics.4
A basic future task is thus to extend HOLMS to the entire modal cube [44] and further provability logics [45].
Another goal is to support multimodal languages by indexing modal operators – treating current monomodal systems as a special case – thereby significantly enhancing the expressiveness of the framework and broadening its potential applications in software and system verification [ 46, 47], [48, 49], [50], [51].
We also aim to integrate deep embeddings of enriched sequent calculi and their metatheory. That implementation would enable using HOLMS for interesting proof-theoretic investigations and facilitate integration with external derivation-search tools.
Another direction is generalising HOLMS to non-normal modal logics (with neighbourhood semantics) [52, 53, 54] and intuitionistic/constructive modalities [55, 56, 57], which are increasingly relevant in computer science. This extension would require adapting our methods and relaxing the current parametric approach to semantic adequacy.
More importantly, we plan to apply our modular mechanisation of the completeness theorem(s) to improve the performance of the (semi)decision procedures in HOLMS to cover more eficiently our proof-search mechanism for the systems we have discussed in the previous pages. 4A diferent methodology based on shallow embeddings of modal reasoning in HOL is documented in [ 42, 43].
This work was partially funded by: the project SERICS – Security and Rights in CyberSpace PE0000014, ifnanced within PNRR, M4C2 I.1.3, funded by the European Union - NextGenerationEU (MUR Code: 2022CY2J5S, CUP: D67G22000340001); the Istituto Nazionale di Alta Matematica – INdAM group GNSAGA; the International Research Network “Logic and Interaction”; the EC-COST Action (CA20111) “EuroProofNet”; the research project “Diferential, Algebraic, Complex and Arithmetic Geometry (2025)”.
The authors have not employed any Generative AI tools. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) (2021) 275–282. URL: https://api.semanticscholar.org/CorpusID:237491844. [17] F. Rajaona, I. Boureanu, R. Ramanujam, S. Wesemeyer, Epistemic model checking for privacy, in: 2024 IEEE 37th Computer Security Foundations Symposium (CSF), IEEE Computer Society, Los Alamitos, CA, USA, 2024, pp. 1–16. URL: https://doi.ieeecomputersociety.org/10.1109/CSF61375. 2024.00020. doi:10.1109/CSF61375.2024.00020. [18] M. Gattinger, J. van Eijck, Towards model checking cryptographic protocols with dynamic epistemic logic, in: Proc. LAMAS, Citeseer, 2015, pp. 1–14. [19] M. Fitting, R. L. Mendelsohn, First-order Modal Logic. Second Edition, Springer, SYLI, volume 480, 2023. [20] R. L. Verbrugge, Provability Logic, in: E. N. Zalta, U. Nodelman (Eds.), The Stanford Encyclopedia of Philosophy, Summer 2024 ed., Metaphysics Research Lab, Stanford University, 2024. [21] G. Japaridze, D. De Jongh, The logic of provability, in: Handbook of Proof Theory. Studies in
Logic and the Foundations of Mathematics, volume 137, Elsevier, 1998, pp. 475–546. [22] G. Boolos, The logic of provability, Cambridge University Press, 1995. [23] A. Bilotta, M. Maggesi, C. Perini Brogi, L. Quartini, Growing HOLMS, a HOL Light Library for Modal Systems, in: D. Porello, C. Vinci, M. Zavatteri (Eds.), Short Paper Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2024, Bolzano, Italy, November 28-29, 2024, volume 3904 of CEUR Workshop Proceedings, CEUR-WS.org, 2024, pp. 41–48. URL: https://ceur-ws.org/Vol-3904/paper5.pdf. [24] A. Bilotta, M. Maggesi, C. Perini Brogi, A HOL Light Library for Modal Systems (HOLMS), https: //holms-lib.github.io/, 2025. Accessed: 2025-06-28. [25] M. Maggesi, C. Perini Brogi, A Formal Proof of Modal Completeness for Provability Logic, in: L. Cohen, C. Kaliszyk (Eds.), 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2021, pp. 26:1–26:18. URL: https://drops. dagstuhl.de/opus/volltexte/2021/13921. doi:10.4230/LIPIcs.ITP.2021.26. [26] M. Maggesi, C. Perini Brogi, Mechanising Gödel-Löb Provability Logic in HOL Light, J.
Autom. Reason. 67 (2023) 29. URL: https://doi.org/10.1007/s10817-023-09677-z. doi:10.1007/ S10817- 023- 09677- Z. [27] D. Garg, V. Genovese, S. Negri, Countermodels from sequent calculi in multi-modal logics, in: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, IEEE Computer Society, 2012, pp. 315–324. URL: https: //doi.org/10.1109/LICS.2012.42. doi:10.1109/LICS.2012.42. [28] S. Negri, Proofs and countermodels in non-classical logics, Logica Universalis 8 (2014) 25–60. [29] S. Negri, J. von Plato, Proof analysis: a contribution to Hilbert’s last problem, Cambridge University
Press, 2011. [30] C. Strachey, Fundamental concepts in programming languages, Higher-order and symbolic computation 13 (2000) 11–49. [31] M. Fitting, Proof methods for modal and intuitionistic logics, volume 169, Springer Science &
Business Media, 2013. [32] J. Van Benthem, Correspondence Theory, Springer Netherlands, Dordrecht, 2001, pp. 325–408.
URL: https://doi.org/10.1007/978-94-017-0454-0_4. doi:10.1007/978- 94- 017- 0454- 0_4. [33] C. Stirling, Bisimulation and logic, Cambridge Tracts in Theoretical Computer Science, Cambridge
University Press, 2011, p. 173–196. [34] C. Nalon, C. Dixon, U. Hustadt, Modal resolution: proofs, layers, and refinements, ACM Transactions on Computational Logic (TOCL) 20 (2019) 1–38. [35] C. Nalon, U. Hustadt, F. Papacchini, C. Dixon, Local reductions for the modal cube, in: International Joint Conference on Automated Reasoning, Springer International Publishing Cham, 2022, pp. 486–505. [36] C. Nalon, U. Hustadt, F. Papacchini, C. Dixon, Buy one get 14 free: Evaluating local reductions for modal logic, in: B. Pientka, C. Tinelli (Eds.), Automated Deduction – CADE 29, Springer Nature Switzerland, Cham, 2023, pp. 382–400. [37] D. Pattinson, N. Olivetti, C. Nalon, Resolution calculi for non-normal modal logics, in: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Springer, 2023, pp. 322–341. [38] U. Hustadt, F. Papacchini, C. Nalon, C. Dixon, Model construction for modal clauses, in: International Joint Conference on Automated Reasoning, Springer, 2024, pp. 3–23. [39] C. Nalon, Eficient theorem-proving for modal logics, in: A. Ciabattoni, D. Gabelaia, I. Sedlár (Eds.), Advances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024, College Publications, 2024, pp. 13–16. [40] A. H. From, Formalized soundness and completeness of epistemic logic, in: A. Silva, R. Wassermann, R. J. G. B. de Queiroz (Eds.), Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Virtual Event, October 5-8, 2021, Proceedings, volume 13038 of Lecture Notes in Computer Science, Springer, 2021, pp. 1–15. URL: https://doi.org/10.1007/ 978-3-030-88853-4_1. doi:10.1007/978- 3- 030- 88853- 4\_1. [41] A. H. From, An Isabelle/HOL Framework for Synthetic Completeness Proofs, in: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP ’25, Association for Computing Machinery, New York, NY, USA, 2025, p. 171–186. URL: https: //doi.org/10.1145/3703595.3705882. doi:10.1145/3703595.3705882. [42] C. Benzmüller, Faithful logic embeddings in HOL - A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level, CoRR abs/2502.19311 (2025). URL: https://doi.org/10.48550/arXiv.2502.19311. doi:10.48550/ARXIV. 2502.19311. arXiv:2502.19311. [43] C. Benzmüller, B. W. Paleo, Higher-order modal logics: Automation and applications, in: W. Faber, A. Paschke (Eds.), Reasoning Web. Web Logic Rules - 11th International Summer School 2015, Berlin, Germany, July 31 - August 4, 2015, Tutorial Lectures, volume 9203 of Lecture Notes in Computer Science, Springer, 2015, pp. 32–74. URL: https://doi.org/10.1007/978-3-319-21768-0_2. doi:10.1007/978- 3- 319- 21768- 0\_2. [44] R. Schmidt, Advances in Modal Logic Tools, Last modified: 03 Mar 23; Accessed: February 2025, 2025. URL: https://www.cs.man.ac.uk/~schmidt/tools/. [45] L. Mikec, Satisfiability verifiers for certain modal logics concerned with provability, Available at https://luka.doublebuffer.net/o/il/, 2025. URL: https://github.com/luka-mikec/provability_sat. [46] A. K. Simpson, Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS, J. Log. Algebraic Methods Program. 60-61 (2004) 287–322. URL: https://doi.org/10.1016/j. jlap.2004.03.004. doi:10.1016/J.JLAP.2004.03.004. [47] A. K. Simpson, Compositionality via cut-elimination: Hennessy-milner logic for an arbitrary GSOS, in: Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, IEEE Computer Society, 1995, pp. 420–430. URL: https: //doi.org/10.1109/LICS.1995.523276. doi:10.1109/LICS.1995.523276. [48] C. Perini Brogi, R. De Nicola, O. Inverso, Simpson’s proof systems for process verification: A fine-tuning (short paper), in: U. de’Liguoro, M. Palazzo, L. Roversi (Eds.), Proceedings of the 25th Italian Conference on Theoretical Computer Science, Torino, Italy, September 11-13, 2024, volume 3811 of CEUR Workshop Proceedings, CEUR-WS.org, 2024, pp. 292–299. URL: https: //ceur-ws.org/Vol-3811/paper050.pdf. [49] G. Costa, C. Perini Brogi, Toward dynamic epistemic verification of zero-knowledge protocols, in: G. D’Angelo, F. L. Luccio, F. Palmieri (Eds.), Proceedings of the 8th Italian Conference on Cyber Security (ITASEC 2024), Salerno, Italy, April 8-12, 2024, volume 3731 of CEUR Workshop Proceedings, CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3731/paper25.pdf. [50] S. Docherty, R. N. Rowe, A non-wellfounded, labelled proof system for propositional dynamic logic, in: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Springer, 2019, pp. 335–352. [51] M. Acclavio, F. Montesi, M. Peressotti, On propositional dynamic logic and concurrency, arXiv preprint arXiv:2403.18508 (2024). [52] T. Dalmonte, N. Olivetti, S. Negri, Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi, in: Advances in Modal Logic 2018, 2018. [53] M. Girlando, S. Negri, N. Olivetti, V. Risch, Conditional beliefs: from neighbourhood semantics to sequent calculus, The review of symbolic logic 11 (2018) 736–779. [54] T. Dalmonte, N. Olivetti, G. Pozzato, C. Terrioux, HYPNO theorem proving with hypersequent calculi for non-normal modal logics, Available at http://193.51.60.97:8000/HYPNO/, 2025. [55] A. Das, I. van der Giessen, S. Marin, Intuitionistic Gödel-Löb logic, à la Simpson: Labelled systems and birelational semantics, in: A. Murano, A. Silva (Eds.), 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 19-23, 2024, Naples, Italy, volume 288 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, pp. 22:1–22:18. URL: https://doi.org/10. 4230/LIPIcs.CSL.2024.22. doi:10.4230/LIPICS.CSL.2024.22. [56] A. Das, S. Marin, On intuitionistic diamonds (and lack thereof), in: International Conference on
Automated Reasoning with Analytic Tableaux and Related Methods, Springer, 2023, pp. 283–301. [57] M. Girlando, M. Morales, MOILab: a prototype theorem prover for intuitionistic modal logic IK based on labelled sequents, Available at https://www.mariannagirlando.com/MOILab.html, 2025.