HOLMS: A HOL Light Library for Modal Systems

(c) Copyright, Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini 2024.
(c) Copyright, Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi 2025-2026.

See the website for a brief overview of our HOLMS library, its evolution, and an introductory guide to the HOL Light theorem prover.

This repository contains HOLMS (HOL-Light Library for Modal Systems), a modular framework designed to implement modal reasoning within the HOL Light proof assistant.

At its current stage, nine modal system and their adequacy proofs are now implemented in HOLMS:

• K the minimal system is developed in k_completeness.ml;
• D in d_completeness.ml;
• T in t_completeness.ml;
• K4 in k4_completeness.ml;
• S4 in s4_completeness.ml;
• B in b_completeness.ml;
• S5 in s5_completeness.ml;
• GL provability logic is developed in gl_completeness.ml;
• Grz features two adequacy proofs: the first in grz_boolos.ml, following Boolos's proof for this system, and the second in grz_modular.ml, where we extend the modular proof strategy to this system using axiom of dependent choice (dep_choice.ml).

HOLMS provides a robust framework for modal reasoning in HOL, offering both high confidence and full automation. It implements the essential mathematical components for principled decision algorithms across various modal systems.

The prototypical automated theorem prover and certified countermodel constructor for GL and the modal cube (implemented for example in k_decid.ml, t_decid.ml, and gl_decid.ml) shows how proof assistants can be successfully combined with enriched sequent calculi, and formalised mathematics.

Moreover we have experimented with an other implementation technique for decision: modal translation. This approach is illustrated for Grz (grz_modular.ml, translations.ml) by embedding Grz into GL and repurposing GL's decision procedure.

The top-level file is make.ml.

Main Theorems

For each normal system $S$ implemented in HOLMS, we prove the following main theorems in its file `S_completeness.ml:

• 1. Identification of the set of frames appropriate to $S$
     proves that a certain set of finite frames $C$, distinguished by a certain property of the accessibility relation, is the set of frames appropriate to $S$; i.e. for each frame in this set if a modal formula $p$ is a theorem of $S$, then $p$ is valid in it.
     $C = \mathsf{APPR}(S)$ and equivalently $\forall F \in C\ (\mathcal{S}. \varnothing \vdash p \implies F \vDash p) \ and \ \forall F\ ((\mathcal{S}. \varnothing \vdash p \implies F \vDash p) \implies F \in C)$ (APPRS_APPR_S)
• 2. Soundness of $S$ with respect to $\mathsf{APPR}(S)$
     proves that if something is a theorem of $S$, then it is valid in its set of appropriate frames.
     $\forall p\ (\mathcal{S}. \varnothing \vdash p \implies \mathsf{APPR}(S) \vDash p)$ (S_APPRS_VALID)
• 3. Consistency of S
     proves that $S$ cannot prove the false.
     $\mathcal{S}. \varnothing \not \vdash \bot$ (S_CONSISTENT)
• 4. Completeness of $S$ related to $\mathsf{APPR}(S)$
     proves that if something holds in the set appropriate to $S$, then it is a theorem of $S$.
     $\forall p\ (\mathsf{APPR}(S) \vDash p \implies \mathcal{S}. \varnothing \vdash p)$ (S_COMPLETENESS_THM)

For example, in t_completeness.ml we prove: (1) RF_APPR_T; (2) T_RF_VALID; (3) T_CONSISTENT; (4) T_COMPLETENESS_THM.

Moreover, HOLMS implements fully automated theorem prover and countermodel constructor for the modal logics $K, T, K4$, and $GL$:

• HOLMS_RULEautomatically proves theorems of these systems;
• HOLMS_BUILD_COUNTERMODEL outputs a countermodel if the given formula is not a theorem of the logic under analysis.

To generalise and parametrise the proofs of completeness for normal systems as much as possible, we develop four main theorems in gen_completeness.ml:

1. GEN_TRUTH_LEMMA;
2. GEN_ACCESSIBILITY_LEMMA;
3. GEN_COUNTERMODEL_ALT ;
4. GEN_LEMMA_FOR_GEN_COMPLETENESS.

Usage guide and source code

Axiomatic Calculus

We define a ternary predicate $\mathcal{S}.\mathcal{H} \vdash p$, which denotes the derivability of a modal formula $p$ from a set of hypotheses $\mathcal{H}$ in an axiomatic extension of logic K via schemas in the set $\mathcal{S}$.

Notice that, by doing so, we conceptualise derivability from $\mathcal{H}$ in $\mathcal{S}$ as derivability from $\mathcal{H}$ in a minimal axiomatic system K that is extended by additional axiom schemas in $\mathcal{S}$.

We inductively define the axioms of the minimal calculus K (K_AXIOMS).

let KAXIOM_RULES,KAXIOM_INDUCT,KAXIOM_CASES = new_inductive_definition
  `(!p q. KAXIOM (p --> (q --> p))) /\
   (!p q r. KAXIOM ((p --> q --> r) --> (p --> q) --> (p --> r))) /\
   (!p. KAXIOM (((p --> False) --> False) --> p)) /\
   (!p q. KAXIOM ((p <-> q) --> p --> q)) /\
   (!p q. KAXIOM ((p <-> q) --> q --> p)) /\
   (!p q. KAXIOM ((p --> q) --> (q --> p) --> (p <-> q))) /\
   KAXIOM (True <-> False --> False) /\
   (!p. KAXIOM (Not p <-> p --> False)) /\
   (!p q. KAXIOM (p && q <-> (p --> q --> False) --> False)) /\
   (!p q. KAXIOM (p || q <-> Not(Not p && Not q))) /\
   (!p q. KAXIOM (Box (p --> q) --> Box p --> Box q))`;;

Then, we inductively introduce the derivability relation of our calculus (MODPROVES).

let MODPROVES_RULES,MODPROVES_INDUCT,MODPROVES_CASES =
  new_inductive_definition
  `(!H p. KAXIOM p ==> [S . H |~ p]) /\
   (!H p. p IN S ==> [S . H |~ p]) /\
   (!H p. p IN H ==> [S . H |~ p]) /\
   (!H p q. [S . H |~ p --> q] /\ [S . H |~ p] ==> [S . H |~ q]) /\
   (!H p. [S . {} |~ p] ==> [S . H |~ Box p])`;;

Deduction Lemma

This lemma guarantees the reduction of the common notion of derivability of modal formula $p$ in an axiomatic calculus characterised by the axiom schemata in S $\mathcal{S} \vdash p$ to the ternary relation $\mathcal{S}.\mathcal{H} \vdash p$.

MODPROVES_DEDUCTION_LEMMA
|- !S H p q. [S . H |~ p --> q] <=> [S . p INSERT H |~ q]

Kripke's Semantics of formulae

We define, by induction on the complexity of a formula, that a certain modal formula $p$ holds in a certain world $w$ of a certain model $\langle W, R, V\rangle$.
$w \Vdash_{\langle W, R, V\rangle} p$

let holds =
  let pth = prove
    (`(!WP. P WP) <=> (!W:W->bool R:W->W->bool. P (W,R))`,
     MATCH_ACCEPT_TAC FORALL_PAIR_THM) in
  (end_itlist CONJ o map (REWRITE_RULE[pth] o GEN_ALL) o CONJUNCTS o
   new_recursive_definition form_RECURSION)
  `(holds WR V False (w:W) <=> F) /\
   (holds WR V True w <=> T) /\
   (holds WR V (Atom s) w <=> V s w) /\
   (holds WR V (Not p) w <=> ~(holds WR V p w)) /\
   (holds WR V (p && q) w <=> holds WR V p w /\ holds WR V q w) /\
   (holds WR V (p || q) w <=> holds WR V p w \/ holds WR V q w) /\
   (holds WR V (p --> q) w <=> holds WR V p w ==> holds WR V q w) /\
   (holds WR V (p <-> q) w <=> holds WR V p w <=> holds WR V q w) /\
   (holds WR V (Box p) w <=>
    !w'. w' IN FST WR /\ SND WR w w' ==> holds WR V p w')`;;

We say that a formula $p$ holds in a certain frame iff it holds for every model in every world of that frame.
$\langle W, R\rangle \vDash p \iff \forall V\ (\forall w \in W\ (w \Vdash_{\langle W, R, V\rangle} p$))

let holds_in = new_definition
  `holds_in (W,R) p <=> !V w:W. w IN W ==> holds (W,R) V p w`;;

We say that a formula $p$ is valid in a class of frames iff it holds in every frame of this class.
$L \vDash p \iff \forall \langle W,R \rangle \in L\ (\langle W,R \rangle \vDash p)$

let valid = new_definition
  `L |= p <=> !f:(W->bool)#(W->W->bool). f IN L ==> holds_in f p`;;

