Omitting types in countable fragments

A satisfiable theory of sentences in a countable formation-closed fragment has a countable nonempty model omitting any countable family of partial types in the fragment, provided none is isolated over the theory in that fragment. The model may be constructed in any universe. Consequently a partial type realized in every countable nonempty model is isolated. Over a language with countably many symbols, applying the theorem to the first-order image fragment gives the first-order omitting types theorem, for a first-order theory satisfiable in the sense of Mathlib's Theory.IsSatisfiable and first-order partial types not isolated by a first-order formula modulo the theory.

The key refutation lemma applies to the consistency property of satisfiable finite instances. Projecting those instances onto a prescribed tuple of Henkin constants gives a consistent formula of the fragment. Non-isolation supplies a model and a tuple satisfying that formula but refuting a member of the type. The projection theorem then interprets all the constants, even when the prescribed tuple repeats a constant. The model-existence theorem with omission requests supplies the final model.

Main results

• FirstOrder.Language.Theoryω.exists_countable_model_omitting: the omitting types theorem for a countable formation-closed fragment.
• FirstOrder.Language.Theoryω.isolatesIn_of_realized_in_every_countable_model: a partial type realized in every countable nonempty model of the theory is isolated.
• FirstOrder.Language.Theory.exists_countable_model_omitting: the first-order omitting types theorem.

References

• D. Marker, Lectures on Infinitary Model Theory, Cambridge University Press, 2016, Chapter 4.
• H. J. Keisler, Model Theory for Infinitary Logic, North-Holland, 1971.

theorem FirstOrder.Language.ConsistencyProperty.exists_insert_not_mem_ofSatisfiable {L : Language} {A : L.Fragment} {T : L.Theoryω} (hA : A.FormationClosed) (hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A) {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (hp : ∀ ψ ∈ p, ⟨n, ψ⟩ ∈ A) (hnp : ¬Theoryω.IsolatesIn A T p) {s : (L.withConstants ℕ).Theoryω} (hs : s ∈ (ofSatisfiable T A hA hT).sets) (c : Fin n → ℕ) : ∃ ψ ∈ p, insert (BoundedFormulaInf.not (BoundedFormulaInf.instConstants ψ c)) s ∈ (ofSatisfiable T A hA hT).sets

A non-isolated type can be refuted at every tuple of Henkin constants in every member of the consistency property of satisfiable finite instances. No countability is needed for this refutation step.

theorem FirstOrder.Language.Theoryω.exists_countable_model_omitting {L : Language} {A : L.Fragment} {T : L.Theoryω} (hAc : (↑A).Countable) (hA : A.FormationClosed) (hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A) (hTs : T.IsSatisfiable) {ι : Type u_1} [Countable ι] {n : ι → ℕ} (p : (i : ι) → Set (L.BoundedFormulaω Empty (n i))) (hp : ∀ (i : ι), ∀ ψ ∈ p i, ⟨n i, ψ⟩ ∈ A) (hnp : ∀ (i : ι), ¬IsolatesIn A T (p i)) : ∃ (M : Type w) (x : L.Structure M), Countable M ∧ Nonempty M ∧ T.Model M ∧ ∀ (i : ι), OmitsType M (p i)

The omitting types theorem for a countable formation-closed fragment. A satisfiable theory of sentences of the fragment has a countable nonempty model, in any universe, omitting any countable family of partial types in the fragment, none isolated over the theory in the fragment. Countability of the language follows from countability and formation closure of the fragment.

theorem FirstOrder.Language.Theoryω.isolatesIn_of_realized_in_every_countable_model {L : Language} {A : L.Fragment} {T : L.Theoryω} (hAc : (↑A).Countable) (hA : A.FormationClosed) (hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A) (hTs : T.IsSatisfiable) {n : ℕ} {p : Set (L.BoundedFormulaω Empty n)} (hp : ∀ ψ ∈ p, ⟨n, ψ⟩ ∈ A) (h : ∀ (M : Type w) [inst : L.Structure M] [Countable M] [Nonempty M], T.Model M → ¬OmitsType M p) : IsolatesIn A T p

A partial type in a countable formation-closed fragment that is realized in every countable nonempty model of a satisfiable theory of the fragment is isolated over that theory. It suffices to test models in any one universe.

theorem FirstOrder.Language.Theory.exists_countable_model_omitting {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] {T : L.Theory} (hT : T.IsSatisfiable) {ι : Type u_1} [Countable ι] {n : ι → ℕ} (p : (i : ι) → Set (L.BoundedFormula Empty (n i))) (hnp : ∀ (i : ι), ¬∃ (φ : L.BoundedFormula Empty (n i)), (insert φ.exs T).IsSatisfiable ∧ ∀ ψ ∈ p i, T ⊨ᵇ (φ.imp ψ).alls) : ∃ (M : Type w) (x : L.Structure M), Countable M ∧ Nonempty M ∧ M ⊨ T ∧ ∀ (i : ι) (a : Fin (n i) → M), ∃ ψ ∈ p i, ¬ψ.Realize Empty.elim a

The first-order omitting types theorem. Over a language with countably many function and relation symbols, a satisfiable first-order theory T has a countable nonempty model, in any universe, omitting any countable family of first-order partial types none of which is isolated modulo T: for no formula φ is T together with the existential closure of φ satisfiable while T models the universal closure of φ → ψ for every ψ in the type.