CPPsiteProjPackage.CPP_BiInt_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 LEM_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 LEM : forall P, P \/ ~ P.
Lemma LEM_prime Γ :
quasi_prime Γ -> prime Γ.
Proof.
intros H1 A B H2.
apply H1 in H2. destruct (LEM (Γ A)) ; auto.
destruct (LEM (Γ B)) ; auto. exfalso. apply H2.
intro. destruct H3 ; auto.
Qed.
Lemma LEM_Lindenbaum Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists Γm, Included _ Γ Γm
/\ closed Γ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 LEM_prime. apply quasi_prime_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in H0 ; auto.
Qed.
Lemma LEM_world Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists w : Canon_worlds, Included _ Γ prim /\ Included _ Δ (Complement _ prim).
Proof.
intros (Γm & Γn & H1 & H2 & H3) % LEM_Lindenbaum.
unshelve eexists.
- apply (Build_Canon_worlds Γm); intuition ; simpl.
apply H3. exists [] ; repeat split ; auto. apply NoDup_nil.
intros ; auto. inversion H0. intros A H5.
destruct (LEM (Γm A)) ; intuition.
- intuition. intros A HA0 HA1. apply H3. exists [A].
simpl ; repeat split ; auto. apply NoDup_cons. intro H8 ; inversion H8.
apply NoDup_nil. intros. destruct H ; 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 H. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists A. exists Bot ; auto.
inversion H0 ; subst. apply Id. apply IdRule_I ; auto. inversion H4.
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. }
pose (LEM_world _ _ H1). destruct e as [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 LEM_world in H0. destruct H0 as [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 H1. auto.
split. apply IHA1. simpl. apply Hw1. apply In_singleton.
intro. apply IHA2 in H0.
assert (In _ (Union BPropF (Complement BPropF (@prim cp)) (Singleton BPropF A2)) A2).
apply Union_intror ; apply In_singleton ; auto. pose (Hw2 A2 H1).
auto.
Qed.
Theorem wQuasiCompleteness : 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 LEM_world in H0. destruct H0 as (w & H1 & H2).
assert ((forall A : BPropF, In (BPropF) (fst s) A -> wforces CM w A)). intros. apply truth_lemma. auto.
apply H in H0. apply truth_lemma in H0. simpl in H0.
pose (H2 (snd s)). destruct i. apply In_singleton. auto.
Qed.
Theorem wCompleteness : forall Γ A,
(loc_conseq Γ A) -> BIH_rules (Γ, A).
Proof.
intros Γ A LC. pose (wQuasiCompleteness (Γ, A)).
destruct (LEM (BIH_rules (Γ, A))) ; auto. exfalso.
apply f ; assumption.
Qed.
End LEM_completeness.
Print Assumptions wCompleteness.
(* 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.
(* Consistency *)
#[export] Instance point_model :
model.
Proof.
unshelve econstructor.
- exact unit.
- exact (fun _ _ => True).
- exact (fun _ _ => True).
- split; auto.
- cbn. trivial.
- intuition.
Defined.
Lemma point_model_dec :
model_dec point_model.
Proof.
intros [] A. induction A; cbn; try now intuition.
- destruct IHA1, IHA2.
+ left. now intros [].
+ right. firstorder.
+ left. now intros [].
+ left. now intros [].
- destruct IHA1, IHA2.
+ right. intro. apply H1. intros. destruct v ; auto.
+ left. intro. auto.
+ right. intro. apply H1. intros. destruct v ; auto.
+ right. intro. apply H1. intros. destruct v ; auto. exfalso ; auto.
Qed.
Lemma consistency :
~ BIH_rules (fromlist [], Bot).
Proof.
intros H % wSoundness_dec. cbn in H. destruct (H point_model tt).
- apply point_model_dec.
- intros A [].
Qed.
(* Completeness implies LEM *)
Section Completeness_LEM.
Variable P : Prop.
Let TLEM (phi : BPropF) :=
P \/ ~ P.
Definition Completeness :=
forall Γ A, loc_conseq Γ A -> BIH_rules (Γ, A).
Theorem Completeness_LEM :
Completeness -> P \/ ~ P.
Proof.
intros HC. assert (H : loc_conseq TLEM (Bot)).
- intros M w H. cbn.
assert (HP : ~ ~ (P \/ ~ P)) by intuition. apply HP. intros HP'.
apply (H (Bot)). apply HP'.
- apply HC in H. apply BIH_finite' in H as [L[H1 H2]]. destruct L as [|A L].
+ now apply consistency in H2.
+ apply (H1 A). now left.
Qed.
End Completeness_LEM.
Print Assumptions Completeness_LEM.
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 LEM_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 LEM : forall P, P \/ ~ P.
Lemma LEM_prime Γ :
quasi_prime Γ -> prime Γ.
Proof.
intros H1 A B H2.
apply H1 in H2. destruct (LEM (Γ A)) ; auto.
destruct (LEM (Γ B)) ; auto. exfalso. apply H2.
intro. destruct H3 ; auto.
Qed.
Lemma LEM_Lindenbaum Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists Γm, Included _ Γ Γm
/\ closed Γ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 LEM_prime. apply quasi_prime_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in H0 ; auto.
Qed.
Lemma LEM_world Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists w : Canon_worlds, Included _ Γ prim /\ Included _ Δ (Complement _ prim).
Proof.
intros (Γm & Γn & H1 & H2 & H3) % LEM_Lindenbaum.
unshelve eexists.
- apply (Build_Canon_worlds Γm); intuition ; simpl.
apply H3. exists [] ; repeat split ; auto. apply NoDup_nil.
intros ; auto. inversion H0. intros A H5.
destruct (LEM (Γm A)) ; intuition.
- intuition. intros A HA0 HA1. apply H3. exists [A].
simpl ; repeat split ; auto. apply NoDup_cons. intro H8 ; inversion H8.
apply NoDup_nil. intros. destruct H ; 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 H. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists A. exists Bot ; auto.
inversion H0 ; subst. apply Id. apply IdRule_I ; auto. inversion H4.
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. }
pose (LEM_world _ _ H1). destruct e as [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 LEM_world in H0. destruct H0 as [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 H1. auto.
split. apply IHA1. simpl. apply Hw1. apply In_singleton.
intro. apply IHA2 in H0.
assert (In _ (Union BPropF (Complement BPropF (@prim cp)) (Singleton BPropF A2)) A2).
apply Union_intror ; apply In_singleton ; auto. pose (Hw2 A2 H1).
auto.
Qed.
Theorem wQuasiCompleteness : 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 LEM_world in H0. destruct H0 as (w & H1 & H2).
assert ((forall A : BPropF, In (BPropF) (fst s) A -> wforces CM w A)). intros. apply truth_lemma. auto.
apply H in H0. apply truth_lemma in H0. simpl in H0.
pose (H2 (snd s)). destruct i. apply In_singleton. auto.
Qed.
Theorem wCompleteness : forall Γ A,
(loc_conseq Γ A) -> BIH_rules (Γ, A).
Proof.
intros Γ A LC. pose (wQuasiCompleteness (Γ, A)).
destruct (LEM (BIH_rules (Γ, A))) ; auto. exfalso.
apply f ; assumption.
Qed.
End LEM_completeness.
Print Assumptions wCompleteness.
(* 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.
(* Consistency *)
#[export] Instance point_model :
model.
Proof.
unshelve econstructor.
- exact unit.
- exact (fun _ _ => True).
- exact (fun _ _ => True).
- split; auto.
- cbn. trivial.
- intuition.
Defined.
Lemma point_model_dec :
model_dec point_model.
Proof.
intros [] A. induction A; cbn; try now intuition.
- destruct IHA1, IHA2.
+ left. now intros [].
+ right. firstorder.
+ left. now intros [].
+ left. now intros [].
- destruct IHA1, IHA2.
+ right. intro. apply H1. intros. destruct v ; auto.
+ left. intro. auto.
+ right. intro. apply H1. intros. destruct v ; auto.
+ right. intro. apply H1. intros. destruct v ; auto. exfalso ; auto.
Qed.
Lemma consistency :
~ BIH_rules (fromlist [], Bot).
Proof.
intros H % wSoundness_dec. cbn in H. destruct (H point_model tt).
- apply point_model_dec.
- intros A [].
Qed.
(* Completeness implies LEM *)
Section Completeness_LEM.
Variable P : Prop.
Let TLEM (phi : BPropF) :=
P \/ ~ P.
Definition Completeness :=
forall Γ A, loc_conseq Γ A -> BIH_rules (Γ, A).
Theorem Completeness_LEM :
Completeness -> P \/ ~ P.
Proof.
intros HC. assert (H : loc_conseq TLEM (Bot)).
- intros M w H. cbn.
assert (HP : ~ ~ (P \/ ~ P)) by intuition. apply HP. intros HP'.
apply (H (Bot)). apply HP'.
- apply HC in H. apply BIH_finite' in H as [L[H1 H2]]. destruct L as [|A L].
+ now apply consistency in H2.
+ apply (H1 A). now left.
Qed.
End Completeness_LEM.
Print Assumptions Completeness_LEM.