Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

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

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Commitef783ae

Browse files
Update index.md
1 parent48c4c32 commitef783ae

File tree

1 file changed

+97
-61
lines changed

1 file changed

+97
-61
lines changed

‎index.md‎

Lines changed: 97 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ This website gives a brief overview of our [HOLMS library](https://github.com/HO
2424
-[Cosimo Perini Brogi](https://logicosimo-gitlab-io-logicosimo-ad8371f8e99a5e895c64ff5b4f9ba89.gitlab.io/), IMT School for Advanced Studies Lucca, Italy
2525
- Leonardo Quartini, University of Florence, Italy
2626

27+
2728
##Principal definitions and theorems
2829

2930
###Axiomatic Definition
@@ -50,7 +51,7 @@ Kripke's Semantics of formulae.
5051
```
5152
let holds =
5253
let pth = prove
53-
(`(!WP. P WP) <=> (!W R. P (W,R))`,
54+
(`(!WP. P WP) <=> (!W:W->bool R:W->W->bool. P (W,R))`,
5455
MATCH_ACCEPT_TAC FORALL_PAIR_THM) in
5556
(end_itlist CONJ o map (REWRITE_RULE[pth] o GEN_ALL) o CONJUNCTS o
5657
new_recursive_definition form_RECURSION)
@@ -66,84 +67,112 @@ let holds =
6667
!w'. w' IN FST WR /\ SND WR w w' ==> holds WR V p w')`;;
6768
6869
let holds_in = new_definition
69-
`holds_in (W,R) p <=> !V w. w IN W ==> holds (W,R) V p w`;;
70+
`holds_in (W,R) p <=> !V w:W. w IN W ==> holds (W,R) V p w`;;
7071
7172
let valid = new_definition
72-
`L |= p <=> !f. L f ==> holds_in f p`;;
73+
`L |= p <=> !f:(W->bool)#(W->W->bool). f IN L ==> holds_in f p`;;
7374
```
7475

75-
###Soundness and consistency of GL
76-
```
77-
GL_consistent
78-
|- ~ [GL_AX . {} |~ False]
79-
```
8076
###Soundness and consistency of K
8177
```
8278
K_CONSISTENT
8379
|- ~ [{} . {} |~ False]
8480
```
8581

82+
###Soundness and consistency of GL
83+
```
84+
GL_consistent
85+
|- ~ [GL_AX . {} |~ False]
86+
```
87+
8688
###Completeness theorem
8789

8890
The proof is organized in three steps.
8991

9092
####STEP 1
9193
Identification of a non-empty set of possible worlds, given by a subclass of maximal consistent sets of formulas.
9294

93-
Parametric Definitions
95+
Parametric Definitions in gen_completness.ml
9496
```
95-
let GEN_STANDARD_FRAME = new_definition
96-
`GEN_STANDARD_FRAME K S p (W,R) <=>
97-
W = {w | MAXIMAL_CONSISTENT S p w /\
97+
let FRAME_DEF = new_definition
98+
`FRAME = {(W:W->bool,R:W->W->bool) | ~(W = {}) /\
99+
(!x y:W. R x y ==> x IN W /\ y IN W)}`;;
100+
101+
let GEN_STANDARD_FRAME_DEF = new_definition
102+
`GEN_STANDARD_FRAME P S p =
103+
FRAME INTER P INTER
104+
{(W,R) | W = {w | MAXIMAL_CONSISTENT S p w /\
98105
(!q. MEM q w ==> q SUBSENTENCE p)} /\
99-
K (W,R) /\
100-
(!q w. Box q SUBFORMULA p /\ w IN W
101-
==> (MEM (Box q) w <=> !x. R w x ==> MEM q x)) /\
102-
(K (W,R) ==> FRAME(W,R))`;;
106+
(!q w. Box q SUBFORMULA p /\ w IN W
107+
==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))}`;;
103108
104-
letGEN_STANDARD_MODEL = new_definition
105-
`GEN_STANDARD_MODELK S p (W,R) V <=>
106-
GEN_STANDARD_FRAMEK S p (W,R) /\
109+
letGEN_STANDARD_MODEL_DEF = new_definition
110+
`GEN_STANDARD_MODELP S p (W,R) V <=>
111+
(W,R) INGEN_STANDARD_FRAMEP S p /\
107112
(!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`;;
108113
```
109114

110-
Definitions inK
115+
Definitions ink_completness.ml
111116
```
112-
let K_FRAME = new_definition
113-
`K_FRAME (W,R) <=> FRAME(W,R) /\ FINITE W`;;
117+
let K_FRAME_DEF = new_definition
118+
`K_FRAME = {(W:W->bool,R) | (W,R) IN FRAME /\ FINITE W}`;;
119+
120+
let K_STANDARD_FRAME_DEF = new_definition
121+
`K_STANDARD_FRAME = GEN_STANDARD_FRAME K_FRAME {}`;;
122+
123+
IN_K_STANDARD_FRAME
124+
|- `(W,R) IN K_STANDARD_FRAME p <=>
125+
W = {w | MAXIMAL_CONSISTENT {} p w /\
126+
(!q. MEM q w ==> q SUBSENTENCE p)} /\
127+
(W,R) IN K_FRAME /\
128+
(!q w. Box q SUBFORMULA p /\ w IN W
129+
==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))`
114130
115-
let K_STANDARD_FRAME = new_definition
116-
`K_STANDARD_FRAME p (W,R) <=>
117-
GEN_STANDARD_FRAME K_FRAME {} p (W,R)`;;
131+
let K_STANDARD_MODEL_DEF = new_definition
132+
`K_STANDARD_MODEL = GEN_STANDARD_MODEL K_FRAME {}`;;
118133
119-
let K_STANDARD_MODEL = new_definition
120-
`K_STANDARD_MODEL p (W,R) V <=>
121-
GEN_STANDARD_MODEL K_FRAME {} p (W,R) V`;;
134+
K_STANDARD_MODEL_CAR
135+
|- `K_STANDARD_MODEL p (W,R) V <=>
136+
(W,R) IN K_STANDARD_FRAME p /\
137+
(!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))`
122138
```
123139

124-
Definitions inGL
140+
Definitions ingl_completness.ml
125141
```
126-
let ITF = new_definition
127-
`ITF <=>
128-
~(W = {}) /\
129-
(!x y. R x y ==> x IN W /\ y IN W) /\
130-
FINITE W /\
131-
(!x. x IN W ==> ~R x x) /\
132-
(!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)`;;
142+
let ITF_DEF = new_definition
143+
`ITF =
144+
{(W:W->bool,R:W->W->bool) |
145+
~(W = {}) /\
146+
(!x y:W. R x y ==> x IN W /\ y IN W) /\
147+
FINITE W /\
148+
(!x. x IN W ==> ~R x x) /\
149+
(!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)}`;;
150+
151+
let GL_STANDARD_FRAME_DEF = new_definition
152+
`GL_STANDARD_FRAME p = GEN_STANDARD_FRAME ITF GL_AX p`;;
133153
134-
let GL_STANDARD_FRAME = new_definition
135-
`GL_STANDARD_FRAME p (W,R) <=>
136-
GEN_STANDARD_FRAME ITF GL_AX p (W,R)`;;
154+
IN_GL_STANDARD_FRAME
155+
|- `!p W R. (W,R) IN GL_STANDARD_FRAME p <=>
156+
W = {w | MAXIMAL_CONSISTENT GL_AX p w /\
157+
(!q. MEM q w ==> q SUBSENTENCE p)} /\
158+
(W,R) IN ITF /\
159+
(!q w. Box q SUBFORMULA p /\ w IN W
160+
==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))`
137161
138-
let GL_STANDARD_MODEL = new_definition
139-
`GL_STANDARD_MODEL p (W,R) V <=>
140-
GEN_STANDARD_MODEL ITF GL_AX p (W,R) V`;;
162+
let GL_STANDARD_MODEL_DEF = new_definition
163+
`GL_STANDARD_MODEL = GEN_STANDARD_MODEL ITF GL_AX`;;
164+
165+
GL_STANDARD_MODEL_CAR
166+
|- `!W R p V.
167+
GL_STANDARD_MODEL p (W,R) V <=>
168+
(W,R) IN GL_STANDARD_FRAME p /\
169+
(!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p)) `
141170
```
142171

