Commit225fc10

authored

Update index.md

1 parent76c8eb1 commit225fc10Copy full SHA for 225fc10

File tree

1 file changed

-371

lines changed

index.md

1 file changed

-371

lines changed

`‎index.md‎`

Lines changed: 2 additions & 371 deletions

Original file line number	Diff line number	Diff line change
`@@ -25,374 +25,5 @@ This website gives a brief overview of our [HOLMS library](https://github.com/HO`
`25`	`25`	`- Leonardo Quartini, University of Florence, Italy`
`26`	`26`
`27`	`27`
`28`		`-##Principal definitions and theorems`
`29`		`-`
`30`		`-###Axiomatic Definition`
`31`		-```
`32`		`-let MODPROVES_RULES,MODPROVES_INDUCT,MODPROVES_CASES =`
`33`		`- new_inductive_definition`
`34`		- `(!H p. KAXIOM p ==> [S . H \|~ p]) /\
`35`		`- (!H p. p IN S ==> [S . H \|~ p]) /\`
`36`		`- (!H p. p IN H ==> [S . H \|~ p]) /\`
`37`		`- (!H p q. [S . H \|~ p --> q] /\ [S . H \|~ p] ==> [S . H \|~ q]) /\`
`38`		- (!H p. [S . {} \|~ p] ==> [S . H \|~ Box p])`;;
`39`		-```
`40`		`-`
`41`		`-###Deduction Lemma`
`42`		-```
`43`		`-MODPROVES_DEDUCTION_LEMMA`
`44`		-\|- `!S H p q. [S . H \|~ p --> q] <=> [S . p INSERT H \|~ q]`
`45`		-```
`46`		`-`
`47`		`-###Relational semantics`
`48`		`-`
`49`		`-Kripke's Semantics of formulae.`
`50`		`-`
`51`		-```
`52`		`-let holds =`
`53`		`- let pth = prove`
`54`		- (`(!WP. P WP) <=> (!W:W->bool R:W->W->bool. P (W,R))`,
`55`		`- MATCH_ACCEPT_TAC FORALL_PAIR_THM) in`
`56`		`- (end_itlist CONJ o map (REWRITE_RULE[pth] o GEN_ALL) o CONJUNCTS o`
`57`		`- new_recursive_definition form_RECURSION)`
`58`		- `(holds WR V False (w:W) <=> F) /\
`59`		`- (holds WR V True w <=> T) /\`
`60`		`- (holds WR V (Atom s) w <=> V s w) /\`
`61`		`- (holds WR V (Not p) w <=> ~(holds WR V p w)) /\`
`62`		`- (holds WR V (p && q) w <=> holds WR V p w /\ holds WR V q w) /\`
`63`		`- (holds WR V (p \|\| q) w <=> holds WR V p w \/ holds WR V q w) /\`
`64`		`- (holds WR V (p --> q) w <=> holds WR V p w ==> holds WR V q w) /\`
`65`		`- (holds WR V (p <-> q) w <=> holds WR V p w <=> holds WR V q w) /\`
`66`		`- (holds WR V (Box p) w <=>`
`67`		- !w'. w' IN FST WR /\ SND WR w w' ==> holds WR V p w')`;;
`68`		`-`
`69`		`-let holds_in = new_definition`
`70`		- `holds_in (W,R) p <=> !V w:W. w IN W ==> holds (W,R) V p w`;;
`71`		`-`
`72`		`-let valid = new_definition`
`73`		- `L \|= p <=> !f:(W->bool)#(W->W->bool). f IN L ==> holds_in f p`;;
`74`		-```
`75`		`-`
`76`		`-###Soundness and consistency of K`
`77`		-```
`78`		`-K_CONSISTENT`
`79`		-\|- `~ [{} . {} \|~ False]`
`80`		-```
`81`		`-`
`82`		`-###Soundness and consistency of GL`
`83`		-```
`84`		`-GL_consistent`
`85`		-\|- `~ [GL_AX . {} \|~ False]`
`86`		-```
`87`		`-`
`88`		`-###Completeness theorem`
`89`		`-`
`90`		`-The proof is organized in three steps.`
`91`		`-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)`
`92`		-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`.
`93`		`-`
`94`		`-####STEP 1`
`95`		`-Identification of a model <W,R,V> 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.`
`96`		`-`
`97`		-Parametric Definitions in`gen_completness.ml` (parameters P, S)
`98`		-```
`99`		`-let FRAME_DEF = new_definition`
`100`		- `FRAME = {(W:W->bool,R:W->W->bool) \| ~(W = {}) /\
`101`		- (!x y:W. R x y ==> x IN W /\ y IN W)}`;;
`102`		`-`
`103`		`-let GEN_STANDARD_FRAME_DEF = new_definition`
`104`		- `GEN_STANDARD_FRAME P S p =
`105`		`- FRAME INTER P INTER`
`106`		`- {(W,R) \| W = {w \| MAXIMAL_CONSISTENT S p w /\`
`107`		`- (!q. MEM q w ==> q SUBSENTENCE p)} /\`
`108`		`- (!q w. Box q SUBFORMULA p /\ w IN W`
`109`		- ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))}`;;
`110`		`-`
`111`		`-let GEN_STANDARD_MODEL_DEF = new_definition`
`112`		- `GEN_STANDARD_MODEL P S p (W,R) V <=>
`113`		`- (W,R) IN GEN_STANDARD_FRAME P S p /\`
`114`		- (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`;;
`115`		-```
`116`		`-`
`117`		-Definitions in`k_completness.ml` (P=K_FRAME, S={})
`118`		-```
`119`		`-let K_FRAME_DEF = new_definition`
`120`		- `K_FRAME = {(W:W->bool,R) \| (W,R) IN FRAME /\ FINITE W}`;;
`121`		`-`
`122`		`-let K_STANDARD_FRAME_DEF = new_definition`
`123`		- `K_STANDARD_FRAME = GEN_STANDARD_FRAME K_FRAME {}`;;
`124`		`-`
`125`		`-IN_K_STANDARD_FRAME`
`126`		-\|- `(W,R) IN K_STANDARD_FRAME p <=>
`127`		`- W = {w \| MAXIMAL_CONSISTENT {} p w /\`
`128`		`- (!q. MEM q w ==> q SUBSENTENCE p)} /\`
`129`		`- (W,R) IN K_FRAME /\`
`130`		`- (!q w. Box q SUBFORMULA p /\ w IN W`
`131`		- ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))`
`132`		`-`
`133`		`-let K_STANDARD_MODEL_DEF = new_definition`
`134`		- `K_STANDARD_MODEL = GEN_STANDARD_MODEL K_FRAME {}`;;
`135`		`-`
`136`		`-K_STANDARD_MODEL_CAR`
`137`		-\|- `K_STANDARD_MODEL p (W,R) V <=>
`138`		`- (W,R) IN K_STANDARD_FRAME p /\`
`139`		- (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`
`140`		-```
`141`		`-`
`142`		-Definitions in`gl_completness.ml` (P=ITF, S=GL_AX)
`143`		-```
`144`		`-let ITF_DEF = new_definition`
`145`		- `ITF =
`146`		`- {(W:W->bool,R:W->W->bool) \|`
`147`		`- ~(W = {}) /\`
`148`		`- (!x y:W. R x y ==> x IN W /\ y IN W) /\`
`149`		`- FINITE W /\`
`150`		`- (!x. x IN W ==> ~R x x) /\`
`151`		- (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)}`;;
`152`		`-`
`153`		`-let GL_STANDARD_FRAME_DEF = new_definition`
`154`		- `GL_STANDARD_FRAME p = GEN_STANDARD_FRAME ITF GL_AX p`;;
`155`		`-`
`156`		`-IN_GL_STANDARD_FRAME`
`157`		-\|- `!p W R. (W,R) IN GL_STANDARD_FRAME p <=>
`158`		`- W = {w \| MAXIMAL_CONSISTENT GL_AX p w /\`
`159`		`- (!q. MEM q w ==> q SUBSENTENCE p)} /\`
`160`		`- (W,R) IN ITF /\`
`161`		`- (!q w. Box q SUBFORMULA p /\ w IN W`
`162`		- ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))`
`163`		`-`
`164`		`-let GL_STANDARD_MODEL_DEF = new_definition`
`165`		- `GL_STANDARD_MODEL = GEN_STANDARD_MODEL ITF GL_AX`;;
`166`		`-`
`167`		`-GL_STANDARD_MODEL_CAR`
`168`		-\|- `!W R p V.
`169`		`- GL_STANDARD_MODEL p (W,R) V <=>`
`170`		`- (W,R) IN GL_STANDARD_FRAME p /\`
`171`		- (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p)) `
`172`		-```
`173`		`-`
`174`		`-####STEP 2`
`175`		`-Definition of a “standard” accessibility relation depending on axiom set S between these worlds such that the frame is appropriate to S.`
`176`		`-`
`177`		-Parametric definition of the standard relation in`gen_completness.ml` (parameter S)
`178`		-```
`179`		`-let GEN_STANDARD_REL = new_definition`
`180`		- `GEN_STANDARD_REL S p w x <=>
`181`		`- MAXIMAL_CONSISTENT S p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\`
`182`		`- MAXIMAL_CONSISTENT S p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\`
`183`		- (!B. MEM (Box B) w ==> MEM B x)`;;
`184`		-```
`185`		`-`
`186`		-Definitions in`k_completness.ml` (S={}) and demonstration of the Accessibility Lemma for K.
`187`		-```
`188`		`-let K_STANDARD_REL_DEF = new_definition`
`189`		- `K_STANDARD_REL p = GEN_STANDARD_REL {} p`;;
`190`		`-`
`191`		`-K_STANDARD_REL_CAR`
`192`		-\|-`K_STANDARD_REL p w x <=>
`193`		`- MAXIMAL_CONSISTENT {} p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\`
`194`		`- MAXIMAL_CONSISTENT {} p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\`
`195`		- (!B. MEM (Box B) w ==> MEM B x)`
`196`		`-`
`197`		`-K_ACCESSIBILITY_LEMMA_1`
`198`		- \|- `!p w q.
`199`		`- ~ [{} . {} \|~ p] /\`
`200`		`- MAXIMAL_CONSISTENT {} p w /\`
`201`		`- (!q. MEM q w ==> q SUBSENTENCE p) /\`
`202`		`- Box q SUBFORMULA p /\`
`203`		`- (!x. K_STANDARD_REL p w x ==> MEM q x)`
`204`		- ==> MEM (Box q) w`
`205`		-```
`206`		`-`
`207`		-Definitions in`gl_completness.ml` (S=GL_AX) and demonstration of the Accessibility Lemma for GL.
`208`		-```
`209`		`-let GL_STANDARD_REL_DEF = new_definition`
`210`		- `GL_STANDARD_REL p w x <=>
`211`		`- GEN_STANDARD_REL GL_AX p w x /\`
`212`		`- (!B. MEM (Box B) w ==> MEM (Box B) x) /\`
`213`		- (?E. MEM (Box E) x /\ MEM (Not (Box E)) w)`;;
`214`		`-`
`215`		`-GL_ACCESSIBILITY_LEMMA`
`216`		-\|- `!p M w q.
`217`		`- ~ [GL_AX . {} \|~ p] /\`
`218`		`- MAXIMAL_CONSISTENT GL_AX p M /\`
`219`		`- (!q. MEM q M ==> q SUBSENTENCE p) /\`
`220`		`- MAXIMAL_CONSISTENT GL_AX p w /\`
`221`		`- (!q. MEM q w ==> q SUBSENTENCE p) /\`
`222`		`- MEM (Not p) M /\`
`223`		`- Box q SUBFORMULA p /\`
`224`		`- (!x. GL_STANDARD_REL p w x ==> MEM q x)`
`225`		- ==> MEM (Box q) w`
`226`		-```
`227`		`-`
`228`		`-####STEP 3`
`229`		-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
`230`		`-for every subformula q of p, through a specific atomic evaluation function on (W,R).`
`231`		`-`
`232`		-Parametric truth lemma in`gen_completness.ml` (parameters P, S)
`233`		-```
`234`		`-GEN_TRUTH_LEMMA`
`235`		-\|- `!P S W R p V q.
`236`		`- ~ [S . {} \|~ p] /\`
`237`		`- GEN_STANDARD_MODEL P S p (W,R) V /\`
`238`		`- q SUBFORMULA p`
`239`		- ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)`
`240`		-```
`241`		-Truth lemma specified for K in`k_completness.ml` (P=K_FRAME, S={})
`242`		-```
`243`		`-let K_TRUTH_LEMMA = prove`
`244`		-(`!W R p V q.
`245`		`- ~ [{} . {} \|~ p] /\`
`246`		`- K_STANDARD_MODEL p (W,R) V /\`
`247`		`- q SUBFORMULA p`
`248`		- ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)`,
`249`		`- REWRITE_TAC[K_STANDARD_MODEL_DEF] THEN MESON_TAC[GEN_TRUTH_LEMMA]);;`
`250`		`-`
`251`		-```
`252`		-Truth lemma specified for GL in`gl_completness.ml` (P=ITF, S=GL_AX)
`253`		-```
`254`		`-let GL_truth_lemma = prove`
`255`		- (`!W R p V q.
`256`		`- ~ [GL_AX . {} \|~ p] /\`
`257`		`- GL_STANDARD_MODEL p (W,R) V /\`
`258`		`- q SUBFORMULA p`
`259`		- ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)`,
`260`		`- REWRITE_TAC[GL_STANDARD_MODEL_DEF] THEN MESON_TAC[GEN_TRUTH_LEMMA]);;`
`261`		`-`
`262`		-```
`263`		`-`
`264`		`-####The Theorem`
`265`		`-`
`266`		-Completeness of K in`k_completness.ml`.
`267`		-This demonstration uses the`K_TRUTH_LEMMA` that specifies the`GEN_TRUTH_LEMMA`, therefore the first part of the demonstration of the completness theorem for K is completely parametrized.
`268`		-```
`269`		`-K_COMPLETENESS_THM`
`270`		-\|- `!p. K_FRAME:(form list->bool)#(form list->form list->bool)->bool \|= p
`271`		- ==> [{} . {} \|~ p]`
`272`		-```
`273`		`-`
`274`		-Completeness of GL in`gl_completness.ml`
`275`		-This demonstration uses the`GL_TRUTH_LEMMA` that specifies the`GEN_TRUTH_LEMMA`, therefore the first part of the demonstration of the completness theorem for GL is completely parametrized.
`276`		-```
`277`		`-GL_COMPLETENESS_THM`
`278`		-\|- `!p. ITF:(form list->bool)#(form list->form list->bool)->bool \|= p
`279`		- ==> [GL_AX . {} \|~ p]`
`280`		-```
`281`		`-`
`282`		`-`
`283`		`-###Finite model property and decidability`
`284`		`-`
`285`		`-####In K`
`286`		`-Construction of the countermodels.`
`287`		-```
`288`		`-let K_STDWORLDS_RULES,K_STDWORLDS_INDUCT,K_STDWORLDS_CASES =`
`289`		`- new_inductive_set`
`290`		- `!M. MAXIMAL_CONSISTENT {} p M /\
`291`		`- (!q. MEM q M ==> q SUBSENTENCE p)`
`292`		- ==> set_of_list M IN K_STDWORLDS p`;;
`293`		`-`
`294`		`-let K_STDREL_RULES,K_STDREL_INDUCT,K_STDREL_CASES = new_inductive_definition`
`295`		- `!w1 w2. K_STANDARD_REL p w1 w2
`296`		- ==> K_STDREL p (set_of_list w1) (set_of_list w2)`;;
`297`		-```
`298`		`-`
`299`		`-Theorem of existence of the finite countermodel.`
`300`		-```
`301`		`-k_COUNTERMODEL_FINITE_SETS`
`302`		-\|- `!p. ~[{} . {} \|~ p] ==> ~holds_in (K_STDWORLDS p, K_STDREL p) p`
`303`		-```
`304`		`-`
`305`		`-####In GL`
`306`		`-Construction of the countermodels.`
`307`		-```
`308`		`-let GL_STDWORLDS_RULES,GL_STDWORLDS_INDUCT,GL_STDWORLDS_CASES =`
`309`		`- new_inductive_set`
`310`		- `!M. MAXIMAL_CONSISTENT GL_AX p M /\
`311`		`- (!q. MEM q M ==> q SUBSENTENCE p)`
`312`		- ==> set_of_list M IN GL_STDWORLDS p`;;
`313`		`-`
`314`		`-let GL_STDREL_RULES,GL_STDREL_INDUCT,GL_STDREL_CASES = new_inductive_definition`
`315`		- `!w1 w2. GL_STANDARD_REL p w1 w2
`316`		- ==> GL_STDREL p (set_of_list w1) (set_of_list w2)`;;
`317`		-```
`318`		`-`
`319`		`-Theorem of existence of the finite countermodel.`
`320`		-```
`321`		`-GL_COUNTERMODEL_FINITE_SETS`
`322`		-\|- `!p. ~ [GL_AX . {} \|~ p] ==> ~holds_in (GL_STDWORLDS p, GL_STDREL p) p`
`323`		-```
`324`		`-`
`325`		`-###Automated theorem proving and countermodel construction`
`326`		`-`
`327`		`-####In K`
`328`		`-`
`329`		-Our tactic`K_TAC` and its associated rule`K_RULE` can automatically prove theorems in the modal logic K.
`330`		`-`
`331`		`-Examples:`
`332`		-```
`333`		-K_RULE `!a b. [{} . {} \|~ Box (a && b) <-> Box a && Box b]`;;
`334`		`-`
`335`		-K_RULE `!a b. [{} . {} \|~ Box a \|\| Box b --> Box (a \|\| b)]`;;
`336`		-```
`337`		`-`
`338`		`-####In GL`
`339`		`-`
`340`		-Our tactic`GL_TAC` and its associated rule`GL_RULE` can automatically prove theorems in the modal logic GL.
`341`		`-Here is a list of examples`
`342`		`-`
`343`		`-####Example of a formula valid in GL but not in K`
`344`		-```
`345`		`-time GL_RULE`
`346`		- `!a. [GL_AX . {} \|~ Box Diam Box Diam a <-> Box Diam a]`;;
`347`		-```
`348`		`-`
`349`		`-####Formalised Second Incompleteness Theorem`
`350`		`-In PA, the following is provable: If PA is consistent, it cannot prove its own consistency.`
`351`		-```
`352`		`-let GL_second_incompleteness_theorem = time GL_RULE`
`353`		- `[GL_AX . {} \|~ Not (Box False) --> Not (Box (Diam True))]`;;
`354`		-```
`355`		`-`
`356`		`-####PA ignores unprovability statements`
`357`		-```
`358`		`-let GL_PA_ignorance = time GL_RULE`
`359`		- `!p. [GL_AX . {} \|~ (Box False) <-> Box (Diam p)]`;;
`360`		-```
`361`		`-`
`362`		`-####PA undecidability of consistency`
`363`		`-If PA does not prove its inconsistency, then its consistency is undecidable.`
`364`		-```
`365`		`-let GL_PA_undecidability_of_consistency = time GL_RULE`
`366`		- `[GL_AX . {} \|~ Not (Box (Box False))
`367`		`- --> Not (Box (Not (Box False))) &&`
`368`		- Not (Box (Not (Not (Box False))))]`;;
`369`		-```
`370`		`-####Undecidability of Gödels formula`
`371`		-```
`372`		`-let GL_undecidability_of_Godels_formula = time GL_RULE`
`373`		- `!p. [GL_AX . {} \|~ Box (p <-> Not (Box p)) && Not (Box (Box False))
`374`		- --> Not (Box p) && Not (Box (Not p))]`;;
`375`		-```
`376`		`-`
`377`		`-####Reflection and iterated consistency`
`378`		`-If a reflection principle implies the second iterated consistency assertion, then the converse implication holds too.`
`379`		-```
`380`		`-let GL_reflection_and_iterated_consistency = time GL_RULE`
`381`		- `!p. [GL_AX . {} \|~ Box ((Box p --> p) --> Diam (Diam True))
`382`		- --> (Diam (Diam True) --> (Box p --> p))]`;;
`383`		-```
`384`		`-`
`385`		`-####A Godel sentence is equiconsistent with a consistency statement`
`386`		-```
`387`		`-let GL_Godel_sentence_equiconsistent_consistency = time GL_RULE`
`388`		- `!p. [GL_AX . {} \|~ Box (p <-> Not (Box p)) <->
`389`		- Box (p <-> Not (Box False))]`;;
`390`		-```
`391`		`-`
`392`		`-####Arithmetical fixpoint`
`393`		`-For any arithmetical sentences p q, p is equivalent to unprovability of q --> p iff p is equivalent to consistency of q.`
`394`		-```
`395`		`-let GL_arithmetical_fixpoint = time GL_RULE`
`396`		- `!p q. [GL_AX . {} \|~ Dotbox (p <-> Not (Box (q --> p))) <->
`397`		- Dotbox (p <-> Diam q)]`;;
`398`		-```
	`28`	`+##HOLMS USAGE GUIDE`
	`29`	`+The[README.md](https://github.com/maggesi/GL/blob/master/README.md) provides an usage guide for our HOLMS library at its current status.`

0 commit comments

Comments

(0)

Movatterモバイル変換

Navigation Menu

Search code, repositories, users, issues, pull requests...

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Commit225fc10

File tree

1 file changed

1 file changed

`‎index.md‎`

0 commit comments