The innovative definition of Kripke's model stands on the notion of modal frame, namely an ordered pair where the first object is a non-empty set (domain of the possible worlds) and the second one is a binary relation on the first set (accessibility relation).

let FRAME_DEF = new_definition
  `FRAME = {(W:W->bool,R:W->W->bool) | ~(W = {}) /\
                                       (!x y:W. R x y ==> x IN W /\ y IN W)}`;;

Theory of Correspondence

We define the set of frames appropriate to S, i.e. the set of all the finite frames such that if p is a theorem of S, then p holds in this frame.
{ $\langle W,R \rangle \in \mathtt{FINITE\textunderscore FRAMES}| \forall p\ (\mathcal{S}. \varnothing \vdash p \implies \langle W,R \rangle \vDash p)$ }

let APPR_DEF = new_definition
  `APPR S = {(W:W->bool,R:W->W->bool) |
             (W,R) IN FINITE_FRAME /\
             (!p. [S. {} |~ p] ==> holds_in (W,R) p)}`;;

For each one of the normal system S developed in HOLMS we prove what set of frames is appropriate to S ( $C = \mathsf{APPR}(S)$ ), i.e. we prove that every frame that is in C is appropriate to S ($\subseteq$: $\forall F \in C\ (\mathcal{S}. \varnothing \vdash p \implies F \vDash p)$ ) and that every frame that is appropriate to S is in C ($\supseteq$: $\forall F\ ((\mathcal{S}. \varnothing \vdash p \implies F \vDash p) \implies F \in C)$ ).

K-Finite Frames

We prove that the set of finite frames is the one appropriate to $K$.

FINITE_FRAME_APPR_K
|- FINITE_FRAME:(W->bool)#(W->W->bool)->bool = APPR {}

D-Finite Serial Frames (SERF)

We prove that the set of finite serial frames is the one appropriate to $D$.

let D_AX = new_definition
  `D_AX = {Box p --> Diam p | p IN (:form)}`;;

let SERF_DEF = new_definition
 `SERF =
  {(W:W->bool,R:W->W->bool) |
    (W,R) IN FINITE_FRAME /\
    (!w:W. w IN W ==> ?y:W. y IN W /\ (R w y))}`;;

SERF_APPR_D
|- SERF: (W->bool)#(W->W->bool)->bool = APPR D_AX

T-Finite Reflexive Frames (RF)

We prove that the set of finite reflexive frames is the one appropriate to $T$.

