Require Import List Lia.
From Undecidability.FOL.Util Require Import Syntax Syntax_facts FullTarski FullTarski_facts FullDeduction_facts FullDeduction.
Import Vector.VectorNotations.
Notation "I ⊨= phi" := (forall rho, sat I rho phi) (at level 20).
Notation "I ⊨=T T" := (forall psi, T psi -> I ⊨= psi) (at level 20).
Notation "I ⊫= Gamma" := (forall rho psi, In psi Gamma -> sat I rho psi) (at level 20).
Section Signature.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Inductive new_preds : Type :=
Q_ : new_preds
| old_preds (P : Σ_preds) : new_preds.
Definition new_preds_ar (P : new_preds) :=
match P with
| Q_ => 0
| old_preds P => ar_preds P
end.
Existing Instance Σ_funcs.
Instance extended_preds : preds_signature :=
{| preds := new_preds ; ar_preds := new_preds_ar |}.
Definition extend_interp {D} :
@interp Σ_funcs Σ_preds D -> Prop -> interp D.
Proof.
intros I Q. split.
- exact (@i_func _ _ _ I).
- intros P. destruct P as [|P0] eqn:?.
+ intros _. exact Q.
+ exact (@i_atom _ _ _ I P0).
Defined.
Definition Q := (@atom Σ_funcs extended_preds _ falsity_off Q_ ([])).
Definition dn {ff} F phi : @form Σ_funcs extended_preds _ ff :=
(phi ~> F) ~> F.
Fixpoint cast {ff} (phi : @form Σ_funcs Σ_preds _ ff) : @form Σ_funcs extended_preds _ falsity_off :=
match phi with
| falsity => Q
| atom P v => (@atom _ _ _ falsity_off (old_preds P) v)
| bin b phi psi => bin b (cast phi) (cast psi)
| quant q phi => quant q (cast phi)
end.
Fixpoint Fr {ff} (phi : @form Σ_funcs Σ_preds _ ff) : @form Σ_funcs extended_preds _ falsity_off :=
match phi with
| falsity => Q
| atom P v => dn Q (@atom _ _ _ falsity_off (old_preds P) v)
| bin Impl phi psi => (Fr phi) ~> (Fr psi)
| bin Conj phi psi => (Fr phi) ∧ (Fr psi)
| bin Disj phi psi => dn Q ((Fr phi) ∨ (Fr psi))
| quant All phi => ∀ (Fr phi)
| quant Ex phi => dn Q (∃ (Fr phi))
end.
Definition Fr_ {ff} Gamma := map (@Fr ff) Gamma.
Fact subst_Fr {ff} (phi : @form Σ_funcs Σ_preds _ ff) sigma:
subst_form sigma (Fr phi) = Fr (subst_form sigma phi).
Proof.
revert sigma.
induction phi; cbn.
- reflexivity.
- now unfold dn.
- destruct b0; cbn; unfold dn, Q; congruence.
- destruct q; cbn; intros sigma; unfold dn, Q; congruence.
Qed.
Fact subst_Fr_ {ff} L sigma :
map (subst_form sigma) (map (@Fr ff) L) = map Fr (map (subst_form sigma) L).
Proof.
induction L.
- reflexivity.
- cbn. now rewrite IHL, subst_Fr.
Qed.
Lemma double_dn Gamma F phi :
Gamma ⊢M dn F (dn F phi) ~> dn F phi.
Proof.
apply II, II. eapply IE with (phi0:= _ ~> _). { apply Ctx; firstorder. }
apply II. apply IE with (phi0:= phi ~> F). all: apply Ctx; auto.
Qed.
Lemma rm_dn Gamma F alpha beta :
(alpha :: Gamma) ⊢M beta -> (dn F alpha :: Gamma) ⊢I dn F beta.
Proof.
intros H.
apply II. eapply IE with (phi:= _ ~> _). { apply Ctx; firstorder. }
apply II. eapply IE with (phi:= beta). {apply Ctx; auto. }
eapply Weak; [eassumption|auto].
Qed.
Lemma form_up_var0_invar {ff} (phi : @form _ _ _ ff) :
phi[up ↑][$0..] = phi.
Proof.
cbn. repeat setoid_rewrite subst_comp.
rewrite <-(subst_var phi) at 2.
apply subst_ext. intros n. unfold funcomp. cbn.
change ((up (fun x : nat => $(S x)) n)) with ($n`[up ↑]).
rewrite subst_term_comp.
apply subst_term_id. now intros [].
Qed.
Lemma dn_forall {F} Gamma phi :
F[↑] = F -> Gamma ⊢M dn F (∀ phi) ~> ∀ dn F phi.
Proof.
intros HF.
apply II. constructor. apply II. cbn.
change ((∀ phi[up ↑])) with ((∀ phi)[↑]).
rewrite !HF.
eapply IE with (phi0:= _ ~> _). { apply Ctx; auto. }
apply II. eapply IE with (phi0:= phi). { apply Ctx; auto. }
cbn. rewrite <-form_up_var0_invar.
apply AllE, Ctx; auto.
Qed.
Fixpoint exist_times' {ff} N (phi : form ff) :=
match N with
0 => phi
| S n => ∃ exist_times' n phi
end.
Lemma exist_dn phi Gamma:
Gamma ⊢M ((∃ (dn Q phi)) ~> dn Q (∃ phi)).
Proof.
apply II, II. eapply ExE. {apply Ctx; auto. }
cbn; fold Q. apply IE with (phi0:= phi ~> Q).
{apply Ctx; auto. }
apply II. eapply IE with (phi0:= ∃ _).
{apply Ctx; auto. }
eapply ExI. rewrite form_up_var0_invar.
apply Ctx; auto.
Qed.
Lemma DNE_Fr {ff} :
forall phi Gamma, Gamma ⊢M dn Q (Fr phi) ~> @Fr ff phi.
Proof.
refine (size_ind size _ _). intros phi sRec.
destruct phi; intros Gamma; unfold dn.
- apply II. eapply IE; cbn. { apply Ctx; auto. }
apply II, Ctx; auto.
- apply double_dn.
- destruct b0; cbn.
+ apply II, CI.
* eapply IE. apply sRec; cbn. 1: lia.
apply rm_dn. eapply CE1, Ctx; auto.
* eapply IE. apply sRec; cbn. 1: lia.
apply rm_dn. eapply CE2, Ctx; auto.
+ apply double_dn.
+ apply II, II. eapply IE. apply sRec; cbn. 1: lia.
apply II. eapply IE with (phi:= _ ~> _). { apply Ctx; auto. }
apply II. eapply IE with (phi:= Fr phi2). { apply Ctx; auto. }
eapply IE with (phi:= Fr phi1); apply Ctx; auto.
- destruct q.
+ cbn. apply II. apply IE with (phi0:= ∀ dn Q (Fr phi)).
{ apply II. constructor. cbn; fold Q.
eapply IE. apply sRec; auto.
rewrite <-form_up_var0_invar.
apply AllE, Ctx; auto. }
constructor.
cbn; fold Q. rewrite <- form_up_var0_invar.
apply AllE. cbn; fold Q.
now apply imps, dn_forall.
+ apply double_dn.
Qed.
Lemma Peirce_Fr {ff} Gamma phi psi : Gamma ⊢M @Fr ff (((phi ~> psi) ~> phi) ~> phi).
Proof.
eapply IE. apply DNE_Fr. cbn.
apply II. eapply IE. { apply Ctx; auto. }
apply II. eapply IE. { apply Ctx; auto. }
apply II. eapply IE. apply DNE_Fr. cbn; fold Q.
apply II. eapply IE with (phi0:= _ ~> _). {apply Ctx; auto. }
apply II, Ctx; auto.
Qed.
Theorem Fr_cl_to_min {ff} Gamma phi :
Gamma ⊢C phi -> (@Fr_ ff Gamma) ⊢M Fr phi.
Proof.
induction 1; unfold Fr_ in *; cbn in *.
- now constructor.
- econstructor; eassumption.
- constructor. now rewrite subst_Fr_.
- eapply AllE with (t0:=t) in IHprv.
now rewrite subst_Fr in IHprv.
- apply II.
eapply IE.
+ apply Ctx. firstorder.
+ apply Weak with (A0 := map Fr A); [|auto].
apply ExI with (t0:=t). now rewrite subst_Fr.
- eapply IE. apply DNE_Fr. unfold dn in *; cbn.
apply II. eapply IE.
{ eapply Weak; [apply IHprv1|auto]. }
apply II. eapply IE. { apply Ctx; auto. }
rewrite <-subst_Fr, <-subst_Fr_ in IHprv2.
eapply ExE. { apply Ctx; auto. }
cbn. eapply Weak; [apply IHprv2|auto].
- specialize (DNE_Fr phi (map Fr A)) as H'.
eapply IE; [eassumption|].
cbn; apply II. eapply Weak; eauto.
- now apply Ctx, in_map.
- now apply CI.
- eapply CE1; eauto.
- eapply CE2; eauto.
- apply II. eapply IE.
+ apply Ctx. auto.
+ apply DI1. eapply Weak; eauto.
- apply II. eapply IE.
+ apply Ctx; auto.
+ apply DI2. eapply Weak; eauto.
- eapply IE. apply DNE_Fr.
apply II. eapply IE.
{ eapply Weak; [apply IHprv1|auto]. }
apply II. eapply IE. { apply Ctx; auto. }
apply imps in IHprv2. apply imps in IHprv3.
eapply DE.
1 : apply Ctx; firstorder.
1,2 : apply imps; eapply Weak; [eassumption|auto].
- apply Peirce_Fr.
Qed.
End Signature.
From Undecidability.Synthetic Require Import Definitions Undecidability.
From Undecidability.FOL.Util Require Import FA_facts Axiomatisations.
From Undecidability.Synthetic Require Import Definitions EnumerabilityFacts.
From Undecidability.FOL.Reductions Require Import H10p_to_FA.
From Undecidability.H10 Require Import H10p H10p_undec.
Require Import Undecidability.FOL.PA.
Section Arithmetic.
Existing Instance PA_preds_signature.
Existing Instance PA_funcs_signature.
Section Model.
Variable D : Type.
Variable I : @interp PA_funcs_signature _ D.
Variable ext_I : @interp PA_funcs_signature extended_preds D.
Lemma Fr_exists_eq N s t :
forall rho, sat ext_I rho (Fr (exist_times N (s == t))) <-> rho ⊨ (dn Friedman.Q (cast (exist_times N (s == t)))).
Proof.
induction N; cbn; intros ?.
- tauto.
- setoid_rewrite IHN. firstorder.
Qed.
Corollary Fr_embed E :
forall rho, sat ext_I rho (Fr (embed E)) <-> rho ⊨ (dn Friedman.Q (cast (embed E))).
Proof.
unfold embed, embed_problem; destruct E as [a b].
apply Fr_exists_eq.
Qed.
Definition ext_nat := extend_interp interp_nat.
Lemma cast_extists_eq N s t P rho :
sat (extend_interp I P) rho (cast (exist_times N (s == t))) -> sat rho (exist_times N (s == t)).
Proof.
revert rho. induction N.
- tauto.
- cbn. intros rho [d Hd]. exists d.
eapply IHN. unfold exist_times. apply Hd.
Qed.
Corollary cast_embed E P rho :
sat (extend_interp I P) rho (cast (embed E)) -> sat I rho (embed E).
Proof.
unfold embed, embed_problem; destruct E as [a b].
apply cast_extists_eq.
Qed.
Lemma sat_Fr_formula {P} phi rho :
I ⊨=T Q' -> Q' phi -> sat (extend_interp I P) rho (Fr phi).
Proof.
intros axioms H.
specialize (axioms phi). revert axioms.
repeat (destruct H as [<-|H]).
all: cbn -[FAeq]; refine (fun A => let F := A _ rho in _); intuition.
destruct H.
Unshelve. all: cbn; try tauto.
Qed.
Lemma sat_Fr_context {P} Gamma rho :
I ⊨=T Q' -> (forall psi : form, In psi Gamma -> Q' psi) -> (forall psi, In psi (Fr_ Gamma) -> sat (extend_interp I P) rho psi).
Proof.
intros axioms.
induction Gamma as [| alpha Gamma IH]; cbn -[FAeq].
- tauto.
- intros H beta [<-| [phi [<- ]] % in_map_iff ].
+ specialize (H alpha (or_introl eq_refl)).
now apply sat_Fr_formula.
+ apply IH; [|now apply in_map].
intros psi Hp. apply H; tauto.
Qed.
End Model.
Theorem sat_embed Gamma (E : H10p_PROBLEM) D (I : interp D) :
I ⊨=T Q' -> (forall psi : form, In psi Gamma -> Q' psi) -> Gamma ⊢C embed E -> I ⊨= embed E.
Proof.
intros HI Hg H % Fr_cl_to_min % soundness rho.
refine (let H' := H D (extend_interp I _) rho _ in _).
apply Fr_embed in H'.
simpl in H'. apply H'.
apply cast_embed. exact I.
Unshelve.
apply sat_Fr_context; auto.
Qed.
Theorem class_Q_to_H10p Gamma (E : H10p_PROBLEM) :
(forall psi : form, In psi Gamma -> Q' psi) -> Gamma ⊢C embed E -> H10p E.
Proof.
intros Hg H. apply nat_H10.
eapply sat_embed; eauto.
clear H; intros alpha H rho.
repeat (destruct H as [<-|H]; cbn; intuition).
destruct H.
Qed.
Corollary T_class_Q_to_H10p (T : form -> Prop) (E : H10p_PROBLEM) :
T <<= Q' -> T ⊢TC embed E -> H10p E.
Proof.
intros ? [Gamma []]. eapply class_Q_to_H10p; intuition.
Qed.
Lemma H10p_to_class_Q :
reduction embed H10p (tprv_class Q').
Proof.
intros E; split.
+ intros H. exists FAeq. split; [intuition|].
now apply H10p_to_FA_prv'.
+ intros H. eapply T_class_Q_to_H10p.
2 : apply H. auto.
Qed.
Lemma undec_class_Q :
undecidable (tprv_class Q').
Proof.
refine (undecidability_from_reducibility _ _).
2 : exists embed; apply H10p_to_class_Q.
apply H10p_undec.
Qed.
Definition Fr_pres T :=
forall D (I : interp D) P, I ⊨=T T -> forall Gamma, (forall psi, In psi Gamma -> T psi) -> (extend_interp I P) ⊫= Fr_ Gamma.
Section Theory.
Variable T : form -> Prop.
Variable Incl : Q' <<= T.
Variable Std : interp_nat ⊨=T T.
Variable Pres : Fr_pres T.
Lemma extract_from_class E :
T ⊢TC embed E -> interp_nat ⊨= embed E.
Proof.
intros [Gamma [H2 H % Fr_cl_to_min % soundness]] rho.
refine (let H' := H nat (extend_interp interp_nat _) rho _ in _).
apply Fr_embed in H'.
simpl in H'. apply H'.
apply cast_embed. exact interp_nat.
Unshelve.
now apply Pres.
Qed.
Lemma reduction_theorem :
reduction embed H10p (tprv_class T).
Proof.
intros E; split.
- intros H % (@H10p_to_FA_prv' class).
exists FAeq; split; [intros ?|auto].
apply Incl.
- intros H. apply nat_H10.
now apply extract_from_class.
Qed.
Lemma undec_class_T :
undecidable (tprv_class T).
Proof.
refine (undecidability_from_reducibility H10p_undec _).
exists embed. apply reduction_theorem.
Qed.
Lemma std_T_consistent :
~ T ⊢TC ⊥.
Proof.
intros [Gamma [H2 H % Fr_cl_to_min % soundness]].
specialize (H nat (ext_nat False) (fun _ => 0)).
apply H. eapply Pres; eauto.
Qed.
Theorem incompleteness_Q :
enumerable T -> complete T -> decidable (TM.HaltTM 1).
Proof.
intros HE HC. apply H10p_undec.
apply (@complete_reduction _ _ enum_PA_syms _ enum_PA_preds _ T HE) with embed.
- now apply std_T_consistent.
- apply HC.
- now apply reduction_theorem.
- apply embed_is_closed.
Qed.
End Theory.
End Arithmetic.