English
Let T be a theory in a language L. If T is κ-categorical for some κ with ℵ0 ≤ κ and a size bound relating L.cards to κ holds, T is satisfiable and every model type of T is infinite, then T is complete; i.e., for every sentence φ, either T ⊨ φ or T ⊨ ¬φ.
Русский
Пусть T — теория в языке L. Если T является κ-категорической для некоторого κ с ℵ0 ≤ κ и выполняется ограничение по кардиналам между L.card и κ, T удовлетворима, и все модели T бесконечны, тогда T полнота; то есть для каждого предложения φ верно либо T ⊨ φ, либо T ⊨ ¬φ.
LaTeX
$$$\\bigl( \\kappa\\text{-Categorical}(T) \\bigr) \\land (\\aleph_0 \\le \\kappa) \\land (\\mathrm{lift}\\, L\\text{.card} \\le \\mathrm{lift}\\, \\kappa) \\land T\\text{.IsSatisfiable} \\land \\bigl(\\forall M : T.ModelType, \\mathrm{Infinite}(M.Carrier)\\bigr) \\Rightarrow \\forall \\varphi,\\; T \\models \\varphi \\lor T \\models \\lnot \\varphi.$$$
Lean4
/-- The Łoś–Vaught Test : a criterion for categorical theories to be complete. -/
theorem isComplete (h : κ.Categorical T) (h1 : ℵ₀ ≤ κ) (h2 : Cardinal.lift.{w} L.card ≤ Cardinal.lift.{max u v} κ)
(hS : T.IsSatisfiable) (hT : ∀ M : Theory.ModelType.{u, v, max u v} T, Infinite M) : T.IsComplete :=
⟨hS, fun φ => by
obtain ⟨_, _⟩ := Theory.exists_model_card_eq ⟨hS.some, hT hS.some⟩ κ h1 h2
rw [Theory.models_sentence_iff, Theory.models_sentence_iff]
by_contra! con
obtain ⟨⟨MF, hMF⟩, MT, hMT⟩ := con
rw [Sentence.realize_not, Classical.not_not] at hMT
refine hMF ?_
haveI := hT MT
haveI := hT MF
obtain ⟨NT, MNT, hNT⟩ := exists_elementarilyEquivalent_card_eq L MT κ h1 h2
obtain ⟨NF, MNF, hNF⟩ := exists_elementarilyEquivalent_card_eq L MF κ h1 h2
obtain ⟨TF⟩ := h (MNT.toModel T) (MNF.toModel T) hNT hNF
exact
((MNT.realize_sentence φ).trans ((StrongHomClass.realize_sentence TF φ).trans (MNF.realize_sentence φ).symm)).1
hMT⟩