let T_AX = new_definition
  `T_AX = {Box p -->  p | p IN (:form)}`;;

let RF_DEF = new_definition
 `RF =
  {(W:W->bool,R:W->W->bool) |
   ~(W = {}) /\
   (!x y:W. R x y ==> x IN W /\ y IN W) /\
   FINITE W /\
   (!x. x IN W ==> R x x)}`;;

RF_APPR_T
|- RF: (W->bool)#(W->W->bool)->bool = APPR T_AX

K4-Finite Transitive Frames (TF)

We prove that the set of finite transitive frames is the one appropriate to $K4$.

let K4_AX = new_definition
  `K4_AX = {Box p --> Box Box p | p IN (:form)}`;;

let TF_DEF = new_definition
  `TF =
   {(W:W->bool,R:W->W->bool) |
    ~(W = {}) /\
    (!x y:W. R x y ==> x IN W /\ y IN W) /\
    FINITE W /\
    (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)}`;;

TF_APPR_K4
|- TF: (W->bool)#(W->W->bool)->bool = APPR K4_AX

S4-Finite Transitive Frames (RTF)

We prove that the set of finite reflexive-transitive frames is the one appropriate to $S4$.

let S4_AX = new_definition
  `S4_AX = {Box p --> Box Box p | p IN (:form)} UNION {Box p --> p |p IN (:form)}`;;
  
let RTF_DEF = new_definition
 `RTF =
  {(W:W->bool,R:W->W->bool) |
   ~(W = {}) /\
   (!x y:W. R x y ==> x IN W /\ y IN W) /\
   FINITE W /\
   (!x. x IN W ==> R x x) /\
   (!x y z:W. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)}`;;

RTF_APPR_S4
|- RTF: (W->bool)#(W->W->bool)->bool = APPR S4_AX

B-Finite Reflexive-Symmetric Frames (RSF)

We prove that the set of finite reflexive-symmetric frames is the one appropriate to $B$.

let B_AX = new_definition
  `B_AX = {p -->  Box Diam p | p IN (:form)} UNION {Box p --> p |p IN (:form)}`;;
  
let RSF_DEF = new_definition
 `RSF =
  {(W:W->bool,R:W->W->bool) |
   ~(W = {}) /\
   (!x y:W. R x y ==> x IN W /\ y IN W) /\
   FINITE W /\
   (!x. x IN W ==> R x x) /\
   (!x y:W. x IN W /\ y IN W /\ R x y ==> R y x )}`;;

RSF_APPR_B
|- RSF: (W->bool)#(W->W->bool)->bool = APPR B_AX

S5-Finite Reflexive-Euclidean Frames (REF)

We prove that the set of finite reflexive-euclidean frames is the one appropriate to $S5$.

let S5_AX = new_definition
  `S5_AX = {Diam p --> Box Diam  p | p IN (:form)} UNION {Box p --> p |p IN (:form)}`;;
  
let REF_DEF = new_definition
 `REF =
  {(W:W->bool,R:W->W->bool) |
   ~(W = {}) /\
   (!x y:W. R x y ==> x IN W /\ y IN W) /\
   FINITE W /\
   (!x. x IN W ==> R x x) /\
   (!x y z:W. x IN W /\ y IN W /\ z IN W /\ R x y /\ R x z ==> R z y)}`;;

REF_APPR_S5 
|- REF: (W->bool)#(W->W->bool)->bool = APPR S5_AX

GL-Finite Irreflexive and Transitive Frames (ITF)

We prove that the set of finite transitive and irreflexive frames is the one appropriate to $GL$.

let GL_AX = new_definition
  `GL_AX = {Box (Box p --> p) --> Box p | p IN (:form)}`;;

let ITF_DEF = new_definition
  `ITF =
   {(W:W->bool,R:W->W->bool) |
    ~(W = {}) /\
    (!x y:W. R x y ==> x IN W /\ y IN W) /\
    FINITE W /\
    (!x. x IN W ==> ~R x x) /\
    (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)}`;;

ITF_APPR_GL
|- ITF: (W->bool)#(W->W->bool)->bool = APPR GL_AX

Grz-Finite Reflexive Antisymmetric and Transitive Frames (RATF)

We prove that the set of finite reflexive antisymmetric and transitive frames is the appropriate to $S4Grz$, an alternative axiomatization for $Grz$.

let GRZ_AX = new_definition
  `GRZ_AX = {Box (Box (p --> Box p) --> p) --> p| p IN (:form)}`;;

let S4GRZ_AX = new_definition
  `S4GRZ_AX = {Box p --> Box Box p | p IN (:form)} UNION
              {Box p --> p |p IN (:form)} UNION
              {Box (Box (p --> Box p) --> p) --> p | p IN (:form)}`;;

GRZ_EQ_S4GRZ 
|- !H p. [GRZ_AX . H |~ p] <=> [S4GRZ_AX . H |~ p]

let RATF_DEF = new_definition
 `RATF =
  {(W:W->bool,R:W->W->bool) |
    ~(W = {}) /\
    (!x y:W. R x y ==> x IN W /\ y IN W) /\
    FINITE W /\
    (!x. x IN W ==> R x x) /\
    (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z) /\
    (!w w':W. w IN W /\ w' IN W /\ R w w' /\ R w' w ==> w = w')}`;;

RATF_APPR_S4GRZ
|- RATF: (W->bool)#(W->W->bool)->bool = APPR S4GRZ_AX

Soundness and Consistency

We parametrically demonstrate the soundness of each $S$ with respect to $\mathsf{APPR}(S)$.

GEN_APPR_VALID
|- !S p. [S. {} |~ p] ==> APPR S:(W->bool)#(W->W->bool)->bool |= p

