proposition: Theorem conservativity_ZF { p : peirce } phi : ZFeq ⊢T embed phi -> minZFeq ⊢T phi.
proof: Proof. intros [A [B HAB]] % ZF_decomp. apply rm_const_prv, loop_deductive' in HAB; auto. exists ([ax_sep' (rm_const_fm psi) | psi ∈ A] ++ [ax_rep' (rm_const_fm psi) | psi ∈ B] ++ minZFeq'). split. - intros psi [|[H|H] % in_app_iff] % in_app_iff; try now constructor. all: apply in_map_iff in H as [psi'[<- H]]. constructor 2. constructor 3. - apply (prv_cut HAB). intros psi [[psi' [<- H]] % in_map_iff|H] % in_app_iff. + apply in_app_iff in H as [[phi' [<- H]] % in_map_iff|[phi' [<- H]] % in_map_iff]. * eapply IE; try apply minZF_sep; auto. apply Ctx, in_app_iff. left. refine (in_map _ _ _ H). * eapply IE; try apply minZF_rep; auto. apply Ctx, in_app_iff. right. apply in_app_iff. left. refine (in_map _ _ _ H). + auto. apply Ctx. auto. Qed.
imports: Undecidability.FOL(Semantics.Tarski.FullFacts Syntax.Facts Deduction.FullNDFacts) Undecidability.FOL.Sets(ZF minZF) Undecidability.FOL.Reductions(PCPb_to_ZF PCPb_to_minZF PCPb_to_ZFD) Undecidability(Shared.ListAutomation)