Definition stable P := ~ ~ P -> P.
Lemma stable_equiv P Q :
P <-> Q -> stable P -> stable Q.
Proof.
firstorder.
Qed.
Definition stab_class := forall Sigma, @theory Sigma -> Prop.
Definition map_closed (S : stab_class) {Sig Sig'} (f : @form Sig -> @form Sig') := forall T, S Sig T -> S Sig' (tmap f T).
Definition ST (S : stab_class) := forall Sigma T phi, closed_T T -> closed phi -> S Sigma T -> stable (T ⊩CE phi).
Section PropT.
Definition dummy_sig : Signature := {| Funcs := False; Preds := False; pred_ar := @except nat ; fun_ar := @except nat |}.
Definition prop_T (P : Prop) := fun phi : @form dummy_sig => phi = ⊥ /\ P.
Lemma prop_T_correct P :
prop_T P ⊩CE ⊥ <-> P.
Proof.
split.
- intros ([ | x] & HA1 & HA2). 1: contradiction (Consistency HA2).
destruct (HA1 x (or_introl eq_refl)). firstorder.
- exists [⊥]; split. 2: ctx. now intros ? [<- | []].
Qed.
Global Instance False_enumT : enumT False.
Proof.
exists (fun _ => []). 1: auto. intros [].
Qed.
End PropT.
Section StabilityClasses.
(* **** Double Negation Elimination *)
Section DN.
Definition DN := forall P, stable P.
Definition any_T : stab_class := fun Σ _ => exists (HdF : eq_dec Funcs) (HdP : eq_dec Preds)
(HeF : enumT Funcs) (HeP : enumT Preds), True.
Definition ST__a := ST any_T.
Lemma any_T_map_closed {Sig Sig' : Signature} {HdF : eq_dec Funcs} {HdP : eq_dec Preds} {HeF : enumT Funcs} {HeP : enumT Preds} (f : @form Sig -> @form Sig') :
map_closed any_T f.
Proof.
intros ? _.
now exists HdF, HdP, HeF, HeP.
Qed.
Lemma dn_to_sta :
DN -> ST__a.
Proof.
intros dn Sig T phi _ clT clphi. apply dn.
Qed.
Lemma sta_to_dn :
ST__a -> DN.
Proof.
intros sta P. eapply stable_equiv. 1: apply (prop_T_correct P). apply sta.
- intros phi n [-> H]. econstructor.
- econstructor.
- exists _. eexists. intros []. cbn.
exists False_enumT, False_enumT. econstructor.
Qed.
End DN.
(* **** Synthetic Markov's Principle *)
Section SyntMP.
Definition tsat (f : nat -> bool) := exists n, f n = true.
Definition MP := forall f : nat -> bool, stable (tsat f).
Definition enum_T : stab_class := fun _ T => exists (HdF : eq_dec Funcs) (HdP : eq_dec Preds)
(HeF : enumT Funcs) (HeP : enumT Preds) L, enum T L.
Definition ST__e := ST enum_T.
Lemma enum_T_map_closed_closing {Sig : Signature} :
@map_closed enum_T Sig (sig_ext Sig) (fun phi => (sig_lift phi)[ext_c]).
Proof.
intros T (? & ? & ? & ? & L & He). exists (dec_sig_ext_Funcs _), (dec_sig_ext_Preds _).
exists (enumT_sig_ext_Funcs _), (enumT_sig_ext_Preds _), (L >> map (fun phi => (sig_lift phi)[ext_c])).
now apply enum_tmap.
Qed.
Lemma enum_T_map_closed_homo {Sig : Signature} (f : @form Sig -> @form Sig) :
map_closed enum_T f.
Proof.
intros T (HdF' & HdP' & HeF' & HeP' & L & He). exists HdF', HdP', HeF', HeP', (L >> map f).
now apply enum_tmap.
Qed.
Section MPEnum.
Hypothesis mp : MP.
Variable (X : Type) (L : nat -> list X) (P : X -> Prop).
Hypothesis (HL : enum P L) (HX : eq_dec X).
Lemma enumeration_semi_decidable x :
exists (f : nat -> bool), P x <-> tsat f.
Proof.
destruct HL as [_ H]. exists (fun n => if list_in_dec x (L n) HX then true else false).
split.
- intros [m ?] % H. exists m. now destruct (list_in_dec x (L m) HX).
- intros [m Hm]. destruct (list_in_dec x (L m) HX) in Hm. 2: discriminate. firstorder.
Qed.
Lemma enumeration_stability x :
stable (P x).
Proof.
intros Hn. destruct (enumeration_semi_decidable x) as [f Hf].
apply Hf. apply mp. intros Hf'. apply Hn. intros [m Hm] % Hf. apply Hf'. now exists m.
Qed.
End MPEnum.
Lemma mp_to_ste :
MP -> ST__e.
Proof.
intros mp Sig T phi clT clphi (? & ? & ? & ? & L & He). apply (enumeration_stability mp (enum_tprv He) (dec_form _ _)).
Qed.
Fixpoint L_tsat_T (f : nat -> bool) (n : nat) : list (@form dummy_sig) :=
match n with
| 0 => []
| S n => L_tsat_T f n ++ if f n then [⊥] else []
end.
Lemma enum_tsat_T (f : nat -> bool) :
enum (prop_T (tsat f)) (L_tsat_T f).
Proof.
split. 1: eauto. split.
- intros [-> [n H]]. exists (S n). cbn. rewrite H. now in_app 2.
- intros [n]. induction n in x, H |-*; cbn in *. 1: contradiction. inv_collect.
destruct (f n) eqn:Hf.
+ destruct H as [<- | []]. firstorder.
+ contradiction.
Qed.
Lemma ste_to_mp :
ST__e -> MP.
Proof.
intros ste f. eapply stable_equiv. 1: apply prop_T_correct.
apply ste.
- intros phi n [-> H]. econstructor.
- econstructor.
- unshelve eexists _, _, _, _, (L_tsat_T f); try exact _. apply (enum_tsat_T f).
Qed.
End SyntMP.
(* **** Object Markov's Principle *)
Section ObjMP.
Definition fin_T : stab_class := fun Sig T => exists (HdF : eq_dec Funcs) (HdP : eq_dec Preds)
(HeF : enumT Funcs) (HeP : enumT Preds) A, forall phi, phi ∈ T <-> phi el A.
Definition ST__f := ST fin_T.
Lemma fin_T_map_closed {Sig Sig'} {HdF : eq_dec Funcs} {HdP : eq_dec Preds} {HeF : enumT Funcs} {HeP : enumT Preds} (f : @form Sig -> @form Sig') :
map_closed fin_T f.
Proof.
intros T (_ & _ & _ & _ & A & HA).
exists HdF, HdP, HeF, HeP.
exists (map f A). intros phi. split.
- intros (psi & Hpsi1 % HA & <-). now apply in_map.
- intros (psi & <- & Hpsi) % in_map_iff. firstorder.
Qed.
Section ConT.
Context {Sigma : Signature}.
Context {HdF : eq_dec Funcs} {HdP : eq_dec Preds} {HeF : enumT Funcs} {HeP : enumT Preds}.
Context {p : peirce} {b : bottom}.
Definition con_T A : theory := fun phi => phi el A.
Lemma con_T_correct A phi :
con_T A ⊩ phi <-> A ⊢ phi.
Proof.
firstorder. apply (Weak H0). firstorder.
Qed.
Lemma fin_T_con_T A :
fin_T (con_T A).
Proof.
exists HdF, HdP, HeF, HeP.
firstorder.
Qed.
End ConT.
Lemma fin_T_to_context {Sig : Signature} T phi :
closed_T T -> fin_T T -> exists A, List.Forall closed A /\ (A ⊢CE phi <-> T ⊩CE phi).
Proof.
intros clT (_ & _ & _ & _ & A & HA). exists A. split; try split.
- eapply Forall_forall. intros ? ? % HA n. now eapply clT.
- intros; exists A; firstorder.
- intros (B & HB1 & HB2). apply (Weak HB2). firstorder.
Qed.
Lemma stf_to_st_context :
ST__f <-> (forall Sigma {HdF : eq_dec Funcs} {HdP : eq_dec Preds} {HeF : enumT Funcs} {HeP : enumT Preds} A (phi : @form Sigma), (List.Forall closed A) -> closed phi -> stable (A ⊢CE phi)).
Proof.
split.
- intros stf HdF HdP HeF HeP Sig A phi clA clphi. eapply stable_equiv. 1: eapply con_T_correct.
apply stf.
+ intros psi n Hpsi. eapply Forall_forall in clA. eapply clA. eassumption.
+ eassumption.
+ eapply fin_T_con_T.
- intros stc Sig T phi clT clphi HT. destruct (fin_T_to_context phi clT HT) as [A [clA HA]].
destruct HT as (HdF & HdP & HeF & HeP & HT).
eapply stable_equiv. apply HA. apply stc; eauto.
Qed.
End ObjMP.
End StabilityClasses.