From Undecidability.FOL Require Import FullSyntax.
From Undecidability.Synthetic Require Import Definitions Undecidability MPFacts.
From Undecidability.Synthetic Require Import DecidabilityFacts EnumerabilityFacts ReducibilityFacts.
From Undecidability.Synthetic Require Import ListEnumerabilityFacts MoreEnumerabilityFacts.
From Undecidability.Shared Require Import Dec.
From Undecidability Require Import Synthetic.Undecidability.
From Equations Require Import Equations.
Require Import ConstructiveEpsilon.
Require Import List.
Import ListNotations.

Local Set Implicit Arguments.
Local Unset Strict Implicit.


#[local]
Existing Instance falsity_on.

Local Hint Constructors prv : core.

Notation "S <<= S'" := (forall phi, S phi -> S' phi) (at level 10).
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 "T ⊨T phi" := (forall D (I : interp D) rho, (forall psi, T psi -> rho ⊨ psi) -> rho ⊨ phi) (at level 55).

Section FixSignature.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Implicit Type T : form -> Prop.

  Definition tprv_class T phi := T ⊢TC phi.
  Definition tprv_intu T phi := T ⊢TI phi.
  Definition tvalid T phi := T ⊨T phi.


  Definition treduction X (f : X -> form) (P : X -> Prop) T :=
    reduction f P (tvalid T) /\ reduction f P (tprv_intu T).


  Fact reduction_consistency {p : peirce} X (f : X -> form) (P : X -> Prop) T :
    reduction f P (tprv T) -> (exists x, ~ P x) -> ~ T ⊢T ⊥.
  Proof.
    intros Hf [x Hx] [A[H1 H2]]. apply Hx, Hf.
    exists A. split; trivial. now apply Exp.
  Qed.

  Section Axiomatisations.

    Context {enum_funcs : enumerable__T Σ_funcs} {eqdec_funcs : eq_dec syms}.
    Context {enum_preds : enumerable__T Σ_preds} {eqdec_preds : eq_dec preds}.


    Instance EqDec_funcs : EqDec Σ_funcs.
    Proof.
      intros x y. apply eqdec_funcs.
    Qed.

    Instance EqDec_preds : EqDec Σ_preds.
    Proof.
      intros x y. apply eqdec_preds.
    Qed.

    Lemma form_discrete :
      discrete form.
    Proof.
      apply discrete_iff. constructor. apply dec_form; trivial.
      all: intros ? ?; unfold dec; decide equality.
    Qed.

    Lemma form_enumerable :
      enumerable__T form.
    Proof.
      eapply enumT_form'; trivial. apply enumT_binop. apply enumT_quantop.
    Qed.


    Variable T : form -> Prop.
    Hypothesis enum_T : enumerable T.

    Lemma tprv_enumerable {p : peirce} :
      enumerable (fun phi => tprv T phi).
    Proof.
      apply enumerable_enum.
      apply enumerable_enum in enum_T as [L HL].
      apply enum_enumT in enum_funcs as [L1 HL1].
      apply enum_enumT in enum_preds as [L2 HL2].
      exists (@L_tded _ _ L1 HL1 L2 HL2 _ _ p falsity_on (cumul L)).
      now apply enum_tprv.
    Qed.


    Definition stripneg `{falsity_flag} (phi : form) : option form :=
      match phi with
      | bin Impl phi ⊥ => Some phi
      | _ => None
      end.

    Instance eq_dec_ff :
      eq_dec falsity_flag.
    Proof.
      intros ff ff'. unfold dec. decide equality.
    Qed.

    Derive Signature for form.

    Lemma stripneg_spec {ff : falsity_flag} {phi psi} :
      stripneg phi = Some psi -> phi = ¬ psi.
    Proof.
      depelim phi; cbn; try destruct b0; try discriminate.
      - inversion H. apply Eqdep.EqdepTheory.inj_pair2 in H1 as ->; eauto. cbn. discriminate.
      - depelim phi2; cbn; try destruct b0; try discriminate.
        inversion H. apply Eqdep.EqdepTheory.inj_pair2 in H1 as ->; eauto. congruence.
    Qed.

    Lemma enumerable_equiv X (P Q : X -> Prop) :
      (forall x, P x <-> Q x) -> enumerable P -> enumerable Q.
    Proof.
      intros H [f Hf]. exists f. intros x. rewrite <- H. apply Hf.
    Qed.

    Definition complete :=
      forall phi, bounded 0 phi -> T ⊢TC phi \/ T ⊢TC ¬ phi.

    Fact complete_decidable :
      (~ T ⊢TC ⊥) -> complete -> decidable (fun phi => bounded 0 phi /\ T ⊢TC phi).
    Proof.
      intros H1 H2.
      assert (H : forall phi, bounded 0 phi -> ~ T ⊢TC phi <-> T ⊢TC ¬ phi).
      - intros phi HP. split; intros H.
        + destruct (H2 phi) as [H3|H3]; tauto.
        + intros [B[HB1 HB2]]. destruct H as [C[HC1 HC2]].
          apply H1. exists (B ++ C). split.
          * intros psi. rewrite in_app_iff. intuition.
          * eapply IE; eapply Weak; eauto. 1:apply incl_appr. 2:apply incl_appl. all:apply incl_refl.
      - apply weakPost; try apply form_discrete.
        + intros phi. destruct (bounded_dec phi 0) as [Hb|Hb].
          destruct (H2 phi Hb) as [Hp|Hp % H]. all: tauto.
        + apply enumerable_conj; try apply form_discrete.
          * apply dec_count_enum; try apply form_enumerable.
            apply decidable_iff. constructor. intros phi. apply bounded_dec.
          * apply tprv_enumerable.
        + apply enumerable_equiv with (fun phi => ~ bounded 0 phi \/ T ⊢TC ¬ phi).
          { intros phi. destruct (bounded_dec phi 0); intuition. }
          apply enumerable_disj; try apply dec_count_enum'; try apply form_enumerable.
          { apply decidable_iff. constructor. intros phi. apply bounded_dec. }
          destruct (tprv_enumerable (p:=class)) as [f Hf].
          exists (fun n => match f n with Some phi => stripneg phi | _ => None end).
          intros phi. rewrite (Hf (¬ phi)). split; intros [n Hn]; exists n; try now rewrite Hn.
          destruct (f n) as [psi|]; try discriminate. now rewrite (stripneg_spec Hn).
    Qed.


    Fact complete_reduction X (P : X -> Prop) (f : X -> form) :
      (~ T ⊢TC ⊥) -> complete -> reduction f P (tprv_class T) -> (forall x, bounded 0 (f x)) -> decidable P.
    Proof.
      intros H1 H2 H3 H4. apply complete_decidable in H1; trivial.
      apply decidable_iff in H1 as [H1]. apply decidable_iff. constructor.
      intros x. destruct (H1 (f x)) as [H|H].
      - left. apply H3, H.
      - right. contradict H. split; try now apply H4. apply H3, H.
    Qed.

  End Axiomatisations.


  Section Reduction.

    Variable T : form -> Prop.

    Variable X : Type.
    Variable P : X -> Prop.
    Variable f : X -> form.

    Variable standard : forall D, interp D -> Prop.

    Hypothesis hyp1 : forall x, P x -> T ⊨T (f x).
    Hypothesis hyp2 : forall D (I : interp D) x, standard I -> I ⊨=T T -> I ⊨= (f x) -> P x.
    Hypothesis hyp3 : forall {p : peirce} x, P x -> T ⊢T (f x).

    Lemma WeakT {p : peirce} (S S' : form -> Prop) phi :
      S ⊢T phi -> S <<= S' -> S' ⊢T phi.
    Proof.
      intros [A[H1 H2]] H. exists A. split; auto.
    Qed.

    Theorem reduction_theorem (S : form -> Prop) :
      T <<= S -> (exists D (I : interp D), standard I /\ I ⊨=T S) -> treduction f P S.
    Proof.
      intros HS (D & I & [std MT]). repeat split; intros H.
      - intros D' I' rho H'. apply hyp1; auto.
      - apply (hyp2 std); auto.
      - apply WeakT with T; trivial. now apply hyp3.
      - apply (hyp2 std); auto. intros rho. apply (tsoundness H); auto.
    Qed.


    Definition LEM := forall P, P \/ ~ P.

    Theorem reduction_theorem_class (S : form -> Prop) :
      LEM -> T <<= S -> (exists D I, @standard D I /\ I ⊨=T S) -> reduction f P (tprv_class S).
    Proof.
      intros lem HS (D & I & [std MT]). split; intros H.
      - apply WeakT with T; trivial. now apply hyp3.
      - apply (hyp2 std); auto. intros rho. apply (tsoundness_class lem H); auto.
    Qed.

  End Reduction.


  Definition list_theory (A : list form) :=
    fun phi => In phi A.

  Lemma red_finite_valid A :
    tvalid (list_theory A) ⪯ valid.
  Proof.
    exists (impl A). intros phi. unfold valid. setoid_rewrite impl_sat. firstorder.
  Qed.

  Lemma red_finite_prv {p : peirce} A :
    tprv (list_theory A) ⪯ (prv nil).
  Proof.
    exists (impl A). intros phi. setoid_rewrite <- impl_prv. rewrite app_nil_r. split; intros H.
    - destruct H as [B[H1 H2]]. apply (Weak (B:=A)) in H2; auto.
      apply (Weak H2). unfold incl. apply in_rev.
    - exists A. split; trivial. apply (Weak H). unfold incl. apply in_rev.
  Qed.


  Lemma red_prv_prv {p : peirce} A T :
    T <<= (prv A) -> prv A ⪯ tprv T.
  Proof.
    intros Ded.
    exists (fun phi => A ==> phi). intros phi; split; intros H.
    - exists nil. split; [auto|]. 1: intros a []. setoid_rewrite <- impl_prv.
      rewrite app_nil_r.
      apply (Weak H). unfold incl. apply in_rev.
    - destruct H as [B [H1 H2 % impl_prv]].
      apply (prv_cut H2). intros psi [H|H] % in_app_iff.
      + apply Ctx. now apply in_rev.
      + now apply Ded, H1.
  Qed.

  Lemma red_prv_valid A T :
    T <<= (prv (p:=intu) A) -> tvalid (list_theory A) ⪯ tvalid T.
  Proof.
    intros Ded.
    exists (fun phi => A ==> phi). intros phi; split; intros H D I rho HI.
    - apply impl_sat. apply H.
    - specialize (H D I rho). setoid_rewrite impl_sat in H. apply H.
      + intros psi HP. apply Ded in HP. apply soundness in HP. apply HP. apply HI.
      + apply HI.
  Qed.

  Lemma red_sub_prv {p : peirce} A T :
    T <<= (list_theory A) -> prv A ⪯ tprv T.
  Proof.
    intros Sub. apply red_prv_prv.
    intros phi H. now apply Ctx, Sub.
  Qed.

  Lemma red_sub_valid {p : peirce} A T :
    T <<= (list_theory A) -> tvalid (list_theory A) ⪯ tvalid T.
  Proof.
    intros Sub. apply red_prv_valid.
    intros phi H. now apply Ctx, Sub.
  Qed.

  Lemma red_union_prv' {p : peirce} A T :
    reduction (fun phi => A ==> phi) (tprv (fun phi => T phi \/ In phi A)) (tprv T).
  Proof.
    intros phi; split; intros [C [H1 H2]].
    - assert (exists C1 C2, incl C1 A /\ list_theory C2 <<= T /\ incl C (C1 ++ C2)).
      + clear H2. induction C.
        * exists nil, nil. cbn. repeat split; auto. all: intros x [].
        * destruct IHC as (C1 & C2 & H2 & H3 & H4).
          -- intros psi HP. apply H1. now right.
          -- destruct (H1 a) as [H|H]; try now left.
             ++ exists C1, (a::C2). repeat split; trivial. firstorder congruence.
                intros psi [->|HP]; auto. 1: { apply in_or_app, or_intror; now left. } apply H4 in HP as [HP|HP] % in_app_iff; auto. 1: now apply in_or_app, or_introl. 1:now apply in_or_app, or_intror, or_intror.
             ++ exists (a::C1), C2. repeat split; firstorder congruence.
      + destruct H as (C1 & C2 & H3 & H4 & H5).
        exists C2. split; try apply H4. apply impl_prv. apply (Weak H2).
        intros psi [H|H] % H5 % in_app_iff; auto. apply in_app_iff. left. apply -> in_rev. now apply H3.
        now apply in_or_app, or_intror.
    - exists (rev A ++ C). split; try now apply impl_prv.
      intros psi [H|H] % in_app_iff; auto. right. now apply in_rev.
  Qed.

  Lemma red_union_prv {p : peirce} A T :
    tprv (fun phi => T phi \/ In phi A) ⪯ tprv T.
  Proof.
    exists (fun phi => A ==> phi). apply red_union_prv'.
  Qed.

  Lemma red_union_valid A T :
    tvalid (fun phi => T phi \/ In phi A) ⪯ tvalid T.
  Proof.
    exists (fun phi => A ==> phi). intros phi; split; intros H D I rho HI.
    - apply impl_sat. intros HA. apply H. firstorder.
    - specialize (H D I rho). setoid_rewrite impl_sat in H. apply H; firstorder.
  Qed.

End FixSignature.



From Undecidability.FOL.Arithmetics Require Import PA DeductionFacts TarskiFacts NatModel.
From Undecidability.FOL.Undecidability.Reductions Require Import H10p_to_FA.
From Undecidability.H10 Require Import H10p H10p_undec.

#[local]
Existing Instance PA_funcs_signature.
#[local]
Existing Instance PA_preds_signature.


Definition Q' := list_theory FAeq.

Lemma PA_undec1 E :
  H10p E -> Q' ⊨T embed E.
Proof.
  intros HE D M HM rho. apply H10p_to_FA_sat; auto.
Qed.


Lemma PA_undec2 D (M : interp D) E :
  standard D M -> M ⊨=T Q' -> M ⊨= embed E -> H10p E.
Proof.
  intros H1 H2 H3. apply standard_embed with (fun n => iO); auto.
Qed.

Lemma PA_undec3 (p : peirce) E :
  H10p E -> Q' ⊢T embed E.
Proof.
  intros H. exists FAeq. split; auto. now apply H10p_to_FA_prv'.
Qed.


Notation "P ⪯T T" := (exists f, treduction f P T) (at level 55).

Theorem undec_Q' :
  H10p ⪯T Q'.
Proof.
  exists embed. apply (reduction_theorem PA_undec1 PA_undec2 PA_undec3).
  - auto.
  - exists nat, interp_nat. split; try apply nat_standard.
    eauto using nat_is_FA_model.
Qed.

Theorem undec_Q :
  H10p ⪯T list_theory Qeq.
Proof.
  exists embed. apply (reduction_theorem PA_undec1 PA_undec2 PA_undec3).
  - firstorder.
  - exists nat, interp_nat. split; try apply nat_standard.
    eauto using nat_is_Q_model.
Qed.

Theorem undec_PA :
  H10p ⪯T PAeq.
Proof.
  exists embed. apply (reduction_theorem PA_undec1 PA_undec2 PA_undec3).
  - eauto using PAeq.
  - exists nat, interp_nat. split; try apply nat_standard.
    eauto using nat_is_PAeq_model.
Qed.



#[global]
Instance eqdec_PA_syms :
  eq_dec syms.
Proof.
  intros x y. unfold dec. decide equality.
Qed.

#[global]
Instance eqdec_PA_preds :
  eq_dec preds.
Proof.
  intros x y. unfold dec. decide equality.
Qed.

#[global]
Definition enum_PA_syms :
  enumerable__T syms.
Proof.
  apply enum_enumT. exists (fun _ => [Zero; Succ; Plus; Mult]).
  intros []; exists 0; auto. all: cbv; eauto.
Qed.

Definition enum_PA_preds :
  enumerable__T preds.
Proof.
  apply enum_enumT. exists (fun _ => [Eq]).
  intros []; exists 0; auto. all: cbv; eauto.
Qed.

Lemma PAeq_enum :
  enumerable PAeq.
Proof.
  destruct enumT_form' as [f Hf].
  - apply enum_PA_syms.
  - apply enum_PA_preds.
  - apply enumT_binop.
  - apply enumT_quantop.
  - exists (fun n => match n with 0 => Some ax_refl | 1 => Some ax_sym | 2 => Some ax_trans
                     | 3 => Some ax_succ_congr | 4 => Some ax_add_congr
                     | 5 => Some ax_mult_congr | 6 => Some ax_add_zero
                     | 7 => Some ax_add_rec | 8 => Some ax_mult_zero | 9 => Some ax_mult_rec
                     | 10 => Some ax_zero_succ | 11 => Some ax_succ_inj
                     | S (S (S (S (S (S (S (S (S (S (S (S n))))))))))) =>
                         match f n with Some phi => Some (ax_induction phi) | _ => None end end).
    intros phi. split.
    + intros [| | |psi].
      * destruct H as [<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]]]].
        now exists 0. now exists 1. now exists 2. now exists 3. now exists 4. now exists 5. now exists 6. now exists 7. now exists 8. now exists 9.
      * now exists 10.
      * now exists 11.
      * destruct (Hf psi) as [n Hn]. exists (12 + n). cbn. now rewrite Hn.
    + intros [[|[|[|[|[|[|[|[|[|[|[|[|]]]]]]]]]]]] [=]]; subst; eauto using PAeq.
      all: try (apply PAeq_FA; cbn; tauto).
      destruct (f n); try congruence. injection H0. intros <-. apply PAeq_induction.
Qed.

Theorem incompleteness_PA (T : form -> Prop) :
  LEM -> Q' <<= T -> enumerable T -> complete T -> interp_nat ⊨=T T -> computational_explosion.
Proof.
  intros lem HFA HE HC HT. apply H10p_undec.
  apply (@complete_reduction _ _ enum_PA_syms _ enum_PA_preds _ T HE) with embed.
  - intros H. apply (@tsoundness_class _ _ lem _ T ⊥ H nat interp_nat (fun n => 0)). firstorder.
  - apply HC.
  - eapply (reduction_theorem_class PA_undec2 PA_undec3); trivial.
    exists nat, interp_nat. split; auto. apply nat_standard.
  - apply embed_is_closed.
Qed.


Fact undec_standard_prv (T : form -> Prop) :
  interp_nat ⊨=T T -> H10p ⪯ @tprv _ _ _ intu T.
Proof.
  intros HT. eapply reduces_transitive; try apply (red_union_prv FAeq).
  exists embed. apply (reduction_theorem PA_undec1 PA_undec2 PA_undec3).
  - auto.
  - exists nat, interp_nat. split; try apply nat_standard.
    intros Phi [H|H]; try now apply HT.
    eauto using nat_is_FA_model.
Qed.

Fact undec_standard_valid (T : form -> Prop) :
  interp_nat ⊨=T T -> H10p ⪯ tvalid T.
Proof.
  intros HT. eapply reduces_transitive; try apply (red_union_valid FAeq).
  exists embed. apply (reduction_theorem PA_undec1 PA_undec2 PA_undec3).
  - auto.
  - exists nat, interp_nat. split; try apply nat_standard.
    intros Phi [H|H]; try now apply HT.
    eauto using nat_is_FA_model.
Qed.


From Undecidability.FOL.Undecidability.Reductions Require Import PCPb_to_ZFeq PCPb_to_ZF PCPb_to_ZFD.
From Undecidability.FOL.Sets Require Import Models.Aczel_CE Models.ZF_model ZF.
From Undecidability.PCP Require Import PCP PCP_undec.


#[local]
Existing Instance ZF_func_sig.
#[local]
Existing Instance ZF_pred_sig.

Definition Z' := list_theory ZFeq'.

Lemma ZF_undec1 B :
  PCPb B -> Z' ⊨T solvable B.
Proof.
  intros HE D M HM rho. apply (PCP_ZFD (p:=intu)) in HE.
  apply (soundness HE). auto.
Qed.


Open Scope sem.
Lemma ZF_undec2 D (M : interp D) B :
  standard M -> M ⊨=T Z' -> M ⊨= solvable B -> PCPb B.
Proof.
  intros H1 H2 H3. apply PCP_ZFeq with (fun _ => ∅); auto.
Qed.

Lemma ZF_undec3 (p : peirce) B :
  PCPb B -> Z' ⊢T solvable B.
Proof.
  intros H. exists ZFeq'. split; auto. now apply PCP_ZFD.
Qed.


Lemma undec_Z' :
  (exists D I, @standard D I /\ I ⊨=T Z') -> treduction solvable PCPb Z'.
Proof.
  apply (reduction_theorem ZF_undec1 ZF_undec2 ZF_undec3); trivial.
Qed.

Lemma undec_Z :
  (exists D I, @standard D I /\ I ⊨=T Zeq) -> treduction solvable PCPb Zeq.
Proof.
  apply (reduction_theorem ZF_undec1 ZF_undec2 ZF_undec3); trivial.
  eauto using Zeq.
Qed.

Lemma undec_ZF :
  (exists D I, @standard D I /\ I ⊨=T ZFeq) -> treduction solvable PCPb ZFeq.
Proof.
  apply (reduction_theorem ZF_undec1 ZF_undec2 ZF_undec3); trivial.
  eauto using ZFeq.
Qed.


Lemma CE_undec_Z' :
  Aczel_CE.CE -> treduction solvable PCPb Z'.
Proof.
  intros H. apply undec_Z'.
  destruct (extensionality_model_eq H) as (D & M & H1 & H2 & H3).
  exists D, M. split; trivial. eauto using Zeq.
Qed.

Lemma CE_undec_Z :
  Aczel_CE.CE -> treduction solvable PCPb Zeq.
Proof.
  intros H. apply undec_Z.
  destruct (extensionality_model_eq H) as (D & M & H1 & H2 & H3).
  exists D, M. split; trivial. auto.
Qed.

Lemma TD_undec_ZF :
  Aczel_CE.CE -> TD -> treduction solvable PCPb ZFeq.
Proof.
  intros HC HD. apply undec_ZF.
  destruct (normaliser_model_eq HC HD) as (D & M & H1 & H2 & H3).
  exists D, M. split; trivial. auto.
Qed.


Lemma refined_undec_Z' :
  treduction solvable PCPb Z'.
Proof.
  apply undec_Z'.
  destruct intensional_model as (D & M & H1 & H2).
  exists D, M. split; trivial. auto.
Qed.



#[local]
Instance eqdec_ZF_syms :
  eq_dec syms.
Proof.
  intros x y. unfold dec. decide equality.
Qed.

#[local]
Instance eqdec_ZF_preds :
  eq_dec preds.
Proof.
  intros x y. unfold dec. decide equality.
Qed.

Definition enum_ZF_syms :
  enumerable__T syms.
Proof.
  apply enum_enumT. exists (fun _ => [eset; pair; power; union; om]).
  intros []; exists 0; auto. all: cbv; eauto. do 4 right. now left.
Qed.

Definition enum_ZF_preds :
  enumerable__T preds.
Proof.
  apply enum_enumT. exists (fun _ => [elem; equal]).
  intros []; exists 0; auto. all: cbv; eauto.
Qed.


Theorem incompleteness_ZF (T : form -> Prop) :
  LEM -> Z' <<= T -> enumerable T -> complete T -> (exists D I, @standard D I /\ I ⊨=T T) -> computational_explosion.
Proof.
  intros lem HFA HE HC (Ds & Is & HI1 & HI2). apply PCPb_undec.
  apply (@complete_reduction _ _ enum_ZF_syms _ enum_ZF_preds _ T HE) with solvable.
  - intros H. apply (@tsoundness_class _ _ lem _ T ⊥ H Ds Is (fun n => ∅)). firstorder.
  - apply HC.
  - eapply (reduction_theorem_class ZF_undec2 ZF_undec3); trivial. now exists Ds, Is.
  - apply solvabe_bound.
Qed.


From Undecidability.FOL Require Import minZF PCPb_to_minZF PCPb_to_minZFeq.

#[local]
Existing Instance sig_empty.
#[local]
Existing Instance ZF_pred_sig.


Definition minZ' := list_theory minZFeq'.

Lemma undec_minZ' :
  PCPb ⪯T minZ'.
Proof.
  exists minsolvable. split; intros B; split; intros H.
  - apply (@PCP_ZFD intu), (@rm_const_prv intu nil), soundness in H. auto.
  - apply PCP_ZFeq'; try apply intensional_model.
    intros V M rho HM. apply min_correct; trivial.
    apply H. now apply min_axioms'.
  - exists minZFeq'. split; auto. now apply (@PCP_ZFD intu), (@rm_const_prv intu nil) in H.
  - destruct H as (A & H1 & H2). eapply (Weak (B:=minZFeq')) in H2; auto.
    apply PCP_ZFeq'; try apply intensional_model. apply soundness in H2.
    intros V M rho HM. apply min_correct; trivial.
    apply H2. now apply min_axioms'.
Qed.


From Undecidability.FOL Require Import BinSig binZF PCPb_to_binZF binZF_undec.

#[local]
Existing Instance sig_empty.
#[local]
Existing Instance sig_binary.


Definition binZ' := list_theory binZF.

Lemma undec_binZ' :
  treduction binsolvable PCPb binZ'.
Proof.
  split; intros B.
  - rewrite (PCPb_entailment_binZF B). split; intros H D M rho; eauto.
  - rewrite (PCPb_deduction_binZF B). split; intros H.
    + exists binZF. split; auto.
    + destruct H as [A[H1 H2]]. apply (Weak H2). auto.
Qed.


Lemma undec_valid :
  undecidable valid.
Proof.
  apply (undecidability_from_reducibility PCPb_undec). eapply reduces_transitive.
  + exists binsolvable. apply (proj1 undec_binZ').
  + apply red_finite_valid.
Qed.

Lemma undec_prv_intu :
  undecidable (prv (p:=intu) nil).
Proof.
  apply (undecidability_from_reducibility PCPb_undec). eapply reduces_transitive.
  + exists binsolvable. apply (proj2 undec_binZ').
  + apply red_finite_prv.
Qed.


Lemma undec_class_binZ' :
  LEM -> reduction binsolvable PCPb (tprv_class binZ').
Proof.
  intros lem. split; intros H.
  - apply (@PCP_ZFD class), (@rm_const_prv class nil) in H. exists binZF. split; trivial.
  - destruct H as [A[H1 H2]]. apply PCP_ZFeq'; try apply intensional_model.
    apply (Weak (B:=binZF)) in H2; auto. apply soundness_class in H2; trivial.
    intros V M rho HM. apply min_correct; trivial. apply H2. now apply min_axioms'.
Qed.

Lemma undec_prv_class :
  LEM -> undecidable (prv (p:=class) nil).
Proof.
  intros lem. apply (undecidability_from_reducibility PCPb_undec). eapply reduces_transitive.
  + exists binsolvable. now apply undec_class_binZ'.
  + apply red_finite_prv.
Qed.