From b57ee2e84e9c1349d84c3073681c8da85695c9cd Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Mon, 27 Jan 2025 15:44:21 +0100 Subject: [PATCH 01/16] Update README.md --- README.md | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index b1c94a4..95481b9 100644 --- a/README.md +++ b/README.md @@ -5,15 +5,23 @@ See the [website](https://holms-lib.github.io/) for a brief overview of our [HOLMS library](https://github.com/HOLMS-lib/HOLMS) for the [HOL Light](https://hol-light.github.io/) theorem prover. This repository introduces HOLMS (HOL-Light Library for Modal Systems), a new framework within the HOL Light proof assistant, designed for automated theorem proving and countermodel construction in modal logics. -Building on our prior work focused on Gödel-Löb logic (GL), we generalise our approach to cover a broader range of normal modal systems, starting here with the minimal system K. +Building on our prior work focused on Gödel-Löb logic (GL), we generalise our approach to cover a broader range of normal modal systems, starting here with: +- K: minimal system; +- K4: system properly extended by GL; +- T: that is not extended by GL or K4, nor is an extension of K4 or K4. HOLMS provides a flexible mechanism for automating proof search and countermodel generation by leveraging labelled sequent calculi, interactive theorem proving, and formal completeness results. The top-level file is `make.ml`. -The main theorems are: +The main parametric theorems are: 1. `GEN_TRUTH_LEMMA` in file `gen_completeness.ml`. -2. `K_COMPLETENESS_THM` in file `k_completness.ml` -3. `GL_COMPLETENESS_THM` in file `gl_completness.ml` +2. + +The main theorems for the normal systems are: +3. `K_COMPLETENESS_THM` in file `k_completness.ml` +4. `T_COMPLETENESS_THM` in file `t_completness.ml +5. `K4_COMPLETENESS_THM` in file `k4_completness.ml +6. `GL_COMPLETENESS_THM` in file `gl_completness.ml` # Usage guide and source code @@ -454,4 +462,4 @@ For any arithmetical sentences p q, p is equivalent to unprovability of q --> p let GL_arithmetical_fixpoint = time GL_RULE `!p q. [GL_AX . {} |~ Dotbox (p <-> Not (Box (q --> p))) <-> Dotbox (p <-> Diam q)]`;; -``` \ No newline at end of file +``` From 6b6f935a90eaf9a7703d45ef976c1d3fa3c92f22 Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Mon, 27 Jan 2025 15:45:52 +0100 Subject: [PATCH 02/16] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 95481b9..8336279 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,7 @@ The top-level file is `make.ml`. The main parametric theorems are: 1. `GEN_TRUTH_LEMMA` in file `gen_completeness.ml`. -2. +2. a The main theorems for the normal systems are: 3. `K_COMPLETENESS_THM` in file `k_completness.ml` From 0948d54d404e82492203dead08ee0ca23cc00f39 Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Mon, 27 Jan 2025 16:34:51 +0100 Subject: [PATCH 03/16] Update main theorems and HOLMS description --- README.md | 29 ++++++++++++++++++----------- 1 file changed, 18 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 8336279..86ba9f8 100644 --- a/README.md +++ b/README.md @@ -6,22 +6,29 @@ See the [website](https://holms-lib.github.io/) for a brief overview of our [HOL This repository introduces HOLMS (HOL-Light Library for Modal Systems), a new framework within the HOL Light proof assistant, designed for automated theorem proving and countermodel construction in modal logics. Building on our prior work focused on Gödel-Löb logic (GL), we generalise our approach to cover a broader range of normal modal systems, starting here with: -- K: minimal system; -- K4: system properly extended by GL; -- T: that is not extended by GL or K4, nor is an extension of K4 or K4. +- K: the minimal system; +- K4: a system properly extended by GL; +- GL: provability logic +- T: a system that is not extended by GL or K4, nor is an extension of K4 or K4. + HOLMS provides a flexible mechanism for automating proof search and countermodel generation by leveraging labelled sequent calculi, interactive theorem proving, and formal completeness results. The top-level file is `make.ml`. -The main parametric theorems are: -1. `GEN_TRUTH_LEMMA` in file `gen_completeness.ml`. -2. a +To partially generalise and parametrize the proof of completness for normal systems, 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_COMPLETNESS` -The main theorems for the normal systems are: -3. `K_COMPLETENESS_THM` in file `k_completness.ml` -4. `T_COMPLETENESS_THM` in file `t_completness.ml -5. `K4_COMPLETENESS_THM` in file `k4_completness.ml -6. `GL_COMPLETENESS_THM` in file `gl_completness.ml` +For each normal system L, implemented in HOLMS, we prove the following main theorems: +1. **The Correspondence theorem for L** proves that a certain set of finite frames, distinguished by an accessibility relation with certain property, correspond (if p follows from L then p is valid in such a frame) to L. (`APPRL_CORR_L`) +2. **The Validity theorem for L** proves that if something is a theorem of L then it is valid in its appropriate frame. (`L_APPRL_VALID`) +3. **Consistency for L** proves that L cannot prove the false. (`L_CONSISTENT`) +4. **The Completness theorem for L** proves that if someting is valid in a frame that corresponds to L then it is a theorem of L. (`L_COMPLETNESS_THM`) +5. **A simple rule of decision for L** that applies a simple decision procedure to prove whether something is a theorem of L or not. (`L_RULE`) + +For example, in `t_completness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`; (5) `T_RULE`. # Usage guide and source code From 66cbcbb79b88160d81dfef2faed2a86700036347 Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Mon, 27 Jan 2025 17:44:58 +0100 Subject: [PATCH 04/16] Theory of corespondence + validity and consistency + gen_completness --- README.md | 193 +++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 139 insertions(+), 54 deletions(-) diff --git a/README.md b/README.md index 86ba9f8..46e1bf2 100644 --- a/README.md +++ b/README.md @@ -15,24 +15,24 @@ HOLMS provides a flexible mechanism for automating proof search and countermodel The top-level file is `make.ml`. -To partially generalise and parametrize the proof of completness for normal systems, we develop four main theorems in `gen_completeness.ml`: +To partially generalise and parametrize the proof of completeness for normal systems, 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_COMPLETNESS` +4. `GEN_LEMMA_FOR_GEN_COMPLETENESS` For each normal system L, implemented in HOLMS, we prove the following main theorems: 1. **The Correspondence theorem for L** proves that a certain set of finite frames, distinguished by an accessibility relation with certain property, correspond (if p follows from L then p is valid in such a frame) to L. (`APPRL_CORR_L`) 2. **The Validity theorem for L** proves that if something is a theorem of L then it is valid in its appropriate frame. (`L_APPRL_VALID`) 3. **Consistency for L** proves that L cannot prove the false. (`L_CONSISTENT`) -4. **The Completness theorem for L** proves that if someting is valid in a frame that corresponds to L then it is a theorem of L. (`L_COMPLETNESS_THM`) +4. **The completeness theorem for L** proves that if someting is valid in a frame that corresponds to L then it is a theorem of L. (`L_COMPLETENESS_THM`) 5. **A simple rule of decision for L** that applies a simple decision procedure to prove whether something is a theorem of L or not. (`L_RULE`) -For example, in `t_completness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`; (5) `T_RULE`. +For example, in `t_completeness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`; (5) `T_RULE`. # Usage guide and source code -## Axiomatic Definition +## Calcus Definition ``` let MODPROVES_RULES,MODPROVES_INDUCT,MODPROVES_CASES = new_inductive_definition @@ -74,8 +74,77 @@ let holds_in = new_definition let valid = new_definition `L |= p <=> !f:(W->bool)#(W->W->bool). f IN L ==> holds_in f p`;; + +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 correspondent frames. +``` +let CORR_DEF = new_definition + `CORR S = {(W:W->bool,R:W->W->bool) | + (((W,R) IN FINITE_FRAME ) /\ + (!p. [S. {} |~ p] ==> holds_in (W:W->bool,R:W->W->bool) (p)))}`;; +``` +We demonstrate that each frame that is correspondent to L is valid for L. +``` +GEN_CORR_VALID +|- `!S p. [S. {} |~ p] ==> CORR S:(W->bool)#(W->W->bool)->bool |= p`;; +``` +For each one of the normal system L developed in HOLMS we prove what set of frames is correspondent to L. + +### K-FINITE FRAMES +We prove that the set of finite frames is the correspond set to K. +``` +FINITE_FRAME_CORR_K + |-`FINITE_FRAME:(W->bool)#(W->W->bool)->bool = CORR {}`;; +``` +### T-REFLEXIVE FRAMES +We prove that the set of reflexive frames is the correspond set to T. +``` +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_CORR_T + |-`FINITE_FRAME:(W->bool)#(W->W->bool)->bool = CORR {}`;; +``` +### K4-TRANSITIVE FRAMES +We prove that the set of transitive frames is the correspond set to K4. +``` +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_CORR_K4 + |-`TF: (W->bool)#(W->W->bool)->bool = CORR K4_AX`;; +``` +### GL-IRREFLEXIVE AND TRANSITIVE FRAMES +We prove that the set of transitive and irreflexive frames is the correspond set to GL. +``` +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_CORR_GL + |-`ITF: (W->bool)#(W->W->bool)->bool = CORR GL_AX`;; ``` + ## Soundness and consistency of K We prove the consistency of K by modus ponens on the converse of `K_FRAME_VALID`. ``` @@ -85,9 +154,6 @@ K_FRAME_VALID ==> (!q. q IN H ==> K_FRAME:(W->bool)#(W->W->bool)->bool |= q) ==> K_FRAME:(W->bool)#(W->W->bool)->bool |= p -K_CONSISTENT -|- ~ [{} . {} |~ False] - let K_CONSISTENT = prove (`~ [{} . {} |~ False]`, REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] K_FRAME_VALID)) THEN @@ -97,48 +163,53 @@ let K_CONSISTENT = prove REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);; ``` -## Soundness and consistency of GL -To develop this proof of consistency we use modal correspondence theory for GL, therefore we prove `TRANSNT_EQ_LOB` and we derive as its consequence`GL_ITF_VALID`. +## Soundness and consistency of T +To develop this proof of consistency we use modal correspondence theory for T and, by `GEN_CORR_VALID `, we prove `T_RF_VALID`. +``` +T_RF_VALID +|- `!p. [T_AX . {} |~ p] ==> RF:(W->bool)#(W->W->bool)->bool |= p` +``` +We prove the consistency of T by modus ponens on the converse of `T_FRAME_VALID`. +``` +let T_CONSISTENT = prove + (`~ [T_AX . {} |~ False]`, + REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] T_RF_VALID)) THEN + REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM; + IN_RF; NOT_FORALL_THM] THEN + MAP_EVERY EXISTS_TAC [`{0}`; `\x:num y:num. x = 0 /\ x = y`] THEN + REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);; ``` -let TRANSNT_DEF = new_definition - `TRANSNT = - {(W:W->bool,R:W->W->bool) | - ~(W = {}) /\ - (!x y:W. R x y ==> x IN W /\ y IN W) /\ - (!x y z:W. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z) /\ - WF(\x y. R y x)}`;; -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)}`;; +## Soundness and consistency of K4 +To develop this proof of consistency we use modal correspondence theory for K4 and, by `GEN_CORR_VALID `, we prove `K4_TF_VALID`. -TRANSNT_EQ_LOB -|- !W R. (!x y:W. R x y ==> x IN W /\ y IN W) - ==> ((!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z - ==> R x z) /\ - WF (\x y. R y x) <=> - (!p. holds_in (W,R) (Box(Box p --> p) --> Box p))) +``` +K4_TF_VALID +|- `!p. [K4_AX . {} |~ p] ==> TF:(W->bool)#(W->W->bool)->bool |= p` +``` + +The consistency theorem for K4 is proved by modus ponens on the converse of `K4_TF_VALID`. +``` +let K4_CONSISTENT = prove + (`~ [K4_AX . {} |~ False]`, + REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] K4_TF_VALID)) THEN + REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM; + IN_TF; 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[]);; +``` -GL_TRANSNT_VALID -|- !H p. [GL_AX . H |~ p] /\ - (!q. q IN H ==> TRANSNT:(W->bool)#(W->W->bool)->bool |= q) - ==> TRANSNT:(W->bool)#(W->W->bool)->bool |= p +## Soundness and consistency of GL +To develop this proof of consistency we use modal correspondence theory for GL and, by `GEN_CORR_VALID `, we prove `GL_ITF_VALID`. +``` GL_ITF_VALID |- !p. [GL_AX . {} |~ p] ==> ITF:(W->bool)#(W->W->bool)->bool |= p ``` The consistency theorem for GL is proved by modus ponens on the converse of `GL_ITF_VALID`. ``` -GL_consistent -|- ~ [GL_AX . {} |~ False] - let GL_consistent = prove (`~ [GL_AX . {} |~ False]`, REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] GL_ITF_VALID)) THEN @@ -158,7 +229,7 @@ In particular the step 3 is already fully formalised in HOLMS with the `GEN_TRU ### STEP 1 Identification of a model depending on a formula p and, in particular, of a non-empty set of possible worlds given by a subclass of maximal consistent sets of formulas. -Parametric Definitions in `gen_completness.ml` (parameters P, S) +Parametric Definitions in `gen_completeness.ml` (parameters P, S) ``` let FRAME_DEF = new_definition `FRAME = {(W:W->bool,R:W->W->bool) | ~(W = {}) /\ @@ -178,7 +249,7 @@ let GEN_STANDARD_MODEL_DEF = new_definition (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`;; ``` -Definitions in `k_completness.ml` (P=K_FRAME, S={}) +Definitions in `k_completeness.ml` (P=K_FRAME, S={}) ``` let K_FRAME_DEF = new_definition `K_FRAME = {(W:W->bool,R) | (W,R) IN FRAME /\ FINITE W}`;; @@ -203,7 +274,7 @@ K_STANDARD_MODEL_CAR (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p)) ``` -Definitions in `gl_completness.ml` (P=ITF, S=GL_AX) +Definitions in `gl_completeness.ml` (P=ITF, S=GL_AX) ``` let ITF_DEF = new_definition `ITF = @@ -238,7 +309,7 @@ GL_STANDARD_MODEL_CAR ### STEP 2 Definition of a “standard” accessibility relation depending on axiom set S between these worlds such that the frame is appropriate to S. -Parametric definition of the standard relation in `gen_completness.ml` (parameter S) +Parametric definition of the standard relation in `gen_completeness.ml` (parameter S) ``` let GEN_STANDARD_REL = new_definition `GEN_STANDARD_REL S p w x <=> @@ -247,7 +318,7 @@ let GEN_STANDARD_REL = new_definition (!B. MEM (Box B) w ==> MEM B x)`;; ``` -Definitions in `k_completness.ml` (S={}) and proof of the Accessibility Lemma for K. +Definitions in `k_completeness.ml` (S={}) and proof of the Accessibility Lemma for K. ``` let K_STANDARD_REL_DEF = new_definition `K_STANDARD_REL p = GEN_STANDARD_REL {} p`;; @@ -267,7 +338,7 @@ K_ACCESSIBILITY_LEMMA_1 ==> MEM (Box q) w ``` -Definitions in `gl_completness.ml` (S=GL_AX) and proofs of the Accessibility Lemma for GL. +Definitions in `gl_completeness.ml` (S=GL_AX) and proofs of the Accessibility Lemma for GL. ``` let GL_STANDARD_REL_DEF = new_definition `GL_STANDARD_REL p w x <=> @@ -292,7 +363,7 @@ GL_ACCESSIBILITY_LEMMA The reduction of the notion of forcing `holds (W,R) V q w` to that of a set-theoretic (list-theoretic) membership MEM q w for every subformula q of p, through a specific atomic evaluation function on (W,R). -Parametric truth lemma in `gen_completness.ml` (parameters P, S) +Parametric truth lemma in `gen_completeness.ml` (parameters P, S) ``` GEN_TRUTH_LEMMA |- !P S W R p V q. @@ -302,7 +373,7 @@ GEN_TRUTH_LEMMA ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w) ``` -Truth lemma specified for K in `k_completness.ml` (P=K_FRAME, S={}) +Truth lemma specified for K in `k_completeness.ml` (P=K_FRAME, S={}) ``` let K_TRUTH_LEMMA = prove (`!W R p V q. @@ -313,7 +384,7 @@ let K_TRUTH_LEMMA = prove REWRITE_TAC[K_STANDARD_MODEL_DEF] THEN MESON_TAC[GEN_TRUTH_LEMMA]);; ``` -Truth lemma specified for GL in `gl_completness.ml` (P=ITF, S=GL_AX) +Truth lemma specified for GL in `gl_completeness.ml` (P=ITF, S=GL_AX) ``` let GL_truth_lemma = prove (`!W R p V q. @@ -326,16 +397,16 @@ let GL_truth_lemma = prove ### The Theorems -Completeness of K in `k_completness.ml`. -This proof uses the `K_TRUTH_LEMMA` that specifies the `GEN_TRUTH_LEMMA`, therefore the first part of the proof of the completness theorem for K is completely parametrized. +Completeness of K in `k_completeness.ml`. +This proof uses the `K_TRUTH_LEMMA` that specifies the `GEN_TRUTH_LEMMA`, therefore the first part of the proof of the completeness theorem for K is completely parametrized. ``` K_COMPLETENESS_THM |- !p. K_FRAME:(form list->bool)#(form list->form list->bool)->bool |= p ==> [{} . {} |~ p] ``` -Completeness of GL in `gl_completness.ml` -This proof uses the `GL_TRUTH_LEMMA` that specifies the `GEN_TRUTH_LEMMA`, therefore the first part of the proof of the completness theorem for GL is completely parametrized. +Completeness of GL in `gl_completeness.ml` +This proof uses the `GL_TRUTH_LEMMA` that specifies the `GEN_TRUTH_LEMMA`, therefore the first part of the proof of the completeness theorem for GL is completely parametrized. ``` GL_COMPLETENESS_THM |- !p. ITF:(form list->bool)#(form list->form list->bool)->bool |= p @@ -343,11 +414,25 @@ GL_COMPLETENESS_THM ``` ### Modal completeness for models on a generic (infinite) domain. -These theorems generalize the previous ones for models with infinite worlds. +Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we quickly generalize the completeness theorem for models with infinite worlds for each normal sysrem. + ``` +GEN_LEMMA_FOR_GEN_COMPLETENESS +|- `!S. INFINITE (:A) + ==> !p. CORR S:(A->bool)#(A->A->bool)->bool |= p + ==> CORR S:(form list->bool)#(form list->form list->bool)->bool |= p`;; + K_COMPLETENESS_THM_GEN -|- !p. INFINITE (:A) /\ K_FRAME:(A->bool)#(A->A->bool)->bool |= p - ==> [{} . {} |~ p] +|- `!p. INFINITE (:A) /\ FINITE_FRAME:(A->bool)#(A->A->bool)->bool |= p + ==> [{} . {} |~ p]` + +T_COMPLETENESS_THM_GEN +|- `!p. INFINITE (:A) /\ RF:(A->bool)#(A->A->bool)->bool |= p + ==> [T_AX . {} |~ p]` + +K4_COMPLETENESS_THM_GEN +|- `!p. INFINITE (:A) /\ TF:(A->bool)#(A->A->bool)->bool |= p + ==> [K4_AX . {} |~ p]` GL_COMPLETENESS_THM_GEN |- !p. INFINITE (:A) /\ ITF:(A->bool)#(A->A->bool)->bool |= p From 7900e9e91dacbf6b373ab11a6458485492f94dae Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Mon, 27 Jan 2025 17:54:24 +0100 Subject: [PATCH 05/16] Esempi di applicazione delle regole alle nuove logiche --- README.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/README.md b/README.md index 46e1bf2..124f7a8 100644 --- a/README.md +++ b/README.md @@ -494,6 +494,28 @@ K_RULE `!a b. [{} . {} |~ Box (a && b) <-> Box a && Box b]`;; K_RULE `!a b. [{} . {} |~ Box a || Box b --> Box (a || b)]`;; ``` + +### In T + +Our tactic `T_TAC` and its associated rule `T_RULE` can automatically prove theorems in the modal logic T. + +Examples: +``` +T_RULE `!a. [ T_AX . {} |~ a --> Diamond a ]`;; +T_RULE `!a. [ T_AX . {} |~ Box a --> Diamond a ]`;; +``` + +### In K4 + +Our tactic `K4_TAC` and its associated rule `K4_RULE` can automatically prove theorems in the modal logic K4. + +### Example of a formula valid in K4 but not in K +``` +time GL_RULE + `!a. [GL_AX . {} |~ Box Diam Box Diam a <-> Box Diam a]`;; +``` + + ### In GL Our tactic `GL_TAC` and its associated rule `GL_RULE` can automatically prove theorems in the modal logic GL. From 151fa175283100f2530498511a4d142ae069211e Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Mon, 27 Jan 2025 18:39:01 +0100 Subject: [PATCH 06/16] Update README.md on completness step --- README.md | 76 ++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 59 insertions(+), 17 deletions(-) diff --git a/README.md b/README.md index 124f7a8..2a3d430 100644 --- a/README.md +++ b/README.md @@ -224,7 +224,6 @@ let GL_consistent = prove The proof is organized in three steps. We can observe that, by working with HOL, it is possible to identify all those lines of reasoning that are _parametric_ for P (the specific propriety of each frame of a logic) and S (the set of axioms of the logic) and develop each of of the three steps while avoiding code duplication as much as possible. -In particular the step 3 is already fully formalised in HOLMS with the `GEN_TRUTH_LEMMA`. ### STEP 1 Identification of a model depending on a formula p and, in particular, of a non-empty set of possible worlds given by a subclass of maximal consistent sets of formulas. @@ -249,29 +248,72 @@ let GEN_STANDARD_MODEL_DEF = new_definition (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`;; ``` -Definitions in `k_completeness.ml` (P=K_FRAME, S={}) +Definitions in `k_completeness.ml` (P=FINITE_FRAME, S={}) ``` -let K_FRAME_DEF = new_definition - `K_FRAME = {(W:W->bool,R) | (W,R) IN FRAME /\ FINITE W}`;; - let K_STANDARD_FRAME_DEF = new_definition - `K_STANDARD_FRAME = GEN_STANDARD_FRAME K_FRAME {}`;; + `K_STANDARD_FRAME = GEN_STANDARD_FRAME {}`;; IN_K_STANDARD_FRAME -|- (W,R) IN K_STANDARD_FRAME p <=> - W = {w | MAXIMAL_CONSISTENT {} p w /\ - (!q. MEM q w ==> q SUBSENTENCE p)} /\ - (W,R) IN K_FRAME /\ - (!q w. Box q SUBFORMULA p /\ w IN W - ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x)) - -let K_STANDARD_MODEL_DEF = new_definition - `K_STANDARD_MODEL = GEN_STANDARD_MODEL K_FRAME {}`;; +|- `(W,R) IN K_STANDARD_FRAME p <=> +W = {w | MAXIMAL_CONSISTENT {} p w /\ + (!q. MEM q w ==> q SUBSENTENCE p)} /\ +(W,R) IN FINITE_FRAME /\ +(!q w. Box q SUBFORMULA p /\ w IN W + ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))` K_STANDARD_MODEL_CAR -|- K_STANDARD_MODEL p (W,R) V <=> +|- `K_STANDARD_MODEL p (W,R) V <=> (W,R) IN K_STANDARD_FRAME p /\ - (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p)) + (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))` +let K_STANDARD_MODEL_DEF = new_definition + `K_STANDARD_MODEL = GEN_STANDARD_MODEL {}`;; + +``` + +Definitions in `t_completeness.ml` (P=FINITE_FRAME, S=T_AX}) +``` +let T_STANDARD_FRAME_DEF = new_definition +`T_STANDARD_FRAME p = GEN_STANDARD_FRAME T_AX p`;; + +IN_T_STANDARD_FRAME +|- `!p W R. (W,R) IN T_STANDARD_FRAME p <=> + W = {w | MAXIMAL_CONSISTENT T_AX p w /\ + (!q. MEM q w ==> q SUBSENTENCE p)} /\ + (W,R) IN RF /\ + (!q w. Box q SUBFORMULA p /\ w IN W + ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))` + +let T_STANDARD_MODEL_DEF = new_definition + `T_STANDARD_MODEL = GEN_STANDARD_MODEL T_AX`;; + +T_STANDARD_MODEL_CAR +|- `!W R p V. + T_STANDARD_MODEL p (W,R) V <=> + (W,R) IN T_STANDARD_FRAME p /\ + (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))` +``` + +Definitions in `k4_completeness.ml` (P=FINITE_FRAME, S=T_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))`, ``` Definitions in `gl_completeness.ml` (P=ITF, S=GL_AX) From 14d9e203a90c620a7ebb6421e4713d0f5db3a077 Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Tue, 28 Jan 2025 13:06:20 +0100 Subject: [PATCH 07/16] Update README.md --- README.md | 54 +++++++++++++++++++++++++++++++++++------------------- 1 file changed, 35 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 2a3d430..e3d0812 100644 --- a/README.md +++ b/README.md @@ -1,34 +1,50 @@ # 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, Leonardo Quartini 2024.
+(c) Copyright, Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi 2025. See the [website](https://holms-lib.github.io/) for a brief overview of our [HOLMS library](https://github.com/HOLMS-lib/HOLMS) for the [HOL Light](https://hol-light.github.io/) theorem prover. -This repository introduces HOLMS (HOL-Light Library for Modal Systems), a new framework within the HOL Light proof assistant, designed for automated theorem proving and countermodel construction in modal logics. -Building on our prior work focused on Gödel-Löb logic (GL), we generalise our approach to cover a broader range of normal modal systems, starting here with: -- K: the minimal system; -- K4: a system properly extended by GL; -- GL: provability logic -- T: a system that is not extended by GL or K4, nor is an extension of K4 or K4. - -HOLMS provides a flexible mechanism for automating proof search and countermodel generation by leveraging labelled sequent calculi, interactive theorem proving, and formal completeness results. +This repository presents a second version of HOLMS (HOL-Light Library for Modal Systems), a modular framework designed for implementing modal reasoning within the HOL Light proof assistant. + +Extending our [previous work on Gödel-Löb logic (GL)](https://doi.org/10.1007/s10817-023-09677-z), we generalize our approach to formalize modal adequacy proofs for axiomatic calculi, thereby enabling the coverage of a broader range of normal modal systems. If the first version of HOLMS, [presented at Overlay 2024](), partially parametrized the completeness proof for GL and added the minimal system K, this second version of HOLMS fully generalizes our approach and, as a demonstration of the flexibility of our methodology, four modal system and their adequacy proofs are now implemented in HOLMS: +- **K**: the minimal system is developed in `k_completeness.ml`; +- **K4**: a system properly extended by GL is developed in `k4_completeness.ml`; +- **GL**: provability logic is developed and fully parametrized in `gl_completeness.ml`; +- **T**: a system that is not extended by GL or K4, nor is an extension of K4 or K4 is developed in `t_completeness.ml`. + +HOLMS lays the foundation for a comprehensive tool for modal reasoning in HOL, offering a high level of confidence and full automation by providing the essential mathematical components of principled decision algorithms for modal systems. The automated theorem prover and countermodel constructor for K and GL, already integrated into our library in `k_decid.ml` and `gl_decid.ml`, serve as evidence of the feasibility of this approach merging general purpose proof assistants, enriched sequent calculi, and formalised mathematics.` The top-level file is `make.ml`. -To partially generalise and parametrize the proof of completeness for normal systems, we develop four main theorems in `gen_completeness.ml`: +## Main Theorems + +For each normal system S, implemented in HOLMS in its file `S_completeness.ml`, we prove the following main theorems: +1. **The Correspondence theorem for S**
proves that a certain set of finite frames C, distinguished by a certain accessibility relation, correspond to S (for each frame in the set if p follows from S, then p is valid in such a frame).
+$C= CORR S$ and equivalently $\forall F \in C (S \vdash p \implies F \vDash p) \land \forall F((S \vdash p \implies F \vDash p) \implies F \in C)$ +(`APPRS_CORR_S`) +2. **Soundness of S with respect to CORR S**
+proves that if something is a theorem of S then it is valid in its correspondent frame.
+$\forall p (S \vdash p \implies CORR S \vDash p)$ +(`S_APPRS_VALID`) +3. **Consistency of S**
+proves that S cannot prove the false.
+$S \not \vdash \bot$ +(`S_CONSISTENT`) +5. **Completeness of S related to CORR S**
+proves that if someting holds in the set correspondent to S, then it is a theorem of S.
+$\forall p (CORR S \vDash p \implies S \vdash p)$ +(`S_COMPLETENESS_THM`) + +Moreover, for each of this systems, HOLMS presents a **simple decision procedure** to prove whether something is a theorem of S or not (`S_RULE`) and a fully automated theorem prover and countermodel constructor for K (`k_completeness.ml`) and GL (`gl_completeness.ml`). +For example, in `t_completeness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`; (5) `T_RULE`. + +To generalize and parametrize 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` - -For each normal system L, implemented in HOLMS, we prove the following main theorems: -1. **The Correspondence theorem for L** proves that a certain set of finite frames, distinguished by an accessibility relation with certain property, correspond (if p follows from L then p is valid in such a frame) to L. (`APPRL_CORR_L`) -2. **The Validity theorem for L** proves that if something is a theorem of L then it is valid in its appropriate frame. (`L_APPRL_VALID`) -3. **Consistency for L** proves that L cannot prove the false. (`L_CONSISTENT`) -4. **The completeness theorem for L** proves that if someting is valid in a frame that corresponds to L then it is a theorem of L. (`L_COMPLETENESS_THM`) -5. **A simple rule of decision for L** that applies a simple decision procedure to prove whether something is a theorem of L or not. (`L_RULE`) - -For example, in `t_completeness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`; (5) `T_RULE`. + # Usage guide and source code From 542bfadbebb1c9066128b541552df2bf6984112c Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Tue, 28 Jan 2025 14:28:26 +0100 Subject: [PATCH 08/16] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index e3d0812..ed8b7b2 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ See the [website](https://holms-lib.github.io/) for a brief overview of our [HOL This repository presents a second version of HOLMS (HOL-Light Library for Modal Systems), a modular framework designed for implementing modal reasoning within the HOL Light proof assistant. -Extending our [previous work on Gödel-Löb logic (GL)](https://doi.org/10.1007/s10817-023-09677-z), we generalize our approach to formalize modal adequacy proofs for axiomatic calculi, thereby enabling the coverage of a broader range of normal modal systems. If the first version of HOLMS, [presented at Overlay 2024](), partially parametrized the completeness proof for GL and added the minimal system K, this second version of HOLMS fully generalizes our approach and, as a demonstration of the flexibility of our methodology, four modal system and their adequacy proofs are now implemented in HOLMS: +Extending our [previous work on Gödel-Löb logic (GL)](https://doi.org/10.1007/s10817-023-09677-z), we generalize our approach to formalize modal adequacy proofs for axiomatic calculi, thereby enabling the coverage of a broader range of normal modal systems. If the first version of HOLMS, [presented at Overlay 2024](https://ceur-ws.org/Vol-3904/paper5.pdf), partially parametrized the completeness proof for GL and added the minimal system K, this second version of HOLMS fully generalizes our approach and, as a demonstration of the flexibility of our methodology, four modal system and their adequacy proofs are now implemented in HOLMS: - **K**: the minimal system is developed in `k_completeness.ml`; - **K4**: a system properly extended by GL is developed in `k4_completeness.ml`; - **GL**: provability logic is developed and fully parametrized in `gl_completeness.ml`; From d28f9babb610cb5fa431bff194f60722f89139cb Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Tue, 28 Jan 2025 14:33:48 +0100 Subject: [PATCH 09/16] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index ed8b7b2..cb29d80 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ Extending our [previous work on Gödel-Löb logic (GL)](https://doi.org/10.1007/ - **GL**: provability logic is developed and fully parametrized in `gl_completeness.ml`; - **T**: a system that is not extended by GL or K4, nor is an extension of K4 or K4 is developed in `t_completeness.ml`. -HOLMS lays the foundation for a comprehensive tool for modal reasoning in HOL, offering a high level of confidence and full automation by providing the essential mathematical components of principled decision algorithms for modal systems. The automated theorem prover and countermodel constructor for K and GL, already integrated into our library in `k_decid.ml` and `gl_decid.ml`, serve as evidence of the feasibility of this approach merging general purpose proof assistants, enriched sequent calculi, and formalised mathematics.` +HOLMS lays the foundation for a comprehensive tool for modal reasoning in HOL, offering a high level of confidence and full automation by providing the essential mathematical components of principled decision algorithms for modal systems. The automated theorem prover and countermodel constructor for K and GL, already integrated into our library in `k_decid.ml` and `gl_decid.ml`, serve as evidence of the feasibility of this approach merging general purpose proof assistants, enriched sequent calculi, and formalised mathematics. The top-level file is `make.ml`. From 41ce1864e1a6eae16a948b5b7553807d7c1e1f6e Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Thu, 30 Jan 2025 10:06:04 +0100 Subject: [PATCH 10/16] Update Semantics, Correspondence Theory, Soundness and consistency and GEN_COMPLETNESS --- README.md | 116 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 61 insertions(+), 55 deletions(-) diff --git a/README.md b/README.md index cb29d80..37997cd 100644 --- a/README.md +++ b/README.md @@ -11,7 +11,7 @@ Extending our [previous work on Gödel-Löb logic (GL)](https://doi.org/10.1007/ - **K**: the minimal system is developed in `k_completeness.ml`; - **K4**: a system properly extended by GL is developed in `k4_completeness.ml`; - **GL**: provability logic is developed and fully parametrized in `gl_completeness.ml`; -- **T**: a system that is not extended by GL or K4, nor is an extension of K4 or K4 is developed in `t_completeness.ml`. +- **T**: a system that is not extended by GL or K4, nor is an extension of GL or K4 is developed in `t_completeness.ml`. HOLMS lays the foundation for a comprehensive tool for modal reasoning in HOL, offering a high level of confidence and full automation by providing the essential mathematical components of principled decision algorithms for modal systems. The automated theorem prover and countermodel constructor for K and GL, already integrated into our library in `k_decid.ml` and `gl_decid.ml`, serve as evidence of the feasibility of this approach merging general purpose proof assistants, enriched sequent calculi, and formalised mathematics. @@ -36,9 +36,11 @@ proves that if someting holds in the set correspondent to S, then it is a theore $\forall p (CORR S \vDash p \implies S \vdash p)$ (`S_COMPLETENESS_THM`) -Moreover, for each of this systems, HOLMS presents a **simple decision procedure** to prove whether something is a theorem of S or not (`S_RULE`) and a fully automated theorem prover and countermodel constructor for K (`k_completeness.ml`) and GL (`gl_completeness.ml`). For example, in `t_completeness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`; (5) `T_RULE`. +Moreover, for each of this systems, HOLMS presents a **simple decision procedure** to prove whether something is a theorem of S or not (`S_RULE`) and a fully automated theorem prover and countermodel constructor for K (`k_completeness.ml`) and GL (`gl_completeness.ml`). + + To generalize and parametrize 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`; @@ -67,6 +69,9 @@ MODPROVES_DEDUCTION_LEMMA ## Relational semantics Kripke's Semantics of formulae. + +We define, by induction on the complexity of a formula, that a certain formula $A$ **holds in a certain world $w$ of a certain model $\langle W, R, V\rangle$**.
+$\langle W, R, V\rangle, w \vDash A$ ``` let holds = let pth = prove @@ -84,40 +89,44 @@ let holds = (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 in every world for every model of that frame.
+$\langle W, R\rangle \vDash p \iff \forall w \in W (\forall V (\langle W, R, V\rangle, w \vDash 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 correspondent frames. +We define the **set of frames correspondent 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 FINITE-FRAMES| \forall p (S \vdash p \implies \langle W,R \rangle \vDash p)$ } ``` let CORR_DEF = new_definition `CORR S = {(W:W->bool,R:W->W->bool) | (((W,R) IN FINITE_FRAME ) /\ (!p. [S. {} |~ p] ==> holds_in (W:W->bool,R:W->W->bool) (p)))}`;; ``` -We demonstrate that each frame that is correspondent to L is valid for L. -``` -GEN_CORR_VALID -|- `!S p. [S. {} |~ p] ==> CORR S:(W->bool)#(W->W->bool)->bool |= p`;; -``` -For each one of the normal system L developed in HOLMS we prove what set of frames is correspondent to L. +For each one of the normal system S developed in HOLMS we prove what set of frames is correspondent to S ($C= CORR S$), then we prove that every frame that is in C is correspondent to S ($\subseteq$: $\forall F \in C(S \vdash p \implies F \vDash p)$ ) and that every frame that is correspondent to S is in C ($\supseteq$: $\forall F((S \vdash p \implies F \vDash p) \implies F \in C)$ ). -### K-FINITE FRAMES -We prove that the set of finite frames is the correspond set to K. +### K-Finite Frames +We prove that the set of finite frames is the one correspondent to K. ``` FINITE_FRAME_CORR_K |-`FINITE_FRAME:(W->bool)#(W->W->bool)->bool = CORR {}`;; ``` -### T-REFLEXIVE FRAMES -We prove that the set of reflexive frames is the correspond set to T. +### T-Finite Reflexive Frames (RF) +We prove that the set of finite reflexive frames is the one correspondent to T. ``` let RF_DEF = new_definition `RF = @@ -130,8 +139,8 @@ let RF_DEF = new_definition RF_CORR_T |-`FINITE_FRAME:(W->bool)#(W->W->bool)->bool = CORR {}`;; ``` -### K4-TRANSITIVE FRAMES -We prove that the set of transitive frames is the correspond set to K4. +### K4-Finite Transitive Frames (TF) +We prove that the set of finite transitive frames is the one correspondent to K4. ``` let TF_DEF = new_definition `TF = @@ -144,8 +153,8 @@ let TF_DEF = new_definition TF_CORR_K4 |-`TF: (W->bool)#(W->W->bool)->bool = CORR K4_AX`;; ``` -### GL-IRREFLEXIVE AND TRANSITIVE FRAMES -We prove that the set of transitive and irreflexive frames is the correspond set to GL. +### GL-Finite Irreflexive and Transitive Frames (ITF) +We prove that the set of finite transitive and irreflexive frames is the one correspondent to GL. ``` let ITF_DEF = new_definition `ITF = @@ -160,34 +169,37 @@ ITF_CORR_GL |-`ITF: (W->bool)#(W->W->bool)->bool = CORR GL_AX`;; ``` +## Soundness and Consistency +We demonstrate the **soundness** of each S with respect to CORR S. +``` +GEN_CORR_VALID +|- `!S p. [S. {} |~ p] ==> CORR S:(W->bool)#(W->W->bool)->bool |= p`;; +``` + +Then, by specializing the proof of `GEN_CORR_VALID`, we prove the soundness of each normal system S developed in HOLMS with respect to its correspondent frame. +Moreover we prove its **consistency**, by modus ponens on the converse of `S_FRAME_VALID`. -## Soundness and consistency of K -We prove the consistency of K by modus ponens on the converse of `K_FRAME_VALID`. +### Soundness and consistency of K ``` -K_FRAME_VALID -|- !H p. - [{} . H |~ p] - ==> (!q. q IN H ==> K_FRAME:(W->bool)#(W->W->bool)->bool |= q) - ==> K_FRAME:(W->bool)#(W->W->bool)->bool |= p +let K_FINITE_FRAME_VALID = prove +(`!p. [{} . {} |~ p] ==> FINITE_FRAME:(W->bool)#(W->W->bool)->bool |= p`, +ASM_MESON_TAC[GEN_CORR_VALID; FINITE_FRAME_CORR_K]);; let K_CONSISTENT = prove (`~ [{} . {} |~ False]`, - REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] K_FRAME_VALID)) THEN + REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] K_FINITE_FRAME_VALID)) THEN REWRITE_TAC[NOT_IN_EMPTY] THEN - REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM; IN_K_FRAME; NOT_FORALL_THM] THEN + REWRITE_TAC[valid; holds; holds_in; FORALL_PAIR_THM; IN_FINITE_FRAME; 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[]);; ``` -## Soundness and consistency of T -To develop this proof of consistency we use modal correspondence theory for T and, by `GEN_CORR_VALID `, we prove `T_RF_VALID`. -``` -T_RF_VALID -|- `!p. [T_AX . {} |~ p] ==> RF:(W->bool)#(W->W->bool)->bool |= p` +### Soundness and consistency of T ``` +let T_RF_VALID = prove + (`!p. [T_AX . {} |~ p] ==> RF:(W->bool)#(W->W->bool)->bool |= p`, + MESON_TAC[GEN_CORR_VALID; RF_CORR_T]);; -We prove the consistency of T by modus ponens on the converse of `T_FRAME_VALID`. -``` let T_CONSISTENT = prove (`~ [T_AX . {} |~ False]`, REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] T_RF_VALID)) THEN @@ -197,16 +209,12 @@ let T_CONSISTENT = prove REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);; ``` -## Soundness and consistency of K4 -To develop this proof of consistency we use modal correspondence theory for K4 and, by `GEN_CORR_VALID `, we prove `K4_TF_VALID`. - -``` -K4_TF_VALID -|- `!p. [K4_AX . {} |~ p] ==> TF:(W->bool)#(W->W->bool)->bool |= p` +### Soundness and consistency of K4 ``` +let K4_TF_VALID = prove + (`!p. [K4_AX . {} |~ p] ==> TF:(W->bool)#(W->W->bool)->bool |= p`, + MESON_TAC[GEN_CORR_VALID; TF_CORR_K4]);; -The consistency theorem for K4 is proved by modus ponens on the converse of `K4_TF_VALID`. -``` let K4_CONSISTENT = prove (`~ [K4_AX . {} |~ False]`, REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] K4_TF_VALID)) THEN @@ -216,16 +224,12 @@ let K4_CONSISTENT = prove REWRITE_TAC[NOT_INSERT_EMPTY; FINITE_SING; IN_SING] THEN MESON_TAC[]);; ``` -## Soundness and consistency of GL -To develop this proof of consistency we use modal correspondence theory for GL and, by `GEN_CORR_VALID `, we prove `GL_ITF_VALID`. - -``` -GL_ITF_VALID -|- !p. [GL_AX . {} |~ p] ==> ITF:(W->bool)#(W->W->bool)->bool |= p +### 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_CORR_VALID; ITF_CORR_GL]);; -The consistency theorem for GL is proved by modus ponens on the converse of `GL_ITF_VALID`. -``` let GL_consistent = prove (`~ [GL_AX . {} |~ False]`, REFUTE_THEN (MP_TAC o MATCH_MP (INST_TYPE [`:num`,`:W`] GL_ITF_VALID)) THEN @@ -472,14 +476,16 @@ GL_COMPLETENESS_THM ``` ### Modal completeness for models on a generic (infinite) domain. -Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we quickly generalize the completeness theorem for models with infinite worlds for each normal sysrem. - +Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we quickly generalize for each normal system the completeness theorem for models with infinite worlds.
+In `gen_completeness`. ``` GEN_LEMMA_FOR_GEN_COMPLETENESS |- `!S. INFINITE (:A) ==> !p. CORR S:(A->bool)#(A->A->bool)->bool |= p ==> CORR S:(form list->bool)#(form list->form list->bool)->bool |= p`;; - +``` +As corollaries of `GEN_LEMMA_FOR_GEN_COMPLETENESS` in the specific files. +``` K_COMPLETENESS_THM_GEN |- `!p. INFINITE (:A) /\ FINITE_FRAME:(A->bool)#(A->A->bool)->bool |= p ==> [{} . {} |~ p]` From 2f10e0f48ec20583816ad961e6764c9d8e371e99 Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Thu, 30 Jan 2025 13:34:48 +0100 Subject: [PATCH 11/16] Completness proof sketch (1) --- README.md | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 66 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 37997cd..a7540db 100644 --- a/README.md +++ b/README.md @@ -241,9 +241,72 @@ let GL_consistent = prove ## Completeness theorems -The proof is organized in three steps. -We can observe that, by working with HOL, it is possible to identify all those lines of reasoning that are _parametric_ for P (the specific propriety of each frame of a logic) and S (the set of axioms of the logic) -and develop each of of the three steps while avoiding code duplication as much as possible. +### Proof Sketch (1) + +Given a modal system $S$, we want to prove that it is **complete with respect to the set of its correspondent frames**: $\forall p (CORRS \vDash p \implies S \vdash p)$ + +``` +S_COMPLETNESS_THM +|. `!p. ( CORR S |= p ==> [S. {} |~ p])` +``` +**1. Rewriting `S_COMPLETNESS`'s statment**
+By using some tautologies and rewriting, we can show that the completeness theorem is equivalent to a more handy sentence:
+$\forall p (S \not \vdash p \implies \exists \langle W,R\rangle_{S,p} \in CORR_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 rewrite the sentence by _contraposition_.
+`e GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM];;`
+ +B. We rewrite validity in a set of frames (`valid`) as validity in a certain world of a certain model (`holds`) and we exploit some _propositional tautologies_.
+`e (REWRITE_TAC[valid; NOT_FORALL_THM; FORALL_PAIR_THM; holds_in; NOT_IMP]);;`
+ +``` +S_COMPLETNESS_THM' +|- `!p. ( `~[S . {} |~ p] ==> + (exists W R. W,R IN CORR S /\ + (exists V m. m IN p1 /\ + ~holds (p1,p2) V p w)))` +``` + +At this point, for each modal formula $p$ we need to construct a **_countermodel_** $𝓜_{S,p}$ and a "**_counterworld_**" $m_{S,p}$ in the domain of the countermodel. + +We can observe that, by working with HOL, it is possible to 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 develop te proof while avoiding code duplication as much as possible. + +**2. Reducing a model theoretic-notion to a set/list-theoretic concept** +The canonical proof of completeness, illustrated in classical textbooks like George Boolos's "The Logic of Provability", exploit 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 set (list in HOLMS) of modal formulas. +If we are able to construct a countermodel with this constraints, we will easily construct a counterworld $m_{S,p}$ that is a set of formulas not including p. + +Then our subgoal would be to prove:
+``` +S_COMPLETNESS_THM'' +|- `!p. ( `~[S . {} |~ p] ==> + (exists W R. W,R IN CORR S /\ + (exists M. M IN p1 /\ + ~ MEM p M)))` +``` + + This subgoal is much more manageable than the previous statement, indeed it reduces the **model-theoretic** notion of _validity_ (`holds (W,R) V p w`) to the **set-theoretic** concept (**list-theoretic** in HOLMS) of _membership_ (`MEM p w`). + + +**3. What do we need to prove?**
+Given our aim of proving $\forall p(S \not \vdash p \implies \exists \langle W,R \rangle_{S,p} \in CORR 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 **correspondent** to S.
+$\langle W,R \rangle_{S,p} \in CORRS$
+ +B. The Kripke's model $𝓜_{S,p} = \langle W,R,V \rangle_{S,p}$ must allows us to **reduce validity to membership**.
+Namely, for our model $𝓜_{S,p}$ holds $\forall w \in W_{S,p} (w \in p \iff 𝓜_{S,p},w \vDash p) $. + +C. The counterworld $m_{S,p}$ must not contain p.
+$p \not \in m_{S,p}$ + +D. Consequently $W_{S,p}$ must be a **set of formula's lists**
+`CORRS:(form list->bool)#(form list->form list->bool)->bool`. + +### The Proof (1) + +The first part of the proof is organized in three steps. ### STEP 1 Identification of a model depending on a formula p and, in particular, of a non-empty set of possible worlds given by a subclass of maximal consistent sets of formulas. From 8b1c3a6b51787f94d6b4d9c4b0db9a55883de884 Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Thu, 30 Jan 2025 20:06:24 +0100 Subject: [PATCH 12/16] Final Update --- README.md | 657 ++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 462 insertions(+), 195 deletions(-) diff --git a/README.md b/README.md index a7540db..8d65dc3 100644 --- a/README.md +++ b/README.md @@ -240,8 +240,9 @@ let GL_consistent = prove ``` ## Completeness theorems +We first sketch the idea behind the demonstration and, then, we will presnt a three-steps proof. -### Proof Sketch (1) +### 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 correspondent frames**: $\forall p (CORRS \vDash p \implies S \vdash p)$ @@ -249,16 +250,13 @@ Given a modal system $S$, we want to prove that it is **complete with respect to S_COMPLETNESS_THM |. `!p. ( CORR S |= p ==> [S. {} |~ p])` ``` -**1. Rewriting `S_COMPLETNESS`'s statment**
+- **1. Rewriting `S_COMPLETNESS`'s statment**
By using some tautologies and rewriting, we can show that the completeness theorem is equivalent to a more handy sentence:
-$\forall p (S \not \vdash p \implies \exists \langle W,R\rangle_{S,p} \in CORR_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 rewrite the sentence by _contraposition_.
-`e GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM];;`
- -B. We rewrite validity in a set of frames (`valid`) as validity in a certain world of a certain model (`holds`) and we exploit some _propositional tautologies_.
-`e (REWRITE_TAC[valid; NOT_FORALL_THM; FORALL_PAIR_THM; holds_in; NOT_IMP]);;`
- +$\forall p (S \not \vdash p \implies \exists \langle W,R\rangle_{S,p} \in CORR_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 rewrite the sentence by _contraposition_.
+ `e GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM];;`

+ - B. We rewrite validity in a set of frames (`valid`) as validity in a certain world of a certain model (`holds`) and we exploit some _propositional tautologies_.
+ `e (REWRITE_TAC[valid; NOT_FORALL_THM; FORALL_PAIR_THM; holds_in; NOT_IMP]);;`
``` S_COMPLETNESS_THM' |- `!p. ( `~[S . {} |~ p] ==> @@ -266,17 +264,14 @@ S_COMPLETNESS_THM' (exists V m. m IN p1 /\ ~holds (p1,p2) V p w)))` ``` - -At this point, for each modal formula $p$ we need to construct a **_countermodel_** $𝓜_{S,p}$ and a "**_counterworld_**" $m_{S,p}$ in the domain of the countermodel. - -We can observe that, by working with HOL, it is possible to 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 develop te proof while avoiding code duplication as much as possible. - -**2. Reducing a model theoretic-notion to a set/list-theoretic concept** -The canonical proof of completeness, illustrated in classical textbooks like George Boolos's "The Logic of Provability", exploit 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) $. - +At this point, for each modal formula $p$ we need to construct a **_countermodel_** $𝓜_{S,p}$ and a "**_counterworld_**" $m_{S,p}$ in the domain of the countermodel.

+We can observe that, by working with HOL, it is possible to 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 develop te proof while avoiding code duplication as much as possible.
+
+- **2. Reducing a model theoretic-notion to a set/list-theoretic concept** +The canonical proof of completeness, illustrated in classical textbooks like George Boolos's "The Logic of Provability", exploit 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 set (list in HOLMS) of modal formulas. If we are able to construct a countermodel with this constraints, we will easily construct a counterworld $m_{S,p}$ that is a set of formulas not including p. - +

Then our subgoal would be to prove:
``` S_COMPLETNESS_THM'' @@ -285,98 +280,98 @@ S_COMPLETNESS_THM'' (exists M. M IN p1 /\ ~ MEM p M)))` ``` +This subgoal is much more manageable than the previous statement, indeed it reduces the **model-theoretic** notion of _validity_ (`holds (W,R) V p w`) to the **set-theoretic** concept (**list-theoretic** in HOLMS) of _membership_ (`MEM p w`). - This subgoal is much more manageable than the previous statement, indeed it reduces the **model-theoretic** notion of _validity_ (`holds (W,R) V p w`) to the **set-theoretic** concept (**list-theoretic** in HOLMS) of _membership_ (`MEM p w`). +- **3. What do we need to prove?**
+Given our aim of proving $\forall p(S \not \vdash p \implies \exists \langle W,R \rangle_{S,p} \in CORR 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 **correspondent** to S.
+ $\langle W,R \rangle_{S,p} \in CORRS$

+ - B. The Kripke's model $𝓜_{S,p} = \langle W,R,V \rangle_{S,p}$ must allows us to **reduce validity to membership**.
+ Namely, for our model $𝓜_{S,p}$ holds $\forall w \in W_{S,p} (w \in p \iff 𝓜_{S,p},w \vDash p) $.

+ - C. The counterworld $m_{S,p}$ must not contain p.
+ $p \not \in m_{S,p}$

+ - D. Consequently $W_{S,p}$ must be a **set of formula's lists**
+ `CORRS:(form list->bool)#(form list->form list->bool)->bool`. -**3. What do we need to prove?**
-Given our aim of proving $\forall p(S \not \vdash p \implies \exists \langle W,R \rangle_{S,p} \in CORR 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 **correspondent** to S.
-$\langle W,R \rangle_{S,p} \in CORRS$
+### STEP 1: Partial definition of a parametric Standard Model -B. The Kripke's model $𝓜_{S,p} = \langle W,R,V \rangle_{S,p}$ must allows us to **reduce validity to membership**.
-Namely, for our model $𝓜_{S,p}$ holds $\forall w \in W_{S,p} (w \in p \iff 𝓜_{S,p},w \vDash p) $. +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 'STANDARD_MODEL` in step 1 is fully parametric. -C. The counterworld $m_{S,p}$ must not contain p.
-$p \not \in m_{S,p}$ +Before this construction of the countermodel, we defined in `consistent.ml` some properties that hold for formulas' lists. -D. Consequently $W_{S,p}$ must be a **set of formula's lists**
-`CORRS:(form list->bool)#(form list->form list->bool)->bool`. +#### Consistent $S$ +A list of formulas $X$ is consistent to a set of axioms $S$ iff and only if $S \not \vdash \neg \bigwedge X$ +``` +let CONSISTENT = new_definition + `CONSISTENT S (X:form list) <=> ~[S . {} |~ Not (CONJLIST X)]`;; +``` -### The Proof (1) +#### Maximal Consistent $S,p$
+A list of formulas $X$ is maximal-consistent to a set of axioms $S$ and modal formula $p$ iff X has no repetitions, X is consistent $_S$ and $\forall q (q \ subformula \ 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)`;; +``` -The first part of the proof is organized in three steps. +#### Lemma of Extension of Maximal Consistent lists +$X \ Consistent_S \implies \exists M (X \subseteq M \ \land \ M \ Maximal-Consistent_{S,p} )$ +``` +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` +``` -### STEP 1 -Identification of a model depending on a formula p and, in particular, of a non-empty set of possible worlds given by a subclass of maximal consistent sets of formulas. +Then we define a **standard model** such that: -Parametric Definitions in `gen_completeness.ml` (parameters P, S) +- **A: The Domain $W_{S,p}$ is $ { $X | Maximal-Consistent_{S,p} \ X $ }**

+ As requested the domain is a set of list 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 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. ``` -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)}`;; +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 \ subformula \ p \implies \forall w \in W_{S,p}(\Box q \in w \iff \forall x (wRx \implies q \in x)))$.
+ This condition ensures that my list-theoretic translation follows kripke's semantics. + - R2: $\langle W,R \rangle_{S,p} \in CORR S$.
+ This second condition guarantees one of the four initial constraints. + +- **C: The Evaluation Relation $R_{S,p}$** is defined as follows
+ $\forall m \in W_{S,p} \ \forall a \in Atom-Form_{\Box} (mVa \iff a \ subformula \ p \land a \in m)$ + +In particular, in HOLMS `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 P S p = - FRAME INTER P INTER + `GEN_STANDARD_FRAME S p = + CORR 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 P S p (W,R) V <=> - (W,R) IN GEN_STANDARD_FRAME P S p /\ + `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 a simple specification of `GEN_STANDARD_FRAME` and `GEN_STANDARD_MODEL` with the parameters `{}`, `T_AX`, `K4_AX` and `GL_AX`, we present here just the definitions for $K4$. -Definitions in `k_completeness.ml` (P=FINITE_FRAME, S={}) -``` -let K_STANDARD_FRAME_DEF = new_definition - `K_STANDARD_FRAME = GEN_STANDARD_FRAME {}`;; - -IN_K_STANDARD_FRAME -|- `(W,R) IN K_STANDARD_FRAME p <=> -W = {w | MAXIMAL_CONSISTENT {} p w /\ - (!q. MEM q w ==> q SUBSENTENCE p)} /\ -(W,R) IN FINITE_FRAME /\ -(!q w. Box q SUBFORMULA p /\ w IN W - ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))` - -K_STANDARD_MODEL_CAR -|- `K_STANDARD_MODEL p (W,R) V <=> - (W,R) IN K_STANDARD_FRAME p /\ - (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))` -let K_STANDARD_MODEL_DEF = new_definition - `K_STANDARD_MODEL = GEN_STANDARD_MODEL {}`;; - -``` - -Definitions in `t_completeness.ml` (P=FINITE_FRAME, S=T_AX}) -``` -let T_STANDARD_FRAME_DEF = new_definition -`T_STANDARD_FRAME p = GEN_STANDARD_FRAME T_AX p`;; - -IN_T_STANDARD_FRAME -|- `!p W R. (W,R) IN T_STANDARD_FRAME p <=> - W = {w | MAXIMAL_CONSISTENT T_AX p w /\ - (!q. MEM q w ==> q SUBSENTENCE p)} /\ - (W,R) IN RF /\ - (!q w. Box q SUBFORMULA p /\ w IN W - ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))` - -let T_STANDARD_MODEL_DEF = new_definition - `T_STANDARD_MODEL = GEN_STANDARD_MODEL T_AX`;; - -T_STANDARD_MODEL_CAR -|- `!W R p V. - T_STANDARD_MODEL p (W,R) V <=> - (W,R) IN T_STANDARD_FRAME p /\ - (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))` -``` - -Definitions in `k4_completeness.ml` (P=FINITE_FRAME, S=T_AX}) +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`;; @@ -399,42 +394,21 @@ K4_STANDARD_MODEL_CAR (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`, ``` -Definitions in `gl_completeness.ml` (P=ITF, S=GL_AX) -``` -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)}`;; - -let GL_STANDARD_FRAME_DEF = new_definition - `GL_STANDARD_FRAME p = GEN_STANDARD_FRAME ITF GL_AX p`;; - -IN_GL_STANDARD_FRAME -|- !p W R. (W,R) IN GL_STANDARD_FRAME p <=> - W = {w | MAXIMAL_CONSISTENT GL_AX p w /\ - (!q. MEM q w ==> q SUBSENTENCE p)} /\ - (W,R) IN ITF /\ - (!q w. Box q SUBFORMULA p /\ w IN W - ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x)) -let GL_STANDARD_MODEL_DEF = new_definition - `GL_STANDARD_MODEL = GEN_STANDARD_MODEL ITF GL_AX`;; +### STEP 2: Definition of a standard accessibility relation for each S +The definition of a standard acessibility relation cannot be fully parametrized, at least following the approach presented in classical textbook. -GL_STANDARD_MODEL_CAR -|- !W R p V. - GL_STANDARD_MODEL p (W,R) V <=> - (W,R) IN GL_STANDARD_FRAME p /\ - (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p)) -``` +Consequently, to avoid code repetions in `gen_completeness.ml` we will define a `GEN_STANDARD_REL` that is parametric to $S$ and $p$, but then we will complete the definition of the standard relation for each normal system in the spefic file of each system `S_completeness.ml` in a way that guarantees that conditions R1 and R2 holds. -### STEP 2 -Definition of a “standard” accessibility relation depending on axiom set S between these worlds such that the frame is appropriate to S. +After we have defined the `S_STANDARD_REL` we will show: +- The most difficult verse of R1's implication in `S_ACCESSIBILITY_LEMMA`
+$\forall q \in Form_{\Box} (\Box q \ subformula \ 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 CORRS$ + +Then `SF_IN_STANDARD_S_FRAME` follows as corollary and, given the hypotesis that $S \not \vdash p$, $\langle W_{S,p},$ S_STANDARD_REL $, V_{S,p} \rangle$ is an `S_STANDARD_MODEL`. -Parametric definition of the standard relation in `gen_completeness.ml` (parameter S) +#### Parametric definition of the standard relation in `gen_completeness`. ``` let GEN_STANDARD_REL = new_definition `GEN_STANDARD_REL S p w x <=> @@ -443,27 +417,161 @@ let GEN_STANDARD_REL = new_definition (!B. MEM (Box B) w ==> MEM B x)`;; ``` -Definitions in `k_completeness.ml` (S={}) and proof of the Accessibility Lemma for 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`;; K_STANDARD_REL_CAR -|- K_STANDARD_REL p w x <=> +|- `K_STANDARD_REL p w x <=> MAXIMAL_CONSISTENT {} p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\ MAXIMAL_CONSISTENT {} p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\ - (!B. MEM (Box B) w ==> MEM B x) - -K_ACCESSIBILITY_LEMMA_1 -|- !p w q. ~ [{} . {} |~ p] /\ - MAXIMAL_CONSISTENT {} p w /\ - (!q. MEM q w ==> q SUBSENTENCE p) /\ - Box q SUBFORMULA p /\ - (!x. K_STANDARD_REL p w x ==> MEM q x) - ==> MEM (Box q) w -``` - -Definitions in `gl_completeness.ml` (S=GL_AX) and proofs of the Accessibility Lemma for GL. + (!B. MEM (Box B) w ==> MEM B x)` +``` + +**Accessibility Lemma for K** that ensures the most difficult verse of R1's implication. +``` +K_ACCESSIBILITY_LEMMA +|- `!p w q. ~ [{} . {} |~ p] /\ + MAXIMAL_CONSISTENT {} p w /\ + (!q. MEM q w ==> q SUBSENTENCE p) /\ + Box q SUBFORMULA p /\ + (!x. K_STANDARD_REL p w x ==> MEM q x) + ==> MEM (Box q) w` +``` +**Maximal Consistent Lemma for K** that ensures R2. +``` +K_MAXIMAL_CONSISTENT +|- (`!p. ~ [{} . {} |~ p] + ==> ({M | MAXIMAL_CONSISTENT {} p M /\ + (!q. MEM q M ==> q SUBSENTENCE p)}, + K_STANDARD_REL p) IN FINITE_FRAME`, +``` +Proof of the corollary that ensures that **our construction for K is a standard frame**. +``` +g `!p. ~ [{} . {} |~ p] + ==> ({M | MAXIMAL_CONSISTENT {} p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + K_STANDARD_REL p) IN K_STANDARD_FRAME p`;; +e (INTRO_TAC "!p; not_theor_p");; +e (REWRITE_TAC [IN_K_STANDARD_FRAME]);; +e CONJ_TAC;; +e (MATCH_MP_TAC K_MAXIMAL_CONSISTENT);; +e (ASM_REWRITE_TAC[]);; +e (INTRO_TAC "!q w; subform w_in");; +e EQ_TAC;; + e (ASM_MESON_TAC[K_STANDARD_REL_CAR]);; + e (INTRO_TAC "Implies_Mem_q");; + e (HYP_TAC "w_in" (REWRITE_RULE[IN_ELIM_THM]));; + e (MATCH_MP_TAC K_ACCESSIBILITY_LEMMA);; + e (EXISTS_TAC `p:form`);; + e (ASM_REWRITE_TAC[]);; +let KF_IN_STANDARD_K_FRAME = top_thm();; +``` + + +#### 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`;; + +T_STANDARD_REL_CAR +|- `!p w x. + T_STANDARD_REL p w x <=> + MAXIMAL_CONSISTENT T_AX p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\ + MAXIMAL_CONSISTENT T_AX p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\ + (!B. MEM (Box B) w ==> MEM B x)` +``` + +**Accessibility Lemma for T** that ensures the most difficult verse of R1's implication. +``` +T_ACCESSIBILITY_LEMMA +|- `!p w q. + ~ [T_AX . {} |~ p] /\ + MAXIMAL_CONSISTENT T_AX p w /\ + (!q. MEM q w ==> q SUBSENTENCE p) /\ + Box q SUBFORMULA p /\ + (!x. T_STANDARD_REL p w x ==> MEM q x) + ==> MEM (Box q) w` +``` +**Maximal Consistent Lemma for T** that ensures R2. +``` +RF_MAXIMAL_CONSISTENT +|- `!p. ~ [T_AX . {} |~ p] + ==> ({M | MAXIMAL_CONSISTENT T_AX p M /\ + (!q. MEM q M ==> q SUBSENTENCE p)}, + T_STANDARD_REL p) IN RF ` +``` +Proof of the corollary that ensures that **our construction for T is a standard frame**. +``` +g `!p. ~ [T_AX . {} |~ p] + ==> ({M | MAXIMAL_CONSISTENT T_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + T_STANDARD_REL p) IN T_STANDARD_FRAME p`;; +e (INTRO_TAC "!p; not_theor_p");; +e (REWRITE_TAC [IN_T_STANDARD_FRAME]);; +e CONJ_TAC;; +e (MATCH_MP_TAC RF_MAXIMAL_CONSISTENT);; +e (ASM_REWRITE_TAC[]);; +e (ASM_REWRITE_TAC[IN_ELIM_THM]);; +e (INTRO_TAC "!q w; boxq maxw subw");; +e EQ_TAC;; + e (ASM_MESON_TAC[T_STANDARD_REL_CAR]);; + e (ASM_MESON_TAC[T_ACCESSIBILITY_LEMMA]);; +let RF_IN_T_STANDARD_FRAME = top_thm();; +``` +#### 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)`;; + +K4_STANDARD_REL_CAR +|- `!p w x. + K4_STANDARD_REL p w x <=> + MAXIMAL_CONSISTENT K4_AX p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\ + MAXIMAL_CONSISTENT K4_AX p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\ + (!B. MEM (Box B) w ==> MEM (Box B) x /\ MEM B x)` +``` + +**Accessibility Lemma for K4** that ensures the most difficult verse of R1's implication. +``` +K4_ACCESSIBILITY_LEMMA +|- `!p w q. + ~ [K4_AX . {} |~ p] /\ + MAXIMAL_CONSISTENT K4_AX p w /\ + (!q. MEM q w ==> q SUBSENTENCE p) /\ + Box q SUBFORMULA p /\ + (!x. K4_STANDARD_REL p w x ==> MEM q x) + ==> MEM (Box q) w` +``` +**Maximal Consistent Lemma for K4** that ensures R2. +``` +TF_MAXIMAL_CONSISTENT +|- `!p. ~ [T_AX . {} |~ p] + ==> ({M | MAXIMAL_CONSISTENT T_AX p M /\ + (!q. MEM q M ==> q SUBSENTENCE p)}, + T_STANDARD_REL p) IN RF ` +``` +Proof of the corollary that ensures that **our construction for K4 is a standard frame**. +``` +g `!p. ~ [K4_AX . {} |~ p] + ==> ({M | MAXIMAL_CONSISTENT K4_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + K4_STANDARD_REL p) IN K4_STANDARD_FRAME p`;; +e (INTRO_TAC "!p; not_theor_p");; +e (REWRITE_TAC [IN_K4_STANDARD_FRAME]);; +e CONJ_TAC;; +e (MATCH_MP_TAC TF_MAXIMAL_CONSISTENT);; +e (ASM_REWRITE_TAC[]);; +e (ASM_REWRITE_TAC[IN_ELIM_THM]);; +e (INTRO_TAC "!q w; boxq maxw subw");; +e EQ_TAC;; + e (ASM_MESON_TAC[K4_STANDARD_REL_CAR]);; + e (ASM_MESON_TAC[K4_ACCESSIBILITY_LEMMA]);; +let K4F_IN_K4_STANDARD_FRAME = top_thm();; +``` + +#### Definition of the standard relation for GL in `gl_completeness.ml`. ``` let GL_STANDARD_REL_DEF = new_definition `GL_STANDARD_REL p w x <=> @@ -471,75 +579,205 @@ let GL_STANDARD_REL_DEF = new_definition (!B. MEM (Box B) w ==> MEM (Box B) x) /\ (?E. MEM (Box E) x /\ MEM (Not (Box E)) w)`;; +GL_STANDARD_REL_CAR +|- `!p w x. + GL_STANDARD_REL p w x <=> + MAXIMAL_CONSISTENT GL_AX p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\ + MAXIMAL_CONSISTENT GL_AX p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\ + (!B. MEM (Box B) w ==> MEM (Box B) x /\ MEM B x) /\ + (?E. MEM (Box E) x /\ MEM (Not (Box E)) w)` +``` + +**Accessibility Lemma for GL** that ensures the most difficult verse of R1's implication. +``` GL_ACCESSIBILITY_LEMMA -|- !p M w q. +|- `!p w q. ~ [GL_AX . {} |~ p] /\ - MAXIMAL_CONSISTENT GL_AX p M /\ - (!q. MEM q M ==> q SUBSENTENCE p) /\ MAXIMAL_CONSISTENT GL_AX p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\ - MEM (Not p) M /\ Box q SUBFORMULA p /\ (!x. GL_STANDARD_REL p w x ==> MEM q x) - ==> MEM (Box q) w + ==> MEM (Box q) w` ``` - -### STEP 3 -The reduction of the notion of forcing `holds (W,R) V q w` to that of a set-theoretic (list-theoretic) membership MEM q w -for every subformula q of p, through a specific atomic evaluation function on (W,R). - -Parametric truth lemma in `gen_completeness.ml` (parameters P, S) +**Maximal Consistent Lemma for GL** that ensures R2. ``` -GEN_TRUTH_LEMMA -|- !P S W R p V q. - ~ [S . {} |~ p] /\ - GEN_STANDARD_MODEL P S p (W,R) V /\ - q SUBFORMULA p - ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w) +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 ` ``` - -Truth lemma specified for K in `k_completeness.ml` (P=K_FRAME, S={}) +Proof of the corollary that ensures that **our construction for GL is a standard frame**. ``` -let K_TRUTH_LEMMA = prove - (`!W R p V q. - ~ [{} . {} |~ p] /\ - K_STANDARD_MODEL p (W,R) V /\ - q SUBFORMULA p - ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)`, - REWRITE_TAC[K_STANDARD_MODEL_DEF] THEN MESON_TAC[GEN_TRUTH_LEMMA]);; +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();; ``` -Truth lemma specified for GL in `gl_completeness.ml` (P=ITF, S=GL_AX) + +### STEP 3: Proving the truth lemma +In this step we prove that, given a standard model and $S \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 forcing `holds (W,R) V q w` to that of a set-theoretic (list-theoretic) membership `MEM q w`. + +Observe that we prove this foundamental lemma in a fully parametric way and, moreover, the proof of completness does not need to specify this lemma for our normal system in analysis. + +#### Parametric truth lemma in `gen_completeness.ml` (parameters P, S) ``` -let GL_truth_lemma = prove - (`!W R p V q. - ~ [GL_AX . {} |~ p] /\ - GL_STANDARD_MODEL p (W,R) V /\ +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)`, - REWRITE_TAC[GL_STANDARD_MODEL_DEF] THEN MESON_TAC[GEN_TRUTH_LEMMA]);; + ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)` ``` ### The Theorems -Completeness of K in `k_completeness.ml`. -This proof uses the `K_TRUTH_LEMMA` that specifies the `GEN_TRUTH_LEMMA`, therefore the first part of the proof of the completeness theorem for K is completely parametrized. -``` -K_COMPLETENESS_THM -|- !p. K_FRAME:(form list->bool)#(form list->form list->bool)->bool |= p - ==> [{} . {} |~ p] -``` - -Completeness of GL in `gl_completeness.ml` -This proof uses the `GL_TRUTH_LEMMA` that specifies the `GEN_TRUTH_LEMMA`, therefore the first part of the proof of the completeness theorem for GL is completely parametrized. -``` -GL_COMPLETENESS_THM -|- !p. ITF:(form list->bool)#(form list->form list->bool)->bool |= p - ==> [GL_AX . {} |~ p] +At this point we built up a _countermodel_ $\langle W,R,V \rangle_{S,p}$ that is a _standard model for S_ and we want to prove that a counterworld in this model exists:
+ $\exist 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 $Maximal_Consistent_{S,p} M$; + - B: $p \not \in M_{S,p}$ + +But thanks to our theorem `NONEMPTY_MAXIMAL_CONSISTENT` $\forall p (S \vdash p \implies (\exists M (Maximal_Consistent_{S,p} M \land \neg p \in M))$,
we know that such an $M_{S,p}$ exists and we can prove `GEN_COUNTERMODEL_ALT`. Observe, indeed, that $Maximal_Consistent_{S,p} M \land \neg p \in M \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)` + + +g `!S W R p. ~ [S . {} |~ p] /\ + (W,R) IN GEN_STANDARD_FRAME S p + ==> + ~holds_in (W,R) p`;; +e (INTRO_TAC "!S W R p; p_not_theor in_standard_frame");; +e (REWRITE_TAC[holds_in; NOT_FORALL_THM; NOT_IMP; IN_ELIM_THM]);; +e (EXISTS_TAC `\a M. Atom a SUBFORMULA p /\ MEM (Atom a) M`);; +e (DESTRUCT_TAC "@M. max mem subf" (MATCH_MP NONEMPTY_MAXIMAL_CONSISTENT (ASSUME `~ [S . {} |~ p]`)));; +e (EXISTS_TAC `M:form list` THEN ASM_REWRITE_TAC[]);; +e (SUBGOAL_THEN `GEN_STANDARD_MODEL S p (W,R) (\a M. Atom a SUBFORMULA p /\ MEM (Atom a) M) ` MP_TAC);; +e (ASM_MESON_TAC[GEN_STANDARD_MODEL_DEF]);; +e (INTRO_TAC "standard_model");; +e CONJ_TAC;; +e (HYP_TAC "in_standard_frame" (REWRITE_RULE[IN_GEN_STANDARD_FRAME]));; +e (ASM_REWRITE_TAC[IN_ELIM_THM]);; +e (MP_TAC (ISPECL + [`S: form ->bool`; + `W: (form)list->bool`; + `R: (form)list-> (form)list ->bool`; + `p:form`; + `(\a M. Atom a SUBFORMULA p /\ MEM (Atom a) M):((char)list->(form)list->bool)`; + `p:form`] GEN_TRUTH_LEMMA));; +e (ANTS_TAC );; +e (ASM_REWRITE_TAC[SUBFORMULA_REFL]);; +e (DISCH_THEN (MP_TAC o SPEC `M:form list`));; +e ANTS_TAC;; +e (HYP_TAC "standard_model" (REWRITE_RULE[GEN_STANDARD_MODEL_DEF; IN_GEN_STANDARD_FRAME]));; +e (ASM_REWRITE_TAC[IN_ELIM_THM]);; +e (DISCH_THEN (SUBST1_TAC o GSYM));; +e (ASM_MESON_TAC[MAXIMAL_CONSISTENT; CONSISTENT_NC]);; +let GEN_COUNTERMODEL_ALT = top_thm();; +``` + +Given the fully parametrized `GEN_COUNTERMODEL_ALT` and `SF_IN_STANDARD_S_FRAME`, the completeness theorems for each $S$ follow and their proofs are so short that we can present them here. + +#### Completeness of K in `k_completeness.ml`. +``` +g `!p. FINITE_FRAME:(form list->bool)#(form list->form list->bool)->bool |= p + ==> [{} . {} |~ 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 {} p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + K_STANDARD_REL p)`);; +e (REWRITE_TAC[NOT_IMP] THEN CONJ_TAC );; +e (MATCH_MP_TAC K_MAXIMAL_CONSISTENT);; +e (ASM_REWRITE_TAC[]);; +e (SUBGOAL_THEN `({M | MAXIMAL_CONSISTENT {} p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + K_STANDARD_REL p) IN GEN_STANDARD_FRAME {} p` + MP_TAC);; +e (ASM_MESON_TAC[KF_IN_STANDARD_K_FRAME; K_STANDARD_FRAME_DEF]);; +e (ASM_MESON_TAC[GEN_COUNTERMODEL_ALT]);; +let K_COMPLETENESS_THM = top_thm ();; +``` + +#### Completeness of T in `t_completeness.ml` +``` +g `!p. RF:(form list->bool)#(form list->form list->bool)->bool |= p + ==> [T_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 T_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + T_STANDARD_REL p)`);; +e (REWRITE_TAC[NOT_IMP] THEN CONJ_TAC );; +e (MATCH_MP_TAC RF_MAXIMAL_CONSISTENT);; +e (ASM_REWRITE_TAC[]);; +e (SUBGOAL_THEN `({M | MAXIMAL_CONSISTENT T_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + T_STANDARD_REL p) IN GEN_STANDARD_FRAME T_AX p` + MP_TAC);; +e (ASM_MESON_TAC[RF_IN_T_STANDARD_FRAME; T_STANDARD_FRAME_DEF]);; +e (ASM_MESON_TAC[GEN_COUNTERMODEL_ALT]);; +let T_COMPLETENESS_THM = top_thm ();; +``` + +#### Completeness of K4 in `k4_completeness.ml` +``` +g `!p. TF:(form list->bool)#(form list->form list->bool)->bool |= p + ==> [K4_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 K4_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + K4_STANDARD_REL p)`);; +e (REWRITE_TAC[NOT_IMP] THEN CONJ_TAC );; +e (MATCH_MP_TAC TF_MAXIMAL_CONSISTENT);; +e (ASM_REWRITE_TAC[]);; +e (SUBGOAL_THEN `({M | MAXIMAL_CONSISTENT K4_AX p M /\ (!q. MEM q M ==> q SUBSENTENCE p)}, + K4_STANDARD_REL p) IN GEN_STANDARD_FRAME K4_AX p` + MP_TAC);; +e (ASM_MESON_TAC[K4F_IN_K4_STANDARD_FRAME; K4_STANDARD_FRAME_DEF]);; +e (ASM_MESON_TAC[GEN_COUNTERMODEL_ALT]);; +let K4_COMPLETENESS_THM = top_thm ();; +``` + +#### 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. -Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we quickly generalize for each normal system the completeness theorem for models with infinite worlds.
+Observe that our proof of completness ha an issue, it requires that `CORR S` is not just a set of correspondent frames but that it is a set of correspondent frames that has domain that is finite and that is a set formulas' lists. Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we quickly generalize for each normal system the completeness theorem for models with infinite worlds.
In `gen_completeness`. ``` GEN_LEMMA_FOR_GEN_COMPLETENESS @@ -588,6 +826,46 @@ k_COUNTERMODEL_FINITE_SETS |- !p. ~[{} . {} |~ p] ==> ~holds_in (K_STDWORLDS p, K_STDREL p) p ``` +### In T +Construction of the countermodels. +``` +let T_STDWORLDS_RULES,T_STDWORLDS_INDUCT,T_STDWORLDS_CASES = + new_inductive_set + `!M. MAXIMAL_CONSISTENT T_AX p M /\ + (!q. MEM q M ==> q SUBSENTENCE p) + ==> set_of_list M IN T_STDWORLDS p`;; + +let T_STDREL_RULES,T_STDREL_INDUCT,T_STDREL_CASES = new_inductive_definition + `!w1 w2. T_STANDARD_REL p w1 w2 + ==> T_STDREL p (set_of_list w1) (set_of_list w2)`;; +``` + +Theorem of existence of the finite countermodel. +``` +T_COUNTERMODEL_FINITE_SETS +|- `!p. ~ [T_AX . {} |~ p] ==> ~holds_in (T_STDWORLDS p, T_STDREL p) p` +``` + +### In K4 +Construction of the countermodels. +``` +let K4_STDWORLDS_RULES,K4_STDWORLDS_INDUCT,K4_STDWORLDS_CASES = + new_inductive_set + `!M. MAXIMAL_CONSISTENT K4_AX p M /\ + (!q. MEM q M ==> q SUBSENTENCE p) + ==> set_of_list M IN K4_STDWORLDS p`;; + +let K4_STDREL_RULES,K4_STDREL_INDUCT,K4_STDREL_CASES = new_inductive_definition + `!w1 w2. K4_STANDARD_REL p w1 w2 + ==> K4_STDREL p (set_of_list w1) (set_of_list w2)`;; +``` + +Theorem of existence of the finite countermodel. +``` +K4_COUNTERMODEL_FINITE_SETS +|- `!p. ~ [K4_AX . {} |~ p] ==> ~holds_in (K4_STDWORLDS p, K4_STDREL p) p` +``` + ### In GL Construction of the countermodels. ``` @@ -624,23 +902,12 @@ K_RULE `!a b. [{} . {} |~ Box a || Box b --> Box (a || b)]`;; ### In T -Our tactic `T_TAC` and its associated rule `T_RULE` can automatically prove theorems in the modal logic T. +Our tactic `T_TAC` and its associated rule `T_RULE` still are the naive ones, but what we did in `k_completeness.ml` and in `gl_completeness.ml` demonstrate that in future works we will automatically prove theorems in the modal logic T. -Examples: -``` -T_RULE `!a. [ T_AX . {} |~ a --> Diamond a ]`;; -T_RULE `!a. [ T_AX . {} |~ Box a --> Diamond a ]`;; -``` ### In K4 -Our tactic `K4_TAC` and its associated rule `K4_RULE` can automatically prove theorems in the modal logic K4. - -### Example of a formula valid in K4 but not in K -``` -time GL_RULE - `!a. [GL_AX . {} |~ Box Diam Box Diam a <-> Box Diam a]`;; -``` +Our tactic `K4_TAC` and its associated rule `K4_RULE` still are the naive ones, but what we did in `k_completeness.ml` and in `gl_completeness.ml` demonstrate that in future works we will automatically prove theorems in the modal logic K4. ### In GL From f138c64fa54ccc29705833766da0e40dbc61cd1b Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Fri, 31 Jan 2025 09:51:18 +0100 Subject: [PATCH 13/16] Eliminazione errori, imprecisioni e refusi --- README.md | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 8d65dc3..aea5c6f 100644 --- a/README.md +++ b/README.md @@ -5,12 +5,12 @@ See the [website](https://holms-lib.github.io/) for a brief overview of our [HOLMS library](https://github.com/HOLMS-lib/HOLMS) for the [HOL Light](https://hol-light.github.io/) theorem prover. -This repository presents a second version of HOLMS (HOL-Light Library for Modal Systems), a modular framework designed for implementing modal reasoning within the HOL Light proof assistant. +This repository presents a second version of HOLMS (HOL-Light Library for Modal Systems), a modular framework designed to implement modal reasoning within the HOL Light proof assistant. -Extending our [previous work on Gödel-Löb logic (GL)](https://doi.org/10.1007/s10817-023-09677-z), we generalize our approach to formalize modal adequacy proofs for axiomatic calculi, thereby enabling the coverage of a broader range of normal modal systems. If the first version of HOLMS, [presented at Overlay 2024](https://ceur-ws.org/Vol-3904/paper5.pdf), partially parametrized the completeness proof for GL and added the minimal system K, this second version of HOLMS fully generalizes our approach and, as a demonstration of the flexibility of our methodology, four modal system and their adequacy proofs are now implemented in HOLMS: +Extending our [previous work on Gödel-Löb logic (GL)](https://doi.org/10.1007/s10817-023-09677-z), we generalise our approach to formalise modal adequacy proofs for axiomatic calculi, thereby enabling the coverage of a broader range of normal modal systems. If the first version of HOLMS, [presented at Overlay 2024](https://ceur-ws.org/Vol-3904/paper5.pdf), partially parametrised the completeness proof for GL and added the minimal system K, this second version of HOLMS fully generalises our method and, as a demonstration of the flexibility of our methodology, four modal system and their adequacy proofs are now implemented in HOLMS: - **K**: the minimal system is developed in `k_completeness.ml`; - **K4**: a system properly extended by GL is developed in `k4_completeness.ml`; -- **GL**: provability logic is developed and fully parametrized in `gl_completeness.ml`; +- **GL**: provability logic is developed and fully parametrised in `gl_completeness.ml`; - **T**: a system that is not extended by GL or K4, nor is an extension of GL or K4 is developed in `t_completeness.ml`. HOLMS lays the foundation for a comprehensive tool for modal reasoning in HOL, offering a high level of confidence and full automation by providing the essential mathematical components of principled decision algorithms for modal systems. The automated theorem prover and countermodel constructor for K and GL, already integrated into our library in `k_decid.ml` and `gl_decid.ml`, serve as evidence of the feasibility of this approach merging general purpose proof assistants, enriched sequent calculi, and formalised mathematics. @@ -19,29 +19,29 @@ The top-level file is `make.ml`. ## Main Theorems -For each normal system S, implemented in HOLMS in its file `S_completeness.ml`, we prove the following main theorems: -1. **The Correspondence theorem for S**
proves that a certain set of finite frames C, distinguished by a certain accessibility relation, correspond to S (for each frame in the set if p follows from S, then p is valid in such a frame).
+For each normal system $S$, implemented in HOLMS in its file `S_completeness.ml`, we prove the following main theorems: +- 1. **The Correspondence theorem for S**
proves that a certain set of finite frames $C$, distinguished by a certain accessibility relation, **correspond** to $S$ (for each frame in the set if $p$ follows from $S$, then $p$ is valid in such a frame).
$C= CORR S$ and equivalently $\forall F \in C (S \vdash p \implies F \vDash p) \land \forall F((S \vdash p \implies F \vDash p) \implies F \in C)$ -(`APPRS_CORR_S`) -2. **Soundness of S with respect to CORR S**
-proves that if something is a theorem of S then it is valid in its correspondent frame.
+(`CORRS_CORR_S`) +- 2. **Soundness of S with respect to CORR S**
+proves that if something is a theorem of $S$ then it is valid in its set of correspondent frames.
$\forall p (S \vdash p \implies CORR S \vDash p)$ -(`S_APPRS_VALID`) -3. **Consistency of S**
-proves that S cannot prove the false.
+(`S_CORRS_VALID`) +- 3. **Consistency of S**
+proves that $S$ cannot prove the false.
$S \not \vdash \bot$ (`S_CONSISTENT`) -5. **Completeness of S related to CORR S**
-proves that if someting holds in the set correspondent to S, then it is a theorem of S.
+- 4. **Completeness of S related to CORR S**
+proves that if someting holds in the set correspondent to $S$, then it is a theorem of $S$.
$\forall p (CORR S \vDash p \implies S \vdash p)$ (`S_COMPLETENESS_THM`) -For example, in `t_completeness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`; (5) `T_RULE`. +For example, in `t_completeness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`. -Moreover, for each of this systems, HOLMS presents a **simple decision procedure** to prove whether something is a theorem of S or not (`S_RULE`) and a fully automated theorem prover and countermodel constructor for K (`k_completeness.ml`) and GL (`gl_completeness.ml`). +Moreover, for each of this systems, HOLMS presents a **simple decision procedure** to prove whether something is a theorem of $S$ or not (`S_RULE`) and a fully automated theorem prover and countermodel constructor for $K$ (`k_completeness.ml`) and $GL$ (`gl_completeness.ml`). -To generalize and parametrize the proofs of completeness for normal systems as much as possible, we develop four main theorems in `gen_completeness.ml`: +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 ` @@ -396,7 +396,7 @@ K4_STANDARD_MODEL_CAR ### STEP 2: Definition of a standard accessibility relation for each S -The definition of a standard acessibility relation cannot be fully parametrized, at least following the approach presented in classical textbook. +The definition of a standard acessibility relation cannot be fully parametrised, at least following the approach presented in classical textbook. Consequently, to avoid code repetions in `gen_completeness.ml` we will define a `GEN_STANDARD_REL` that is parametric to $S$ and $p$, but then we will complete the definition of the standard relation for each normal system in the spefic file of each system `S_completeness.ml` in a way that guarantees that conditions R1 and R2 holds. @@ -693,7 +693,7 @@ e (ASM_MESON_TAC[MAXIMAL_CONSISTENT; CONSISTENT_NC]);; let GEN_COUNTERMODEL_ALT = top_thm();; ``` -Given the fully parametrized `GEN_COUNTERMODEL_ALT` and `SF_IN_STANDARD_S_FRAME`, the completeness theorems for each $S$ follow and their proofs are so short that we can present them here. +Given the fully parametrised `GEN_COUNTERMODEL_ALT` and `SF_IN_STANDARD_S_FRAME`, the completeness theorems for each $S$ follow and their proofs are so short that we can present them here. #### Completeness of K in `k_completeness.ml`. ``` @@ -777,7 +777,7 @@ let GL_COMPLETENESS_THM = top_thm ();; ``` ### Modal completeness for models on a generic (infinite) domain. -Observe that our proof of completness ha an issue, it requires that `CORR S` is not just a set of correspondent frames but that it is a set of correspondent frames that has domain that is finite and that is a set formulas' lists. Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we quickly generalize for each normal system the completeness theorem for models with infinite worlds.
+Observe that our proof of completness ha an issue, it requires that `CORR S` is not just a set of correspondent frames but that it is a set of correspondent frames that has domain that is finite and that is a set formulas' lists. Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we quickly generalise for each normal system the completeness theorem for models with infinite worlds.
In `gen_completeness`. ``` GEN_LEMMA_FOR_GEN_COMPLETENESS From c4ca592b96b24f4f99354deedcb5641ce394369a Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Fri, 31 Jan 2025 11:01:17 +0100 Subject: [PATCH 14/16] Update README.md --- README.md | 100 +++++++++++++++++++++++++++++++----------------------- 1 file changed, 58 insertions(+), 42 deletions(-) diff --git a/README.md b/README.md index aea5c6f..84b1e4c 100644 --- a/README.md +++ b/README.md @@ -38,7 +38,7 @@ $\forall p (CORR S \vDash p \implies S \vdash p)$ For example, in `t_completeness.ml` we prove: (1) `RF_CORR_T`; (2) `T_RF_VALID`; (3) `T_CONSISTENT`; (4) `T_COMPLETENESS_THM`. -Moreover, for each of this systems, HOLMS presents a **simple decision procedure** to prove whether something is a theorem of $S$ or not (`S_RULE`) and a fully automated theorem prover and countermodel constructor for $K$ (`k_completeness.ml`) and $GL$ (`gl_completeness.ml`). +Moreover, for each of this systems, HOLMS presents a **simple decision procedure** to prove whether something is a theorem of $S$ or not (`S_RULE`) and a **fully automated theorem prover and countermodel constructor** for $K$ (`k_completeness.ml`) and $GL$ (`gl_completeness.ml`). To generalise and parametrise the proofs of completeness for normal systems as much as possible, we develop four main theorems in `gen_completeness.ml`: @@ -50,7 +50,23 @@ To generalise and parametrise the proofs of completeness for normal systems as m # Usage guide and source code -## Calcus Definition +## Axiomatic Calcus +We inductively define the **axioms** of our modal calculus (`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 **rules of inference** of our calculus (`MODPROVES`). ``` let MODPROVES_RULES,MODPROVES_INDUCT,MODPROVES_CASES = new_inductive_definition @@ -67,8 +83,7 @@ MODPROVES_DEDUCTION_LEMMA |- !S H p q. [S . H |~ p --> q] <=> [S . p INSERT H |~ q] ``` -## Relational semantics -Kripke's Semantics of formulae. +## Kripke's Semantics of formulae We define, by induction on the complexity of a formula, that a certain formula $A$ **holds in a certain world $w$ of a certain model $\langle W, R, V\rangle$**.
$\langle W, R, V\rangle, w \vDash A$ @@ -90,8 +105,8 @@ let holds = (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 in every world for every model of that frame.
-$\langle W, R\rangle \vDash p \iff \forall w \in W (\forall V (\langle W, R, V\rangle, w \vDash p$)) +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 (\langle W, R, V\rangle, w \vDash p$)) ``` let holds_in = new_definition `holds_in (W,R) p <=> !V w:W. w IN W ==> holds (W,R) V p w`;; @@ -117,16 +132,16 @@ let CORR_DEF = new_definition (((W,R) IN FINITE_FRAME ) /\ (!p. [S. {} |~ p] ==> holds_in (W:W->bool,R:W->W->bool) (p)))}`;; ``` -For each one of the normal system S developed in HOLMS we prove what set of frames is correspondent to S ($C= CORR S$), then we prove that every frame that is in C is correspondent to S ($\subseteq$: $\forall F \in C(S \vdash p \implies F \vDash p)$ ) and that every frame that is correspondent to S is in C ($\supseteq$: $\forall F((S \vdash p \implies F \vDash p) \implies F \in C)$ ). +For each one of the normal system S developed in HOLMS we prove what set of frames is correspondent to S ($C= CORR S$), i.e. we prove that every frame that is in C is correspondent to S ($\subseteq$: $\forall F \in C(S \vdash p \implies F \vDash p)$ ) and that every frame that is correspondent to S is in C ($\supseteq$: $\forall F((S \vdash p \implies F \vDash p) \implies F \in C)$ ). ### K-Finite Frames -We prove that the set of finite frames is the one correspondent to K. +We prove that the set of **finite frames** is the one correspondent to **$K$**. ``` FINITE_FRAME_CORR_K |-`FINITE_FRAME:(W->bool)#(W->W->bool)->bool = CORR {}`;; ``` ### T-Finite Reflexive Frames (RF) -We prove that the set of finite reflexive frames is the one correspondent to T. +We prove that the set of **finite reflexive frames** is the one correspondent to **$T$**. ``` let RF_DEF = new_definition `RF = @@ -140,7 +155,7 @@ RF_CORR_T |-`FINITE_FRAME:(W->bool)#(W->W->bool)->bool = CORR {}`;; ``` ### K4-Finite Transitive Frames (TF) -We prove that the set of finite transitive frames is the one correspondent to K4. +We prove that the set of **finite transitive frames** is the one correspondent to **$K4$**. ``` let TF_DEF = new_definition `TF = @@ -154,7 +169,7 @@ TF_CORR_K4 |-`TF: (W->bool)#(W->W->bool)->bool = CORR K4_AX`;; ``` ### GL-Finite Irreflexive and Transitive Frames (ITF) -We prove that the set of finite transitive and irreflexive frames is the one correspondent to GL. +We prove that the set of **finite transitive and irreflexive frames** is the one correspondent to **$GL$**. ``` let ITF_DEF = new_definition `ITF = @@ -170,14 +185,14 @@ ITF_CORR_GL ``` ## Soundness and Consistency -We demonstrate the **soundness** of each S with respect to CORR S. +We parametrically demonstrate the **soundness** of each $S$ with respect to $CORR S$. ``` GEN_CORR_VALID |- `!S p. [S. {} |~ p] ==> CORR S:(W->bool)#(W->W->bool)->bool |= p`;; ``` -Then, by specializing the proof of `GEN_CORR_VALID`, we prove the soundness of each normal system S developed in HOLMS with respect to its correspondent frame. -Moreover we prove its **consistency**, by modus ponens on the converse of `S_FRAME_VALID`. +Then, by specializing the proof of `GEN_CORR_VALID`, we prove the soundness of each normal system $S$ developed in HOLMS with respect to its correspondent frame. +Moreover we prove its **consistency**, by modus ponens on the converse of `S_CORRS_VALID`. ### Soundness and consistency of K ``` @@ -239,8 +254,8 @@ let GL_consistent = prove 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 presnt a three-steps proof. +## Completeness Theorems +We first sketch the idea behind the demonstration and, then, we will present a three-step proof. ### The Idea behind the Proof @@ -251,24 +266,24 @@ S_COMPLETNESS_THM |. `!p. ( CORR S |= p ==> [S. {} |~ p])` ``` - **1. Rewriting `S_COMPLETNESS`'s statment**
-By using some tautologies and rewriting, we can show that the completeness theorem is equivalent to a more handy sentence:
+By using some tautologies and rewritings, we can show that the completeness theorem is equivalent to a more handy sentence:
$\forall p (S \not \vdash p \implies \exists \langle W,R\rangle_{S,p} \in CORR_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 rewrite the sentence by _contraposition_.
+ - A. We rewrote the sentence by _contraposition_.
`e GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM];;`

- - B. We rewrite validity in a set of frames (`valid`) as validity in a certain world of a certain model (`holds`) and we exploit some _propositional tautologies_.
+ - 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]);;`
``` S_COMPLETNESS_THM' |- `!p. ( `~[S . {} |~ p] ==> - (exists W R. W,R IN CORR S /\ - (exists V m. m IN p1 /\ - ~holds (p1,p2) V p w)))` + (? W R. W,R IN CORR S /\ + (? V m. m IN W /\ + ~holds (W,R) V p w)))` ``` -At this point, for each modal formula $p$ we need to construct a **_countermodel_** $𝓜_{S,p}$ and a "**_counterworld_**" $m_{S,p}$ in the domain of the countermodel.

-We can observe that, by working with HOL, it is possible to 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 develop te proof while avoiding code duplication as much as possible.
+To prove this rewritten statment, 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 completness proof while **avoiding code duplication as much as possible**.

-- **2. Reducing a model theoretic-notion to a set/list-theoretic concept** -The canonical proof of completeness, illustrated in classical textbooks like George Boolos's "The Logic of Provability", exploit 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) $.

+- **2. Reducing a model theoretic-notion to a set/list-theoretic concept**
+The canonical proof of completeness, illustrated in classical textbooks like [George Boolos's "The Logic of Provability"](https://www.cambridge.org/core/books/logic-of-provability/F1549530F91505462083CE2FEB6444AA), 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 set (list in HOLMS) of modal formulas. If we are able to construct a countermodel with this constraints, we will easily construct a counterworld $m_{S,p}$ that is a set of formulas not including p.

@@ -276,11 +291,11 @@ Then our subgoal would be to prove:
``` S_COMPLETNESS_THM'' |- `!p. ( `~[S . {} |~ p] ==> - (exists W R. W,R IN CORR S /\ - (exists M. M IN p1 /\ + (? W R. W,R IN CORR S /\ + (? M. M IN W /\ ~ MEM p M)))` ``` -This subgoal is much more manageable than the previous statement, indeed it reduces the **model-theoretic** notion of _validity_ (`holds (W,R) V p w`) to the **set-theoretic** concept (**list-theoretic** in HOLMS) of _membership_ (`MEM p w`). +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 **set-theoretic** concept (**list-theoretic** in HOLMS) of _membership_ (`MEM p w`). - **3. What do we need to prove?**
@@ -291,15 +306,16 @@ Given our aim of proving $\forall p(S \not \vdash p \implies \exists \langle W,R Namely, for our model $𝓜_{S,p}$ holds $\forall w \in W_{S,p} (w \in p \iff 𝓜_{S,p},w \vDash p) $.

- C. The counterworld $m_{S,p}$ must not contain p.
$p \not \in m_{S,p}$

- - D. Consequently $W_{S,p}$ must be a **set of formula's lists**
+ - D. $W_{S,p}$ must be a **set of formulas' lists**
`CORRS:(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 'STANDARD_MODEL` in step 1 is fully parametric. +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$. -Before this construction of the countermodel, we defined in `consistent.ml` some properties that hold for formulas' lists. +### 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 usefull to define the domain of the countermodel. #### Consistent $S$ A list of formulas $X$ is consistent to a set of axioms $S$ iff and only if $S \not \vdash \neg \bigwedge X$ @@ -309,7 +325,7 @@ let CONSISTENT = new_definition ``` #### Maximal Consistent $S,p$
-A list of formulas $X$ is maximal-consistent to a set of axioms $S$ and modal formula $p$ iff X has no repetitions, X is consistent $_S$ and $\forall q (q \ subformula \ p \implies q \in X \lor \neg q \in l)$. +A list of formulas $X$ is maximal-consistent to a set of axioms $S$ and modal formula $p$ iff $X \ has \ no \ repetitions$, $X \ is \ consistent_S$ and $\forall q (q \ subformula \ p \implies q \in X \lor \neg q \in l)$. ``` let MAXIMAL_CONSISTENT = new_definition `MAXIMAL_CONSISTENT S p X <=> @@ -328,13 +344,13 @@ EXTEND_MAXIMAL_CONSISTENT X SUBLIST M` ``` -Then we define a **standard model** such that: +### Definition of the parametric Countermodel +We define a **standard model** such that: -- **A: The Domain $W_{S,p}$ is $ { $X | Maximal-Consistent_{S,p} \ X $ }**

- As requested the domain is a set of list 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 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. +- **A: The Domain $W_{S,p}$ is { $X | Maximal-Consistent_{S,p} \ X$ }**

+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] @@ -349,11 +365,11 @@ NONEMPTY_MAXIMAL_CONSISTENT - R2: $\langle W,R \rangle_{S,p} \in CORR S$.
This second condition guarantees one of the four initial constraints. -- **C: The Evaluation Relation $R_{S,p}$** is defined as follows
+- **C: The Evaluation Relation $V_{S,p}$** is defined as follows
$\forall m \in W_{S,p} \ \forall a \in Atom-Form_{\Box} (mVa \iff a \ subformula \ p \land a \in m)$ -In particular, in HOLMS `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. +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 @@ -369,7 +385,7 @@ let GEN_STANDARD_MODEL_DEF = new_definition (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 a simple specification of `GEN_STANDARD_FRAME` and `GEN_STANDARD_MODEL` with the parameters `{}`, `T_AX`, `K4_AX` and `GL_AX`, we present here just the definitions for $K4$. +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`) ``` From 5ab14ac01530107863c9f5bb3c082989512b98b9 Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Fri, 31 Jan 2025 17:26:41 +0100 Subject: [PATCH 15/16] Final Update README.md --- README.md | 65 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 33 insertions(+), 32 deletions(-) diff --git a/README.md b/README.md index 84b1e4c..96efcf5 100644 --- a/README.md +++ b/README.md @@ -412,19 +412,21 @@ K4_STANDARD_MODEL_CAR ### 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. +The definition of a _standard acessibility relation_ cannot be fully parametrised, at least following the approach presented in classical textbook. -Consequently, to avoid code repetions in `gen_completeness.ml` we will define a `GEN_STANDARD_REL` that is parametric to $S$ and $p$, but then we will complete the definition of the standard relation for each normal system in the spefic file of each system `S_completeness.ml` in a way that guarantees that conditions R1 and R2 holds. +Consequently, to avoid code repetions, we will: -After we have defined the `S_STANDARD_REL` we will show: -- The most difficult verse of R1's implication in `S_ACCESSIBILITY_LEMMA`
+- 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 that conditions R1 and R2 holds. + In particular we will show: + - The most difficult verse of R1's implication in `S_ACCESSIBILITY_LEMMA`
$\forall q \in Form_{\Box} (\Box q \ subformula \ 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`.
+ - R2 holds for $\langle W_{S,p},$ _S_STANDARD_REL_ $\rangle$ in ` S_MAXIMAL_CONSISTENT`.
$\langle W_{S,p},$ _S_STANDARD_REL_ $\rangle \in CORRS$ -Then `SF_IN_STANDARD_S_FRAME` follows as corollary and, given the hypotesis that $S \not \vdash p$, $\langle W_{S,p},$ S_STANDARD_REL $, V_{S,p} \rangle$ is an `S_STANDARD_MODEL`. +Then `CORRS_IN_STANDARD_S_FRAME` follows as corollary and, given the hypotesis $S \not \vdash p$, $\langle W_{S,p},$ S_STANDARD_REL $, V_{S,p} \rangle$ is an `S_STANDARD_MODEL`. -#### Parametric definition of the standard relation in `gen_completeness`. +#### A: Parametric definition of the standard relation in `gen_completeness`. ``` let GEN_STANDARD_REL = new_definition `GEN_STANDARD_REL S p w x <=> @@ -433,7 +435,7 @@ let GEN_STANDARD_REL = new_definition (!B. MEM (Box B) w ==> MEM B x)`;; ``` -#### Definition of the standard relation for K in `k_completeness.ml`. +#### B: 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`;; @@ -445,7 +447,7 @@ K_STANDARD_REL_CAR (!B. MEM (Box B) w ==> MEM B x)` ``` -**Accessibility Lemma for K** that ensures the most difficult verse of R1's implication. +**Accessibility lemma for K** that ensures the most difficult verse of R1's implication. ``` K_ACCESSIBILITY_LEMMA |- `!p w q. ~ [{} . {} |~ p] /\ @@ -455,7 +457,7 @@ K_ACCESSIBILITY_LEMMA (!x. K_STANDARD_REL p w x ==> MEM q x) ==> MEM (Box q) w` ``` -**Maximal Consistent Lemma for K** that ensures R2. +**Maximal consistent lemma for K** ensures R2. ``` K_MAXIMAL_CONSISTENT |- (`!p. ~ [{} . {} |~ p] @@ -485,7 +487,7 @@ let KF_IN_STANDARD_K_FRAME = top_thm();; ``` -#### Definition of the standard relation for T in `t_completeness.ml`. +#### B: Definition of the standard relation for T in `t_completeness.ml`. ``` let T_STANDARD_REL_DEF = new_definition `T_STANDARD_REL p w x <=> @@ -499,7 +501,7 @@ T_STANDARD_REL_CAR (!B. MEM (Box B) w ==> MEM B x)` ``` -**Accessibility Lemma for T** that ensures the most difficult verse of R1's implication. +**Accessibility lemma for T** that ensures the most difficult verse of R1's implication. ``` T_ACCESSIBILITY_LEMMA |- `!p w q. @@ -510,7 +512,7 @@ T_ACCESSIBILITY_LEMMA (!x. T_STANDARD_REL p w x ==> MEM q x) ==> MEM (Box q) w` ``` -**Maximal Consistent Lemma for T** that ensures R2. +**Maximal consistent lemma for T** that ensures R2. ``` RF_MAXIMAL_CONSISTENT |- `!p. ~ [T_AX . {} |~ p] @@ -535,7 +537,7 @@ e EQ_TAC;; e (ASM_MESON_TAC[T_ACCESSIBILITY_LEMMA]);; let RF_IN_T_STANDARD_FRAME = top_thm();; ``` -#### Definition of the standard relation for K4 in `k4_completeness.ml`. +#### B: Definition of the standard relation for K4 in `k4_completeness.ml`. ``` let K4_STANDARD_REL_DEF = new_definition `K4_STANDARD_REL p w x <=> @@ -550,7 +552,7 @@ K4_STANDARD_REL_CAR (!B. MEM (Box B) w ==> MEM (Box B) x /\ MEM B x)` ``` -**Accessibility Lemma for K4** that ensures the most difficult verse of R1's implication. +**Accessibility lemma for K4** that ensures the most difficult verse of R1's implication. ``` K4_ACCESSIBILITY_LEMMA |- `!p w q. @@ -561,7 +563,7 @@ K4_ACCESSIBILITY_LEMMA (!x. K4_STANDARD_REL p w x ==> MEM q x) ==> MEM (Box q) w` ``` -**Maximal Consistent Lemma for K4** that ensures R2. +**Maximal consistent lemma for K4** that ensures R2. ``` TF_MAXIMAL_CONSISTENT |- `!p. ~ [T_AX . {} |~ p] @@ -587,7 +589,7 @@ e EQ_TAC;; let K4F_IN_K4_STANDARD_FRAME = top_thm();; ``` -#### Definition of the standard relation for GL in `gl_completeness.ml`. +#### B: Definition of the standard relation for GL in `gl_completeness.ml`. ``` let GL_STANDARD_REL_DEF = new_definition `GL_STANDARD_REL p w x <=> @@ -643,10 +645,10 @@ 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 $S \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 forcing `holds (W,R) V q w` to that of a set-theoretic (list-theoretic) membership `MEM q w`. +In this step we prove that, given a standard model and $S \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 completness does not need to specify this lemma for our normal system in analysis. +Observe that we prove this foundamental lemma in a fully parametric way and, moreover, the proof of completness does not need to specify this lemma for the normal system in analysis. #### Parametric truth lemma in `gen_completeness.ml` (parameters P, S) ``` @@ -660,14 +662,11 @@ GEN_TRUTH_LEMMA ### The Theorems -At this point we built up a _countermodel_ $\langle W,R,V \rangle_{S,p}$ that is a _standard model for S_ and we want to prove that a counterworld in this model exists:
- $\exist M_{S,p} \in W_{S,p} (p \not \in M_{S,p} )$ +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 $Maximal-Consistent_{S,p} \ m$; + - B: $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 $Maximal_Consistent_{S,p} M$; - - B: $p \not \in M_{S,p}$ - -But thanks to our theorem `NONEMPTY_MAXIMAL_CONSISTENT` $\forall p (S \vdash p \implies (\exists M (Maximal_Consistent_{S,p} M \land \neg p \in M))$,
we know that such an $M_{S,p}$ exists and we can prove `GEN_COUNTERMODEL_ALT`. Observe, indeed, that $Maximal_Consistent_{S,p} M \land \neg p \in M \implies p \not \in M_{S,p}$. +Thanks to our theorem `NONEMPTY_MAXIMAL_CONSISTENT` $\forall p (S \vdash p \implies (\exists m (Maximal-Consistent_{S,p} \ m \ \land \ \neg p \in M))$, we know that such an $m_{S,p}$ exists and we can prove `GEN_COUNTERMODEL_ALT`. Observe, indeed, that $Maximal-Consistent_{S,p} \ m \ \land \ \neg p \in m_{S,p} \implies p \not \in m_{S,p}$. ``` NONEMPTY_MAXIMAL_CONSISTENT |- `!S p. ~ [S . {} |~ p] @@ -709,7 +708,7 @@ e (ASM_MESON_TAC[MAXIMAL_CONSISTENT; CONSISTENT_NC]);; let GEN_COUNTERMODEL_ALT = top_thm();; ``` -Given the fully parametrised `GEN_COUNTERMODEL_ALT` and `SF_IN_STANDARD_S_FRAME`, the completeness theorems for each $S$ follow and their proofs are so short that we can present them here. +Given the fully parametrised `GEN_COUNTERMODEL_ALT` and `SF_IN_STANDARD_S_FRAME`, the completeness theorems for every $S$ follow and their proofs are so brief that we can present them here. #### Completeness of K in `k_completeness.ml`. ``` @@ -793,7 +792,9 @@ let GL_COMPLETENESS_THM = top_thm ();; ``` ### Modal completeness for models on a generic (infinite) domain. -Observe that our proof of completness ha an issue, it requires that `CORR S` is not just a set of correspondent frames but that it is a set of correspondent frames that has domain that is finite and that is a set formulas' lists. Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we quickly generalise for each normal system the completeness theorem for models with infinite worlds.
+Observe that our proof of completness has an issue: it requires that `CORR S` is not just a set of correspondent frames but a set of correspondent frames with has a **finite** domain that is **a set formulas' lists**. Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we can quickly generalise each completeness theorem for models with infinite worlds. + + In `gen_completeness`. ``` GEN_LEMMA_FOR_GEN_COMPLETENESS @@ -801,7 +802,7 @@ GEN_LEMMA_FOR_GEN_COMPLETENESS ==> !p. CORR S:(A->bool)#(A->A->bool)->bool |= p ==> CORR S:(form list->bool)#(form list->form list->bool)->bool |= p`;; ``` -As corollaries of `GEN_LEMMA_FOR_GEN_COMPLETENESS` in the specific files. +As corollaries of `GEN_LEMMA_FOR_GEN_COMPLETENESS`, in the specific files. ``` K_COMPLETENESS_THM_GEN |- `!p. INFINITE (:A) /\ FINITE_FRAME:(A->bool)#(A->A->bool)->bool |= p @@ -918,12 +919,12 @@ K_RULE `!a b. [{} . {} |~ Box a || Box b --> Box (a || b)]`;; ### In T -Our tactic `T_TAC` and its associated rule `T_RULE` still are the naive ones, but what we did in `k_completeness.ml` and in `gl_completeness.ml` demonstrate that in future works we will automatically prove theorems in the modal logic T. +Our tactic `T_TAC` and its associated rule `T_RULE` still are the naive ones, but what we did in `k_completeness.ml` and in `gl_completeness.ml` demonstrates that in future works we will be able to automatically prove theorems in the modal logic T. ### In K4 -Our tactic `K4_TAC` and its associated rule `K4_RULE` still are the naive ones, but what we did in `k_completeness.ml` and in `gl_completeness.ml` demonstrate that in future works we will automatically prove theorems in the modal logic K4. +Our tactic `K4_TAC` and its associated rule `K4_RULE` still are the naive ones, but what we did in `k_completeness.ml` and in `gl_completeness.ml` demonstrates that in future works we will be able to automatically prove theorems in the modal logic K4. ### In GL From 20359b0732154f368fbe8675a562575440a2317e Mon Sep 17 00:00:00 2001 From: Antonella Bilotta Date: Sat, 1 Feb 2025 10:48:23 +0100 Subject: [PATCH 16/16] Grammatical Correptions --- README.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 96efcf5..60fdcb1 100644 --- a/README.md +++ b/README.md @@ -262,10 +262,10 @@ We first sketch the idea behind the demonstration and, then, we will present a t Given a modal system $S$, we want to prove that it is **complete with respect to the set of its correspondent frames**: $\forall p (CORRS \vDash p \implies S \vdash p)$ ``` -S_COMPLETNESS_THM +S_COMPLETENESS_THM |. `!p. ( CORR S |= p ==> [S. {} |~ p])` ``` -- **1. Rewriting `S_COMPLETNESS`'s statment**
+- **1. Rewriting `S_COMPLETENESS`'s statment**
By using some tautologies and rewritings, we can show that the completeness theorem is equivalent to a more handy sentence:
$\forall p (S \not \vdash p \implies \exists \langle W,R\rangle_{S,p} \in CORR_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_.
@@ -273,14 +273,14 @@ $\forall p (S \not \vdash p \implies \exists \langle W,R\rangle_{S,p} \in CORR_S - 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]);;`
``` -S_COMPLETNESS_THM' +S_COMPLETENESS_THM' |- `!p. ( `~[S . {} |~ p] ==> (? W R. W,R IN CORR S /\ (? V m. m IN W /\ ~holds (W,R) V p w)))` ``` To prove this rewritten statment, 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 completness proof while **avoiding code duplication as much as possible**.
+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 set/list-theoretic concept**
The canonical proof of completeness, illustrated in classical textbooks like [George Boolos's "The Logic of Provability"](https://www.cambridge.org/core/books/logic-of-provability/F1549530F91505462083CE2FEB6444AA), 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) $.

@@ -289,7 +289,7 @@ If we are able to construct a countermodel with this constraints, we will easily

Then our subgoal would be to prove:
``` -S_COMPLETNESS_THM'' +S_COMPLETENESS_THM'' |- `!p. ( `~[S . {} |~ p] ==> (? W R. W,R IN CORR S /\ (? M. M IN W /\ @@ -648,7 +648,7 @@ let GLF_IN_GL_STANDARD_FRAME = top_thm();; In this step we prove that, given a standard model and $S \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 completness does not need to specify this lemma for the normal system in analysis. +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) ``` @@ -792,7 +792,7 @@ let GL_COMPLETENESS_THM = top_thm ();; ``` ### Modal completeness for models on a generic (infinite) domain. -Observe that our proof of completness has an issue: it requires that `CORR S` is not just a set of correspondent frames but a set of correspondent frames with has a **finite** domain that is **a set formulas' lists**. Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we can quickly generalise each completeness theorem for models with infinite worlds. +Observe that our proof of completeness has an issue: it requires that `CORR S` is not just a set of correspondent frames but a set of correspondent frames with has a **finite** domain that is **a set formulas' lists**. Thanks to the parametric lemma `GEN_LEMMA_FOR_GEN_COMPLETENESS`, we can quickly generalise each completeness theorem for models with infinite worlds. In `gen_completeness`.