Theories.v 38.2 KB
 Pierre Letouzey committed Feb 26, 2019 1 2 3 `````` (** Notion of 1st order theories *) `````` Pierre Letouzey committed Apr 02, 2019 4 ``````Require Import Arith Omega Defs Proofs Mix Meta Countable. `````` Pierre Letouzey committed Apr 09, 2019 5 ``````Require Import Coq.Program.Equality. `````` Pierre Letouzey committed Feb 26, 2019 6 7 8 ``````Import ListNotations. Local Open Scope bool_scope. Local Open Scope eqb_scope. `````` Pierre Letouzey committed Apr 02, 2019 9 `````` `````` Pierre Letouzey committed Apr 09, 2019 10 11 12 13 14 ``````(** Well-formed formulas over a particular signature, that are moreover : - with bounded variables that are indeed bounded - without free variables *) `````` Pierre Letouzey committed Apr 09, 2019 15 ``````Definition Wf (sign:signature) (A:formula) := `````` Pierre Letouzey committed Apr 04, 2019 16 `````` check sign A = true /\ BClosed A /\ FClosed A. `````` Pierre Letouzey committed Feb 26, 2019 17 `````` `````` Pierre Letouzey committed Apr 09, 2019 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 ``````Hint Unfold Wf. Lemma Wf_dec sign A : { Wf sign A }+{ ~Wf sign A}. Proof. destruct (check sign A) eqn:C. - destruct (level A =? 0) eqn:L. + destruct (Vars.is_empty (fvars A)) eqn:E. * left. repeat split; auto. now apply eqb_eq. now apply Vars.is_empty_spec. * right; intros (_ & _ & E'). apply Vars.is_empty_spec in E'. congruence. + right; intros (_ & L' & _). apply eqb_eq in L'. congruence. - right; intros (C' & _ & _). congruence. Qed. Lemma False_wf sign : Wf sign False. Proof. repeat split. red. cbn. varsdec. Qed. Lemma Op_wf sign o A B : Wf sign (Op o A B) <-> Wf sign A /\ Wf sign B. Proof. unfold Wf, BClosed, FClosed. cbn. rewrite lazy_andb_iff. rewrite max_0. intuition. Qed. Lemma bsubst_cst_wf sign c A : `````` Pierre Letouzey committed Apr 09, 2019 49 `````` sign.(funsymbs) c = Some 0 -> `````` Pierre Letouzey committed Apr 09, 2019 50 51 52 53 54 55 56 57 58 `````` Wf sign (∃A) -> Wf sign (bsubst 0 (Cst c) A). Proof. intros E (CK & BC & FC). repeat split; unfold BClosed, FClosed in *; cbn in *. - rewrite check_bsubst; auto. cbn. now rewrite E, eqb_refl. - apply Nat.le_0_r, level_bsubst; auto with *. - rewrite bsubst_fvars. cbn - [Vars.union]. varsdec. Qed. `````` Pierre Letouzey committed Apr 09, 2019 59 ``````Definition ValidDerivOn logic (sign:signature) d := `````` Pierre Letouzey committed Apr 04, 2019 60 `````` check sign d = true /\ BClosed d /\ Valid logic d. `````` Pierre Letouzey committed Apr 03, 2019 61 `````` `````` Pierre Letouzey committed Feb 26, 2019 62 ``````Record theory := `````` Pierre Letouzey committed Apr 09, 2019 63 `````` { sign :> signature; `````` Pierre Letouzey committed Apr 02, 2019 64 `````` IsAxiom : formula -> Prop; `````` Pierre Letouzey committed Apr 09, 2019 65 `````` WfAxiom : forall A, IsAxiom A -> Wf sign A }. `````` Pierre Letouzey committed Apr 02, 2019 66 67 `````` Implicit Type th : theory. `````` Pierre Letouzey committed Feb 26, 2019 68 69 70 71 `````` Section SomeLogic. Variable logic : Defs.logic. `````` Pierre Letouzey committed Apr 09, 2019 72 73 ``````Definition IsTheoremStrict th (T:formula) := Wf th T /\ `````` Pierre Letouzey committed Apr 03, 2019 74 75 76 77 78 `````` exists d axs, ValidDerivOn logic th d /\ Forall th.(IsAxiom) axs /\ Claim d (axs ⊢ T). `````` Pierre Letouzey committed Apr 02, 2019 79 ``````Definition IsTheorem th T := `````` Pierre Letouzey committed Apr 09, 2019 80 `````` Wf th T /\ `````` Pierre Letouzey committed Apr 03, 2019 81 82 83 84 `````` exists axs, Forall th.(IsAxiom) axs /\ Pr logic (axs ⊢ T). `````` Pierre Letouzey committed Apr 09, 2019 85 86 ``````Hint Unfold IsTheorem IsTheoremStrict. `````` Pierre Letouzey committed Apr 03, 2019 87 88 89 90 91 92 ``````(** We can "fix" a proof made with things not in the signature, or a signature badly used, or with remaining bounded vars. *) Lemma thm_alt th T : IsTheorem th T <-> IsTheoremStrict th T. Proof. `````` Pierre Letouzey committed Apr 04, 2019 93 `````` split. `````` Pierre Letouzey committed Apr 09, 2019 94 95 96 `````` - intros (WF & axs & F & PR). split; auto. rewrite Provable_alt in PR. destruct PR as (d & V & C). `````` Pierre Letouzey committed Apr 04, 2019 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 `````` assert (Hx := fresh_var_ok (fvars d)). set (x := fresh_var (fvars d)) in *. assert (Hy := fresh_var_ok (Vars.add x (fvars d))). set (y := fresh_var (Vars.add x (fvars d))) in *. exists (forcelevel_deriv y (restrict_deriv th x d)). exists axs; repeat split; auto. + rewrite <- restrict_forcelevel_deriv. apply restrict_deriv_check. + apply forcelevel_deriv_bclosed. + apply forcelevel_deriv_valid. * rewrite restrict_deriv_fvars. varsdec. * apply restrict_valid; auto. + rewrite Forall_forall in F. unfold Claim. rewrite claim_forcelevel, claim_restrict, C. cbn. f_equal. * assert (check th axs = true). { unfold check, check_list. apply forallb_forall. intros A HA. apply WfAxiom; auto. } rewrite check_restrict_ctx_id by auto. apply forcelevel_ctx_id. unfold BClosed, level, level_list. apply list_max_map_0. intros A HA. apply (WfAxiom th A); auto. `````` Pierre Letouzey committed Apr 09, 2019 123 `````` * rewrite check_restrict_id by apply WF. `````` Pierre Letouzey committed Apr 04, 2019 124 `````` apply forcelevel_id. `````` Pierre Letouzey committed Apr 09, 2019 125 `````` assert (level T = 0) by apply WF. `````` Pierre Letouzey committed Apr 04, 2019 126 127 128 129 130 131 132 133 `````` auto with *. - intros (CL & d & axs & V & F & C). split; auto. exists axs; split; auto. rewrite Provable_alt. exists d; split; auto. apply V. Qed. `````` Pierre Letouzey committed Apr 02, 2019 134 135 136 137 138 139 140 141 142 143 144 145 `````` Lemma ax_thm th A : IsAxiom th A -> IsTheorem th A. Proof. intros Ax. repeat split. - now apply WfAxiom. - eapply WfAxiom; eauto. - eapply WfAxiom; eauto. - exists [A]; split. + apply Forall_forall. simpl; intuition; now subst. + apply R_Ax; simpl; auto. Qed. `````` Pierre Letouzey committed Feb 26, 2019 146 `````` `````` Pierre Letouzey committed Apr 02, 2019 147 ``````Definition Inconsistent th := IsTheorem th False. `````` Pierre Letouzey committed Feb 26, 2019 148 `````` `````` Pierre Letouzey committed Apr 02, 2019 149 ``````Definition Consistent th := ~IsTheorem th False. `````` Pierre Letouzey committed Feb 26, 2019 150 151 152 153 154 155 156 `````` Definition opt_finer {A} (o o' : option A) := o=None \/ o=o'. Definition optfun_finer {A B} (f f' : A -> option B) := forall a, opt_finer (f a) (f' a). `````` Pierre Letouzey committed Apr 02, 2019 157 ``````Definition SignExtend sign sign' := `````` Pierre Letouzey committed Apr 09, 2019 158 159 `````` optfun_finer (sign.(funsymbs)) (sign'.(funsymbs)) /\ optfun_finer (sign.(predsymbs)) (sign'.(predsymbs)). `````` Pierre Letouzey committed Feb 26, 2019 160 `````` `````` Pierre Letouzey committed Apr 09, 2019 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 ``````Lemma signext_refl sign : SignExtend sign sign. Proof. red; unfold optfun_finer, opt_finer. intuition. Qed. Lemma signext_trans sign1 sign2 sign3 : SignExtend sign1 sign2 -> SignExtend sign2 sign3 -> SignExtend sign1 sign3. Proof. intros (F12,P12) (F23,P23). split; unfold optfun_finer, opt_finer in *; intros a. - destruct (F12 a) as [? | ->]; auto. - destruct (P12 a) as [? | ->]; auto. Qed. `````` Pierre Letouzey committed Apr 02, 2019 176 177 178 179 180 181 ``````Lemma signext_check_term sign sign' (t:term) : SignExtend sign sign' -> check sign t = true -> check sign' t = true. Proof. intros (SE,_). induction t using term_ind'; cbn; auto. destruct (SE f) as [->|<-]; try easy. `````` Pierre Letouzey committed Apr 09, 2019 182 `````` destruct funsymbs; auto. `````` Pierre Letouzey committed Apr 02, 2019 183 184 185 186 187 188 189 190 191 192 `````` destruct (length args =? a); auto. rewrite !forallb_forall; auto. Qed. Lemma signext_check sign sign' (f:formula) : SignExtend sign sign' -> check sign f = true -> check sign' f = true. Proof. intros SE. induction f; cbn; auto. destruct (proj2 SE p) as [->|<-]; try easy. `````` Pierre Letouzey committed Apr 09, 2019 193 `````` destruct predsymbs; auto. `````` Pierre Letouzey committed Apr 02, 2019 194 195 196 197 198 `````` destruct (length l =? a); auto. rewrite !forallb_forall; eauto using signext_check_term. rewrite !lazy_andb_iff; intuition. Qed. `````` Pierre Letouzey committed Apr 09, 2019 199 200 201 202 203 204 ``````Lemma signext_wf sign sign' (f:formula) : SignExtend sign sign' -> Wf sign f -> Wf sign' f. Proof. intros SE (CK & H). split; eauto using signext_check. Qed. `````` Pierre Letouzey committed Apr 02, 2019 205 206 207 208 ``````Definition Extend th1 th2 := SignExtend th1 th2 /\ forall T, IsTheorem th1 T -> IsTheorem th2 T. `````` Pierre Letouzey committed Apr 09, 2019 209 210 211 212 213 214 215 216 217 218 219 220 ``````Lemma extend_refl th : Extend th th. Proof. split; auto using signext_refl. Qed. Lemma extend_trans th1 th2 th3 : Extend th1 th2 -> Extend th2 th3 -> Extend th1 th3. Proof. intros (SE12,TH12) (SE23,TH23). split; eauto using signext_trans. Qed. `````` Pierre Letouzey committed Apr 02, 2019 221 222 223 224 225 226 227 228 229 230 231 232 ``````Lemma Pr_relay c c' f : Pr logic (c ⊢ f) -> (forall A, In A c -> Pr logic (c' ⊢ A)) -> Pr logic (c' ⊢ f). Proof. revert c' f. induction c. - intros c' f PR _. eapply Pr_weakening; eauto. constructor. now red. - intros c' f PR H. simpl in H. apply R_Imp_e with a; auto. Qed. `````` Pierre Letouzey committed Feb 26, 2019 233 `````` `````` Pierre Letouzey committed Apr 02, 2019 234 235 236 237 238 239 240 241 242 ``````Lemma extend_alt th1 th2 : Extend th1 th2 <-> SignExtend th1 th2 /\ forall A, IsAxiom th1 A -> IsTheorem th2 A. Proof. split. - intros (SE,TT); split; auto. intros A HA. apply ax_thm in HA. auto. - intros (SE,AT); split; auto. `````` Pierre Letouzey committed Apr 09, 2019 243 244 245 `````` intros T (CL & axs & Haxs & PR). split. + eapply signext_wf; eauto. `````` Pierre Letouzey committed Apr 02, 2019 246 247 `````` + assert (exists axs2, Forall (IsAxiom th2) axs2 /\ forall A, In A axs -> Pr logic (axs2 ⊢ A)). `````` Pierre Letouzey committed Apr 09, 2019 248 `````` { clear SE CL PR. `````` Pierre Letouzey committed Apr 02, 2019 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 `````` induction axs. - exists []; split; auto. - inversion_clear Haxs. destruct IHaxs as (axs2 & U & V); auto. destruct (AT a) as (_ & axa & Haxa & PR); auto. exists (axa ++ axs2); split. + rewrite Forall_forall in *. intros x. rewrite in_app_iff. intuition. + simpl. intros A [->|HA]. * eapply Pr_weakening; eauto. constructor. intros x Hx. rewrite in_app_iff. intuition. * eapply Pr_weakening with (axs2 ⊢ A); eauto. constructor. intros x Hx. rewrite in_app_iff. intuition. } destruct H as (axs2 & Haxs2 & PR'). exists axs2; split; auto. apply Pr_relay with axs; auto. Qed. Definition IsEqualityTheory th := `````` Pierre Letouzey committed Apr 09, 2019 267 `````` th.(predsymbs) "=" = Some 2 /\ `````` Pierre Letouzey committed Apr 02, 2019 268 `````` IsTheorem th (∀Pred "=" [#0; #0])%form /\ `````` Pierre Letouzey committed Feb 26, 2019 269 `````` forall A z, `````` Pierre Letouzey committed Apr 09, 2019 270 `````` check th A = true -> `````` Pierre Letouzey committed Apr 04, 2019 271 `````` BClosed A -> `````` Pierre Letouzey committed Apr 02, 2019 272 273 274 275 `````` Vars.Equal (fvars A) (Vars.singleton z) -> IsTheorem th (∀∀(Pred "=" [#1;#0] -> fsubst z (#1) A -> fsubst z (#0) A))%form. (** TODO: more about equality theories *) `````` Pierre Letouzey committed Feb 26, 2019 276 `````` `````` Pierre Letouzey committed Apr 02, 2019 277 278 ``````Definition ConservativeExt th1 th2 := Extend th1 th2 /\ `````` Pierre Letouzey committed Apr 09, 2019 279 280 281 282 283 284 285 286 287 288 289 290 291 `````` forall T, IsTheorem th2 T /\ Wf th1 T <-> IsTheorem th1 T. Lemma consext_alt th1 th2 : ConservativeExt th1 th2 <-> (Extend th1 th2 /\ forall T, IsTheorem th2 T -> check th1 T = true -> IsTheorem th1 T). Proof. split; intros (U,V); split; auto. - intros T HT CK. apply V. do 2 (split; auto). apply HT. - intros T. split. + intros (W,X). apply V; auto. apply X. + split. now apply U. apply H. Qed. `````` Pierre Letouzey committed Feb 26, 2019 292 293 `````` Lemma consext_inconsistency th1 th2 : `````` Pierre Letouzey committed Apr 09, 2019 294 `````` ConservativeExt th1 th2 -> Inconsistent th2 <-> Inconsistent th1. `````` Pierre Letouzey committed Feb 26, 2019 295 ``````Proof. `````` Pierre Letouzey committed Apr 09, 2019 296 `````` unfold Inconsistent. intros (_,<-). intuition. `````` Pierre Letouzey committed Feb 26, 2019 297 298 299 ``````Qed. Lemma consext_consistency th1 th2 : `````` Pierre Letouzey committed Apr 09, 2019 300 301 302 303 304 305 306 307 308 309 310 311 312 313 `````` ConservativeExt th1 th2 -> Consistent th1 <-> Consistent th2. Proof. unfold Consistent. intros (_,<-). intuition. Qed. Lemma consext_refl th : ConservativeExt th th. Proof. rewrite consext_alt. split; auto using extend_refl. Qed. Lemma consext_trans th1 th2 th3 : ConservativeExt th1 th2 -> ConservativeExt th2 th3 -> ConservativeExt th1 th3. `````` Pierre Letouzey committed Feb 26, 2019 314 ``````Proof. `````` Pierre Letouzey committed Apr 09, 2019 315 316 317 318 319 320 321 `````` rewrite !consext_alt. intros (E12,T12) (E23,T23). split; eauto using extend_trans. intros T HT C. apply T12; auto. apply T23; auto. eapply signext_check; eauto. apply E12. `````` Pierre Letouzey committed Feb 26, 2019 322 323 ``````Qed. `````` Pierre Letouzey committed Apr 03, 2019 324 ``````(** If we only extend the signature, not the axioms, then `````` Pierre Letouzey committed Apr 04, 2019 325 326 327 `````` it's a conservative extension. To prove this, normally we restrict a proof to the small signature, but here with [Pr] it's implicit (see thm_alt) *) `````` Pierre Letouzey committed Apr 03, 2019 328 `````` `````` Pierre Letouzey committed Feb 26, 2019 329 ``````Lemma ext_sign_only th1 th2 : `````` Pierre Letouzey committed Apr 02, 2019 330 331 332 `````` SignExtend th1 th2 -> (forall A, IsAxiom th1 A <-> IsAxiom th2 A) -> ConservativeExt th1 th2. `````` Pierre Letouzey committed Feb 26, 2019 333 ``````Proof. `````` Pierre Letouzey committed Apr 09, 2019 334 `````` intros SE EQ. rewrite consext_alt. split. `````` Pierre Letouzey committed Apr 03, 2019 335 336 337 338 `````` - apply extend_alt. split; auto. intros A. rewrite EQ. apply ax_thm. - intros T (CL & axs & F & PR) CK. split. + split; auto. apply CL. `````` Pierre Letouzey committed Apr 04, 2019 339 340 `````` + exists axs. split; auto. rewrite Forall_forall in *. intros x Hx. rewrite EQ; auto. `````` Pierre Letouzey committed Apr 03, 2019 341 342 ``````Qed. `````` Pierre Letouzey committed Apr 09, 2019 343 344 345 ``````(** Tweaking the function symbols of a signature *) Definition modify_funsymbs sign modif := `````` Pierre Letouzey committed Apr 09, 2019 346 347 `````` {| funsymbs := modif (sign.(funsymbs)); predsymbs := sign.(predsymbs) |}. `````` Pierre Letouzey committed Apr 09, 2019 348 349 350 351 `````` (** Henkin extension : from an existential theorem [∃A], adding a new constant [c] as witness and the new axiom [A(c)]. *) `````` Pierre Letouzey committed Feb 26, 2019 352 353 `````` Definition Henkin_sign sign c := `````` Pierre Letouzey committed Apr 09, 2019 354 355 `````` modify_funsymbs sign (fun funs f => if f =? c then Some 0 else funs f). `````` Pierre Letouzey committed Feb 26, 2019 356 357 `````` Definition Henkin_axiom Ax (A:formula) c := `````` Pierre Letouzey committed Apr 09, 2019 358 `````` fun f => Ax f \/ f = bsubst 0 (Cst c) A. `````` Pierre Letouzey committed Apr 03, 2019 359 `````` `````` Pierre Letouzey committed Apr 09, 2019 360 ``````Lemma Henkin_signext sign c : `````` Pierre Letouzey committed Apr 09, 2019 361 `````` sign.(funsymbs) c = None -> `````` Pierre Letouzey committed Apr 03, 2019 362 363 364 365 366 367 `````` SignExtend sign (Henkin_sign sign c). Proof. intros Hc. split; unfold optfun_finer, opt_finer; cbn; auto. intros a. case eqbspec; intros; subst; auto. Qed. `````` Pierre Letouzey committed Feb 26, 2019 368 `````` `````` Pierre Letouzey committed Apr 02, 2019 369 ``````Lemma Henkin_ax_wf th A c : `````` Pierre Letouzey committed Apr 09, 2019 370 `````` th.(funsymbs) c = None -> `````` Pierre Letouzey committed Apr 02, 2019 371 372 `````` IsTheorem th (∃A) -> forall B, Henkin_axiom th.(IsAxiom) A c B -> `````` Pierre Letouzey committed Apr 09, 2019 373 374 375 376 377 378 379 `````` Wf (Henkin_sign th c) B. Proof. intros Hc (CL & _) B [HB| -> ]. - eauto using signext_wf, Henkin_signext, WfAxiom. - apply bsubst_cst_wf. + simpl. now rewrite eqb_refl. + eauto using signext_wf, Henkin_signext. `````` Pierre Letouzey committed Apr 03, 2019 380 ``````Qed. `````` Pierre Letouzey committed Feb 26, 2019 381 382 `````` Definition Henkin_ext th A c `````` Pierre Letouzey committed Apr 09, 2019 383 `````` (E:th.(funsymbs) c = None) `````` Pierre Letouzey committed Apr 02, 2019 384 `````` (Thm:IsTheorem th (∃A)) := `````` Pierre Letouzey committed Apr 09, 2019 385 `````` {| sign := Henkin_sign th c; `````` Pierre Letouzey committed Apr 02, 2019 386 387 388 `````` IsAxiom := Henkin_axiom th.(IsAxiom) A c; WfAxiom := Henkin_ax_wf th A c E Thm |}. `````` Pierre Letouzey committed Feb 26, 2019 389 390 `````` Lemma Henkin_consext th A c `````` Pierre Letouzey committed Apr 09, 2019 391 `````` (E:th.(funsymbs) c = None) `````` Pierre Letouzey committed Apr 02, 2019 392 393 `````` (Thm:IsTheorem th (∃A)) : ConservativeExt th (Henkin_ext th A c E Thm). `````` Pierre Letouzey committed Feb 26, 2019 394 ``````Proof. `````` Pierre Letouzey committed Apr 09, 2019 395 `````` rewrite consext_alt. `````` Pierre Letouzey committed Apr 03, 2019 396 397 `````` split. - apply extend_alt. split. `````` Pierre Letouzey committed Apr 09, 2019 398 `````` + now apply Henkin_signext. `````` Pierre Letouzey committed Apr 03, 2019 399 `````` + intros A0 HA0. `````` Pierre Letouzey committed Apr 09, 2019 400 `````` apply ax_thm; simpl; left; auto. `````` Pierre Letouzey committed Apr 03, 2019 401 402 403 404 405 406 407 `````` - intros T (CL & axs & F & PR) CK; simpl in *. split. + split; auto. apply CL. + set (newAx := bsubst 0 (Cst c) A). set (axs' := filter (fun f => negb (f =? newAx)) axs). simpl in *. destruct Thm as (CLA & axsA & FA & PRA). `````` Pierre Letouzey committed Apr 09, 2019 408 409 410 411 412 413 `````` assert (F' : Forall (IsAxiom th) axs'). { rewrite Forall_forall in *. intros x. unfold axs'. rewrite filter_In. rewrite negb_true_iff, eqb_neq. intros (IN,NE); auto. apply F in IN. unfold Henkin_axiom in IN; intuition. } `````` Pierre Letouzey committed Apr 03, 2019 414 415 `````` exists (axs' ++ axsA); split. * rewrite Forall_forall in *. `````` Pierre Letouzey committed Apr 09, 2019 416 417 `````` intros x. rewrite in_app_iff; intuition. * assert (PR' : Pr logic (newAx::axs' ⊢ T)). `````` Pierre Letouzey committed Apr 03, 2019 418 419 420 421 422 `````` { eapply Pr_weakening; eauto. constructor. unfold axs'. intros v. simpl. rewrite filter_In. rewrite negb_true_iff, eqb_neq. destruct (eqbspec v newAx); intuition. } `````` Pierre Letouzey committed Apr 09, 2019 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 `````` apply Provable_alt in PR'. destruct PR' as (d & V & C). assert (Vars.Empty (fvars (axs' ++ axsA))). { intros v. unfold fvars, fvars_list. rewrite vars_unionmap_in. intros (a & Hv & Ha). rewrite in_app_iff in Ha. revert v Hv. apply (WfAxiom th). rewrite Forall_forall in F', FA; intuition. } apply VarsP.empty_is_empty_1 in H. set (vars := Vars.union (fvars A) (fvars d)). assert (Hx := fresh_var_ok vars). set (x := fresh_var vars) in *. apply (restrict_valid logic th x) in V; auto with set. assert (C' := claim_restrict th x d). rewrite C in C'. cbn in C'. rewrite (check_restrict_id th x T) in C'; auto. assert (map (restrict th x) axs' = axs'). { apply map_id_iff. intros a Ha. apply check_restrict_id. apply WfAxiom. rewrite Forall_forall in F'; auto. } rewrite H0 in C'; clear H0. assert (restrict th x newAx = bsubst 0 (FVar x) A). { unfold newAx. rewrite restrict_bsubst. f_equal. - cbn. now rewrite E. - apply check_restrict_id. apply CLA. } rewrite H0 in C'; clear H0. apply Valid_Pr in V. rewrite C' in V. apply (R_Ex_e logic x _ A). { cbn. rewrite H. destruct d. unfold vars in Hx. cbn in C. subst s. cbn in Hx. varsdec. } { clear PR V. eapply Pr_weakening; eauto. constructor. intros v. rewrite in_app_iff; auto. } { clear PR PRA. eapply Pr_weakening; eauto. constructor. intros v. simpl. rewrite in_app_iff; intuition. } Qed. (** A variant of Henkin where the constant is already in the signature (but not used in the axioms nor in the existential theorem we consider). Not a conservative extension stricto sensu, but at least this preserves consistency. *) Definition delcst sign c := modify_funsymbs sign (fun funs f => if f =? c then None else funs f). Lemma delcst_signext sign c : SignExtend (delcst sign c) sign. Proof. split; unfold optfun_finer, opt_finer; cbn; auto. intros a. case eqbspec; intros; subst; auto. Qed. Definition AxiomsWithout th c := forall A, IsAxiom th A -> Wf (delcst th c) A. Definition delcst_th th c (AW : AxiomsWithout th c) := {| sign := delcst th c; IsAxiom := IsAxiom th; WfAxiom := AW |}. Lemma delcst_consext th c (AW : AxiomsWithout th c) : ConservativeExt (delcst_th th c AW) th. Proof. apply ext_sign_only. now apply delcst_signext. intuition. Qed. Lemma Henkin_ax_wf' th A c : `````` Pierre Letouzey committed Apr 09, 2019 499 `````` th.(funsymbs) c = Some 0 -> `````` Pierre Letouzey committed Apr 09, 2019 500 501 502 503 504 505 506 507 508 `````` IsTheorem th (∃A) -> forall B, Henkin_axiom th.(IsAxiom) A c B -> Wf th B. Proof. intros E Thm B [HB| -> ]. - now apply WfAxiom. - apply bsubst_cst_wf; auto. apply Thm. Qed. Definition Henkin_halfext th A c `````` Pierre Letouzey committed Apr 09, 2019 509 `````` (E : th.(funsymbs) c = Some 0) `````` Pierre Letouzey committed Apr 09, 2019 510 511 512 513 514 515 516 517 518 519 520 521 522 523 `````` (Thm : IsTheorem th (∃A)) := {| sign := th; IsAxiom := Henkin_axiom th.(IsAxiom) A c; WfAxiom := Henkin_ax_wf' th A c E Thm |}. (** The extension from [th - c] to [Henkin_halfext] is conservative, but not the one from [th] to [Henkin_halfext]. For instance, [A(c)] is a theorem of the extension, and is in the language of [th], but it has no reason to be a theorem of [th]. *) Lemma Henkin_halfext_consext th A c `````` Pierre Letouzey committed Apr 09, 2019 524 `````` (E : th.(funsymbs) c = Some 0) `````` Pierre Letouzey committed Apr 09, 2019 525 526 527 528 529 530 531 532 533 534 535 536 537 538 `````` (Thm : IsTheorem th (∃A)) (AW : AxiomsWithout th c) (CK : check (delcst th c) A = true) : ConservativeExt (delcst_th th c AW) (Henkin_halfext th A c E Thm). Proof. rewrite consext_alt. split. - apply extend_trans with th. + apply delcst_consext. + rewrite extend_alt. split; cbn; auto using signext_refl. intros B HB. apply ax_thm. cbn. now left. - intros T. `````` Pierre Letouzey committed Apr 09, 2019 539 `````` assert (E' : funsymbs (delcst_th th c AW) c = None). `````` Pierre Letouzey committed Apr 09, 2019 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 `````` { cbn. now rewrite eqb_refl. } assert (Thm' : IsTheorem (delcst_th th c AW) (∃A)). { apply delcst_consext; split; auto. cbn. split. now cbn. apply Thm. } assert (HC := Henkin_consext _ _ _ E' Thm'). rewrite consext_alt in HC. intros HT CKT. apply HC; auto. split. + eapply signext_wf. * apply Henkin_signext. cbn. now rewrite eqb_refl. * split. apply CKT. apply HT. + cbn. apply HT. Qed. (** At least we preserve consistency *) Lemma Henkin_halfext_consistent th A c `````` Pierre Letouzey committed Apr 09, 2019 558 `````` (E : th.(funsymbs) c = Some 0) `````` Pierre Letouzey committed Apr 09, 2019 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 `````` (Thm : IsTheorem th (∃A)) (AW : AxiomsWithout th c) (CK : check (delcst th c) A = true) : Consistent th <-> Consistent (Henkin_halfext th A c E Thm). Proof. rewrite <- (consext_consistency (delcst_th th c AW) th) by apply delcst_consext. apply consext_consistency. now apply Henkin_halfext_consext. Qed. (** Henkin extensions over *all* existential formulas. *) (** The ultimate goal : building a theory that is saturated of Henkin witnesses. *) Definition WitnessSaturated th := forall A, IsTheorem th (∃ A) -> exists c, `````` Pierre Letouzey committed Apr 09, 2019 579 `````` th.(funsymbs) c = Some 0 /\ `````` Pierre Letouzey committed Apr 09, 2019 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 `````` IsTheorem th (bsubst 0 (Cst c) A). (** Actually, we won't bother considering only existential *theorems* (since anyway we'll have additionnal theorems later). Instead, for all [∃A] formula, we obtain "conditional" statements [∃A -> A(c)] for some constant [c]. This is done by an Henkin extension based on the (classical) tautology [∃y((∃xA(x))->A(y))]. *) (** So the intermediate goal is to build a theory which is "super-saturated" of Henkin witnesses : *) Definition WitnessSuperSaturated th := forall A, Wf th (∃ A) -> exists c, `````` Pierre Letouzey committed Apr 09, 2019 596 `````` th.(funsymbs) c = Some 0 /\ `````` Pierre Letouzey committed Apr 09, 2019 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 `````` IsTheorem th ((∃ A) -> bsubst 0 (Cst c) A). (** Super-saturated implies saturated *) Lemma supersaturated_saturated th : WitnessSuperSaturated th -> WitnessSaturated th. Proof. intros WSS A Thm. destruct (WSS A (proj1 Thm)) as (c & Hc & Thm'). exists c; split; auto. split. - destruct Thm' as (WF', _). now apply Op_wf in WF'. - destruct Thm as (_ & axs & F & V). destruct Thm' as (_ & axs' & F' & V'). exists (axs ++ axs'); split. + rewrite Forall_forall in *. intros f. rewrite in_app_iff; intuition. + apply R_Imp_e with (∃ A)%form. * eapply Pr_weakening; eauto. constructor. intros a. rewrite in_app_iff; now right. * clear V'. eapply Pr_weakening; eauto. constructor. intros a. rewrite in_app_iff; now left. Qed. (** We'll need an infinite pool of fresh constant names (axiomatized as an injective function from nat to string). Moreover, we should be able to recognize these names (for building the new signature). *) `````` Pierre Letouzey committed Apr 09, 2019 627 ``````Record NewCsts (sign : signature) := `````` Pierre Letouzey committed Apr 09, 2019 628 629 `````` { csts :> nat -> string; csts_inj : forall n m, csts n = csts m -> n = m; `````` Pierre Letouzey committed Apr 09, 2019 630 `````` csts_ok : forall n, sign.(funsymbs) (csts n) = None; `````` Pierre Letouzey committed Apr 09, 2019 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 `````` test : string -> bool; test_ok : forall s, test s = true <-> exists n, csts n = s }. (** An important technical note : we cannot just iterate on formulas of the initial theory, otherwise, we'll end up with some final existential formulas not handled (the one using the constants we've added in the process). So we add all these "fresh" constants at first, and then do Henkin "half-extensions" (see above). *) Definition HenkinAll_sign sign (nc : NewCsts sign) := modify_funsymbs sign (fun funs f => if test _ nc f then Some 0 else funs f). Lemma HenkinAll_signext sign (nc : NewCsts sign) : SignExtend sign (HenkinAll_sign sign nc). Proof. split; unfold optfun_finer, opt_finer; cbn; auto. intros a. destruct test eqn:E; intros; subst; auto. left. apply test_ok in E. destruct E as (n & <-). apply csts_ok. Qed. Lemma exex_tauto A : level A <= 1 -> Pr Classic ([] ⊢ ∃ ((∃ A) -> A)). Proof. intros HA. apply R_Or_e with (∃ A)%form (~(∃ A))%form. apply Excluded_Middle. - assert (Hx := fresh_var_ok (fvars A)). set (x := fresh_var (fvars A)) in *. apply R'_Ex_e with x. cbn. varsdec. apply R_Ex_i with (FVar x); auto. cbn. apply R_Imp_i. apply R_Ax. simpl; auto. - assert (Hx := fresh_var_ok (fvars A)). set (x := fresh_var (fvars A)) in *. apply R_Ex_i with (FVar x); auto. cbn. rewrite form_level_bsubst_id; auto. apply R_Imp_i. apply R_Fa_e. apply R_Not_e with (∃ A)%form; apply R_Ax; simpl; auto. Qed. Lemma exex_thm th A : logic = Classic -> Wf th (∃A) -> IsTheorem th (∃ ((∃ A) -> A)). Proof. intros LG CL. split. - destruct CL as (CK & BC & FC). repeat split. + cbn in *. now rewrite CK. + red. cbn. rewrite BC. cbn. apply BC. + red; red in FC. cbn in *. varsdec. - exists []; split; auto. subst logic. apply exex_tauto. assert (Nat.pred (level A) = 0) by apply CL. omega. Qed. (* TODO use a different module name than Vars for constant names. A generic Names ? *) Fixpoint term_funs t := match t with | FVar _ | BVar _ => Vars.empty | Fun f l => Vars.add f (vars_unionmap term_funs l) end. Fixpoint form_funs f := match f with | True | False => Vars.empty | Pred p l => vars_unionmap term_funs l | Not f => form_funs f | Op _ f1 f2 => Vars.union (form_funs f1) (form_funs f2) | Quant _ f => form_funs f end. Lemma term_funs_ok sign t c : ~Vars.In c (term_funs t) -> check (delcst sign c) t = check sign t. Proof. revert t. fix IH 1. destruct t as [ | | f l]; cbn; auto. intros NI. case eqbspec; [varsdec|]. `````` Pierre Letouzey committed Apr 09, 2019 718 `````` intros _. destruct funsymbs; auto. `````` Pierre Letouzey committed Apr 09, 2019 719 720 721 722 723 724 725 726 727 728 729 730 `````` case eqb; auto. revert l NI. fix IH' 1. destruct l as [ |t l]; cbn; auto. intros NI'. rewrite IH by varsdec. f_equal. apply IH'. varsdec. Qed. Lemma form_funs_ok sign f c : ~Vars.In c (form_funs f) -> check (delcst sign c) f = check sign f. Proof. induction f; cbn; auto. `````` Pierre Letouzey committed Apr 09, 2019 731 `````` - intros NI. destruct predsymbs; auto. `````` Pierre Letouzey committed Apr 09, 2019 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 `````` case eqb; auto. revert l NI. induction l as [|t l]; cbn; auto. intros NI'. rewrite term_funs_ok by varsdec. f_equal. apply IHl. varsdec. - intros NI. now rewrite IHf1, IHf2 by varsdec. Qed. Lemma form_funs_wf sign f c : ~Vars.In c (form_funs f) -> Wf (delcst sign c) f <-> Wf sign f. Proof. intros NI. split; intros (CK,H); split; try apply H. rewrite <- CK. symmetry. now apply form_funs_ok. rewrite <- CK. now apply form_funs_ok. Qed. Fixpoint fresh_cst_loop n used candidates := match n with | 0 => candidates 0 | S n => let c := candidates 0 in if Vars.mem c used then let candidates' := fun n => candidates (S n) in fresh_cst_loop n (Vars.remove c used) candidates' else c end. Definition fresh_cst used candidates := fresh_cst_loop (Vars.cardinal used) used candidates. Lemma fresh_cst_loop_in_cands n used candidates : Vars.cardinal used = n -> exists m, fresh_cst_loop n used candidates = candidates m. Proof. revert used candidates. induction n; simpl; intros used cs E; auto. - now exists 0. - destruct Vars.mem eqn:M. + rewrite Vars.mem_spec in M. destruct (IHn (Vars.remove (cs 0) used) (fun n : nat => cs (S n))) as (m,Hm). rewrite <- (@VarsP.remove_cardinal_1 used (cs 0)) in E; auto. now exists (S m). + now exists 0. Qed. Lemma fresh_cst_in_cands used candidates : exists m, fresh_cst used candidates = candidates m. Proof. now apply fresh_cst_loop_in_cands. Qed. Lemma fresh_cst_loop_ok n used candidates : Vars.cardinal used = n -> (forall n m, candidates n = candidates m -> n = m) -> ~Vars.In (fresh_cst_loop n used candidates) used. Proof. revert used candidates. induction n as [|n IH]; intros used cs E INJ. - apply VarsP.cardinal_inv_1 in E. varsdec. - simpl. destruct Vars.mem eqn:M. + set (used' := Vars.remove (cs 0) used). set (cs' := fun n : nat => cs (S n)). specialize (IH used' cs'). unfold used' in IH at 3. rewrite Vars.remove_spec in IH. assert (Vars.cardinal used' = n). { unfold used'. rewrite Vars.mem_spec in M. rewrite <- (@VarsP.remove_cardinal_1 used (cs 0)) in E; auto. } intros IN. apply IH; auto. * unfold cs'. intros m p E'. apply INJ in E'; auto. * split; auto. destruct (fresh_cst_loop_in_cands n used' cs') as (m,->); auto. unfold cs'. intros E'. now apply INJ in E'. + rewrite <-Vars.mem_spec. now rewrite M. Qed. Lemma fresh_cst_ok used candidates : (forall n m, candidates n = candidates m -> n = m) -> ~Vars.In (fresh_cst used candidates) used. Proof. now apply fresh_cst_loop_ok. Qed. Fixpoint HenkinAxList th (nc : NewCsts th) n := match n with | 0 => [] | S n => let axs := HenkinAxList th nc n in let A := decode_form n in match Wf_dec (HenkinAll_sign th nc) (∃A) with | left CL => let used := Vars.union (form_funs A) (vars_unionmap form_funs axs) in let c := fresh_cst used nc in ((∃A)-> bsubst 0 (Cst c) A)%form :: axs | right _ => axs end end. Lemma equivtheories_thm th th' : sign th = sign th' -> (forall A, IsAxiom th A <-> IsAxiom th' A) -> forall T, IsTheorem th T -> IsTheorem th' T. Proof. intros E AX T (WF & axs & F & V). split. - now rewrite <- E. - exists axs; split; auto. rewrite Forall_forall in *. intros B HB. rewrite <- AX; auto. Qed. Lemma equivtheories_consistency th th' : sign th = sign th' -> (forall A, IsAxiom th A <-> IsAxiom th' A) -> Consistent th <-> Consistent th'. Proof. intros E AX. split; intros H Thm. - apply (equivtheories_thm th' th) in Thm; auto. intros A. now symmetry. - apply (equivtheories_thm th th') in Thm; auto. Qed. Lemma delcst_HenkinAll_signext th (nc : NewCsts th) n : SignExtend th (delcst (HenkinAll_sign th nc) (nc n)). Proof. split; cbn; unfold optfun_finer, opt_finer; auto. intros a. case eqbspec. - intros ->. left. apply csts_ok. - intros _. destruct (test th nc a) eqn:E; auto. left. apply test_ok in E. destruct E as (m, <-). apply csts_ok. Qed. Lemma HenkinAxList_wf th (nc : NewCsts th) n : forall A, IsAxiom th A \/ In A (HenkinAxList th nc n) -> Wf (HenkinAll_sign th nc) A. Proof. induction n as [|n IH]. - simpl. intros A [HA|Fa]; [|easy]. eauto using signext_wf, HenkinAll_signext, WfAxiom. - intros A [HA|IN]; auto. simpl in IN. set (f := decode_form n) in *. destruct Wf_dec as [CL|_]; auto. set (used := Vars.union _ _) in *. destruct (fresh_cst_in_cands used nc) as (m,Hm). assert (NI := fresh_cst_ok used nc (csts_inj _ nc)). set (c := fresh_cst used nc) in *. destruct IN as [<-|IN]; auto. apply Op_wf; auto. split; auto. apply bsubst_cst_wf; auto. simpl. replace (test _ nc c) with true; auto. symmetry. rewrite Hm, test_ok. now exists m. Qed. Definition HenkinSeq th (nc : NewCsts th) n := {| sign := HenkinAll_sign th nc; IsAxiom := fun A => IsAxiom th A \/ In A (HenkinAxList th nc n); WfAxiom := HenkinAxList_wf th nc n |}. Lemma HenkinSeq_extend th nc n : Extend th (HenkinSeq th nc n). Proof. apply extend_alt. split. apply HenkinAll_signext. intros. apply ax_thm. simpl. now left. Qed. Lemma HenkinSeq_consistent th nc n : logic = Classic -> Consistent th <-> Consistent (HenkinSeq th nc n). Proof. intros LG. induction n; simpl. - apply consext_consistency. apply ext_sign_only; cbn. + apply HenkinAll_signext. + intuition. - rewrite IHn. unfold Consistent, IsTheorem. simpl. set (f := decode_form n) in *. destruct Wf_dec as [WF|WF] eqn:Ew; [|reflexivity]. set (used := Vars.union _ _) in *. destruct (fresh_cst_in_cands used nc) as (m,Hm). assert (NI := fresh_cst_ok used nc (csts_inj _ nc)). set (c := fresh_cst used nc) in *. `````` Pierre Letouzey committed Apr 09, 2019 928 `````` assert (E : (HenkinSeq th nc n).(funsymbs) c = Some 0). `````` Pierre Letouzey committed Apr 09, 2019 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 `````` { simpl. replace (test th nc c) with true; auto. symmetry. rewrite Hm, test_ok. now exists m. } assert (Thm : IsTheorem (HenkinSeq th nc n) (∃ ((∃ f) -> f))%form). { apply exex_thm; auto. } rewrite (Henkin_halfext_consistent _ ((∃ f) -> f)%form c E Thm). rewrite (equivtheories_consistency (Henkin_halfext (HenkinSeq th nc n) ((∃ f) -> f) c E Thm) (HenkinSeq th nc (S n))). + unfold Consistent, IsTheorem. simpl. fold f. rewrite Ew. reflexivity. + simpl; auto. + intros A. cbn - [decode_form]. fold f. rewrite Ew. fold used. fold c. clearbody f. clearbody c. unfold Henkin_axiom. simpl. split. * intros [[H|H]|H]; auto. right; left. rewrite H. cbn. f_equal. f_equal. symmetry. apply form_level_bsubst_id. assert (pred (level f) = 0) by apply WF. omega. * intros [H|[H|H]]; auto. right. rewrite <- H. cbn. f_equal. f_equal. symmetry. apply form_level_bsubst_id. assert (pred (level f) = 0) by apply WF. omega. + intros A [HA|HA]. * cbn. apply signext_wf with th; auto using WfAxiom. rewrite Hm. apply delcst_HenkinAll_signext. * rewrite form_funs_wf. apply WfAxiom. simpl. now right. intros IN. assert (Vars.In c (vars_unionmap form_funs (HenkinAxList th nc n))). { rewrite vars_unionmap_in. now exists A. } varsdec. + clearbody f. clear Ew. rewrite form_funs_ok. cbn. destruct WF as (CK,?). cbn in CK. now rewrite CK. cbn. varsdec. Qed. Lemma HenkinSeq_ax_grows th (nc : NewCsts th) n m A : n <= m -> IsAxiom (HenkinSeq th nc n) A -> IsAxiom (HenkinSeq th nc m) A. Proof. induction 1; auto. intros Hn. specialize (IHle Hn). clear Hn. simpl. destruct Wf_dec; [|auto]. simpl. cbn in IHle. intuition. Qed. Definition HenkinAll_axioms th (nc : NewCsts th) := fun f => exists n, IsAxiom (HenkinSeq th nc n) f. Lemma HenkinAll_ax_wf th (nc : NewCsts th) : forall B, HenkinAll_axioms th nc B -> Wf (HenkinAll_sign th nc) B. Proof. intros B (n & Hn). now apply WfAxiom in Hn. Qed. Definition HenkinAll_ext th (nc : NewCsts th) := {| sign := HenkinAll_sign th nc; IsAxiom := HenkinAll_axioms th nc; WfAxiom := HenkinAll_ax_wf th nc |}. Lemma HenkinAll_extend th (nc : NewCsts th) : Extend th (HenkinAll_ext th nc). Proof. apply extend_alt. split. - apply HenkinAll_signext. - intros A HA. apply ax_thm. exists 0. now left. Qed. Lemma HenkinAll_Forall_max th (nc : NewCsts th) axs : Forall (HenkinAll_axioms th nc) axs -> exists n, Forall (IsAxiom (HenkinSeq th nc n)) axs. Proof. induction axs. - intros _. now exists 0. - inversion_clear 1. destruct IHaxs as (n & F); auto. destruct H0 as (n' & H'). exists (Nat.max n' n). constructor. apply HenkinSeq_ax_grows with n'; auto with *. rewrite Forall_forall in *. intros f Hf. apply HenkinSeq_ax_grows with n; auto with *. Qed. (** TODO: conservative extention over th. Not that useful... *) Lemma HenkinAll_consistent th (nc : NewCsts th) : logic = Classic -> Consistent th -> Consistent (HenkinAll_ext th nc). Proof. intros LG C (_ & axs & F & V). apply HenkinAll_Forall_max in F. destruct F as (n & F). rewrite (HenkinSeq_consistent th nc n) in C; auto. apply C. split. - apply False_wf. - exists axs; auto. Qed. Lemma HenkinAll_ext_supersaturated th (nc : NewCsts th) : logic = Classic -> WitnessSuperSaturated (HenkinAll_ext th nc). Proof. red. intros LG A CL. set (n := code_form A). assert (Ax : forall A, In A (HenkinAxList th nc (S n)) -> IsAxiom (HenkinAll_ext th nc) A). { intros B HB. exists (S n). now right. } cbn - [decode_form code_form] in Ax. assert (HA : decode_form n = A) by apply decode_code_form. rewrite HA in Ax. cbn in CL. destruct Wf_dec; [|easy]. set (used := Vars.union _ _) in *. destruct (fresh_cst_in_cands used nc) as (m,Hm). assert (NI := fresh_cst_ok used nc (csts_inj _ nc)). set (c := fresh_cst used nc) in *. exists c; split. - rewrite Hm. cbn. replace (test th nc (nc m)) with true; auto. symmetry. apply test_ok. now exists m. - apply ax_thm. apply Ax. now left. Qed. `````` Pierre Letouzey committed Feb 26, 2019 1065 `````` `````` Pierre Letouzey committed Apr 03, 2019 1066 1067 ``````(** Completeness of a theory *) `````` Pierre Letouzey committed Apr 02, 2019 1068 ``````Definition Complete th := `````` Pierre Letouzey committed Apr 09, 2019 1069 `````` forall A, Wf th A -> `````` Pierre Letouzey committed Apr 02, 2019 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 `````` IsTheorem th A \/ IsTheorem th (~A)%form. Definition DecidedBy (Ax:formula->Prop) f := exists c, Forall Ax c /\ (Pr logic (c ⊢ f) \/ Pr logic (c ⊢ ~f)). Fixpoint ax_completion th n : formula -> Prop := match n with | 0 => IsAxiom th | S n => let prev := ax_completion th n in fun f => prev f \/ `````` Pierre Letouzey committed Apr 09, 2019 1082 `````` (f = decode_form n /\ Wf th f /\ ~DecidedBy prev f) `````` Pierre Letouzey committed Apr 02, 2019 1083 1084 1085 1086 1087 1088 `````` end. Definition ax_infinite_completion th := fun f => exists n, ax_completion th n f. Lemma completion_wf th n : `````` Pierre Letouzey committed Apr 09, 2019 1089 `````` forall A, ax_completion th n A -> Wf th A. `````` Pierre Letouzey committed Apr 02, 2019 1090 1091 1092 1093 1094 1095 1096 ``````Proof. induction n; simpl. - apply WfAxiom. - intuition. Qed. Lemma infcompletion_wf th : `````` Pierre Letouzey committed Apr 09, 2019 1097 `````` forall A, ax_infinite_completion th A -> Wf th A. `````` Pierre Letouzey committed Apr 02, 2019 1098 1099 1100 1101 1102 ``````Proof. intros A (n,HA). eapply completion_wf; eauto. Qed. Definition th_completion th n := `````` Pierre Letouzey committed Apr 09, 2019 1103 `````` {| sign := th; `````` Pierre Letouzey committed Apr 02, 2019 1104 1105 1106 1107 1108 `````` IsAxiom := ax_completion th n; WfAxiom := completion_wf th n |}. Definition th_infcompletion th := `````` Pierre Letouzey committed Apr 09, 2019 1109 `````` {| sign := th; `````` Pierre Letouzey committed Apr 02, 2019 1110 1111 1112 1113 1114 1115 1116 1117 1118 `````` IsAxiom := ax_infinite_completion th; WfAxiom := infcompletion_wf th |}. Lemma ax_completion_carac th n A : ax_completion th n A <-> IsAxiom th A \/ (exists m, m < n /\ A = decode_form m /\ `````` Pierre Letouzey committed Apr 09, 2019 1119 `````` Wf th A /\ `````` Pierre Letouzey committed Apr 02, 2019 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 `````` ~DecidedBy (ax_completion th m) A). Proof. induction n; simpl. - split; auto. intros [H|(m & Hm & _)]; auto. inversion Hm. - split; [intros [H|H]|intros [H|(m & Hm & H)]]. + apply IHn in H. destruct H as [H|(m & Hm & H)]; auto. right; exists m; auto with *. + right. exists n; auto with *. + left. apply IHn. now left. `````` Pierre Letouzey committed Apr 09, 2019 1130 `````` + inversion Hm; try subst; auto. `````` Pierre Letouzey committed Apr 02, 2019 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 `````` left. apply IHn. right. exists m. split; auto with *. Qed. Lemma ax_completion_grows th n m : n <= m -> forall A, ax_completion th n A -> ax_completion th m A. Proof. intros LE A. rewrite !ax_completion_carac. intros [H|(k & Hk & H)]; auto. right. exists k; auto with *. Qed. Lemma ax_completion_init th : forall A, IsAxiom th A -> ax_infinite_completion th A. Proof. intros A HA. now exists 0. Qed. Lemma th_infcompletion_extend th : Extend th (th_infcompletion th). Proof. apply extend_alt. split; simpl. - firstorder. - intros A HA. apply ax_thm. simpl. now apply ax_completion_init. Qed. Lemma adhoc_partition {A} c (U V:A -> Prop) l : Forall (fun x => U x \/ (x=c/\ V x)) l -> exists l', Forall U l' /\ (ListSubset l l' \/ (V c /\ ListSubset l (c::l'))). Proof. induction l. - exists []. split; auto. now left. - inversion_clear 1. destruct IHl as (l' & Hl' & OR); auto. destruct H0 as [H0|(<-,H0)]. + exists (a::l'); firstorder. + exists l'; firstorder. Qed. Lemma th_completion_consistent th n : Consistent th -> Consistent (th_completion th n). Proof. intros C. induction n; simpl. - unfold Consistent, IsTheorem. simpl. auto. - unfold Consistent, IsTheorem. simpl. set (fn := decode_form n). clearbody fn. intros (_ & axs & F & PR). apply adhoc_partition in F. destruct F as (axs' & F & [LS|((CL,ND),LS)]). + eapply Pr_weakening in PR; eauto. apply IHn. split. split; cbn; auto. exists axs'; cbn; auto. + apply ND. exists axs'; split; auto. right. apply R_Not_i. eapply Pr_weakening in PR; eauto. Qed. Lemma Forall_max th axs : Forall (ax_infinite_completion th) axs -> exists n, Forall (ax_completion th n) axs. Proof. induction axs. - intros _. now exists 0. - inversion_clear 1. destruct IHaxs as (n & F); auto. destruct H0 as (n' & H0). exists (Nat.max n n'). constructor. apply ax_completion_grows with n'; auto with *. rewrite Forall_forall in F |- *. intros x Hx. apply ax_completion_grows with n; auto with *. Qed. Lemma th_infcompletion_consistent th : Consistent th -> Consistent (th_infcompletion th). Proof. intros C. unfold Consistent, IsTheorem. simpl. intros (_ & axs & F & PR). apply Forall_max in F. destruct F as (n,F). apply (th_completion_consistent th n) in C. apply C. split. split; cbn; auto. now exists axs. Qed. `````` Pierre Letouzey committed Apr 09, 2019 1215 1216 ``````Definition MyExcludedMiddle := forall Ax A, DecidedBy Ax A \/ ~DecidedBy Ax A. `````` Pierre Letouzey committed Apr 02, 2019 1217 1218 `````` Lemma th_completion_decides_fn th n : `````` Pierre Letouzey committed Apr 09, 2019 1219 1220 `````` MyExcludedMiddle -> Wf th (decode_form n) -> `````` Pierre Letouzey committed Apr 02, 2019 1221 1222 `````` DecidedBy (ax_completion th (S n)) (decode_form n). Proof. `````` Pierre Letouzey committed Apr 09, 2019 1223 `````` intros EM. `````` Pierre Letouzey committed Apr 02, 2019 1224 1225 1226 1227 `````` set (fn := decode_form n). intros CL. unfold DecidedBy. simpl. `````` Pierre Letouzey committed Apr 09, 2019 1228 `````` destruct (EM (ax_completion th n) fn) as [(axs & F & OR)|N]. `````` Pierre Letouzey committed Apr 02, 2019 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 `````` - exists axs; split; auto. rewrite Forall_forall in *; intuition. - exists [fn]; split; auto. left. apply R_Ax; simpl; auto. Qed. Lemma completion_infcompletion_extend th n A : IsTheorem (th_completion th n) A -> IsTheorem (th_infcompletion th) A. Proof. intros (CL & axs & F & PR). split; auto. exists axs; split; auto. simpl in *. rewrite Forall_forall in *. intros x Hx. exists n; auto. Qed. Lemma th_infcompletion_complete th : `````` Pierre Letouzey committed Apr 09, 2019 1247 `````` MyExcludedMiddle -> `````` Pierre Letouzey committed Apr 02, 2019 1248 1249 `````` Complete (th_infcompletion th). Proof. `````` Pierre Letouzey committed Apr 09, 2019 1250 `````` intros EM A CL. `````` Pierre Letouzey committed Apr 02, 2019 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 `````` destruct (th_completion_decides_fn th (code_form A)) as (axs & F & OR); rewrite ?decode_code_form in *; auto. set (n := code_form A) in *. clearbody n. destruct OR as [LF|RG]; [left|right]; apply completion_infcompletion_extend with (S n). - split; auto. exists axs; auto. - split; auto. exists axs; auto. Qed. Theorem completion th : `````` Pierre Letouzey committed Apr 09, 2019 1261 `````` MyExcludedMiddle -> `````` Pierre Letouzey committed Apr 02, 2019 1262 1263 1264 `````` Consistent th -> exists th', Extend th th' /\ Consistent th' /\ Complete th'. Proof. `````` Pierre Letouzey committed Apr 09, 2019 1265 `````` intros EM C. `````` Pierre Letouzey committed Apr 02, 2019 1266 1267 1268 `````` exists (th_infcompletion th); split; [|split]. - apply th_infcompletion_extend. - now apply th_infcompletion_consistent. `````` Pierre Letouzey committed Apr 09, 2019 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 `````` - apply th_infcompletion_complete; auto. Qed. (** Combining both saturation and completion *) Definition supercomplete th (nc : NewCsts th) := th_infcompletion (HenkinAll_ext th nc). Lemma supercomplete_extend th nc : Extend th (supercomplete th nc). Proof. eapply extend_trans; [|eapply th_infcompletion_extend]. apply HenkinAll_extend. Qed. Lemma supercomplete_consistent th nc : logic = Classic -> Consistent th -> Consistent (supercomplete th nc). Proof. intros LG C. apply th_infcompletion_consistent. apply HenkinAll_consistent; auto. `````` Pierre Letouzey committed Apr 02, 2019 1291 1292 ``````Qed. `````` Pierre Letouzey committed Apr 09, 2019 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 ``````Lemma supercomplete_supersaturated th nc : logic = Classic -> WitnessSuperSaturated (supercomplete th nc). Proof. intros LG. intros A WF. cbn in WF. destruct (HenkinAll_ext_supersaturated th nc LG A WF) as (c & Hc & Thm). exists c. split; auto. unfold supercomplete. now apply th_infcompletion_extend. Qed. Lemma supercomplete_saturated th nc : logic = Classic -> WitnessSaturated (supercomplete th nc). Proof. intros LG. now apply supersaturated_saturated, supercomplete_supersaturated. Qed. Lemma supercomplete_complete th nc : MyExcludedMiddle -> Complete (supercomplete th nc). Proof. apply th_infcompletion_complete. Qed. Lemma supercompletion : logic = Classic -> MyExcludedMiddle -> forall th (nc : NewCsts th), Consistent th -> `````` Pierre Letouzey committed Apr 15, 2019 1325 `````` { th' | `````` Pierre Letouzey committed Apr 09, 2019 1326 `````` Extend th th' /\ Consistent th' /\ `````` Pierre Letouzey committed Apr 15, 2019 1327 `````` WitnessSaturated th' /\ Complete th' }. `````` Pierre Letouzey committed Apr 09, 2019 1328 1329 1330 1331 1332 1333 1334 1335 ``````Proof. intros LG EM th nc C. exists (supercomplete th nc). split;[|split;[|split]]. - now apply supercomplete_extend. - now apply supercomplete_consistent. - now apply supercomplete_saturated. - now apply supercomplete_complete. Qed. `````` Pierre Letouzey committed Apr 02, 2019 1336 `````` `````` Pierre Letouzey committed Feb 26, 2019 1337 ``End SomeLogic.``