Then, by specializing the proof of GEN_APPR_VALID, we prove the soundness of each normal system $S$ developed in HOLMS with respect to its appropriate frame. Moreover we prove its consistency, by modus ponens on the converse of S_APPRS_VALID.

In the following, we present the proof of soundness for GL as an example :

Soundness and consistency of GL

let GL_ITF_VALID = prove
(`!p. [GL_AX . {} |~ p] ==> ITF:(W->bool)#(W->W->bool)->bool |= p`,
ASM_MESON_TAC[GEN_APPR_VALID; ITF_APPR_GL]);;

let GL_consistent = prove
 (`~ [GL_AX . {} |~  False]`,
  REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] GL_ITF_VALID)) THEN
  REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM;
              IN_ITF; NOT_FORALL_THM] THEN
  MAP_EVERY EXISTS_TAC [`{0}`; `\x:num y:num. F`] THEN
  REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);;

Completeness Theorems

We first sketch the idea behind the demonstration and, then, we will present a three-step proof.

The Idea behind the Proof

Given a modal system $S$, we want to prove that it is complete with respect to the set of its appropriate frames: $\forall p (\mathsf{APPR}(S) \vDash p \implies \mathcal{S}. \varnothing \vdash p)$

val it : goalstack = 1 subgoal (1 total)
`!p. APPR S |= p ==> [S. {} |~ p]`

• 1. Rewriting S_COMPLETENESS's statement
  By using some tautologies and rewritings, we can show that the completeness theorem is equivalent to a more handy sentence:
  $\forall p (\mathcal{S}. \varnothing \not \vdash p \implies \exists \langle W,R\rangle_{S,p} \in \mathsf{APPR}(S) (\exists V_{S,p} \exists m_{S,p} \in W_{S,p} (\langle W_{S,p}, R_{S,p}, V_{S,p} \rangle, m_{S,p} \not \vDash p))$
  
  
  • A. We rewrote the sentence by contraposition.
    e GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM];;
    
    
  • B. We rewrote validity in a set of frames (valid) as validity in a certain world of a certain model (holds) and we exploited some propositional tautologies.
    e (REWRITE_TAC[valid; NOT_FORALL_THM; FORALL_PAIR_THM; holds_in; NOT_IMP]);;
    

val it : goalstack = 1 subgoal (1 total)
`!p. ~[S . {} |~ p]
     ==> ?W R. (W,R) IN APPR S /\
               (?V m. m IN W /\ ~holds (W,R) V p w)`

To prove this rewritten statement, we need to construct a countermodel $𝓜_{S,p}$ and a "counterworld" $m_{S,p}$ in the domain of the countermodel for each modal formula $p$.

We can observe that, by working with HOL, we identify all those lines of reasoning that are parametric with respect to $S$ (the axiom system) and to $p$ (the formula we are analysing) and we develop the completeness proof while avoiding code duplication as much as possible.

• 2. Reducing a model-theoretic notion to a list-theoretic concept
  The canonical proof of completeness, illustrated in classical textbooks like George Boolos's "The Logic of Provability", exploits the idea of working in a context (countermodel) such that: $\forall w \in W_{S,p} (w \in p \iff 𝓜_{S,p},w \vDash p) $.
  
  Observe that, in such a context, the members of the domain $W_{S,p}$ are lists of modal formulas. If we are able to construct a countermodel with these constraints, we will easily construct a counterworld $m_{S,p}$ that is a list of formulas not including p.
  
  Then our subgoal would be to prove:
  

val it : goalstack = 1 subgoal (1 total)
`!p. ~[S . {} |~ p]
       ==> ?W R. (W,R) IN APPR S /\
                 (?M. M IN W /\ ~ MEM p M)`

This subgoal is much more manageable than the previous one, indeed it reduces the model-theoretic notion of validity (holds (W,R) V p w) to the list-theoretic concept of membership (MEM p w).

• 3. What do we need to prove?
  Given our aim of proving $\forall p(\mathcal{S}. \varnothing \not \vdash p \implies \exists \langle W,R \rangle_{S,p} \in \mathsf{APPR}(S) (\exists m_{S,p} \in W_{S,p}(p \not \in m_{S,p})))$, we need a countermodel and counterworld following these constraints:
  
  
  • A. The Kripke's frame $\langle W,R \rangle_{S,p}$ must be appropriate to S.
    $\langle W,R \rangle_{S,p} \in \mathsf{APPR}(S)$
    
    
  • B. The Kripke's model $𝓜_{S,p} = \langle W,R,V \rangle_{S,p}$ must allow us to reduce validity to membership for every subformula of p.
    Namely, for our model $𝓜_{S,p}$ holds $\forall q (q < p \ \implies \ \forall w \in W_{S,p} (w \in q \iff 𝓜_{S,p},w \vDash q))$, where $<$ denotes the subformula relation.
    
  • C. The counterworld $m_{S,p}$ must not contain $p$.
    
  • D. $W_{S,p}$ must be a set of formulas lists
    APPR S:(form list->bool)#(form list->form list->bool)->bool.

STEP 1: Partial definition of a parametric Standard Model

We partially identify the countermodel $𝓜_{S,p} = \langle W,R,V \rangle_{S,p}$ by defining $W_{S,p}$ as a set of maximal consistent lists, $V$ as a particular binary relation over formulas' atoms and worlds and by requesting two constraints for $R_{S,p}$. The definition of S_STANDARD_MODEL in step 1 is fully parametric and does not involve any peculiarities of the modal system $S$. Consequently this definition is pesented in gen_completeness.ml as GEN_STANDARD_MODEL.

