FOcdint.FO_CDInt_completeness
Require Import FunctionalExtensionality.
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import Arith.
Require Import FO_CDInt_Syntax.
Require Import FO_CDInt_GHC.
Require Import FO_CDInt_logic.
Require Import FOCDIH_properties.
Require Import FO_CDInt_Stand_Lindenbaum_lem.
Require Import FO_CDInt_Up_Lindenbaum_lem.
Require Import FO_CDInt_Kripke_sem.
Section completeness.
Variable SLEM : forall P : Prop, P + ~ P.
Corollary LEM : forall P : Prop, P \/ ~ P.
Proof.
intro P ; destruct (SLEM P) ; auto.
Qed.
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.
Notation "x 'el' L" := (List.In x L) (at level 70).
Notation "T |- phi" := (FOCDIH_prv T phi) (at level 80).
Notation adj T phi := (fun psi => T psi \/ psi = phi).
(* Canonical model construction *)
Class cworlds : Type :=
{ cX : form -> Prop ;
cconsist : consist cX ;
cprime : prime cX ;
cded_clos : ded_clos cX ;
cex_henk : ex_henk cX ;
call_henk : all_henk cX }.
Coercion cX : cworlds >-> Funclass.
Instance universal_interp : interp term :=
{| i_func := func |}.
Lemma universal_interp_eval rho (t : term) : eval rho t = t `[rho].
Proof.
induction t using term_ind ; auto.
Qed.
Lemma universal_interp_eval0 n (t : Vector.t term n): (Vector.map (eval var) t) = t.
Proof.
pose (Vector.map_id term n t). assert (eval var = (fun x : term => x)).
{ apply functional_extensionality. intros. pose (universal_interp_eval var x).
rewrite subst_term_var in e0. auto. } rewrite H. auto.
Qed.
Program Instance Canon_model : kmodel term :=
{|
nodes := cworlds ;
reachable X Y := forall A, X A -> Y A ;
k_interp := universal_interp ;
k_P := fun C P v => C (atom P v)
|}.
Lemma cwTradLind : forall X A, closed_S X -> closed A -> ~ (FOCDIH_prv X A) ->
exists (cw : cworlds), ~ cw A /\ Included _ X cw.
Proof.
intros.
assert (~ pair_der X (Singleton _ A)).
{ intro. destruct H2 as (l & Hl0 & Hl1 & Hl2).
apply H1. apply forall_list_disj with l ; auto.
intros. apply Hl1 in H2. inversion H2 ; subst. apply
imp_Id_gen. }
eapply Stand_Lindenbaum_lemma_pair in H2 ; auto.
destruct H2. repeat destruct p.
epose (Build_cworlds x _ p0 d e a). exists c. split.
intro. apply n. exists [A]. repeat split.
apply NoDup_cons ; auto. apply NoDup_nil.
intros B HB. inversion HB ; subst. split.
inversion H3. cbn. eapply MP.
apply Ax ; eapply A3 ; reflexivity. apply Id ; auto.
intros B HB. apply i ; auto.
apply LEM.
apply form_enum_unused.
intros B HB. inversion HB ; subst ; auto.
Unshelve.
intro D. apply n.
exists [] ; cbn ; repeat split ; auto.
apply NoDup_nil. intros ; contradiction.
Qed.
Lemma cwUpLind : forall (cw : cworlds) A B, ~ (FOCDIH_prv (fun x => cw x \/ x = A) B) ->
exists (cw' : cworlds), (forall C, cw C \/ C = A -> cw' C) /\ ~ (cw' B).
Proof.
intros cw A B H.
eapply Up_Lindenbaum_lemma in H ; auto. destruct H ; repeat destruct p.
epose (Build_cworlds x _ p d e a). exists c0. split ; auto.
intros. destruct H ; subst ; auto. apply x0 ; auto.
apply cconsist. apply cprime. apply cded_clos. apply cex_henk. apply call_henk.
Unshelve. auto.
Qed.
Lemma truth_lemma : forall A (cw : cworlds),
(ksat cw var A) <-> (cw A).
Proof.
pose (form_ind_subst (fun x => forall (cw : cworlds), ksat cw var x <-> cw x)).
apply i ; clear i ; auto.
(* ⊥ *)
- intros cw. split ; intro.
* inversion H.
* simpl in *. apply cconsist. apply Id ; auto.
(* atom *)
- intros P t cw. split ; intros ; simpl in * ; [ rewrite universal_interp_eval0 in H ; auto | rewrite universal_interp_eval0 ; auto].
(* Binary connectives *)
- intros b f1 IHf1 f2 IHf2 cw. destruct b ; simpl in *.
(* f1 ∧ f2 *)
* split ; intro.
+ destruct H. rewrite IHf1 in H. rewrite IHf2 in H0. apply cded_clos.
eapply MP. eapply MP. eapply MP. apply Ax ; eapply A8 ; reflexivity.
apply imp_Id_gen. eapply MP. apply Thm_irrel. all: apply Id ; auto.
+ split.
apply IHf1. apply cded_clos. eapply MP. apply Ax ; eapply A6 ; reflexivity.
apply Id ; exact H.
apply IHf2. apply cded_clos. eapply MP. apply Ax ; eapply A7 ; reflexivity.
apply Id ; exact H.
(* f1 ∨ f2 *)
* split ; intro.
+ destruct H.
rewrite IHf1 in H. apply cded_clos.
eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id ; auto.
rewrite IHf2 in H. apply cded_clos.
eapply MP. apply Ax ; eapply A4 ; reflexivity. apply Id ; auto.
+ apply cprime in H. rewrite IHf1 ; rewrite IHf2 ; auto.
(* f1 --> f2 *)
* split ; intro.
+ destruct (LEM (cw (f1 --> f2))) ; auto. exfalso.
assert ((FOCDIH_prv (Union _ cw (Singleton _ f1)) f2) -> False).
intro. eapply FOCDIH_Deduction_Theorem in H1 ; simpl ; auto. apply H0.
apply cded_clos ; auto.
pose (cwUpLind cw f1 f2). destruct e.
intro. apply H1. eapply (FOCDIH_monot _ _ H2). intros A HA. inversion HA.
apply Union_introl ; auto. subst. apply Union_intror ; apply In_singleton.
destruct H2. apply H3. apply IHf2 ; auto. apply H ; auto. apply IHf1 ; auto.
+ intros. apply IHf2. apply IHf1 in H1. apply cded_clos.
eapply MP. apply Id ; apply H0 ; exact H. apply Id ; auto.
(* Quantifiers *)
- destruct q.
(* Universal *)
* split ; intros.
+ apply all_henk'. apply LEM. apply call_henk. intros. apply H. apply ksat_comp. apply ksat_ext with (rho:= ($c)..) ; auto.
intros. unfold funcomp. unfold scons. destruct x. pose (subst_term_var ($c)) ; auto. simpl. auto.
+ simpl. intros. assert (In form cw f2[j..]). apply cded_clos.
eapply MP. apply Ax ; eapply QA2 ; reflexivity. apply Id ; auto.
apply H in H1. apply ksat_comp in H1. apply ksat_ext with (rho:= j..) in H1 ; auto.
intros. destruct x ; auto. cbn. pose (subst_term_var j). rewrite universal_interp_eval. auto.
(* Existential *)
* split ; intros.
+ destruct H0. apply ksat_ext with (rho:= (x.. >> eval var)) in H0. apply ksat_comp in H0.
apply H in H0. apply cded_clos.
eapply MP. apply Ax ; eapply QA3 ; reflexivity. apply Id ; exact H0.
intros. destruct x0 ; auto. cbn. pose (subst_term_var x). rewrite universal_interp_eval. auto.
+ simpl. apply cex_henk in H0. destruct H0. exists ($x). apply H in c.
apply ksat_comp in c. apply ksat_ext with (rho:= $x..) in c ; auto.
intros. destruct x0 ; auto.
Qed.
Theorem quasi_completeness : forall X A, closed_S X -> closed A -> ~ FOCDIH_prv X A -> ~ loc_conseq X A.
Proof.
intros X A cstS cstf notder csq. apply cwTradLind in notder as [cw H] ; auto. destruct H.
apply H. apply truth_lemma. apply csq.
intros. apply truth_lemma ; apply H0 ; auto.
Qed.
Theorem Completeness : forall X A, closed_S X -> closed A ->
loc_conseq X A -> FOCDIH_prv X A.
Proof.
intros X A cstS cstf csq. destruct (SLEM (X |- A)) ; [auto | exfalso].
apply quasi_completeness in n ; auto.
Qed.
Print Assumptions Completeness.
End completeness.
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import Arith.
Require Import FO_CDInt_Syntax.
Require Import FO_CDInt_GHC.
Require Import FO_CDInt_logic.
Require Import FOCDIH_properties.
Require Import FO_CDInt_Stand_Lindenbaum_lem.
Require Import FO_CDInt_Up_Lindenbaum_lem.
Require Import FO_CDInt_Kripke_sem.
Section completeness.
Variable SLEM : forall P : Prop, P + ~ P.
Corollary LEM : forall P : Prop, P \/ ~ P.
Proof.
intro P ; destruct (SLEM P) ; auto.
Qed.
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.
Notation "x 'el' L" := (List.In x L) (at level 70).
Notation "T |- phi" := (FOCDIH_prv T phi) (at level 80).
Notation adj T phi := (fun psi => T psi \/ psi = phi).
(* Canonical model construction *)
Class cworlds : Type :=
{ cX : form -> Prop ;
cconsist : consist cX ;
cprime : prime cX ;
cded_clos : ded_clos cX ;
cex_henk : ex_henk cX ;
call_henk : all_henk cX }.
Coercion cX : cworlds >-> Funclass.
Instance universal_interp : interp term :=
{| i_func := func |}.
Lemma universal_interp_eval rho (t : term) : eval rho t = t `[rho].
Proof.
induction t using term_ind ; auto.
Qed.
Lemma universal_interp_eval0 n (t : Vector.t term n): (Vector.map (eval var) t) = t.
Proof.
pose (Vector.map_id term n t). assert (eval var = (fun x : term => x)).
{ apply functional_extensionality. intros. pose (universal_interp_eval var x).
rewrite subst_term_var in e0. auto. } rewrite H. auto.
Qed.
Program Instance Canon_model : kmodel term :=
{|
nodes := cworlds ;
reachable X Y := forall A, X A -> Y A ;
k_interp := universal_interp ;
k_P := fun C P v => C (atom P v)
|}.
Lemma cwTradLind : forall X A, closed_S X -> closed A -> ~ (FOCDIH_prv X A) ->
exists (cw : cworlds), ~ cw A /\ Included _ X cw.
Proof.
intros.
assert (~ pair_der X (Singleton _ A)).
{ intro. destruct H2 as (l & Hl0 & Hl1 & Hl2).
apply H1. apply forall_list_disj with l ; auto.
intros. apply Hl1 in H2. inversion H2 ; subst. apply
imp_Id_gen. }
eapply Stand_Lindenbaum_lemma_pair in H2 ; auto.
destruct H2. repeat destruct p.
epose (Build_cworlds x _ p0 d e a). exists c. split.
intro. apply n. exists [A]. repeat split.
apply NoDup_cons ; auto. apply NoDup_nil.
intros B HB. inversion HB ; subst. split.
inversion H3. cbn. eapply MP.
apply Ax ; eapply A3 ; reflexivity. apply Id ; auto.
intros B HB. apply i ; auto.
apply LEM.
apply form_enum_unused.
intros B HB. inversion HB ; subst ; auto.
Unshelve.
intro D. apply n.
exists [] ; cbn ; repeat split ; auto.
apply NoDup_nil. intros ; contradiction.
Qed.
Lemma cwUpLind : forall (cw : cworlds) A B, ~ (FOCDIH_prv (fun x => cw x \/ x = A) B) ->
exists (cw' : cworlds), (forall C, cw C \/ C = A -> cw' C) /\ ~ (cw' B).
Proof.
intros cw A B H.
eapply Up_Lindenbaum_lemma in H ; auto. destruct H ; repeat destruct p.
epose (Build_cworlds x _ p d e a). exists c0. split ; auto.
intros. destruct H ; subst ; auto. apply x0 ; auto.
apply cconsist. apply cprime. apply cded_clos. apply cex_henk. apply call_henk.
Unshelve. auto.
Qed.
Lemma truth_lemma : forall A (cw : cworlds),
(ksat cw var A) <-> (cw A).
Proof.
pose (form_ind_subst (fun x => forall (cw : cworlds), ksat cw var x <-> cw x)).
apply i ; clear i ; auto.
(* ⊥ *)
- intros cw. split ; intro.
* inversion H.
* simpl in *. apply cconsist. apply Id ; auto.
(* atom *)
- intros P t cw. split ; intros ; simpl in * ; [ rewrite universal_interp_eval0 in H ; auto | rewrite universal_interp_eval0 ; auto].
(* Binary connectives *)
- intros b f1 IHf1 f2 IHf2 cw. destruct b ; simpl in *.
(* f1 ∧ f2 *)
* split ; intro.
+ destruct H. rewrite IHf1 in H. rewrite IHf2 in H0. apply cded_clos.
eapply MP. eapply MP. eapply MP. apply Ax ; eapply A8 ; reflexivity.
apply imp_Id_gen. eapply MP. apply Thm_irrel. all: apply Id ; auto.
+ split.
apply IHf1. apply cded_clos. eapply MP. apply Ax ; eapply A6 ; reflexivity.
apply Id ; exact H.
apply IHf2. apply cded_clos. eapply MP. apply Ax ; eapply A7 ; reflexivity.
apply Id ; exact H.
(* f1 ∨ f2 *)
* split ; intro.
+ destruct H.
rewrite IHf1 in H. apply cded_clos.
eapply MP. apply Ax ; eapply A3 ; reflexivity. apply Id ; auto.
rewrite IHf2 in H. apply cded_clos.
eapply MP. apply Ax ; eapply A4 ; reflexivity. apply Id ; auto.
+ apply cprime in H. rewrite IHf1 ; rewrite IHf2 ; auto.
(* f1 --> f2 *)
* split ; intro.
+ destruct (LEM (cw (f1 --> f2))) ; auto. exfalso.
assert ((FOCDIH_prv (Union _ cw (Singleton _ f1)) f2) -> False).
intro. eapply FOCDIH_Deduction_Theorem in H1 ; simpl ; auto. apply H0.
apply cded_clos ; auto.
pose (cwUpLind cw f1 f2). destruct e.
intro. apply H1. eapply (FOCDIH_monot _ _ H2). intros A HA. inversion HA.
apply Union_introl ; auto. subst. apply Union_intror ; apply In_singleton.
destruct H2. apply H3. apply IHf2 ; auto. apply H ; auto. apply IHf1 ; auto.
+ intros. apply IHf2. apply IHf1 in H1. apply cded_clos.
eapply MP. apply Id ; apply H0 ; exact H. apply Id ; auto.
(* Quantifiers *)
- destruct q.
(* Universal *)
* split ; intros.
+ apply all_henk'. apply LEM. apply call_henk. intros. apply H. apply ksat_comp. apply ksat_ext with (rho:= ($c)..) ; auto.
intros. unfold funcomp. unfold scons. destruct x. pose (subst_term_var ($c)) ; auto. simpl. auto.
+ simpl. intros. assert (In form cw f2[j..]). apply cded_clos.
eapply MP. apply Ax ; eapply QA2 ; reflexivity. apply Id ; auto.
apply H in H1. apply ksat_comp in H1. apply ksat_ext with (rho:= j..) in H1 ; auto.
intros. destruct x ; auto. cbn. pose (subst_term_var j). rewrite universal_interp_eval. auto.
(* Existential *)
* split ; intros.
+ destruct H0. apply ksat_ext with (rho:= (x.. >> eval var)) in H0. apply ksat_comp in H0.
apply H in H0. apply cded_clos.
eapply MP. apply Ax ; eapply QA3 ; reflexivity. apply Id ; exact H0.
intros. destruct x0 ; auto. cbn. pose (subst_term_var x). rewrite universal_interp_eval. auto.
+ simpl. apply cex_henk in H0. destruct H0. exists ($x). apply H in c.
apply ksat_comp in c. apply ksat_ext with (rho:= $x..) in c ; auto.
intros. destruct x0 ; auto.
Qed.
Theorem quasi_completeness : forall X A, closed_S X -> closed A -> ~ FOCDIH_prv X A -> ~ loc_conseq X A.
Proof.
intros X A cstS cstf notder csq. apply cwTradLind in notder as [cw H] ; auto. destruct H.
apply H. apply truth_lemma. apply csq.
intros. apply truth_lemma ; apply H0 ; auto.
Qed.
Theorem Completeness : forall X A, closed_S X -> closed A ->
loc_conseq X A -> FOCDIH_prv X A.
Proof.
intros X A cstS cstf csq. destruct (SLEM (X |- A)) ; [auto | exfalso].
apply quasi_completeness in n ; auto.
Qed.
Print Assumptions Completeness.
End completeness.