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

diff --git a/Arithmetic/tarski.ml b/Arithmetic/tarski.ml
new file mode 100644
index 0000000..246eb47
--- /dev/null
+++ b/Arithmetic/tarski.ml
@@ -0,0 +1,364 @@
+(* ========================================================================= *)
+(* Arithmetization of syntax and Tarski's theorem.                           *)
+(* ========================================================================= *)
+
+prioritize_num();;
+
+(* ------------------------------------------------------------------------- *)
+(* This is to fake the fact that we might really be using strings.           *)
+(* ------------------------------------------------------------------------- *)
+
+let number = new_definition
+ `number(x) = 2 * (x DIV 2) + (1 - x MOD 2)`;;
+
+let denumber = new_definition
+ `denumber = number`;;
+
+let NUMBER_DENUMBER = prove
+ (`(!s. denumber(number s) = s) /\
+   (!n. number(denumber n) = n)`,
+  REWRITE_TAC[number; denumber] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
+  SIMP_TAC[ARITH_RULE `x < 2 ==> (2 * y + x) DIV 2 = y`;
+           MOD_MULT_ADD; MOD_LT; GSYM DIVISION; ARITH_EQ;
+           ARITH_RULE `1 - m < 2`; ARITH_RULE `x < 2 ==> 1 - (1 - x) = x`]);;
+
+let NUMBER_INJ = prove
+ (`!x y. number(x) = number(y) <=> x = y`,
+  MESON_TAC[NUMBER_DENUMBER]);;
+
+let NUMBER_SURJ = prove
+ (`!y. ?x. number(x) = y`,
+  MESON_TAC[NUMBER_DENUMBER]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Arithmetization.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+let gterm = new_recursive_definition term_RECURSION
+  `(gterm (V x) = NPAIR 0 (number x)) /\
+   (gterm Z = NPAIR 1 0) /\
+   (gterm (Suc t) = NPAIR 2 (gterm t)) /\
+   (gterm (s ++ t) = NPAIR 3 (NPAIR (gterm s) (gterm t))) /\
+   (gterm (s ** t) = NPAIR 4 (NPAIR (gterm s) (gterm t)))`;;
+
+let gform = new_recursive_definition form_RECURSION
+  `(gform False = NPAIR 0 0) /\
+   (gform True = NPAIR 0 1) /\
+   (gform (s === t) = NPAIR 1 (NPAIR (gterm s) (gterm t))) /\
+   (gform (s << t) = NPAIR 2 (NPAIR (gterm s) (gterm t))) /\
+   (gform (s <<= t) = NPAIR 3 (NPAIR (gterm s) (gterm t))) /\
+   (gform (Not p) = NPAIR 4 (gform p)) /\
+   (gform (p && q) = NPAIR 5 (NPAIR (gform p) (gform q))) /\
+   (gform (p || q) = NPAIR 6 (NPAIR (gform p) (gform q))) /\
+   (gform (p --> q) = NPAIR 7 (NPAIR (gform p) (gform q))) /\
+   (gform (p <-> q) = NPAIR 8 (NPAIR (gform p) (gform q))) /\
+   (gform (!! x p) = NPAIR 9 (NPAIR (number x) (gform p))) /\
+   (gform (?? x p) = NPAIR 10 (NPAIR (number x) (gform p)))`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Injectivity.                                                              *)
+(* ------------------------------------------------------------------------- *)
+
+let GTERM_INJ = prove
+ (`!s t. (gterm s = gterm t) <=> (s = t)`,
+  MATCH_MP_TAC term_INDUCT THEN REPEAT CONJ_TAC THENL
+   [ALL_TAC;
+    GEN_TAC;
+    GEN_TAC THEN DISCH_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC] THEN
+  MATCH_MP_TAC term_INDUCT THEN
+  ASM_REWRITE_TAC[term_DISTINCT; term_INJ; gterm;
+                  NPAIR_INJ; NUMBER_INJ; ARITH_EQ]);;
+
+let GFORM_INJ = prove
+ (`!p q. (gform p = gform q) <=> (p = q)`,
+  MATCH_MP_TAC form_INDUCT THEN REPEAT CONJ_TAC THENL
+   [ALL_TAC;
+    ALL_TAC;
+    GEN_TAC THEN GEN_TAC;
+    GEN_TAC THEN GEN_TAC;
+    GEN_TAC THEN GEN_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC;
+    REPEAT GEN_TAC THEN STRIP_TAC] THEN
+  MATCH_MP_TAC form_INDUCT THEN
+  ASM_REWRITE_TAC[form_DISTINCT; form_INJ; gform; NPAIR_INJ; ARITH_EQ] THEN
+  REWRITE_TAC[GTERM_INJ; NUMBER_INJ]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Useful case theorems.                                                     *)
+(* ------------------------------------------------------------------------- *)
+
+let GTERM_CASES = prove
+ (`((gterm u = NPAIR 0 (number x)) <=> (u = V x)) /\
+   ((gterm u = NPAIR 1 0) <=> (u = Z)) /\
+   ((gterm u = NPAIR 2 n) <=> (?t. (u = Suc t) /\ (gterm t = n))) /\
+   ((gterm u = NPAIR 3 (NPAIR m n)) <=>
+          (?s t. (u = s ++ t) /\ (gterm s = m) /\ (gterm t = n))) /\
+   ((gterm u = NPAIR 4 (NPAIR m n)) <=>
+          (?s t. (u = s ** t) /\ (gterm s = m) /\ (gterm t = n)))`,
+  STRUCT_CASES_TAC(SPEC `u:term` term_CASES) THEN
+  ASM_REWRITE_TAC[gterm; NPAIR_INJ; ARITH_EQ; NUMBER_INJ;
+                  term_DISTINCT; term_INJ] THEN
+  MESON_TAC[]);;
+
+let GFORM_CASES = prove
+ (`((gform r = NPAIR 0 0) <=> (r = False)) /\
+   ((gform r = NPAIR 0 1) <=> (r = True)) /\
+   ((gform r = NPAIR 1 (NPAIR m n)) <=>
+        (?s t. (r = s === t) /\ (gterm s = m) /\ (gterm t = n))) /\
+   ((gform r = NPAIR 2 (NPAIR m n)) <=>
+        (?s t. (r = s << t) /\ (gterm s = m) /\ (gterm t = n))) /\
+   ((gform r = NPAIR 3 (NPAIR m n)) <=>
+        (?s t. (r = s <<= t) /\ (gterm s = m) /\ (gterm t = n))) /\
+   ((gform r = NPAIR 4 n) = (?p. (r = Not p) /\ (gform p = n))) /\
+   ((gform r = NPAIR 5 (NPAIR m n)) <=>
+        (?p q. (r = p && q) /\ (gform p = m) /\ (gform q = n))) /\
+   ((gform r = NPAIR 6 (NPAIR m n)) <=>
+        (?p q. (r = p || q) /\ (gform p = m) /\ (gform q = n))) /\
+   ((gform r = NPAIR 7 (NPAIR m n)) <=>
+        (?p q. (r = p --> q) /\ (gform p = m) /\ (gform q = n))) /\
+   ((gform r = NPAIR 8 (NPAIR m n)) <=>
+        (?p q. (r = p <-> q) /\ (gform p = m) /\ (gform q = n))) /\
+   ((gform r = NPAIR 9 (NPAIR (number x) n)) <=>
+        (?p. (r = !!x p) /\ (gform p = n))) /\
+   ((gform r = NPAIR 10 (NPAIR (number x) n)) <=>
+        (?p. (r = ??x p) /\ (gform p = n)))`,
+  STRUCT_CASES_TAC(SPEC `r:form` form_CASES) THEN
+  ASM_REWRITE_TAC[gform; NPAIR_INJ; ARITH_EQ; NUMBER_INJ;
+                  form_DISTINCT; form_INJ] THEN
+  MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Definability of "godel number of numeral n".                              *)
+(* ------------------------------------------------------------------------- *)
+
+let gnumeral = new_definition
+  `gnumeral m n = (gterm(numeral m) = n)`;;
+
+let arith_gnumeral1 = new_definition
+ `arith_gnumeral1 a b = formsubst ((3 |-> a) ((4 |-> b) V))
+       (??0 (??1
+       (V 3 === arith_pair (V 0) (V 1) &&
+        V 4 === arith_pair (Suc(V 0)) (arith_pair (numeral 2) (V 1)))))`;;
+
+let ARITH_GNUMERAL1 = prove
+ (`!v a b. holds v (arith_gnumeral1 a b) <=>
+                ?x y. termval v a = NPAIR x y /\
+                      termval v b = NPAIR (SUC x) (NPAIR 2 y)`,
+  REWRITE_TAC[arith_gnumeral1; holds; HOLDS_FORMSUBST] THEN
+  REWRITE_TAC[termval; ARITH_EQ; o_THM; valmod; ARITH_PAIR; TERMVAL_NUMERAL]);;
+
+let FV_GNUMERAL1 = prove
+ (`!s t. FV(arith_gnumeral1 s t) = FVT s UNION FVT t`,
+  REWRITE_TAC[arith_gnumeral1] THEN FV_TAC[FVT_PAIR; FVT_NUMERAL]);;
+
+let arith_gnumeral1' = new_definition
+ `arith_gnumeral1' x y = arith_rtc arith_gnumeral1 x y`;;
+
+let ARITH_GNUMERAL1' = prove
+ (`!v s t. holds v (arith_gnumeral1' s t) <=>
+              RTC (\a b. ?x y. a = NPAIR x y /\
+                               b = NPAIR (SUC x) (NPAIR 2 y))
+                  (termval v s) (termval v t)`,
+  REWRITE_TAC[arith_gnumeral1'] THEN MATCH_MP_TAC ARITH_RTC THEN
+  REWRITE_TAC[ARITH_GNUMERAL1]);;
+
+let FV_GNUMERAL1' = prove
+ (`!s t. FV(arith_gnumeral1' s t) = FVT s UNION FVT t`,
+  SIMP_TAC[arith_gnumeral1'; FV_RTC; FV_GNUMERAL1]);;
+
+let arith_gnumeral = new_definition
+ `arith_gnumeral n p =
+        formsubst ((0 |-> n) ((1 |-> p) V))
+            (arith_gnumeral1' (arith_pair Z (numeral 3))
+                              (arith_pair (V 0) (V 1)))`;;
+
+let ARITH_GNUMERAL = prove
+ (`!v s t. holds v (arith_gnumeral s t) <=>
+            gnumeral (termval v s) (termval v t)`,
+  REWRITE_TAC[arith_gnumeral; holds; HOLDS_FORMSUBST;
+              ARITH_GNUMERAL1'; ARITH_PAIR; TERMVAL_NUMERAL] THEN
+  REWRITE_TAC[termval; ARITH_EQ; o_THM; valmod] THEN
+  MP_TAC(INST
+   [`(gterm o numeral)`,`fn:num->num`;
+    `3`,`e:num`;
+    `\a:num b:num. NPAIR 2 a`,`f:num->num->num`] PRIMREC_SIGMA) THEN
+  ANTS_TAC THENL
+   [REWRITE_TAC[gterm; numeral; o_THM] THEN REWRITE_TAC[NPAIR; ARITH];
+    SIMP_TAC[gnumeral; o_THM]]);;
+
+let FV_GNUMERAL = prove
+ (`!s t. FV(arith_gnumeral s t) =  FVT(s) UNION FVT(t)`,
+  REWRITE_TAC[arith_gnumeral] THEN
+  FV_TAC[FV_GNUMERAL1'; FVT_PAIR; FVT_NUMERAL]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Diagonal substitution.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+let qdiag = new_definition
+  `qdiag x q = qsubst (x,numeral(gform q)) q`;;
+
+let arith_qdiag = new_definition
+  `arith_qdiag x s t =
+        formsubst ((1 |-> s) ((2 |-> t) V))
+        (?? 3
+           (arith_gnumeral (V 1) (V 3) &&
+            arith_pair (numeral 10)  (arith_pair (numeral(number x))
+                                                 (arith_pair (numeral 5)
+              (arith_pair (arith_pair (numeral 1)
+       (arith_pair (arith_pair (numeral 0) (numeral(number x))) (V 3)))
+                   (V 1)))) ===
+        V 2))`;;
+
+let QDIAG_FV = prove
+ (`FV(qdiag x q) = FV(q) DELETE x`,
+  REWRITE_TAC[qdiag; FV_QSUBST; FVT_NUMERAL; UNION_EMPTY]);;
+
+let HOLDS_QDIAG = prove
+ (`!v x q. holds v (qdiag x q) = holds ((x |-> gform q) v) q`,
+  SIMP_TAC[qdiag; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY; TERMVAL_NUMERAL]);;
+
+let ARITH_QDIAG = prove
+ (`(termval v s = gform p)
+   ==> (holds v (arith_qdiag x s t) <=> (termval v t = gform(qdiag x p)))`,
+  REPEAT STRIP_TAC THEN
+  REWRITE_TAC[qdiag; qsubst; arith_qdiag; gform; gterm] THEN
+  ASM_REWRITE_TAC[HOLDS_FORMSUBST; holds; termval; TERMVAL_NUMERAL;
+   gnumeral; ARITH_GNUMERAL; ARITH_PAIR] THEN
+  ASM_REWRITE_TAC[o_DEF; valmod; ARITH_EQ; termval] THEN MESON_TAC[]);;
+
+let FV_QDIAG = prove
+ (`!x s t. FV(arith_qdiag x s t) = FVT(s) UNION FVT(t)`,
+  REWRITE_TAC[arith_qdiag; FORMSUBST_FV; FV; FV_GNUMERAL; FVT_PAIR;
+              UNION_EMPTY; FVT_NUMERAL; FVT; TERMSUBST_FVT] THEN
+  REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
+  REWRITE_TAC[DISJ_ACI; IN_DELETE; IN_UNION; IN_SING] THEN
+  REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
+  REWRITE_TAC[EXISTS_OR_THM; GSYM CONJ_ASSOC; UNWIND_THM2; ARITH_EQ] THEN
+  REWRITE_TAC[valmod; ARITH_EQ; DISJ_ACI]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Hence diagonalization of a predicate.                                     *)
+(* ------------------------------------------------------------------------- *)
+
+let diagonalize = new_definition
+  `diagonalize x q =
+        let y = VARIANT(x INSERT FV(q)) in
+        ??y (arith_qdiag x (V x) (V y) && formsubst ((x |-> V y) V) q)`;;
+
+let FV_DIAGONALIZE = prove
+ (`!x q. FV(diagonalize x q) = x INSERT (FV q)`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[diagonalize] THEN LET_TAC THEN
+  REWRITE_TAC[FV; FV_QDIAG; FORMSUBST_FV; EXTENSION; IN_INSERT; IN_DELETE;
+              IN_UNION; IN_ELIM_THM; FVT; NOT_IN_EMPTY] THEN
+  X_GEN_TAC `u:num` THEN
+  SUBGOAL_THEN `~(y = x) /\ !z. z IN FV(q) ==> ~(y = z)` STRIP_ASSUME_TAC THENL
+   [ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT];
+    ALL_TAC] THEN
+  ASM_CASES_TAC `u:num = x` THEN ASM_REWRITE_TAC[] THEN
+  ASM_CASES_TAC `u:num = y` THEN ASM_REWRITE_TAC[] THEN
+  REWRITE_TAC[valmod; COND_RAND; FVT; IN_SING; COND_EXPAND] THEN
+  ASM_MESON_TAC[]);;
+
+let ARITH_DIAGONALIZE = prove
+ (`(v x = gform p)
+   ==> !q. holds v (diagonalize x q) <=> holds ((x |-> gform(qdiag x p)) v) q`,
+  REPEAT STRIP_TAC THEN REWRITE_TAC[diagonalize] THEN LET_TAC THEN
+  REWRITE_TAC[holds] THEN
+  SUBGOAL_THEN `!a. holds ((y |-> a) v) (arith_qdiag x (V x) (V y)) <=>
+                    (termval ((y |-> a) v) (V y) = gform(qdiag x p))`
+   (fun th -> REWRITE_TAC[th])
+  THENL
+   [GEN_TAC THEN MATCH_MP_TAC ARITH_QDIAG THEN REWRITE_TAC[termval; valmod] THEN
+    SUBGOAL_THEN `~(x:num = y)` (fun th -> ASM_REWRITE_TAC[th]) THEN
+    ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT];
+    ALL_TAC] THEN
+  REWRITE_TAC[HOLDS_FORMSUBST; termval; VALMOD_BASIC; UNWIND_THM2] THEN
+  MATCH_MP_TAC HOLDS_VALUATION THEN
+  X_GEN_TAC `u:num` THEN DISCH_TAC THEN
+  REWRITE_TAC[o_THM; termval; valmod] THEN
+  COND_CASES_TAC THEN REWRITE_TAC[termval] THEN
+  COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
+  ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT]);;
+
+(* ------------------------------------------------------------------------- *)
+(* And hence the fixed point.                                                *)
+(* ------------------------------------------------------------------------- *)
+
+let fixpoint = new_definition
+  `fixpoint x q = qdiag x (diagonalize x q)`;;
+
+let FV_FIXPOINT = prove
+ (`!x p. FV(fixpoint x p) = FV(p) DELETE x`,
+  REWRITE_TAC[fixpoint; FV_QDIAG; QDIAG_FV; FV_DIAGONALIZE;
+              FVT_NUMERAL] THEN
+  SET_TAC[]);;
+
+let HOLDS_FIXPOINT = prove
+ (`!x p v. holds v (fixpoint x p) <=>
+           holds ((x |-> gform(fixpoint x p)) v) p`,
+  REPEAT GEN_TAC THEN SIMP_TAC[fixpoint; holds; HOLDS_QDIAG] THEN
+  SUBGOAL_THEN
+   `((x |-> gform(diagonalize x p)) v) x = gform (diagonalize x p)`
+  MP_TAC THENL [REWRITE_TAC[VALMOD_BASIC]; ALL_TAC] THEN
+  DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP ARITH_DIAGONALIZE th]) THEN
+  REWRITE_TAC[VALMOD_VALMOD_BASIC]);;
+
+let HOLDS_IFF_FIXPOINT = prove
+ (`!x p v. holds v
+        (fixpoint x p <-> qsubst (x,numeral(gform(fixpoint x p))) p)`,
+  SIMP_TAC[holds; HOLDS_FIXPOINT; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY;
+           TERMVAL_NUMERAL]);;
+
+let CARNAP = prove
+ (`!x q. ?p. (FV(p) = FV(q) DELETE x) /\
+             true (p <-> qsubst (x,numeral(gform p)) q)`,
+  REPEAT GEN_TAC THEN EXISTS_TAC `fixpoint x q` THEN
+  REWRITE_TAC[true_def; HOLDS_IFF_FIXPOINT; FV_FIXPOINT]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Hence Tarski's theorem on the undefinability of truth.                    *)
+(* ------------------------------------------------------------------------- *)
+
+let definable_by = new_definition
+  `definable_by P s <=> ?p x. P p /\ (!v. holds v p <=> (v(x)) IN s)`;;
+
+let definable = new_definition
+  `definable s <=> ?p x. !v. holds v p <=> (v(x)) IN s`;;
+
+let TARSKI_THEOREM = prove
+ (`~(definable {gform p | true p})`,
+  REWRITE_TAC[definable; IN_ELIM_THM; NOT_EXISTS_THM] THEN
+  MAP_EVERY X_GEN_TAC [`p:form`; `x:num`] THEN DISCH_TAC THEN
+  MP_TAC(SPECL [`x:num`; `Not p`] CARNAP) THEN
+  DISCH_THEN(X_CHOOSE_THEN `q:form` (MP_TAC o CONJUNCT2)) THEN
+  SIMP_TAC[true_def; holds; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY] THEN
+  ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[VALMOD_BASIC; TERMVAL_NUMERAL] THEN
+  REWRITE_TAC[true_def; GFORM_INJ] THEN MESON_TAC[]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Misc. stuff to sanity-check the book.                                     *)
+(* ------------------------------------------------------------------------- *)
+
+(*****
+let pairpair = new_definition
+ `pair(x,y) = NPAIR x y`;;
+
+let BREAK =
+  rand o concl o (ONCE_REWRITE_CONV[gform; gterm] THENC
+                  REWRITE_CONV[GSYM pairpair]);;
+
+let tm0 = `gform(?? x (V x === k && p))`;;
+let tm1 = BREAK tm0;;
+let tm2 = BREAK tm1;;
+let tm3 = BREAK tm2;;
+let tm4 = BREAK tm3;;
+
+******)