proposition: Theorem undecidable_deduction_HFN : undecidable deduction_HFN.
proof: Proof. apply (undecidability_from_reducibility PCPb_undec). exists PCPb_to_HF.solvable. intros B. split. - intros H. eapply Weak. try apply PCP_HFD; auto. intros phi Hp. firstorder. - intros H % soundness. destruct HFN_model as (M & H1 & H2 & H3 & H4). specialize (H M H1 (fun _ => @i_func _ _ _ _ eset Vector.nil)). eapply PCPb_iff_dPCPb, PCP_HF2; try apply H; trivial. + intros rho phi Hp. apply H4. now right. + intros phi [<-|[<-|[<-|[<-|Hp]]]]; try now apply H4. all: cbn; setoid_rewrite H2; congruence. 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)