1 (* ========================================================================= *)
2 (* Godel's theorem in its true form. *)
3 (* ========================================================================= *)
5 (* ------------------------------------------------------------------------- *)
6 (* Classes of formulas, via auxiliary "shared" inductive definition. *)
7 (* ------------------------------------------------------------------------- *)
9 let sigmapi_RULES,sigmapi_INDUCT,sigmapi_CASES = new_inductive_definition
10 `(!b n. sigmapi b n False) /\
11 (!b n. sigmapi b n True) /\
12 (!b n s t. sigmapi b n (s === t)) /\
13 (!b n s t. sigmapi b n (s << t)) /\
14 (!b n s t. sigmapi b n (s <<= t)) /\
15 (!b n p. sigmapi (~b) n p ==> sigmapi b n (Not p)) /\
16 (!b n p q. sigmapi b n p /\ sigmapi b n q ==> sigmapi b n (p && q)) /\
17 (!b n p q. sigmapi b n p /\ sigmapi b n q ==> sigmapi b n (p || q)) /\
18 (!b n p q. sigmapi (~b) n p /\ sigmapi b n q ==> sigmapi b n (p --> q)) /\
19 (!b n p q. (!b. sigmapi b n p) /\ (!b. sigmapi b n q)
20 ==> sigmapi b n (p <-> q)) /\
21 (!n x p. sigmapi T n p /\ ~(n = 0) ==> sigmapi T n (??x p)) /\
22 (!n x p. sigmapi F n p /\ ~(n = 0) ==> sigmapi F n (!!x p)) /\
23 (!b n x p t. sigmapi b n p /\ ~(x IN FVT t)
24 ==> sigmapi b n (??x (V x << t && p))) /\
25 (!b n x p t. sigmapi b n p /\ ~(x IN FVT t)
26 ==> sigmapi b n (??x (V x <<= t && p))) /\
27 (!b n x p t. sigmapi b n p /\ ~(x IN FVT t)
28 ==> sigmapi b n (!!x (V x << t --> p))) /\
29 (!b n x p t. sigmapi b n p /\ ~(x IN FVT t)
30 ==> sigmapi b n (!!x (V x <<= t --> p))) /\
31 (!b c n p. sigmapi b n p ==> sigmapi c (n + 1) p)`;;
33 let SIGMA = new_definition `SIGMA = sigmapi T`;;
34 let PI = new_definition `PI = sigmapi F`;;
35 let DELTA = new_definition `DELTA n p <=> SIGMA n p /\ PI n p`;;
37 let SIGMAPI_PROP = prove
38 (`(!n b. sigmapi b n False <=> T) /\
39 (!n b. sigmapi b n True <=> T) /\
40 (!n b s t. sigmapi b n (s === t) <=> T) /\
41 (!n b s t. sigmapi b n (s << t) <=> T) /\
42 (!n b s t. sigmapi b n (s <<= t) <=> T) /\
43 (!n b p. sigmapi b n (Not p) <=> sigmapi (~b) n p) /\
44 (!n b p q. sigmapi b n (p && q) <=> sigmapi b n p /\ sigmapi b n q) /\
45 (!n b p q. sigmapi b n (p || q) <=> sigmapi b n p /\ sigmapi b n q) /\
46 (!n b p q. sigmapi b n (p --> q) <=> sigmapi (~b) n p /\ sigmapi b n q) /\
47 (!n b p q. sigmapi b n (p <-> q) <=> (sigmapi b n p /\ sigmapi (~b) n p) /\
48 (sigmapi b n q /\ sigmapi (~b) n q))`,
49 REWRITE_TAC[sigmapi_RULES] THEN
50 GEN_REWRITE_TAC DEPTH_CONV [AND_FORALL_THM] THEN
51 INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; SUC_SUB1] THEN
52 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [sigmapi_CASES] THEN
53 REWRITE_TAC[form_DISTINCT; form_INJ] THEN
54 REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1;
56 REWRITE_TAC[ARITH_RULE `~(0 = n + 1)`] THEN
57 REWRITE_TAC[ARITH_RULE `(SUC m = n + 1) <=> (n = m)`; UNWIND_THM2] THEN
58 ASM_REWRITE_TAC[] THEN
59 BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[ADD1] THEN
60 REWRITE_TAC[CONJ_ACI] THEN
61 REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THEN
62 MESON_TAC[sigmapi_RULES]);;
64 let SIGMAPI_MONO_LEMMA = prove
65 (`(!b n p. sigmapi b n p ==> sigmapi b (n + 1) p) /\
66 (!b n p. ~(n = 0) /\ sigmapi b (n - 1) p ==> sigmapi b n p) /\
67 (!b n p. ~(n = 0) /\ sigmapi (~b) (n - 1) p ==> sigmapi b n p)`,
71 FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (ARITH_RULE
72 `~(n = 0) ==> (n = (n - 1) + 1)`))] THEN
73 POP_ASSUM MP_TAC THEN ASM_MESON_TAC[sigmapi_RULES]);;
75 let SIGMAPI_REV_EXISTS = prove
76 (`!n b x p. sigmapi b n (??x p) ==> sigmapi b n p`,
77 MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
78 REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [sigmapi_CASES] THEN
79 REWRITE_TAC[form_DISTINCT; form_INJ] THEN
80 REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
81 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SIGMAPI_PROP] THEN
82 ASM_MESON_TAC[ARITH_RULE `n < n + 1`; sigmapi_RULES]);;
84 let SIGMAPI_REV_FORALL = prove
85 (`!n b x p. sigmapi b n (!!x p) ==> sigmapi b n p`,
86 MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
87 REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [sigmapi_CASES] THEN
88 REWRITE_TAC[form_DISTINCT; form_INJ] THEN
89 REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
90 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SIGMAPI_PROP] THEN
91 ASM_MESON_TAC[ARITH_RULE `n < n + 1`; sigmapi_RULES]);;
93 let SIGMAPI_CLAUSES_CODE = prove
94 (`(!n b. sigmapi b n False <=> T) /\
95 (!n b. sigmapi b n True <=> T) /\
96 (!n b s t. sigmapi b n (s === t) <=> T) /\
97 (!n b s t. sigmapi b n (s << t) <=> T) /\
98 (!n b s t. sigmapi b n (s <<= t) <=> T) /\
99 (!n b p. sigmapi b n (Not p) <=> sigmapi (~b) n p) /\
100 (!n b p q. sigmapi b n (p && q) <=> sigmapi b n p /\ sigmapi b n q) /\
101 (!n b p q. sigmapi b n (p || q) <=> sigmapi b n p /\ sigmapi b n q) /\
102 (!n b p q. sigmapi b n (p --> q) <=> sigmapi (~b) n p /\ sigmapi b n q) /\
103 (!n b p q. sigmapi b n (p <-> q) <=> (sigmapi b n p /\ sigmapi (~b) n p) /\
104 (sigmapi b n q /\ sigmapi (~b) n q)) /\
105 (!n b x p. sigmapi b n (??x p) <=>
107 ?q t. (p = (V x << t && q) \/ p = (V x <<= t && q)) /\
110 else ~(n = 0) /\ sigmapi (~b) (n - 1) (??x p)) /\
111 (!n b x p. sigmapi b n (!!x p) <=>
113 ?q t. (p = (V x << t --> q) \/ p = (V x <<= t --> q)) /\
116 else ~(n = 0) /\ sigmapi (~b) (n - 1) (!!x p))`,
117 REWRITE_TAC[SIGMAPI_PROP] THEN CONJ_TAC THEN REPEAT GEN_TAC THEN
118 GEN_REWRITE_TAC LAND_CONV [sigmapi_CASES] THEN
119 REWRITE_TAC[form_DISTINCT; form_INJ] THEN
120 REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
121 ONCE_REWRITE_TAC[TAUT `a \/ b \/ c \/ d <=> (b \/ c) \/ (a \/ d)`] THEN
122 REWRITE_TAC[CONJ_ASSOC; OR_EXISTS_THM; GSYM RIGHT_OR_DISTRIB] THEN
124 `(if b /\ c \/ d then e else c /\ f) <=>
125 d /\ e \/ c /\ ~d /\ (if b then e else f)`] THEN
126 MATCH_MP_TAC(TAUT `(a <=> a') /\ (~a' ==> (b <=> b'))
127 ==> (a \/ b <=> a' \/ b')`) THEN
129 [REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
130 REPEAT(AP_TERM_TAC THEN ABS_TAC) THEN
131 EQ_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
132 REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[SIGMAPI_PROP] THEN
135 (ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH_RULE `~(0 = n + 1)`]) THEN
136 ASM_SIMP_TAC[ARITH_RULE `~(n = 0) ==> (n = m + 1 <=> m = n - 1)`] THEN
137 REWRITE_TAC[UNWIND_THM2] THEN
138 W(fun (asl,w) -> ASM_CASES_TAC (find_term is_exists w)) THEN
139 ASM_REWRITE_TAC[CONTRAPOS_THM] THENL
140 [DISCH_THEN(DISJ_CASES_THEN ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
141 FIRST_X_ASSUM(CHOOSE_THEN(MP_TAC o MATCH_MP SIGMAPI_REV_EXISTS)) THEN
142 DISCH_THEN(MP_TAC o MATCH_MP(last(CONJUNCTS sigmapi_RULES))) THEN
143 ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `~(n = 0) ==> 1 <= n`];
144 ASM_CASES_TAC `b:bool` THEN
145 ASM_REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THENL
146 [DISCH_THEN(CHOOSE_THEN(MP_TAC o MATCH_MP SIGMAPI_REV_EXISTS)) THEN
147 DISCH_THEN(MP_TAC o MATCH_MP(last(CONJUNCTS sigmapi_RULES))) THEN
148 ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `~(n = 0) ==> 1 <= n`];
149 REWRITE_TAC[EXISTS_BOOL_THM] THEN
150 REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THEN
151 ONCE_REWRITE_TAC[sigmapi_CASES] THEN
152 REWRITE_TAC[form_DISTINCT; form_INJ] THEN ASM_MESON_TAC[]];
153 DISCH_THEN(DISJ_CASES_THEN ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
154 FIRST_X_ASSUM(CHOOSE_THEN(MP_TAC o MATCH_MP SIGMAPI_REV_FORALL)) THEN
155 DISCH_THEN(MP_TAC o MATCH_MP(last(CONJUNCTS sigmapi_RULES))) THEN
156 ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `~(n = 0) ==> 1 <= n`];
157 ASM_CASES_TAC `b:bool` THEN
158 ASM_REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THENL
159 [REWRITE_TAC[EXISTS_BOOL_THM] THEN
160 REWRITE_TAC[TAUT `(a \/ b <=> a) <=> (b ==> a)`] THEN
161 ONCE_REWRITE_TAC[sigmapi_CASES] THEN
162 REWRITE_TAC[form_DISTINCT; form_INJ] THEN ASM_MESON_TAC[];
163 DISCH_THEN(CHOOSE_THEN(MP_TAC o MATCH_MP SIGMAPI_REV_FORALL)) THEN
164 DISCH_THEN(MP_TAC o MATCH_MP(last(CONJUNCTS sigmapi_RULES))) THEN
165 ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `~(n = 0) ==> 1 <= n`]]]);;
167 let SIGMAPI_CLAUSES = prove
168 (`(!n b. sigmapi b n False <=> T) /\
169 (!n b. sigmapi b n True <=> T) /\
170 (!n b s t. sigmapi b n (s === t) <=> T) /\
171 (!n b s t. sigmapi b n (s << t) <=> T) /\
172 (!n b s t. sigmapi b n (s <<= t) <=> T) /\
173 (!n b p. sigmapi b n (Not p) <=> sigmapi (~b) n p) /\
174 (!n b p q. sigmapi b n (p && q) <=> sigmapi b n p /\ sigmapi b n q) /\
175 (!n b p q. sigmapi b n (p || q) <=> sigmapi b n p /\ sigmapi b n q) /\
176 (!n b p q. sigmapi b n (p --> q) <=> sigmapi (~b) n p /\ sigmapi b n q) /\
177 (!n b p q. sigmapi b n (p <-> q) <=> (sigmapi b n p /\ sigmapi (~b) n p) /\
178 (sigmapi b n q /\ sigmapi (~b) n q)) /\
179 (!n b x p. sigmapi b n (??x p) <=>
181 ?q t. (p = (V x << t && q) \/ p = (V x <<= t && q)) /\
184 else 2 <= n /\ sigmapi (~b) (n - 1) p) /\
185 (!n b x p. sigmapi b n (!!x p) <=>
187 ?q t. (p = (V x << t --> q) \/ p = (V x <<= t --> q)) /\
190 else 2 <= n /\ sigmapi (~b) (n - 1) p)`,
191 REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
192 GEN_REWRITE_TAC LAND_CONV [SIGMAPI_CLAUSES_CODE] THEN
194 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN
195 BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[] THEN
196 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
197 GEN_REWRITE_TAC LAND_CONV [SIGMAPI_CLAUSES_CODE] THEN
198 ASM_REWRITE_TAC[ARITH_RULE `~(n - 1 = 0) <=> 2 <= n`] THEN
201 (* ------------------------------------------------------------------------- *)
202 (* Show that it respects substitution. *)
203 (* ------------------------------------------------------------------------- *)
205 let SIGMAPI_FORMSUBST = prove
206 (`!p v n b. sigmapi b n p ==> sigmapi b n (formsubst v p)`,
207 MATCH_MP_TAC form_INDUCT THEN
208 REWRITE_TAC[SIGMAPI_CLAUSES; formsubst] THEN SIMP_TAC[] THEN
209 REWRITE_TAC[AND_FORALL_THM] THEN MAP_EVERY X_GEN_TAC [`x:num`; `p:form`] THEN
210 MATCH_MP_TAC(TAUT `(a ==> b /\ c) ==> (a ==> b) /\ (a ==> c)`) THEN
211 DISCH_TAC THEN REWRITE_TAC[AND_FORALL_THM] THEN
212 MAP_EVERY X_GEN_TAC [`i:num->term`; `n:num`; `b:bool`] THEN
213 REWRITE_TAC[FV] THEN LET_TAC THEN
214 CONV_TAC(ONCE_DEPTH_CONV let_CONV) THEN
215 REWRITE_TAC[SIGMAPI_CLAUSES] THEN
216 ONCE_REWRITE_TAC[TAUT
217 `((if p \/ q then x else y) ==> (if p \/ q' then x' else y')) <=>
219 (~p ==> (if q then x else y) ==> (if q' then x' else y'))`] THEN
220 ASM_SIMP_TAC[] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
221 CONJ_TAC THEN DISCH_THEN(K ALL_TAC) THEN MATCH_MP_TAC(TAUT
222 `(p ==> p') /\ (x ==> x') /\ (y ==> y') /\ (y ==> x)
223 ==> (if p then x else y) ==> (if p' then x' else y')`) THEN
224 ASM_SIMP_TAC[SIGMAPI_MONO_LEMMA; ARITH_RULE `2 <= n ==> ~(n = 0)`] THEN
225 STRIP_TAC THEN ASM_REWRITE_TAC[formsubst; form_INJ; termsubst] THEN
226 REWRITE_TAC[form_DISTINCT] THEN
227 ONCE_REWRITE_TAC[TAUT `((a /\ b) /\ c) /\ d <=> b /\ c /\ a /\ d`] THEN
228 REWRITE_TAC[UNWIND_THM1; termsubst; VALMOD_BASIC] THEN
229 REWRITE_TAC[TERMSUBST_FVT; IN_ELIM_THM; NOT_EXISTS_THM] THEN
230 X_GEN_TAC `y:num` THEN REWRITE_TAC[valmod] THEN
231 (COND_CASES_TAC THENL [ASM_MESON_TAC[]; ALL_TAC]) THEN
232 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
233 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (funpow 2 LAND_CONV) [SYM th]) THEN
234 FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[FV; FVT] THEN
235 REWRITE_TAC[IN_DELETE; IN_UNION; IN_SING; GSYM DISJ_ASSOC] THEN
236 REWRITE_TAC[TAUT `(a \/ b \/ c) /\ ~a <=> ~a /\ b \/ ~a /\ c`] THEN
237 (COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]]) THEN
238 W(fun (asl,w) -> let t = lhand(rand w) in
239 MP_TAC(SPEC (rand(rand t)) VARIANT_THM) THEN
240 SPEC_TAC(t,`u:num`)) THEN
241 REWRITE_TAC[CONTRAPOS_THM; FORMSUBST_FV; IN_ELIM_THM; FV] THEN
242 GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC `y:num` THEN
243 ASM_REWRITE_TAC[valmod; IN_UNION]);;
245 (* ------------------------------------------------------------------------- *)
246 (* Hence all our main concepts are OK. *)
247 (* ------------------------------------------------------------------------- *)
249 let SIGMAPI_TAC ths =
250 REPEAT STRIP_TAC THEN
252 TRY(MATCH_MP_TAC SIGMAPI_FORMSUBST) THEN
253 let ths' = ths @ [SIGMAPI_CLAUSES; form_DISTINCT;
254 form_INJ; GSYM CONJ_ASSOC; UNWIND_THM1; GSYM EXISTS_REFL;
255 FVT; IN_SING; ARITH_EQ] in
256 REWRITE_TAC ths' THEN ASM_SIMP_TAC ths';;
258 let SIGMAPI_DIVIDES = prove
259 (`!n s t. sigmapi b n (arith_divides s t)`,
260 SIGMAPI_TAC[arith_divides]);;
262 let SIGMAPI_PRIME = prove
263 (`!n t. sigmapi b n (arith_prime t)`,
264 SIGMAPI_TAC[arith_prime; SIGMAPI_DIVIDES]);;
266 let SIGMAPI_PRIMEPOW = prove
267 (`!n s t. sigmapi b n (arith_primepow s t)`,
268 SIGMAPI_TAC[arith_primepow; SIGMAPI_DIVIDES; SIGMAPI_PRIME]);;
270 let SIGMAPI_RTC = prove
271 (`(!s t. sigmapi T 1 (R s t))
272 ==> !s t. sigmapi T 1 (arith_rtc R s t)`,
273 REPEAT STRIP_TAC THEN REWRITE_TAC[arith_rtc] THEN
274 MATCH_MP_TAC SIGMAPI_FORMSUBST THEN
275 REWRITE_TAC[SIGMAPI_CLAUSES; form_INJ; GSYM CONJ_ASSOC; UNWIND_THM1;
276 GSYM EXISTS_REFL; FVT; IN_SING; ARITH_EQ; SIGMAPI_DIVIDES;
277 SIGMAPI_PRIME; SIGMAPI_PRIMEPOW; form_DISTINCT] THEN
280 let SIGMAPI_RTCP = prove
281 (`(!s t u. sigmapi T 1 (R s t u))
282 ==> !s t u. sigmapi T 1 (arith_rtcp R s t u)`,
283 REPEAT STRIP_TAC THEN REWRITE_TAC[arith_rtcp] THEN
284 MATCH_MP_TAC SIGMAPI_FORMSUBST THEN
285 REWRITE_TAC[SIGMAPI_CLAUSES; form_INJ; GSYM CONJ_ASSOC; UNWIND_THM1;
286 GSYM EXISTS_REFL; FVT; IN_SING; ARITH_EQ; SIGMAPI_DIVIDES;
287 SIGMAPI_PRIME; SIGMAPI_PRIMEPOW; form_DISTINCT] THEN
290 let SIGMAPI_TERM1 = prove
291 (`!s t. sigmapi T 1 (arith_term1 s t)`,
292 SIGMAPI_TAC[arith_term1]);;
294 let SIGMAPI_TERM = prove
295 (`!t. sigmapi T 1 (arith_term t)`,
296 SIGMAPI_TAC[arith_term; SIGMAPI_RTC; SIGMAPI_TERM1]);;
298 let SIGMAPI_FORM1 = prove
299 (`!s t. sigmapi T 1 (arith_form1 s t)`,
300 SIGMAPI_TAC[arith_form1; SIGMAPI_TERM]);;
302 let SIGMAPI_FORM = prove
303 (`!t. sigmapi T 1 (arith_form t)`,
304 SIGMAPI_TAC[arith_form; SIGMAPI_RTC; SIGMAPI_FORM1]);;
306 let SIGMAPI_FREETERM1 = prove
307 (`!s t u. sigmapi T 1 (arith_freeterm1 s t u)`,
308 SIGMAPI_TAC[arith_freeterm1]);;
310 let SIGMAPI_FREETERM = prove
311 (`!s t. sigmapi T 1 (arith_freeterm s t)`,
312 SIGMAPI_TAC[arith_freeterm; SIGMAPI_FREETERM1; SIGMAPI_RTCP]);;
314 let SIGMAPI_FREEFORM1 = prove
315 (`!s t u. sigmapi T 1 (arith_freeform1 s t u)`,
316 SIGMAPI_TAC[arith_freeform1; SIGMAPI_FREETERM; SIGMAPI_FORM]);;
318 let SIGMAPI_FREEFORM = prove
319 (`!s t. sigmapi T 1 (arith_freeform s t)`,
320 SIGMAPI_TAC[arith_freeform; SIGMAPI_FREEFORM1; SIGMAPI_RTCP]);;
322 let SIGMAPI_AXIOM = prove
323 (`!t. sigmapi T 1 (arith_axiom t)`,
324 SIGMAPI_TAC[arith_axiom; SIGMAPI_FREEFORM; SIGMAPI_FREETERM; SIGMAPI_FORM;
327 let SIGMAPI_PROV1 = prove
328 (`!A. (!t. sigmapi T 1 (A t)) ==> !s t. sigmapi T 1 (arith_prov1 A s t)`,
329 SIGMAPI_TAC[arith_prov1; SIGMAPI_AXIOM]);;
331 let SIGMAPI_PROV = prove
332 (`(!t. sigmapi T 1 (A t)) ==> !t. sigmapi T 1 (arith_prov A t)`,
333 SIGMAPI_TAC[arith_prov; SIGMAPI_PROV1; SIGMAPI_RTC]);;
335 let SIGMAPI_PRIMRECSTEP = prove
336 (`(!s t u. sigmapi T 1 (R s t u))
337 ==> !s t. sigmapi T 1 (arith_primrecstep R s t)`,
338 SIGMAPI_TAC[arith_primrecstep]);;
340 let SIGMAPI_PRIMREC = prove
341 (`(!s t u. sigmapi T 1 (R s t u))
342 ==> !s t. sigmapi T 1 (arith_primrec R c s t)`,
343 SIGMAPI_TAC[arith_primrec; SIGMAPI_PRIMRECSTEP; SIGMAPI_RTC]);;
345 let SIGMAPI_GNUMERAL1 = prove
346 (`!s t. sigmapi T 1 (arith_gnumeral1 s t)`,
347 SIGMAPI_TAC[arith_gnumeral1]);;
349 let SIGMAPI_GNUMERAL = prove
350 (`!s t. sigmapi T 1 (arith_gnumeral s t)`,
351 SIGMAPI_TAC[arith_gnumeral; arith_gnumeral1';
352 SIGMAPI_GNUMERAL1; SIGMAPI_RTC]);;
354 let SIGMAPI_QSUBST = prove
355 (`!x n p. sigmapi T 1 p ==> sigmapi T 1 (qsubst(x,n) p)`,
356 SIGMAPI_TAC[qsubst]);;
358 let SIGMAPI_QDIAG = prove
359 (`!x s t. sigmapi T 1 (arith_qdiag x s t)`,
360 SIGMAPI_TAC[arith_qdiag; SIGMAPI_GNUMERAL]);;
362 let SIGMAPI_DIAGONALIZE = prove
363 (`!x p. sigmapi T 1 p ==> sigmapi T 1 (diagonalize x p)`,
364 SIGMAPI_TAC[diagonalize; SIGMAPI_QDIAG;
365 SIGMAPI_FORMSUBST; LET_DEF; LET_END_DEF]);;
367 let SIGMAPI_FIXPOINT = prove
368 (`!x p. sigmapi T 1 p ==> sigmapi T 1 (fixpoint x p)`,
369 SIGMAPI_TAC[fixpoint; qdiag; SIGMAPI_QSUBST; SIGMAPI_DIAGONALIZE]);;
371 (* ------------------------------------------------------------------------- *)
372 (* The Godel sentence, "H" being Sigma and "G" being Pi. *)
373 (* ------------------------------------------------------------------------- *)
375 let hsentence = new_definition
377 fixpoint 0 (arith_prov Arep (arith_pair (numeral 4) (V 0)))`;;
379 let gsentence = new_definition
380 `gsentence Arep = Not(hsentence Arep)`;;
382 let FV_HSENTENCE = prove
383 (`!Arep. (!t. FV(Arep t) = FVT t) ==> (FV(hsentence Arep) = {})`,
384 SIMP_TAC[hsentence; FV_FIXPOINT; FV_PROV] THEN
385 REWRITE_TAC[FVT_PAIR; FVT_NUMERAL; FVT; UNION_EMPTY; DELETE_INSERT;
388 let FV_GSENTENCE = prove
389 (`!Arep. (!t. FV(Arep t) = FVT t) ==> (FV(gsentence Arep) = {})`,
390 SIMP_TAC[gsentence; FV_HSENTENCE; FV]);;
392 let SIGMAPI_HSENTENCE = prove
393 (`!Arep. (!t. sigmapi T 1 (Arep t)) ==> sigmapi T 1 (hsentence Arep)`,
394 SIGMAPI_TAC[hsentence; SIGMAPI_FIXPOINT; SIGMAPI_PROV]);;
396 let SIGMAPI_GSENTENCE = prove
397 (`!Arep. (!t. sigmapi T 1 (Arep t)) ==> sigmapi F 1 (gsentence Arep)`,
398 SIGMAPI_TAC[gsentence; SIGMAPI_HSENTENCE]);;
400 (* ------------------------------------------------------------------------- *)
401 (* Hence the key fixpoint properties. *)
402 (* ------------------------------------------------------------------------- *)
404 let HSENTENCE_FIX_STRONG = prove
406 (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
407 ==> !v. holds v (hsentence Arep) <=> A |-- Not(hsentence Arep)`,
408 REWRITE_TAC[hsentence; true_def; HOLDS_FIXPOINT] THEN
409 REPEAT STRIP_TAC THEN
410 FIRST_ASSUM(MP_TAC o MATCH_MP ARITH_PROV) THEN
411 REWRITE_TAC[IN] THEN CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
412 DISCH_TAC THEN ASM_REWRITE_TAC[ARITH_PAIR; TERMVAL_NUMERAL] THEN
413 REWRITE_TAC[termval; valmod; GSYM gform] THEN REWRITE_TAC[PROV_THM]);;
415 let HSENTENCE_FIX = prove
417 (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
418 ==> (true(hsentence Arep) <=> A |-- Not(hsentence Arep))`,
419 REWRITE_TAC[true_def] THEN MESON_TAC[HSENTENCE_FIX_STRONG]);;
421 let GSENTENCE_FIX = prove
423 (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
424 ==> (true(gsentence Arep) <=> ~(A |-- gsentence Arep))`,
425 REWRITE_TAC[true_def; holds; gsentence] THEN
426 MESON_TAC[HSENTENCE_FIX_STRONG]);;
428 (* ------------------------------------------------------------------------- *)
429 (* Auxiliary concepts. *)
430 (* ------------------------------------------------------------------------- *)
432 let ground = new_definition
433 `ground t <=> (FVT t = {})`;;
435 let complete_for = new_definition
436 `complete_for P A <=> !p. P p /\ true p ==> A |-- p`;;
438 let sound_for = new_definition
439 `sound_for P A <=> !p. P p /\ A |-- p ==> true p`;;
441 let consistent = new_definition
442 `consistent A <=> ~(?p. A |-- p /\ A |-- Not p)`;;
444 let CONSISTENT_ALT = prove
445 (`!A p. A |-- p /\ A |-- Not p <=> A |-- False`,
446 MESON_TAC[proves_RULES; axiom_RULES]);;
448 (* ------------------------------------------------------------------------- *)
449 (* The purest and most symmetric and beautiful form of G1. *)
450 (* ------------------------------------------------------------------------- *)
452 let DEFINABLE_BY_ONEVAR = prove
453 (`definable_by (SIGMA 1) s <=>
454 ?p x. SIGMA 1 p /\ (FV p = {x}) /\ !v. holds v p <=> (v x) IN s`,
455 REWRITE_TAC[definable_by; SIGMA] THEN
456 EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
457 DISCH_THEN(X_CHOOSE_THEN `p:form` (X_CHOOSE_TAC `x:num`)) THEN
458 EXISTS_TAC `(V x === V x) && formsubst (\y. if y = x then V x else Z) p` THEN
459 EXISTS_TAC `x:num` THEN ASM_SIMP_TAC[SIGMAPI_CLAUSES; SIGMAPI_FORMSUBST] THEN
460 ASM_REWRITE_TAC[HOLDS_FORMSUBST; FORMSUBST_FV; FV; holds] THEN
461 REWRITE_TAC[COND_RAND; EXTENSION; IN_ELIM_THM; IN_SING; FVT; IN_UNION;
462 COND_EXPAND; NOT_IN_EMPTY; o_THM; termval] THEN
465 let CLOSED_NOT_TRUE = prove
466 (`!p. closed p ==> (true(Not p) <=> ~(true p))`,
467 REWRITE_TAC[closed; true_def; holds] THEN
468 MESON_TAC[HOLDS_VALUATION; NOT_IN_EMPTY]);;
471 (`!A. definable_by (SIGMA 1) (IMAGE gform A)
472 ==> ?G. PI 1 G /\ closed G /\
473 (sound_for (PI 1 INTER closed) A ==> true G /\ ~(A |-- G)) /\
474 (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))`,
476 REWRITE_TAC[sound_for; INTER; IN_ELIM_THM; DEFINABLE_BY_ONEVAR] THEN
477 DISCH_THEN(X_CHOOSE_THEN `Arep:form` (X_CHOOSE_THEN `a:num`
478 STRIP_ASSUME_TAC)) THEN
479 MP_TAC(SPECL [`A:form->bool`; `\t. formsubst ((a |-> t) V) Arep`]
481 REWRITE_TAC[] THEN ANTS_TAC THENL
482 [ASM_REWRITE_TAC[HOLDS_FORMSUBST] THEN REWRITE_TAC[termval; valmod; o_THM];
484 STRIP_TAC THEN EXISTS_TAC `gsentence (\t. formsubst ((a |-> t) V) Arep)` THEN
485 ASM_REWRITE_TAC[] THEN
486 MATCH_MP_TAC(TAUT `a /\ b /\ (a /\ b ==> c /\ d) ==> a /\ b /\ c /\ d`) THEN
487 REPEAT CONJ_TAC THENL
488 [REWRITE_TAC[PI] THEN MATCH_MP_TAC SIGMAPI_GSENTENCE THEN
489 RULE_ASSUM_TAC(REWRITE_RULE[SIGMA]) THEN ASM_SIMP_TAC[SIGMAPI_FORMSUBST];
490 REWRITE_TAC[closed] THEN MATCH_MP_TAC FV_GSENTENCE THEN
491 ASM_REWRITE_TAC[FORMSUBST_FV; EXTENSION; IN_ELIM_THM; IN_SING;
492 valmod; UNWIND_THM2];
494 ABBREV_TAC `G = gsentence (\t. formsubst ((a |-> t) V) Arep)` THEN
495 REPEAT STRIP_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
496 SUBGOAL_THEN `true(Not G)` MP_TAC THENL
497 [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN] THEN
498 REWRITE_TAC[SIGMA; SIGMAPI_CLAUSES] THEN ASM_MESON_TAC[closed; FV; PI];
500 FIRST_ASSUM(SUBST1_TAC o MATCH_MP CLOSED_NOT_TRUE) THEN
501 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
502 SUBGOAL_THEN `true False` MP_TAC THENL
503 [ALL_TAC; REWRITE_TAC[true_def; holds]] THEN
504 FIRST_X_ASSUM MATCH_MP_TAC THEN
505 REWRITE_TAC[closed; IN; SIGMA; SIGMAPI_CLAUSES; FV] THEN
506 ASM_MESON_TAC[CONSISTENT_ALT]);;
508 (* ------------------------------------------------------------------------- *)
509 (* Some more familiar variants. *)
510 (* ------------------------------------------------------------------------- *)
512 let COMPLETE_SOUND_SENTENCE = prove
513 (`consistent A /\ complete_for (sigmapi (~b) n INTER closed) A
514 ==> sound_for (sigmapi b n INTER closed) A`,
515 REWRITE_TAC[consistent; sound_for; complete_for; IN; INTER; IN_ELIM_THM] THEN
516 REWRITE_TAC[NOT_EXISTS_THM] THEN
517 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
518 DISCH_THEN(fun th -> X_GEN_TAC `p:form` THEN MP_TAC(SPEC `Not p` th)) THEN
519 REWRITE_TAC[SIGMAPI_CLAUSES] THEN
520 REWRITE_TAC[closed; FV; true_def; holds] THEN
521 ASM_MESON_TAC[HOLDS_VALUATION; NOT_IN_EMPTY]);;
524 (`!A. consistent A /\
525 complete_for (SIGMA 1 INTER closed) A /\
526 definable_by (SIGMA 1) (IMAGE gform A)
527 ==> ?G. PI 1 G /\ closed G /\ true G /\ ~(A |-- G) /\
528 (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))`,
529 REWRITE_TAC[SIGMA] THEN REPEAT STRIP_TAC THEN
530 MP_TAC(SPEC `A:form->bool` G1) THEN ASM_REWRITE_TAC[SIGMA; PI] THEN
531 MATCH_MP_TAC MONO_EXISTS THEN ASM_SIMP_TAC[COMPLETE_SOUND_SENTENCE]);;