proposition: Theorem PCPb_entailment_minZ : (exists V (M : interp V), extensional M /\ standard M /\ forall rho psi, Z psi -> rho ⊨ psi) -> reduction minsolvable PCPb entailment_minZ.
proof: Proof. intros (V & M & H1 & H2 & H3). intros B. split; intros H. - intros V' M' rho' HM1 HM2. apply (@PCP_ZFD intu), (@rm_const_prv intu nil), soundness in H. apply H, extensional_eq_min'; trivial. eauto using minZ. - specialize (H V (@min_model V M) (fun _ => ∅)). unfold minsolvable in H. rewrite <- min_correct in H; trivial; eauto using Z. rewrite PCPb_iff_dPCPb. eapply PCP_ZF2 in H2 as [s Hs]; trivial; try apply H; eauto using Z. now exists s. apply min_axioms_Z; eauto using Z. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.FOL.ZF_undec Undecidability.FOL.Sets.minZF Undecidability.FOL.Sets.Models.ZF_model Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Semantics.Tarski.FullSoundness Undecidability.FOL.ZF Undecidability.FOL.Reductions(PCPb_to_ZFeq PCPb_to_minZFeq PCPb_to_ZF PCPb_to_ZFD PCPb_to_binZF PCPb_to_minZF) Undecidability.PCP(PCP PCP_undec Util.PCP_facts Reductions.PCPb_iff_dPCPb)