empty_infinite_Theory_isComplete — Mathlib

English

The theory of infinite models in the empty language is complete; i.e., among sentences of the empty language, every sentence is decided by the theory of infinite models.

Русский

Теория бесконечных моделей пустого языка полна; то есть любая формула без символов отношений определяется теорией бесконечных моделей.

LaTeX

$$$\\text{Language.empty.infiniteTheory}.\\text{IsComplete}.$$$

Lean4

theorem empty_infinite_Theory_isComplete : Language.empty.infiniteTheory.IsComplete :=
  (empty_theory_categorical.{0} ℵ₀ _).isComplete ℵ₀ _ le_rfl (by simp)
    ⟨by
      haveI : Language.empty.Structure ℕ := emptyStructure
      exact ((model_infiniteTheory_iff Language.empty).2 (inferInstanceAs (Infinite ℕ))).bundled⟩
    fun M => (model_infiniteTheory_iff Language.empty).1 M.is_model

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