143172
####STEP 2
144173
Definition of a “standard” accessibility relation depending on axiom set S between these worlds such that the frame is appropriate to S.
145174

146-
Parametric definition of the standard relation
175+
Parametric definition of the standard relation in gen_completness.ml
147176
```
148177
let GEN_STANDARD_REL = new_definition
149178
`GEN_STANDARD_REL S p w x <=>
@@ -152,11 +181,16 @@ let GEN_STANDARD_REL = new_definition
152181
(!B. MEM (Box B) w ==> MEM B x)`;;
153182
```
154183

155-
InK
184+
Ink_completness.ml
156185
```
157186
let K_STANDARD_REL_DEF = new_definition
158-
`K_STANDARD_REL pw x <=> GEN_STANDARD_REL {} p w x`;;
187+
`K_STANDARD_REL p= GEN_STANDARD_REL {} p`;;
159188
189+
K_STANDARD_REL_CAR
190+
|-`K_STANDARD_REL p w x <=>
191+
MAXIMAL_CONSISTENT {} p w /\ (!q. MEM q w ==> q SUBSENTENCE p) /\
192+
MAXIMAL_CONSISTENT {} p x /\ (!q. MEM q x ==> q SUBSENTENCE p) /\
193+
(!B. MEM (Box B) w ==> MEM B x)`
160194
161195
K_ACCESSIBILITY_LEMMA_1
162196
|- `!p w q.
@@ -170,14 +204,14 @@ K_ACCESSIBILITY_LEMMA_1
170204

