Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability.
Require Import Undecidability.FOL.ZF.
Require Import Undecidability.FOL.ZF_undec.
Require Import Undecidability.FOL.binZF.
From Undecidability.FOL.Util Require Import FullTarski FullDeduction_facts ZF_model.
From Undecidability.FOL.Reductions Require Import PCPb_to_ZF PCPb_to_ZFeq PCPb_to_ZFD PCPb_to_binZF.
From Undecidability.PCP Require Import PCP PCP_undec Util.PCP_facts Reductions.PCPb_iff_dPCPb.
Theorem PCPb_entailment_binZF :
PCPb ⪯ entailment_binZF.
Proof.
exists (fun B => rm_const_fm (solvable B)). intros B. split; intros H.
- intros V' M' rho' HM. apply (@PCP_ZFD intu), (@rm_const_prv intu nil), soundness in H. apply H; trivial.
- apply PCP_ZFeq'; try apply intensional_model.
intros V M rho HM. apply min_correct; trivial.
apply H. now apply min_axioms'.
Qed.
Corollary undecidable_entailment_binZF :
undecidable entailment_binZF.
Proof.
apply (undecidability_from_reducibility PCPb_undec), PCPb_entailment_binZF.
Qed.
Theorem PCPb_deduction_binZF :
PCPb ⪯ deduction_binZF.
Proof.
exists (fun B => rm_const_fm (solvable B)). intros B. split; intros H.
- now apply (@PCP_ZFD intu), (@rm_const_prv intu nil) in H.
- apply PCP_ZFeq'; try apply intensional_model. apply soundness in H.
intros V M rho HM. apply min_correct; trivial.
apply H. now apply min_axioms'.
Qed.
Theorem undecidable_deduction_binZF :
undecidable deduction_binZF.
Proof.
now apply (undecidability_from_reducibility PCPb_undec), PCPb_deduction_binZF.
Qed.
Require Import Undecidability.FOL.ZF.
Require Import Undecidability.FOL.ZF_undec.
Require Import Undecidability.FOL.binZF.
From Undecidability.FOL.Util Require Import FullTarski FullDeduction_facts ZF_model.
From Undecidability.FOL.Reductions Require Import PCPb_to_ZF PCPb_to_ZFeq PCPb_to_ZFD PCPb_to_binZF.
From Undecidability.PCP Require Import PCP PCP_undec Util.PCP_facts Reductions.PCPb_iff_dPCPb.
Theorem PCPb_entailment_binZF :
PCPb ⪯ entailment_binZF.
Proof.
exists (fun B => rm_const_fm (solvable B)). intros B. split; intros H.
- intros V' M' rho' HM. apply (@PCP_ZFD intu), (@rm_const_prv intu nil), soundness in H. apply H; trivial.
- apply PCP_ZFeq'; try apply intensional_model.
intros V M rho HM. apply min_correct; trivial.
apply H. now apply min_axioms'.
Qed.
Corollary undecidable_entailment_binZF :
undecidable entailment_binZF.
Proof.
apply (undecidability_from_reducibility PCPb_undec), PCPb_entailment_binZF.
Qed.
Theorem PCPb_deduction_binZF :
PCPb ⪯ deduction_binZF.
Proof.
exists (fun B => rm_const_fm (solvable B)). intros B. split; intros H.
- now apply (@PCP_ZFD intu), (@rm_const_prv intu nil) in H.
- apply PCP_ZFeq'; try apply intensional_model. apply soundness in H.
intros V M rho HM. apply min_correct; trivial.
apply H. now apply min_axioms'.
Qed.
Theorem undecidable_deduction_binZF :
undecidable deduction_binZF.
Proof.
now apply (undecidability_from_reducibility PCPb_undec), PCPb_deduction_binZF.
Qed.