isSatisfiable_empty

Mathlib.ModelTheory.Satisfiability

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Theory.isSatisfiable_empty

English

The empty theory in any language is satisfiable; there exists a model of the empty theory.

Русский

Пустая теория по любому языку удовлетворима; существует модель пустой теории.

LaTeX

$$$\\text{IsSatisfiable}(\\emptyset)\\; =\\; \\text{true}$$$

Lean4

theorem isSatisfiable_empty (L : Language.{u, v}) : IsSatisfiable (∅ : L.Theory) :=
  ⟨default⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru