Arithmetic/arithprov.ml

   1 (* ========================================================================= *)
   2 (* Proof that provability is definable; weak form of Godel's theorem.        *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Auxiliary predicate: all numbers in an iterated-pair "list".              *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let ALLN_DEF =
  12   let th = prove
  13    (`!P. ?ALLN. !z.
  14          ALLN z <=>
  15                 if ?x y. z = NPAIR x y
  16                 then P (@x. ?y. NPAIR x y = z) /\
  17                      ALLN (@y. ?x. NPAIR x y = z)
  18                 else T`,
  19     GEN_TAC THEN MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN
  20     REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
  21     BINOP_TAC THENL [ALL_TAC; FIRST_ASSUM MATCH_MP_TAC] THEN
  22     FIRST_ASSUM(REPEAT_TCL CHOOSE_THEN SUBST1_TAC) THEN
  23     REWRITE_TAC[NPAIR_INJ; RIGHT_EXISTS_AND_THM; EXISTS_REFL;
  24                 SELECT_REFL; NPAIR_LT; LEFT_EXISTS_AND_THM]) in
  25   new_specification ["ALLN"] (REWRITE_RULE[SKOLEM_THM] th);;
  26
  27 let ALLN = prove
  28  (`(ALLN P 0 <=> T) /\
  29    (ALLN P (NPAIR x y) <=> P x /\ ALLN P y)`,
  30   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [ALLN_DEF] THEN
  31   REWRITE_TAC[NPAIR_NONZERO] THEN
  32   REWRITE_TAC[NPAIR_INJ; LEFT_EXISTS_AND_THM; RIGHT_EXISTS_AND_THM] THEN
  33   REWRITE_TAC[EXISTS_REFL; GSYM EXISTS_REFL]);;
  34
  35 (* ------------------------------------------------------------------------- *)
  36 (* Valid term.                                                               *)
  37 (* ------------------------------------------------------------------------- *)
  38
  39 let TERM1 = new_definition
  40   `TERM1 x y <=>
  41         (?l u. (x = l) /\ (y = NPAIR (NPAIR 0 u) l)) \/
  42         (?l. (x = l) /\ (y = NPAIR (NPAIR 1 0) l)) \/
  43         (?t l. (x = NPAIR t l) /\ (y = NPAIR (NPAIR 2 t) l)) \/
  44         (?n s t l. ((n = 3) \/ (n = 4)) /\
  45                    (x = NPAIR s (NPAIR t l)) /\
  46                    (y = NPAIR (NPAIR n (NPAIR s t)) l))`;;
  47
  48 let TERM = new_definition
  49   `TERM n <=> RTC TERM1 0 (NPAIR n 0)`;;
  50
  51 let isagterm = new_definition
  52   `isagterm n <=> ?t. n = gterm t`;;
  53
  54 let TERM_LEMMA1 = prove
  55  (`!x y. TERM1 x y ==> ALLN isagterm x ==> ALLN isagterm y`,
  56   REPEAT GEN_TAC THEN REWRITE_TAC[TERM1] THEN
  57   REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
  58   SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN; isagterm] THEN
  59   MESON_TAC[gterm; NUMBER_SURJ]);;
  60
  61 let TERM_LEMMA2 = prove
  62  (`!t a. RTC TERM1 a (NPAIR (gterm t) a)`,
  63   MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[gterm] THEN
  64   MESON_TAC[RTC_INC; RTC_TRANS; TERM1]);;
  65
  66 let TERM_THM = prove
  67  (`!n. TERM n <=> ?t. n = gterm t`,
  68   GEN_TAC THEN REWRITE_TAC[TERM] THEN EQ_TAC THENL
  69    [ALL_TAC; MESON_TAC[TERM_LEMMA2]] THEN
  70   SUBGOAL_THEN `!x y. RTC TERM1 x y ==> ALLN isagterm x ==> ALLN isagterm y`
  71    (fun th -> MESON_TAC[ALLN; isagterm; th]) THEN
  72   MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[TERM_LEMMA1] THEN MESON_TAC[]);;
  73
  74 (* ------------------------------------------------------------------------- *)
  75 (* Valid formula.                                                            *)
  76 (* ------------------------------------------------------------------------- *)
  77
  78 let FORM1 = new_definition
  79   `FORM1 x y <=>
  80         (?l. (x = l) /\ (y = NPAIR (NPAIR 0 0) l)) \/
  81         (?l. (x = l) /\ (y = NPAIR (NPAIR 0 1) l)) \/
  82         (?n s t l. ((n = 1) \/ (n = 2) \/ (n = 3)) /\
  83                    TERM s /\ TERM t /\
  84                    (x = l) /\
  85                    (y = NPAIR (NPAIR n (NPAIR s t)) l)) \/
  86         (?p l. (x = NPAIR p l) /\
  87                (y = NPAIR (NPAIR 4 p) l)) \/
  88         (?n p q l. ((n = 5) \/ (n = 6) \/ (n = 7) \/ (n = 8)) /\
  89                    (x = NPAIR p (NPAIR q l)) /\
  90                    (y = NPAIR (NPAIR n (NPAIR p q)) l)) \/
  91         (?n u p l. ((n = 9) \/ (n = 10)) /\
  92                    (x = NPAIR p l) /\
  93                    (y = NPAIR (NPAIR n (NPAIR u p)) l))`;;
  94
  95 let FORM = new_definition
  96   `FORM n <=> RTC FORM1 0 (NPAIR n 0)`;;
  97
  98 let isagform = new_definition
  99   `isagform n <=> ?t. n = gform t`;;
 100
 101 let FORM_LEMMA1 = prove
 102  (`!x y. FORM1 x y ==> ALLN isagform x ==> ALLN isagform y`,
 103   REPEAT GEN_TAC THEN REWRITE_TAC[FORM1] THEN
 104   REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 105   SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN; isagform] THEN
 106   MESON_TAC[gform; TERM_THM; NUMBER_SURJ]);;
 107
 108 (*** Following really blows up if we just use FORM1
 109  *** instead of manually breaking up the conjuncts
 110  ***)
 111
 112 let FORM_LEMMA2 = prove
 113  (`!p a. RTC FORM1 a (NPAIR (gform p) a)`,
 114   MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[gform] THEN
 115   REPEAT CONJ_TAC THEN
 116   MESON_TAC[RTC_INC; RTC_TRANS; TERM_THM;
 117      REWRITE_RULE[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`]
 118                  (snd(EQ_IMP_RULE (SPEC_ALL FORM1)))]);;
 119
 120 let FORM_THM = prove
 121  (`!n. FORM n <=> ?p. n = gform p`,
 122   GEN_TAC THEN REWRITE_TAC[FORM] THEN EQ_TAC THENL
 123    [ALL_TAC; MESON_TAC[FORM_LEMMA2]] THEN
 124   SUBGOAL_THEN `!x y. RTC FORM1 x y ==> ALLN isagform x ==> ALLN isagform y`
 125    (fun th -> MESON_TAC[ALLN; isagform; th]) THEN
 126   MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FORM_LEMMA1] THEN MESON_TAC[]);;
 127
 128 (* ------------------------------------------------------------------------- *)
 129 (* Term without particular variable.                                         *)
 130 (* ------------------------------------------------------------------------- *)
 131
 132 let FREETERM1 = new_definition
 133   `FREETERM1 m x y <=>
 134         (?l u. ~(u = m) /\ (x = l) /\ (y = NPAIR (NPAIR 0 u) l)) \/
 135         (?l. (x = l) /\ (y = NPAIR (NPAIR 1 0) l)) \/
 136         (?t l. (x = NPAIR t l) /\ (y = NPAIR (NPAIR 2 t) l)) \/
 137         (?n s t l. ((n = 3) \/ (n = 4)) /\
 138                    (x = NPAIR s (NPAIR t l)) /\
 139                    (y = NPAIR (NPAIR n (NPAIR s t)) l))`;;
 140
 141 let FREETERM = new_definition
 142   `FREETERM m n <=> RTC (FREETERM1 m) 0 (NPAIR n 0)`;;
 143
 144 let isafterm = new_definition
 145   `isafterm m n <=> ?t. ~(m IN IMAGE number (FVT t)) /\ (n = gterm t)`;;
 146
 147 let ISAFTERM = prove
 148  (`(~(number x = m) ==> isafterm m (NPAIR 0 (number x))) /\
 149    isafterm m (NPAIR 1 0) /\
 150    (isafterm m t ==> isafterm m (NPAIR 2 t)) /\
 151    (isafterm m s /\ isafterm m t ==> isafterm m (NPAIR 3 (NPAIR s t))) /\
 152    (isafterm m s /\ isafterm m t ==> isafterm m (NPAIR 4 (NPAIR s t)))`,
 153   REWRITE_TAC[isafterm; gterm] THEN REPEAT CONJ_TAC THENL
 154    [DISCH_TAC THEN EXISTS_TAC `V x`;
 155     EXISTS_TAC `Z`;
 156     DISCH_THEN(X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC) THEN
 157     EXISTS_TAC `Suc t`;
 158     DISCH_THEN(CONJUNCTS_THEN2
 159      (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
 160      (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC)) THEN
 161     EXISTS_TAC `s ++ t`;
 162     DISCH_THEN(CONJUNCTS_THEN2
 163      (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
 164      (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC)) THEN
 165     EXISTS_TAC `s ** t`] THEN
 166   ASM_REWRITE_TAC[gterm; FVT; IMAGE_UNION; NOT_IN_EMPTY; IN_SING; IN_UNION;
 167                   IMAGE_CLAUSES]);;
 168
 169 let FREETERM_LEMMA1 = prove
 170  (`!m x y. FREETERM1 m x y ==> ALLN (isafterm m) x ==> ALLN (isafterm m) y`,
 171   REPEAT GEN_TAC THEN REWRITE_TAC[FREETERM1] THEN
 172   REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 173   SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
 174   MESON_TAC[ISAFTERM; NUMBER_SURJ]);;
 175
 176 let FREETERM_LEMMA2 = prove
 177  (`!m t a. ~(m IN IMAGE number (FVT t))
 178            ==> RTC (FREETERM1 m) a (NPAIR (gterm t) a)`,
 179   GEN_TAC THEN MATCH_MP_TAC term_INDUCT THEN
 180   REWRITE_TAC[gterm; FVT; NOT_IN_EMPTY; IN_SING; IN_UNION;
 181               IMAGE_CLAUSES; IMAGE_UNION] THEN
 182   REWRITE_TAC[DE_MORGAN_THM] THEN
 183   REPEAT CONJ_TAC THEN
 184   TRY(REPEAT GEN_TAC THEN DISCH_THEN
 185    (fun th -> GEN_TAC THEN STRIP_TAC THEN MP_TAC th)) THEN
 186   ASM_REWRITE_TAC[] THEN
 187   MESON_TAC[RTC_INC; RTC_TRANS; FREETERM1]);;
 188
 189 let FREETERM_THM = prove
 190  (`!m n. FREETERM m n <=> ?t. ~(m IN IMAGE number (FVT(t))) /\ (n = gterm t)`,
 191   REPEAT GEN_TAC THEN REWRITE_TAC[FREETERM] THEN EQ_TAC THENL
 192    [ALL_TAC; MESON_TAC[FREETERM_LEMMA2]] THEN
 193   SUBGOAL_THEN `!x y. RTC (FREETERM1 m) x y
 194                       ==> ALLN (isafterm m) x ==> ALLN (isafterm m) y`
 195    (fun th -> MESON_TAC[ALLN; isagterm; isafterm; th]) THEN
 196   MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FREETERM_LEMMA1] THEN MESON_TAC[]);;
 197
 198 (* ------------------------------------------------------------------------- *)
 199 (* Formula without particular free variable.                                 *)
 200 (* ------------------------------------------------------------------------- *)
 201
 202 let FREEFORM1 = new_definition
 203   `FREEFORM1 m x y <=>
 204         (?l. (x = l) /\ (y = NPAIR (NPAIR 0 0) l)) \/
 205         (?l. (x = l) /\ (y = NPAIR (NPAIR 0 1) l)) \/
 206         (?n s t l. ((n = 1) \/ (n = 2) \/ (n = 3)) /\
 207                    FREETERM m s /\ FREETERM m t /\
 208                    (x = l) /\
 209                    (y = NPAIR (NPAIR n (NPAIR s t)) l)) \/
 210         (?p l. (x = NPAIR p l) /\
 211                (y = NPAIR (NPAIR 4 p) l)) \/
 212         (?n p q l. ((n = 5) \/ (n = 6) \/ (n = 7) \/ (n = 8)) /\
 213                    (x = NPAIR p (NPAIR q l)) /\
 214                    (y = NPAIR (NPAIR n (NPAIR p q)) l)) \/
 215         (?n u p l. ((n = 9) \/ (n = 10)) /\
 216                    (x = NPAIR p l) /\
 217                    (y = NPAIR (NPAIR n (NPAIR u p)) l)) \/
 218         (?n p l. ((n = 9) \/ (n = 10)) /\
 219                  (x = l) /\ FORM p /\
 220                  (y = NPAIR (NPAIR n (NPAIR m p)) l))`;;
 221
 222 let FREEFORM = new_definition
 223   `FREEFORM m n <=> RTC (FREEFORM1 m) 0 (NPAIR n 0)`;;
 224
 225 let isafform = new_definition
 226   `isafform m n <=> ?p. ~(m IN IMAGE number (FV p)) /\ (n = gform p)`;;
 227
 228 let ISAFFORM = prove
 229  (`isafform m (NPAIR 0 0) /\
 230    isafform m (NPAIR 0 1) /\
 231    (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 1 (NPAIR s t))) /\
 232    (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 2 (NPAIR s t))) /\
 233    (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 3 (NPAIR s t))) /\
 234    (isafform m p ==> isafform m (NPAIR 4 p)) /\
 235    (isafform m p /\ isafform m q ==> isafform m (NPAIR 5 (NPAIR p q))) /\
 236    (isafform m p /\ isafform m q ==> isafform m (NPAIR 6 (NPAIR p q))) /\
 237    (isafform m p /\ isafform m q ==> isafform m (NPAIR 7 (NPAIR p q))) /\
 238    (isafform m p /\ isafform m q ==> isafform m (NPAIR 8 (NPAIR p q))) /\
 239    (isafform m p ==> isafform m (NPAIR 9 (NPAIR x p))) /\
 240    (isafform m p ==> isafform m (NPAIR 10 (NPAIR x p))) /\
 241    (isagform p ==> isafform m (NPAIR 9 (NPAIR m p))) /\
 242    (isagform p ==> isafform m (NPAIR 10 (NPAIR m p)))`,
 243   let tac0 = DISCH_THEN(X_CHOOSE_THEN `p:form` STRIP_ASSUME_TAC)
 244   and  tac1 =
 245     DISCH_THEN(CONJUNCTS_THEN2
 246      (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
 247      (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC))
 248   and tac2 =
 249     DISCH_THEN(CONJUNCTS_THEN2
 250      (X_CHOOSE_THEN `p:form` STRIP_ASSUME_TAC)
 251      (X_CHOOSE_THEN `q:form` STRIP_ASSUME_TAC)) in
 252   REWRITE_TAC[isafform; gform; isagform; isafterm] THEN REPEAT CONJ_TAC THENL
 253    [EXISTS_TAC `False`;
 254     EXISTS_TAC `True`;
 255     tac1 THEN EXISTS_TAC `s === t`;
 256     tac1 THEN EXISTS_TAC `s << t`;
 257     tac1 THEN EXISTS_TAC `s <<= t`;
 258     tac0 THEN EXISTS_TAC `Not p`;
 259     tac2 THEN EXISTS_TAC `p && q`;
 260     tac2 THEN EXISTS_TAC `p || q`;
 261     tac2 THEN EXISTS_TAC `p --> q`;
 262     tac2 THEN EXISTS_TAC `p <-> q`;
 263     tac0 THEN EXISTS_TAC `!!(denumber x) p`;
 264     tac0 THEN EXISTS_TAC `??(denumber x) p`;
 265     tac0 THEN EXISTS_TAC `!!(denumber m) p`;
 266     tac0 THEN EXISTS_TAC `??(denumber m) p`] THEN
 267   ASM_REWRITE_TAC[FV; IN_DELETE; NOT_IN_EMPTY; IN_SING; IN_UNION; gform;
 268                   NUMBER_DENUMBER; IMAGE_CLAUSES; IMAGE_UNION] THEN
 269   ASM SET_TAC[NUMBER_DENUMBER]);;
 270
 271 let FREEFORM_LEMMA1 = prove
 272  (`!x y. FREEFORM1 m x y ==> ALLN (isafform m) x ==> ALLN (isafform m) y`,
 273   REPEAT GEN_TAC THEN REWRITE_TAC[FREEFORM1] THEN
 274   REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 275   SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
 276   REWRITE_TAC[FREETERM_THM; GSYM isafterm] THEN
 277   REWRITE_TAC[FORM_THM; GSYM isagform] THEN MESON_TAC[ISAFFORM]);;
 278
 279 let FREEFORM_LEMMA2 = prove
 280  (`!m p a. ~(m IN IMAGE number (FV p))
 281            ==> RTC (FREEFORM1 m) a (NPAIR (gform p) a)`,
 282   let lemma = prove
 283    (`m IN IMAGE number (s DELETE k) <=>
 284      m IN IMAGE number s /\ ~(m = number k)`,
 285     SET_TAC[NUMBER_INJ]) in
 286   GEN_TAC THEN MATCH_MP_TAC form_INDUCT THEN
 287   REWRITE_TAC[gform; FV; NOT_IN_EMPTY; IN_DELETE; IN_SING; IN_UNION;
 288               lemma; IMAGE_UNION; IMAGE_CLAUSES] THEN
 289   REWRITE_TAC[DE_MORGAN_THM] THEN
 290   REPEAT CONJ_TAC THEN
 291   TRY(REPEAT GEN_TAC THEN DISCH_THEN
 292    (fun th -> GEN_TAC THEN STRIP_TAC THEN MP_TAC th)) THEN
 293   ASM_REWRITE_TAC[] THEN
 294   MESON_TAC[RTC_INC; RTC_TRANS; FORM_THM;
 295         REWRITE_RULE[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`;
 296                      FREETERM_THM]
 297                  (snd(EQ_IMP_RULE (SPEC_ALL FREEFORM1)))]);;
 298
 299 let FREEFORM_THM = prove
 300  (`!m n. FREEFORM m n <=> ?p. ~(m IN IMAGE number (FV p)) /\ (n = gform p)`,
 301   REPEAT GEN_TAC THEN REWRITE_TAC[FREEFORM] THEN EQ_TAC THENL
 302    [ALL_TAC; MESON_TAC[FREEFORM_LEMMA2]] THEN
 303   SUBGOAL_THEN `!x y. RTC (FREEFORM1 m) x y
 304                       ==> ALLN (isafform m) x ==> ALLN (isafform m) y`
 305    (fun th -> MESON_TAC[ALLN; isagform; isafform; th]) THEN
 306   MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FREEFORM_LEMMA1] THEN MESON_TAC[]);;
 307
 308 (* ------------------------------------------------------------------------- *)
 309 (* Arithmetization of logical axioms --- autogenerated.                      *)
 310 (* ------------------------------------------------------------------------- *)
 311
 312 let AXIOM,AXIOM_THM =
 313   let th0 = prove
 314    (`((?x p. P (number x) (gform p) /\ ~(x IN FV(p))) <=>
 315       (?x p. FREEFORM x p /\ P x p)) /\
 316      ((?x t. P (number x) (gterm t) /\ ~(x IN FVT(t))) <=>
 317       (?x t. FREETERM x t /\ P x t))`,
 318     REWRITE_TAC[FREETERM_THM; FREEFORM_THM] THEN CONJ_TAC THEN
 319     REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 320     ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
 321     GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV) [SWAP_EXISTS_THM] THEN
 322     REWRITE_TAC[UNWIND_THM2; IN_IMAGE] THEN
 323     ASM_MESON_TAC[IN_IMAGE; NUMBER_DENUMBER])
 324   and th1 = prove
 325    (`((?p. P(gform p)) <=> (?p. FORM(p) /\ P p)) /\
 326      ((?t. P(gterm t)) <=> (?t. TERM(t) /\ P t))`,
 327     MESON_TAC[FORM_THM; TERM_THM])
 328   and th2 = prove
 329    (`(?x. P(number x)) <=> (?x. P x)`,
 330     MESON_TAC[NUMBER_DENUMBER]) in
 331   let th = (REWRITE_CONV[GSYM GFORM_INJ] THENC
 332           REWRITE_CONV[gform; gterm] THENC
 333           REWRITE_CONV[th0] THENC REWRITE_CONV[th1] THENC
 334           REWRITE_CONV[th2] THENC
 335           REWRITE_CONV[RIGHT_AND_EXISTS_THM])
 336          (rhs(concl(SPEC `a:form` axiom_CASES))) in
 337   let dtm = mk_eq(`(AXIOM:num->bool) a`,
 338                    subst [`a:num`,`gform a`] (rhs(concl th))) in
 339   let AXIOM = new_definition dtm in
 340   let AXIOM_THM = prove
 341    (`!p. AXIOM(gform p) <=> axiom p`,
 342     REWRITE_TAC[axiom_CASES; AXIOM; th]) in
 343   AXIOM,AXIOM_THM;;
 344
 345 (* ------------------------------------------------------------------------- *)
 346 (* Prove also that all AXIOMs are in fact numbers of formulas.               *)
 347 (* ------------------------------------------------------------------------- *)
 348
 349 let GTERM_CASES_ALT = prove
 350  (`(gterm u = NPAIR 0 x <=> u = V(denumber x))`,
 351   REWRITE_TAC[GSYM GTERM_CASES; NUMBER_DENUMBER]);;
 352
 353 let GFORM_CASES_ALT = prove
 354  (`(gform r = NPAIR 9 (NPAIR x n) <=>
 355     (?p. r = !!(denumber x) p /\ gform p = n)) /\
 356    (gform r = NPAIR 10 (NPAIR x n) <=>
 357     (?p. r = ??(denumber x) p /\ gform p = n))`,
 358   REWRITE_TAC[GSYM GFORM_CASES; NUMBER_DENUMBER]);;
 359
 360 let AXIOM_FORMULA = prove
 361  (`!a. AXIOM a ==> ?p. a = gform p`,
 362   REWRITE_TAC[AXIOM; FREEFORM_THM; FREETERM_THM; FORM_THM; TERM_THM] THEN
 363   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 364   CONV_TAC(BINDER_CONV SYM_CONV) THEN
 365   REWRITE_TAC[GFORM_CASES; GTERM_CASES;
 366               GTERM_CASES_ALT; GFORM_CASES_ALT] THEN
 367   MESON_TAC[NUMBER_DENUMBER]);;
 368
 369 let AXIOM_THM_STRONG = prove
 370  (`!a. AXIOM a <=> ?p. axiom p /\ (a = gform p)`,
 371   MESON_TAC[AXIOM_THM; AXIOM_FORMULA]);;
 372
 373 (* ------------------------------------------------------------------------- *)
 374 (* Arithmetization of the full logical inference rules.                      *)
 375 (* ------------------------------------------------------------------------- *)
 376
 377 let PROV1 = new_definition
 378   `PROV1 A x y <=>
 379         (?a. (AXIOM a \/ a IN A) /\ (y = NPAIR a x)) \/
 380         (?p q l. (x = NPAIR (NPAIR 7 (NPAIR p q)) (NPAIR p l)) /\
 381                  (y = NPAIR q l)) \/
 382         (?p u l. (x = NPAIR p l) /\ (y = NPAIR (NPAIR 9 (NPAIR u p)) l))`;;
 383
 384 let PROV = new_definition
 385   `PROV A n <=> RTC (PROV1 A) 0 (NPAIR n 0)`;;
 386
 387 let isaprove = new_definition
 388   `isaprove A n <=> ?p. (gform p = n) /\ A |-- p`;;
 389
 390 let PROV_LEMMA1 = prove
 391  (`!A p q. PROV1 (IMAGE gform A) x y
 392            ==> ALLN (isaprove A) x ==> ALLN (isaprove A) y`,
 393   REPEAT GEN_TAC THEN REWRITE_TAC[PROV1] THEN
 394   REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 395   SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
 396   REWRITE_TAC[isaprove] THEN REPEAT CONJ_TAC THEN
 397   REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
 398    [ASM_MESON_TAC[AXIOM_THM_STRONG; proves_RULES];
 399     ASM_MESON_TAC[IN_IMAGE; GFORM_INJ; proves_RULES; gform];
 400     ALL_TAC;
 401     ASM_MESON_TAC[NUMBER_DENUMBER;
 402                   IN_IMAGE; GFORM_INJ; proves_RULES; gform]] THEN
 403   REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 404   ONCE_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 405   MATCH_MP_TAC form_INDUCT THEN
 406   REWRITE_TAC[gform; NPAIR_INJ; ARITH_EQ] THEN
 407   MAP_EVERY X_GEN_TAC [`P:form`; `Q:form`] THEN
 408   DISCH_THEN(K ALL_TAC) THEN
 409   DISCH_THEN(CONJUNCTS_THEN2 (STRIP_ASSUME_TAC o GSYM) MP_TAC) THEN
 410   ASM_REWRITE_TAC[GFORM_INJ] THEN
 411   REWRITE_TAC[GSYM CONJ_ASSOC; UNWIND_THM2] THEN
 412   ASM_MESON_TAC[proves_RULES]);;
 413
 414 let PROV_LEMMA2 = prove
 415  (`!A p. A |-- p ==> !a. RTC (PROV1 (IMAGE gform A)) a (NPAIR (gform p) a)`,
 416   GEN_TAC THEN MATCH_MP_TAC proves_INDUCT THEN REWRITE_TAC[gform] THEN
 417   MESON_TAC[RTC_INC; RTC_TRANS; PROV1; IN_IMAGE; AXIOM_THM]);;
 418
 419 let PROV_THM_STRONG = prove
 420  (`!A n. PROV (IMAGE gform A) n <=> ?p. A |-- p /\ (gform p = n)`,
 421   REPEAT GEN_TAC THEN REWRITE_TAC[PROV] THEN EQ_TAC THENL
 422    [ALL_TAC; MESON_TAC[PROV_LEMMA2]] THEN
 423   SUBGOAL_THEN
 424    `!x y. RTC (PROV1 (IMAGE gform A)) x y
 425            ==> ALLN (isaprove A) x ==> ALLN (isaprove A) y`
 426    (fun th -> MESON_TAC[ALLN; isaprove; GFORM_INJ; th]) THEN
 427   MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[PROV_LEMMA1] THEN MESON_TAC[]);;
 428
 429 let PROV_THM = prove
 430  (`!A p. PROV (IMAGE gform A) (gform p) <=> A |-- p`,
 431   MESON_TAC[PROV_THM_STRONG; GFORM_INJ]);;
 432
 433 (* ------------------------------------------------------------------------- *)
 434 (* Now really objectify all that.                                            *)
 435 (* ------------------------------------------------------------------------- *)
 436
 437 let arith_term1,ARITH_TERM1 = OBJECTIFY [] "arith_term1" TERM1;;
 438
 439 let FV_TERM1 = prove
 440  (`!s t. FV(arith_term1 s t) = (FVT s) UNION (FVT t)`,
 441   FV_TAC[arith_term1; FVT_PAIR; FVT_NUMERAL]);;
 442
 443 let arith_term,ARITH_TERM = OBJECTIFY_RTC ARITH_TERM1 "arith_term" TERM;;
 444
 445 let FV_TERM = prove
 446  (`!t. FV(arith_term t) = FVT t`,
 447   FV_TAC[arith_term; FV_RTC; FV_TERM1; FVT_PAIR; FVT_NUMERAL]);;
 448
 449 let arith_form1,ARITH_FORM1 =
 450  OBJECTIFY [ARITH_TERM] "arith_form1" FORM1;;
 451
 452 let FV_FORM1 = prove
 453  (`!s t. FV(arith_form1 s t) = (FVT s) UNION (FVT t)`,
 454   FV_TAC[arith_form1; FV_TERM; FVT_PAIR; FVT_NUMERAL]);;
 455
 456 let arith_form,ARITH_FORM = OBJECTIFY_RTC ARITH_FORM1 "arith_form" FORM;;
 457
 458 let FV_FORM = prove
 459  (`!t. FV(arith_form t) = FVT t`,
 460   FV_TAC[arith_form; FV_RTC; FV_FORM1; FVT_PAIR; FVT_NUMERAL]);;
 461
 462 let arith_freeterm1,ARITH_FREETERM1 =
 463  OBJECTIFY [] "arith_freeterm1" FREETERM1;;
 464
 465 let FV_FREETERM1 = prove
 466  (`!s t u. FV(arith_freeterm1 s t u) = (FVT s) UNION (FVT t) UNION (FVT u)`,
 467   FV_TAC[arith_freeterm1; FVT_PAIR; FVT_NUMERAL]);;
 468
 469 let arith_freeterm,ARITH_FREETERM =
 470   OBJECTIFY_RTCP ARITH_FREETERM1 "arith_freeterm" FREETERM;;
 471
 472 let FV_FREETERM = prove
 473  (`!s t. FV(arith_freeterm s t) = (FVT s) UNION (FVT t)`,
 474   FV_TAC[arith_freeterm; FV_RTCP; FV_FREETERM1; FVT_PAIR; FVT_NUMERAL]);;
 475
 476 let arith_freeform1,ARITH_FREEFORM1 =
 477  OBJECTIFY [ARITH_FREETERM; ARITH_FORM] "arith_freeform1" FREEFORM1;;
 478
 479 let FV_FREEFORM1 = prove
 480  (`!s t u. FV(arith_freeform1 s t u) = (FVT s) UNION (FVT t) UNION (FVT u)`,
 481   FV_TAC[arith_freeform1; FV_FREETERM; FV_FORM; FVT_PAIR; FVT_NUMERAL]);;
 482
 483 let arith_freeform,ARITH_FREEFORM =
 484  OBJECTIFY_RTCP ARITH_FREEFORM1 "arith_freeform" FREEFORM;;
 485
 486 let FV_FREEFORM = prove
 487  (`!s t. FV(arith_freeform s t) = (FVT s) UNION (FVT t)`,
 488   FV_TAC[arith_freeform; FV_RTCP; FV_FREEFORM1; FVT_PAIR; FVT_NUMERAL]);;
 489
 490 let arith_axiom,ARITH_AXIOM =
 491  OBJECTIFY [ARITH_FORM; ARITH_FREEFORM; ARITH_FREETERM; ARITH_TERM]
 492            "arith_axiom" AXIOM;;
 493
 494 let FV_AXIOM = prove
 495  (`!t. FV(arith_axiom t) = FVT t`,
 496   FV_TAC[arith_axiom; FV_FREETERM; FV_FREEFORM; FV_TERM; FV_FORM;
 497          FVT_PAIR; FVT_NUMERAL]);;
 498
 499 (* ------------------------------------------------------------------------- *)
 500 (* Parametrization by A means it's easier to do these cases manually.        *)
 501 (* ------------------------------------------------------------------------- *)
 502
 503 let arith_prov1,ARITH_PROV1 =
 504   let PROV1' = REWRITE_RULE[IN] PROV1 in
 505  OBJECTIFY [ASSUME `!v n. holds v (A n) <=> Ax (termval v n)`; ARITH_AXIOM]
 506    "arith_prov1" PROV1';;
 507
 508 let ARITH_PROV1 = prove
 509  (`(!v t. holds v (A t) <=> Ax(termval v t))
 510    ==> (!v s t.
 511              holds v (arith_prov1 A s t) <=>
 512              PROV1 Ax (termval v s) (termval v t))`,
 513   REWRITE_TAC[arith_prov1; holds; HOLDS_FORMSUBST] THEN
 514   REPEAT STRIP_TAC THEN
 515   ASM_REWRITE_TAC[termval; valmod; o_THM; ARITH_EQ; ARITH_PAIR;
 516                   TERMVAL_NUMERAL; ARITH_AXIOM] THEN
 517   REWRITE_TAC[PROV1; IN]);;
 518
 519 let FV_PROV1 = prove
 520  (`(!t. FV(A t) = FVT t) ==> !s t. FV(arith_prov1 A s t) = FVT(s) UNION FVT(t)`,
 521   FV_TAC[arith_prov1; FV_AXIOM; FVT_NUMERAL; FVT_PAIR]);;
 522
 523 let arith_prov = new_definition
 524  `arith_prov A n =
 525     formsubst ((0 |-> n) V)
 526         (arith_rtc (arith_prov1 A) (numeral 0)
 527                    (arith_pair (V 0) (numeral 0)))`;;
 528
 529 let ARITH_PROV = prove
 530  (`!Ax A. (!v t. holds v (A t) <=> Ax(termval v t))
 531           ==> !v n. holds v (arith_prov A n) <=> PROV Ax (termval v n)`,
 532   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP ARITH_PROV1) THEN
 533   DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC) THEN
 534   CONV_TAC(TOP_DEPTH_CONV ETA_CONV) THEN DISCH_TAC THEN
 535   ASM_REWRITE_TAC[arith_prov; HOLDS_FORMSUBST] THEN
 536   REWRITE_TAC[termval; valmod; o_DEF; TERMVAL_NUMERAL; ARITH_PAIR] THEN
 537   REWRITE_TAC[PROV]);;
 538
 539 let FV_PROV = prove
 540  (`(!t. FV(A t) = FVT t) ==> !t. FV(arith_prov A t) = FVT t`,
 541   FV_TAC[arith_prov; FV_PROV1; FV_RTC; FVT_NUMERAL; FVT_PAIR]);;
 542
 543 (* ------------------------------------------------------------------------- *)
 544 (* Our final conclusion.                                                     *)
 545 (* ------------------------------------------------------------------------- *)
 546
 547 let PROV_DEFINABLE = prove
 548  (`!Ax. definable {gform p | p IN Ax} ==> definable {gform p | Ax |-- p}`,
 549   GEN_TAC THEN REWRITE_TAC[definable; IN_ELIM_THM] THEN
 550   DISCH_THEN(X_CHOOSE_THEN `A:form` (X_CHOOSE_TAC `x:num`)) THEN
 551   MP_TAC(SPECL [`IMAGE gform Ax`; `\t. formsubst ((x |-> t) V) A`]
 552                ARITH_PROV) THEN
 553   REWRITE_TAC[] THEN ANTS_TAC THENL
 554    [ASM_REWRITE_TAC[HOLDS_FORMSUBST] THEN
 555     REWRITE_TAC[o_THM; VALMOD_BASIC; IMAGE; IN_ELIM_THM];
 556     ALL_TAC] THEN
 557   REWRITE_TAC[PROV_THM_STRONG] THEN DISCH_TAC THEN
 558   EXISTS_TAC `arith_prov (\t. formsubst ((x |-> t) V) A) (V x)` THEN
 559   ASM_REWRITE_TAC[termval] THEN MESON_TAC[]);;
 560
 561 (* ------------------------------------------------------------------------- *)
 562 (* The crudest conclusion: truth undefinable, provability not, so:           *)
 563 (* ------------------------------------------------------------------------- *)
 564
 565 let GODEL_CRUDE = prove
 566  (`!Ax. definable {gform p | p IN Ax} ==> ?p. ~(true p <=> Ax |-- p)`,
 567   REPEAT STRIP_TAC THEN MP_TAC TARSKI_THEOREM THEN
 568   FIRST_X_ASSUM(MP_TAC o MATCH_MP PROV_DEFINABLE) THEN
 569   MATCH_MP_TAC(TAUT `(~c ==> (a <=> b)) ==> a ==> ~b ==> c`) THEN
 570   SIMP_TAC[NOT_EXISTS_THM]);;