Arithmetic/tarski.ml

   1 (* ========================================================================= *)
   2 (* Arithmetization of syntax and Tarski's theorem.                           *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* This is to fake the fact that we might really be using strings.           *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let number = new_definition
  12  `number(x) = 2 * (x DIV 2) + (1 - x MOD 2)`;;
  13
  14 let denumber = new_definition
  15  `denumber = number`;;
  16
  17 let NUMBER_DENUMBER = prove
  18  (`(!s. denumber(number s) = s) /\
  19    (!n. number(denumber n) = n)`,
  20   REWRITE_TAC[number; denumber] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
  21   SIMP_TAC[ARITH_RULE `x < 2 ==> (2 * y + x) DIV 2 = y`;
  22            MOD_MULT_ADD; MOD_LT; GSYM DIVISION; ARITH_EQ;
  23            ARITH_RULE `1 - m < 2`; ARITH_RULE `x < 2 ==> 1 - (1 - x) = x`]);;
  24
  25 let NUMBER_INJ = prove
  26  (`!x y. number(x) = number(y) <=> x = y`,
  27   MESON_TAC[NUMBER_DENUMBER]);;
  28
  29 let NUMBER_SURJ = prove
  30  (`!y. ?x. number(x) = y`,
  31   MESON_TAC[NUMBER_DENUMBER]);;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Arithmetization.                                                          *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 let gterm = new_recursive_definition term_RECURSION
  38   `(gterm (V x) = NPAIR 0 (number x)) /\
  39    (gterm Z = NPAIR 1 0) /\
  40    (gterm (Suc t) = NPAIR 2 (gterm t)) /\
  41    (gterm (s ++ t) = NPAIR 3 (NPAIR (gterm s) (gterm t))) /\
  42    (gterm (s ** t) = NPAIR 4 (NPAIR (gterm s) (gterm t)))`;;
  43
  44 let gform = new_recursive_definition form_RECURSION
  45   `(gform False = NPAIR 0 0) /\
  46    (gform True = NPAIR 0 1) /\
  47    (gform (s === t) = NPAIR 1 (NPAIR (gterm s) (gterm t))) /\
  48    (gform (s << t) = NPAIR 2 (NPAIR (gterm s) (gterm t))) /\
  49    (gform (s <<= t) = NPAIR 3 (NPAIR (gterm s) (gterm t))) /\
  50    (gform (Not p) = NPAIR 4 (gform p)) /\
  51    (gform (p && q) = NPAIR 5 (NPAIR (gform p) (gform q))) /\
  52    (gform (p || q) = NPAIR 6 (NPAIR (gform p) (gform q))) /\
  53    (gform (p --> q) = NPAIR 7 (NPAIR (gform p) (gform q))) /\
  54    (gform (p <-> q) = NPAIR 8 (NPAIR (gform p) (gform q))) /\
  55    (gform (!! x p) = NPAIR 9 (NPAIR (number x) (gform p))) /\
  56    (gform (?? x p) = NPAIR 10 (NPAIR (number x) (gform p)))`;;
  57
  58 (* ------------------------------------------------------------------------- *)
  59 (* Injectivity.                                                              *)
  60 (* ------------------------------------------------------------------------- *)
  61
  62 let GTERM_INJ = prove
  63  (`!s t. (gterm s = gterm t) <=> (s = t)`,
  64   MATCH_MP_TAC term_INDUCT THEN REPEAT CONJ_TAC THENL
  65    [ALL_TAC;
  66     GEN_TAC;
  67     GEN_TAC THEN DISCH_TAC;
  68     REPEAT GEN_TAC THEN STRIP_TAC;
  69     REPEAT GEN_TAC THEN STRIP_TAC] THEN
  70   MATCH_MP_TAC term_INDUCT THEN
  71   ASM_REWRITE_TAC[term_DISTINCT; term_INJ; gterm;
  72                   NPAIR_INJ; NUMBER_INJ; ARITH_EQ]);;
  73
  74 let GFORM_INJ = prove
  75  (`!p q. (gform p = gform q) <=> (p = q)`,
  76   MATCH_MP_TAC form_INDUCT THEN REPEAT CONJ_TAC THENL
  77    [ALL_TAC;
  78     ALL_TAC;
  79     GEN_TAC THEN GEN_TAC;
  80     GEN_TAC THEN GEN_TAC;
  81     GEN_TAC THEN GEN_TAC;
  82     REPEAT GEN_TAC THEN STRIP_TAC;
  83     REPEAT GEN_TAC THEN STRIP_TAC;
  84     REPEAT GEN_TAC THEN STRIP_TAC;
  85     REPEAT GEN_TAC THEN STRIP_TAC;
  86     REPEAT GEN_TAC THEN STRIP_TAC;
  87     REPEAT GEN_TAC THEN STRIP_TAC;
  88     REPEAT GEN_TAC THEN STRIP_TAC] THEN
  89   MATCH_MP_TAC form_INDUCT THEN
  90   ASM_REWRITE_TAC[form_DISTINCT; form_INJ; gform; NPAIR_INJ; ARITH_EQ] THEN
  91   REWRITE_TAC[GTERM_INJ; NUMBER_INJ]);;
  92
  93 (* ------------------------------------------------------------------------- *)
  94 (* Useful case theorems.                                                     *)
  95 (* ------------------------------------------------------------------------- *)
  96
  97 let GTERM_CASES = prove
  98  (`((gterm u = NPAIR 0 (number x)) <=> (u = V x)) /\
  99    ((gterm u = NPAIR 1 0) <=> (u = Z)) /\
 100    ((gterm u = NPAIR 2 n) <=> (?t. (u = Suc t) /\ (gterm t = n))) /\
 101    ((gterm u = NPAIR 3 (NPAIR m n)) <=>
 102           (?s t. (u = s ++ t) /\ (gterm s = m) /\ (gterm t = n))) /\
 103    ((gterm u = NPAIR 4 (NPAIR m n)) <=>
 104           (?s t. (u = s ** t) /\ (gterm s = m) /\ (gterm t = n)))`,
 105   STRUCT_CASES_TAC(SPEC `u:term` term_CASES) THEN
 106   ASM_REWRITE_TAC[gterm; NPAIR_INJ; ARITH_EQ; NUMBER_INJ;
 107                   term_DISTINCT; term_INJ] THEN
 108   MESON_TAC[]);;
 109
 110 let GFORM_CASES = prove
 111  (`((gform r = NPAIR 0 0) <=> (r = False)) /\
 112    ((gform r = NPAIR 0 1) <=> (r = True)) /\
 113    ((gform r = NPAIR 1 (NPAIR m n)) <=>
 114         (?s t. (r = s === t) /\ (gterm s = m) /\ (gterm t = n))) /\
 115    ((gform r = NPAIR 2 (NPAIR m n)) <=>
 116         (?s t. (r = s << t) /\ (gterm s = m) /\ (gterm t = n))) /\
 117    ((gform r = NPAIR 3 (NPAIR m n)) <=>
 118         (?s t. (r = s <<= t) /\ (gterm s = m) /\ (gterm t = n))) /\
 119    ((gform r = NPAIR 4 n) = (?p. (r = Not p) /\ (gform p = n))) /\
 120    ((gform r = NPAIR 5 (NPAIR m n)) <=>
 121         (?p q. (r = p && q) /\ (gform p = m) /\ (gform q = n))) /\
 122    ((gform r = NPAIR 6 (NPAIR m n)) <=>
 123         (?p q. (r = p || q) /\ (gform p = m) /\ (gform q = n))) /\
 124    ((gform r = NPAIR 7 (NPAIR m n)) <=>
 125         (?p q. (r = p --> q) /\ (gform p = m) /\ (gform q = n))) /\
 126    ((gform r = NPAIR 8 (NPAIR m n)) <=>
 127         (?p q. (r = p <-> q) /\ (gform p = m) /\ (gform q = n))) /\
 128    ((gform r = NPAIR 9 (NPAIR (number x) n)) <=>
 129         (?p. (r = !!x p) /\ (gform p = n))) /\
 130    ((gform r = NPAIR 10 (NPAIR (number x) n)) <=>
 131         (?p. (r = ??x p) /\ (gform p = n)))`,
 132   STRUCT_CASES_TAC(SPEC `r:form` form_CASES) THEN
 133   ASM_REWRITE_TAC[gform; NPAIR_INJ; ARITH_EQ; NUMBER_INJ;
 134                   form_DISTINCT; form_INJ] THEN
 135   MESON_TAC[]);;
 136
 137 (* ------------------------------------------------------------------------- *)
 138 (* Definability of "godel number of numeral n".                              *)
 139 (* ------------------------------------------------------------------------- *)
 140
 141 let gnumeral = new_definition
 142   `gnumeral m n = (gterm(numeral m) = n)`;;
 143
 144 let arith_gnumeral1 = new_definition
 145  `arith_gnumeral1 a b = formsubst ((3 |-> a) ((4 |-> b) V))
 146        (??0 (??1
 147        (V 3 === arith_pair (V 0) (V 1) &&
 148         V 4 === arith_pair (Suc(V 0)) (arith_pair (numeral 2) (V 1)))))`;;
 149
 150 let ARITH_GNUMERAL1 = prove
 151  (`!v a b. holds v (arith_gnumeral1 a b) <=>
 152                 ?x y. termval v a = NPAIR x y /\
 153                       termval v b = NPAIR (SUC x) (NPAIR 2 y)`,
 154   REWRITE_TAC[arith_gnumeral1; holds; HOLDS_FORMSUBST] THEN
 155   REWRITE_TAC[termval; ARITH_EQ; o_THM; valmod; ARITH_PAIR; TERMVAL_NUMERAL]);;
 156
 157 let FV_GNUMERAL1 = prove
 158  (`!s t. FV(arith_gnumeral1 s t) = FVT s UNION FVT t`,
 159   REWRITE_TAC[arith_gnumeral1] THEN FV_TAC[FVT_PAIR; FVT_NUMERAL]);;
 160
 161 let arith_gnumeral1' = new_definition
 162  `arith_gnumeral1' x y = arith_rtc arith_gnumeral1 x y`;;
 163
 164 let ARITH_GNUMERAL1' = prove
 165  (`!v s t. holds v (arith_gnumeral1' s t) <=>
 166               RTC (\a b. ?x y. a = NPAIR x y /\
 167                                b = NPAIR (SUC x) (NPAIR 2 y))
 168                   (termval v s) (termval v t)`,
 169   REWRITE_TAC[arith_gnumeral1'] THEN MATCH_MP_TAC ARITH_RTC THEN
 170   REWRITE_TAC[ARITH_GNUMERAL1]);;
 171
 172 let FV_GNUMERAL1' = prove
 173  (`!s t. FV(arith_gnumeral1' s t) = FVT s UNION FVT t`,
 174   SIMP_TAC[arith_gnumeral1'; FV_RTC; FV_GNUMERAL1]);;
 175
 176 let arith_gnumeral = new_definition
 177  `arith_gnumeral n p =
 178         formsubst ((0 |-> n) ((1 |-> p) V))
 179             (arith_gnumeral1' (arith_pair Z (numeral 3))
 180                               (arith_pair (V 0) (V 1)))`;;
 181
 182 let ARITH_GNUMERAL = prove
 183  (`!v s t. holds v (arith_gnumeral s t) <=>
 184             gnumeral (termval v s) (termval v t)`,
 185   REWRITE_TAC[arith_gnumeral; holds; HOLDS_FORMSUBST;
 186               ARITH_GNUMERAL1'; ARITH_PAIR; TERMVAL_NUMERAL] THEN
 187   REWRITE_TAC[termval; ARITH_EQ; o_THM; valmod] THEN
 188   MP_TAC(INST
 189    [`(gterm o numeral)`,`fn:num->num`;
 190     `3`,`e:num`;
 191     `\a:num b:num. NPAIR 2 a`,`f:num->num->num`] PRIMREC_SIGMA) THEN
 192   ANTS_TAC THENL
 193    [REWRITE_TAC[gterm; numeral; o_THM] THEN REWRITE_TAC[NPAIR; ARITH];
 194     SIMP_TAC[gnumeral; o_THM]]);;
 195
 196 let FV_GNUMERAL = prove
 197  (`!s t. FV(arith_gnumeral s t) =  FVT(s) UNION FVT(t)`,
 198   REWRITE_TAC[arith_gnumeral] THEN
 199   FV_TAC[FV_GNUMERAL1'; FVT_PAIR; FVT_NUMERAL]);;
 200
 201 (* ------------------------------------------------------------------------- *)
 202 (* Diagonal substitution.                                                    *)
 203 (* ------------------------------------------------------------------------- *)
 204
 205 let qdiag = new_definition
 206   `qdiag x q = qsubst (x,numeral(gform q)) q`;;
 207
 208 let arith_qdiag = new_definition
 209   `arith_qdiag x s t =
 210         formsubst ((1 |-> s) ((2 |-> t) V))
 211         (?? 3
 212            (arith_gnumeral (V 1) (V 3) &&
 213             arith_pair (numeral 10)  (arith_pair (numeral(number x))
 214                                                  (arith_pair (numeral 5)
 215               (arith_pair (arith_pair (numeral 1)
 216        (arith_pair (arith_pair (numeral 0) (numeral(number x))) (V 3)))
 217                    (V 1)))) ===
 218         V 2))`;;
 219
 220 let QDIAG_FV = prove
 221  (`FV(qdiag x q) = FV(q) DELETE x`,
 222   REWRITE_TAC[qdiag; FV_QSUBST; FVT_NUMERAL; UNION_EMPTY]);;
 223
 224 let HOLDS_QDIAG = prove
 225  (`!v x q. holds v (qdiag x q) = holds ((x |-> gform q) v) q`,
 226   SIMP_TAC[qdiag; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY; TERMVAL_NUMERAL]);;
 227
 228 let ARITH_QDIAG = prove
 229  (`(termval v s = gform p)
 230    ==> (holds v (arith_qdiag x s t) <=> (termval v t = gform(qdiag x p)))`,
 231   REPEAT STRIP_TAC THEN
 232   REWRITE_TAC[qdiag; qsubst; arith_qdiag; gform; gterm] THEN
 233   ASM_REWRITE_TAC[HOLDS_FORMSUBST; holds; termval; TERMVAL_NUMERAL;
 234    gnumeral; ARITH_GNUMERAL; ARITH_PAIR] THEN
 235   ASM_REWRITE_TAC[o_DEF; valmod; ARITH_EQ; termval] THEN MESON_TAC[]);;
 236
 237 let FV_QDIAG = prove
 238  (`!x s t. FV(arith_qdiag x s t) = FVT(s) UNION FVT(t)`,
 239   REWRITE_TAC[arith_qdiag; FORMSUBST_FV; FV; FV_GNUMERAL; FVT_PAIR;
 240               UNION_EMPTY; FVT_NUMERAL; FVT; TERMSUBST_FVT] THEN
 241   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 242   REWRITE_TAC[DISJ_ACI; IN_DELETE; IN_UNION; IN_SING] THEN
 243   REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
 244   REWRITE_TAC[EXISTS_OR_THM; GSYM CONJ_ASSOC; UNWIND_THM2; ARITH_EQ] THEN
 245   REWRITE_TAC[valmod; ARITH_EQ; DISJ_ACI]);;
 246
 247 (* ------------------------------------------------------------------------- *)
 248 (* Hence diagonalization of a predicate.                                     *)
 249 (* ------------------------------------------------------------------------- *)
 250
 251 let diagonalize = new_definition
 252   `diagonalize x q =
 253         let y = VARIANT(x INSERT FV(q)) in
 254         ??y (arith_qdiag x (V x) (V y) && formsubst ((x |-> V y) V) q)`;;
 255
 256 let FV_DIAGONALIZE = prove
 257  (`!x q. FV(diagonalize x q) = x INSERT (FV q)`,
 258   REPEAT GEN_TAC THEN REWRITE_TAC[diagonalize] THEN LET_TAC THEN
 259   REWRITE_TAC[FV; FV_QDIAG; FORMSUBST_FV; EXTENSION; IN_INSERT; IN_DELETE;
 260               IN_UNION; IN_ELIM_THM; FVT; NOT_IN_EMPTY] THEN
 261   X_GEN_TAC `u:num` THEN
 262   SUBGOAL_THEN `~(y = x) /\ !z. z IN FV(q) ==> ~(y = z)` STRIP_ASSUME_TAC THENL
 263    [ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT];
 264     ALL_TAC] THEN
 265   ASM_CASES_TAC `u:num = x` THEN ASM_REWRITE_TAC[] THEN
 266   ASM_CASES_TAC `u:num = y` THEN ASM_REWRITE_TAC[] THEN
 267   REWRITE_TAC[valmod; COND_RAND; FVT; IN_SING; COND_EXPAND] THEN
 268   ASM_MESON_TAC[]);;
 269
 270 let ARITH_DIAGONALIZE = prove
 271  (`(v x = gform p)
 272    ==> !q. holds v (diagonalize x q) <=> holds ((x |-> gform(qdiag x p)) v) q`,
 273   REPEAT STRIP_TAC THEN REWRITE_TAC[diagonalize] THEN LET_TAC THEN
 274   REWRITE_TAC[holds] THEN
 275   SUBGOAL_THEN `!a. holds ((y |-> a) v) (arith_qdiag x (V x) (V y)) <=>
 276                     (termval ((y |-> a) v) (V y) = gform(qdiag x p))`
 277    (fun th -> REWRITE_TAC[th])
 278   THENL
 279    [GEN_TAC THEN MATCH_MP_TAC ARITH_QDIAG THEN REWRITE_TAC[termval; valmod] THEN
 280     SUBGOAL_THEN `~(x:num = y)` (fun th -> ASM_REWRITE_TAC[th]) THEN
 281     ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT];
 282     ALL_TAC] THEN
 283   REWRITE_TAC[HOLDS_FORMSUBST; termval; VALMOD_BASIC; UNWIND_THM2] THEN
 284   MATCH_MP_TAC HOLDS_VALUATION THEN
 285   X_GEN_TAC `u:num` THEN DISCH_TAC THEN
 286   REWRITE_TAC[o_THM; termval; valmod] THEN
 287   COND_CASES_TAC THEN REWRITE_TAC[termval] THEN
 288   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 289   ASM_MESON_TAC[VARIANT_FINITE; FINITE_INSERT; FV_FINITE; IN_INSERT]);;
 290
 291 (* ------------------------------------------------------------------------- *)
 292 (* And hence the fixed point.                                                *)
 293 (* ------------------------------------------------------------------------- *)
 294
 295 let fixpoint = new_definition
 296   `fixpoint x q = qdiag x (diagonalize x q)`;;
 297
 298 let FV_FIXPOINT = prove
 299  (`!x p. FV(fixpoint x p) = FV(p) DELETE x`,
 300   REWRITE_TAC[fixpoint; FV_QDIAG; QDIAG_FV; FV_DIAGONALIZE;
 301               FVT_NUMERAL] THEN
 302   SET_TAC[]);;
 303
 304 let HOLDS_FIXPOINT = prove
 305  (`!x p v. holds v (fixpoint x p) <=>
 306            holds ((x |-> gform(fixpoint x p)) v) p`,
 307   REPEAT GEN_TAC THEN SIMP_TAC[fixpoint; holds; HOLDS_QDIAG] THEN
 308   SUBGOAL_THEN
 309    `((x |-> gform(diagonalize x p)) v) x = gform (diagonalize x p)`
 310   MP_TAC THENL [REWRITE_TAC[VALMOD_BASIC]; ALL_TAC] THEN
 311   DISCH_THEN(fun th -> REWRITE_TAC[MATCH_MP ARITH_DIAGONALIZE th]) THEN
 312   REWRITE_TAC[VALMOD_VALMOD_BASIC]);;
 313
 314 let HOLDS_IFF_FIXPOINT = prove
 315  (`!x p v. holds v
 316         (fixpoint x p <-> qsubst (x,numeral(gform(fixpoint x p))) p)`,
 317   SIMP_TAC[holds; HOLDS_FIXPOINT; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY;
 318            TERMVAL_NUMERAL]);;
 319
 320 let CARNAP = prove
 321  (`!x q. ?p. (FV(p) = FV(q) DELETE x) /\
 322              true (p <-> qsubst (x,numeral(gform p)) q)`,
 323   REPEAT GEN_TAC THEN EXISTS_TAC `fixpoint x q` THEN
 324   REWRITE_TAC[true_def; HOLDS_IFF_FIXPOINT; FV_FIXPOINT]);;
 325
 326 (* ------------------------------------------------------------------------- *)
 327 (* Hence Tarski's theorem on the undefinability of truth.                    *)
 328 (* ------------------------------------------------------------------------- *)
 329
 330 let definable_by = new_definition
 331   `definable_by P s <=> ?p x. P p /\ (!v. holds v p <=> (v(x)) IN s)`;;
 332
 333 let definable = new_definition
 334   `definable s <=> ?p x. !v. holds v p <=> (v(x)) IN s`;;
 335
 336 let TARSKI_THEOREM = prove
 337  (`~(definable {gform p | true p})`,
 338   REWRITE_TAC[definable; IN_ELIM_THM; NOT_EXISTS_THM] THEN
 339   MAP_EVERY X_GEN_TAC [`p:form`; `x:num`] THEN DISCH_TAC THEN
 340   MP_TAC(SPECL [`x:num`; `Not p`] CARNAP) THEN
 341   DISCH_THEN(X_CHOOSE_THEN `q:form` (MP_TAC o CONJUNCT2)) THEN
 342   SIMP_TAC[true_def; holds; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY] THEN
 343   ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[VALMOD_BASIC; TERMVAL_NUMERAL] THEN
 344   REWRITE_TAC[true_def; GFORM_INJ] THEN MESON_TAC[]);;