English
Let p be a complete type p ∈ T.CompleteType α. Then there exists a model type M of T such that p is realized in M (i.e., p ∈ T.realizedTypes M α). In other words, every complete type is realizable in some model of T.
Русский
Пусть p — полный тип над теорией T в переменных α. Тогда существует модельный тип M модели T, такая что p реализуется в M (то есть p ∈ T.realizedTypes M α). Другими словами, любой полный тип реализуем в некоторой модели T.
LaTeX
$$$\exists M \text{ with } M \models T \ \,\land\\ p \in T.realizedTypes\ M\ \alpha$$$
Lean4
theorem exists_modelType_is_realized_in (p : T.CompleteType α) :
∃ M : Theory.ModelType.{u, v, max u v w} T, p ∈ T.realizedTypes M α :=
by
obtain ⟨M⟩ := p.isMaximal.1
refine ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), ?_⟩
refine SetLike.ext fun φ => ?_
simp only [CompleteType.mem_typeOf]
refine
(@Formula.realize_equivSentence_symm_con _ ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ M.struc
_ φ).trans
(_root_.trans (_root_.trans ?_ (p.isMaximal.isComplete.realize_sentence_iff φ M))
(p.isMaximal.mem_iff_models φ).symm)
rfl
