CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Coq.Logic.Description.
Require Import Coq.Logic.FunctionalExtensionality.
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_remove_list.
Require Import CPP_BiInt_enum.
Require Import CPP_BiInt_Lindenbaum_lem_prelim.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* For any formula and context, either add the formula to the context, if the addition of
the formula to the context preserve relative consistency, or keep the context as is. *)
Definition choice_form (Γ Δ : @Ensemble BPropF) (A : BPropF) : Ensemble BPropF :=
fun x => (In _ Γ x) \/ ((pair_derrec (Union _ Γ (Singleton _ A), Δ) -> False) /\ A = x).
(* For any natural number, apply choice_form to the formula which it encodes. *)
Definition choice_code (Γ Δ : @Ensemble BPropF) (n :nat) : @Ensemble BPropF :=
(choice_form Γ Δ (form_enum n)).
(* We build prime pairs by stages. We start with the initial pair, and add formulas to the
left component by using the enumeration of formulas we have together with choice_code. *)
Fixpoint nprime_theory (Γ Δ : @Ensemble BPropF) (n : nat) : @Ensemble BPropF :=
match n with
| 0 => Γ
| S m => choice_code (nprime_theory Γ Δ m) Δ m
end.
(* We can thus define the left component of our pair: it is the collection of the left
component of all the nprime_theory. Note that this theory would classically be
a prime theory: this is why we call them prime_theory. *)
Definition prime_theory (Γ Δ : @Ensemble BPropF) : @Ensemble BPropF :=
fun x => (exists n, In _ (nprime_theory Γ Δ n) x).
(* Then, we define some properties of sets of formulas, or pairs of sets of formulas. *)
Definition closed (Γ : @Ensemble (BPropF)) :=
forall A, BIH_rules (Γ, A) -> Γ A.
Definition stable (Γ : @Ensemble (BPropF)) :=
forall A, ~ ~ Γ A -> Γ A.
Definition prime (Γ : @Ensemble (BPropF)) :=
forall A B, Γ (Or A B) -> Γ A \/ Γ B.
Definition quasi_prime (Γ : @Ensemble (BPropF)) :=
forall A B, Γ (Or A B) -> ~ ~ (Γ A \/ Γ B).
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* A helper lemma linking primeness and list_disj. *)
Lemma list_disj_prime : forall Γ,
~ (BIH_rules (Γ, Bot)) ->
prime Γ ->
forall x, Γ (list_disj x) -> exists y, List.In y x /\ Γ y.
Proof.
intros Γ H. induction x ; simpl ; intros ; auto.
- exfalso ; auto. apply H. apply Id. apply IdRule_I ; auto.
- apply H0 in H1. destruct H1 ; auto.
+ exists a ; split ; auto.
+ apply IHx in H1. destruct H1. destruct H1.
exists x0 ; split ; auto.
Qed.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* Properties of our prime theories, and the pairs built out of them. *)
(* A prime theory is an extension of the initial theory. *)
Lemma nprime_theory_extens : forall n (Γ Δ: @Ensemble BPropF) x,
In (BPropF) Γ x -> In (BPropF) (nprime_theory Γ Δ n) x.
Proof.
induction n.
- simpl. intros. unfold In. unfold choice_code. unfold choice_form. auto.
- simpl. intros. pose (IHn Γ Δ x H). unfold choice_code.
unfold choice_form. simpl. unfold In ; auto.
Qed.
Lemma nprime_theory_extens_le : forall m n (Γ Δ: @Ensemble BPropF) x,
In (BPropF) (nprime_theory Γ Δ n) x -> (le n m) -> In (BPropF) (nprime_theory Γ Δ m) x.
Proof.
induction m.
- intros. simpl. inversion H0. subst. simpl in H. auto.
- intros. inversion H0.
+ subst. auto.
+ subst. simpl. unfold In. apply IHm in H ; auto. unfold choice_code.
unfold choice_form. unfold In ; auto.
Qed.
Lemma prime_theory_extens : forall (Γ Δ: @Ensemble BPropF) x,
In (BPropF) Γ x -> In (BPropF) (prime_theory Γ Δ) x.
Proof.
intros. unfold prime_theory. unfold In. exists 0. unfold nprime_theory.
unfold choice_code. unfold choice_form ; auto.
Qed.
(* A prime theory preserves derivability. *)
Lemma der_nprime_theory_mprime_theory_le : forall n m (Γ Δ: @Ensemble BPropF) A,
(BIH_rules (nprime_theory Γ Δ n, A)) -> (le n m) ->
(BIH_rules (nprime_theory Γ Δ m, A)).
Proof.
intros.
pose (BIH_monot (nprime_theory Γ Δ n, A) H (nprime_theory Γ Δ m)).
simpl in b. apply b. intro. intros. apply nprime_theory_extens_le with (n:=n) ; auto.
Qed.
Lemma der_prime_theory_nprime_theory : forall s, (BIH_rules s) ->
(forall (Γ Δ: @Ensemble BPropF) A, (prime_theory Γ Δ = fst s) ->
(A = snd s) ->
(exists n, (BIH_rules (nprime_theory Γ Δ n, A)))).
Proof.
intros s D. induction D ; intros.
- inversion H. subst. simpl in H0. subst. simpl. unfold prime_theory in H2. destruct H2.
exists x. apply Id. apply IdRule_I. auto.
- inversion H. subst. simpl in H0. subst. simpl. exists 0. apply Ax. apply AxRule_I.
auto.
- inversion H1. subst. simpl in H2. subst.
assert (J1: List.In (prime_theory Γ Δ, A0 --> B) [(prime_theory Γ Δ, A0 --> B); (prime_theory Γ Δ, A0)]).
apply in_eq. pose (H (prime_theory Γ Δ, A0 --> B) J1).
assert (J2: List.In (prime_theory Γ Δ, A0) [(prime_theory Γ Δ, A0 --> B); (prime_theory Γ Δ, A0)]).
apply in_cons. apply in_eq. pose (H (prime_theory Γ Δ, A0) J2).
assert (J3: prime_theory Γ Δ = prime_theory Γ Δ). auto.
assert (J4: A0 --> B = A0 --> B). auto.
pose (H0 (prime_theory Γ Δ, A0 --> B) J1 Γ Δ (A0 --> B) J3 J4). destruct e. clear J4.
clear b. clear J1.
assert (J5: A0 = A0). auto.
pose (H0 (prime_theory Γ Δ, A0) J2 Γ Δ A0 J3 J5). destruct e. clear J5.
clear J3. clear b0. clear J2.
exists (max x x0). simpl.
apply MP with (ps:=[(nprime_theory Γ Δ (Init.Nat.max x x0), A0 --> B);(nprime_theory Γ Δ (Init.Nat.max x x0), A0)]).
2: apply MPRule_I. intros. inversion H4. subst.
pose (der_nprime_theory_mprime_theory_le x (Init.Nat.max x x0) _ _ _ H2). apply b.
lia. inversion H5. 2: inversion H6. subst. clear H4. clear H5.
pose (der_nprime_theory_mprime_theory_le x0 (Init.Nat.max x x0) _ _ _ H3). apply b. lia.
- subst. inversion H1. subst. simpl in H2. subst.
assert (J1: List.In (Empty_set (BPropF), A) [(Empty_set (BPropF), A)]). apply in_eq.
pose (H (Empty_set (BPropF), A) J1). simpl. exists 0. apply DNw with (ps:=[(Empty_set (BPropF), A)]).
2: apply DNwRule_I. intros. inversion H2. subst. auto. inversion H3.
Qed.
(* Each step of the construction preserves relative consistency. *)
Lemma Under_nprime_theory : forall n (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
(pair_derrec (nprime_theory Γ Δ n, Δ) -> False).
Proof.
induction n.
- intros. apply H. unfold nprime_theory in H0. auto.
- intros Γ Δ H. specialize (IHn _ _ H). intro.
apply IHn. destruct H0. destruct H0. destruct H1. simpl in H1.
apply BIH_monot with (Γ1:=nprime_theory Γ Δ n) in H2. simpl in H2. exists x.
repeat split ; auto. intros a Ha. simpl in Ha. unfold choice_code in Ha.
simpl in H2. unfold choice_code in H2. unfold In. unfold choice_form in Ha.
unfold choice_form in H2. unfold In in Ha. destruct Ha ; auto.
destruct H3 ; subst. exfalso. apply H3. exists x. repeat split ; auto. simpl.
apply BIH_monot with (Γ1:=Union BPropF (nprime_theory Γ Δ n) (Singleton BPropF (form_enum n))) in H2 ; auto.
intros b Hb. simpl in Hb. unfold In in Hb. destruct Hb. apply Union_introl ; auto.
destruct H4 ; subst. apply Union_intror. apply In_singleton.
Qed.
(* The pair built out of a prime theory and the right component of the initial
pair is relative consistent. *)
Lemma Under_Lind_pair_init : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
pair_derrec (prime_theory Γ Δ, Δ) -> False.
Proof.
intros. destruct H0. destruct H0. destruct H1. simpl in H1. simpl in H2.
epose (der_prime_theory_nprime_theory _ H2). simpl in e.
assert (prime_theory Γ Δ = prime_theory Γ Δ). auto.
assert (list_disj x = list_disj x). auto.
pose (e _ _ _ H3 H4). destruct e0. clear e.
pose (Under_nprime_theory x0 _ _ H). apply f.
exists x ; repeat split ; auto.
Qed.
(* A prime pair is closed under derivation. *)
Lemma closeder_fst_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) -> closed (prime_theory Γ Δ).
Proof.
intros. intros A H0. unfold prime_theory. exists (S (form_index A)). unfold In.
remember (form_index A) as n. unfold nprime_theory. pose (form_enum_index A). destruct n.
- unfold choice_form. right. split. intro. pose (Under_Lind_pair_init _ _ H). apply f.
destruct H1. simpl in H1. destruct H1. destruct H2. exists x.
repeat split ; auto. simpl.
pose (BIH_comp _ H3 (prime_theory Γ Δ)). simpl in b. apply b.
intros. inversion H4 ; subst. apply Id. apply IdRule_I. exists 0 ; auto.
simpl. unfold choice_code. unfold choice_form. unfold In ; auto.
inversion H5 ; subst ; auto. rewrite <- Heqn in e. rewrite e ; auto.
rewrite Heqn ; auto.
- right. split. intro. pose (Under_Lind_pair_init _ _ H). apply f.
destruct H1. simpl in H1. destruct H1. destruct H2. exists x.
repeat split ; auto. simpl.
pose (BIH_comp _ H3 (prime_theory Γ Δ)). simpl in b. apply b.
intros. inversion H4 ; subst. apply Id. apply IdRule_I. exists (S n) ; auto.
simpl. unfold choice_code. unfold choice_form. unfold In ; auto.
inversion H5 ; subst ; auto. rewrite <- Heqn in e. rewrite e ; auto.
rewrite Heqn ; auto.
Qed.
(* If a formula is not in the prime theory, then we know that not-not provability of the pair with the
prime theory and the formula on the left, and the right component of the initial theory
on the right, *)
Lemma not_In_prime_theory_deriv : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
forall A, ~ (prime_theory Γ Δ A) -> ~~ (pair_derrec (Union _ (prime_theory Γ Δ) (Singleton _ A), Δ)).
Proof.
intros. intro. apply H0. exists (S (form_index A)).
unfold nprime_theory. simpl. unfold In.
remember (form_index A) as n. pose (form_enum_index A). destruct n.
- unfold choice_code. unfold choice_form. right ; split.
intro. apply H1. destruct H2. simpl in H2. destruct H2. destruct H3.
exists x. simpl ; repeat split ; auto.
apply BIH_monot with (Γ1:=Union BPropF (prime_theory Γ Δ) (Singleton BPropF A)) in H4 ; auto.
intro. simpl ; intros. inversion H5 ; subst. apply Union_introl.
exists 0 ; auto.
apply Union_intror. rewrite <- Heqn in e. rewrite <- e. auto.
rewrite Heqn ; auto.
- right ; split.
intro. apply H1. destruct H2. simpl in H2. destruct H2. destruct H3.
exists x. simpl ; repeat split ; auto.
apply BIH_monot with (Γ1:=Union BPropF (prime_theory Γ Δ) (Singleton BPropF A)) in H4 ; auto.
intro. simpl ; intros. inversion H5 ; subst. apply Union_introl.
exists (S n) ; auto.
apply Union_intror. rewrite <- Heqn in e. rewrite <- e. auto.
rewrite Heqn ; auto.
Qed.
(* A prime theory is (constructively) quasi-prime. *)
Lemma quasi_prime_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
quasi_prime (prime_theory Γ Δ).
Proof.
intros. intros A B H0. intro.
assert (p: forall C, ~ ~ (prime_theory Γ Δ C \/ ~ (prime_theory Γ Δ C))).
intros C H2. apply H2. right. intro. apply H2 ; auto.
pose (p A). pose (p B). apply n. intro. destruct H2. apply H1 ; auto.
apply n0 ; intro. destruct H3. apply H1 ; auto.
apply not_In_prime_theory_deriv in H2 ; auto. apply H2. intro.
apply not_In_prime_theory_deriv in H3 ; auto. apply H3 ; intro.
apply Under_Lind_pair_init with (Γ:=Γ) (Δ:=Δ) ; auto.
destruct H4. simpl in H4. destruct H4. destruct H6.
destruct H5. simpl in H5. destruct H5. destruct H8.
exists (x ++ remove_list x x0). repeat split ; auto.
apply add_remove_list_preserve_NoDup ; auto.
simpl ; intros. apply in_app_or in H10. destruct H10 ; auto.
apply In_remove_list_In_list in H10 ; auto. simpl.
remember (list_disj (x ++ remove_list x x0)) as E.
apply MP with (ps:=[(prime_theory Γ Δ, (Or A B) --> E);
(prime_theory Γ Δ, (Or A B))]). 2: apply MPRule_I. intros. inversion H10.
rewrite <- H11.
apply MP with (ps:=[(prime_theory Γ Δ, (B --> E) --> (Or A B --> E));
(prime_theory Γ Δ, (B --> E))]). 2: apply MPRule_I. intros. inversion H12.
rewrite <- H13.
apply MP with (ps:=[(prime_theory Γ Δ, (A --> E) --> (B --> E) --> (Or A B --> E));
(prime_theory Γ Δ, (A --> E))]). 2: apply MPRule_I. intros. inversion H14.
rewrite <- H15. apply Ax. apply AxRule_I. apply RA4_I. exists A. exists B.
exists E. auto. inversion H15. 2: inversion H16. rewrite <- H16. subst.
apply der_list_disj_remove1.
apply BIH_Deduction_Theorem with (s:=(Union (BPropF) (prime_theory Γ Δ) (Singleton (BPropF) A), list_disj x)) ; auto.
inversion H13. subst.
apply der_list_disj_remove2.
apply BIH_Deduction_Theorem with (s:=(Union (BPropF) (prime_theory Γ Δ) (Singleton (BPropF) B), list_disj x0)) ; auto.
inversion H14. inversion H11. rewrite <- H12.
apply Id. apply IdRule_I ; auto. inversion H12.
Qed.
(* A prime theory is consistent. *)
Lemma Consist_nprime_theory : forall n (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
(BIH_rules (nprime_theory Γ Δ n, Bot) -> False).
Proof.
intros. pose (Under_nprime_theory n Γ Δ H).
apply f. exists []. repeat split ; auto. apply NoDup_nil.
intros. inversion H1.
Qed.
Lemma Consist_prime_theory : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
(BIH_rules (prime_theory Γ Δ, Bot) -> False).
Proof.
intros. apply closeder_fst_Lind_pair in H0 ; auto. unfold prime_theory in H0.
unfold In in H0. destruct H0. apply Consist_nprime_theory with (Γ:=Γ) (Δ:=Δ) (n:=x) ; auto.
apply Id. apply IdRule_I. auto.
Qed.
(* A prime pair is relative consistent. *)
Lemma Under_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
pair_derrec (prime_theory Γ Δ, Complement _ (prime_theory Γ Δ)) -> False.
Proof.
intros. destruct H0. destruct H0. destruct H1. simpl in H1. simpl in H2.
induction x.
- simpl in H2. pose (Consist_prime_theory _ _ H H2) ; auto.
- simpl in H2.
pose (closeder_fst_Lind_pair _ _ H _ H2).
pose (quasi_prime_Lind_pair _ _ H).
simpl in p. pose (q a (list_disj x) p). apply n. intro.
destruct H3. assert (List.In a (a :: x)). apply in_eq. pose (H1 _ H4) ; auto.
apply IHx. inversion H0 ; auto. intros. apply H1. apply in_cons ; auto.
apply Id. apply IdRule_I ; auto.
Qed.
(* The right component of a prime pair (the complement of the left component) is
an extension of the right component of the initial pair. *)
Lemma Compl_prime_theory_extens : forall (Γ Δ: @Ensemble BPropF) x,
(pair_derrec (Γ, Δ) -> False) -> In (BPropF) Δ x -> In (BPropF) (Complement _ (prime_theory Γ Δ)) x.
Proof.
intros. intros H1.
apply Under_Lind_pair_init with (Γ:=Γ) (Δ:=Δ) ; auto.
exists [x]. repeat split. apply NoDup_cons. intro. inversion H2.
apply NoDup_nil. simpl. intros. destruct H2 ; subst ; auto. exfalso ; auto.
simpl. apply MP with (ps:=[(prime_theory Γ Δ, x --> Or x Bot);(prime_theory Γ Δ, x)]).
2: apply MPRule_I. intros. inversion H2 ; subst.
apply Ax. apply AxRule_I. apply RA2_I. exists x ; exists Bot ; auto.
inversion H3 ; subst. apply Id. apply IdRule_I ; auto. inversion H4.
Qed.
(* A prime pair is (left-)stable. *)
Lemma stable_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
stable (prime_theory Γ Δ).
Proof.
intros. intro. intros. exists (S (form_index A)).
unfold nprime_theory. unfold In.
remember (form_index A) as n. pose (form_enum_index A). destruct n.
- unfold choice_code. unfold choice_form. right ; split.
intro. apply H0. intro.
apply Under_Lind_pair_init with (Γ:=Γ) (Δ:=Δ) ; auto.
destruct H1. simpl in H1. destruct H1. destruct H3.
exists x. simpl ; repeat split ; auto.
apply BIH_monot with (Γ1:=(prime_theory Γ Δ)) in H4 ; auto.
intro. simpl ; intros. inversion H5 ; subst. exists 1 ; auto.
unfold nprime_theory. unfold choice_code. unfold choice_form. left ; auto.
inversion H6 ; subst ; auto. rewrite <- Heqn in e. rewrite e. auto.
rewrite Heqn ; auto.
- unfold choice_code. unfold choice_form. right ; split.
intro. apply H0. intro.
apply Under_Lind_pair_init with (Γ:=Γ) (Δ:=Δ) ; auto.
destruct H1. simpl in H1. destruct H1. destruct H3.
exists x. simpl ; repeat split ; auto.
apply BIH_monot with (Γ1:=(prime_theory Γ Δ)) in H4 ; auto.
intro. simpl ; intros. inversion H5 ; subst. exists (S n) ; auto.
inversion H6 ; subst ; auto. rewrite <- Heqn in e. rewrite e. auto.
rewrite Heqn ; auto.
Qed.
(* A prime pair is (right-)stable. *)
Lemma right_stable_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
stable (Complement _ (prime_theory Γ Δ)).
Proof.
intros. intro. intros. intro. apply H0. intro. auto.
Qed.
(* Lindenbaum lemma. *)
Lemma Lindenbaum Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists Γm, Included _ Γ Γm
/\ closed Γm
/\ stable Γm
/\ quasi_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 quasi_prime_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in H0 ; auto.
Qed.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Coq.Logic.Description.
Require Import Coq.Logic.FunctionalExtensionality.
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_remove_list.
Require Import CPP_BiInt_enum.
Require Import CPP_BiInt_Lindenbaum_lem_prelim.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* For any formula and context, either add the formula to the context, if the addition of
the formula to the context preserve relative consistency, or keep the context as is. *)
Definition choice_form (Γ Δ : @Ensemble BPropF) (A : BPropF) : Ensemble BPropF :=
fun x => (In _ Γ x) \/ ((pair_derrec (Union _ Γ (Singleton _ A), Δ) -> False) /\ A = x).
(* For any natural number, apply choice_form to the formula which it encodes. *)
Definition choice_code (Γ Δ : @Ensemble BPropF) (n :nat) : @Ensemble BPropF :=
(choice_form Γ Δ (form_enum n)).
(* We build prime pairs by stages. We start with the initial pair, and add formulas to the
left component by using the enumeration of formulas we have together with choice_code. *)
Fixpoint nprime_theory (Γ Δ : @Ensemble BPropF) (n : nat) : @Ensemble BPropF :=
match n with
| 0 => Γ
| S m => choice_code (nprime_theory Γ Δ m) Δ m
end.
(* We can thus define the left component of our pair: it is the collection of the left
component of all the nprime_theory. Note that this theory would classically be
a prime theory: this is why we call them prime_theory. *)
Definition prime_theory (Γ Δ : @Ensemble BPropF) : @Ensemble BPropF :=
fun x => (exists n, In _ (nprime_theory Γ Δ n) x).
(* Then, we define some properties of sets of formulas, or pairs of sets of formulas. *)
Definition closed (Γ : @Ensemble (BPropF)) :=
forall A, BIH_rules (Γ, A) -> Γ A.
Definition stable (Γ : @Ensemble (BPropF)) :=
forall A, ~ ~ Γ A -> Γ A.
Definition prime (Γ : @Ensemble (BPropF)) :=
forall A B, Γ (Or A B) -> Γ A \/ Γ B.
Definition quasi_prime (Γ : @Ensemble (BPropF)) :=
forall A B, Γ (Or A B) -> ~ ~ (Γ A \/ Γ B).
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* A helper lemma linking primeness and list_disj. *)
Lemma list_disj_prime : forall Γ,
~ (BIH_rules (Γ, Bot)) ->
prime Γ ->
forall x, Γ (list_disj x) -> exists y, List.In y x /\ Γ y.
Proof.
intros Γ H. induction x ; simpl ; intros ; auto.
- exfalso ; auto. apply H. apply Id. apply IdRule_I ; auto.
- apply H0 in H1. destruct H1 ; auto.
+ exists a ; split ; auto.
+ apply IHx in H1. destruct H1. destruct H1.
exists x0 ; split ; auto.
Qed.
(* ------------------------------------------------------------------------------------------------------------------------------------ *)
(* Properties of our prime theories, and the pairs built out of them. *)
(* A prime theory is an extension of the initial theory. *)
Lemma nprime_theory_extens : forall n (Γ Δ: @Ensemble BPropF) x,
In (BPropF) Γ x -> In (BPropF) (nprime_theory Γ Δ n) x.
Proof.
induction n.
- simpl. intros. unfold In. unfold choice_code. unfold choice_form. auto.
- simpl. intros. pose (IHn Γ Δ x H). unfold choice_code.
unfold choice_form. simpl. unfold In ; auto.
Qed.
Lemma nprime_theory_extens_le : forall m n (Γ Δ: @Ensemble BPropF) x,
In (BPropF) (nprime_theory Γ Δ n) x -> (le n m) -> In (BPropF) (nprime_theory Γ Δ m) x.
Proof.
induction m.
- intros. simpl. inversion H0. subst. simpl in H. auto.
- intros. inversion H0.
+ subst. auto.
+ subst. simpl. unfold In. apply IHm in H ; auto. unfold choice_code.
unfold choice_form. unfold In ; auto.
Qed.
Lemma prime_theory_extens : forall (Γ Δ: @Ensemble BPropF) x,
In (BPropF) Γ x -> In (BPropF) (prime_theory Γ Δ) x.
Proof.
intros. unfold prime_theory. unfold In. exists 0. unfold nprime_theory.
unfold choice_code. unfold choice_form ; auto.
Qed.
(* A prime theory preserves derivability. *)
Lemma der_nprime_theory_mprime_theory_le : forall n m (Γ Δ: @Ensemble BPropF) A,
(BIH_rules (nprime_theory Γ Δ n, A)) -> (le n m) ->
(BIH_rules (nprime_theory Γ Δ m, A)).
Proof.
intros.
pose (BIH_monot (nprime_theory Γ Δ n, A) H (nprime_theory Γ Δ m)).
simpl in b. apply b. intro. intros. apply nprime_theory_extens_le with (n:=n) ; auto.
Qed.
Lemma der_prime_theory_nprime_theory : forall s, (BIH_rules s) ->
(forall (Γ Δ: @Ensemble BPropF) A, (prime_theory Γ Δ = fst s) ->
(A = snd s) ->
(exists n, (BIH_rules (nprime_theory Γ Δ n, A)))).
Proof.
intros s D. induction D ; intros.
- inversion H. subst. simpl in H0. subst. simpl. unfold prime_theory in H2. destruct H2.
exists x. apply Id. apply IdRule_I. auto.
- inversion H. subst. simpl in H0. subst. simpl. exists 0. apply Ax. apply AxRule_I.
auto.
- inversion H1. subst. simpl in H2. subst.
assert (J1: List.In (prime_theory Γ Δ, A0 --> B) [(prime_theory Γ Δ, A0 --> B); (prime_theory Γ Δ, A0)]).
apply in_eq. pose (H (prime_theory Γ Δ, A0 --> B) J1).
assert (J2: List.In (prime_theory Γ Δ, A0) [(prime_theory Γ Δ, A0 --> B); (prime_theory Γ Δ, A0)]).
apply in_cons. apply in_eq. pose (H (prime_theory Γ Δ, A0) J2).
assert (J3: prime_theory Γ Δ = prime_theory Γ Δ). auto.
assert (J4: A0 --> B = A0 --> B). auto.
pose (H0 (prime_theory Γ Δ, A0 --> B) J1 Γ Δ (A0 --> B) J3 J4). destruct e. clear J4.
clear b. clear J1.
assert (J5: A0 = A0). auto.
pose (H0 (prime_theory Γ Δ, A0) J2 Γ Δ A0 J3 J5). destruct e. clear J5.
clear J3. clear b0. clear J2.
exists (max x x0). simpl.
apply MP with (ps:=[(nprime_theory Γ Δ (Init.Nat.max x x0), A0 --> B);(nprime_theory Γ Δ (Init.Nat.max x x0), A0)]).
2: apply MPRule_I. intros. inversion H4. subst.
pose (der_nprime_theory_mprime_theory_le x (Init.Nat.max x x0) _ _ _ H2). apply b.
lia. inversion H5. 2: inversion H6. subst. clear H4. clear H5.
pose (der_nprime_theory_mprime_theory_le x0 (Init.Nat.max x x0) _ _ _ H3). apply b. lia.
- subst. inversion H1. subst. simpl in H2. subst.
assert (J1: List.In (Empty_set (BPropF), A) [(Empty_set (BPropF), A)]). apply in_eq.
pose (H (Empty_set (BPropF), A) J1). simpl. exists 0. apply DNw with (ps:=[(Empty_set (BPropF), A)]).
2: apply DNwRule_I. intros. inversion H2. subst. auto. inversion H3.
Qed.
(* Each step of the construction preserves relative consistency. *)
Lemma Under_nprime_theory : forall n (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
(pair_derrec (nprime_theory Γ Δ n, Δ) -> False).
Proof.
induction n.
- intros. apply H. unfold nprime_theory in H0. auto.
- intros Γ Δ H. specialize (IHn _ _ H). intro.
apply IHn. destruct H0. destruct H0. destruct H1. simpl in H1.
apply BIH_monot with (Γ1:=nprime_theory Γ Δ n) in H2. simpl in H2. exists x.
repeat split ; auto. intros a Ha. simpl in Ha. unfold choice_code in Ha.
simpl in H2. unfold choice_code in H2. unfold In. unfold choice_form in Ha.
unfold choice_form in H2. unfold In in Ha. destruct Ha ; auto.
destruct H3 ; subst. exfalso. apply H3. exists x. repeat split ; auto. simpl.
apply BIH_monot with (Γ1:=Union BPropF (nprime_theory Γ Δ n) (Singleton BPropF (form_enum n))) in H2 ; auto.
intros b Hb. simpl in Hb. unfold In in Hb. destruct Hb. apply Union_introl ; auto.
destruct H4 ; subst. apply Union_intror. apply In_singleton.
Qed.
(* The pair built out of a prime theory and the right component of the initial
pair is relative consistent. *)
Lemma Under_Lind_pair_init : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
pair_derrec (prime_theory Γ Δ, Δ) -> False.
Proof.
intros. destruct H0. destruct H0. destruct H1. simpl in H1. simpl in H2.
epose (der_prime_theory_nprime_theory _ H2). simpl in e.
assert (prime_theory Γ Δ = prime_theory Γ Δ). auto.
assert (list_disj x = list_disj x). auto.
pose (e _ _ _ H3 H4). destruct e0. clear e.
pose (Under_nprime_theory x0 _ _ H). apply f.
exists x ; repeat split ; auto.
Qed.
(* A prime pair is closed under derivation. *)
Lemma closeder_fst_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) -> closed (prime_theory Γ Δ).
Proof.
intros. intros A H0. unfold prime_theory. exists (S (form_index A)). unfold In.
remember (form_index A) as n. unfold nprime_theory. pose (form_enum_index A). destruct n.
- unfold choice_form. right. split. intro. pose (Under_Lind_pair_init _ _ H). apply f.
destruct H1. simpl in H1. destruct H1. destruct H2. exists x.
repeat split ; auto. simpl.
pose (BIH_comp _ H3 (prime_theory Γ Δ)). simpl in b. apply b.
intros. inversion H4 ; subst. apply Id. apply IdRule_I. exists 0 ; auto.
simpl. unfold choice_code. unfold choice_form. unfold In ; auto.
inversion H5 ; subst ; auto. rewrite <- Heqn in e. rewrite e ; auto.
rewrite Heqn ; auto.
- right. split. intro. pose (Under_Lind_pair_init _ _ H). apply f.
destruct H1. simpl in H1. destruct H1. destruct H2. exists x.
repeat split ; auto. simpl.
pose (BIH_comp _ H3 (prime_theory Γ Δ)). simpl in b. apply b.
intros. inversion H4 ; subst. apply Id. apply IdRule_I. exists (S n) ; auto.
simpl. unfold choice_code. unfold choice_form. unfold In ; auto.
inversion H5 ; subst ; auto. rewrite <- Heqn in e. rewrite e ; auto.
rewrite Heqn ; auto.
Qed.
(* If a formula is not in the prime theory, then we know that not-not provability of the pair with the
prime theory and the formula on the left, and the right component of the initial theory
on the right, *)
Lemma not_In_prime_theory_deriv : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
forall A, ~ (prime_theory Γ Δ A) -> ~~ (pair_derrec (Union _ (prime_theory Γ Δ) (Singleton _ A), Δ)).
Proof.
intros. intro. apply H0. exists (S (form_index A)).
unfold nprime_theory. simpl. unfold In.
remember (form_index A) as n. pose (form_enum_index A). destruct n.
- unfold choice_code. unfold choice_form. right ; split.
intro. apply H1. destruct H2. simpl in H2. destruct H2. destruct H3.
exists x. simpl ; repeat split ; auto.
apply BIH_monot with (Γ1:=Union BPropF (prime_theory Γ Δ) (Singleton BPropF A)) in H4 ; auto.
intro. simpl ; intros. inversion H5 ; subst. apply Union_introl.
exists 0 ; auto.
apply Union_intror. rewrite <- Heqn in e. rewrite <- e. auto.
rewrite Heqn ; auto.
- right ; split.
intro. apply H1. destruct H2. simpl in H2. destruct H2. destruct H3.
exists x. simpl ; repeat split ; auto.
apply BIH_monot with (Γ1:=Union BPropF (prime_theory Γ Δ) (Singleton BPropF A)) in H4 ; auto.
intro. simpl ; intros. inversion H5 ; subst. apply Union_introl.
exists (S n) ; auto.
apply Union_intror. rewrite <- Heqn in e. rewrite <- e. auto.
rewrite Heqn ; auto.
Qed.
(* A prime theory is (constructively) quasi-prime. *)
Lemma quasi_prime_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
quasi_prime (prime_theory Γ Δ).
Proof.
intros. intros A B H0. intro.
assert (p: forall C, ~ ~ (prime_theory Γ Δ C \/ ~ (prime_theory Γ Δ C))).
intros C H2. apply H2. right. intro. apply H2 ; auto.
pose (p A). pose (p B). apply n. intro. destruct H2. apply H1 ; auto.
apply n0 ; intro. destruct H3. apply H1 ; auto.
apply not_In_prime_theory_deriv in H2 ; auto. apply H2. intro.
apply not_In_prime_theory_deriv in H3 ; auto. apply H3 ; intro.
apply Under_Lind_pair_init with (Γ:=Γ) (Δ:=Δ) ; auto.
destruct H4. simpl in H4. destruct H4. destruct H6.
destruct H5. simpl in H5. destruct H5. destruct H8.
exists (x ++ remove_list x x0). repeat split ; auto.
apply add_remove_list_preserve_NoDup ; auto.
simpl ; intros. apply in_app_or in H10. destruct H10 ; auto.
apply In_remove_list_In_list in H10 ; auto. simpl.
remember (list_disj (x ++ remove_list x x0)) as E.
apply MP with (ps:=[(prime_theory Γ Δ, (Or A B) --> E);
(prime_theory Γ Δ, (Or A B))]). 2: apply MPRule_I. intros. inversion H10.
rewrite <- H11.
apply MP with (ps:=[(prime_theory Γ Δ, (B --> E) --> (Or A B --> E));
(prime_theory Γ Δ, (B --> E))]). 2: apply MPRule_I. intros. inversion H12.
rewrite <- H13.
apply MP with (ps:=[(prime_theory Γ Δ, (A --> E) --> (B --> E) --> (Or A B --> E));
(prime_theory Γ Δ, (A --> E))]). 2: apply MPRule_I. intros. inversion H14.
rewrite <- H15. apply Ax. apply AxRule_I. apply RA4_I. exists A. exists B.
exists E. auto. inversion H15. 2: inversion H16. rewrite <- H16. subst.
apply der_list_disj_remove1.
apply BIH_Deduction_Theorem with (s:=(Union (BPropF) (prime_theory Γ Δ) (Singleton (BPropF) A), list_disj x)) ; auto.
inversion H13. subst.
apply der_list_disj_remove2.
apply BIH_Deduction_Theorem with (s:=(Union (BPropF) (prime_theory Γ Δ) (Singleton (BPropF) B), list_disj x0)) ; auto.
inversion H14. inversion H11. rewrite <- H12.
apply Id. apply IdRule_I ; auto. inversion H12.
Qed.
(* A prime theory is consistent. *)
Lemma Consist_nprime_theory : forall n (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
(BIH_rules (nprime_theory Γ Δ n, Bot) -> False).
Proof.
intros. pose (Under_nprime_theory n Γ Δ H).
apply f. exists []. repeat split ; auto. apply NoDup_nil.
intros. inversion H1.
Qed.
Lemma Consist_prime_theory : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
(BIH_rules (prime_theory Γ Δ, Bot) -> False).
Proof.
intros. apply closeder_fst_Lind_pair in H0 ; auto. unfold prime_theory in H0.
unfold In in H0. destruct H0. apply Consist_nprime_theory with (Γ:=Γ) (Δ:=Δ) (n:=x) ; auto.
apply Id. apply IdRule_I. auto.
Qed.
(* A prime pair is relative consistent. *)
Lemma Under_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
pair_derrec (prime_theory Γ Δ, Complement _ (prime_theory Γ Δ)) -> False.
Proof.
intros. destruct H0. destruct H0. destruct H1. simpl in H1. simpl in H2.
induction x.
- simpl in H2. pose (Consist_prime_theory _ _ H H2) ; auto.
- simpl in H2.
pose (closeder_fst_Lind_pair _ _ H _ H2).
pose (quasi_prime_Lind_pair _ _ H).
simpl in p. pose (q a (list_disj x) p). apply n. intro.
destruct H3. assert (List.In a (a :: x)). apply in_eq. pose (H1 _ H4) ; auto.
apply IHx. inversion H0 ; auto. intros. apply H1. apply in_cons ; auto.
apply Id. apply IdRule_I ; auto.
Qed.
(* The right component of a prime pair (the complement of the left component) is
an extension of the right component of the initial pair. *)
Lemma Compl_prime_theory_extens : forall (Γ Δ: @Ensemble BPropF) x,
(pair_derrec (Γ, Δ) -> False) -> In (BPropF) Δ x -> In (BPropF) (Complement _ (prime_theory Γ Δ)) x.
Proof.
intros. intros H1.
apply Under_Lind_pair_init with (Γ:=Γ) (Δ:=Δ) ; auto.
exists [x]. repeat split. apply NoDup_cons. intro. inversion H2.
apply NoDup_nil. simpl. intros. destruct H2 ; subst ; auto. exfalso ; auto.
simpl. apply MP with (ps:=[(prime_theory Γ Δ, x --> Or x Bot);(prime_theory Γ Δ, x)]).
2: apply MPRule_I. intros. inversion H2 ; subst.
apply Ax. apply AxRule_I. apply RA2_I. exists x ; exists Bot ; auto.
inversion H3 ; subst. apply Id. apply IdRule_I ; auto. inversion H4.
Qed.
(* A prime pair is (left-)stable. *)
Lemma stable_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
stable (prime_theory Γ Δ).
Proof.
intros. intro. intros. exists (S (form_index A)).
unfold nprime_theory. unfold In.
remember (form_index A) as n. pose (form_enum_index A). destruct n.
- unfold choice_code. unfold choice_form. right ; split.
intro. apply H0. intro.
apply Under_Lind_pair_init with (Γ:=Γ) (Δ:=Δ) ; auto.
destruct H1. simpl in H1. destruct H1. destruct H3.
exists x. simpl ; repeat split ; auto.
apply BIH_monot with (Γ1:=(prime_theory Γ Δ)) in H4 ; auto.
intro. simpl ; intros. inversion H5 ; subst. exists 1 ; auto.
unfold nprime_theory. unfold choice_code. unfold choice_form. left ; auto.
inversion H6 ; subst ; auto. rewrite <- Heqn in e. rewrite e. auto.
rewrite Heqn ; auto.
- unfold choice_code. unfold choice_form. right ; split.
intro. apply H0. intro.
apply Under_Lind_pair_init with (Γ:=Γ) (Δ:=Δ) ; auto.
destruct H1. simpl in H1. destruct H1. destruct H3.
exists x. simpl ; repeat split ; auto.
apply BIH_monot with (Γ1:=(prime_theory Γ Δ)) in H4 ; auto.
intro. simpl ; intros. inversion H5 ; subst. exists (S n) ; auto.
inversion H6 ; subst ; auto. rewrite <- Heqn in e. rewrite e. auto.
rewrite Heqn ; auto.
Qed.
(* A prime pair is (right-)stable. *)
Lemma right_stable_Lind_pair : forall (Γ Δ: @Ensemble BPropF), (pair_derrec (Γ, Δ) -> False) ->
stable (Complement _ (prime_theory Γ Δ)).
Proof.
intros. intro. intros. intro. apply H0. intro. auto.
Qed.
(* Lindenbaum lemma. *)
Lemma Lindenbaum Γ Δ :
~ pair_derrec (Γ, Δ) ->
exists Γm, Included _ Γ Γm
/\ closed Γm
/\ stable Γm
/\ quasi_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 quasi_prime_Lind_pair ; auto.
- intro. apply Under_Lind_pair_init in H0 ; auto.
Qed.