mem_or_not_mem

Mathlib.ModelTheory.Satisfiability

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

English

In completeTheory, for any sentence φ, either φ is in the theory or φ.not is.

Русский

Для полной теории φ или в теории, либо φ.not.

LaTeX

$$$φ \\in \\text{completeTheory}(M) \\lor φ.not \\in \\text{completeTheory}(M)$$$

Lean4

theorem mem_or_not_mem (h : T.IsMaximal) (φ : L.Sentence) : φ ∈ T ∨ φ.not ∈ T :=
  h.2 φ

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

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

Разделы

Аффилиация

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