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.

Model existence over arbitrary (possibly uncountable) languages

The countability assumptions of model_existence are entirely cosmetic — they secure only the countable model conclusion. The model-building core carries no countability hypothesis: ConsistencyProperty.exists_maximal (Zorn), TermModel, termModelStructure, and truthLemma have no Countable requirement anywhere in Construction.lean / ConsistencyProperty.lean (the sole Countable in those files, at Construction.lean:344, is the Countable (TermModel) instance, used only to certify a countable output). model_existence's own _hS_countable : S.Countable argument is underscore-prefixed — genuinely unused.

So dropping the gate yields model existence over an arbitrary language; the term model is uncountable exactly when the language is. This is the cardinal-agnostic backend for the EM/Skolem-hull realizability project (Phase 3 spike of the Morley–Hanf plan). Output-size refinements (#M ≥ #J) are deferred — the goal here is modest (∃ M, M ⊨ S).

theorem FirstOrder.Language.model_existence_uncountable_language {L : Language} (C : L.ConsistencyPropertyEq) (S : Set L.Sentenceω) (hS : S ∈ C.sets) : ∃ (M : Type u) (x : L.Structure M), Theoryω.Model S M

Model existence over an arbitrary language (cardinal-agnostic core of model_existence). If S belongs to a consistency property with equality, then S has a model — with no countability hypothesis on the language or S, and no cardinality claim on the model. The model is the Henkin term model of a maximal consistent extension of S; identical proof to model_existence minus the Countable M certificate.

theorem FirstOrder.Language.consistent_theory_has_model_uncountable_language {L : Language} (C : L.ConsistencyPropertyEq) (T : L.Theoryω) (hT : T ∈ C.sets) : ∃ (M : Type u) (x : L.Structure M), T.Model M

A consistent theory over an arbitrary language has a model (no countability assumption). Corollary of model_existence_uncountable_language.