Consistency and Maximal Consistency

Before we build up the countermodel, we define in consistent.ml some properties that hold for formulas lists and that will be useful to define the domain of the countermodel.

S-Consistent

A list of formulas $X$ is $S$-consistent to a set of axioms $S$ iff and only if $\mathcal{S.} \varnothing \not \vdash \neg \bigwedge X$

let CONSISTENT = new_definition
  `CONSISTENT S (X:form list) <=> ~[S . {} |~ Not (CONJLIST X)]`;;

S,p-Maximal Consistent

A list of formulas $X$ is $(S,p)$-maximal to a set of axioms $S$ and modal formula $p$ iff $X \ \text{has no repetitions}$, $X \ is \ S\text{-consistent}$ and $\forall q (q < p \implies q \in X \lor \neg q \in l)$.

let MAXIMAL_CONSISTENT = new_definition
  `MAXIMAL_CONSISTENT S p X <=>
   CONSISTENT S X /\ NOREPETITION X /\
   (!q. q SUBFORMULA p ==> MEM q X \/ MEM (Not q) X)`;;

Extension of Consistent Lists to Maximal Consistent Lists

Lindenbaum Lemma: $X \text{ is } S\text{-consistent} \land \forall q ( q \in X \implies (q < p \lor \neg q < p)) \implies \exists M (X \subseteq M \ \land \ M \text{ is } (S,p)\text{-maximal-consistent} )$

EXTEND_MAXIMAL_CONSISTENT
|- !S p X. CONSISTENT S X /\
           (!q. MEM q X ==> q SUBSENTENCE p)
           ==> ?M. MAXIMAL_CONSISTENT S p M /\
                   (!q. MEM q M ==> q SUBSENTENCE p) /\
                   X SUBLIST M

Definition of the parametric Countermodel

We define a standard model such that:

• A: The Domain $W_{S,p}$ is { $X | (S,p)\text{-maximal-consistent} \ X \land \forall q ( q \in X \implies (q < p \lor \neg q < p))$ }
  
  As requested, the domain is a set of lists of formulas and, in particular, it is a subclass of maximal consistent sets of formulas.
  Observe that, in principle, we can employ general sets of formulas in the formalisation. However, from the practical viewpoint, lists without repetitions are better suited in HOL since they are automatically finite and we can easily manipulate them by structural recursion.
  
  We prove, as requested for the domain of a frame, that $W_{S,p}$ is non-empty by using NONEMPTY_MAXIMAL_CONSISTENT, a corollary of the lemma of extension of maximal consistent lists.

NONEMPTY_MAXIMAL_CONSISTENT
|- !S p. ~ [S . {} |~ p]
         ==> ?M. MAXIMAL_CONSISTENT S p M /\
                 MEM (Not p) M /\
                 (!q. MEM q M ==> q SUBSENTENCE p)

• B: The Accessibility Relation $R_{S,p}$ should meet two conditions

  • R1: $\forall q \in Form_{\Box} (\Box q < p \implies \forall w \in W_{S,p}(\Box q \in w \Leftrightarrow \forall x (wRx \implies q \in x)))$.
    This condition ensures that our list-theoretic translation follows Kripke's semantics.
  • R2: $\langle W,R \rangle_{S,p} \in \mathsf{APPR}(S)$.
    This second condition guarantees one of the four initial constraints.

• C: The Evaluation Relation $V_{S,p}$ is defined as follows
  $\forall m \in W_{S,p} \ \forall a \in \text{Atom-Form}_{\Box} (mVa \iff a < p \land a \in m)$

In particular, in HOLMS's gen_completeness.ml we develop a parametric (to $S$ and $p$) definition of GEN_STANDARD_FRAME and GEN_STANDARD_MODEL and then we specialize these definitions for each normal system.

let GEN_STANDARD_FRAME_DEF = new_definition
  `GEN_STANDARD_FRAME S p =
   APPR S INTER
   {(W,R) | W = {w | MAXIMAL_CONSISTENT S p w /\
            (!q. MEM q w ==> q SUBSENTENCE p)} /\
            (!q w. Box q SUBFORMULA p /\ w IN W
                   ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))}`;;

let GEN_STANDARD_MODEL_DEF = new_definition
  `GEN_STANDARD_MODEL S p (W,R) V <=>
   (W,R) IN GEN_STANDARD_FRAME S p /\
   (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`;;

Because the definitions of K_STANDARD_MODEL, T_STANDARD_MODEL, K4_STANDARD_MODEL and GL_STANDARD_MODEL are just instances of GEN_STANDARD_FRAME and GEN_STANDARD_MODEL with the parameters {}, T_AX, K4_AX and GL_AX, here we present only the definitions for $K4$.

Definitions in k4_completeness.ml (S=K4_AX)

let K4_STANDARD_FRAME_DEF = new_definition
`K4_STANDARD_FRAME p = GEN_STANDARD_FRAME K4_AX p`;;

IN_K4_STANDARD_FRAME
|- !p W R. (W,R) IN K4_STANDARD_FRAME p <=>
           W = {w | MAXIMAL_CONSISTENT K4_AX p w /\
                    (!q. MEM q w ==> q SUBSENTENCE p)} /\
           (W,R) IN TF /\
           (!q w. Box q SUBFORMULA p /\ w IN W
                  ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))

let K4_STANDARD_MODEL_DEF = new_definition
   `K4_STANDARD_MODEL = GEN_STANDARD_MODEL K4_AX`;;

K4_STANDARD_MODEL_CAR
|- !W R p V.
     K4_STANDARD_MODEL p (W,R) V <=>
     (W,R) IN K4_STANDARD_FRAME p /\
     (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))

