CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_Lindenbaum_lem.
Require Import CPP_BiInt_soundness_constr.
Section WLEMS_Quasi_completeness.
Class Canon_worlds : Type :=
{ prim : @Ensemble (BPropF) ;
NotDer : ~ (BIH_rules (prim, Bot)) ;
Closed : closed prim ;
Stable : stable prim ;
Prime : prime prim
}.
Definition Canon_rel (P0 P1 : Canon_worlds) : Prop :=
Included _ (@prim P0) (@prim P1).
Definition Canon_val (P : Canon_worlds) (q : nat) : Prop :=
In _ prim (# q).
Lemma C_R_refl u : Canon_rel u u.
Proof.
unfold Canon_rel. intro. auto.
Qed.
Lemma C_R_trans u v w: Canon_rel u v -> Canon_rel v w -> Canon_rel u w.
Proof.
intros. intro. intros. auto.
Qed.
Lemma C_val_persist : forall u v, Canon_rel u v -> forall p, Canon_val u p -> Canon_val v p.
Proof.
intros. apply H. auto.
Qed.
Instance CM : model :=
{|
nodes := Canon_worlds ;
reachable := Canon_rel ;
val := Canon_val ;
reach_refl := C_R_refl ;
reach_tran := C_R_trans ;
persist := C_val_persist ;
|}.
Axiom WLEMS : forall p : BPropF -> Prop, ~ ~ (forall A, ~ p A \/ ~ ~ p A).
Lemma WLEMS_prime Γ :
stable Γ -> quasi_prime Γ -> ~ ~ prime Γ.
Proof.
intros H1 H2 H3. apply (WLEMS Γ). intros H4.
apply H3. intros A B H. destruct (H4 A).
- right. apply H1. intros H'. apply H2 in H. intuition.
- left. now apply H1.
Qed.
Definition pseudo_complete (w : @Ensemble (BPropF) * @Ensemble (BPropF)) :=
forall A, ~ ~ (fst w A \/ snd w A).
Lemma WLEMS_Lindenbaum Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists Γm, Included _ Γ Γm
/\ closed Γm
/\ stable Γm
/\ ~ ~ prime Γm
/\ ~ pair_derrec (Γm, Δ).
Proof.
intros.
exists (prime_theory Γ Δ).
repeat split.
- intro. apply prime_theory_extens.
- apply closeder_fst_Lind_pair ; auto.
- apply stable_Lind_pair ; auto.
- apply WLEMS_prime. 2: apply quasi_prime_Lind_pair ; auto.
apply stable_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in H0 ; auto.
Qed.
Lemma WLEMS_world Γ Δ :
~ pair_derrec (Γ, Δ) ->
~~ exists w : Canon_worlds, Included _ Γ prim /\ Included _ Δ (Complement _ prim).
Proof.
intros (Γm & Γn & H1 & H2 & H3 & H4) % WLEMS_Lindenbaum H.
apply H3. intros H9. apply H. unshelve eexists.
- apply (Build_Canon_worlds Γm); intuition.
apply H4. exists [] ; repeat split ; auto. apply NoDup_nil.
intros ; auto. inversion H5.
- intuition. intros A HA0 HA1. apply H4. exists [A].
simpl ; repeat split ; auto. apply NoDup_cons. intro H8 ; inversion H8.
apply NoDup_nil. intros. destruct H0 ; try contradiction. subst ; auto.
unfold In in HA1. unfold prim in HA1.
apply MP with (ps:=[(Γm, A --> (Or A Bot));(Γm, A)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists A. exists Bot ; auto.
inversion H5 ; subst. apply Id. apply IdRule_I ; auto. inversion H6.
Qed.
Lemma truth_lemma : forall A (cp : Canon_worlds),
(wforces CM cp A) <-> (In _ (@prim cp) A).
Proof.
induction A ; intro ; split ; intros ; simpl ; try simpl in H ; auto.
(* Bot *)
- inversion H.
- apply NotDer. apply Id. apply IdRule_I. auto.
(* Top *)
- apply Closed. apply wTop.
(* And A1 A2 *)
- destruct H. apply IHA1 in H. simpl in H. apply IHA2 in H0. simpl in H0.
apply Closed.
apply MP with (ps:=[(prim, A1 --> (And A1 A2));(prim, A1)]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(prim, (A1 --> A2) --> (A1 --> (And A1 A2)));(prim, (A1 --> A2))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(prim, (A1 --> A1) --> (A1 --> A2) --> (A1 --> (And A1 A2)));(prim, (A1 --> A1))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA7_I. exists A1. exists A1. exists A2. auto. inversion H4.
subst. 2: inversion H5. apply wimp_Id_gen. inversion H3. subst. 2: inversion H4.
apply MP with (ps:=[(prim, A2 --> (A1 --> A2));(prim, A2)]).
2: apply MPRule_I. intros. inversion H4. subst. apply wThm_irrel.
inversion H5. subst. 2: inversion H6. apply Id. apply IdRule_I. assumption.
inversion H2. subst. apply Id. apply IdRule_I. assumption. inversion H3.
- split. apply IHA1. simpl. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp (And A1 A2) A1);(prim, (And A1 A2))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA5_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
apply IHA2. simpl. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp (And A1 A2) A2);(prim, (And A1 A2))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA6_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
(* Or A1 A2 *)
- destruct H.
apply IHA1 in H. simpl in H. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp A1 (Or A1 A2));(prim, A1)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA2_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
apply IHA2 in H. simpl in H. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp A2 (Or A1 A2));(prim, A2)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA3_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
- apply Prime in H ; auto. destruct H. left. apply IHA1 ; auto.
right. apply IHA2 ; auto.
(* Imp A1 A2 *)
- apply Stable. intros H0.
assert (pair_derrec (Union _ (prim) (Singleton _ A1), Singleton _ A2) -> False).
intro. apply gen_BIH_Deduction_Theorem in H1. apply H0.
{ apply Closed. destruct H1.
destruct H1. destruct H2. destruct x. simpl in H3. simpl in H2.
apply MP with (ps:=[(prim, Imp (Bot) (A1 --> A2));(prim, Bot)]). 2: apply MPRule_I.
intros. inversion H4. subst. apply wEFQ. inversion H5. 2: inversion H6. subst.
assumption. inversion H1. subst. pose (H2 b). assert (List.In b (b :: x)). apply in_eq.
apply s in H4. inversion H4. subst. destruct x. simpl in H3.
apply absorp_Or1 in H3. auto. pose (H2 b). assert (List.In b (A1 --> A2 :: b :: x)).
apply in_cons. apply in_eq. apply s0 in H5. inversion H5. subst. inversion H1.
subst. exfalso. apply H10. apply in_eq. }
apply WLEMS_world in H1. apply H1. intros [w[Hw1 Hw2]].
assert (J2: Canon_rel cp w). unfold Canon_rel. simpl.
intro. intros. apply Hw1. apply Union_introl. auto. apply H in J2.
apply IHA2 in J2. assert (In BPropF (Complement _ prim) A2). apply Hw2.
apply In_singleton. apply H2 ; auto.
apply IHA1. simpl. apply Hw1. apply Union_intror. apply In_singleton.
- intros.
apply IHA1 in H1. simpl in H1. unfold Canon_rel in H0. simpl in H0.
apply H0 in H.
apply IHA2. simpl.
assert (pair_derrec (prim, Singleton _ A2)). exists [A2]. repeat split.
apply NoDup_cons ; auto ; apply NoDup_nil. intros. inversion H2. subst. apply In_singleton.
inversion H3. simpl.
apply MP with (ps:=[(prim, Imp A2 (Or A2 (Bot)));(prim, A2)]). 2: apply MPRule_I.
intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA2_I. exists A2. exists (Bot).
auto. inversion H3. subst.
apply MP with (ps:=[(prim, Imp A1 A2);(prim, A1)]). 2: apply MPRule_I.
intros. inversion H4. subst. apply Id. apply IdRule_I. auto.
inversion H5. 2: inversion H6. subst. apply Id. apply IdRule_I. auto.
inversion H4.
apply Closed. destruct H2. destruct H2.
destruct H3. destruct x. simpl in H4. apply MP with (ps:=[(prim, Imp (Bot) A2);(prim, Bot)]).
2: apply MPRule_I. intros. inversion H5. subst. apply wEFQ. inversion H6. 2: inversion H7.
subst. auto. inversion H2. subst. pose (H3 b). assert (List.In b (b :: x)).
apply in_eq. apply s in H5. inversion H5. subst. destruct x. simpl in H4.
apply absorp_Or1 in H4. auto. exfalso. pose (H3 b0). assert (List.In b0 (b :: b0 :: x)).
apply in_cons. apply in_eq. apply s0 in H6. inversion H6. subst. apply H7. apply in_eq.
(* Excl A1 A2 *)
- apply Stable. intros Hw. apply H. intros. apply IHA1 in H1.
assert (In (BPropF) (prim) (Or A2 (Excl A1 A2))).
{ apply Closed.
apply MP with (ps:=[(prim, Imp A1 (Or A2 (Excl A1 A2)));(prim, A1)]). 2: apply MPRule_I.
intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA11_I. exists A1.
exists A2. auto. inversion H3. 2: inversion H4. subst. apply Id. apply IdRule_I. auto. }
apply Prime in H2. destruct H2 ; auto. apply IHA2 ; auto. contradict Hw. apply H0, H2.
- assert (pair_derrec ((Singleton _ A1), Union _ (Complement _ prim) (Singleton _ A2)) -> False).
intro. destruct H0. destruct H0. destruct H1. simpl in H2. simpl in H1.
pose (remove_disj x A2 (Singleton (BPropF) A1)).
assert (BIH_rules (Singleton (BPropF) A1, Or A2 (list_disj (remove eq_dec_form A2 x)))).
apply MP with (ps:=[(Singleton (BPropF) A1, list_disj x --> Or A2
(list_disj (remove eq_dec_form A2 x)));(Singleton (BPropF) A1, list_disj x)]).
2: apply MPRule_I. intros. inversion H3. subst. auto. inversion H4. subst.
auto. inversion H5. clear b. clear H2.
assert (Singleton (BPropF) A1 = Union _ (Empty_set _) (Singleton (BPropF) A1)).
apply Extensionality_Ensembles. split. intro. intros. inversion H2. subst.
apply Union_intror. apply In_singleton. intro. intros. inversion H2.
subst. inversion H4. inversion H4. subst. apply In_singleton. rewrite H2 in H3.
assert (J1: Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1) =
Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1)). auto.
assert (J2: Or A2 (list_disj (remove eq_dec_form A2 x)) = Or A2 (list_disj (remove eq_dec_form A2 x))). auto.
pose (BIH_Deduction_Theorem (Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1),
Or A2 (list_disj (remove eq_dec_form A2 x))) H3 A1 (Or A2 (list_disj (remove eq_dec_form A2 x)))
(Empty_set _) J1 J2). apply wdual_residuation in b. clear J2. clear J1. clear H2.
assert (prim (list_disj (remove eq_dec_form A2 x))). apply Closed.
apply MP with (ps:=[(prim, Excl A1 A2 --> list_disj (remove eq_dec_form A2 x));(prim, Excl A1 A2)]).
2: apply MPRule_I. intros. inversion H2. subst.
pose (BIH_monot (Empty_set (BPropF), Excl A1 A2 --> list_disj (remove eq_dec_form A2 x))
b (prim)). apply b0. clear b0. simpl. intro. intros. inversion H4. inversion H4.
subst. 2: inversion H5. clear H2. apply Id. apply IdRule_I. auto.
apply list_disj_prime in H2. destruct H2. destruct H2.
apply in_remove in H2 ; destruct H2.
apply H1 in H2. inversion H2 ; subst. auto. inversion H6 ; subst ; auto.
2: apply Prime. apply NotDer.
intros Hv. apply WLEMS_world in H0. apply H0. intros [w[Hw1 Hw2]].
enough (exists v, Canon_rel v cp /\ wforces CM v A1 /\ ~ wforces CM v A2) by firstorder.
exists w. split; try apply Hw1. unfold Canon_rel.
intro. intros. apply Stable. intros Hx. pose (Hw2 x). simpl in i.
assert (In (BPropF) (Union (BPropF) (Complement _ (@prim cp)) (Singleton (BPropF) A2)) x).
apply Union_introl. auto.
apply i in H2. auto.
split. apply IHA1. simpl. apply Hw1. apply In_singleton.
intro. apply IHA2 in H1.
assert (In _ (Union BPropF (Complement BPropF (@prim cp)) (Singleton BPropF A2)) A2).
apply Union_intror ; apply In_singleton ; auto. pose (Hw2 A2 H2).
auto.
Qed.
Theorem Quasi_completeness : forall s,
(BIH_rules s -> False) -> ((loc_conseq (fst s) (snd s)) -> False).
Proof.
intros s WD H.
assert ((pair_derrec (fst s, Singleton _ (snd s))) -> False). intro. apply WD.
destruct H0. destruct H0. destruct H1. simpl in *. destruct x. simpl in H2. destruct s.
simpl in *.
apply MP with (ps:=[(e, Imp Bot b);(e, Bot)]). 2: apply MPRule_I.
intros. inversion H3. subst. Search Bot. apply wEFQ. inversion H4. subst.
2: inversion H5. auto.
simpl in H2. destruct x. simpl in H2. destruct s. simpl in *.
assert (b0=b). pose (H1 b). destruct s ; auto. subst. apply absorp_Or1 ; auto. simpl in *.
exfalso. pose (H1 b). pose (H1 b0). destruct s0 ; destruct s1 ; auto. rewrite NoDup_cons_iff in H0.
destruct H0. apply H0 ; apply in_eq.
apply WLEMS_world in H0. apply H0. intros (w & H1 & H2).
assert ((forall A : BPropF, In (BPropF) (fst s) A -> wforces CM w A)). intros. apply truth_lemma. auto.
apply H in H3. apply truth_lemma in H3.
pose (H2 (snd s)). destruct i. apply In_singleton. auto.
Qed.
End WLEMS_Quasi_completeness.
Print Assumptions Quasi_completeness.
Section Quasi_completeness_WLEMS.
(* Reformulation of BIH_finite *)
Definition fromlist {X} (L : list X) : Ensemble X :=
fun x => List.In x L.
Lemma BIH_finite' T A :
BIH_rules (T, A) -> exists L : list (BPropF), (forall B, List.In B L -> T B) /\ BIH_rules (fromlist L, A).
Proof.
intros [T'[H1[H2[L HL]]]] % BIH_finite. cbn in *. exists L. split.
- intros B HB. apply H1, HL, HB.
- eapply (BIH_monot (T', A)); trivial. cbn. intros B HB. apply HL, HB.
Qed.
(* Assumme enough variables in V *)
Variable i : nat -> nat.
Definition Var' n := Var (i n).
(* Assumme not too many variables in V *)
Variable j : nat -> nat.
Hypothesis Hij : forall x, j (i x) = x.
Variable p : nat -> Prop.
Let Tp phi :=
exists n, phi = Or (Var' n) (Neg (Var' n)) \/ p n /\ phi = Var' n \/ ~ p n /\ phi = Neg (Var' n).
Instance bounded_model (N : nat) :
model.
Proof.
unshelve econstructor.
- exact unit.
- exact (fun _ _ => True).
- exact (fun _ x => if j x <=? N then p (j x) else True).
- split; auto.
- cbn. trivial.
- intuition.
Defined.
Lemma bounded_model_dec' N :
~ ~ forall x, wforces (bounded_model N) tt (Var x) \/ (wforces (bounded_model N) tt (Var x) -> False).
Proof.
cbn. induction N; intros HX.
- assert (H' : ~ ~ (p 0 \/ ~ p 0)) by tauto. apply H'. intros H.
apply HX. intros x. assert (j x <= 0 \/ 0 < j x) as [Hx|Hx] by lia.
+ rewrite (Compare_dec.leb_correct _ _ Hx). assert (j x = 0) as -> by lia. apply H.
+ apply Compare_dec.leb_iff_conv in Hx as ->. now left.
- apply IHN. intros IHN'. assert (H' : ~ ~ (p (S N) \/ ~ p (S N))) by tauto. apply H'. intros H.
apply HX. intros x. destruct (j x <=? S N) eqn : Hb; try now left.
specialize (IHN' x). destruct (j x <=? N) eqn : Hb'; try apply IHN'.
enough (j x = S N) as -> by apply H.
apply Nat.leb_le in Hb. apply Nat.leb_nle in Hb'. lia.
Qed.
Lemma bounded_model_dec N :
~ ~ model_dec (bounded_model N).
Proof.
intros H. apply bounded_model_dec' with N. intros HN.
apply H. intros [] A. induction A; cbn; try now intuition.
- apply HN.
- destruct IHA1, IHA2.
+ left. now intros [].
+ right. firstorder.
+ left. now intros [].
+ left. now intros [].
- destruct IHA1, IHA2.
+ right. intro. apply H2. intros. destruct v ; auto.
+ left. intro. apply H2 in H0 ; auto.
+ right. intro. apply H2. intros. destruct v ; auto.
+ right. intro. apply H2. intros. destruct v ; auto. exfalso ; auto.
Qed.
Let Tp_bounded N phi :=
exists n, n <= N /\ (phi = Or (Var' n) (Neg (Var' n)) \/ p n /\ phi = Var' n \/ ~ p n /\ phi = Neg (Var' n)).
Lemma list_bounded L :
(forall A, List.In A L -> Tp A) -> exists N, forall A, List.In A L -> Tp_bounded N A.
Proof.
intros HL. induction L as [|B L IH].
- exists 0. intros A [].
- destruct (HL B) as [n Hn]; try now left.
destruct IH as [N HN]; try now intuition.
exists (N + n). intros A [->|HA].
+ exists n. split; try apply Hn. lia.
+ apply HN in HA as [n'[H1 H2]]. exists n'. split; try apply H2. lia.
Qed.
Lemma list_consistent' L N :
(forall A, List.In A L -> Tp_bounded N A) -> ~ ~ (forall A, List.In A L -> wforces (bounded_model N) tt A).
Proof.
intros HL. induction L as [|B L IH].
- intros H. apply H. intros A [].
- destruct (HL B) as [n [H1 H2]]; try now left.
intros H. apply IH; try now intuition. intros IH'.
assert (Hn : ~ ~ (p n \/ ~ p n)) by tauto. apply Hn. intros Hn'.
apply H. intros A [->|HA]; try now apply IH'. destruct H2 as [->|[[H2 ->]|[H2 ->]]].
+ cbn. rewrite Hij. apply Nat.leb_le in H1 as ->. tauto.
+ cbn. rewrite Hij. apply Nat.leb_le in H1 as ->. tauto.
+ cbn. rewrite Hij. apply Nat.leb_le in H1 as ->. tauto.
Qed.
Lemma list_consistent L :
(forall A, List.In A L -> Tp A) -> exists N, ~ ~ (forall A, List.In A L -> wforces (bounded_model N) tt A).
Proof.
intros [N HN] % list_bounded. exists N. now apply list_consistent'.
Qed.
Lemma Tp_consistent :
~ BIH_rules (Tp, Bot).
Proof.
intros H. apply BIH_finite' in H as [L[H1 H2]].
apply list_consistent in H1 as [N HN]. apply HN. intros HN'.
apply (bounded_model_dec N). intros HM.
apply wSoundness_dec in H2. cbn in H2. destruct (H2 (bounded_model N) tt).
- apply HM.
- apply HN'.
Qed.
Definition QuasiComp :=
forall T A, loc_conseq T A -> ~ ~ BIH_rules (T, A).
Theorem QuasiComp_WLEMS :
QuasiComp -> ~ ~ forall n, ~ p n \/ ~ ~ p n.
Proof.
intros HQC Hp. apply (@HQC Tp (Bot)); try apply Tp_consistent.
intros M w HM. apply Hp. intros n.
destruct (HM (Or (Var' n) (Neg (Var' n)))) as [H|H].
- exists n. now left.
- right. intros HP. assert (HTP : Tp (Neg (Var' n))) by (unfold Tp; intuition eauto).
apply (HM (Neg (Var' n)) HTP w); try apply reach_refl. apply H.
- left. intros HP. apply (H w); try apply reach_refl.
assert (HTP : Tp (Var' n)) by (unfold Tp; intuition eauto). apply (HM (Var' n) HTP).
Qed.
End Quasi_completeness_WLEMS.
Print Assumptions QuasiComp_WLEMS.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_Lindenbaum_lem.
Require Import CPP_BiInt_soundness_constr.
Section WLEMS_Quasi_completeness.
Class Canon_worlds : Type :=
{ prim : @Ensemble (BPropF) ;
NotDer : ~ (BIH_rules (prim, Bot)) ;
Closed : closed prim ;
Stable : stable prim ;
Prime : prime prim
}.
Definition Canon_rel (P0 P1 : Canon_worlds) : Prop :=
Included _ (@prim P0) (@prim P1).
Definition Canon_val (P : Canon_worlds) (q : nat) : Prop :=
In _ prim (# q).
Lemma C_R_refl u : Canon_rel u u.
Proof.
unfold Canon_rel. intro. auto.
Qed.
Lemma C_R_trans u v w: Canon_rel u v -> Canon_rel v w -> Canon_rel u w.
Proof.
intros. intro. intros. auto.
Qed.
Lemma C_val_persist : forall u v, Canon_rel u v -> forall p, Canon_val u p -> Canon_val v p.
Proof.
intros. apply H. auto.
Qed.
Instance CM : model :=
{|
nodes := Canon_worlds ;
reachable := Canon_rel ;
val := Canon_val ;
reach_refl := C_R_refl ;
reach_tran := C_R_trans ;
persist := C_val_persist ;
|}.
Axiom WLEMS : forall p : BPropF -> Prop, ~ ~ (forall A, ~ p A \/ ~ ~ p A).
Lemma WLEMS_prime Γ :
stable Γ -> quasi_prime Γ -> ~ ~ prime Γ.
Proof.
intros H1 H2 H3. apply (WLEMS Γ). intros H4.
apply H3. intros A B H. destruct (H4 A).
- right. apply H1. intros H'. apply H2 in H. intuition.
- left. now apply H1.
Qed.
Definition pseudo_complete (w : @Ensemble (BPropF) * @Ensemble (BPropF)) :=
forall A, ~ ~ (fst w A \/ snd w A).
Lemma WLEMS_Lindenbaum Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists Γm, Included _ Γ Γm
/\ closed Γm
/\ stable Γm
/\ ~ ~ prime Γm
/\ ~ pair_derrec (Γm, Δ).
Proof.
intros.
exists (prime_theory Γ Δ).
repeat split.
- intro. apply prime_theory_extens.
- apply closeder_fst_Lind_pair ; auto.
- apply stable_Lind_pair ; auto.
- apply WLEMS_prime. 2: apply quasi_prime_Lind_pair ; auto.
apply stable_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in H0 ; auto.
Qed.
Lemma WLEMS_world Γ Δ :
~ pair_derrec (Γ, Δ) ->
~~ exists w : Canon_worlds, Included _ Γ prim /\ Included _ Δ (Complement _ prim).
Proof.
intros (Γm & Γn & H1 & H2 & H3 & H4) % WLEMS_Lindenbaum H.
apply H3. intros H9. apply H. unshelve eexists.
- apply (Build_Canon_worlds Γm); intuition.
apply H4. exists [] ; repeat split ; auto. apply NoDup_nil.
intros ; auto. inversion H5.
- intuition. intros A HA0 HA1. apply H4. exists [A].
simpl ; repeat split ; auto. apply NoDup_cons. intro H8 ; inversion H8.
apply NoDup_nil. intros. destruct H0 ; try contradiction. subst ; auto.
unfold In in HA1. unfold prim in HA1.
apply MP with (ps:=[(Γm, A --> (Or A Bot));(Γm, A)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists A. exists Bot ; auto.
inversion H5 ; subst. apply Id. apply IdRule_I ; auto. inversion H6.
Qed.
Lemma truth_lemma : forall A (cp : Canon_worlds),
(wforces CM cp A) <-> (In _ (@prim cp) A).
Proof.
induction A ; intro ; split ; intros ; simpl ; try simpl in H ; auto.
(* Bot *)
- inversion H.
- apply NotDer. apply Id. apply IdRule_I. auto.
(* Top *)
- apply Closed. apply wTop.
(* And A1 A2 *)
- destruct H. apply IHA1 in H. simpl in H. apply IHA2 in H0. simpl in H0.
apply Closed.
apply MP with (ps:=[(prim, A1 --> (And A1 A2));(prim, A1)]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(prim, (A1 --> A2) --> (A1 --> (And A1 A2)));(prim, (A1 --> A2))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(prim, (A1 --> A1) --> (A1 --> A2) --> (A1 --> (And A1 A2)));(prim, (A1 --> A1))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA7_I. exists A1. exists A1. exists A2. auto. inversion H4.
subst. 2: inversion H5. apply wimp_Id_gen. inversion H3. subst. 2: inversion H4.
apply MP with (ps:=[(prim, A2 --> (A1 --> A2));(prim, A2)]).
2: apply MPRule_I. intros. inversion H4. subst. apply wThm_irrel.
inversion H5. subst. 2: inversion H6. apply Id. apply IdRule_I. assumption.
inversion H2. subst. apply Id. apply IdRule_I. assumption. inversion H3.
- split. apply IHA1. simpl. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp (And A1 A2) A1);(prim, (And A1 A2))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA5_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
apply IHA2. simpl. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp (And A1 A2) A2);(prim, (And A1 A2))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA6_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
(* Or A1 A2 *)
- destruct H.
apply IHA1 in H. simpl in H. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp A1 (Or A1 A2));(prim, A1)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA2_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
apply IHA2 in H. simpl in H. apply Closed ; auto.
apply MP with (ps:=[(prim, Imp A2 (Or A1 A2));(prim, A2)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA3_I. exists A1. exists A2. auto. inversion H1. 2: inversion H2.
subst. apply Id. apply IdRule_I ; auto.
- apply Prime in H ; auto. destruct H. left. apply IHA1 ; auto.
right. apply IHA2 ; auto.
(* Imp A1 A2 *)
- apply Stable. intros H0.
assert (pair_derrec (Union _ (prim) (Singleton _ A1), Singleton _ A2) -> False).
intro. apply gen_BIH_Deduction_Theorem in H1. apply H0.
{ apply Closed. destruct H1.
destruct H1. destruct H2. destruct x. simpl in H3. simpl in H2.
apply MP with (ps:=[(prim, Imp (Bot) (A1 --> A2));(prim, Bot)]). 2: apply MPRule_I.
intros. inversion H4. subst. apply wEFQ. inversion H5. 2: inversion H6. subst.
assumption. inversion H1. subst. pose (H2 b). assert (List.In b (b :: x)). apply in_eq.
apply s in H4. inversion H4. subst. destruct x. simpl in H3.
apply absorp_Or1 in H3. auto. pose (H2 b). assert (List.In b (A1 --> A2 :: b :: x)).
apply in_cons. apply in_eq. apply s0 in H5. inversion H5. subst. inversion H1.
subst. exfalso. apply H10. apply in_eq. }
apply WLEMS_world in H1. apply H1. intros [w[Hw1 Hw2]].
assert (J2: Canon_rel cp w). unfold Canon_rel. simpl.
intro. intros. apply Hw1. apply Union_introl. auto. apply H in J2.
apply IHA2 in J2. assert (In BPropF (Complement _ prim) A2). apply Hw2.
apply In_singleton. apply H2 ; auto.
apply IHA1. simpl. apply Hw1. apply Union_intror. apply In_singleton.
- intros.
apply IHA1 in H1. simpl in H1. unfold Canon_rel in H0. simpl in H0.
apply H0 in H.
apply IHA2. simpl.
assert (pair_derrec (prim, Singleton _ A2)). exists [A2]. repeat split.
apply NoDup_cons ; auto ; apply NoDup_nil. intros. inversion H2. subst. apply In_singleton.
inversion H3. simpl.
apply MP with (ps:=[(prim, Imp A2 (Or A2 (Bot)));(prim, A2)]). 2: apply MPRule_I.
intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA2_I. exists A2. exists (Bot).
auto. inversion H3. subst.
apply MP with (ps:=[(prim, Imp A1 A2);(prim, A1)]). 2: apply MPRule_I.
intros. inversion H4. subst. apply Id. apply IdRule_I. auto.
inversion H5. 2: inversion H6. subst. apply Id. apply IdRule_I. auto.
inversion H4.
apply Closed. destruct H2. destruct H2.
destruct H3. destruct x. simpl in H4. apply MP with (ps:=[(prim, Imp (Bot) A2);(prim, Bot)]).
2: apply MPRule_I. intros. inversion H5. subst. apply wEFQ. inversion H6. 2: inversion H7.
subst. auto. inversion H2. subst. pose (H3 b). assert (List.In b (b :: x)).
apply in_eq. apply s in H5. inversion H5. subst. destruct x. simpl in H4.
apply absorp_Or1 in H4. auto. exfalso. pose (H3 b0). assert (List.In b0 (b :: b0 :: x)).
apply in_cons. apply in_eq. apply s0 in H6. inversion H6. subst. apply H7. apply in_eq.
(* Excl A1 A2 *)
- apply Stable. intros Hw. apply H. intros. apply IHA1 in H1.
assert (In (BPropF) (prim) (Or A2 (Excl A1 A2))).
{ apply Closed.
apply MP with (ps:=[(prim, Imp A1 (Or A2 (Excl A1 A2)));(prim, A1)]). 2: apply MPRule_I.
intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA11_I. exists A1.
exists A2. auto. inversion H3. 2: inversion H4. subst. apply Id. apply IdRule_I. auto. }
apply Prime in H2. destruct H2 ; auto. apply IHA2 ; auto. contradict Hw. apply H0, H2.
- assert (pair_derrec ((Singleton _ A1), Union _ (Complement _ prim) (Singleton _ A2)) -> False).
intro. destruct H0. destruct H0. destruct H1. simpl in H2. simpl in H1.
pose (remove_disj x A2 (Singleton (BPropF) A1)).
assert (BIH_rules (Singleton (BPropF) A1, Or A2 (list_disj (remove eq_dec_form A2 x)))).
apply MP with (ps:=[(Singleton (BPropF) A1, list_disj x --> Or A2
(list_disj (remove eq_dec_form A2 x)));(Singleton (BPropF) A1, list_disj x)]).
2: apply MPRule_I. intros. inversion H3. subst. auto. inversion H4. subst.
auto. inversion H5. clear b. clear H2.
assert (Singleton (BPropF) A1 = Union _ (Empty_set _) (Singleton (BPropF) A1)).
apply Extensionality_Ensembles. split. intro. intros. inversion H2. subst.
apply Union_intror. apply In_singleton. intro. intros. inversion H2.
subst. inversion H4. inversion H4. subst. apply In_singleton. rewrite H2 in H3.
assert (J1: Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1) =
Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1)). auto.
assert (J2: Or A2 (list_disj (remove eq_dec_form A2 x)) = Or A2 (list_disj (remove eq_dec_form A2 x))). auto.
pose (BIH_Deduction_Theorem (Union (BPropF) (Empty_set (BPropF)) (Singleton (BPropF) A1),
Or A2 (list_disj (remove eq_dec_form A2 x))) H3 A1 (Or A2 (list_disj (remove eq_dec_form A2 x)))
(Empty_set _) J1 J2). apply wdual_residuation in b. clear J2. clear J1. clear H2.
assert (prim (list_disj (remove eq_dec_form A2 x))). apply Closed.
apply MP with (ps:=[(prim, Excl A1 A2 --> list_disj (remove eq_dec_form A2 x));(prim, Excl A1 A2)]).
2: apply MPRule_I. intros. inversion H2. subst.
pose (BIH_monot (Empty_set (BPropF), Excl A1 A2 --> list_disj (remove eq_dec_form A2 x))
b (prim)). apply b0. clear b0. simpl. intro. intros. inversion H4. inversion H4.
subst. 2: inversion H5. clear H2. apply Id. apply IdRule_I. auto.
apply list_disj_prime in H2. destruct H2. destruct H2.
apply in_remove in H2 ; destruct H2.
apply H1 in H2. inversion H2 ; subst. auto. inversion H6 ; subst ; auto.
2: apply Prime. apply NotDer.
intros Hv. apply WLEMS_world in H0. apply H0. intros [w[Hw1 Hw2]].
enough (exists v, Canon_rel v cp /\ wforces CM v A1 /\ ~ wforces CM v A2) by firstorder.
exists w. split; try apply Hw1. unfold Canon_rel.
intro. intros. apply Stable. intros Hx. pose (Hw2 x). simpl in i.
assert (In (BPropF) (Union (BPropF) (Complement _ (@prim cp)) (Singleton (BPropF) A2)) x).
apply Union_introl. auto.
apply i in H2. auto.
split. apply IHA1. simpl. apply Hw1. apply In_singleton.
intro. apply IHA2 in H1.
assert (In _ (Union BPropF (Complement BPropF (@prim cp)) (Singleton BPropF A2)) A2).
apply Union_intror ; apply In_singleton ; auto. pose (Hw2 A2 H2).
auto.
Qed.
Theorem Quasi_completeness : forall s,
(BIH_rules s -> False) -> ((loc_conseq (fst s) (snd s)) -> False).
Proof.
intros s WD H.
assert ((pair_derrec (fst s, Singleton _ (snd s))) -> False). intro. apply WD.
destruct H0. destruct H0. destruct H1. simpl in *. destruct x. simpl in H2. destruct s.
simpl in *.
apply MP with (ps:=[(e, Imp Bot b);(e, Bot)]). 2: apply MPRule_I.
intros. inversion H3. subst. Search Bot. apply wEFQ. inversion H4. subst.
2: inversion H5. auto.
simpl in H2. destruct x. simpl in H2. destruct s. simpl in *.
assert (b0=b). pose (H1 b). destruct s ; auto. subst. apply absorp_Or1 ; auto. simpl in *.
exfalso. pose (H1 b). pose (H1 b0). destruct s0 ; destruct s1 ; auto. rewrite NoDup_cons_iff in H0.
destruct H0. apply H0 ; apply in_eq.
apply WLEMS_world in H0. apply H0. intros (w & H1 & H2).
assert ((forall A : BPropF, In (BPropF) (fst s) A -> wforces CM w A)). intros. apply truth_lemma. auto.
apply H in H3. apply truth_lemma in H3.
pose (H2 (snd s)). destruct i. apply In_singleton. auto.
Qed.
End WLEMS_Quasi_completeness.
Print Assumptions Quasi_completeness.
Section Quasi_completeness_WLEMS.
(* Reformulation of BIH_finite *)
Definition fromlist {X} (L : list X) : Ensemble X :=
fun x => List.In x L.
Lemma BIH_finite' T A :
BIH_rules (T, A) -> exists L : list (BPropF), (forall B, List.In B L -> T B) /\ BIH_rules (fromlist L, A).
Proof.
intros [T'[H1[H2[L HL]]]] % BIH_finite. cbn in *. exists L. split.
- intros B HB. apply H1, HL, HB.
- eapply (BIH_monot (T', A)); trivial. cbn. intros B HB. apply HL, HB.
Qed.
(* Assumme enough variables in V *)
Variable i : nat -> nat.
Definition Var' n := Var (i n).
(* Assumme not too many variables in V *)
Variable j : nat -> nat.
Hypothesis Hij : forall x, j (i x) = x.
Variable p : nat -> Prop.
Let Tp phi :=
exists n, phi = Or (Var' n) (Neg (Var' n)) \/ p n /\ phi = Var' n \/ ~ p n /\ phi = Neg (Var' n).
Instance bounded_model (N : nat) :
model.
Proof.
unshelve econstructor.
- exact unit.
- exact (fun _ _ => True).
- exact (fun _ x => if j x <=? N then p (j x) else True).
- split; auto.
- cbn. trivial.
- intuition.
Defined.
Lemma bounded_model_dec' N :
~ ~ forall x, wforces (bounded_model N) tt (Var x) \/ (wforces (bounded_model N) tt (Var x) -> False).
Proof.
cbn. induction N; intros HX.
- assert (H' : ~ ~ (p 0 \/ ~ p 0)) by tauto. apply H'. intros H.
apply HX. intros x. assert (j x <= 0 \/ 0 < j x) as [Hx|Hx] by lia.
+ rewrite (Compare_dec.leb_correct _ _ Hx). assert (j x = 0) as -> by lia. apply H.
+ apply Compare_dec.leb_iff_conv in Hx as ->. now left.
- apply IHN. intros IHN'. assert (H' : ~ ~ (p (S N) \/ ~ p (S N))) by tauto. apply H'. intros H.
apply HX. intros x. destruct (j x <=? S N) eqn : Hb; try now left.
specialize (IHN' x). destruct (j x <=? N) eqn : Hb'; try apply IHN'.
enough (j x = S N) as -> by apply H.
apply Nat.leb_le in Hb. apply Nat.leb_nle in Hb'. lia.
Qed.
Lemma bounded_model_dec N :
~ ~ model_dec (bounded_model N).
Proof.
intros H. apply bounded_model_dec' with N. intros HN.
apply H. intros [] A. induction A; cbn; try now intuition.
- apply HN.
- destruct IHA1, IHA2.
+ left. now intros [].
+ right. firstorder.
+ left. now intros [].
+ left. now intros [].
- destruct IHA1, IHA2.
+ right. intro. apply H2. intros. destruct v ; auto.
+ left. intro. apply H2 in H0 ; auto.
+ right. intro. apply H2. intros. destruct v ; auto.
+ right. intro. apply H2. intros. destruct v ; auto. exfalso ; auto.
Qed.
Let Tp_bounded N phi :=
exists n, n <= N /\ (phi = Or (Var' n) (Neg (Var' n)) \/ p n /\ phi = Var' n \/ ~ p n /\ phi = Neg (Var' n)).
Lemma list_bounded L :
(forall A, List.In A L -> Tp A) -> exists N, forall A, List.In A L -> Tp_bounded N A.
Proof.
intros HL. induction L as [|B L IH].
- exists 0. intros A [].
- destruct (HL B) as [n Hn]; try now left.
destruct IH as [N HN]; try now intuition.
exists (N + n). intros A [->|HA].
+ exists n. split; try apply Hn. lia.
+ apply HN in HA as [n'[H1 H2]]. exists n'. split; try apply H2. lia.
Qed.
Lemma list_consistent' L N :
(forall A, List.In A L -> Tp_bounded N A) -> ~ ~ (forall A, List.In A L -> wforces (bounded_model N) tt A).
Proof.
intros HL. induction L as [|B L IH].
- intros H. apply H. intros A [].
- destruct (HL B) as [n [H1 H2]]; try now left.
intros H. apply IH; try now intuition. intros IH'.
assert (Hn : ~ ~ (p n \/ ~ p n)) by tauto. apply Hn. intros Hn'.
apply H. intros A [->|HA]; try now apply IH'. destruct H2 as [->|[[H2 ->]|[H2 ->]]].
+ cbn. rewrite Hij. apply Nat.leb_le in H1 as ->. tauto.
+ cbn. rewrite Hij. apply Nat.leb_le in H1 as ->. tauto.
+ cbn. rewrite Hij. apply Nat.leb_le in H1 as ->. tauto.
Qed.
Lemma list_consistent L :
(forall A, List.In A L -> Tp A) -> exists N, ~ ~ (forall A, List.In A L -> wforces (bounded_model N) tt A).
Proof.
intros [N HN] % list_bounded. exists N. now apply list_consistent'.
Qed.
Lemma Tp_consistent :
~ BIH_rules (Tp, Bot).
Proof.
intros H. apply BIH_finite' in H as [L[H1 H2]].
apply list_consistent in H1 as [N HN]. apply HN. intros HN'.
apply (bounded_model_dec N). intros HM.
apply wSoundness_dec in H2. cbn in H2. destruct (H2 (bounded_model N) tt).
- apply HM.
- apply HN'.
Qed.
Definition QuasiComp :=
forall T A, loc_conseq T A -> ~ ~ BIH_rules (T, A).
Theorem QuasiComp_WLEMS :
QuasiComp -> ~ ~ forall n, ~ p n \/ ~ ~ p n.
Proof.
intros HQC Hp. apply (@HQC Tp (Bot)); try apply Tp_consistent.
intros M w HM. apply Hp. intros n.
destruct (HM (Or (Var' n) (Neg (Var' n)))) as [H|H].
- exists n. now left.
- right. intros HP. assert (HTP : Tp (Neg (Var' n))) by (unfold Tp; intuition eauto).
apply (HM (Neg (Var' n)) HTP w); try apply reach_refl. apply H.
- left. intros HP. apply (H w); try apply reach_refl.
assert (HTP : Tp (Var' n)) by (unfold Tp; intuition eauto). apply (HM (Var' n) HTP).
Qed.
End Quasi_completeness_WLEMS.
Print Assumptions QuasiComp_WLEMS.