proposition: Theorem PCP_Z B : (exists V (M : interp V), extensional M /\ standard M /\ forall rho psi, Z psi -> rho ⊨ psi) -> PCPb B <-> entailment_Z (solvable B).
proof: Proof. intros HZF. rewrite PCPb_iff_dPCPb. split; intros H. - clear HZF. destruct H as [s H]. intros M HM rho H1 H2. eapply PCP_ZF1; eauto. intros sigma phi HP. apply H2. now constructor. - destruct HZF as (M & H1 & H2 & H3 & H4). specialize (H M H1 (fun _ => @i_func _ _ _ _ eset Vector.nil) H2 H4). apply PCP_ZF2 in H as [s Hs]; trivial; try now exists s. intros sigma phi HP. apply H4. now constructor. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Lia Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)