STEP 2: Definition of a standard accessibility relation for each S

The definition of a standard acessibility relation cannot be fully parametrised, at least following the approach presented in classical textbook.

Consequently, to avoid code repetition, we will:

• A: Define a parametric GEN_STANDARD_REL in gen_completeness.ml,
• B: Complete the definition of S_STANDARD_REL in its spefic file S_completeness.ml, in a way that guarantees the conditions R1 and R2. In particular, we will show:
  • The most difficult verse of R1's implication in S_ACCESSIBILITY_LEMMA
    $\forall q \in Form_{\Box} (\Box q < p \implies \forall w \in W_{S,p}(\Box q \in w \Longleftarrow \forall x (wRx \implies q \in x)))$
  • R2 holds for $\langle W_{S,p},$ S_STANDARD_REL $\rangle$ in S_MAXIMAL_CONSISTENT.
    $\langle W_{S,p},$ S_STANDARD_REL $\rangle \in \mathsf{APPR}(S)$ Then SF_IN_STANDARD_S_FRAMEE follows as corollary and, given the hypotesis $\mathcal{S}.\varnothing \not \vdash p$, $\langle W_{S,p},$ S_STANDARD_REL $, V_{S,p} \rangle$ is an S_STANDARD_MODEL.

In the following, we provide the definitions of accessibility relations for each implemented system and, as an example, the accessibiility lemma and the maximal consistent lemma for GL:

A: Parametric definition of the standard relation in gen_completeness.

let GEN_STANDARD_REL = new_definition
  `GEN_STANDARD_REL S p w x <=>
   MAXIMAL_CONSISTENT S p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\
   MAXIMAL_CONSISTENT S p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\
   (!B. MEM (Box B) w ==> MEM B x)`;;

B.K: Definition of the standard relation for K in k_completeness.ml.

let K_STANDARD_REL_DEF = new_definition
  `K_STANDARD_REL p = GEN_STANDARD_REL {} p`;;

B.D: Definition of the standard relation for D in d_completeness.ml.

let D_STANDARD_REL_DEF = new_definition
  `D_STANDARD_REL p w x <=>
   GEN_STANDARD_REL D_AX p w x`;;

B.T: Definition of the standard relation for T in t_completeness.ml.

let T_STANDARD_REL_DEF = new_definition
  `T_STANDARD_REL p w x <=>
   GEN_STANDARD_REL T_AX p w x`;;

B:K4: Definition of the standard relation for K4 in k4_completeness.ml.

let K4_STANDARD_REL_DEF = new_definition
  `K4_STANDARD_REL p w x <=>
   GEN_STANDARD_REL K4_AX p w x /\
   (!B. MEM (Box B) w ==> MEM (Box B) x)`;;

B:S4: Definition of the standard relation for S4 in s4_completeness.ml.

let S4_STANDARD_REL_DEF = new_definition
  `S4_STANDARD_REL p w x <=>
   GEN_STANDARD_REL S4_AX p w x /\
   (!B. MEM (Box B) w ==> MEM (Box B) x)`;;

B:B: Definition of the standard relation for B in b_completeness.ml.

let B_STANDARD_REL_DEF = new_definition
  `B_STANDARD_REL p w x <=>
   GEN_STANDARD_REL B_AX p w x /\
   (!B. MEM (Box B) x ==> MEM B w)`;;

B:S5: Definition of the standard relation for S5 in s5_completeness.ml.

let S5_STANDARD_REL_DEF = new_definition
  `S5_STANDARD_REL p w x <=>
   GEN_STANDARD_REL S5_AX p w x /\
   (!B. MEM (Box B) w <=> MEM (Box B) x)`;;

B.GL: Definition of the standard relation for GL in gl_completeness.ml.

let GL_STANDARD_REL_DEF = new_definition
  `GL_STANDARD_REL p w x <=>
   GEN_STANDARD_REL GL_AX p w x /\
   (!B. MEM (Box B) w ==> MEM (Box B) x) /\
   (?E. MEM (Box E) x /\ MEM (Not (Box E)) w)`;;

B.Grz: Definition of the standard relation for S4Grz in grz_modular.ml.

let S4GRZ_STANDARD_REL_DEF = new_definition
  `S4GRZ_STANDARD_REL p w x <=>
    w IN S4GRZ_STANDARD_WORLDS p  /\
    x IN S4GRZ_STANDARD_WORLDS p  /\
    Q_REL p w x /\ (Q_REL p x w ==> w = x)`;;

let Q_REL_DEF = new_definition
  `Q_REL p w x <=>
   w IN S4GRZ_STANDARD_WORLDS p  /\
   x IN S4GRZ_STANDARD_WORLDS p  /\
   (!B. B SUBSENTENCE p \/
        (?C. Box C SUBFORMULA p /\ (Box B = Box(C --> Box C)))
        ==> (MEM (Box B) w ==> MEM (Box B) x))`;;

Accessibility Lemma for GL that ensures the most difficult verse of R1's implication.

GL_ACCESSIBILITY_LEMMA
|- !p w q.
     ~ [GL_AX . {} |~ p] /\
     MAXIMAL_CONSISTENT GL_AX p w /\
     (!q. MEM q w ==> q SUBSENTENCE p) /\
     Box q SUBFORMULA p /\
     (!x. GL_STANDARD_REL p w x ==> MEM q x)
     ==> MEM (Box q) w

Maximal Consistent Lemma for GL that ensures R2.

