isComplete — Mathlib

English

Let L be a language and M a nonempty L-structure. Then the complete theory of M is complete; equivalently, for every sentence φ in L, either φ is a theorem of the complete theory of M or its negation is.

Русский

Пусть L — язык, а M — непустая структура над L. Тогда полная теория M является полной; то есть для любой формулы φ языка L выполняется либо φ, либо ¬φ выводимы из полной теории M.

LaTeX

$$$\\bigl( \\text{L.completeTheory } M \\bigr) \\text{ is complete, i.e. } \\forall \\varphi \\in \\text{Sent}(L), \\; (L.completeTheory\\,M) \\models \\varphi \\; \\lor\\; (L.completeTheory\\,M) \\models \\lnot \\varphi.$$$

Lean4

theorem isComplete [Nonempty M] : (L.completeTheory M).IsComplete :=
  (completeTheory.isMaximal L M).isComplete

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