proposition: Theorem MONADIC_PROP_discernable_dec_FSAT_dec_equiv (Σ : fo_signature) : (forall r, @ar_rels Σ r = 0) -> (forall u v : rels Σ, decidable (u ≢ v)) ≋ forall A, decidable (FSAT Σ A).
proof: Proof. intros H; split. + intros; apply FULL_MONADIC_discernable; eauto. + intros H1. assert (forall A, decidable (FSAT (Σ0 Σ) A)) as H2. { revert H1; apply ireduction_decidable, FSAT_x0_FSAT_PROP; auto. } exact (FSAT_dec_implies_discernable_rels_dec H2). Qed.
imports: List Arith Undecidability.Synthetic(Definitions ReducibilityFacts InformativeDefinitions InformativeReducibilityFacts) Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable discernable fol_ops fo_sig fo_terms fo_logic fo_sat fo_sat_dec red_utils Sig_Sig_fin Sig_rem_props Sig_rem_constants Sig0 Sig1 Sig1_1 Sig_discernable)