ITF_MAXIMAL_CONSISTENT
|- !p. ~ [GL_AX . {} |~ p]
         ==> ({M | MAXIMAL_CONSISTENT GL_AX p M /\
                   (!q. MEM q M ==> q SUBSENTENCE p)},
              GL_STANDARD_REL p)
             IN ITF

Proof of the corollary that ensures that our construction for GL is a standard frame.

g `!p. ~ [GL_AX . {} |~ p]
       ==> ({M | MAXIMAL_CONSISTENT GL_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
            GL_STANDARD_REL p)
           IN GL_STANDARD_FRAME p`;;
e (INTRO_TAC "!p; not_theor_p");;
e (REWRITE_TAC [IN_GL_STANDARD_FRAME]);;
e CONJ_TAC;;
 e (MATCH_MP_TAC ITF_MAXIMAL_CONSISTENT);;
 e (ASM_REWRITE_TAC[]);;
 e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
e (INTRO_TAC "!q w; subform max_cons_w implies_w");;
e EQ_TAC;;
 e (ASM_MESON_TAC[GL_STANDARD_REL_CAR]);;
e (ASM_MESON_TAC[GL_ACCESSIBILITY_LEMMA]);;
let GLF_IN_GL_STANDARD_FRAME = top_thm();;

STEP 3: Proving the truth lemma

In this step, we prove that, given a standard model and $\mathcal{S}. \varnothing \not \vdash p$, the desiderandum in the proof sketch holds, and indeed something stronger holds: For every subformula q of p we can reduce the notion of holds (W,R) V q w to the list-theoretic one of membership MEM q w.

Observe that we prove this foundamental lemma in a fully parametric way and, moreover, the proof of completeness does not need to specify this lemma for the normal system in analysis.

Parametric truth lemma in gen_completeness.ml (parameters P, S)

GEN_TRUTH_LEMMA
|- !S W R p V q.
     ~ [S . {} |~ p] /\
     GEN_STANDARD_MODEL S p (W,R) V /\
     q SUBFORMULA p
     ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)

The Theorems

We built up a countermodel $\langle W,R,V \rangle_{S,p}$ that is a standard model for S, and now we want to prove that a counterworld in this model exists: $\exists m_{S,p} \in W_{S,p} (p \not \in m_{S,p} )$. So we need an $m_{S,p}$ such that:

• A: $m_{S,p} \in W_{S,p}$ that is to say $m_{S,p}$ is $(S,p)\text{-maximal-consistent}$;
• B: $p \not \in m_{S,p}$

Thanks to our theorem NONEMPTY_MAXIMAL_CONSISTENT $\forall p (\mathcal{S}.\varnothing \vdash p \implies (\exists m (\m \text{ is }(S,p)\text{-maximal-consistent} \ \land \ \neg p \in M))$, we know that such an $m_{S,p}$ exists and we can prove GEN_COUNTERMODEL_ALT. Observe, indeed, that $m$ is $(S,p)$--maximal-consistent $\land \ \neg p \in m_{S,p} \implies p \not \in m_{S,p}$.

NONEMPTY_MAXIMAL_CONSISTENT
|- !S p. ~ [S . {} |~ p]
         ==> ?M. MAXIMAL_CONSISTENT S p M /\
                 MEM (Not p) M /\
                 (!q. MEM q M ==> q SUBSENTENCE p)

GEN_COUNTERMODEL_ALT
|- !S W R p. ~ [S . {} |~ p] /\
             (W,R) IN GEN_STANDARD_FRAME S p
             ==>
             ~ holds_in (W,R) p

Given the fully parametrised GEN_COUNTERMODEL_ALT and SF_IN_STANDARD_S_FRAME, the completeness theorem for every $S$ follows and the proof for GL is presented below as an example:

Completeness of GL in gl_completeness.ml

g `!p. ITF:(form list->bool)#(form list->form list->bool)->bool |= p
       ==> [GL_AX . {} |~ p]`;;
e (GEN_TAC THEN GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] );;
e (INTRO_TAC "p_not_theor");;
e (REWRITE_TAC[valid; NOT_FORALL_THM]);;
e (EXISTS_TAC `({M | MAXIMAL_CONSISTENT GL_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
               GL_STANDARD_REL p)`);;
e (REWRITE_TAC[NOT_IMP] THEN CONJ_TAC);;
 e (MATCH_MP_TAC ITF_MAXIMAL_CONSISTENT);;
 e (ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `({M | MAXIMAL_CONSISTENT GL_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)},
                   GL_STANDARD_REL p) IN GEN_STANDARD_FRAME GL_AX p`
                  MP_TAC);;
 e (ASM_MESON_TAC[GLF_IN_GL_STANDARD_FRAME; GL_STANDARD_FRAME_DEF]);;
e (ASM_MESON_TAC[GEN_COUNTERMODEL_ALT]);;
let GL_COMPLETENESS_THM = top_thm ();;

Modal completeness for models on a generic (infinite) domain.

