proposition: Theorem undecidable_deduction_FST : undecidable deduction_FST.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). exists solvable'. intros B. split. - intros HP % (PCP_FSTD (p:=intu)). apply HP. - intros HP % soundness. apply PCP_FST. intros I M rho H. apply HP. apply H. 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)