FObiint.FO_BiInt_Down_Lindenbaum_lem
Require Import FunctionalExtensionality.
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import Arith.
Require Import existsT.
Require Import FO_BiInt_Syntax.
Require Import FO_BiInt_GHC.
Require Import FO_BiInt_logic.
Require Import FOBIH_properties.
Require Import FO_BiInt_Stand_Lindenbaum_lem.
Require Import FO_BiInt_Kripke_sem.
Section DownLind.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Variable eq_dec_preds : forall x y : preds, {x = y}+{x <> y}.
Variable eq_dec_funcs : forall x y : Σ_funcs, {x = y}+{x <> y}.
(* Delete the following once we have the enumeration of formulas. *)
Variable form_enum : nat -> form.
Variable form_enum_sur : forall A, exists n, form_enum n = A.
Variable form_enum_unused : forall n, forall A m, form_enum m = A -> m <= n -> unused n A.
Variable form_index : form -> nat.
Variable form_enum_index : forall A, form_enum (form_index A) = A.
Variable form_index_inj : forall A B, form_index A = form_index B -> A = B.
Variable SLEM : forall P : Prop, P + ~ P.
Corollary LEM : forall P : Prop, P \/ ~ P.
Proof.
intro P ; destruct (SLEM P) ; auto.
Qed.
Notation "x 'el' L" := (List.In x L) (at level 70).
Notation "T |- phi" := (FOBIH_prv T phi) (at level 80).
Notation adj T phi := (fun psi => T psi \/ psi = phi).
Section DownLind_constr.
Variable w : form -> Prop .
Variable wex_henk : ex_henk w.
Lemma list_disj_subst_form l σ : (list_disj l)[σ] = list_disj (map (subst_form σ) l).
Proof.
induction l ; cbn ; auto.
apply f_equal ; auto.
Qed.
Lemma Ldext_ex {L1 L2 psi} :
~ pair_der (Singleton _ (((∃ psi) ∧ list_conj L1) --< list_disj L2)) (Complement _ w)
-> { c | w ((psi[$c..] ∧ list_conj L1) --< list_disj L2) }.
Proof.
intros HD.
assert (w (∃ (psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑]))).
- destruct (LEM (w (∃ psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑]))) ; auto.
exfalso. apply HD. apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
eapply dual_MP.
+ exists [] ; repeat split ; auto.
* apply NoDup_nil.
* intros B HB ; inversion HB.
* cbn. apply Dual_Constant_Domain.
+ assert (pair_der (Singleton form (∃ psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑])) (Complement form w)).
{ exists [(∃ psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑])]. repeat split ; auto.
- apply NoDup_cons. intro H0 ; inversion H0. apply NoDup_nil.
- intros C HC ; inversion HC ; subst ; auto. inversion H0.
- cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id ; apply In_singleton. }
destruct H0 as (l & Hl0 & Hl1 & Hl2). exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) (list_disj L2 :: l)).
repeat split ; auto.
* apply NoDup_nodup.
* intros C HC. apply nodup_In in HC. inversion HC ; subst. left ; split. right ; apply Hl1 ; auto.
* apply list_disj_nodup. cbn. eapply FOBIH_subst in Hl2. Unshelve. 4: exact ↑. all: auto.
apply FOBIH_monot with (Γ1:= Singleton _ ((∃ psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑])[↑])) in Hl2.
-- cbn in Hl2.
assert (Singleton form ((psi[up ↑] ∧ (list_conj L1)[↑][up ↑] --< (list_disj L2)[↑][up ↑])[$0..]) |- (list_disj l)[↑]).
{ apply MP with (∃ psi[up ↑] ∧ (list_conj L1)[↑][up ↑] --< (list_disj L2)[↑][up ↑]).
- apply FOBIH_Deduction_Theorem. apply (FOBIH_monot _ _ Hl2).
intros C HC. right ; auto.
- eapply MP. 2: apply Id ; apply In_singleton. apply Ax ; eapply QA3 ; reflexivity. }
cbn in H0. rewrite !form_subst_help in H0.
apply FOBIH_monot with (Γ:= Union _ (Empty_set _) (Singleton form (∃ psi ∧ (list_conj L1)[↑]))).
++ apply FOBIH_Detachment_Theorem. apply EC ; cbn.
apply FOBIH_Deduction_Theorem. apply FOBIH_monot with (Γ:= Singleton form (psi ∧ (list_conj L1)[↑])).
** rewrite (list_disj_subst_form l). apply FOBIH_Dual_Detachment_Theorem. rewrite <- list_disj_subst_form. auto.
** intros C HC ; inversion HC ; subst. right ; split.
++ intros C HC ; inversion HC ; subst ; auto. inversion H1.
-- intros C HC ; destruct HC as (B & HB0 & HB1) ; subst. inversion HB1 ; subst. split.
- apply wex_henk in H as [c Hc]. cbn in Hc. rewrite !subst_shift in Hc. exists c. apply Hc.
Qed.
Lemma Ldext_all {L1 L2 psi} :
~ pair_der (Singleton _ ((list_conj L1 --< ∀ psi) --< list_disj L2)) (Complement _ w)
-> { c | w ((list_conj L1 --< psi[$c..]) --< list_disj L2) }.
Proof.
intros HD.
assert (w (∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑])).
- destruct (LEM (w (∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑]))) ; auto.
exfalso. apply HD.
assert (pair_der (Singleton form (∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑])) (Complement form w)).
{ exists [(∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑])]. repeat split ; auto.
+ apply NoDup_cons. intro H0 ; inversion H0. apply NoDup_nil.
+ intros C HC ; inversion HC ; subst ; auto. inversion H0.
+ cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id ; apply In_singleton. }
destruct H0 as (l & Hl0 & Hl1 & Hl2). exists l.
repeat split ; auto.
+ apply FOBIH_Dual_Deduction_Theorem. eapply MP.
* eapply MP.
-- eapply MP.
++ apply Imp_trans.
++ apply imp_Id_gen.
-- apply list_disj_app. eapply MP.
++ apply Thm_irrel.
++ apply FOBIH_Dual_Deduction_Theorem. eapply MP.
** apply FOBIH_monot with (Γ:=Empty_set _).
--- apply Constant_Domain_Ax.
--- intros C HC ; inversion HC.
** apply prv_AI. eapply FOBIH_subst in Hl2. Unshelve. 3: exact ↑. 2: exact ⊤.
apply FOBIH_monot with (Γ1:= Singleton _ ((∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑])[↑])) in Hl2.
--- cbn in Hl2.
assert (Singleton form ((((list_conj L1)[↑][up ↑] --< psi[up ↑]) --< (list_disj L2)[↑][up ↑])[$0..]) |- (list_disj l)[↑]).
{ apply MP with (∃ ((list_conj L1)[↑][up ↑] --< psi[up ↑]) --< (list_disj L2)[↑][up ↑]).
- apply FOBIH_Deduction_Theorem. apply (FOBIH_monot _ _ Hl2).
intros C HC. right ; auto.
- eapply MP.
* apply Ax ; eapply QA3 ; reflexivity.
* apply Id ; apply In_singleton. }
cbn in H0. rewrite !form_subst_help in H0.
rewrite list_disj_subst_form.
apply FOBIH_monot with (Γ:= (Singleton form (list_conj L1)[↑])).
*** apply FOBIH_Dual_Detachment_Theorem. rewrite map_app. apply list_disj_app_distr.
rewrite <- list_disj_subst_form. apply FOBIH_Dual_Detachment_Theorem. rewrite <- list_disj_subst_form ; auto.
*** intros C HC ; inversion HC ; subst. exists (list_conj L1) ; repeat split ; auto.
--- intros C HC ; destruct HC as (B & HB0 & HB1) ; inversion HB1 ; subst ; split.
* apply prv_Top.
- apply wex_henk in H as [c Hc]. cbn in Hc. rewrite !subst_shift in Hc. exists c. apply Hc.
Qed.
Variable wall_henk : all_henk w.
Variable wconsist : consist w.
Variable wprime : prime w.
Variable wded_clos : ded_clos w.
Variable A0 B0 : form.
Hypothesis w_nder : ~ (pair_der (Singleton _ A0) (fun x => (Complement _ w) x \/ x = B0)).
Fixpoint Ldext (n : nat) : list form * list form :=
match n with
| 0 => ([A0], [B0])
| S n => let (L1, L2) := Ldext n in let phi := form_enum n in
match form_all phi, form_ex phi with
| inl (exist _ psi _), _ => match SLEM (pair_der (Singleton _ ((list_conj L1 --< ∀ psi) --< list_disj L2)) (Complement _ w)) with
| inl _ => (∀ psi :: L1, L2)
| inr H => (L1, ∀ psi :: psi[$(proj1_sig (Ldext_all H))..] :: L2)
end
| _, inl (exist _ psi _) => match SLEM (pair_der (Singleton _ (((∃ psi) ∧ list_conj L1) --< list_disj L2)) (Complement _ w)) with
| inl _ => (L1, ∃ psi :: L2)
| inr H => (∃ psi :: psi[$(proj1_sig (Ldext_ex H))..] :: L1, L2)
end
| _, _ => if SLEM (pair_der (Singleton _ ((list_conj (phi :: L1)) --< list_disj L2)) (Complement _ w))
then (L1, phi :: L2) else (phi :: L1, L2)
end
end.
Lemma Ldext_cum1 n n' :
n <= n' -> incl (fst (Ldext n)) (fst (Ldext n')).
Proof.
induction 1. firstorder. intros phi HP. cbn. destruct (Ldext m) eqn: HL.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM.
all: cbn ; auto.
Qed.
Lemma Ldext_cum2 n n' :
n <= n' -> incl (snd (Ldext n)) (snd (Ldext n')).
Proof.
induction 1. firstorder. intros phi HP. cbn. destruct (Ldext m) eqn: HL.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM.
all: cbn ; auto.
Qed.
Lemma Ldext_nder n :
~ (pair_der (Singleton _ (list_conj (fst (Ldext n)) --< list_disj (snd (Ldext n)))) (Complement _ w)).
Proof.
induction n; intros HD.
- cbn in HD. apply w_nder.
assert (adj (Complement form w) B0 = Union _ (Singleton _ B0) (Complement _ w)).
apply Extensionality_Ensembles ; split ; intros A HA ; unfold In in *. destruct HA ; subst.
right ; auto. left ; split. inversion HA ; subst ; auto. inversion H ; subst ; auto.
rewrite H ; clear H. apply (@gen_FOBIH_Dual_Detachment_Theorem) ; auto.
destruct HD as (l & Hl0 & Hl1 & Hl2). exists l ; repeat split ; auto.
apply (FOBIH_comp _ _ Hl2). intros B HB ; inversion HB ; subst.
apply FOBIH_monot with (Γ:= Union _ (Empty_set _) (Singleton form (A0 --< B0))).
apply FOBIH_Detachment_Theorem. eapply MP. eapply MP. apply Imp_trans.
apply monoL_Excl. eapply MP. eapply MP. apply Ax ; eapply A5 ; reflexivity.
apply imp_Id_gen. apply EFQ. apply monoR_Excl.
eapply MP. eapply MP. apply Ax ; eapply A8 ; reflexivity. apply imp_Id_gen.
apply FOBIH_Deduction_Theorem. apply prv_Top.
intros C HC ; inversion HC ; subst ; auto. inversion H.
- cbn in *. destruct Ldext, form_all as [[]|]; try destruct form_ex as [[]|] ;
destruct SLEM; try destruct Ldext_all; try destruct Ldext_ex; subst; cbn in *.
+ apply IHn. apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in p ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in p ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in HD ; auto.
apply (@Cut) with (∀ x) ; auto.
destruct HD as (l' & Hl'0 & Hl'1 & Hl'2). exists l' ; repeat split ; auto.
apply (FOBIH_comp _ _ Hl'2) ; auto. intros. inversion H ; subst. apply prv_CI ; apply Id.
right ; split. left ; split.
destruct p as (l' & Hl'0 & Hl'1 & Hl'2). exists l' ; repeat split ; auto.
intros. apply Hl'1 in H. inversion H ; subst. inversion H0 ; subst. right ; split.
inversion H0 ; subst. left ; auto. left ; right ; auto.
+ destruct HD as (l' & Hl'0 & Hl'1 & Hl'2).
assert (w (list_disj l')). apply wded_clos. eapply MP. eapply MP. eapply MP. apply Imp_trans.
apply FOBIH_monot with (Γ:= Empty_set _). apply monoR_Excl. apply monoL_Excl.
eapply MP. eapply MP. apply Ax ; eapply A5 ; reflexivity.
apply Ax ; eapply QA2 ; reflexivity. apply imp_Id_gen. intros C HC ; inversion HC.
2: apply Id ; exact w0.
apply FOBIH_monot with (Γ:= Empty_set _). apply FOBIH_Deduction_Theorem.
apply FOBIH_monot with (Γ:=Singleton form ((list_conj l --< (∀ x) ∨ x[$x0..]) --< list_disj l0)).
apply FOBIH_Dual_Deduction_Theorem.
apply FOBIH_monot with (Γ:=Union _ (Empty_set _) (Singleton form ((list_conj l --< (∀ x) ∨ x[$x0..])))).
apply FOBIH_Detachment_Theorem. apply list_disj_app. apply FOBIH_Deduction_Theorem.
apply FOBIH_monot with (Γ:=Singleton form ((list_conj l --< (∀ x) ∨ x[$x0..]))). apply FOBIH_Dual_Deduction_Theorem.
apply FOBIH_Dual_Detachment_Theorem in Hl'2.
apply (prv_DE _ _ _ _ Hl'2). apply (prv_DE _ (∀ x) (x[$x0..] ∨ list_disj l0)). apply Id ; right ; split.
apply prv_DI1. apply prv_DI1. apply Id ; unfold In ; auto. apply (prv_DE _ x[$x0..] (list_disj l0)). apply Id ; right ; split.
apply prv_DI1. apply prv_DI2 ; apply Id ; unfold In ; auto. apply prv_DI2. apply list_disj_app_distr.
apply prv_DI1. apply Id ; unfold In ; auto. apply prv_DI2. apply list_disj_app_distr. apply prv_DI2. apply Id ; unfold In ; auto.
intros C HC ; inversion HC ; subst ; right ; auto. intros C HC ; inversion HC ; subst ; auto. inversion H.
intros C HC ; inversion HC ; subst ; right ; auto. intros C HC ; inversion HC.
apply list_disj_prime in H ; auto. destruct H as (B & HB0 & HB1). apply Hl'1 in HB0 ; auto.
+ apply IHn. apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in p ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in HD ; auto.
apply (@Cut) with (∃ x) ; auto.
destruct p as (l' & Hl'0 & Hl'1 & Hl'2). exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) (list_disj l0 :: l')) ; repeat split ; auto.
apply NoDup_nodup. intros. apply nodup_In in H. inversion H ; subst. left ; split. apply Hl'1 in H0 ; auto.
apply list_disj_nodup. cbn. apply prv_DI2. apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs _ _ _ Hl'2). intros C HC ; inversion HC ; subst.
apply prv_CI ; apply Id. right ; split. left ; split.
apply (@Cut) with ((∃ x) ∨ list_disj l0) ; auto.
exists [(∃ x) ; list_disj l0]. repeat split. apply NoDup_cons. intro. inversion H ; subst. destruct l0 ; cbn in H0 ; inversion H0.
inversion H0. apply NoDup_cons. intro. inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. right ; split. inversion H ; subst. left ; left ; split. inversion H0.
cbn. eapply MP. apply Or_imp_assoc. apply Ax ; eapply A3 ; reflexivity. apply Id ; right ; split.
destruct HD as (l' & Hl'0 & Hl'1 & Hl'2). exists l'. repeat split ; auto. intros A HA ; apply Hl'1 in HA ; inversion HA ; subst.
inversion H ; subst. right ; split. left ; left ; right ; auto.
+ destruct HD as (l' & Hl'0 & Hl'1 & Hl'2).
assert (w (list_disj l')). apply wded_clos. eapply MP. eapply MP. eapply MP. apply Imp_trans.
apply FOBIH_monot with (Γ:= Empty_set _). apply monoR_Excl. 4: apply Id ; exact w0.
apply FOBIH_Deduction_Theorem. apply prv_CI. eapply MP. apply Ax ; eapply QA3 ; reflexivity.
apply prv_CE1 with (list_conj l). apply Id ; right ; split. apply prv_CI. apply prv_CE1 with (list_conj l).
apply Id ; right ; split. apply prv_CE2 with (x[$x0..]). apply Id ; right ; split. intros A HA ; inversion HA.
apply FOBIH_Deduction_Theorem. apply (FOBIH_monot _ _ Hl'2). intros A HA ; inversion HA ; subst ; right ; split.
apply list_disj_prime in H ; auto. destruct H as (B & HB0 & HB1). apply Hl'1 in HB0 ; auto.
+ apply IHn. apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in p ; auto.
assert (pair_der (Union _ (Singleton _ (list_conj l)) (Singleton _ (form_enum n))) (Union _ (Singleton form (list_disj l0)) (Complement _ w))).
destruct p as (l' & Hl'0 & Hl'1 & Hl'2). exists l' ; repeat split ; auto. apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs _ _ _ Hl'2).
intros C HC ; inversion HC ; subst. apply prv_CI. apply Id ; right ; split. apply Id ; left ; split.
assert (pair_der (Singleton _ (list_conj l)) (Union _ (Union _ (Singleton _ (list_disj l0)) (Complement _ w)) (Singleton _ (form_enum n)))).
destruct HD as (l' & Hl'0 & Hl'1 & Hl'2). exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) ((form_enum n) :: (list_disj l0) :: l')) ; repeat split ; auto.
apply NoDup_nodup. intros A HA ; apply nodup_In in HA ; inversion HA ; subst. right ; split.
inversion H0 ; subst. left ; left ; split. left ; right ; apply Hl'1 ; auto. apply list_disj_nodup.
cbn. apply FOBIH_Dual_Detachment_Theorem in Hl'2. apply prv_DE with (form_enum n ∨ list_disj l0) (list_disj l') ; auto.
apply prv_DE with (form_enum n) (list_disj l0). apply Id ; unfold In ; auto. apply prv_DI1. apply Id ; unfold In ; auto.
apply prv_DI2 ; apply prv_DI1 ; apply Id ; unfold In ; auto. apply prv_DI2 ; apply prv_DI2 ; apply Id ; unfold In ; auto.
apply (@Cut) with (form_enum n) ; auto.
+ auto.
Qed.
Lemma Ldext_A0 n :
A0 el fst (Ldext n).
Proof.
induction n; cbn; try tauto.
destruct (Ldext n) as [L1 L2]. cbn in IHn.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM; cbn; tauto.
Qed.
Lemma Ldext_B0 n :
B0 el snd (Ldext n).
Proof.
induction n; cbn; try tauto.
destruct (Ldext n) as [L1 L2]. cbn in IHn.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM; cbn; tauto.
Qed.
Definition dext phi := exists n, phi el fst (Ldext n).
Lemma dext_der n :
dext |- list_conj (fst (Ldext n)).
Proof.
apply prv_list_conj. intros A HA. apply prv_ctx. now exists n.
Qed.
Lemma dext_prv phi :
dext |- phi -> exists n, (fun psi => psi el fst (Ldext n)) |- phi.
Proof.
intros [L[H1 H2]] % (@prv_compact _ _ eq_dec_preds eq_dec_funcs). revert phi H2.
induction L as [|psi L IH]; intros phi H2.
- exists 0. cbn. eapply prv_weak; try apply H2. intros B [].
- destruct (H1 psi) as [k Hk]; try now left.
destruct IH with (psi --> phi) as [n Hn].
* intros B HB. apply H1. now right.
* apply prv_DT. eapply prv_weak; try apply H2. unfold Included, In. cbn. intuition.
* exists (n + k). apply prv_DT in Hn. eapply prv_weak; try apply Hn.
intros B [| ->] ; eapply Ldext_cum1; try eassumption; lia.
Qed.
Lemma Ldext_mono T n n' :
n <= n' -> T |- list_disj (snd (Ldext n)) -> T |- list_disj (snd (Ldext n')).
Proof.
intros H. apply list_disj_mono. now apply Ldext_cum2.
Qed.
Lemma list_disj_weak : forall (T : form -> Prop) (L L' : list form),
(forall A, A el L -> T |- A --> list_disj L') -> T |- list_disj L -> T |- list_disj L'.
Proof.
intros T L. revert T. induction L ; cbn ; auto.
- intros. eapply MP. apply EFQ. auto.
- intros. eapply MP. eapply MP. eapply MP. apply Ax ; eapply A5 ; reflexivity.
3: exact H0. apply H ; auto. apply FOBIH_Deduction_Theorem. apply IHL.
intros. apply FOBIH_monot with T. apply H ; auto. intros C HC ; left ; auto.
apply Id ; right ; split.
Qed.
Lemma dext_nder n :
~ (pair_der dext (Union _ (Singleton _ (list_disj (snd (Ldext n)))) (Complement _ w))).
Proof.
intros (l & Hl0 & Hl1 & Hl2). destruct (dext_prv _ Hl2) as (k & Hk).
apply (Ldext_nder (max n k)). apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) ((list_disj (snd (Ldext (Init.Nat.max n k)))) :: remove (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) (list_disj (snd (Ldext n))) l)).
repeat split ; auto. apply NoDup_nodup. intros A HA ; apply nodup_In in HA. inversion HA ; subst. left ; split.
right. apply in_remove in H. destruct H. apply Hl1 in H. inversion H ; subst. exfalso ; inversion H1 ; subst ; auto. auto.
apply list_disj_nodup. apply list_disj_weak with l.
intros A HA. destruct ((@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) A (list_disj (snd (Ldext n)))) ; subst. apply FOBIH_Deduction_Theorem.
eapply MP. apply Ax ; eapply A3 ; reflexivity. apply list_disj_mono with (snd (Ldext n)).
apply Ldext_cum2. lia. apply Id ; right ; split. pose (Hl1 _ HA).
inversion u ; subst. inversion H ; subst. exfalso ; auto. cbn. eapply MP. eapply MP. apply Imp_trans.
2: apply Ax ; eapply A4 ; reflexivity. apply FOBIH_Deduction_Theorem. apply prv_list_disj with A.
apply in_in_remove ; auto. apply Id ; right ; split. apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs _ _ _ Hk). intros B HB.
eapply MP. apply list_conj_in_list. apply (Ldext_cum1 k (max n k)) ; auto. lia. apply Id ; split.
Qed.
Lemma dext_el phi :
dext phi -> w phi.
Proof.
intro H ; subst ; auto. destruct H.
destruct (LEM (w phi)) ; auto. exfalso. eapply (dext_nder (S x)) ; auto.
exists [phi]. repeat split.
- apply NoDup_cons. intro H2 ; inversion H2. apply NoDup_nil.
- intros D HD ; inversion HD ; subst. right ; auto. inversion H1.
- cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id. exists x ; exact H.
Qed.
Lemma dext_ex_henk :
ex_henk dext.
Proof.
intros phi H. remember (form_index (∃ phi)) as n.
destruct (Ldext n) as [L1 L2] eqn: HL.
destruct (SLEM (pair_der (Singleton _ (((∃ phi) ∧ list_conj L1) --< list_disj L2)) (Complement _ w))) eqn: HS.
{ exfalso. destruct H. assert (J: pair_der (Singleton form ((∃ phi) ∧ list_conj L1 --< list_disj L2)) (Complement form w)) ; auto.
destruct J as (l & Hl0 & Hl1 & Hl2). apply FOBIH_Dual_Detachment_Theorem in Hl2.
apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs) with (T':=Union _ (Singleton form (∃ phi)) (Singleton form (list_conj L1))) in Hl2.
apply (Ldext_nder (max (S n) x)). apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) ((list_disj (snd (Ldext (Init.Nat.max (S n) x)))) :: l)).
repeat split ; auto. apply NoDup_nodup. intros A HA ; apply nodup_In in HA. inversion HA ; subst. left ; split.
right ; apply Hl1 ; auto. apply list_disj_nodup. remember (Ldext (Init.Nat.max (S n) x)) as X. cbn.
apply prv_DE with (list_disj L2) (list_disj l). apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs _ _ _ Hl2).
intros A HA ; inversion HA ; subst. inversion H0 ; subst. eapply MP. eapply list_conj_in_list with (l:=(fst (Ldext (Init.Nat.max (S (form_index (∃ phi))) x)))).
apply Ldext_cum1 with x ; auto ; lia. apply Id ; split. inversion H0 ; subst.
apply prv_list_conj. intros B HB. eapply MP. eapply list_conj_in_list with (l:=(fst (Ldext (Init.Nat.max (S (form_index (∃ phi))) x)))).
apply Ldext_cum1 with (form_index (∃ phi)). lia. rewrite HL ; cbn ; auto. apply Id ; split. subst ; apply prv_DI1.
apply list_disj_mono with L2. assert (L2 = snd (Ldext (form_index (∃ phi)))). rewrite HL ; auto. rewrite H0. apply Ldext_cum2 ; lia.
apply Id ; right ; split. apply prv_DI2. apply Id ; right ; split.
intros B HB ; inversion HB ; subst. apply prv_CI. apply Id ; left ; split. apply Id ; right ; split. }
exists (proj1_sig (Ldext_ex n0)). exists (S n). cbn.
rewrite HL.
destruct form_all as [[]|]. rewrite Heqn in e. rewrite form_enum_index in e ; try discriminate.
destruct form_ex as [[]|].
- rewrite Heqn in e ; rewrite form_enum_index in e ; injection e. intros <-. rewrite HS. right. left. reflexivity.
- contradict n2. exists phi. rewrite Heqn. apply form_enum_index.
Qed.
Lemma dext_all_henk :
all_henk dext.
Proof.
intros phi HP. remember (form_index (∀ phi)) as n.
destruct (Ldext n) as [L1 L2] eqn: HL.
destruct (SLEM (pair_der (Singleton _ ((list_conj L1 --< ∀ phi) --< list_disj L2)) (Complement _ w))) eqn: HS.
- exfalso. apply HP. exists (S n). cbn. rewrite HL. rewrite Heqn ; cbn. rewrite form_enum_index ; cbn.
destruct form_all as [[]|].
+ injection e as ->. rewrite HS. now left.
+ contradict n0. now exists phi.
- exists (proj1_sig (Ldext_all n0)). intro. destruct H as (c & Hc).
apply (Ldext_nder (max (S n) c)). apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
exists [(list_disj (snd (Ldext (Init.Nat.max (S n) c))))].
repeat split ; auto. apply NoDup_cons. intro H ; inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H.
remember (Ldext (Init.Nat.max (S n) c)) as X. cbn.
eapply MP. apply Ax ; eapply A3 ; reflexivity. eapply MP. apply list_disj_In0. Unshelve. 3: exact phi[$(proj1_sig (Ldext_all n0))..]. subst.
pose (Ldext_cum2 (S (form_index (∀ phi)))). apply i. lia. cbn. rewrite HL. rewrite form_enum_index.
destruct form_all as [[]|]. inversion e ; subst. rewrite HS ; cbn. auto.
exfalso ; apply n ; exists phi ; auto. subst. eapply MP. apply list_conj_in_list.
pose (Ldext_cum1 c (max (S (form_index (∀ phi))) c)). apply i ; auto. lia. apply Id ; split.
Qed.
Lemma dext_ded_clos :
ded_clos dext.
Proof.
intros phi HP. destruct (form_enum_sur phi) as [n <-].
exists (S n). cbn. destruct Ldext eqn: HL.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM eqn:EqD; cbn in * ; auto.
- exfalso. rewrite e in HP. apply dext_nder with (S n).
exists [(list_disj (snd (Ldext (S n))))]. repeat split. apply NoDup_cons. intro H ; inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H.
remember (snd (Ldext (S n))) as X. cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. subst.
apply prv_list_disj with (∀ x) ; auto. cbn. rewrite HL ; cbn. destruct form_all as [[]|].
rewrite e in e0. inversion e0 ; subst. rewrite EqD ; cbn. auto. exfalso. apply n1. exists x ; firstorder.
- exfalso. rewrite e in HP. apply dext_nder with (S n).
exists [(list_disj (snd (Ldext (S n))))]. repeat split. apply NoDup_cons. intro H ; inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H.
remember (snd (Ldext (S n))) as X. cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. subst.
apply prv_list_disj with (∃ x) ; auto. cbn. rewrite HL ; cbn. destruct form_all as [[]|]. rewrite e0 in e. inversion e.
destruct form_ex as [[]|]. rewrite e0 in e. inversion e ; subst. rewrite EqD ; cbn. auto.
exfalso. apply n2. exists x ; firstorder.
- exfalso. apply dext_nder with (S n).
exists [(list_disj (snd (Ldext (S n))))]. repeat split. apply NoDup_cons. intro H ; inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H.
remember (snd (Ldext (S n))) as X. cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. subst.
apply prv_list_disj with (form_enum n) ; auto. cbn. rewrite HL ; cbn. destruct form_all as [[]|]. exfalso ; apply n0 ; exists x ; auto.
destruct form_ex as [[]|]. exfalso ; apply n1 ; exists x ; auto. rewrite EqD ; cbn. auto.
Qed.
Lemma dext_A0 :
dext A0.
Proof.
exists 0 ; cbn ; auto.
Qed.
Lemma dext_B0 :
~ dext B0.
Proof.
intros H. apply (dext_nder 0). exists [(list_disj (snd (Ldext 0)))].
repeat split. apply NoDup_cons. intro H0 ; inversion H0. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H0.
cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id ; auto.
Qed.
Lemma dext_consist :
consist dext.
Proof.
intros H. apply dext_B0. apply dext_ded_clos.
apply prv_MP with ⊥; trivial. apply EFQ.
Qed.
Lemma dext_prime :
prime dext.
Proof.
intros phi psi HD.
destruct (SLEM (dext phi)), (SLEM (dext psi)); try tauto.
remember (form_index phi) as m.
remember (form_index psi) as k.
exfalso.
assert (phi el (snd (Ldext (S m)))).
{ cbn. destruct Ldext eqn: HL. destruct (form_all (form_enum m)) eqn: EqAll. destruct s. subst.
destruct (SLEM (pair_der (Singleton form ((list_conj l --< (∀ x)) --< list_disj l0)) (Complement form w))) eqn: EqD.
exfalso. apply n. exists (S (form_index phi)). cbn. rewrite HL. rewrite EqAll. rewrite EqD. rewrite <- e.
rewrite form_enum_index. cbn ; auto. cbn. rewrite <- e ; rewrite form_enum_index ; auto.
destruct (form_ex (form_enum m)) eqn: EqEx. destruct s. subst.
destruct (SLEM (pair_der (Singleton form ((∃ x) ∧ list_conj l --< list_disj l0)) (Complement form w))) eqn: EqD.
rewrite <- e ; rewrite form_enum_index ; cbn ; auto.
exfalso. apply n. exists (S (form_index phi)). cbn. rewrite HL. rewrite EqAll. rewrite EqEx. rewrite EqD. rewrite <- e.
rewrite form_enum_index. cbn ; auto.
destruct (SLEM (pair_der (Singleton form (form_enum m ∧ list_conj l --< list_disj l0)) (Complement form w))) eqn: EqD.
rewrite Heqm ; rewrite form_enum_index ; cbn ; auto.
exfalso. apply n. exists (S (form_index phi)). cbn. rewrite <- Heqm. rewrite HL. rewrite EqAll. rewrite EqEx.
rewrite EqD. rewrite Heqm. rewrite form_enum_index. cbn ; auto. }
assert (psi el (snd (Ldext (S k)))).
{ cbn. destruct (Ldext k) eqn: HL. destruct (form_all (form_enum k)) eqn: EqAll. destruct s. subst.
destruct (SLEM (pair_der (Singleton form ((list_conj l --< (∀ x)) --< list_disj l0)) (Complement form w))) eqn: EqD.
exfalso. apply n0. exists (S (form_index psi)). cbn. rewrite HL. rewrite EqAll. rewrite EqD. rewrite <- e.
rewrite form_enum_index. cbn ; auto. cbn. rewrite <- e ; rewrite form_enum_index ; auto.
destruct (form_ex (form_enum k)) eqn: EqEx. destruct s. subst.
destruct (SLEM (pair_der (Singleton form ((∃ x) ∧ list_conj l --< list_disj l0)) (Complement form w))) eqn: EqD.
rewrite <- e ; rewrite form_enum_index ; cbn ; auto.
exfalso. apply n0. exists (S (form_index psi)). cbn. rewrite HL. rewrite EqAll. rewrite EqEx. rewrite EqD. rewrite <- e.
rewrite form_enum_index. cbn ; auto.
destruct (SLEM (pair_der (Singleton form (form_enum k ∧ list_conj l --< list_disj l0)) (Complement form w))) eqn: EqD.
rewrite Heqk ; rewrite form_enum_index ; cbn ; auto.
exfalso. apply n0. exists (S (form_index psi)). cbn. rewrite <- Heqk. rewrite HL. rewrite EqAll. rewrite EqEx.
rewrite EqD. rewrite Heqk. rewrite form_enum_index. cbn ; auto. }
apply dext_nder with (max (S m) (S k)).
exists [(list_disj (snd (Ldext (Init.Nat.max (S m) (S k)))))]. repeat split.
- apply NoDup_cons. intro H1 ; inversion H1. apply NoDup_nil.
- intros A HA ; inversion HA ; subst.
+ left ; split.
+ inversion H1.
- eapply MP. apply Ax ; eapply A3 ; reflexivity.
apply list_disj_mono with [phi;psi].
+ intros C HC. inversion HC ; subst.
* eapply (Ldext_cum2 _ _ _ _ H).
* inversion H1 ; subst.
-- eapply (Ldext_cum2 _ _ _ _ H0).
-- inversion H2.
+ cbn. eapply MP.
* apply Or_imp_assoc. apply Ax ; eapply A3 ; reflexivity.
* apply Id ; auto.
Unshelve. all: lia.
Qed.
End DownLind_constr.
Open Scope type.
Lemma Down_Lindenbaum_lemma : forall w A B,
consist w -> prime w -> ded_clos w ->
ex_henk w -> all_henk w ->
~ (pair_der (Singleton _ A) (adj (Complement form w) B)) ->
existsT2 w', consist w' *
prime w' *
ded_clos w' *
ex_henk w' *
all_henk w' *
(w' A) *
(~ (w' B)) *
(forall C, w' C -> w C).
Proof.
intros w A B cons prim dedclos exh allh H.
exists (dext w exh A B) ; auto. cbn ; repeat split ; auto.
- apply dext_consist ; auto.
- apply dext_prime ; auto.
- apply dext_ded_clos ; auto.
- apply dext_ex_henk ; auto.
- apply dext_all_henk ; auto.
- apply dext_A0.
- apply dext_B0 ; auto.
- apply dext_el ; auto.
Qed.
End DownLind.
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import Arith.
Require Import existsT.
Require Import FO_BiInt_Syntax.
Require Import FO_BiInt_GHC.
Require Import FO_BiInt_logic.
Require Import FOBIH_properties.
Require Import FO_BiInt_Stand_Lindenbaum_lem.
Require Import FO_BiInt_Kripke_sem.
Section DownLind.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Variable eq_dec_preds : forall x y : preds, {x = y}+{x <> y}.
Variable eq_dec_funcs : forall x y : Σ_funcs, {x = y}+{x <> y}.
(* Delete the following once we have the enumeration of formulas. *)
Variable form_enum : nat -> form.
Variable form_enum_sur : forall A, exists n, form_enum n = A.
Variable form_enum_unused : forall n, forall A m, form_enum m = A -> m <= n -> unused n A.
Variable form_index : form -> nat.
Variable form_enum_index : forall A, form_enum (form_index A) = A.
Variable form_index_inj : forall A B, form_index A = form_index B -> A = B.
Variable SLEM : forall P : Prop, P + ~ P.
Corollary LEM : forall P : Prop, P \/ ~ P.
Proof.
intro P ; destruct (SLEM P) ; auto.
Qed.
Notation "x 'el' L" := (List.In x L) (at level 70).
Notation "T |- phi" := (FOBIH_prv T phi) (at level 80).
Notation adj T phi := (fun psi => T psi \/ psi = phi).
Section DownLind_constr.
Variable w : form -> Prop .
Variable wex_henk : ex_henk w.
Lemma list_disj_subst_form l σ : (list_disj l)[σ] = list_disj (map (subst_form σ) l).
Proof.
induction l ; cbn ; auto.
apply f_equal ; auto.
Qed.
Lemma Ldext_ex {L1 L2 psi} :
~ pair_der (Singleton _ (((∃ psi) ∧ list_conj L1) --< list_disj L2)) (Complement _ w)
-> { c | w ((psi[$c..] ∧ list_conj L1) --< list_disj L2) }.
Proof.
intros HD.
assert (w (∃ (psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑]))).
- destruct (LEM (w (∃ psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑]))) ; auto.
exfalso. apply HD. apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
eapply dual_MP.
+ exists [] ; repeat split ; auto.
* apply NoDup_nil.
* intros B HB ; inversion HB.
* cbn. apply Dual_Constant_Domain.
+ assert (pair_der (Singleton form (∃ psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑])) (Complement form w)).
{ exists [(∃ psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑])]. repeat split ; auto.
- apply NoDup_cons. intro H0 ; inversion H0. apply NoDup_nil.
- intros C HC ; inversion HC ; subst ; auto. inversion H0.
- cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id ; apply In_singleton. }
destruct H0 as (l & Hl0 & Hl1 & Hl2). exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) (list_disj L2 :: l)).
repeat split ; auto.
* apply NoDup_nodup.
* intros C HC. apply nodup_In in HC. inversion HC ; subst. left ; split. right ; apply Hl1 ; auto.
* apply list_disj_nodup. cbn. eapply FOBIH_subst in Hl2. Unshelve. 4: exact ↑. all: auto.
apply FOBIH_monot with (Γ1:= Singleton _ ((∃ psi ∧ (list_conj L1)[↑] --< (list_disj L2)[↑])[↑])) in Hl2.
-- cbn in Hl2.
assert (Singleton form ((psi[up ↑] ∧ (list_conj L1)[↑][up ↑] --< (list_disj L2)[↑][up ↑])[$0..]) |- (list_disj l)[↑]).
{ apply MP with (∃ psi[up ↑] ∧ (list_conj L1)[↑][up ↑] --< (list_disj L2)[↑][up ↑]).
- apply FOBIH_Deduction_Theorem. apply (FOBIH_monot _ _ Hl2).
intros C HC. right ; auto.
- eapply MP. 2: apply Id ; apply In_singleton. apply Ax ; eapply QA3 ; reflexivity. }
cbn in H0. rewrite !form_subst_help in H0.
apply FOBIH_monot with (Γ:= Union _ (Empty_set _) (Singleton form (∃ psi ∧ (list_conj L1)[↑]))).
++ apply FOBIH_Detachment_Theorem. apply EC ; cbn.
apply FOBIH_Deduction_Theorem. apply FOBIH_monot with (Γ:= Singleton form (psi ∧ (list_conj L1)[↑])).
** rewrite (list_disj_subst_form l). apply FOBIH_Dual_Detachment_Theorem. rewrite <- list_disj_subst_form. auto.
** intros C HC ; inversion HC ; subst. right ; split.
++ intros C HC ; inversion HC ; subst ; auto. inversion H1.
-- intros C HC ; destruct HC as (B & HB0 & HB1) ; subst. inversion HB1 ; subst. split.
- apply wex_henk in H as [c Hc]. cbn in Hc. rewrite !subst_shift in Hc. exists c. apply Hc.
Qed.
Lemma Ldext_all {L1 L2 psi} :
~ pair_der (Singleton _ ((list_conj L1 --< ∀ psi) --< list_disj L2)) (Complement _ w)
-> { c | w ((list_conj L1 --< psi[$c..]) --< list_disj L2) }.
Proof.
intros HD.
assert (w (∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑])).
- destruct (LEM (w (∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑]))) ; auto.
exfalso. apply HD.
assert (pair_der (Singleton form (∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑])) (Complement form w)).
{ exists [(∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑])]. repeat split ; auto.
+ apply NoDup_cons. intro H0 ; inversion H0. apply NoDup_nil.
+ intros C HC ; inversion HC ; subst ; auto. inversion H0.
+ cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id ; apply In_singleton. }
destruct H0 as (l & Hl0 & Hl1 & Hl2). exists l.
repeat split ; auto.
+ apply FOBIH_Dual_Deduction_Theorem. eapply MP.
* eapply MP.
-- eapply MP.
++ apply Imp_trans.
++ apply imp_Id_gen.
-- apply list_disj_app. eapply MP.
++ apply Thm_irrel.
++ apply FOBIH_Dual_Deduction_Theorem. eapply MP.
** apply FOBIH_monot with (Γ:=Empty_set _).
--- apply Constant_Domain_Ax.
--- intros C HC ; inversion HC.
** apply prv_AI. eapply FOBIH_subst in Hl2. Unshelve. 3: exact ↑. 2: exact ⊤.
apply FOBIH_monot with (Γ1:= Singleton _ ((∃ ((list_conj L1)[↑] --< psi) --< (list_disj L2)[↑])[↑])) in Hl2.
--- cbn in Hl2.
assert (Singleton form ((((list_conj L1)[↑][up ↑] --< psi[up ↑]) --< (list_disj L2)[↑][up ↑])[$0..]) |- (list_disj l)[↑]).
{ apply MP with (∃ ((list_conj L1)[↑][up ↑] --< psi[up ↑]) --< (list_disj L2)[↑][up ↑]).
- apply FOBIH_Deduction_Theorem. apply (FOBIH_monot _ _ Hl2).
intros C HC. right ; auto.
- eapply MP.
* apply Ax ; eapply QA3 ; reflexivity.
* apply Id ; apply In_singleton. }
cbn in H0. rewrite !form_subst_help in H0.
rewrite list_disj_subst_form.
apply FOBIH_monot with (Γ:= (Singleton form (list_conj L1)[↑])).
*** apply FOBIH_Dual_Detachment_Theorem. rewrite map_app. apply list_disj_app_distr.
rewrite <- list_disj_subst_form. apply FOBIH_Dual_Detachment_Theorem. rewrite <- list_disj_subst_form ; auto.
*** intros C HC ; inversion HC ; subst. exists (list_conj L1) ; repeat split ; auto.
--- intros C HC ; destruct HC as (B & HB0 & HB1) ; inversion HB1 ; subst ; split.
* apply prv_Top.
- apply wex_henk in H as [c Hc]. cbn in Hc. rewrite !subst_shift in Hc. exists c. apply Hc.
Qed.
Variable wall_henk : all_henk w.
Variable wconsist : consist w.
Variable wprime : prime w.
Variable wded_clos : ded_clos w.
Variable A0 B0 : form.
Hypothesis w_nder : ~ (pair_der (Singleton _ A0) (fun x => (Complement _ w) x \/ x = B0)).
Fixpoint Ldext (n : nat) : list form * list form :=
match n with
| 0 => ([A0], [B0])
| S n => let (L1, L2) := Ldext n in let phi := form_enum n in
match form_all phi, form_ex phi with
| inl (exist _ psi _), _ => match SLEM (pair_der (Singleton _ ((list_conj L1 --< ∀ psi) --< list_disj L2)) (Complement _ w)) with
| inl _ => (∀ psi :: L1, L2)
| inr H => (L1, ∀ psi :: psi[$(proj1_sig (Ldext_all H))..] :: L2)
end
| _, inl (exist _ psi _) => match SLEM (pair_der (Singleton _ (((∃ psi) ∧ list_conj L1) --< list_disj L2)) (Complement _ w)) with
| inl _ => (L1, ∃ psi :: L2)
| inr H => (∃ psi :: psi[$(proj1_sig (Ldext_ex H))..] :: L1, L2)
end
| _, _ => if SLEM (pair_der (Singleton _ ((list_conj (phi :: L1)) --< list_disj L2)) (Complement _ w))
then (L1, phi :: L2) else (phi :: L1, L2)
end
end.
Lemma Ldext_cum1 n n' :
n <= n' -> incl (fst (Ldext n)) (fst (Ldext n')).
Proof.
induction 1. firstorder. intros phi HP. cbn. destruct (Ldext m) eqn: HL.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM.
all: cbn ; auto.
Qed.
Lemma Ldext_cum2 n n' :
n <= n' -> incl (snd (Ldext n)) (snd (Ldext n')).
Proof.
induction 1. firstorder. intros phi HP. cbn. destruct (Ldext m) eqn: HL.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM.
all: cbn ; auto.
Qed.
Lemma Ldext_nder n :
~ (pair_der (Singleton _ (list_conj (fst (Ldext n)) --< list_disj (snd (Ldext n)))) (Complement _ w)).
Proof.
induction n; intros HD.
- cbn in HD. apply w_nder.
assert (adj (Complement form w) B0 = Union _ (Singleton _ B0) (Complement _ w)).
apply Extensionality_Ensembles ; split ; intros A HA ; unfold In in *. destruct HA ; subst.
right ; auto. left ; split. inversion HA ; subst ; auto. inversion H ; subst ; auto.
rewrite H ; clear H. apply (@gen_FOBIH_Dual_Detachment_Theorem) ; auto.
destruct HD as (l & Hl0 & Hl1 & Hl2). exists l ; repeat split ; auto.
apply (FOBIH_comp _ _ Hl2). intros B HB ; inversion HB ; subst.
apply FOBIH_monot with (Γ:= Union _ (Empty_set _) (Singleton form (A0 --< B0))).
apply FOBIH_Detachment_Theorem. eapply MP. eapply MP. apply Imp_trans.
apply monoL_Excl. eapply MP. eapply MP. apply Ax ; eapply A5 ; reflexivity.
apply imp_Id_gen. apply EFQ. apply monoR_Excl.
eapply MP. eapply MP. apply Ax ; eapply A8 ; reflexivity. apply imp_Id_gen.
apply FOBIH_Deduction_Theorem. apply prv_Top.
intros C HC ; inversion HC ; subst ; auto. inversion H.
- cbn in *. destruct Ldext, form_all as [[]|]; try destruct form_ex as [[]|] ;
destruct SLEM; try destruct Ldext_all; try destruct Ldext_ex; subst; cbn in *.
+ apply IHn. apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in p ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in p ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in HD ; auto.
apply (@Cut) with (∀ x) ; auto.
destruct HD as (l' & Hl'0 & Hl'1 & Hl'2). exists l' ; repeat split ; auto.
apply (FOBIH_comp _ _ Hl'2) ; auto. intros. inversion H ; subst. apply prv_CI ; apply Id.
right ; split. left ; split.
destruct p as (l' & Hl'0 & Hl'1 & Hl'2). exists l' ; repeat split ; auto.
intros. apply Hl'1 in H. inversion H ; subst. inversion H0 ; subst. right ; split.
inversion H0 ; subst. left ; auto. left ; right ; auto.
+ destruct HD as (l' & Hl'0 & Hl'1 & Hl'2).
assert (w (list_disj l')). apply wded_clos. eapply MP. eapply MP. eapply MP. apply Imp_trans.
apply FOBIH_monot with (Γ:= Empty_set _). apply monoR_Excl. apply monoL_Excl.
eapply MP. eapply MP. apply Ax ; eapply A5 ; reflexivity.
apply Ax ; eapply QA2 ; reflexivity. apply imp_Id_gen. intros C HC ; inversion HC.
2: apply Id ; exact w0.
apply FOBIH_monot with (Γ:= Empty_set _). apply FOBIH_Deduction_Theorem.
apply FOBIH_monot with (Γ:=Singleton form ((list_conj l --< (∀ x) ∨ x[$x0..]) --< list_disj l0)).
apply FOBIH_Dual_Deduction_Theorem.
apply FOBIH_monot with (Γ:=Union _ (Empty_set _) (Singleton form ((list_conj l --< (∀ x) ∨ x[$x0..])))).
apply FOBIH_Detachment_Theorem. apply list_disj_app. apply FOBIH_Deduction_Theorem.
apply FOBIH_monot with (Γ:=Singleton form ((list_conj l --< (∀ x) ∨ x[$x0..]))). apply FOBIH_Dual_Deduction_Theorem.
apply FOBIH_Dual_Detachment_Theorem in Hl'2.
apply (prv_DE _ _ _ _ Hl'2). apply (prv_DE _ (∀ x) (x[$x0..] ∨ list_disj l0)). apply Id ; right ; split.
apply prv_DI1. apply prv_DI1. apply Id ; unfold In ; auto. apply (prv_DE _ x[$x0..] (list_disj l0)). apply Id ; right ; split.
apply prv_DI1. apply prv_DI2 ; apply Id ; unfold In ; auto. apply prv_DI2. apply list_disj_app_distr.
apply prv_DI1. apply Id ; unfold In ; auto. apply prv_DI2. apply list_disj_app_distr. apply prv_DI2. apply Id ; unfold In ; auto.
intros C HC ; inversion HC ; subst ; right ; auto. intros C HC ; inversion HC ; subst ; auto. inversion H.
intros C HC ; inversion HC ; subst ; right ; auto. intros C HC ; inversion HC.
apply list_disj_prime in H ; auto. destruct H as (B & HB0 & HB1). apply Hl'1 in HB0 ; auto.
+ apply IHn. apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in p ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in HD ; auto.
apply (@Cut) with (∃ x) ; auto.
destruct p as (l' & Hl'0 & Hl'1 & Hl'2). exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) (list_disj l0 :: l')) ; repeat split ; auto.
apply NoDup_nodup. intros. apply nodup_In in H. inversion H ; subst. left ; split. apply Hl'1 in H0 ; auto.
apply list_disj_nodup. cbn. apply prv_DI2. apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs _ _ _ Hl'2). intros C HC ; inversion HC ; subst.
apply prv_CI ; apply Id. right ; split. left ; split.
apply (@Cut) with ((∃ x) ∨ list_disj l0) ; auto.
exists [(∃ x) ; list_disj l0]. repeat split. apply NoDup_cons. intro. inversion H ; subst. destruct l0 ; cbn in H0 ; inversion H0.
inversion H0. apply NoDup_cons. intro. inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. right ; split. inversion H ; subst. left ; left ; split. inversion H0.
cbn. eapply MP. apply Or_imp_assoc. apply Ax ; eapply A3 ; reflexivity. apply Id ; right ; split.
destruct HD as (l' & Hl'0 & Hl'1 & Hl'2). exists l'. repeat split ; auto. intros A HA ; apply Hl'1 in HA ; inversion HA ; subst.
inversion H ; subst. right ; split. left ; left ; right ; auto.
+ destruct HD as (l' & Hl'0 & Hl'1 & Hl'2).
assert (w (list_disj l')). apply wded_clos. eapply MP. eapply MP. eapply MP. apply Imp_trans.
apply FOBIH_monot with (Γ:= Empty_set _). apply monoR_Excl. 4: apply Id ; exact w0.
apply FOBIH_Deduction_Theorem. apply prv_CI. eapply MP. apply Ax ; eapply QA3 ; reflexivity.
apply prv_CE1 with (list_conj l). apply Id ; right ; split. apply prv_CI. apply prv_CE1 with (list_conj l).
apply Id ; right ; split. apply prv_CE2 with (x[$x0..]). apply Id ; right ; split. intros A HA ; inversion HA.
apply FOBIH_Deduction_Theorem. apply (FOBIH_monot _ _ Hl'2). intros A HA ; inversion HA ; subst ; right ; split.
apply list_disj_prime in H ; auto. destruct H as (B & HB0 & HB1). apply Hl'1 in HB0 ; auto.
+ apply IHn. apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
apply (@gen_FOBIH_Dual_Detachment_Theorem) in p ; auto.
assert (pair_der (Union _ (Singleton _ (list_conj l)) (Singleton _ (form_enum n))) (Union _ (Singleton form (list_disj l0)) (Complement _ w))).
destruct p as (l' & Hl'0 & Hl'1 & Hl'2). exists l' ; repeat split ; auto. apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs _ _ _ Hl'2).
intros C HC ; inversion HC ; subst. apply prv_CI. apply Id ; right ; split. apply Id ; left ; split.
assert (pair_der (Singleton _ (list_conj l)) (Union _ (Union _ (Singleton _ (list_disj l0)) (Complement _ w)) (Singleton _ (form_enum n)))).
destruct HD as (l' & Hl'0 & Hl'1 & Hl'2). exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) ((form_enum n) :: (list_disj l0) :: l')) ; repeat split ; auto.
apply NoDup_nodup. intros A HA ; apply nodup_In in HA ; inversion HA ; subst. right ; split.
inversion H0 ; subst. left ; left ; split. left ; right ; apply Hl'1 ; auto. apply list_disj_nodup.
cbn. apply FOBIH_Dual_Detachment_Theorem in Hl'2. apply prv_DE with (form_enum n ∨ list_disj l0) (list_disj l') ; auto.
apply prv_DE with (form_enum n) (list_disj l0). apply Id ; unfold In ; auto. apply prv_DI1. apply Id ; unfold In ; auto.
apply prv_DI2 ; apply prv_DI1 ; apply Id ; unfold In ; auto. apply prv_DI2 ; apply prv_DI2 ; apply Id ; unfold In ; auto.
apply (@Cut) with (form_enum n) ; auto.
+ auto.
Qed.
Lemma Ldext_A0 n :
A0 el fst (Ldext n).
Proof.
induction n; cbn; try tauto.
destruct (Ldext n) as [L1 L2]. cbn in IHn.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM; cbn; tauto.
Qed.
Lemma Ldext_B0 n :
B0 el snd (Ldext n).
Proof.
induction n; cbn; try tauto.
destruct (Ldext n) as [L1 L2]. cbn in IHn.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM; cbn; tauto.
Qed.
Definition dext phi := exists n, phi el fst (Ldext n).
Lemma dext_der n :
dext |- list_conj (fst (Ldext n)).
Proof.
apply prv_list_conj. intros A HA. apply prv_ctx. now exists n.
Qed.
Lemma dext_prv phi :
dext |- phi -> exists n, (fun psi => psi el fst (Ldext n)) |- phi.
Proof.
intros [L[H1 H2]] % (@prv_compact _ _ eq_dec_preds eq_dec_funcs). revert phi H2.
induction L as [|psi L IH]; intros phi H2.
- exists 0. cbn. eapply prv_weak; try apply H2. intros B [].
- destruct (H1 psi) as [k Hk]; try now left.
destruct IH with (psi --> phi) as [n Hn].
* intros B HB. apply H1. now right.
* apply prv_DT. eapply prv_weak; try apply H2. unfold Included, In. cbn. intuition.
* exists (n + k). apply prv_DT in Hn. eapply prv_weak; try apply Hn.
intros B [| ->] ; eapply Ldext_cum1; try eassumption; lia.
Qed.
Lemma Ldext_mono T n n' :
n <= n' -> T |- list_disj (snd (Ldext n)) -> T |- list_disj (snd (Ldext n')).
Proof.
intros H. apply list_disj_mono. now apply Ldext_cum2.
Qed.
Lemma list_disj_weak : forall (T : form -> Prop) (L L' : list form),
(forall A, A el L -> T |- A --> list_disj L') -> T |- list_disj L -> T |- list_disj L'.
Proof.
intros T L. revert T. induction L ; cbn ; auto.
- intros. eapply MP. apply EFQ. auto.
- intros. eapply MP. eapply MP. eapply MP. apply Ax ; eapply A5 ; reflexivity.
3: exact H0. apply H ; auto. apply FOBIH_Deduction_Theorem. apply IHL.
intros. apply FOBIH_monot with T. apply H ; auto. intros C HC ; left ; auto.
apply Id ; right ; split.
Qed.
Lemma dext_nder n :
~ (pair_der dext (Union _ (Singleton _ (list_disj (snd (Ldext n)))) (Complement _ w))).
Proof.
intros (l & Hl0 & Hl1 & Hl2). destruct (dext_prv _ Hl2) as (k & Hk).
apply (Ldext_nder (max n k)). apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) ((list_disj (snd (Ldext (Init.Nat.max n k)))) :: remove (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) (list_disj (snd (Ldext n))) l)).
repeat split ; auto. apply NoDup_nodup. intros A HA ; apply nodup_In in HA. inversion HA ; subst. left ; split.
right. apply in_remove in H. destruct H. apply Hl1 in H. inversion H ; subst. exfalso ; inversion H1 ; subst ; auto. auto.
apply list_disj_nodup. apply list_disj_weak with l.
intros A HA. destruct ((@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) A (list_disj (snd (Ldext n)))) ; subst. apply FOBIH_Deduction_Theorem.
eapply MP. apply Ax ; eapply A3 ; reflexivity. apply list_disj_mono with (snd (Ldext n)).
apply Ldext_cum2. lia. apply Id ; right ; split. pose (Hl1 _ HA).
inversion u ; subst. inversion H ; subst. exfalso ; auto. cbn. eapply MP. eapply MP. apply Imp_trans.
2: apply Ax ; eapply A4 ; reflexivity. apply FOBIH_Deduction_Theorem. apply prv_list_disj with A.
apply in_in_remove ; auto. apply Id ; right ; split. apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs _ _ _ Hk). intros B HB.
eapply MP. apply list_conj_in_list. apply (Ldext_cum1 k (max n k)) ; auto. lia. apply Id ; split.
Qed.
Lemma dext_el phi :
dext phi -> w phi.
Proof.
intro H ; subst ; auto. destruct H.
destruct (LEM (w phi)) ; auto. exfalso. eapply (dext_nder (S x)) ; auto.
exists [phi]. repeat split.
- apply NoDup_cons. intro H2 ; inversion H2. apply NoDup_nil.
- intros D HD ; inversion HD ; subst. right ; auto. inversion H1.
- cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id. exists x ; exact H.
Qed.
Lemma dext_ex_henk :
ex_henk dext.
Proof.
intros phi H. remember (form_index (∃ phi)) as n.
destruct (Ldext n) as [L1 L2] eqn: HL.
destruct (SLEM (pair_der (Singleton _ (((∃ phi) ∧ list_conj L1) --< list_disj L2)) (Complement _ w))) eqn: HS.
{ exfalso. destruct H. assert (J: pair_der (Singleton form ((∃ phi) ∧ list_conj L1 --< list_disj L2)) (Complement form w)) ; auto.
destruct J as (l & Hl0 & Hl1 & Hl2). apply FOBIH_Dual_Detachment_Theorem in Hl2.
apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs) with (T':=Union _ (Singleton form (∃ phi)) (Singleton form (list_conj L1))) in Hl2.
apply (Ldext_nder (max (S n) x)). apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
exists (nodup (@eq_dec_form _ _ eq_dec_preds eq_dec_funcs) ((list_disj (snd (Ldext (Init.Nat.max (S n) x)))) :: l)).
repeat split ; auto. apply NoDup_nodup. intros A HA ; apply nodup_In in HA. inversion HA ; subst. left ; split.
right ; apply Hl1 ; auto. apply list_disj_nodup. remember (Ldext (Init.Nat.max (S n) x)) as X. cbn.
apply prv_DE with (list_disj L2) (list_disj l). apply (@prv_cut _ _ eq_dec_preds eq_dec_funcs _ _ _ Hl2).
intros A HA ; inversion HA ; subst. inversion H0 ; subst. eapply MP. eapply list_conj_in_list with (l:=(fst (Ldext (Init.Nat.max (S (form_index (∃ phi))) x)))).
apply Ldext_cum1 with x ; auto ; lia. apply Id ; split. inversion H0 ; subst.
apply prv_list_conj. intros B HB. eapply MP. eapply list_conj_in_list with (l:=(fst (Ldext (Init.Nat.max (S (form_index (∃ phi))) x)))).
apply Ldext_cum1 with (form_index (∃ phi)). lia. rewrite HL ; cbn ; auto. apply Id ; split. subst ; apply prv_DI1.
apply list_disj_mono with L2. assert (L2 = snd (Ldext (form_index (∃ phi)))). rewrite HL ; auto. rewrite H0. apply Ldext_cum2 ; lia.
apply Id ; right ; split. apply prv_DI2. apply Id ; right ; split.
intros B HB ; inversion HB ; subst. apply prv_CI. apply Id ; left ; split. apply Id ; right ; split. }
exists (proj1_sig (Ldext_ex n0)). exists (S n). cbn.
rewrite HL.
destruct form_all as [[]|]. rewrite Heqn in e. rewrite form_enum_index in e ; try discriminate.
destruct form_ex as [[]|].
- rewrite Heqn in e ; rewrite form_enum_index in e ; injection e. intros <-. rewrite HS. right. left. reflexivity.
- contradict n2. exists phi. rewrite Heqn. apply form_enum_index.
Qed.
Lemma dext_all_henk :
all_henk dext.
Proof.
intros phi HP. remember (form_index (∀ phi)) as n.
destruct (Ldext n) as [L1 L2] eqn: HL.
destruct (SLEM (pair_der (Singleton _ ((list_conj L1 --< ∀ phi) --< list_disj L2)) (Complement _ w))) eqn: HS.
- exfalso. apply HP. exists (S n). cbn. rewrite HL. rewrite Heqn ; cbn. rewrite form_enum_index ; cbn.
destruct form_all as [[]|].
+ injection e as ->. rewrite HS. now left.
+ contradict n0. now exists phi.
- exists (proj1_sig (Ldext_all n0)). intro. destruct H as (c & Hc).
apply (Ldext_nder (max (S n) c)). apply (@gen_FOBIH_Dual_Deduction_Theorem) ; auto.
exists [(list_disj (snd (Ldext (Init.Nat.max (S n) c))))].
repeat split ; auto. apply NoDup_cons. intro H ; inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H.
remember (Ldext (Init.Nat.max (S n) c)) as X. cbn.
eapply MP. apply Ax ; eapply A3 ; reflexivity. eapply MP. apply list_disj_In0. Unshelve. 3: exact phi[$(proj1_sig (Ldext_all n0))..]. subst.
pose (Ldext_cum2 (S (form_index (∀ phi)))). apply i. lia. cbn. rewrite HL. rewrite form_enum_index.
destruct form_all as [[]|]. inversion e ; subst. rewrite HS ; cbn. auto.
exfalso ; apply n ; exists phi ; auto. subst. eapply MP. apply list_conj_in_list.
pose (Ldext_cum1 c (max (S (form_index (∀ phi))) c)). apply i ; auto. lia. apply Id ; split.
Qed.
Lemma dext_ded_clos :
ded_clos dext.
Proof.
intros phi HP. destruct (form_enum_sur phi) as [n <-].
exists (S n). cbn. destruct Ldext eqn: HL.
destruct form_all as [[]|]; try destruct form_ex as [[]|]; destruct SLEM eqn:EqD; cbn in * ; auto.
- exfalso. rewrite e in HP. apply dext_nder with (S n).
exists [(list_disj (snd (Ldext (S n))))]. repeat split. apply NoDup_cons. intro H ; inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H.
remember (snd (Ldext (S n))) as X. cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. subst.
apply prv_list_disj with (∀ x) ; auto. cbn. rewrite HL ; cbn. destruct form_all as [[]|].
rewrite e in e0. inversion e0 ; subst. rewrite EqD ; cbn. auto. exfalso. apply n1. exists x ; firstorder.
- exfalso. rewrite e in HP. apply dext_nder with (S n).
exists [(list_disj (snd (Ldext (S n))))]. repeat split. apply NoDup_cons. intro H ; inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H.
remember (snd (Ldext (S n))) as X. cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. subst.
apply prv_list_disj with (∃ x) ; auto. cbn. rewrite HL ; cbn. destruct form_all as [[]|]. rewrite e0 in e. inversion e.
destruct form_ex as [[]|]. rewrite e0 in e. inversion e ; subst. rewrite EqD ; cbn. auto.
exfalso. apply n2. exists x ; firstorder.
- exfalso. apply dext_nder with (S n).
exists [(list_disj (snd (Ldext (S n))))]. repeat split. apply NoDup_cons. intro H ; inversion H. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H.
remember (snd (Ldext (S n))) as X. cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. subst.
apply prv_list_disj with (form_enum n) ; auto. cbn. rewrite HL ; cbn. destruct form_all as [[]|]. exfalso ; apply n0 ; exists x ; auto.
destruct form_ex as [[]|]. exfalso ; apply n1 ; exists x ; auto. rewrite EqD ; cbn. auto.
Qed.
Lemma dext_A0 :
dext A0.
Proof.
exists 0 ; cbn ; auto.
Qed.
Lemma dext_B0 :
~ dext B0.
Proof.
intros H. apply (dext_nder 0). exists [(list_disj (snd (Ldext 0)))].
repeat split. apply NoDup_cons. intro H0 ; inversion H0. apply NoDup_nil.
intros A HA ; inversion HA ; subst. left ; split. inversion H0.
cbn. eapply MP. apply Ax ; eapply A3 ; reflexivity. eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id ; auto.
Qed.
Lemma dext_consist :
consist dext.
Proof.
intros H. apply dext_B0. apply dext_ded_clos.
apply prv_MP with ⊥; trivial. apply EFQ.
Qed.
Lemma dext_prime :
prime dext.
Proof.
intros phi psi HD.
destruct (SLEM (dext phi)), (SLEM (dext psi)); try tauto.
remember (form_index phi) as m.
remember (form_index psi) as k.
exfalso.
assert (phi el (snd (Ldext (S m)))).
{ cbn. destruct Ldext eqn: HL. destruct (form_all (form_enum m)) eqn: EqAll. destruct s. subst.
destruct (SLEM (pair_der (Singleton form ((list_conj l --< (∀ x)) --< list_disj l0)) (Complement form w))) eqn: EqD.
exfalso. apply n. exists (S (form_index phi)). cbn. rewrite HL. rewrite EqAll. rewrite EqD. rewrite <- e.
rewrite form_enum_index. cbn ; auto. cbn. rewrite <- e ; rewrite form_enum_index ; auto.
destruct (form_ex (form_enum m)) eqn: EqEx. destruct s. subst.
destruct (SLEM (pair_der (Singleton form ((∃ x) ∧ list_conj l --< list_disj l0)) (Complement form w))) eqn: EqD.
rewrite <- e ; rewrite form_enum_index ; cbn ; auto.
exfalso. apply n. exists (S (form_index phi)). cbn. rewrite HL. rewrite EqAll. rewrite EqEx. rewrite EqD. rewrite <- e.
rewrite form_enum_index. cbn ; auto.
destruct (SLEM (pair_der (Singleton form (form_enum m ∧ list_conj l --< list_disj l0)) (Complement form w))) eqn: EqD.
rewrite Heqm ; rewrite form_enum_index ; cbn ; auto.
exfalso. apply n. exists (S (form_index phi)). cbn. rewrite <- Heqm. rewrite HL. rewrite EqAll. rewrite EqEx.
rewrite EqD. rewrite Heqm. rewrite form_enum_index. cbn ; auto. }
assert (psi el (snd (Ldext (S k)))).
{ cbn. destruct (Ldext k) eqn: HL. destruct (form_all (form_enum k)) eqn: EqAll. destruct s. subst.
destruct (SLEM (pair_der (Singleton form ((list_conj l --< (∀ x)) --< list_disj l0)) (Complement form w))) eqn: EqD.
exfalso. apply n0. exists (S (form_index psi)). cbn. rewrite HL. rewrite EqAll. rewrite EqD. rewrite <- e.
rewrite form_enum_index. cbn ; auto. cbn. rewrite <- e ; rewrite form_enum_index ; auto.
destruct (form_ex (form_enum k)) eqn: EqEx. destruct s. subst.
destruct (SLEM (pair_der (Singleton form ((∃ x) ∧ list_conj l --< list_disj l0)) (Complement form w))) eqn: EqD.
rewrite <- e ; rewrite form_enum_index ; cbn ; auto.
exfalso. apply n0. exists (S (form_index psi)). cbn. rewrite HL. rewrite EqAll. rewrite EqEx. rewrite EqD. rewrite <- e.
rewrite form_enum_index. cbn ; auto.
destruct (SLEM (pair_der (Singleton form (form_enum k ∧ list_conj l --< list_disj l0)) (Complement form w))) eqn: EqD.
rewrite Heqk ; rewrite form_enum_index ; cbn ; auto.
exfalso. apply n0. exists (S (form_index psi)). cbn. rewrite <- Heqk. rewrite HL. rewrite EqAll. rewrite EqEx.
rewrite EqD. rewrite Heqk. rewrite form_enum_index. cbn ; auto. }
apply dext_nder with (max (S m) (S k)).
exists [(list_disj (snd (Ldext (Init.Nat.max (S m) (S k)))))]. repeat split.
- apply NoDup_cons. intro H1 ; inversion H1. apply NoDup_nil.
- intros A HA ; inversion HA ; subst.
+ left ; split.
+ inversion H1.
- eapply MP. apply Ax ; eapply A3 ; reflexivity.
apply list_disj_mono with [phi;psi].
+ intros C HC. inversion HC ; subst.
* eapply (Ldext_cum2 _ _ _ _ H).
* inversion H1 ; subst.
-- eapply (Ldext_cum2 _ _ _ _ H0).
-- inversion H2.
+ cbn. eapply MP.
* apply Or_imp_assoc. apply Ax ; eapply A3 ; reflexivity.
* apply Id ; auto.
Unshelve. all: lia.
Qed.
End DownLind_constr.
Open Scope type.
Lemma Down_Lindenbaum_lemma : forall w A B,
consist w -> prime w -> ded_clos w ->
ex_henk w -> all_henk w ->
~ (pair_der (Singleton _ A) (adj (Complement form w) B)) ->
existsT2 w', consist w' *
prime w' *
ded_clos w' *
ex_henk w' *
all_henk w' *
(w' A) *
(~ (w' B)) *
(forall C, w' C -> w C).
Proof.
intros w A B cons prim dedclos exh allh H.
exists (dext w exh A B) ; auto. cbn ; repeat split ; auto.
- apply dext_consist ; auto.
- apply dext_prime ; auto.
- apply dext_ded_clos ; auto.
- apply dext_ex_henk ; auto.
- apply dext_all_henk ; auto.
- apply dext_A0.
- apply dext_B0 ; auto.
- apply dext_el ; auto.
Qed.
End DownLind.