1 (* ========================================================================= *)
2 (* Arithmetization of syntax and Tarski's theorem. *)
3 (* ========================================================================= *)
7 (* ------------------------------------------------------------------------- *)
8 (* This is to fake the fact that we might really be using strings. *)
9 (* ------------------------------------------------------------------------- *)
11 let number = new_definition
12 `number(x) = 2 * (x DIV 2) + (1 - x MOD 2)`;;
14 let denumber = new_definition
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`]);;
25 let NUMBER_INJ = prove
26 (`!x y. number(x) = number(y) <=> x = y`,
27 MESON_TAC[NUMBER_DENUMBER]);;
29 let NUMBER_SURJ = prove
30 (`!y. ?x. number(x) = y`,
31 MESON_TAC[NUMBER_DENUMBER]);;
33 (* ------------------------------------------------------------------------- *)
34 (* Arithmetization. *)
35 (* ------------------------------------------------------------------------- *)
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)))`;;
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)))`;;
58 (* ------------------------------------------------------------------------- *)
60 (* ------------------------------------------------------------------------- *)
63 (`!s t. (gterm s = gterm t) <=> (s = t)`,
64 MATCH_MP_TAC term_INDUCT THEN REPEAT CONJ_TAC THENL
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]);;
75 (`!p q. (gform p = gform q) <=> (p = q)`,
76 MATCH_MP_TAC form_INDUCT THEN REPEAT CONJ_TAC THENL
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]);;
93 (* ------------------------------------------------------------------------- *)
94 (* Useful case theorems. *)
95 (* ------------------------------------------------------------------------- *)
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
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
137 (* ------------------------------------------------------------------------- *)
138 (* Definability of "godel number of numeral n". *)
139 (* ------------------------------------------------------------------------- *)
141 let gnumeral = new_definition
142 `gnumeral m n = (gterm(numeral m) = n)`;;
144 let arith_gnumeral1 = new_definition
145 `arith_gnumeral1 a b = formsubst ((3 |-> a) ((4 |-> b) V))
147 (V 3 === arith_pair (V 0) (V 1) &&
148 V 4 === arith_pair (Suc(V 0)) (arith_pair (numeral 2) (V 1)))))`;;
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]);;
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]);;
161 let arith_gnumeral1' = new_definition
162 `arith_gnumeral1' x y = arith_rtc arith_gnumeral1 x y`;;
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]);;
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]);;
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)))`;;
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
189 [`(gterm o numeral)`,`fn:num->num`;
191 `\a:num b:num. NPAIR 2 a`,`f:num->num->num`] PRIMREC_SIGMA) THEN
193 [REWRITE_TAC[gterm; numeral; o_THM] THEN REWRITE_TAC[NPAIR; ARITH];
194 SIMP_TAC[gnumeral; o_THM]]);;
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]);;
201 (* ------------------------------------------------------------------------- *)
202 (* Diagonal substitution. *)
203 (* ------------------------------------------------------------------------- *)
205 let qdiag = new_definition
206 `qdiag x q = qsubst (x,numeral(gform q)) q`;;
208 let arith_qdiag = new_definition
210 formsubst ((1 |-> s) ((2 |-> t) V))
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)))
221 (`FV(qdiag x q) = FV(q) DELETE x`,
222 REWRITE_TAC[qdiag; FV_QSUBST; FVT_NUMERAL; UNION_EMPTY]);;
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]);;
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[]);;
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]);;
247 (* ------------------------------------------------------------------------- *)
248 (* Hence diagonalization of a predicate. *)
249 (* ------------------------------------------------------------------------- *)
251 let diagonalize = new_definition
253 let y = VARIANT(x INSERT FV(q)) in
254 ??y (arith_qdiag x (V x) (V y) && formsubst ((x |-> V y) V) q)`;;
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];
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
270 let ARITH_DIAGONALIZE = prove
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])
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];
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]);;
291 (* ------------------------------------------------------------------------- *)
292 (* And hence the fixed point. *)
293 (* ------------------------------------------------------------------------- *)
295 let fixpoint = new_definition
296 `fixpoint x q = qdiag x (diagonalize x q)`;;
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;
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
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]);;
314 let HOLDS_IFF_FIXPOINT = prove
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;
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]);;
326 (* ------------------------------------------------------------------------- *)
327 (* Hence Tarski's theorem on the undefinability of truth. *)
328 (* ------------------------------------------------------------------------- *)
330 let definable_by = new_definition
331 `definable_by P s <=> ?p x. P p /\ (!v. holds v p <=> (v(x)) IN s)`;;
333 let definable = new_definition
334 `definable s <=> ?p x. !v. holds v p <=> (v(x)) IN s`;;
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[]);;