proposition: Theorem undecidable_deduction_FSTI : undecidable deduction_FSTI.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). exists solvable. intros B. split; intros H. - exists FSTeq. split; try apply FSTeq_base. now apply PCPb_to_FSTD.PCP_FSTD. - destruct FSTI_model as (D & I & H1 & H2 & H3). rewrite PCPb_iff_dPCPb. unshelve eapply PCP_FST2; eauto. + exact (fun _ => @i_func _ _ _ _ eset Vector.nil). + intros sigma psi Hp. apply H3. now constructor. + apply (tsoundness H). intros psi [theta [<-|[<-|[<-|[<-|Hp]]]]|theta]. 1-4: cbn; setoid_rewrite H1; congruence. * apply H3. now constructor. * apply H3. constructor 2. 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)