1 (* ========================================================================= *)
2 (* Proof that provability is definable; weak form of Godel's theorem. *)
3 (* ========================================================================= *)
7 (* ------------------------------------------------------------------------- *)
8 (* Auxiliary predicate: all numbers in an iterated-pair "list". *)
9 (* ------------------------------------------------------------------------- *)
15 if ?x y. z = NPAIR x y
16 then P (@x. ?y. NPAIR x y = z) /\
17 ALLN (@y. ?x. NPAIR x y = z)
19 GEN_TAC THEN MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN
20 REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
21 BINOP_TAC THENL [ALL_TAC; FIRST_ASSUM MATCH_MP_TAC] THEN
22 FIRST_ASSUM(REPEAT_TCL CHOOSE_THEN SUBST1_TAC) THEN
23 REWRITE_TAC[NPAIR_INJ; RIGHT_EXISTS_AND_THM; EXISTS_REFL;
24 SELECT_REFL; NPAIR_LT; LEFT_EXISTS_AND_THM]) in
25 new_specification ["ALLN"] (REWRITE_RULE[SKOLEM_THM] th);;
29 (ALLN P (NPAIR x y) <=> P x /\ ALLN P y)`,
30 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [ALLN_DEF] THEN
31 REWRITE_TAC[NPAIR_NONZERO] THEN
32 REWRITE_TAC[NPAIR_INJ; LEFT_EXISTS_AND_THM; RIGHT_EXISTS_AND_THM] THEN
33 REWRITE_TAC[EXISTS_REFL; GSYM EXISTS_REFL]);;
35 (* ------------------------------------------------------------------------- *)
37 (* ------------------------------------------------------------------------- *)
39 let TERM1 = new_definition
41 (?l u. (x = l) /\ (y = NPAIR (NPAIR 0 u) l)) \/
42 (?l. (x = l) /\ (y = NPAIR (NPAIR 1 0) l)) \/
43 (?t l. (x = NPAIR t l) /\ (y = NPAIR (NPAIR 2 t) l)) \/
44 (?n s t l. ((n = 3) \/ (n = 4)) /\
45 (x = NPAIR s (NPAIR t l)) /\
46 (y = NPAIR (NPAIR n (NPAIR s t)) l))`;;
48 let TERM = new_definition
49 `TERM n <=> RTC TERM1 0 (NPAIR n 0)`;;
51 let isagterm = new_definition
52 `isagterm n <=> ?t. n = gterm t`;;
54 let TERM_LEMMA1 = prove
55 (`!x y. TERM1 x y ==> ALLN isagterm x ==> ALLN isagterm y`,
56 REPEAT GEN_TAC THEN REWRITE_TAC[TERM1] THEN
57 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
58 SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN; isagterm] THEN
59 MESON_TAC[gterm; NUMBER_SURJ]);;
61 let TERM_LEMMA2 = prove
62 (`!t a. RTC TERM1 a (NPAIR (gterm t) a)`,
63 MATCH_MP_TAC term_INDUCT THEN REWRITE_TAC[gterm] THEN
64 MESON_TAC[RTC_INC; RTC_TRANS; TERM1]);;
67 (`!n. TERM n <=> ?t. n = gterm t`,
68 GEN_TAC THEN REWRITE_TAC[TERM] THEN EQ_TAC THENL
69 [ALL_TAC; MESON_TAC[TERM_LEMMA2]] THEN
70 SUBGOAL_THEN `!x y. RTC TERM1 x y ==> ALLN isagterm x ==> ALLN isagterm y`
71 (fun th -> MESON_TAC[ALLN; isagterm; th]) THEN
72 MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[TERM_LEMMA1] THEN MESON_TAC[]);;
74 (* ------------------------------------------------------------------------- *)
76 (* ------------------------------------------------------------------------- *)
78 let FORM1 = new_definition
80 (?l. (x = l) /\ (y = NPAIR (NPAIR 0 0) l)) \/
81 (?l. (x = l) /\ (y = NPAIR (NPAIR 0 1) l)) \/
82 (?n s t l. ((n = 1) \/ (n = 2) \/ (n = 3)) /\
85 (y = NPAIR (NPAIR n (NPAIR s t)) l)) \/
86 (?p l. (x = NPAIR p l) /\
87 (y = NPAIR (NPAIR 4 p) l)) \/
88 (?n p q l. ((n = 5) \/ (n = 6) \/ (n = 7) \/ (n = 8)) /\
89 (x = NPAIR p (NPAIR q l)) /\
90 (y = NPAIR (NPAIR n (NPAIR p q)) l)) \/
91 (?n u p l. ((n = 9) \/ (n = 10)) /\
93 (y = NPAIR (NPAIR n (NPAIR u p)) l))`;;
95 let FORM = new_definition
96 `FORM n <=> RTC FORM1 0 (NPAIR n 0)`;;
98 let isagform = new_definition
99 `isagform n <=> ?t. n = gform t`;;
101 let FORM_LEMMA1 = prove
102 (`!x y. FORM1 x y ==> ALLN isagform x ==> ALLN isagform y`,
103 REPEAT GEN_TAC THEN REWRITE_TAC[FORM1] THEN
104 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
105 SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN; isagform] THEN
106 MESON_TAC[gform; TERM_THM; NUMBER_SURJ]);;
108 (*** Following really blows up if we just use FORM1
109 *** instead of manually breaking up the conjuncts
112 let FORM_LEMMA2 = prove
113 (`!p a. RTC FORM1 a (NPAIR (gform p) a)`,
114 MATCH_MP_TAC form_INDUCT THEN REWRITE_TAC[gform] THEN
116 MESON_TAC[RTC_INC; RTC_TRANS; TERM_THM;
117 REWRITE_RULE[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`]
118 (snd(EQ_IMP_RULE (SPEC_ALL FORM1)))]);;
121 (`!n. FORM n <=> ?p. n = gform p`,
122 GEN_TAC THEN REWRITE_TAC[FORM] THEN EQ_TAC THENL
123 [ALL_TAC; MESON_TAC[FORM_LEMMA2]] THEN
124 SUBGOAL_THEN `!x y. RTC FORM1 x y ==> ALLN isagform x ==> ALLN isagform y`
125 (fun th -> MESON_TAC[ALLN; isagform; th]) THEN
126 MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FORM_LEMMA1] THEN MESON_TAC[]);;
128 (* ------------------------------------------------------------------------- *)
129 (* Term without particular variable. *)
130 (* ------------------------------------------------------------------------- *)
132 let FREETERM1 = new_definition
134 (?l u. ~(u = m) /\ (x = l) /\ (y = NPAIR (NPAIR 0 u) l)) \/
135 (?l. (x = l) /\ (y = NPAIR (NPAIR 1 0) l)) \/
136 (?t l. (x = NPAIR t l) /\ (y = NPAIR (NPAIR 2 t) l)) \/
137 (?n s t l. ((n = 3) \/ (n = 4)) /\
138 (x = NPAIR s (NPAIR t l)) /\
139 (y = NPAIR (NPAIR n (NPAIR s t)) l))`;;
141 let FREETERM = new_definition
142 `FREETERM m n <=> RTC (FREETERM1 m) 0 (NPAIR n 0)`;;
144 let isafterm = new_definition
145 `isafterm m n <=> ?t. ~(m IN IMAGE number (FVT t)) /\ (n = gterm t)`;;
148 (`(~(number x = m) ==> isafterm m (NPAIR 0 (number x))) /\
149 isafterm m (NPAIR 1 0) /\
150 (isafterm m t ==> isafterm m (NPAIR 2 t)) /\
151 (isafterm m s /\ isafterm m t ==> isafterm m (NPAIR 3 (NPAIR s t))) /\
152 (isafterm m s /\ isafterm m t ==> isafterm m (NPAIR 4 (NPAIR s t)))`,
153 REWRITE_TAC[isafterm; gterm] THEN REPEAT CONJ_TAC THENL
154 [DISCH_TAC THEN EXISTS_TAC `V x`;
156 DISCH_THEN(X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC) THEN
158 DISCH_THEN(CONJUNCTS_THEN2
159 (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
160 (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC)) THEN
162 DISCH_THEN(CONJUNCTS_THEN2
163 (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
164 (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC)) THEN
165 EXISTS_TAC `s ** t`] THEN
166 ASM_REWRITE_TAC[gterm; FVT; IMAGE_UNION; NOT_IN_EMPTY; IN_SING; IN_UNION;
169 let FREETERM_LEMMA1 = prove
170 (`!m x y. FREETERM1 m x y ==> ALLN (isafterm m) x ==> ALLN (isafterm m) y`,
171 REPEAT GEN_TAC THEN REWRITE_TAC[FREETERM1] THEN
172 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
173 SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
174 MESON_TAC[ISAFTERM; NUMBER_SURJ]);;
176 let FREETERM_LEMMA2 = prove
177 (`!m t a. ~(m IN IMAGE number (FVT t))
178 ==> RTC (FREETERM1 m) a (NPAIR (gterm t) a)`,
179 GEN_TAC THEN MATCH_MP_TAC term_INDUCT THEN
180 REWRITE_TAC[gterm; FVT; NOT_IN_EMPTY; IN_SING; IN_UNION;
181 IMAGE_CLAUSES; IMAGE_UNION] THEN
182 REWRITE_TAC[DE_MORGAN_THM] THEN
184 TRY(REPEAT GEN_TAC THEN DISCH_THEN
185 (fun th -> GEN_TAC THEN STRIP_TAC THEN MP_TAC th)) THEN
186 ASM_REWRITE_TAC[] THEN
187 MESON_TAC[RTC_INC; RTC_TRANS; FREETERM1]);;
189 let FREETERM_THM = prove
190 (`!m n. FREETERM m n <=> ?t. ~(m IN IMAGE number (FVT(t))) /\ (n = gterm t)`,
191 REPEAT GEN_TAC THEN REWRITE_TAC[FREETERM] THEN EQ_TAC THENL
192 [ALL_TAC; MESON_TAC[FREETERM_LEMMA2]] THEN
193 SUBGOAL_THEN `!x y. RTC (FREETERM1 m) x y
194 ==> ALLN (isafterm m) x ==> ALLN (isafterm m) y`
195 (fun th -> MESON_TAC[ALLN; isagterm; isafterm; th]) THEN
196 MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FREETERM_LEMMA1] THEN MESON_TAC[]);;
198 (* ------------------------------------------------------------------------- *)
199 (* Formula without particular free variable. *)
200 (* ------------------------------------------------------------------------- *)
202 let FREEFORM1 = new_definition
204 (?l. (x = l) /\ (y = NPAIR (NPAIR 0 0) l)) \/
205 (?l. (x = l) /\ (y = NPAIR (NPAIR 0 1) l)) \/
206 (?n s t l. ((n = 1) \/ (n = 2) \/ (n = 3)) /\
207 FREETERM m s /\ FREETERM m t /\
209 (y = NPAIR (NPAIR n (NPAIR s t)) l)) \/
210 (?p l. (x = NPAIR p l) /\
211 (y = NPAIR (NPAIR 4 p) l)) \/
212 (?n p q l. ((n = 5) \/ (n = 6) \/ (n = 7) \/ (n = 8)) /\
213 (x = NPAIR p (NPAIR q l)) /\
214 (y = NPAIR (NPAIR n (NPAIR p q)) l)) \/
215 (?n u p l. ((n = 9) \/ (n = 10)) /\
217 (y = NPAIR (NPAIR n (NPAIR u p)) l)) \/
218 (?n p l. ((n = 9) \/ (n = 10)) /\
220 (y = NPAIR (NPAIR n (NPAIR m p)) l))`;;
222 let FREEFORM = new_definition
223 `FREEFORM m n <=> RTC (FREEFORM1 m) 0 (NPAIR n 0)`;;
225 let isafform = new_definition
226 `isafform m n <=> ?p. ~(m IN IMAGE number (FV p)) /\ (n = gform p)`;;
229 (`isafform m (NPAIR 0 0) /\
230 isafform m (NPAIR 0 1) /\
231 (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 1 (NPAIR s t))) /\
232 (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 2 (NPAIR s t))) /\
233 (isafterm m s /\ isafterm m t ==> isafform m (NPAIR 3 (NPAIR s t))) /\
234 (isafform m p ==> isafform m (NPAIR 4 p)) /\
235 (isafform m p /\ isafform m q ==> isafform m (NPAIR 5 (NPAIR p q))) /\
236 (isafform m p /\ isafform m q ==> isafform m (NPAIR 6 (NPAIR p q))) /\
237 (isafform m p /\ isafform m q ==> isafform m (NPAIR 7 (NPAIR p q))) /\
238 (isafform m p /\ isafform m q ==> isafform m (NPAIR 8 (NPAIR p q))) /\
239 (isafform m p ==> isafform m (NPAIR 9 (NPAIR x p))) /\
240 (isafform m p ==> isafform m (NPAIR 10 (NPAIR x p))) /\
241 (isagform p ==> isafform m (NPAIR 9 (NPAIR m p))) /\
242 (isagform p ==> isafform m (NPAIR 10 (NPAIR m p)))`,
243 let tac0 = DISCH_THEN(X_CHOOSE_THEN `p:form` STRIP_ASSUME_TAC)
245 DISCH_THEN(CONJUNCTS_THEN2
246 (X_CHOOSE_THEN `s:term` STRIP_ASSUME_TAC)
247 (X_CHOOSE_THEN `t:term` STRIP_ASSUME_TAC))
249 DISCH_THEN(CONJUNCTS_THEN2
250 (X_CHOOSE_THEN `p:form` STRIP_ASSUME_TAC)
251 (X_CHOOSE_THEN `q:form` STRIP_ASSUME_TAC)) in
252 REWRITE_TAC[isafform; gform; isagform; isafterm] THEN REPEAT CONJ_TAC THENL
255 tac1 THEN EXISTS_TAC `s === t`;
256 tac1 THEN EXISTS_TAC `s << t`;
257 tac1 THEN EXISTS_TAC `s <<= t`;
258 tac0 THEN EXISTS_TAC `Not p`;
259 tac2 THEN EXISTS_TAC `p && q`;
260 tac2 THEN EXISTS_TAC `p || q`;
261 tac2 THEN EXISTS_TAC `p --> q`;
262 tac2 THEN EXISTS_TAC `p <-> q`;
263 tac0 THEN EXISTS_TAC `!!(denumber x) p`;
264 tac0 THEN EXISTS_TAC `??(denumber x) p`;
265 tac0 THEN EXISTS_TAC `!!(denumber m) p`;
266 tac0 THEN EXISTS_TAC `??(denumber m) p`] THEN
267 ASM_REWRITE_TAC[FV; IN_DELETE; NOT_IN_EMPTY; IN_SING; IN_UNION; gform;
268 NUMBER_DENUMBER; IMAGE_CLAUSES; IMAGE_UNION] THEN
269 ASM SET_TAC[NUMBER_DENUMBER]);;
271 let FREEFORM_LEMMA1 = prove
272 (`!x y. FREEFORM1 m x y ==> ALLN (isafform m) x ==> ALLN (isafform m) y`,
273 REPEAT GEN_TAC THEN REWRITE_TAC[FREEFORM1] THEN
274 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
275 SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
276 REWRITE_TAC[FREETERM_THM; GSYM isafterm] THEN
277 REWRITE_TAC[FORM_THM; GSYM isagform] THEN MESON_TAC[ISAFFORM]);;
279 let FREEFORM_LEMMA2 = prove
280 (`!m p a. ~(m IN IMAGE number (FV p))
281 ==> RTC (FREEFORM1 m) a (NPAIR (gform p) a)`,
283 (`m IN IMAGE number (s DELETE k) <=>
284 m IN IMAGE number s /\ ~(m = number k)`,
285 SET_TAC[NUMBER_INJ]) in
286 GEN_TAC THEN MATCH_MP_TAC form_INDUCT THEN
287 REWRITE_TAC[gform; FV; NOT_IN_EMPTY; IN_DELETE; IN_SING; IN_UNION;
288 lemma; IMAGE_UNION; IMAGE_CLAUSES] THEN
289 REWRITE_TAC[DE_MORGAN_THM] THEN
291 TRY(REPEAT GEN_TAC THEN DISCH_THEN
292 (fun th -> GEN_TAC THEN STRIP_TAC THEN MP_TAC th)) THEN
293 ASM_REWRITE_TAC[] THEN
294 MESON_TAC[RTC_INC; RTC_TRANS; FORM_THM;
295 REWRITE_RULE[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`;
297 (snd(EQ_IMP_RULE (SPEC_ALL FREEFORM1)))]);;
299 let FREEFORM_THM = prove
300 (`!m n. FREEFORM m n <=> ?p. ~(m IN IMAGE number (FV p)) /\ (n = gform p)`,
301 REPEAT GEN_TAC THEN REWRITE_TAC[FREEFORM] THEN EQ_TAC THENL
302 [ALL_TAC; MESON_TAC[FREEFORM_LEMMA2]] THEN
303 SUBGOAL_THEN `!x y. RTC (FREEFORM1 m) x y
304 ==> ALLN (isafform m) x ==> ALLN (isafform m) y`
305 (fun th -> MESON_TAC[ALLN; isagform; isafform; th]) THEN
306 MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[FREEFORM_LEMMA1] THEN MESON_TAC[]);;
308 (* ------------------------------------------------------------------------- *)
309 (* Arithmetization of logical axioms --- autogenerated. *)
310 (* ------------------------------------------------------------------------- *)
312 let AXIOM,AXIOM_THM =
314 (`((?x p. P (number x) (gform p) /\ ~(x IN FV(p))) <=>
315 (?x p. FREEFORM x p /\ P x p)) /\
316 ((?x t. P (number x) (gterm t) /\ ~(x IN FVT(t))) <=>
317 (?x t. FREETERM x t /\ P x t))`,
318 REWRITE_TAC[FREETERM_THM; FREEFORM_THM] THEN CONJ_TAC THEN
319 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
320 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
321 GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV) [SWAP_EXISTS_THM] THEN
322 REWRITE_TAC[UNWIND_THM2; IN_IMAGE] THEN
323 ASM_MESON_TAC[IN_IMAGE; NUMBER_DENUMBER])
325 (`((?p. P(gform p)) <=> (?p. FORM(p) /\ P p)) /\
326 ((?t. P(gterm t)) <=> (?t. TERM(t) /\ P t))`,
327 MESON_TAC[FORM_THM; TERM_THM])
329 (`(?x. P(number x)) <=> (?x. P x)`,
330 MESON_TAC[NUMBER_DENUMBER]) in
331 let th = (REWRITE_CONV[GSYM GFORM_INJ] THENC
332 REWRITE_CONV[gform; gterm] THENC
333 REWRITE_CONV[th0] THENC REWRITE_CONV[th1] THENC
334 REWRITE_CONV[th2] THENC
335 REWRITE_CONV[RIGHT_AND_EXISTS_THM])
336 (rhs(concl(SPEC `a:form` axiom_CASES))) in
337 let dtm = mk_eq(`(AXIOM:num->bool) a`,
338 subst [`a:num`,`gform a`] (rhs(concl th))) in
339 let AXIOM = new_definition dtm in
340 let AXIOM_THM = prove
341 (`!p. AXIOM(gform p) <=> axiom p`,
342 REWRITE_TAC[axiom_CASES; AXIOM; th]) in
345 (* ------------------------------------------------------------------------- *)
346 (* Prove also that all AXIOMs are in fact numbers of formulas. *)
347 (* ------------------------------------------------------------------------- *)
349 let GTERM_CASES_ALT = prove
350 (`(gterm u = NPAIR 0 x <=> u = V(denumber x))`,
351 REWRITE_TAC[GSYM GTERM_CASES; NUMBER_DENUMBER]);;
353 let GFORM_CASES_ALT = prove
354 (`(gform r = NPAIR 9 (NPAIR x n) <=>
355 (?p. r = !!(denumber x) p /\ gform p = n)) /\
356 (gform r = NPAIR 10 (NPAIR x n) <=>
357 (?p. r = ??(denumber x) p /\ gform p = n))`,
358 REWRITE_TAC[GSYM GFORM_CASES; NUMBER_DENUMBER]);;
360 let AXIOM_FORMULA = prove
361 (`!a. AXIOM a ==> ?p. a = gform p`,
362 REWRITE_TAC[AXIOM; FREEFORM_THM; FREETERM_THM; FORM_THM; TERM_THM] THEN
363 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
364 CONV_TAC(BINDER_CONV SYM_CONV) THEN
365 REWRITE_TAC[GFORM_CASES; GTERM_CASES;
366 GTERM_CASES_ALT; GFORM_CASES_ALT] THEN
367 MESON_TAC[NUMBER_DENUMBER]);;
369 let AXIOM_THM_STRONG = prove
370 (`!a. AXIOM a <=> ?p. axiom p /\ (a = gform p)`,
371 MESON_TAC[AXIOM_THM; AXIOM_FORMULA]);;
373 (* ------------------------------------------------------------------------- *)
374 (* Arithmetization of the full logical inference rules. *)
375 (* ------------------------------------------------------------------------- *)
377 let PROV1 = new_definition
379 (?a. (AXIOM a \/ a IN A) /\ (y = NPAIR a x)) \/
380 (?p q l. (x = NPAIR (NPAIR 7 (NPAIR p q)) (NPAIR p l)) /\
382 (?p u l. (x = NPAIR p l) /\ (y = NPAIR (NPAIR 9 (NPAIR u p)) l))`;;
384 let PROV = new_definition
385 `PROV A n <=> RTC (PROV1 A) 0 (NPAIR n 0)`;;
387 let isaprove = new_definition
388 `isaprove A n <=> ?p. (gform p = n) /\ A |-- p`;;
390 let PROV_LEMMA1 = prove
391 (`!A p q. PROV1 (IMAGE gform A) x y
392 ==> ALLN (isaprove A) x ==> ALLN (isaprove A) y`,
393 REPEAT GEN_TAC THEN REWRITE_TAC[PROV1] THEN
394 REWRITE_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
395 SIMP_TAC[LEFT_IMP_EXISTS_THM; ALLN] THEN
396 REWRITE_TAC[isaprove] THEN REPEAT CONJ_TAC THEN
397 REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
398 [ASM_MESON_TAC[AXIOM_THM_STRONG; proves_RULES];
399 ASM_MESON_TAC[IN_IMAGE; GFORM_INJ; proves_RULES; gform];
401 ASM_MESON_TAC[NUMBER_DENUMBER;
402 IN_IMAGE; GFORM_INJ; proves_RULES; gform]] THEN
403 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
404 ONCE_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
405 MATCH_MP_TAC form_INDUCT THEN
406 REWRITE_TAC[gform; NPAIR_INJ; ARITH_EQ] THEN
407 MAP_EVERY X_GEN_TAC [`P:form`; `Q:form`] THEN
408 DISCH_THEN(K ALL_TAC) THEN
409 DISCH_THEN(CONJUNCTS_THEN2 (STRIP_ASSUME_TAC o GSYM) MP_TAC) THEN
410 ASM_REWRITE_TAC[GFORM_INJ] THEN
411 REWRITE_TAC[GSYM CONJ_ASSOC; UNWIND_THM2] THEN
412 ASM_MESON_TAC[proves_RULES]);;
414 let PROV_LEMMA2 = prove
415 (`!A p. A |-- p ==> !a. RTC (PROV1 (IMAGE gform A)) a (NPAIR (gform p) a)`,
416 GEN_TAC THEN MATCH_MP_TAC proves_INDUCT THEN REWRITE_TAC[gform] THEN
417 MESON_TAC[RTC_INC; RTC_TRANS; PROV1; IN_IMAGE; AXIOM_THM]);;
419 let PROV_THM_STRONG = prove
420 (`!A n. PROV (IMAGE gform A) n <=> ?p. A |-- p /\ (gform p = n)`,
421 REPEAT GEN_TAC THEN REWRITE_TAC[PROV] THEN EQ_TAC THENL
422 [ALL_TAC; MESON_TAC[PROV_LEMMA2]] THEN
424 `!x y. RTC (PROV1 (IMAGE gform A)) x y
425 ==> ALLN (isaprove A) x ==> ALLN (isaprove A) y`
426 (fun th -> MESON_TAC[ALLN; isaprove; GFORM_INJ; th]) THEN
427 MATCH_MP_TAC RTC_INDUCT THEN REWRITE_TAC[PROV_LEMMA1] THEN MESON_TAC[]);;
430 (`!A p. PROV (IMAGE gform A) (gform p) <=> A |-- p`,
431 MESON_TAC[PROV_THM_STRONG; GFORM_INJ]);;
433 (* ------------------------------------------------------------------------- *)
434 (* Now really objectify all that. *)
435 (* ------------------------------------------------------------------------- *)
437 let arith_term1,ARITH_TERM1 = OBJECTIFY [] "arith_term1" TERM1;;
440 (`!s t. FV(arith_term1 s t) = (FVT s) UNION (FVT t)`,
441 FV_TAC[arith_term1; FVT_PAIR; FVT_NUMERAL]);;
443 let arith_term,ARITH_TERM = OBJECTIFY_RTC ARITH_TERM1 "arith_term" TERM;;
446 (`!t. FV(arith_term t) = FVT t`,
447 FV_TAC[arith_term; FV_RTC; FV_TERM1; FVT_PAIR; FVT_NUMERAL]);;
449 let arith_form1,ARITH_FORM1 =
450 OBJECTIFY [ARITH_TERM] "arith_form1" FORM1;;
453 (`!s t. FV(arith_form1 s t) = (FVT s) UNION (FVT t)`,
454 FV_TAC[arith_form1; FV_TERM; FVT_PAIR; FVT_NUMERAL]);;
456 let arith_form,ARITH_FORM = OBJECTIFY_RTC ARITH_FORM1 "arith_form" FORM;;
459 (`!t. FV(arith_form t) = FVT t`,
460 FV_TAC[arith_form; FV_RTC; FV_FORM1; FVT_PAIR; FVT_NUMERAL]);;
462 let arith_freeterm1,ARITH_FREETERM1 =
463 OBJECTIFY [] "arith_freeterm1" FREETERM1;;
465 let FV_FREETERM1 = prove
466 (`!s t u. FV(arith_freeterm1 s t u) = (FVT s) UNION (FVT t) UNION (FVT u)`,
467 FV_TAC[arith_freeterm1; FVT_PAIR; FVT_NUMERAL]);;
469 let arith_freeterm,ARITH_FREETERM =
470 OBJECTIFY_RTCP ARITH_FREETERM1 "arith_freeterm" FREETERM;;
472 let FV_FREETERM = prove
473 (`!s t. FV(arith_freeterm s t) = (FVT s) UNION (FVT t)`,
474 FV_TAC[arith_freeterm; FV_RTCP; FV_FREETERM1; FVT_PAIR; FVT_NUMERAL]);;
476 let arith_freeform1,ARITH_FREEFORM1 =
477 OBJECTIFY [ARITH_FREETERM; ARITH_FORM] "arith_freeform1" FREEFORM1;;
479 let FV_FREEFORM1 = prove
480 (`!s t u. FV(arith_freeform1 s t u) = (FVT s) UNION (FVT t) UNION (FVT u)`,
481 FV_TAC[arith_freeform1; FV_FREETERM; FV_FORM; FVT_PAIR; FVT_NUMERAL]);;
483 let arith_freeform,ARITH_FREEFORM =
484 OBJECTIFY_RTCP ARITH_FREEFORM1 "arith_freeform" FREEFORM;;
486 let FV_FREEFORM = prove
487 (`!s t. FV(arith_freeform s t) = (FVT s) UNION (FVT t)`,
488 FV_TAC[arith_freeform; FV_RTCP; FV_FREEFORM1; FVT_PAIR; FVT_NUMERAL]);;
490 let arith_axiom,ARITH_AXIOM =
491 OBJECTIFY [ARITH_FORM; ARITH_FREEFORM; ARITH_FREETERM; ARITH_TERM]
492 "arith_axiom" AXIOM;;
495 (`!t. FV(arith_axiom t) = FVT t`,
496 FV_TAC[arith_axiom; FV_FREETERM; FV_FREEFORM; FV_TERM; FV_FORM;
497 FVT_PAIR; FVT_NUMERAL]);;
499 (* ------------------------------------------------------------------------- *)
500 (* Parametrization by A means it's easier to do these cases manually. *)
501 (* ------------------------------------------------------------------------- *)
503 let arith_prov1,ARITH_PROV1 =
504 let PROV1' = REWRITE_RULE[IN] PROV1 in
505 OBJECTIFY [ASSUME `!v n. holds v (A n) <=> Ax (termval v n)`; ARITH_AXIOM]
506 "arith_prov1" PROV1';;
508 let ARITH_PROV1 = prove
509 (`(!v t. holds v (A t) <=> Ax(termval v t))
511 holds v (arith_prov1 A s t) <=>
512 PROV1 Ax (termval v s) (termval v t))`,
513 REWRITE_TAC[arith_prov1; holds; HOLDS_FORMSUBST] THEN
514 REPEAT STRIP_TAC THEN
515 ASM_REWRITE_TAC[termval; valmod; o_THM; ARITH_EQ; ARITH_PAIR;
516 TERMVAL_NUMERAL; ARITH_AXIOM] THEN
517 REWRITE_TAC[PROV1; IN]);;
520 (`(!t. FV(A t) = FVT t) ==> !s t. FV(arith_prov1 A s t) = FVT(s) UNION FVT(t)`,
521 FV_TAC[arith_prov1; FV_AXIOM; FVT_NUMERAL; FVT_PAIR]);;
523 let arith_prov = new_definition
525 formsubst ((0 |-> n) V)
526 (arith_rtc (arith_prov1 A) (numeral 0)
527 (arith_pair (V 0) (numeral 0)))`;;
529 let ARITH_PROV = prove
530 (`!Ax A. (!v t. holds v (A t) <=> Ax(termval v t))
531 ==> !v n. holds v (arith_prov A n) <=> PROV Ax (termval v n)`,
532 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP ARITH_PROV1) THEN
533 DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC) THEN
534 CONV_TAC(TOP_DEPTH_CONV ETA_CONV) THEN DISCH_TAC THEN
535 ASM_REWRITE_TAC[arith_prov; HOLDS_FORMSUBST] THEN
536 REWRITE_TAC[termval; valmod; o_DEF; TERMVAL_NUMERAL; ARITH_PAIR] THEN
540 (`(!t. FV(A t) = FVT t) ==> !t. FV(arith_prov A t) = FVT t`,
541 FV_TAC[arith_prov; FV_PROV1; FV_RTC; FVT_NUMERAL; FVT_PAIR]);;
543 (* ------------------------------------------------------------------------- *)
544 (* Our final conclusion. *)
545 (* ------------------------------------------------------------------------- *)
547 let PROV_DEFINABLE = prove
548 (`!Ax. definable {gform p | p IN Ax} ==> definable {gform p | Ax |-- p}`,
549 GEN_TAC THEN REWRITE_TAC[definable; IN_ELIM_THM] THEN
550 DISCH_THEN(X_CHOOSE_THEN `A:form` (X_CHOOSE_TAC `x:num`)) THEN
551 MP_TAC(SPECL [`IMAGE gform Ax`; `\t. formsubst ((x |-> t) V) A`]
553 REWRITE_TAC[] THEN ANTS_TAC THENL
554 [ASM_REWRITE_TAC[HOLDS_FORMSUBST] THEN
555 REWRITE_TAC[o_THM; VALMOD_BASIC; IMAGE; IN_ELIM_THM];
557 REWRITE_TAC[PROV_THM_STRONG] THEN DISCH_TAC THEN
558 EXISTS_TAC `arith_prov (\t. formsubst ((x |-> t) V) A) (V x)` THEN
559 ASM_REWRITE_TAC[termval] THEN MESON_TAC[]);;
561 (* ------------------------------------------------------------------------- *)
562 (* The crudest conclusion: truth undefinable, provability not, so: *)
563 (* ------------------------------------------------------------------------- *)
565 let GODEL_CRUDE = prove
566 (`!Ax. definable {gform p | p IN Ax} ==> ?p. ~(true p <=> Ax |-- p)`,
567 REPEAT STRIP_TAC THEN MP_TAC TARSKI_THEOREM THEN
568 FIRST_X_ASSUM(MP_TAC o MATCH_MP PROV_DEFINABLE) THEN
569 MATCH_MP_TAC(TAUT `(~c ==> (a <=> b)) ==> a ==> ~b ==> c`) THEN
570 SIMP_TAC[NOT_EXISTS_THM]);;