X-Git-Url: http://colo12-c703.uibk.ac.at/git/?p=G%C3%B6del%27s%20incompleteness%20theorem%2F.git;a=blobdiff_plain;f=Arithmetic%2Farithprov.ml;fp=Arithmetic%2Farithprov.ml;h=ab308ff2abaa6d490f6a9655f077ce98d804f843;hp=0000000000000000000000000000000000000000;hb=87defde679eb7f7eb6d8f7203472a6f6a8ab2966;hpb=67928fe38836205ca8d0705b3695186e998e3e29

diff --git a/Arithmetic/arithprov.ml b/Arithmetic/arithprov.ml
new file mode 100644
index 0000000..ab308ff
--- /dev/null
+++ b/Arithmetic/arithprov.ml
@@ -0,0 +1,570 @@
+(* ========================================================================= *)
+(* Proof that provability is definable; weak form of Godel's theorem.        *)
+(* ========================================================================= *)
+
+prioritize_num();;
+
+(* ------------------------------------------------------------------------- *)
+(* Auxiliary predicate: all numbers in an iterated-pair "list".              *)
+(* ------------------------------------------------------------------------- *)
+
+let ALLN_DEF =
+  let th = prove
+   (`!P. ?ALLN. !z.
+         ALLN z <=>
+                if ?x y. z = NPAIR x y
+                then P (@x. ?y. NPAIR x y = z) /\
+                     ALLN (@y. ?x. NPAIR x y = z)
+                else T`,
+    GEN_TAC THEN MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN
+    REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
+    BINOP_TAC THENL [ALL_TAC; FIRST_ASSUM MATCH_MP_TAC] THEN
+    FIRST_ASSUM(REPEAT_TCL CHOOSE_THEN SUBST1_TAC) THEN
+    REWRITE_TAC[NPAIR_INJ; RIGHT_EXISTS_AND_THM; EXISTS_REFL;
+                SELECT_REFL; NPAIR_LT; LEFT_EXISTS_AND_THM]) in
+  new_specification ["ALLN"] (REWRITE_RULE[SKOLEM_THM] th);;
+
+let ALLN = prove
+ (`(ALLN P 0 <=> T) /\
+   (ALLN P (NPAIR x y) <=> P x /\ ALLN P y)`,
+  REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [ALLN_DEF] THEN
+  REWRITE_TAC[NPAIR_NONZERO] THEN
+  REWRITE_TAC[NPAIR_INJ; LEFT_EXISTS_AND_THM; RIGHT_EXISTS_AND_THM] THEN
+  REWRITE_TAC[EXISTS_REFL; GSYM EXISTS_REFL]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Valid term.                                                               *)
+(* ------------------------------------------------------------------------- *)
+
+let TERM1 = new_definition
+  `TERM1 x y <=>
+        (?l u. (x = l) /\ (y = NPAIR (NPAIR 0 u) l)) \/
+        (?l. (x = l) /\ (y = NPAIR (NPAIR 1 0) l)) \/
+        (?t l. (x = NPAIR t l) /\ (y = NPAIR (NPAIR 2 t) l)) \/
+        (?n s t l. ((n = 3) \/ (n = 4)) /\
+                   (x = NPAIR s (NPAIR t l)) /\
+                   (y = NPAIR (NPAIR n (NPAIR s t)) l))`;;
+
+let TERM = new_definition
+  `TERM n <=> RTC TERM1 0 (NPAIR n 0)`;;
+
+let isagterm = new_definition
+  `isagterm n <=> ?t. n = gterm t`;;
+
+let TERM_LEMMA1 = prove
+ (`!x y. TERM1 x y ==> ALLN isagterm x ==> ALLN isagterm y`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[TERM1] THEN
+  REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+  SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN; isagterm] THEN
+  MESON_TAC[gterm; NUMBER_SURJ]);;
+
+let TERM_LEMMA2 = prove
+ (`!t a. RTC TERM1 a (NPAIR (gterm t) a)`,
+  MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[gterm] THEN
+  MESON_TAC[RTC_INC; RTC_TRANS; TERM1]);;
+
+let TERM_THM = prove
+ (`!n. TERM n <=> ?t. n = gterm t`,
+  GEN_TAC THEN REWRITE_TAC[TERM] THEN EQ_TAC THENL
+   [ALL_TAC; MESON_TAC[TERM_LEMMA2]] THEN
+  SUBGOAL_THEN `!x y. RTC TERM1 x y ==> ALLN isagterm x ==> ALLN isagterm y`
+   (fun th -> MESON_TAC[ALLN; isagterm; th]) THEN
+  MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[TERM_LEMMA1] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Valid formula.                                                            *)
+(* ------------------------------------------------------------------------- *)
+
+let FORM1 = new_definition
+  `FORM1 x y <=>
+        (?l. (x = l) /\ (y = NPAIR (NPAIR 0 0) l)) \/
+        (?l. (x = l) /\ (y = NPAIR (NPAIR 0 1) l)) \/
+        (?n s t l. ((n = 1) \/ (n = 2) \/ (n = 3)) /\
+                   TERM s /\ TERM t /\
+                   (x = l) /\
+                   (y = NPAIR (NPAIR n (NPAIR s t)) l)) \/
+        (?p l. (x = NPAIR p l) /\
+               (y = NPAIR (NPAIR 4 p) l)) \/
+        (?n p q l. ((n = 5) \/ (n = 6) \/ (n = 7) \/ (n = 8)) /\
+                   (x = NPAIR p (NPAIR q l)) /\
+                   (y = NPAIR (NPAIR n (NPAIR p q)) l)) \/
+        (?n u p l. ((n = 9) \/ (n = 10)) /\
+                   (x = NPAIR p l) /\
+                   (y = NPAIR (NPAIR n (NPAIR u p)) l))`;;
+
+let FORM = new_definition
+  `FORM n <=> RTC FORM1 0 (NPAIR n 0)`;;
+
+let isagform = new_definition
+  `isagform n <=> ?t. n = gform t`;;
+
+let FORM_LEMMA1 = prove
+ (`!x y. FORM1 x y ==> ALLN isagform x ==> ALLN isagform y`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[FORM1] THEN
+  REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+  SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN; isagform] THEN
+  MESON_TAC[gform; TERM_THM; NUMBER_SURJ]);;
+
+(*** Following really blows up if we just use FORM1
+ *** instead of manually breaking up the conjuncts
+ ***)
+
+let FORM_LEMMA2 = prove
+ (`!p a. RTC FORM1 a (NPAIR (gform p) a)`,
+  MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[gform] THEN
+  REPEAT CONJ_TAC THEN
+  MESON_TAC[RTC_INC; RTC_TRANS; TERM_THM;
+     REWRITE_RULE[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`]
+                 (snd(EQ_IMP_RULE (SPEC_ALL FORM1)))]);;
+
+let FORM_THM = prove
+ (`!n. FORM n <=> ?p. n = gform p`,
+  GEN_TAC THEN REWRITE_TAC[FORM] THEN EQ_TAC THENL
+   [ALL_TAC; MESON_TAC[FORM_LEMMA2]] THEN
+  SUBGOAL_THEN `!x y. RTC FORM1 x y ==> ALLN isagform x ==> ALLN isagform y`
+   (fun th -> MESON_TAC[ALLN; isagform; th]) THEN
+  MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FORM_LEMMA1] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Term without particular variable.                                         *)
+(* ------------------------------------------------------------------------- *)
+
+let FREETERM1 = new_definition
+  `FREETERM1 m x y <=>
+        (?l u. ~(u = m) /\ (x = l) /\ (y = NPAIR (NPAIR 0 u) l)) \/
+        (?l. (x = l) /\ (y = NPAIR (NPAIR 1 0) l)) \/
+        (?t l. (x = NPAIR t l) /\ (y = NPAIR (NPAIR 2 t) l)) \/
+        (?n s t l. ((n = 3) \/ (n = 4)) /\
+                   (x = NPAIR s (NPAIR t l)) /\
+                   (y = NPAIR (NPAIR n (NPAIR s t)) l))`;;
+
+let FREETERM = new_definition
+  `FREETERM m n <=> RTC (FREETERM1 m) 0 (NPAIR n 0)`;;
+
+let isafterm = new_definition
+  `isafterm m n <=> ?t. ~(m IN IMAGE number (FVT t)) /\ (n = gterm t)`;;
+
+let ISAFTERM = prove
+ (`(~(number x = m) ==> isafterm m (NPAIR 0 (number x))) /\
+   isafterm m (NPAIR 1 0) /\
+   (isafterm m t ==> isafterm m (NPAIR 2 t)) /\
+   (isafterm m s /\ isafterm m t ==> isafterm m (NPAIR 3 (NPAIR s t))) /\
+   (isafterm m s /\ isafterm m t ==> isafterm m (NPAIR 4 (NPAIR s t)))`,
+  REWRITE_TAC[isafterm; gterm] THEN REPEAT CONJ_TAC THENL
+   [DISCH_TAC THEN EXISTS_TAC `V x`;
+    EXISTS_TAC `Z`;
+    DISCH_THEN(X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC) THEN
+    EXISTS_TAC `Suc t`;
+    DISCH_THEN(CONJUNCTS_THEN2
+     (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
+     (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC)) THEN
+    EXISTS_TAC `s ++ t`;
+    DISCH_THEN(CONJUNCTS_THEN2
+     (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
+     (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC)) THEN
+    EXISTS_TAC `s ** t`] THEN
+  ASM_REWRITE_TAC[gterm; FVT; IMAGE_UNION; NOT_IN_EMPTY; IN_SING; IN_UNION;
+                  IMAGE_CLAUSES]);;
+
+let FREETERM_LEMMA1 = prove
+ (`!m x y. FREETERM1 m x y ==> ALLN (isafterm m) x ==> ALLN (isafterm m) y`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[FREETERM1] THEN
+  REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+  SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
+  MESON_TAC[ISAFTERM; NUMBER_SURJ]);;
+
+let FREETERM_LEMMA2 = prove
+ (`!m t a. ~(m IN IMAGE number (FVT t))
+           ==> RTC (FREETERM1 m) a (NPAIR (gterm t) a)`,
+  GEN_TAC THEN MATCH_MP_TAC term_INDUCT THEN
+  REWRITE_TAC[gterm; FVT; NOT_IN_EMPTY; IN_SING; IN_UNION;
+              IMAGE_CLAUSES; IMAGE_UNION] THEN
+  REWRITE_TAC[DE_MORGAN_THM] THEN
+  REPEAT CONJ_TAC THEN
+  TRY(REPEAT GEN_TAC THEN DISCH_THEN
+   (fun th -> GEN_TAC THEN STRIP_TAC THEN MP_TAC th)) THEN
+  ASM_REWRITE_TAC[] THEN
+  MESON_TAC[RTC_INC; RTC_TRANS; FREETERM1]);;
+
+let FREETERM_THM = prove
+ (`!m n. FREETERM m n <=> ?t. ~(m IN IMAGE number (FVT(t))) /\ (n = gterm t)`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[FREETERM] THEN EQ_TAC THENL
+   [ALL_TAC; MESON_TAC[FREETERM_LEMMA2]] THEN
+  SUBGOAL_THEN `!x y. RTC (FREETERM1 m) x y
+                      ==> ALLN (isafterm m) x ==> ALLN (isafterm m) y`
+   (fun th -> MESON_TAC[ALLN; isagterm; isafterm; th]) THEN
+  MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FREETERM_LEMMA1] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Formula without particular free variable.                                 *)
+(* ------------------------------------------------------------------------- *)
+
+let FREEFORM1 = new_definition
+  `FREEFORM1 m x y <=>
+        (?l. (x = l) /\ (y = NPAIR (NPAIR 0 0) l)) \/
+        (?l. (x = l) /\ (y = NPAIR (NPAIR 0 1) l)) \/
+        (?n s t l. ((n = 1) \/ (n = 2) \/ (n = 3)) /\
+                   FREETERM m s /\ FREETERM m t /\
+                   (x = l) /\
+                   (y = NPAIR (NPAIR n (NPAIR s t)) l)) \/
+        (?p l. (x = NPAIR p l) /\
+               (y = NPAIR (NPAIR 4 p) l)) \/
+        (?n p q l. ((n = 5) \/ (n = 6) \/ (n = 7) \/ (n = 8)) /\
+                   (x = NPAIR p (NPAIR q l)) /\
+                   (y = NPAIR (NPAIR n (NPAIR p q)) l)) \/
+        (?n u p l. ((n = 9) \/ (n = 10)) /\
+                   (x = NPAIR p l) /\
+                   (y = NPAIR (NPAIR n (NPAIR u p)) l)) \/
+        (?n p l. ((n = 9) \/ (n = 10)) /\
+                 (x = l) /\ FORM p /\
+                 (y = NPAIR (NPAIR n (NPAIR m p)) l))`;;
+
+let FREEFORM = new_definition
+  `FREEFORM m n <=> RTC (FREEFORM1 m) 0 (NPAIR n 0)`;;
+
+let isafform = new_definition
+  `isafform m n <=> ?p. ~(m IN IMAGE number (FV p)) /\ (n = gform p)`;;
+
+let ISAFFORM = prove
+ (`isafform m (NPAIR 0 0) /\
+   isafform m (NPAIR 0 1) /\
+   (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 1 (NPAIR s t))) /\
+   (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 2 (NPAIR s t))) /\
+   (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 3 (NPAIR s t))) /\
+   (isafform m p ==> isafform m (NPAIR 4 p)) /\
+   (isafform m p /\ isafform m q ==> isafform m (NPAIR 5 (NPAIR p q))) /\
+   (isafform m p /\ isafform m q ==> isafform m (NPAIR 6 (NPAIR p q))) /\
+   (isafform m p /\ isafform m q ==> isafform m (NPAIR 7 (NPAIR p q))) /\
+   (isafform m p /\ isafform m q ==> isafform m (NPAIR 8 (NPAIR p q))) /\
+   (isafform m p ==> isafform m (NPAIR 9 (NPAIR x p))) /\
+   (isafform m p ==> isafform m (NPAIR 10 (NPAIR x p))) /\
+   (isagform p ==> isafform m (NPAIR 9 (NPAIR m p))) /\
+   (isagform p ==> isafform m (NPAIR 10 (NPAIR m p)))`,
+  let tac0 = DISCH_THEN(X_CHOOSE_THEN `p:form` STRIP_ASSUME_TAC)
+  and  tac1 =
+    DISCH_THEN(CONJUNCTS_THEN2
+     (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
+     (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC))
+  and tac2 =
+    DISCH_THEN(CONJUNCTS_THEN2
+     (X_CHOOSE_THEN `p:form` STRIP_ASSUME_TAC)
+     (X_CHOOSE_THEN `q:form` STRIP_ASSUME_TAC)) in
+  REWRITE_TAC[isafform; gform; isagform; isafterm] THEN REPEAT CONJ_TAC THENL
+   [EXISTS_TAC `False`;
+    EXISTS_TAC `True`;
+    tac1 THEN EXISTS_TAC `s === t`;
+    tac1 THEN EXISTS_TAC `s << t`;
+    tac1 THEN EXISTS_TAC `s <<= t`;
+    tac0 THEN EXISTS_TAC `Not p`;
+    tac2 THEN EXISTS_TAC `p && q`;
+    tac2 THEN EXISTS_TAC `p || q`;
+    tac2 THEN EXISTS_TAC `p --> q`;
+    tac2 THEN EXISTS_TAC `p <-> q`;
+    tac0 THEN EXISTS_TAC `!!(denumber x) p`;
+    tac0 THEN EXISTS_TAC `??(denumber x) p`;
+    tac0 THEN EXISTS_TAC `!!(denumber m) p`;
+    tac0 THEN EXISTS_TAC `??(denumber m) p`] THEN
+  ASM_REWRITE_TAC[FV; IN_DELETE; NOT_IN_EMPTY; IN_SING; IN_UNION; gform;
+                  NUMBER_DENUMBER; IMAGE_CLAUSES; IMAGE_UNION] THEN
+  ASM SET_TAC[NUMBER_DENUMBER]);;
+
+let FREEFORM_LEMMA1 = prove
+ (`!x y. FREEFORM1 m x y ==> ALLN (isafform m) x ==> ALLN (isafform m) y`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[FREEFORM1] THEN
+  REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+  SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
+  REWRITE_TAC[FREETERM_THM; GSYM isafterm] THEN
+  REWRITE_TAC[FORM_THM; GSYM isagform] THEN MESON_TAC[ISAFFORM]);;
+
+let FREEFORM_LEMMA2 = prove
+ (`!m p a. ~(m IN IMAGE number (FV p))
+           ==> RTC (FREEFORM1 m) a (NPAIR (gform p) a)`,
+  let lemma = prove
+   (`m IN IMAGE number (s DELETE k) <=>
+     m IN IMAGE number s /\ ~(m = number k)`,
+    SET_TAC[NUMBER_INJ]) in
+  GEN_TAC THEN MATCH_MP_TAC form_INDUCT THEN
+  REWRITE_TAC[gform; FV; NOT_IN_EMPTY; IN_DELETE; IN_SING; IN_UNION;
+              lemma; IMAGE_UNION; IMAGE_CLAUSES] THEN
+  REWRITE_TAC[DE_MORGAN_THM] THEN
+  REPEAT CONJ_TAC THEN
+  TRY(REPEAT GEN_TAC THEN DISCH_THEN
+   (fun th -> GEN_TAC THEN STRIP_TAC THEN MP_TAC th)) THEN
+  ASM_REWRITE_TAC[] THEN
+  MESON_TAC[RTC_INC; RTC_TRANS; FORM_THM;
+        REWRITE_RULE[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`;
+                     FREETERM_THM]
+                 (snd(EQ_IMP_RULE (SPEC_ALL FREEFORM1)))]);;
+
+let FREEFORM_THM = prove
+ (`!m n. FREEFORM m n <=> ?p. ~(m IN IMAGE number (FV p)) /\ (n = gform p)`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[FREEFORM] THEN EQ_TAC THENL
+   [ALL_TAC; MESON_TAC[FREEFORM_LEMMA2]] THEN
+  SUBGOAL_THEN `!x y. RTC (FREEFORM1 m) x y
+                      ==> ALLN (isafform m) x ==> ALLN (isafform m) y`
+   (fun th -> MESON_TAC[ALLN; isagform; isafform; th]) THEN
+  MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FREEFORM_LEMMA1] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Arithmetization of logical axioms --- autogenerated.                      *)
+(* ------------------------------------------------------------------------- *)
+
+let AXIOM,AXIOM_THM =
+  let th0 = prove
+   (`((?x p. P (number x) (gform p) /\ ~(x IN FV(p))) <=> 
+      (?x p. FREEFORM x p /\ P x p)) /\
+     ((?x t. P (number x) (gterm t) /\ ~(x IN FVT(t))) <=>
+      (?x t. FREETERM x t /\ P x t))`,
+    REWRITE_TAC[FREETERM_THM; FREEFORM_THM] THEN CONJ_TAC THEN 
+    REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN        
+    ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN         
+    GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV) [SWAP_EXISTS_THM] THEN
+    REWRITE_TAC[UNWIND_THM2; IN_IMAGE] THEN 
+    ASM_MESON_TAC[IN_IMAGE; NUMBER_DENUMBER]) 
+  and th1 = prove
+   (`((?p. P(gform p)) <=> (?p. FORM(p) /\ P p)) /\
+     ((?t. P(gterm t)) <=> (?t. TERM(t) /\ P t))`,
+    MESON_TAC[FORM_THM; TERM_THM])
+  and th2 = prove
+   (`(?x. P(number x)) <=> (?x. P x)`,
+    MESON_TAC[NUMBER_DENUMBER]) in
+  let th = (REWRITE_CONV[GSYM GFORM_INJ] THENC
+          REWRITE_CONV[gform; gterm] THENC
+          REWRITE_CONV[th0] THENC REWRITE_CONV[th1] THENC  
+          REWRITE_CONV[th2] THENC
+          REWRITE_CONV[RIGHT_AND_EXISTS_THM])
+         (rhs(concl(SPEC `a:form` axiom_CASES))) in
+  let dtm = mk_eq(`(AXIOM:num->bool) a`,
+                   subst [`a:num`,`gform a`] (rhs(concl th))) in
+  let AXIOM = new_definition dtm in
+  let AXIOM_THM = prove
+   (`!p. AXIOM(gform p) <=> axiom p`,
+    REWRITE_TAC[axiom_CASES; AXIOM; th]) in
+  AXIOM,AXIOM_THM;;
+
+(* ------------------------------------------------------------------------- *)
+(* Prove also that all AXIOMs are in fact numbers of formulas.               *)
+(* ------------------------------------------------------------------------- *)
+
+let GTERM_CASES_ALT = prove
+ (`(gterm u = NPAIR 0 x <=> u = V(denumber x))`,
+  REWRITE_TAC[GSYM GTERM_CASES; NUMBER_DENUMBER]);;
+
+let GFORM_CASES_ALT = prove
+ (`(gform r = NPAIR 9 (NPAIR x n) <=>
+    (?p. r = !!(denumber x) p /\ gform p = n)) /\
+   (gform r = NPAIR 10 (NPAIR x n) <=>
+    (?p. r = ??(denumber x) p /\ gform p = n))`,
+  REWRITE_TAC[GSYM GFORM_CASES; NUMBER_DENUMBER]);;
+
+let AXIOM_FORMULA = prove
+ (`!a. AXIOM a ==> ?p. a = gform p`,
+  REWRITE_TAC[AXIOM; FREEFORM_THM; FREETERM_THM; FORM_THM; TERM_THM] THEN
+  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
+  CONV_TAC(BINDER_CONV SYM_CONV) THEN
+  REWRITE_TAC[GFORM_CASES; GTERM_CASES; 
+              GTERM_CASES_ALT; GFORM_CASES_ALT] THEN
+  MESON_TAC[NUMBER_DENUMBER]);;
+
+let AXIOM_THM_STRONG = prove
+ (`!a. AXIOM a <=> ?p. axiom p /\ (a = gform p)`,
+  MESON_TAC[AXIOM_THM; AXIOM_FORMULA]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Arithmetization of the full logical inference rules.                      *)
+(* ------------------------------------------------------------------------- *)
+
+let PROV1 = new_definition
+  `PROV1 A x y <=>
+        (?a. (AXIOM a \/ a IN A) /\ (y = NPAIR a x)) \/
+        (?p q l. (x = NPAIR (NPAIR 7 (NPAIR p q)) (NPAIR p l)) /\
+                 (y = NPAIR q l)) \/
+        (?p u l. (x = NPAIR p l) /\ (y = NPAIR (NPAIR 9 (NPAIR u p)) l))`;;
+
+let PROV = new_definition
+  `PROV A n <=> RTC (PROV1 A) 0 (NPAIR n 0)`;;
+
+let isaprove = new_definition
+  `isaprove A n <=> ?p. (gform p = n) /\ A |-- p`;;
+
+let PROV_LEMMA1 = prove
+ (`!A p q. PROV1 (IMAGE gform A) x y
+           ==> ALLN (isaprove A) x ==> ALLN (isaprove A) y`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[PROV1] THEN
+  REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
+  SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
+  REWRITE_TAC[isaprove] THEN REPEAT CONJ_TAC THEN
+  REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
+   [ASM_MESON_TAC[AXIOM_THM_STRONG; proves_RULES];
+    ASM_MESON_TAC[IN_IMAGE; GFORM_INJ; proves_RULES; gform];
+    ALL_TAC;
+    ASM_MESON_TAC[NUMBER_DENUMBER;
+                  IN_IMAGE; GFORM_INJ; proves_RULES; gform]] THEN
+  REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
+  ONCE_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
+  MATCH_MP_TAC form_INDUCT THEN
+  REWRITE_TAC[gform; NPAIR_INJ; ARITH_EQ] THEN
+  MAP_EVERY X_GEN_TAC [`P:form`; `Q:form`] THEN
+  DISCH_THEN(K ALL_TAC) THEN
+  DISCH_THEN(CONJUNCTS_THEN2 (STRIP_ASSUME_TAC o GSYM) MP_TAC) THEN
+  ASM_REWRITE_TAC[GFORM_INJ] THEN
+  REWRITE_TAC[GSYM CONJ_ASSOC; UNWIND_THM2] THEN
+  ASM_MESON_TAC[proves_RULES]);;
+
+let PROV_LEMMA2 = prove
+ (`!A p. A |-- p ==> !a. RTC (PROV1 (IMAGE gform A)) a (NPAIR (gform p) a)`,
+  GEN_TAC THEN MATCH_MP_TAC proves_INDUCT THEN REWRITE_TAC[gform] THEN
+  MESON_TAC[RTC_INC; RTC_TRANS; PROV1; IN_IMAGE; AXIOM_THM]);;
+
+let PROV_THM_STRONG = prove
+ (`!A n. PROV (IMAGE gform A) n <=> ?p. A |-- p /\ (gform p = n)`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[PROV] THEN EQ_TAC THENL
+   [ALL_TAC; MESON_TAC[PROV_LEMMA2]] THEN
+  SUBGOAL_THEN
+   `!x y. RTC (PROV1 (IMAGE gform A)) x y
+           ==> ALLN (isaprove A) x ==> ALLN (isaprove A) y`
+   (fun th -> MESON_TAC[ALLN; isaprove; GFORM_INJ; th]) THEN
+  MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[PROV_LEMMA1] THEN MESON_TAC[]);;
+
+let PROV_THM = prove
+ (`!A p. PROV (IMAGE gform A) (gform p) <=> A |-- p`,
+  MESON_TAC[PROV_THM_STRONG; GFORM_INJ]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Now really objectify all that.                                            *)
+(* ------------------------------------------------------------------------- *)
+
+let arith_term1,ARITH_TERM1 = OBJECTIFY [] "arith_term1" TERM1;;
+
+let FV_TERM1 = prove
+ (`!s t. FV(arith_term1 s t) = (FVT s) UNION (FVT t)`,
+  FV_TAC[arith_term1; FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_term,ARITH_TERM = OBJECTIFY_RTC ARITH_TERM1 "arith_term" TERM;;
+
+let FV_TERM = prove
+ (`!t. FV(arith_term t) = FVT t`,
+  FV_TAC[arith_term; FV_RTC; FV_TERM1; FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_form1,ARITH_FORM1 =
+ OBJECTIFY [ARITH_TERM] "arith_form1" FORM1;;
+
+let FV_FORM1 = prove
+ (`!s t. FV(arith_form1 s t) = (FVT s) UNION (FVT t)`,
+  FV_TAC[arith_form1; FV_TERM; FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_form,ARITH_FORM = OBJECTIFY_RTC ARITH_FORM1 "arith_form" FORM;;
+
+let FV_FORM = prove
+ (`!t. FV(arith_form t) = FVT t`,
+  FV_TAC[arith_form; FV_RTC; FV_FORM1; FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_freeterm1,ARITH_FREETERM1 =
+ OBJECTIFY [] "arith_freeterm1" FREETERM1;;
+
+let FV_FREETERM1 = prove
+ (`!s t u. FV(arith_freeterm1 s t u) = (FVT s) UNION (FVT t) UNION (FVT u)`,
+  FV_TAC[arith_freeterm1; FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_freeterm,ARITH_FREETERM =
+  OBJECTIFY_RTCP ARITH_FREETERM1 "arith_freeterm" FREETERM;;
+
+let FV_FREETERM = prove
+ (`!s t. FV(arith_freeterm s t) = (FVT s) UNION (FVT t)`,
+  FV_TAC[arith_freeterm; FV_RTCP; FV_FREETERM1; FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_freeform1,ARITH_FREEFORM1 =
+ OBJECTIFY [ARITH_FREETERM; ARITH_FORM] "arith_freeform1" FREEFORM1;;
+
+let FV_FREEFORM1 = prove
+ (`!s t u. FV(arith_freeform1 s t u) = (FVT s) UNION (FVT t) UNION (FVT u)`,
+  FV_TAC[arith_freeform1; FV_FREETERM; FV_FORM; FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_freeform,ARITH_FREEFORM =
+ OBJECTIFY_RTCP ARITH_FREEFORM1 "arith_freeform" FREEFORM;;
+
+let FV_FREEFORM = prove
+ (`!s t. FV(arith_freeform s t) = (FVT s) UNION (FVT t)`,
+  FV_TAC[arith_freeform; FV_RTCP; FV_FREEFORM1; FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_axiom,ARITH_AXIOM =
+ OBJECTIFY [ARITH_FORM; ARITH_FREEFORM; ARITH_FREETERM; ARITH_TERM]
+           "arith_axiom" AXIOM;;
+
+let FV_AXIOM = prove
+ (`!t. FV(arith_axiom t) = FVT t`,
+  FV_TAC[arith_axiom; FV_FREETERM; FV_FREEFORM; FV_TERM; FV_FORM;
+         FVT_PAIR; FVT_NUMERAL]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Parametrization by A means it's easier to do these cases manually.        *)
+(* ------------------------------------------------------------------------- *)
+
+let arith_prov1,ARITH_PROV1 =
+  let PROV1' = REWRITE_RULE[IN] PROV1 in
+ OBJECTIFY [ASSUME `!v n. holds v (A n) <=> Ax (termval v n)`; ARITH_AXIOM]
+   "arith_prov1" PROV1';;
+
+let ARITH_PROV1 = prove
+ (`(!v t. holds v (A t) <=> Ax(termval v t))
+   ==> (!v s t.
+             holds v (arith_prov1 A s t) <=>
+             PROV1 Ax (termval v s) (termval v t))`,
+  REWRITE_TAC[arith_prov1; holds; HOLDS_FORMSUBST] THEN
+  REPEAT STRIP_TAC THEN
+  ASM_REWRITE_TAC[termval; valmod; o_THM; ARITH_EQ; ARITH_PAIR;
+                  TERMVAL_NUMERAL; ARITH_AXIOM] THEN
+  REWRITE_TAC[PROV1; IN]);;
+
+let FV_PROV1 = prove
+ (`(!t. FV(A t) = FVT t) ==> !s t. FV(arith_prov1 A s t) = FVT(s) UNION FVT(t)`,
+  FV_TAC[arith_prov1; FV_AXIOM; FVT_NUMERAL; FVT_PAIR]);;
+
+let arith_prov = new_definition
+ `arith_prov A n =
+    formsubst ((0 |-> n) V)
+        (arith_rtc (arith_prov1 A) (numeral 0)
+                   (arith_pair (V 0) (numeral 0)))`;;
+
+let ARITH_PROV = prove
+ (`!Ax A. (!v t. holds v (A t) <=> Ax(termval v t))
+          ==> !v n. holds v (arith_prov A n) <=> PROV Ax (termval v n)`,
+  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP ARITH_PROV1) THEN
+  DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC) THEN
+  CONV_TAC(TOP_DEPTH_CONV ETA_CONV) THEN DISCH_TAC THEN
+  ASM_REWRITE_TAC[arith_prov; HOLDS_FORMSUBST] THEN
+  REWRITE_TAC[termval; valmod; o_DEF; TERMVAL_NUMERAL; ARITH_PAIR] THEN
+  REWRITE_TAC[PROV]);;
+
+let FV_PROV = prove
+ (`(!t. FV(A t) = FVT t) ==> !t. FV(arith_prov A t) = FVT t`,
+  FV_TAC[arith_prov; FV_PROV1; FV_RTC; FVT_NUMERAL; FVT_PAIR]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Our final conclusion.                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+let PROV_DEFINABLE = prove
+ (`!Ax. definable {gform p | p IN Ax} ==> definable {gform p | Ax |-- p}`,
+  GEN_TAC THEN REWRITE_TAC[definable; IN_ELIM_THM] THEN
+  DISCH_THEN(X_CHOOSE_THEN `A:form` (X_CHOOSE_TAC `x:num`)) THEN
+  MP_TAC(SPECL [`IMAGE gform Ax`; `\t. formsubst ((x |-> t) V) A`]
+               ARITH_PROV) THEN
+  REWRITE_TAC[] THEN ANTS_TAC THENL
+   [ASM_REWRITE_TAC[HOLDS_FORMSUBST] THEN
+    REWRITE_TAC[o_THM; VALMOD_BASIC; IMAGE; IN_ELIM_THM];
+    ALL_TAC] THEN
+  REWRITE_TAC[PROV_THM_STRONG] THEN DISCH_TAC THEN
+  EXISTS_TAC `arith_prov (\t. formsubst ((x |-> t) V) A) (V x)` THEN
+  ASM_REWRITE_TAC[termval] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* The crudest conclusion: truth undefinable, provability not, so:           *)
+(* ------------------------------------------------------------------------- *)
+
+let GODEL_CRUDE = prove
+ (`!Ax. definable {gform p | p IN Ax} ==> ?p. ~(true p <=> Ax |-- p)`,
+  REPEAT STRIP_TAC THEN MP_TAC TARSKI_THEOREM THEN
+  FIRST_X_ASSUM(MP_TAC o MATCH_MP PROV_DEFINABLE) THEN
+  MATCH_MP_TAC(TAUT `(~c ==> (a <=> b)) ==> a ==> ~b ==> c`) THEN
+  SIMP_TAC[NOT_EXISTS_THM]);;