Arithmetic/godel.ml

   1 (* ========================================================================= *)
   2 (* Godel's theorem in its true form.                                         *)
   3 (* ========================================================================= *)
   4
   5 (* ------------------------------------------------------------------------- *)
   6 (* Classes of formulas, via auxiliary "shared" inductive definition.         *)
   7 (* ------------------------------------------------------------------------- *)
   8
   9 let sigmapi_RULES,sigmapi_INDUCT,sigmapi_CASES = new_inductive_definition
  10   `(!b n. sigmapi b n False) /\
  11    (!b n. sigmapi b n True) /\
  12    (!b n s t. sigmapi b n (s === t)) /\
  13    (!b n s t. sigmapi b n (s << t)) /\
  14    (!b n s t. sigmapi b n (s <<= t)) /\
  15    (!b n p. sigmapi (~b) n p ==> sigmapi b n (Not p)) /\
  16    (!b n p q. sigmapi b n p /\ sigmapi b n q ==> sigmapi b n (p && q)) /\
  17    (!b n p q. sigmapi b n p /\ sigmapi b n q ==> sigmapi b n (p || q)) /\
  18    (!b n p q. sigmapi (~b) n p /\ sigmapi b n q ==> sigmapi b n (p --> q)) /\
  19    (!b n p q. (!b. sigmapi b n p) /\ (!b. sigmapi b n q)
  20             ==> sigmapi b n (p <-> q)) /\
  21    (!n x p. sigmapi T n p /\ ~(n = 0) ==> sigmapi T n (??x p)) /\
  22    (!n x p. sigmapi F n p /\ ~(n = 0) ==> sigmapi F n (!!x p)) /\
  23    (!b n x p t. sigmapi b n p /\ ~(x IN FVT t)
  24             ==> sigmapi b n (??x (V x << t && p))) /\
  25    (!b n x p t. sigmapi b n p /\ ~(x IN FVT t)
  26             ==> sigmapi b n (??x (V x <<= t && p))) /\
  27    (!b n x p t. sigmapi b n p /\ ~(x IN FVT t)
  28             ==> sigmapi b n (!!x (V x << t --> p))) /\
  29    (!b n x p t. sigmapi b n p /\ ~(x IN FVT t)
  30             ==> sigmapi b n (!!x (V x <<= t --> p))) /\
  31    (!b c n p. sigmapi b n p ==> sigmapi c (n + 1) p)`;;
  32
  33 let SIGMA = new_definition `SIGMA = sigmapi T`;;
  34 let PI = new_definition `PI = sigmapi F`;;
  35 let DELTA = new_definition `DELTA n p <=> SIGMA n p /\ PI n p`;;
  36
  37 let SIGMAPI_PROP = prove
  38  (`(!n b. sigmapi b n False <=> T) /\
  39    (!n b. sigmapi b n True <=> T) /\
  40    (!n b s t. sigmapi b n (s === t) <=> T) /\
  41    (!n b s t. sigmapi b n (s << t) <=> T) /\
  42    (!n b s t. sigmapi b n (s <<= t) <=> T) /\
  43    (!n b p. sigmapi b n (Not p) <=> sigmapi (~b) n p) /\
  44    (!n b p q. sigmapi b n (p && q) <=> sigmapi b n p /\ sigmapi b n q) /\
  45    (!n b p q. sigmapi b n (p || q) <=> sigmapi b n p /\ sigmapi b n q) /\
  46    (!n b p q. sigmapi b n (p --> q) <=> sigmapi (~b) n p /\ sigmapi b n q) /\
  47    (!n b p q. sigmapi b n (p <-> q) <=> (sigmapi b n p /\ sigmapi (~b) n p) /\
  48                                         (sigmapi b n q /\ sigmapi (~b) n q))`,
  49    REWRITE_TAC[sigmapi_RULES] THEN
  50    GEN_REWRITE_TAC DEPTH_CONV [AND_FORALL_THM] THEN
  51    INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; SUC_SUB1] THEN
  52    REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [sigmapi_CASES] THEN
  53    REWRITE_TAC[form_DISTINCT; form_INJ] THEN
  54    REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1;
  55                FORALL_BOOL_THM] THEN
  56    REWRITE_TAC[ARITH_RULE `~(0 = n + 1)`] THEN
  57    REWRITE_TAC[ARITH_RULE `(SUC m = n + 1) <=> (n = m)`; UNWIND_THM2] THEN
  58    ASM_REWRITE_TAC[] THEN
  59    BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[ADD1] THEN
  60    REWRITE_TAC[CONJ_ACI] THEN
  61    REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THEN
  62    MESON_TAC[sigmapi_RULES]);;
  63
  64 let SIGMAPI_MONO_LEMMA = prove
  65  (`(!b n p. sigmapi b n p ==> sigmapi b (n + 1) p) /\
  66    (!b n p. ~(n = 0) /\ sigmapi b (n - 1) p ==> sigmapi b n p) /\
  67    (!b n p. ~(n = 0) /\ sigmapi (~b) (n - 1) p ==> sigmapi b n p)`,
  68   CONJ_TAC THENL
  69    [REPEAT STRIP_TAC;
  70     REPEAT STRIP_TAC THEN
  71     FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
  72      `~(n = 0) ==> (n = (n - 1) + 1)`))] THEN
  73   POP_ASSUM MP_TAC THEN ASM_MESON_TAC[sigmapi_RULES]);;
  74
  75 let SIGMAPI_REV_EXISTS = prove
  76  (`!n b x p. sigmapi b n (??x p) ==> sigmapi b n p`,
  77   MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
  78   REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [sigmapi_CASES] THEN
  79   REWRITE_TAC[form_DISTINCT; form_INJ] THEN
  80   REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
  81   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SIGMAPI_PROP] THEN
  82   ASM_MESON_TAC[ARITH_RULE `n < n + 1`; sigmapi_RULES]);;
  83
  84 let SIGMAPI_REV_FORALL = prove
  85  (`!n b x p. sigmapi b n (!!x p) ==> sigmapi b n p`,
  86   MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
  87   REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [sigmapi_CASES] THEN
  88   REWRITE_TAC[form_DISTINCT; form_INJ] THEN
  89   REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
  90   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SIGMAPI_PROP] THEN
  91   ASM_MESON_TAC[ARITH_RULE `n < n + 1`; sigmapi_RULES]);;
  92
  93 let SIGMAPI_CLAUSES_CODE = prove
  94  (`(!n b. sigmapi b n False <=> T) /\
  95    (!n b. sigmapi b n True <=> T) /\
  96    (!n b s t. sigmapi b n (s === t) <=> T) /\
  97    (!n b s t. sigmapi b n (s << t) <=> T) /\
  98    (!n b s t. sigmapi b n (s <<= t) <=> T) /\
  99    (!n b p. sigmapi b n (Not p) <=> sigmapi (~b) n p) /\
 100    (!n b p q. sigmapi b n (p && q) <=> sigmapi b n p /\ sigmapi b n q) /\
 101    (!n b p q. sigmapi b n (p || q) <=> sigmapi b n p /\ sigmapi b n q) /\
 102    (!n b p q. sigmapi b n (p --> q) <=> sigmapi (~b) n p /\ sigmapi b n q) /\
 103    (!n b p q. sigmapi b n (p <-> q) <=> (sigmapi b n p /\ sigmapi (~b) n p) /\
 104                                         (sigmapi b n q /\ sigmapi (~b) n q)) /\
 105    (!n b x p. sigmapi b n (??x p) <=>
 106                 if b /\ ~(n = 0) \/
 107                    ?q t. (p = (V x << t && q) \/ p = (V x <<= t && q)) /\
 108                          ~(x IN FVT t)
 109                 then sigmapi b n p
 110                 else ~(n = 0) /\ sigmapi (~b) (n - 1) (??x p)) /\
 111    (!n b x p. sigmapi b n (!!x p) <=>
 112                 if ~b /\ ~(n = 0) \/
 113                    ?q t. (p = (V x << t --> q) \/ p = (V x <<= t --> q)) /\
 114                          ~(x IN FVT t)
 115                 then sigmapi b n p
 116                 else ~(n = 0) /\ sigmapi (~b) (n - 1) (!!x p))`,
 117   REWRITE_TAC[SIGMAPI_PROP] THEN CONJ_TAC THEN REPEAT GEN_TAC THEN
 118   GEN_REWRITE_TAC LAND_CONV [sigmapi_CASES] THEN
 119   REWRITE_TAC[form_DISTINCT; form_INJ] THEN
 120   REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
 121   ONCE_REWRITE_TAC[TAUT `a \/ b \/ c \/ d <=> (b \/ c) \/ (a \/ d)`] THEN
 122   REWRITE_TAC[CONJ_ASSOC; OR_EXISTS_THM; GSYM RIGHT_OR_DISTRIB] THEN
 123   REWRITE_TAC[TAUT
 124    `(if b /\ c \/ d then e else c /\ f) <=>
 125     d /\ e \/ c /\ ~d /\ (if b then e else f)`] THEN
 126   MATCH_MP_TAC(TAUT `(a <=> a') /\ (~a' ==> (b <=> b'))
 127                      ==> (a \/ b <=> a' \/ b')`) THEN
 128   (CONJ_TAC THENL
 129     [REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 130      REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
 131      EQ_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 132      REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[SIGMAPI_PROP] THEN
 133      SIMP_TAC[];
 134      ALL_TAC]) THEN
 135   (ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH_RULE `~(0 = n + 1)`]) THEN
 136   ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> (n = m + 1 <=> m = n - 1)`] THEN
 137   REWRITE_TAC[UNWIND_THM2] THEN
 138   W(fun (asl,w) -> ASM_CASES_TAC (find_term is_exists w)) THEN
 139   ASM_REWRITE_TAC[CONTRAPOS_THM] THENL
 140    [DISCH_THEN(DISJ_CASES_THEN ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
 141     FIRST_X_ASSUM(CHOOSE_THEN(MP_TAC o MATCH_MP SIGMAPI_REV_EXISTS)) THEN
 142     DISCH_THEN(MP_TAC o MATCH_MP(last(CONJUNCTS sigmapi_RULES))) THEN
 143     ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `~(n = 0) ==> 1 <= n`];
 144     ASM_CASES_TAC `b:bool` THEN
 145     ASM_REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THENL
 146      [DISCH_THEN(CHOOSE_THEN(MP_TAC o MATCH_MP SIGMAPI_REV_EXISTS)) THEN
 147       DISCH_THEN(MP_TAC o MATCH_MP(last(CONJUNCTS sigmapi_RULES))) THEN
 148       ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `~(n = 0) ==> 1 <= n`];
 149       REWRITE_TAC[EXISTS_BOOL_THM] THEN
 150       REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THEN
 151       ONCE_REWRITE_TAC[sigmapi_CASES] THEN
 152       REWRITE_TAC[form_DISTINCT; form_INJ] THEN ASM_MESON_TAC[]];
 153     DISCH_THEN(DISJ_CASES_THEN ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
 154     FIRST_X_ASSUM(CHOOSE_THEN(MP_TAC o MATCH_MP SIGMAPI_REV_FORALL)) THEN
 155     DISCH_THEN(MP_TAC o MATCH_MP(last(CONJUNCTS sigmapi_RULES))) THEN
 156     ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `~(n = 0) ==> 1 <= n`];
 157     ASM_CASES_TAC `b:bool` THEN
 158     ASM_REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THENL
 159      [REWRITE_TAC[EXISTS_BOOL_THM] THEN
 160       REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THEN
 161       ONCE_REWRITE_TAC[sigmapi_CASES] THEN
 162       REWRITE_TAC[form_DISTINCT; form_INJ] THEN ASM_MESON_TAC[];
 163       DISCH_THEN(CHOOSE_THEN(MP_TAC o MATCH_MP SIGMAPI_REV_FORALL)) THEN
 164       DISCH_THEN(MP_TAC o MATCH_MP(last(CONJUNCTS sigmapi_RULES))) THEN
 165       ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `~(n = 0) ==> 1 <= n`]]]);;
 166
 167 let SIGMAPI_CLAUSES = prove
 168  (`(!n b. sigmapi b n False <=> T) /\
 169    (!n b. sigmapi b n True <=> T) /\
 170    (!n b s t. sigmapi b n (s === t) <=> T) /\
 171    (!n b s t. sigmapi b n (s << t) <=> T) /\
 172    (!n b s t. sigmapi b n (s <<= t) <=> T) /\
 173    (!n b p. sigmapi b n (Not p) <=> sigmapi (~b) n p) /\
 174    (!n b p q. sigmapi b n (p && q) <=> sigmapi b n p /\ sigmapi b n q) /\
 175    (!n b p q. sigmapi b n (p || q) <=> sigmapi b n p /\ sigmapi b n q) /\
 176    (!n b p q. sigmapi b n (p --> q) <=> sigmapi (~b) n p /\ sigmapi b n q) /\
 177    (!n b p q. sigmapi b n (p <-> q) <=> (sigmapi b n p /\ sigmapi (~b) n p) /\
 178                                         (sigmapi b n q /\ sigmapi (~b) n q)) /\
 179    (!n b x p. sigmapi b n (??x p) <=>
 180                 if b /\ ~(n = 0) \/
 181                    ?q t. (p = (V x << t && q) \/ p = (V x <<= t && q)) /\
 182                          ~(x IN FVT t)
 183                 then sigmapi b n p
 184                 else 2 <= n /\ sigmapi (~b) (n - 1) p) /\
 185    (!n b x p. sigmapi b n (!!x p) <=>
 186                 if ~b /\ ~(n = 0) \/
 187                    ?q t. (p = (V x << t --> q) \/ p = (V x <<= t --> q)) /\
 188                          ~(x IN FVT t)
 189                 then sigmapi b n p
 190                 else 2 <= n /\ sigmapi (~b) (n - 1) p)`,
 191   REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
 192   GEN_REWRITE_TAC LAND_CONV [SIGMAPI_CLAUSES_CODE] THEN
 193   REWRITE_TAC[] THEN
 194   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN
 195   BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[] THEN
 196   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 197   GEN_REWRITE_TAC LAND_CONV [SIGMAPI_CLAUSES_CODE] THEN
 198   ASM_REWRITE_TAC[ARITH_RULE `~(n - 1 = 0) <=> 2 <= n`] THEN
 199   MESON_TAC[]);;
 200
 201 (* ------------------------------------------------------------------------- *)
 202 (* Show that it respects substitution.                                       *)
 203 (* ------------------------------------------------------------------------- *)
 204
 205 let SIGMAPI_FORMSUBST = prove
 206  (`!p v n b. sigmapi b n p ==> sigmapi b n (formsubst v p)`,
 207   MATCH_MP_TAC form_INDUCT THEN
 208   REWRITE_TAC[SIGMAPI_CLAUSES; formsubst] THEN SIMP_TAC[] THEN
 209   REWRITE_TAC[AND_FORALL_THM] THEN MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN
 210   MATCH_MP_TAC(TAUT `(a ==> b /\ c) ==> (a ==> b) /\ (a ==> c)`) THEN
 211   DISCH_TAC THEN REWRITE_TAC[AND_FORALL_THM] THEN
 212   MAP_EVERY X_GEN_TAC [`i:num->term`; `n:num`; `b:bool`] THEN
 213   REWRITE_TAC[FV] THEN LET_TAC THEN
 214   CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
 215   REWRITE_TAC[SIGMAPI_CLAUSES] THEN
 216   ONCE_REWRITE_TAC[TAUT
 217    `((if p \/ q then x else y) ==> (if p \/ q' then x' else y')) <=>
 218     (p /\ x ==> x') /\
 219     (~p ==> (if q then x else y) ==> (if q' then x' else y'))`] THEN
 220   ASM_SIMP_TAC[] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
 221   CONJ_TAC THEN DISCH_THEN(K ALL_TAC) THEN MATCH_MP_TAC(TAUT
 222    `(p ==> p') /\ (x ==> x') /\ (y ==> y') /\ (y ==> x)
 223     ==> (if p then x else y) ==> (if p' then x' else y')`) THEN
 224   ASM_SIMP_TAC[SIGMAPI_MONO_LEMMA; ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
 225   STRIP_TAC THEN ASM_REWRITE_TAC[formsubst; form_INJ; termsubst] THEN
 226   REWRITE_TAC[form_DISTINCT] THEN
 227   ONCE_REWRITE_TAC[TAUT `((a /\ b) /\ c) /\ d <=> b /\ c /\ a /\ d`] THEN
 228   REWRITE_TAC[UNWIND_THM1; termsubst; VALMOD_BASIC] THEN
 229   REWRITE_TAC[TERMSUBST_FVT; IN_ELIM_THM; NOT_EXISTS_THM] THEN
 230   X_GEN_TAC `y:num` THEN REWRITE_TAC[valmod] THEN
 231   (COND_CASES_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]) THEN
 232   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 233   FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (funpow 2 LAND_CONV) [SYM th]) THEN
 234   FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[FV; FVT] THEN
 235   REWRITE_TAC[IN_DELETE; IN_UNION; IN_SING; GSYM DISJ_ASSOC] THEN
 236   REWRITE_TAC[TAUT `(a \/ b \/ c) /\ ~a <=> ~a /\ b \/ ~a /\ c`] THEN
 237   (COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]]) THEN
 238   W(fun (asl,w) -> let t = lhand(rand w) in
 239                    MP_TAC(SPEC (rand(rand t)) VARIANT_THM) THEN
 240                    SPEC_TAC(t,`u:num`)) THEN
 241   REWRITE_TAC[CONTRAPOS_THM; FORMSUBST_FV; IN_ELIM_THM; FV] THEN
 242   GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC `y:num` THEN
 243   ASM_REWRITE_TAC[valmod; IN_UNION]);;
 244
 245 (* ------------------------------------------------------------------------- *)
 246 (* Hence all our main concepts are OK.                                       *)
 247 (* ------------------------------------------------------------------------- *)
 248
 249 let SIGMAPI_TAC ths =
 250   REPEAT STRIP_TAC THEN
 251   REWRITE_TAC ths THEN
 252   TRY(MATCH_MP_TAC SIGMAPI_FORMSUBST) THEN
 253   let ths' = ths @  [SIGMAPI_CLAUSES; form_DISTINCT;
 254                      form_INJ; GSYM CONJ_ASSOC; UNWIND_THM1; GSYM EXISTS_REFL;
 255                      FVT; IN_SING; ARITH_EQ] in
 256   REWRITE_TAC ths' THEN ASM_SIMP_TAC ths';;
 257
 258 let SIGMAPI_DIVIDES = prove
 259  (`!n s t. sigmapi b n (arith_divides s t)`,
 260   SIGMAPI_TAC[arith_divides]);;
 261
 262 let SIGMAPI_PRIME = prove
 263  (`!n t. sigmapi b n (arith_prime t)`,
 264   SIGMAPI_TAC[arith_prime; SIGMAPI_DIVIDES]);;
 265
 266 let SIGMAPI_PRIMEPOW = prove
 267  (`!n s t. sigmapi b n (arith_primepow s t)`,
 268   SIGMAPI_TAC[arith_primepow; SIGMAPI_DIVIDES; SIGMAPI_PRIME]);;
 269
 270 let SIGMAPI_RTC = prove
 271  (`(!s t. sigmapi T 1 (R s t))
 272    ==> !s t. sigmapi T 1 (arith_rtc R s t)`,
 273   REPEAT STRIP_TAC THEN REWRITE_TAC[arith_rtc] THEN
 274   MATCH_MP_TAC SIGMAPI_FORMSUBST THEN
 275   REWRITE_TAC[SIGMAPI_CLAUSES; form_INJ; GSYM CONJ_ASSOC; UNWIND_THM1;
 276               GSYM EXISTS_REFL; FVT; IN_SING; ARITH_EQ; SIGMAPI_DIVIDES;
 277               SIGMAPI_PRIME; SIGMAPI_PRIMEPOW; form_DISTINCT] THEN
 278   ASM_REWRITE_TAC[]);;
 279
 280 let SIGMAPI_RTCP = prove
 281  (`(!s t u. sigmapi T 1 (R s t u))
 282    ==> !s t u. sigmapi T 1 (arith_rtcp R s t u)`,
 283   REPEAT STRIP_TAC THEN REWRITE_TAC[arith_rtcp] THEN
 284   MATCH_MP_TAC SIGMAPI_FORMSUBST THEN
 285   REWRITE_TAC[SIGMAPI_CLAUSES; form_INJ; GSYM CONJ_ASSOC; UNWIND_THM1;
 286               GSYM EXISTS_REFL; FVT; IN_SING; ARITH_EQ; SIGMAPI_DIVIDES;
 287               SIGMAPI_PRIME; SIGMAPI_PRIMEPOW; form_DISTINCT] THEN
 288   ASM_REWRITE_TAC[]);;
 289
 290 let SIGMAPI_TERM1 = prove
 291  (`!s t. sigmapi T 1 (arith_term1 s t)`,
 292   SIGMAPI_TAC[arith_term1]);;
 293
 294 let SIGMAPI_TERM = prove
 295  (`!t. sigmapi T 1 (arith_term t)`,
 296   SIGMAPI_TAC[arith_term; SIGMAPI_RTC; SIGMAPI_TERM1]);;
 297
 298 let SIGMAPI_FORM1 = prove
 299  (`!s t. sigmapi T 1 (arith_form1 s t)`,
 300   SIGMAPI_TAC[arith_form1; SIGMAPI_TERM]);;
 301
 302 let SIGMAPI_FORM = prove
 303  (`!t. sigmapi T 1 (arith_form t)`,
 304   SIGMAPI_TAC[arith_form; SIGMAPI_RTC; SIGMAPI_FORM1]);;
 305
 306 let SIGMAPI_FREETERM1 = prove
 307  (`!s t u. sigmapi T 1 (arith_freeterm1 s t u)`,
 308   SIGMAPI_TAC[arith_freeterm1]);;
 309
 310 let SIGMAPI_FREETERM = prove
 311  (`!s t. sigmapi T 1 (arith_freeterm s t)`,
 312   SIGMAPI_TAC[arith_freeterm; SIGMAPI_FREETERM1; SIGMAPI_RTCP]);;
 313
 314 let SIGMAPI_FREEFORM1 = prove
 315  (`!s t u. sigmapi T 1 (arith_freeform1 s t u)`,
 316   SIGMAPI_TAC[arith_freeform1; SIGMAPI_FREETERM; SIGMAPI_FORM]);;
 317
 318 let SIGMAPI_FREEFORM = prove
 319  (`!s t. sigmapi T 1 (arith_freeform s t)`,
 320   SIGMAPI_TAC[arith_freeform; SIGMAPI_FREEFORM1; SIGMAPI_RTCP]);;
 321
 322 let SIGMAPI_AXIOM = prove
 323  (`!t. sigmapi T 1 (arith_axiom t)`,
 324   SIGMAPI_TAC[arith_axiom; SIGMAPI_FREEFORM; SIGMAPI_FREETERM; SIGMAPI_FORM;
 325               SIGMAPI_TERM]);;
 326
 327 let SIGMAPI_PROV1 = prove
 328  (`!A. (!t. sigmapi T 1 (A t)) ==> !s t. sigmapi T 1 (arith_prov1 A s t)`,
 329   SIGMAPI_TAC[arith_prov1; SIGMAPI_AXIOM]);;
 330
 331 let SIGMAPI_PROV = prove
 332  (`(!t. sigmapi T 1 (A t)) ==> !t. sigmapi T 1 (arith_prov A t)`,
 333   SIGMAPI_TAC[arith_prov; SIGMAPI_PROV1; SIGMAPI_RTC]);;
 334
 335 let SIGMAPI_PRIMRECSTEP = prove
 336  (`(!s t u. sigmapi T 1 (R s t u))
 337    ==> !s t. sigmapi T 1 (arith_primrecstep R s t)`,
 338   SIGMAPI_TAC[arith_primrecstep]);;
 339
 340 let SIGMAPI_PRIMREC = prove
 341  (`(!s t u. sigmapi T 1 (R s t u))
 342    ==> !s t. sigmapi T 1 (arith_primrec R c s t)`,
 343   SIGMAPI_TAC[arith_primrec; SIGMAPI_PRIMRECSTEP; SIGMAPI_RTC]);;
 344
 345 let  SIGMAPI_GNUMERAL1 = prove
 346  (`!s t. sigmapi T 1 (arith_gnumeral1 s t)`,
 347   SIGMAPI_TAC[arith_gnumeral1]);;
 348
 349 let SIGMAPI_GNUMERAL = prove
 350  (`!s t. sigmapi T 1 (arith_gnumeral s t)`,
 351   SIGMAPI_TAC[arith_gnumeral; arith_gnumeral1';
 352               SIGMAPI_GNUMERAL1; SIGMAPI_RTC]);;
 353
 354 let SIGMAPI_QSUBST = prove
 355  (`!x n p.  sigmapi T 1 p ==> sigmapi T 1 (qsubst(x,n) p)`,
 356   SIGMAPI_TAC[qsubst]);;
 357
 358 let SIGMAPI_QDIAG = prove
 359  (`!x s t. sigmapi T 1 (arith_qdiag x s t)`,
 360   SIGMAPI_TAC[arith_qdiag; SIGMAPI_GNUMERAL]);;
 361
 362 let SIGMAPI_DIAGONALIZE = prove
 363  (`!x p. sigmapi T 1 p ==> sigmapi T 1 (diagonalize x p)`,
 364   SIGMAPI_TAC[diagonalize; SIGMAPI_QDIAG;
 365         SIGMAPI_FORMSUBST; LET_DEF; LET_END_DEF]);;
 366
 367 let SIGMAPI_FIXPOINT = prove
 368  (`!x p. sigmapi T 1 p ==> sigmapi T 1 (fixpoint x p)`,
 369   SIGMAPI_TAC[fixpoint; qdiag; SIGMAPI_QSUBST; SIGMAPI_DIAGONALIZE]);;
 370
 371 (* ------------------------------------------------------------------------- *)
 372 (* The Godel sentence, "H" being Sigma and "G" being Pi.                     *)
 373 (* ------------------------------------------------------------------------- *)
 374
 375 let hsentence = new_definition
 376   `hsentence Arep =
 377     fixpoint 0 (arith_prov Arep (arith_pair (numeral 4) (V 0)))`;;
 378
 379 let gsentence = new_definition
 380   `gsentence Arep = Not(hsentence Arep)`;;
 381
 382 let FV_HSENTENCE = prove
 383  (`!Arep. (!t. FV(Arep t) = FVT t) ==> (FV(hsentence Arep) = {})`,
 384   SIMP_TAC[hsentence; FV_FIXPOINT; FV_PROV] THEN
 385   REWRITE_TAC[FVT_PAIR; FVT_NUMERAL; FVT; UNION_EMPTY; DELETE_INSERT;
 386               EMPTY_DELETE]);;
 387
 388 let FV_GSENTENCE = prove
 389  (`!Arep. (!t. FV(Arep t) = FVT t) ==> (FV(gsentence Arep) = {})`,
 390   SIMP_TAC[gsentence; FV_HSENTENCE; FV]);;
 391
 392 let SIGMAPI_HSENTENCE = prove
 393  (`!Arep. (!t. sigmapi T 1 (Arep t)) ==> sigmapi T 1 (hsentence Arep)`,
 394   SIGMAPI_TAC[hsentence; SIGMAPI_FIXPOINT; SIGMAPI_PROV]);;
 395
 396 let SIGMAPI_GSENTENCE = prove
 397  (`!Arep. (!t. sigmapi T 1 (Arep t)) ==> sigmapi F 1 (gsentence Arep)`,
 398   SIGMAPI_TAC[gsentence; SIGMAPI_HSENTENCE]);;
 399
 400 (* ------------------------------------------------------------------------- *)
 401 (* Hence the key fixpoint properties.                                        *)
 402 (* ------------------------------------------------------------------------- *)
 403
 404 let HSENTENCE_FIX_STRONG = prove
 405  (`!A Arep.
 406         (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
 407         ==> !v. holds v (hsentence Arep) <=> A |-- Not(hsentence Arep)`,
 408   REWRITE_TAC[hsentence; true_def; HOLDS_FIXPOINT] THEN
 409   REPEAT STRIP_TAC THEN
 410   FIRST_ASSUM(MP_TAC o MATCH_MP ARITH_PROV) THEN
 411   REWRITE_TAC[IN] THEN CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
 412   DISCH_TAC THEN ASM_REWRITE_TAC[ARITH_PAIR; TERMVAL_NUMERAL] THEN
 413   REWRITE_TAC[termval; valmod; GSYM gform] THEN REWRITE_TAC[PROV_THM]);;
 414
 415 let HSENTENCE_FIX = prove
 416  (`!A Arep.
 417         (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
 418         ==> (true(hsentence Arep) <=> A |-- Not(hsentence Arep))`,
 419   REWRITE_TAC[true_def] THEN MESON_TAC[HSENTENCE_FIX_STRONG]);;
 420
 421 let GSENTENCE_FIX = prove
 422  (`!A Arep.
 423         (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
 424         ==> (true(gsentence Arep) <=> ~(A |-- gsentence Arep))`,
 425   REWRITE_TAC[true_def; holds; gsentence] THEN
 426   MESON_TAC[HSENTENCE_FIX_STRONG]);;
 427
 428 (* ------------------------------------------------------------------------- *)
 429 (* Auxiliary concepts.                                                       *)
 430 (* ------------------------------------------------------------------------- *)
 431
 432 let ground = new_definition
 433   `ground t <=> (FVT t = {})`;;
 434
 435 let complete_for = new_definition
 436   `complete_for P A <=> !p. P p /\ true p ==> A |-- p`;;
 437
 438 let sound_for = new_definition
 439   `sound_for P A <=> !p. P p /\ A |-- p ==> true p`;;
 440
 441 let consistent = new_definition
 442   `consistent A <=> ~(?p. A |-- p /\ A |-- Not p)`;;
 443
 444 let CONSISTENT_ALT = prove
 445  (`!A p. A |-- p /\ A |-- Not p <=> A |-- False`,
 446   MESON_TAC[proves_RULES; axiom_RULES]);;
 447
 448 (* ------------------------------------------------------------------------- *)
 449 (* The purest and most symmetric and beautiful form of G1.                   *)
 450 (* ------------------------------------------------------------------------- *)
 451
 452 let DEFINABLE_BY_ONEVAR = prove
 453  (`definable_by (SIGMA 1) s <=>
 454         ?p x. SIGMA 1 p /\ (FV p = {x}) /\ !v. holds v p <=> (v x) IN s`,
 455   REWRITE_TAC[definable_by; SIGMA] THEN
 456   EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
 457   DISCH_THEN(X_CHOOSE_THEN `p:form` (X_CHOOSE_TAC `x:num`)) THEN
 458   EXISTS_TAC `(V x === V x) && formsubst (\y. if y = x then V x else Z) p` THEN
 459   EXISTS_TAC `x:num` THEN ASM_SIMP_TAC[SIGMAPI_CLAUSES; SIGMAPI_FORMSUBST] THEN
 460   ASM_REWRITE_TAC[HOLDS_FORMSUBST; FORMSUBST_FV; FV; holds] THEN
 461   REWRITE_TAC[COND_RAND; EXTENSION; IN_ELIM_THM; IN_SING; FVT; IN_UNION;
 462               COND_EXPAND; NOT_IN_EMPTY; o_THM; termval] THEN
 463   MESON_TAC[]);;
 464
 465 let CLOSED_NOT_TRUE = prove
 466  (`!p. closed p ==> (true(Not p) <=> ~(true p))`,
 467   REWRITE_TAC[closed; true_def; holds] THEN
 468   MESON_TAC[HOLDS_VALUATION; NOT_IN_EMPTY]);;
 469
 470 let G1 = prove
 471  (`!A. definable_by (SIGMA 1) (IMAGE gform A)
 472        ==> ?G. PI 1 G /\ closed G /\
 473                (sound_for (PI 1 INTER closed) A ==> true G /\ ~(A |-- G)) /\
 474                (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))`,
 475   GEN_TAC THEN
 476   REWRITE_TAC[sound_for; INTER; IN_ELIM_THM; DEFINABLE_BY_ONEVAR] THEN
 477   DISCH_THEN(X_CHOOSE_THEN `Arep:form` (X_CHOOSE_THEN `a:num`
 478         STRIP_ASSUME_TAC)) THEN
 479   MP_TAC(SPECL [`A:form->bool`; `\t. formsubst ((a |-> t) V) Arep`]
 480          GSENTENCE_FIX) THEN
 481   REWRITE_TAC[] THEN ANTS_TAC THENL
 482    [ASM_REWRITE_TAC[HOLDS_FORMSUBST] THEN REWRITE_TAC[termval; valmod; o_THM];
 483     ALL_TAC] THEN
 484   STRIP_TAC THEN EXISTS_TAC `gsentence (\t. formsubst ((a |-> t) V) Arep)` THEN
 485   ASM_REWRITE_TAC[] THEN
 486   MATCH_MP_TAC(TAUT `a /\ b /\ (a /\ b ==> c /\ d) ==> a /\ b /\ c /\ d`) THEN
 487   REPEAT CONJ_TAC THENL
 488    [REWRITE_TAC[PI] THEN MATCH_MP_TAC SIGMAPI_GSENTENCE THEN
 489     RULE_ASSUM_TAC(REWRITE_RULE[SIGMA]) THEN ASM_SIMP_TAC[SIGMAPI_FORMSUBST];
 490     REWRITE_TAC[closed] THEN MATCH_MP_TAC FV_GSENTENCE THEN
 491     ASM_REWRITE_TAC[FORMSUBST_FV; EXTENSION; IN_ELIM_THM; IN_SING;
 492                     valmod; UNWIND_THM2];
 493     ALL_TAC] THEN
 494   ABBREV_TAC `G = gsentence (\t. formsubst ((a |-> t) V) Arep)` THEN
 495   REPEAT STRIP_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
 496   SUBGOAL_THEN `true(Not G)` MP_TAC THENL
 497    [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN] THEN
 498     REWRITE_TAC[SIGMA; SIGMAPI_CLAUSES] THEN ASM_MESON_TAC[closed; FV; PI];
 499     ALL_TAC] THEN
 500   FIRST_ASSUM(SUBST1_TAC o MATCH_MP CLOSED_NOT_TRUE) THEN
 501   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 502   SUBGOAL_THEN `true False` MP_TAC THENL
 503    [ALL_TAC; REWRITE_TAC[true_def; holds]] THEN
 504   FIRST_X_ASSUM MATCH_MP_TAC THEN
 505   REWRITE_TAC[closed; IN; SIGMA; SIGMAPI_CLAUSES; FV] THEN
 506   ASM_MESON_TAC[CONSISTENT_ALT]);;
 507
 508 (* ------------------------------------------------------------------------- *)
 509 (* Some more familiar variants.                                              *)
 510 (* ------------------------------------------------------------------------- *)
 511
 512 let COMPLETE_SOUND_SENTENCE = prove
 513  (`consistent A /\ complete_for (sigmapi (~b) n INTER closed) A
 514    ==> sound_for (sigmapi b n INTER closed) A`,
 515   REWRITE_TAC[consistent; sound_for; complete_for; IN; INTER; IN_ELIM_THM] THEN
 516   REWRITE_TAC[NOT_EXISTS_THM] THEN
 517   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 518   DISCH_THEN(fun th -> X_GEN_TAC `p:form` THEN MP_TAC(SPEC `Not p` th)) THEN
 519   REWRITE_TAC[SIGMAPI_CLAUSES] THEN
 520   REWRITE_TAC[closed; FV; true_def; holds] THEN
 521   ASM_MESON_TAC[HOLDS_VALUATION; NOT_IN_EMPTY]);;
 522
 523 let G1_TRAD = prove
 524  (`!A. consistent A /\
 525        complete_for (SIGMA 1 INTER closed) A /\
 526        definable_by (SIGMA 1) (IMAGE gform A)
 527        ==> ?G. PI 1 G /\ closed G /\ true G /\ ~(A |-- G) /\
 528                (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))`,
 529   REWRITE_TAC[SIGMA] THEN REPEAT STRIP_TAC THEN
 530   MP_TAC(SPEC `A:form->bool` G1) THEN ASM_REWRITE_TAC[SIGMA; PI] THEN
 531   MATCH_MP_TAC MONO_EXISTS THEN ASM_SIMP_TAC[COMPLETE_SOUND_SENTENCE]);;