@@ -58,10 +58,8 @@ let holds =
5858let holds_in = new_definition
5959 `holds_in (W,R) p <=> !V w. w IN W ==> holds (W,R) V p w`;;
6060
61- parse_as_infix("|=",(11,"right"));;
62-
6361let valid = new_definition
64- `L:(W->bool)#(W->W->bool)->bool |= p <=> !f. L f ==> holds_in f p`;;
62+ `L |= p <=> !f. L f ==> holds_in f p`;;
6563```
6664
6765###Soundness and consistency of GL
@@ -116,9 +114,9 @@ let K_STANDARD_MODEL = new_definition
116114Definitions in GL
117115```
118116let ITF = new_definition
119- `ITF(W:W->bool,R:W->W->bool) <=>
117+ `ITF <=>
120118 ~(W = {}) /\
121- (!x y:W . R x y ==> x IN W /\ y IN W) /\
119+ (!x y. R x y ==> x IN W /\ y IN W) /\
122120 FINITE W /\
123121 (!x. x IN W ==> ~R x x) /\
124122 (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)`;;
@@ -195,15 +193,13 @@ GEN_TRUTH_LEMMA
195193Completeness of K
196194```
197195K_COMPLETENESS_THM
198- |- !p. K_FRAME:(form list->bool)#(form list->form list->bool)->bool |= p
199- ==> [{} . {} |~ p]
196+ |- !p. K_FRAME |= p ==> [{} . {} |~ p]
200197```
201198
202199Completeness of GL
203200```
204201COMPLETENESS_THEOREM
205- |- !p. ITF:(form list->bool)#(form list->form list->bool)->bool |= p
206- ==> [GL_AX . {} |~ p]
202+ |- !p. ITF |= p ==> [GL_AX . {} |~ p]
207203```
208204
209205###Finite model property and decidability