CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr
Require Import List.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_soundness_constr.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_enum.
Require Import CPP_BiInt_Lindenbaum_lem_prelim.
Require Import CPP_BiInt_Lindenbaum_lem.
Require Import CPP_BiInt_quasi_completeness_constr.
Require Import Coq.Arith.Cantor.
Definition MP :=
forall f : nat -> bool, ~ ~ (exists n, f n = true) -> exists n, f n = true.
Definition semidec {X} (p : X -> Prop) :=
exists f : X -> nat -> bool, forall x, p x <-> exists n, f x n = true.
Definition enum {X} (p : X -> Prop) :=
exists f : nat -> option X, forall x, p x <-> exists n, f n = Some x.
Definition SemidecCompleteness :=
forall Γ A, semidec Γ -> loc_conseq Γ A -> BIH_rules (Γ, A).
Section SemDec_Completeness.
Variable MPax : MP.
Lemma MP_stable {X} (p : X -> Prop) :
semidec p -> forall x, ~ ~ p x -> p x.
Proof.
intros [f Hf] x. rewrite Hf. apply MPax.
Qed.
Lemma semidec_enum (p : BPropF -> Prop) :
semidec p <-> enum p.
Proof.
split; intros [f Hf].
- exists (fun n => let (k, l) := of_nat n in if f (form_enum k) l then Some (form_enum k) else None).
intros A. rewrite Hf. split; intros [n Hn].
+ destruct (form_enum_sur A) as [l <-]. exists (to_nat (l, n)).
rewrite cancel_of_to. now rewrite Hn.
+ destruct of_nat. destruct f eqn : Hn0; try discriminate. exists n1. congruence.
- exists (fun x n => match f n with Some A => if eq_dec_form A x then true else false | None => false end).
intros A. rewrite Hf. split; intros [n Hn]; exists n.
+ rewrite Hn. destruct eq_dec_form; tauto.
+ destruct f; try discriminate. destruct eq_dec_form; try discriminate. now rewrite e.
Qed.
Theorem SemidecCompleteness_MP_WDNS :
SemidecCompleteness.
Proof.
intros Gamma A HG H.
assert (HN : ~ ~ BIH_rules (Gamma, A)).
- intros H'. now apply Quasi_completeness in H'.
- pattern A. apply MP_stable; trivial.
apply semidec_enum. apply semidec_enum in HG as [f Hf].
exists (fun n => form_enum_ded n f). intros B.
rewrite <- form_enum_ded_spec.
split; intros H'; eapply BIH_monot in H'; try apply H'; intros C; apply Hf.
Qed.
End SemDec_Completeness.
(* Reformulation of BIH_finite *)
Definition fromlist {X} (L : list X) : Ensemble X :=
fun x => List.In x L.
Lemma BIH_finite' T A :
BIH_rules (T, A) -> exists L : list (BPropF), (forall B, List.In B L -> T B) /\ BIH_rules (fromlist L, A).
Proof.
intros [T'[H1[H2[L HL]]]] % BIH_finite. cbn in *. exists L. split.
- intros B HB. apply H1, HL, HB.
- eapply (BIH_monot (T', A)); trivial. cbn. intros B HB. apply HL, HB.
Qed.
(* Consistency *)
#[export] Instance point_model :
model.
Proof.
unshelve econstructor.
- exact unit.
- exact (fun _ _ => True).
- exact (fun _ _ => True).
- split; auto.
- cbn. trivial.
- intuition.
Defined.
Lemma point_model_dec :
model_dec point_model.
Proof.
intros [] A. induction A; cbn; try now intuition.
- destruct IHA1, IHA2.
+ left. now intros [].
+ right. firstorder.
+ left. now intros [].
+ left. now intros [].
- destruct IHA1, IHA2.
+ right. intro. apply H1. intros. destruct v ; auto.
+ left. intro. auto.
+ right. intro. apply H1. intros. destruct v ; auto.
+ right. intro. apply H1. intros. destruct v ; auto. exfalso ; auto.
Qed.
Lemma consistency :
~ BIH_rules (fromlist [], Bot).
Proof.
intros H % wSoundness_dec. cbn in H. destruct (H point_model tt).
- apply point_model_dec.
- intros A [].
Qed.
(* Completeness restricted to semi-decidable theories implies MP *)
Section MP.
Theorem SemidecCompleteness_MP :
SemidecCompleteness -> MP.
Proof.
intros HC f HF. assert (H : loc_conseq (fun A => exists n, f n = true) (Bot)).
- intros M w H. cbn.
apply HF. intros HF'. apply (H (Bot)). apply HF'.
- apply HC in H.
+ apply BIH_finite' in H as [L[H1 H2]]. destruct L as [|A L].
* now apply consistency in H2.
* apply (H1 A). now left.
+ exists (fun _ => f). reflexivity.
Qed.
End MP.
Print Assumptions SemidecCompleteness_MP.
Export ListNotations.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_Kripke_sem_constr.
Require Import CPP_BiInt_soundness_constr.
Require Import CPP_BiInt_meta_interactions1.
Require Import CPP_BiInt_meta_interactions2.
Require Import CPP_BiInt_enum.
Require Import CPP_BiInt_Lindenbaum_lem_prelim.
Require Import CPP_BiInt_Lindenbaum_lem.
Require Import CPP_BiInt_quasi_completeness_constr.
Require Import Coq.Arith.Cantor.
Definition MP :=
forall f : nat -> bool, ~ ~ (exists n, f n = true) -> exists n, f n = true.
Definition semidec {X} (p : X -> Prop) :=
exists f : X -> nat -> bool, forall x, p x <-> exists n, f x n = true.
Definition enum {X} (p : X -> Prop) :=
exists f : nat -> option X, forall x, p x <-> exists n, f n = Some x.
Definition SemidecCompleteness :=
forall Γ A, semidec Γ -> loc_conseq Γ A -> BIH_rules (Γ, A).
Section SemDec_Completeness.
Variable MPax : MP.
Lemma MP_stable {X} (p : X -> Prop) :
semidec p -> forall x, ~ ~ p x -> p x.
Proof.
intros [f Hf] x. rewrite Hf. apply MPax.
Qed.
Lemma semidec_enum (p : BPropF -> Prop) :
semidec p <-> enum p.
Proof.
split; intros [f Hf].
- exists (fun n => let (k, l) := of_nat n in if f (form_enum k) l then Some (form_enum k) else None).
intros A. rewrite Hf. split; intros [n Hn].
+ destruct (form_enum_sur A) as [l <-]. exists (to_nat (l, n)).
rewrite cancel_of_to. now rewrite Hn.
+ destruct of_nat. destruct f eqn : Hn0; try discriminate. exists n1. congruence.
- exists (fun x n => match f n with Some A => if eq_dec_form A x then true else false | None => false end).
intros A. rewrite Hf. split; intros [n Hn]; exists n.
+ rewrite Hn. destruct eq_dec_form; tauto.
+ destruct f; try discriminate. destruct eq_dec_form; try discriminate. now rewrite e.
Qed.
Theorem SemidecCompleteness_MP_WDNS :
SemidecCompleteness.
Proof.
intros Gamma A HG H.
assert (HN : ~ ~ BIH_rules (Gamma, A)).
- intros H'. now apply Quasi_completeness in H'.
- pattern A. apply MP_stable; trivial.
apply semidec_enum. apply semidec_enum in HG as [f Hf].
exists (fun n => form_enum_ded n f). intros B.
rewrite <- form_enum_ded_spec.
split; intros H'; eapply BIH_monot in H'; try apply H'; intros C; apply Hf.
Qed.
End SemDec_Completeness.
(* Reformulation of BIH_finite *)
Definition fromlist {X} (L : list X) : Ensemble X :=
fun x => List.In x L.
Lemma BIH_finite' T A :
BIH_rules (T, A) -> exists L : list (BPropF), (forall B, List.In B L -> T B) /\ BIH_rules (fromlist L, A).
Proof.
intros [T'[H1[H2[L HL]]]] % BIH_finite. cbn in *. exists L. split.
- intros B HB. apply H1, HL, HB.
- eapply (BIH_monot (T', A)); trivial. cbn. intros B HB. apply HL, HB.
Qed.
(* Consistency *)
#[export] Instance point_model :
model.
Proof.
unshelve econstructor.
- exact unit.
- exact (fun _ _ => True).
- exact (fun _ _ => True).
- split; auto.
- cbn. trivial.
- intuition.
Defined.
Lemma point_model_dec :
model_dec point_model.
Proof.
intros [] A. induction A; cbn; try now intuition.
- destruct IHA1, IHA2.
+ left. now intros [].
+ right. firstorder.
+ left. now intros [].
+ left. now intros [].
- destruct IHA1, IHA2.
+ right. intro. apply H1. intros. destruct v ; auto.
+ left. intro. auto.
+ right. intro. apply H1. intros. destruct v ; auto.
+ right. intro. apply H1. intros. destruct v ; auto. exfalso ; auto.
Qed.
Lemma consistency :
~ BIH_rules (fromlist [], Bot).
Proof.
intros H % wSoundness_dec. cbn in H. destruct (H point_model tt).
- apply point_model_dec.
- intros A [].
Qed.
(* Completeness restricted to semi-decidable theories implies MP *)
Section MP.
Theorem SemidecCompleteness_MP :
SemidecCompleteness -> MP.
Proof.
intros HC f HF. assert (H : loc_conseq (fun A => exists n, f n = true) (Bot)).
- intros M w H. cbn.
apply HF. intros HF'. apply (H (Bot)). apply HF'.
- apply HC in H.
+ apply BIH_finite' in H as [L[H1 H2]]. destruct L as [|A L].
* now apply consistency in H2.
* apply (H1 A). now left.
+ exists (fun _ => f). reflexivity.
Qed.
End MP.
Print Assumptions SemidecCompleteness_MP.