proposition: Theorem PCPb_deduction_Z : (exists V (M : interp V), extensional M /\ standard M /\ forall rho psi, Z psi -> rho ⊨ psi) -> reduction solvable PCPb deduction_Z.
proof: Proof. intros (V & M & H1 & H2 & H3). intros B. split. - intros H % (@PCP_ZFD intu). exists ZFeq'. split; eauto using Zeq. - intros H'. specialize (tsoundness H'). clear H'. intros H'. apply PCPb_iff_dPCPb. eapply PCP_ZF2; eauto using Z. apply (H' V M (fun _ => ∅)). intros psi []. + apply extensional_eq; eauto using Z. + apply H3. constructor 2. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability Undecidability.FOL(Semantics.Tarski.FullFacts Semantics.Tarski.FullSoundness) Undecidability.FOL.Sets.Models(Aczel_CE Aczel_TD ZF_model HF_model) Undecidability.FOL.Reductions(ZF_to_HF PCPb_to_HF PCPb_to_HFD PCPb_to_ZFeq PCPb_to_ZF PCPb_to_ZFD) Undecidability.FOL.Sets.ZF Undecidability.FOL.ZF Undecidability.PCP(PCP PCP_undec Util.PCP_facts Reductions.PCPb_iff_dPCPb)