From FOL Require Import FullSyntax Arithmetics.
Require Import FOL.Incompleteness.Axiomatisations.
Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability.
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 List Lia.
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 FriedmanTranslation.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 FriedmanTranslation.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 auto with solve_subterm.
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 auto with zarith).
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 auto with solve_subterm.
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 :
forall Gamma P, (forall psi, In psi Gamma -> T psi) -> (extend_interp interp_nat P) ⊫= Fr_ Gamma.
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 Std.
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 Std; eauto.
Qed.
Theorem incompleteness_Q :
enumerable T -> complete T -> computational_explosion.
Proof.
intros HE HC. apply H10p_undec.
apply (@complete_reduction PA_funcs_signature PA_preds_signature enumerable_PA_funcs _ enumerable_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.
Require Import FOL.Incompleteness.Axiomatisations.
Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability.
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 List Lia.
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 FriedmanTranslation.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 FriedmanTranslation.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 auto with solve_subterm.
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 auto with zarith).
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 auto with solve_subterm.
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 :
forall Gamma P, (forall psi, In psi Gamma -> T psi) -> (extend_interp interp_nat P) ⊫= Fr_ Gamma.
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 Std.
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 Std; eauto.
Qed.
Theorem incompleteness_Q :
enumerable T -> complete T -> computational_explosion.
Proof.
intros HE HC. apply H10p_undec.
apply (@complete_reduction PA_funcs_signature PA_preds_signature enumerable_PA_funcs _ enumerable_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.