Model Existence Theorem

This file states the model existence theorem for Lω₁ω: any set of sentences that belongs to a consistency property has a countable model.

Main Results

• model_existence: If S is consistent (belongs to a consistency property), then S has a countable model. (Marker Theorem 4.1.2 / Keisler)

References

• [Mar16], Theorem 4.1.2
• [Kei71]

theorem FirstOrder.Language.model_existence {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (C : L.ConsistencyPropertyEq) (S : Set L.Sentenceω) (hS : S ∈ C.sets) (_hS_countable : S.Countable) : ∃ (M : Type u) (x : L.Structure M) (_ : Countable M), Theoryω.Model S M

Model Existence Theorem for Lω₁ω (Marker Theorem 4.1.2).

If a countable set S of Lω₁ω sentences in a countable language belongs to a consistency property with equality axioms, then S has a countable model.

The proof proceeds by a Henkin-style construction:

1. Extend the language with countably many new constants
2. Extend S to a maximal consistent set S* using a priority argument
3. Build a term model from S*
4. Verify the model satisfies all sentences in S

The countability assumptions on the language and S are essential: without them, a consistent set like {c_i ≠ c_j | i ≠ j} for uncountably many constants can force any model to be uncountable.

This is the fundamental model-building tool for infinitary logic.

theorem FirstOrder.Language.consistent_theory_has_model {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (C : L.ConsistencyPropertyEq) (T : L.Theoryω) (hT : T ∈ C.sets) (hT_countable : Set.Countable T) : ∃ (M : Type u) (x : L.Structure M) (_ : Countable M), T.Model M

A consistent countable theory in a countable language has a countable model.

This is a direct corollary of model existence.