Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability.
Require Import Undecidability.FOL.binFST.
Require Import Undecidability.FOL.binZF_undec.
Require Import Undecidability.FOL.Reductions.binZF_to_binFST.
Theorem undecidable_entailment_binFST :
undecidable entailment_binFST.
Proof.
apply (undecidability_from_reducibility undecidable_entailment_binZF).
exists ZF_to_FST. intros phi. apply reduction_entailment.
Qed.
Theorem undecidable_deduction_binFST :
undecidable deduction_binFST.
Proof.
apply (undecidability_from_reducibility undecidable_deduction_binZF).
exists ZF_to_FST. intros phi. apply reduction_deduction.
Qed.
Require Import Undecidability.FOL.binFST.
Require Import Undecidability.FOL.binZF_undec.
Require Import Undecidability.FOL.Reductions.binZF_to_binFST.
Theorem undecidable_entailment_binFST :
undecidable entailment_binFST.
Proof.
apply (undecidability_from_reducibility undecidable_entailment_binZF).
exists ZF_to_FST. intros phi. apply reduction_entailment.
Qed.
Theorem undecidable_deduction_binFST :
undecidable deduction_binFST.
Proof.
apply (undecidability_from_reducibility undecidable_deduction_binZF).
exists ZF_to_FST. intros phi. apply reduction_deduction.
Qed.