proposition: Theorem undecidable_entailment_FSTI : undecidable entailment_FSTI.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). exists solvable. intros B. rewrite PCPb_iff_dPCPb. split; intros H. - destruct H as [s H]. intros M HM rho H1 H2. eapply PCP_FST1; eauto. intros sigma psi Hp. apply H2. now constructor. - destruct FSTI_model as (D & I & H1 & H2 & H3). specialize (H D I (fun _ => @i_func _ _ _ _ eset Vector.nil) H1 H3). apply PCP_FST2 in H as [s Hs]; trivial. now exists s. intros sigma psi Hp. apply H3. now constructor. Qed.
imports: Undecidability.Synthetic(Definitions Undecidability) Undecidability.FOL(Sets.FST Semantics.Tarski.FullFacts Semantics.Tarski.FullSoundness Deduction.FullNDFacts Sets.Models.FST_model FST) Undecidability.FOL.Reductions(PCPb_to_FST PCPb_to_FSTD ZF_to_FST) Undecidability.PCP(PCP PCP_undec Reductions.PCPb_iff_dPCPb)