Observe that our proof of completeness requires that APPR S is not just a set of appropriate frames (APPR S:(W->bool)#(W->W->bool)->bool) but a set of appropriate frames sitting on the type of formulas' lists (APPR S:(form list->bool)#(form list->form list->bool)->bool). Nevertheless, thanks to the parametric lemma GEN_LEMMA_FOR_GEN_COMPLETENESS, we can quickly generalise each completeness theorem for models on domains with a generic infinite type.

In gen_completeness.ml.

GEN_LEMMA_FOR_GEN_COMPLETENESS
|- !S. INFINITE (:A)
       ==> !p. APPR S:(A->bool)#(A->A->bool)->bool |= p
               ==> APPR S:(form list->bool)#(form list->form list->bool)->bool |= p

As corollaries of GEN_LEMMA_FOR_GEN_COMPLETENESS, the general completeness theorems are proved in their specific files, e.g:

GL_COMPLETENESS_THM_GEN
|- !p. INFINITE (:A) /\ ITF:(A->bool)#(A->A->bool)->bool |= p
       ==> [GL_AX . {} |~ p]

Automated theorem proving and countermodel construction

Our tactic HOLMS_TAC and its associated rule HOLMS_RULE can automatically prove theorems in the modal logics above by performing a root-first proof search in the associated labelled sequent calculus. When the tactic halts witout reaching a proof, the proof state holds a countermodel. The procedure HOLMS_BUILD_COUNTERMODEL outputs the generated countermodel and *_CERTIFY_TAC verifies that the candidate countermodel falsifies the input formula in the logic *.

Here we report two basic examples. More examples of proofs and countermodels can be found in the file tests.ml.

Example of automatic theorem syntesis

Automatic proof of the Formal Second Incompleteness Theorem in the Gödel–Löb modal logic:

# HOLMS_RULE `[GL_AX . {} |~ Not Box False --> Not Box Diam True]`;;
1 worlds
2 worlds
val it : thm = |- [GL_AX . {} |~ Not Box False --> Not Box Diam True]

Example of countermodel generation

Generation of a countermodel to the Löb schema in the modal logic K:

# let tm = `!a. [T_AX . {} |~ a --> Box Diam a[T_AX . {} |~ a --> Box Diam a]`;;
# let ctm = HOLMS_BUILD_COUNTERMODEL tm;;
1 worlds
2 worlds
val ctm : term =
  `holds (W,R) V (Box Not a) y /\
   R w y /\
   R y y /\
   y IN W /\
   holds (W,R) V a w /\
   R w w /\
   w IN W /\
   W,R IN RF /\
   ~holds (W,R) V a y`
# T_HOLMS_CERTIFY_COUNTERMODEL ctm tm;;
val it : thm = |- ~(forall a. RF |= a --> Box Diam a)

Translation Technique for Grz

Instead then shallow embedding the labelled sequent calculus for Grz (G3Grz) and performing a root-first proof search in this calculus, we experiment with a different technique.

In particular, we mechanise a full and faithful embedding of Grz into Gödel-Löb provability logic (GL) in two steps:

• Implementing the standard splitting translation within HOL Light and proving its fullness and faithfulness;

  let TRANSL = define
  `(!s. TRANSL (Atom s) = Atom s) /\
   TRANSL True = True /\
   TRANSL False = False /\
   (!p. TRANSL (Not p) = Not (TRANSL p)) /\
   (!p q. TRANSL (p && q) = TRANSL p && TRANSL q) /\
   (!p q. TRANSL (p || q) = TRANSL p || TRANSL q) /\
   (!p q. TRANSL (p --> q) = TRANSL p --> TRANSL q) /\
   (!p q. TRANSL (p <-> q) = TRANSL p <-> TRANSL q) /\
   (!p. TRANSL (Box p) = Dotbox (TRANSL p))`;;
  

  GRZ_TRANSL 
  |- `!p. [GRZ_AX . {} |~ p] <=> [GL_AX . {} |~ TRANSL (p)]`
  

• Reducing validity problems in Grz to corresponding validity problems in GL.

  let GRZ_TAC : tactic =
   let vsubst_rplus = vsubst [`R_PLUS (W:num->bool) R`,`R:num->num->bool`] in
   let tac =
     GEN_REWRITE_TAC I [GRZ_TRANSL] THEN
     CONV_TAC (RAND_CONV TRANSL_CONV) THEN
     REWRITE_TAC[dotbox_DEF] THEN
     GL_TAC in
   (* Call tac and translate countermodel in case of failure *)
   fun gl ->
     try tac gl with Failure s ->
       the_HOLMS_countermodel := vsubst_rplus !the_HOLMS_countermodel;
       FAIL_TAC s gl;;
  

By doing so, we directly reuse HOLMS's existing verified decision procedure for GL to decide Grz-theoremhood automatically.

Here we report two interesting example of decision and countermodel construction in Grz.

let Contingent_DEF = new_definition 
 `Contingent p  = Diam p && Diam Not p` ;;

let Penultimate_DEF = new_definition 
 `Penultimate p = p && Diam Not p && Box (Not p --> Box Not p)`;;

# g `[GRZ_AX . {}
            |~ Contingent (Atom "p") --> 
               Diam (Penultimate (Atom "p") || 
                     Penultimate (Not (Atom "p")))]`;;  
# e (REWRITE_TAC[Contingent_DEF; Penultimate_DEF]);;
# e (REWRITE_TAC[diam_DEF]);;
# e HOLMS_TAC;;
|- [GRZ_AX . {}
     |~ Contingent (Atom "p") -->
        Diam (Penultimate (Atom "p") || Penultimate (Not Atom "p"))]

let tm = `[GRZ_AX . {} |~ Diam Box Atom "a" --> Box Diam Atom "a"]`;;

# HOLMS_RULE tm;;
Exception: Failure "GRZ_TAC: Proof not found".

# let ctm = HOLMS_BUILD_COUNTERMODEL tm;;
1 worlds
1 worlds
1 worlds
2 worlds
3 worlds
val ctm : term =
 ` w IN W /\ y IN W /\  y' IN W /\
   W,R IN RATF /\
   R y' y' /\ R y y /\ R w w /\ R w y' /\ R w y /\
   V "a" y' /\   ~V "a" y`

# GRZ_HOLMS_CERTIFY_COUNTERMODEL ctm tm;;
val it : thm = |- ~(RATF |= Diam Box Atom "a" --> Box Diam Atom "a")