171205
In GL
172206
```
173-
letGL_STANDARD_REL = new_definition
207+
letGL_STANDARD_REL_DEF = new_definition
174208
`GL_STANDARD_REL p w x <=>
175209
GEN_STANDARD_REL GL_AX p w x /\
176210
(!B. MEM (Box B) w ==> MEM (Box B) x) /\
177211
(?E. MEM (Box E) x /\ MEM (Not (Box E)) w)`;;
178212
179-
ACCESSIBILITY_LEMMA
180-
|- !p M w q.
213+
GL_ACCESSIBILITY_LEMMA
214+
|-`!p M w q.
181215
~ [GL_AX . {} |~ p] /\
182216
MAXIMAL_CONSISTENT GL_AX p M /\
183217
(!q. MEM q M ==> q SUBSENTENCE p) /\
@@ -186,30 +220,32 @@ ACCESSIBILITY_LEMMA
186220
MEM (Not p) M /\
187221
Box q SUBFORMULA p /\
188222
(!x. GL_STANDARD_REL p w x ==> MEM q x)
189-
==> MEM (Box q) w
223+
==> MEM (Box q) w`
190224
```
191225

192226
####STEP 3
193-
Parametric truth lemma.
227+
Parametric truth lemma in gen_completness.ml
194228
```
195229
GEN_TRUTH_LEMMA
196-
|-!K S W R p V q.
230+
|-`!P S W R p V q.
197231
~ [S . {} |~ p] /\
198-
GEN_STANDARD_MODELK S p (W,R) V /\
232+
GEN_STANDARD_MODELP S p (W,R) V /\
199233
q SUBFORMULA p
200-
==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)
234+
==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w)`
201235
```
202236

203-
Completeness of K
237+
Completeness of K in k_completness.ml
204238
```
205239
K_COMPLETENESS_THM
206-
|- !p. K_FRAME |= p ==> [{} . {} |~ p]
240+
|- `!p. K_FRAME:(form list->bool)#(form list->form list->bool)->bool |= p
241+
==> [{} . {} |~ p]`
207242
```
208243

209-
Completeness of GL
244+
Completeness of GL in gl_completness.ml
210245
```
211246
COMPLETENESS_THEOREM
212-
|- !p. ITF |= p ==> [GL_AX . {} |~ p]
247+
|- `!p. ITF:(form list->bool)#(form list->form list->bool)->bool |= p
248+
==> [GL_AX . {} |~ p]`
213249
```
214250

215251
###Finite model property and decidability
@@ -230,8 +266,8 @@ let K_STDREL_RULES,K_STDREL_INDUCT,K_STDREL_CASES = new_inductive_definition
230266

231267
Theorem of existence of the finite countermodel.
232268
```
233-
GL_COUNTERMODEL_FINITE_SETS
234-
|- !p. ~[{} . {} |~ p] ==> ~holds_in (K_STDWORLDS p, K_STDREL p) p
269+
k_COUNTERMODEL_FINITE_SETS
270+
|-`!p. ~[{} . {} |~ p] ==> ~holds_in (K_STDWORLDS p, K_STDREL p) p`
235271
```
236272

237273
####In GL
@@ -251,7 +287,7 @@ let GL_STDREL_RULES,GL_STDREL_INDUCT,GL_STDREL_CASES = new_inductive_definition
251287
Theorem of existence of the finite countermodel.
252288
```
253289
GL_COUNTERMODEL_FINITE_SETS
254-
|- !p. ~ [GL_AX . {} |~ p] ==> ~holds_in (GL_STDWORLDS p, GL_STDREL p) p
290+
|-`!p. ~ [GL_AX . {} |~ p] ==> ~holds_in (GL_STDWORLDS p, GL_STDREL p) p`
255291
```
256292

257293
###Automated theorem proving and countermodel construction
@@ -281,7 +317,7 @@ time GL_RULE
281317
####Formalised Second Incompleteness Theorem
282318
In PA, the following is provable: If PA is consistent, it cannot prove its own consistency.
283319
```
284-
let GL_second_incompleteness_theorem = GL_RULE
320+
let GL_second_incompleteness_theorem =timeGL_RULE
285321
`[GL_AX . {} |~ Not (Box False) --> Not (Box (Diam True))]`;;
286322
```
287323

0 commit comments

Comments
 (0)
[8]ページ先頭
©2009-2025 Movatter.jp