--- /dev/null
+(* ========================================================================= *)
+(* 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;;
+
+******)
git://colo12-c703.uibk.ac.at / Gödel's incompleteness theorem/.git / blobdiff