proposition: Theorem FO_does_not_characterize_classes : exists (M : fo_model Σ bool) (_ : fo_model_dec M) (a b : bool), (forall x y, fo_bisimilar (Σ := Σ) nil [tt] M x y <-> x = y) /\ (forall x y φ ρ, fol_vars φ ⊑ [0] -> M,x·ρ ⊨ φ <-> M,y·ρ ⊨ φ) /\ exists ξ, fol_vars ξ ⊑ [0;1] /\ forall ρ, M,a·a·ρ ⊨ ξ /\ ~ M,b·a·ρ ⊨ ξ.
proof: Proof. exists M, M_dec, true, false; msplit 2; auto. exists (fo_bisimilar_formula (Σ := Σ) nil [tt] finite_t_bool M_dec); split. + apply fo_bisimilar_formula_vars. + intro; rewrite !fo_bisimilar_formula_sem; split; auto; intro; tauto. Qed.
imports: List Arith Nat Lia Relations Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations decidable gfp fol_ops fo_sig fo_terms fo_logic fo_definable fo_sat)