English
For any sentence φ, T ⊨ᵇ φ holds if and only if the theory T together with φ.not is not satisfiable; i.e., there is no model of T that makes φ false.
Русский
Для любого предложения φ, T ⊨ᵇ φ эквивалентно тому, что теория T вместе с ¬φ не имеет удовлетворения; то есть не существует модели T, в которой φ ложно.
LaTeX
$$$T \models^{\mathrm{b}} \varphi \iff \neg \operatorname{IsSatisfiable}(T \cup \{\neg \varphi\})$$$
Lean4
theorem models_iff_not_satisfiable (φ : L.Sentence) : T ⊨ᵇ φ ↔ ¬IsSatisfiable (T ∪ { φ.not }) :=
by
rw [models_sentence_iff, IsSatisfiable]
refine
⟨fun h1 h2 =>
(Sentence.realize_not _).1
(realize_sentence_of_mem (T ∪ {Formula.not φ}) (Set.subset_union_right (Set.mem_singleton _)))
(h1 (h2.some.subtheoryModel Set.subset_union_left)),
fun h M => ?_⟩
contrapose! h
rw [← Sentence.realize_not] at h
refine
⟨{ Carrier := M
is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => ?_⟩ }⟩
rw [Set.mem_singleton_iff.1 h']
exact h
