KM.GHC.Lindenbaum_lem
From Stdlib Require Import List Arith Lia Ensembles.
From Stdlib.Logic Require Import Description FunctionalExtensionality.
Export ListNotations.
Require Import syntax.
Require Import KMH.
Require Import logics.
Require Import properties.
Require Import enum.
Section General_Lind.
Section Sets_of_forms.
Definition SubTheory (Γ Δ: @Ensemble form) (Incl: Included _ Δ Γ) := forall φ, (KMH_prv Δ φ /\ In _ Γ φ) -> In _ Δ φ.
Definition closed Γ :=
forall φ, KMH_prv Γ φ -> Γ φ.
Definition prime (Γ : @Ensemble form) :=
forall φ ψ, Γ (Or φ ψ) -> Γ φ \/ Γ ψ.
Definition quasi_prime (Γ : @Ensemble form) :=
forall φ ψ, Γ (Or φ ψ) -> ~ ~ (Γ φ \/ Γ ψ).
End Sets_of_forms.
Section prelims.
Lemma prime_list_disj l Γ :
prime Γ -> Γ (list_disj l) -> exists A, (List.In A l \/ A = Bot) /\ Γ A.
Proof.
induction l ; cbn ; intros.
- exists Bot ; auto.
- destruct (H _ _ H0). exists a ; split ; auto. apply IHl in H1 ; auto.
destruct H1 as (A & [H2 | H2] & H3). exists A ; split ; auto. subst.
exists Bot ; split ; auto.
Qed.
Definition Theory Γ := closed Γ /\ prime Γ.
Definition AllForm := fun (A: form) => True.
Lemma Theory_AllForm : Theory AllForm.
Proof.
split.
- intros A HA. unfold AllForm ; auto.
- intros A B Hor. left ; unfold AllForm ; auto.
Qed.
End prelims.
Section Prime.
(* We define the step-by-step construction of the Lindenbaum extension. *)
Definition choice_form Γ ψ φ: Ensemble form :=
fun x => Γ x \/ (~ (KMH_prv (Union _ Γ (Singleton _ x)) ψ) /\ φ = x).
Definition choice_code Γ ψ (n :nat) : @Ensemble form := (choice_form Γ ψ (form_enum n)).
Fixpoint nLind_theory Γ ψ n : @Ensemble form :=
match n with
| 0 => Γ
| S m => choice_code (nLind_theory Γ ψ m) ψ m
end.
(* The Lindenbaum extension is then defined as follows. *)
Definition Lind_theory Γ ψ : @Ensemble form :=
fun x => (exists n, In _ (nLind_theory Γ ψ n) x).
End Prime.
Section PrimeProps.
(* The Lindenbaum theory is an extension of the initial set of formulas. *)
Lemma nLind_theory_extens : forall n Γ ψ φ,
In _ Γ φ -> In _ (nLind_theory Γ ψ n) φ.
Proof.
induction n.
- cbn. intros. unfold In. unfold choice_code. unfold choice_form. auto.
- cbn. intros. pose (IHn Γ ψ φ H). unfold choice_code.
unfold choice_form. cbn. unfold In ; auto.
Qed.
Lemma nLind_theory_extens_le : forall m n Γ ψ φ,
In _ (nLind_theory Γ ψ n) φ -> (le n m) -> In _ (nLind_theory Γ ψ m) φ.
Proof.
induction m.
- intros. cbn. inversion H0. subst. cbn in H. auto.
- intros. inversion H0.
+ subst. auto.
+ subst. cbn. unfold In. apply IHm in H ; auto. unfold choice_code.
unfold choice_form. unfold In ; auto.
Qed.
Lemma Lind_theory_extens : forall Γ ψ φ,
Γ φ -> In _ (Lind_theory Γ ψ) φ.
Proof.
intros. unfold Lind_theory. unfold In. exists 0. unfold nLind_theory.
unfold choice_code. unfold choice_form ; auto.
Qed.
(* The Lindenbaum theory preserves derivability from the initial set of formulas. *)
Lemma der_nLind_theory_mLind_theory_le : forall n m Γ ψ φ,
(KMH_prv (nLind_theory Γ ψ n) φ) -> (le n m) ->
(KMH_prv (nLind_theory Γ ψ m) φ).
Proof.
intros. apply (KMH_monot _ _ H) ; auto.
intros C HC ; apply nLind_theory_extens_le with (n:=n) ; auto.
Qed.
Lemma der_Lind_theory_nLind_theory : forall Γ ψ A, KMH_prv (Lind_theory Γ ψ) A ->
exists n, KMH_prv (nLind_theory Γ ψ n) A.
Proof.
intros Γ ψ A D. remember (Lind_theory Γ ψ) as X. revert Γ ψ HeqX.
induction D ; cbn ; intros ; subst.
- destruct H as (n & Hn). exists n ; apply Id ; auto.
- exists 0 ; apply Ax ; auto.
- destruct (IHD2 Γ0 ψ) ; auto. destruct (IHD1 Γ0 ψ) ; auto.
exists (max x x0). eapply MP. apply der_nLind_theory_mLind_theory_le with x0.
exact H0. lia. apply der_nLind_theory_mLind_theory_le with x. exact H. lia.
- exists 0. apply Nec ; auto.
Qed.
(* Each step of the construction preserves underivability of the formula ψ. *)
Lemma Under_nLind_theory : forall n Γ ψ,
~ KMH_prv Γ ψ ->
~ KMH_prv (nLind_theory Γ ψ n) ψ.
Proof.
induction n ; intros ; cbn in * ; auto.
specialize (IHn _ _ H). intro.
apply IHn. unfold choice_code in *. unfold choice_form in *.
apply (KMH_monot _ _ H0).
intros a Ha ; cbn in Ha. unfold In in *. destruct Ha ; auto.
destruct H1. destruct H2 ; subst. exfalso.
apply H1. apply (KMH_monot _ _ H0).
intros a Ha ; cbn in Ha. unfold In in *. destruct Ha.
left ; auto. destruct H2 ; destruct H3 ; subst.
right ; apply In_singleton.
Qed.
(* The Lindenbaum theory does not derive ψ. *)
Lemma Under_Lind_theory: forall Γ ψ,
~ KMH_prv Γ ψ ->
~ KMH_prv (Lind_theory Γ ψ) ψ.
Proof.
intros Γ ψ Incl H.
destruct (der_Lind_theory_nLind_theory _ _ _ H).
pose (Under_nLind_theory x _ _ Incl H0). auto.
Qed.
(* The Lindenbaum theory is closed under derivation. *)
Lemma restr_closeder_Lind_theory : forall Γ ψ,
~ KMH_prv Γ ψ ->
closed (Lind_theory Γ ψ).
Proof.
intros Γ ψ H. intros A H0. unfold Lind_theory. exists (S (form_index A)). unfold In. cbn.
unfold choice_code. unfold choice_form. right. repeat split ; auto. 2: apply form_enum_index.
intro. eapply Under_Lind_theory ; auto. exact H.
eapply MP. 2: exact H0. apply KMH_Deduction_Theorem in H1.
apply (KMH_monot _ _ H1). intros C HC. exists (form_index A) ; auto.
Qed.
(* Not being in Lind_theory implies not being derivable from the theory. *)
Lemma not_In_Lind_theory_deriv : forall Γ ψ,
~ KMH_prv Γ ψ ->
forall A, Γ A -> ~ (Lind_theory Γ ψ A) ->
~~ KMH_prv (Union _ (Lind_theory Γ ψ) (Singleton _ A)) ψ.
Proof.
intros Γ ψ H A HA H0 H1. apply H0. exists (S (form_index A)).
cbn. unfold In. unfold choice_code. unfold choice_form ; cbn.
right. repeat split ; auto. 2: apply form_enum_index.
intro. apply H1. apply (KMH_monot _ _ H2). intros C HC. unfold In in *. inversion HC ; subst.
unfold In in *. left. exists (form_index A) ; auto. right ; auto.
Qed.
(* The Lindenbaum theory is quasi-prime. *)
Lemma quasi_prime_Lind_theory: forall Γ ψ,
~ KMH_prv Γ ψ ->
quasi_prime (Lind_theory Γ ψ).
Proof.
intros Γ ψ H0 a b Hor H1.
apply H1. left. exists (S (form_index a)). cbn.
unfold choice_code. unfold choice_form. unfold In.
right. repeat split ; auto. 2: apply form_enum_index.
intro. apply H1. right. exists (S (form_index b)). cbn.
subst. unfold choice_code. unfold choice_form. right. repeat split.
2: apply form_enum_index. intro.
pose (Under_Lind_theory Γ ψ H0). apply n.
eapply MP. eapply MP. eapply MP. apply Ax ; left ; eapply IA5 ; reflexivity.
apply KMH_Deduction_Theorem.
apply KMH_monot with (Γ1:=Union form (Lind_theory Γ ψ) (Singleton form a)) in H. exact H.
cbn ; intros c Hc. inversion Hc ; subst. apply Union_introl. unfold In. exists (form_index a) ; auto.
inversion H3 ; subst ; apply Union_intror ; apply In_singleton.
apply KMH_Deduction_Theorem.
apply KMH_monot with (Γ1:=Union form (Lind_theory Γ ψ) (Singleton form b)) in H2. exact H2.
cbn ; intros c Hc. inversion Hc ; subst. apply Union_introl. unfold In. exists (form_index b) ; auto.
inversion H3 ; subst ; apply Union_intror ; apply In_singleton.
apply Id ; auto.
Qed.
(* The Lindenbaum theory preserves consistency. *)
Lemma Consist_nLind_theory : forall n Γ ψ,
~ KMH_prv Γ ψ ->
~ KMH_prv (nLind_theory Γ ψ n) ⊥.
Proof.
intros n Γ ψ H H0. pose (Under_nLind_theory n Γ ψ H).
apply n0. eapply MP. apply EFQ. auto.
Qed.
Lemma Consist_Lind_theory : forall Γ ψ,
~ KMH_prv Γ ψ ->
~ KMH_prv (Lind_theory Γ ψ) ⊥.
Proof.
intros Γ ψ H0 H1.
pose (Under_Lind_theory Γ ψ H0). apply n. eapply MP.
apply EFQ. auto.
Qed.
End PrimeProps.
Section Lindenbaum_lemma.
(* Lindenbaum lemma. *)
Lemma Lindenbaum Γ ψ :
~ KMH_prv Γ ψ ->
{ Γm | Included _ Γ Γm
/\ closed Γm
/\ quasi_prime Γm
/\ ~ KMH_prv Γm ψ}.
Proof.
intros.
exists (Lind_theory Γ ψ).
repeat split.
- intro. apply Lind_theory_extens.
- apply restr_closeder_Lind_theory ; auto.
- pose quasi_prime_Lind_theory ; auto.
- intro. apply Under_Lind_theory in H0 ; auto.
Qed.
End Lindenbaum_lemma.
End General_Lind.
From Stdlib.Logic Require Import Description FunctionalExtensionality.
Export ListNotations.
Require Import syntax.
Require Import KMH.
Require Import logics.
Require Import properties.
Require Import enum.
Section General_Lind.
Section Sets_of_forms.
Definition SubTheory (Γ Δ: @Ensemble form) (Incl: Included _ Δ Γ) := forall φ, (KMH_prv Δ φ /\ In _ Γ φ) -> In _ Δ φ.
Definition closed Γ :=
forall φ, KMH_prv Γ φ -> Γ φ.
Definition prime (Γ : @Ensemble form) :=
forall φ ψ, Γ (Or φ ψ) -> Γ φ \/ Γ ψ.
Definition quasi_prime (Γ : @Ensemble form) :=
forall φ ψ, Γ (Or φ ψ) -> ~ ~ (Γ φ \/ Γ ψ).
End Sets_of_forms.
Section prelims.
Lemma prime_list_disj l Γ :
prime Γ -> Γ (list_disj l) -> exists A, (List.In A l \/ A = Bot) /\ Γ A.
Proof.
induction l ; cbn ; intros.
- exists Bot ; auto.
- destruct (H _ _ H0). exists a ; split ; auto. apply IHl in H1 ; auto.
destruct H1 as (A & [H2 | H2] & H3). exists A ; split ; auto. subst.
exists Bot ; split ; auto.
Qed.
Definition Theory Γ := closed Γ /\ prime Γ.
Definition AllForm := fun (A: form) => True.
Lemma Theory_AllForm : Theory AllForm.
Proof.
split.
- intros A HA. unfold AllForm ; auto.
- intros A B Hor. left ; unfold AllForm ; auto.
Qed.
End prelims.
Section Prime.
(* We define the step-by-step construction of the Lindenbaum extension. *)
Definition choice_form Γ ψ φ: Ensemble form :=
fun x => Γ x \/ (~ (KMH_prv (Union _ Γ (Singleton _ x)) ψ) /\ φ = x).
Definition choice_code Γ ψ (n :nat) : @Ensemble form := (choice_form Γ ψ (form_enum n)).
Fixpoint nLind_theory Γ ψ n : @Ensemble form :=
match n with
| 0 => Γ
| S m => choice_code (nLind_theory Γ ψ m) ψ m
end.
(* The Lindenbaum extension is then defined as follows. *)
Definition Lind_theory Γ ψ : @Ensemble form :=
fun x => (exists n, In _ (nLind_theory Γ ψ n) x).
End Prime.
Section PrimeProps.
(* The Lindenbaum theory is an extension of the initial set of formulas. *)
Lemma nLind_theory_extens : forall n Γ ψ φ,
In _ Γ φ -> In _ (nLind_theory Γ ψ n) φ.
Proof.
induction n.
- cbn. intros. unfold In. unfold choice_code. unfold choice_form. auto.
- cbn. intros. pose (IHn Γ ψ φ H). unfold choice_code.
unfold choice_form. cbn. unfold In ; auto.
Qed.
Lemma nLind_theory_extens_le : forall m n Γ ψ φ,
In _ (nLind_theory Γ ψ n) φ -> (le n m) -> In _ (nLind_theory Γ ψ m) φ.
Proof.
induction m.
- intros. cbn. inversion H0. subst. cbn in H. auto.
- intros. inversion H0.
+ subst. auto.
+ subst. cbn. unfold In. apply IHm in H ; auto. unfold choice_code.
unfold choice_form. unfold In ; auto.
Qed.
Lemma Lind_theory_extens : forall Γ ψ φ,
Γ φ -> In _ (Lind_theory Γ ψ) φ.
Proof.
intros. unfold Lind_theory. unfold In. exists 0. unfold nLind_theory.
unfold choice_code. unfold choice_form ; auto.
Qed.
(* The Lindenbaum theory preserves derivability from the initial set of formulas. *)
Lemma der_nLind_theory_mLind_theory_le : forall n m Γ ψ φ,
(KMH_prv (nLind_theory Γ ψ n) φ) -> (le n m) ->
(KMH_prv (nLind_theory Γ ψ m) φ).
Proof.
intros. apply (KMH_monot _ _ H) ; auto.
intros C HC ; apply nLind_theory_extens_le with (n:=n) ; auto.
Qed.
Lemma der_Lind_theory_nLind_theory : forall Γ ψ A, KMH_prv (Lind_theory Γ ψ) A ->
exists n, KMH_prv (nLind_theory Γ ψ n) A.
Proof.
intros Γ ψ A D. remember (Lind_theory Γ ψ) as X. revert Γ ψ HeqX.
induction D ; cbn ; intros ; subst.
- destruct H as (n & Hn). exists n ; apply Id ; auto.
- exists 0 ; apply Ax ; auto.
- destruct (IHD2 Γ0 ψ) ; auto. destruct (IHD1 Γ0 ψ) ; auto.
exists (max x x0). eapply MP. apply der_nLind_theory_mLind_theory_le with x0.
exact H0. lia. apply der_nLind_theory_mLind_theory_le with x. exact H. lia.
- exists 0. apply Nec ; auto.
Qed.
(* Each step of the construction preserves underivability of the formula ψ. *)
Lemma Under_nLind_theory : forall n Γ ψ,
~ KMH_prv Γ ψ ->
~ KMH_prv (nLind_theory Γ ψ n) ψ.
Proof.
induction n ; intros ; cbn in * ; auto.
specialize (IHn _ _ H). intro.
apply IHn. unfold choice_code in *. unfold choice_form in *.
apply (KMH_monot _ _ H0).
intros a Ha ; cbn in Ha. unfold In in *. destruct Ha ; auto.
destruct H1. destruct H2 ; subst. exfalso.
apply H1. apply (KMH_monot _ _ H0).
intros a Ha ; cbn in Ha. unfold In in *. destruct Ha.
left ; auto. destruct H2 ; destruct H3 ; subst.
right ; apply In_singleton.
Qed.
(* The Lindenbaum theory does not derive ψ. *)
Lemma Under_Lind_theory: forall Γ ψ,
~ KMH_prv Γ ψ ->
~ KMH_prv (Lind_theory Γ ψ) ψ.
Proof.
intros Γ ψ Incl H.
destruct (der_Lind_theory_nLind_theory _ _ _ H).
pose (Under_nLind_theory x _ _ Incl H0). auto.
Qed.
(* The Lindenbaum theory is closed under derivation. *)
Lemma restr_closeder_Lind_theory : forall Γ ψ,
~ KMH_prv Γ ψ ->
closed (Lind_theory Γ ψ).
Proof.
intros Γ ψ H. intros A H0. unfold Lind_theory. exists (S (form_index A)). unfold In. cbn.
unfold choice_code. unfold choice_form. right. repeat split ; auto. 2: apply form_enum_index.
intro. eapply Under_Lind_theory ; auto. exact H.
eapply MP. 2: exact H0. apply KMH_Deduction_Theorem in H1.
apply (KMH_monot _ _ H1). intros C HC. exists (form_index A) ; auto.
Qed.
(* Not being in Lind_theory implies not being derivable from the theory. *)
Lemma not_In_Lind_theory_deriv : forall Γ ψ,
~ KMH_prv Γ ψ ->
forall A, Γ A -> ~ (Lind_theory Γ ψ A) ->
~~ KMH_prv (Union _ (Lind_theory Γ ψ) (Singleton _ A)) ψ.
Proof.
intros Γ ψ H A HA H0 H1. apply H0. exists (S (form_index A)).
cbn. unfold In. unfold choice_code. unfold choice_form ; cbn.
right. repeat split ; auto. 2: apply form_enum_index.
intro. apply H1. apply (KMH_monot _ _ H2). intros C HC. unfold In in *. inversion HC ; subst.
unfold In in *. left. exists (form_index A) ; auto. right ; auto.
Qed.
(* The Lindenbaum theory is quasi-prime. *)
Lemma quasi_prime_Lind_theory: forall Γ ψ,
~ KMH_prv Γ ψ ->
quasi_prime (Lind_theory Γ ψ).
Proof.
intros Γ ψ H0 a b Hor H1.
apply H1. left. exists (S (form_index a)). cbn.
unfold choice_code. unfold choice_form. unfold In.
right. repeat split ; auto. 2: apply form_enum_index.
intro. apply H1. right. exists (S (form_index b)). cbn.
subst. unfold choice_code. unfold choice_form. right. repeat split.
2: apply form_enum_index. intro.
pose (Under_Lind_theory Γ ψ H0). apply n.
eapply MP. eapply MP. eapply MP. apply Ax ; left ; eapply IA5 ; reflexivity.
apply KMH_Deduction_Theorem.
apply KMH_monot with (Γ1:=Union form (Lind_theory Γ ψ) (Singleton form a)) in H. exact H.
cbn ; intros c Hc. inversion Hc ; subst. apply Union_introl. unfold In. exists (form_index a) ; auto.
inversion H3 ; subst ; apply Union_intror ; apply In_singleton.
apply KMH_Deduction_Theorem.
apply KMH_monot with (Γ1:=Union form (Lind_theory Γ ψ) (Singleton form b)) in H2. exact H2.
cbn ; intros c Hc. inversion Hc ; subst. apply Union_introl. unfold In. exists (form_index b) ; auto.
inversion H3 ; subst ; apply Union_intror ; apply In_singleton.
apply Id ; auto.
Qed.
(* The Lindenbaum theory preserves consistency. *)
Lemma Consist_nLind_theory : forall n Γ ψ,
~ KMH_prv Γ ψ ->
~ KMH_prv (nLind_theory Γ ψ n) ⊥.
Proof.
intros n Γ ψ H H0. pose (Under_nLind_theory n Γ ψ H).
apply n0. eapply MP. apply EFQ. auto.
Qed.
Lemma Consist_Lind_theory : forall Γ ψ,
~ KMH_prv Γ ψ ->
~ KMH_prv (Lind_theory Γ ψ) ⊥.
Proof.
intros Γ ψ H0 H1.
pose (Under_Lind_theory Γ ψ H0). apply n. eapply MP.
apply EFQ. auto.
Qed.
End PrimeProps.
Section Lindenbaum_lemma.
(* Lindenbaum lemma. *)
Lemma Lindenbaum Γ ψ :
~ KMH_prv Γ ψ ->
{ Γm | Included _ Γ Γm
/\ closed Γm
/\ quasi_prime Γm
/\ ~ KMH_prv Γm ψ}.
Proof.
intros.
exists (Lind_theory Γ ψ).
repeat split.
- intro. apply Lind_theory_extens.
- apply restr_closeder_Lind_theory ; auto.
- pose quasi_prime_Lind_theory ; auto.
- intro. apply Under_Lind_theory in H0 ; auto.
Qed.
End Lindenbaum_lemma.
End General_Lind.