Downward Löwenheim-Skolem for Lω₁ω

This file proves the downward Löwenheim-Skolem theorem for Lω₁ω: any Lω₁ω sentence satisfied by a countable model in a countable language has a countable model (in any target universe).

Main Results

• downward_LS_with_naming: Any satisfiable Lω₁ω sentence has a countable model, given a naming function (no countability assumption on the original model).
• downward_LS: Any Lω₁ω sentence satisfied by a countable model ([Countable M]) has a countable model. Uses language extension L[[M]], requiring M countable.

Implementation Notes

The proof constructs a ConsistencyPropertyEq from the given model M using the "true in M" consistency property. To provide witnesses for the C7 quantifier axioms, we extend the language L with constants naming each element of M, then apply the model existence theorem in the extended language, and restrict the resulting countable model back to L.

For languages where every element of M is already named by a closed term (e.g., after Skolemization or in Henkin languages), we can work directly in L without extension using NamingFunction.

References

• [Mar16]
• [KK04]

noncomputable def FirstOrder.Language.namingFunctionWithConstants (L : Language) (M : Type u) [L.Structure M] : (L.withConstants M).NamingFunction M

The naming function for the extended language L[[M]]: each element m : M is named by the constant symbol L.con m, which evaluates to m in the canonical L[[M]]-structure on M.

Equations

• L.namingFunctionWithConstants M = { name := fun (m : M) => FirstOrder.Language.func (Sum.inr m) Fin.elim0, sound := ⋯ }

instance FirstOrder.Language.countable_sum_functions (L₁ : Language) (L₂ : Language) [Countable ((l : ℕ) × L₁.Functions l)] [Countable ((l : ℕ) × L₂.Functions l)] : Countable ((l : ℕ) × (L₁.sum L₂).Functions l)

The sum language L.sum L' has countable function symbols when both L and L' do.

instance FirstOrder.Language.countable_sum_relations (L₁ : Language) (L₂ : Language) [Countable ((l : ℕ) × L₁.Relations l)] [Countable ((l : ℕ) × L₂.Relations l)] : Countable ((l : ℕ) × (L₁.sum L₂).Relations l)

The sum language L.sum L' has countable relation symbols when both L and L' do.

instance FirstOrder.Language.countable_constantsOn_functions (α : Type u_1) [Countable α] : Countable ((l : ℕ) × (constantsOn α).Functions l)

The constantsOn language has countable function symbols when the index type is countable.

instance FirstOrder.Language.countable_constantsOn_relations (α : Type u_1) : Countable ((l : ℕ) × (constantsOn α).Relations l)

The constantsOn language has countable relation symbols (they're all empty).

theorem FirstOrder.Language.downward_LS_with_naming {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) (M : Type u_1) [L.Structure M] (ι : L.NamingFunction M) (hM : φ.Realize M) : ∃ (N : Type u) (x : L.Structure N) (_ : Countable N), φ.Realize N

Downward Löwenheim-Skolem with naming function: If a countable language has a naming function (every element is named by a closed term), then any satisfiable sentence has a countable model.

This is the version that avoids language extension by assuming a naming function already exists. In practice, this applies to Henkin languages and term models.

theorem FirstOrder.Language.downward_LS_theory_with_naming {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (T : L.Theoryω) (M : Type u_1) [L.Structure M] (ι : L.NamingFunction M) (hM : T.Model M) (hT_countable : Set.Countable T) : ∃ (N : Type u) (x : L.Structure N) (_ : Countable N), T.Model N

Downward Löwenheim-Skolem for theories with naming function. A corollary of consistent_theory_has_model.

theorem FirstOrder.Language.downward_LS {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) (M : Type u) [L.Structure M] [Countable M] (hM : φ.Realize M) : ∃ (N : Type u) (x : L.Structure N) (_ : Countable N), φ.Realize N

Downward Löwenheim-Skolem for Lω₁ω: Any satisfiable sentence in a countable language with a countable model has a countable model (in universe u).

The proof extends L with constants for each element of M to form L[[M]], constructs a naming function, applies model existence, then restricts back. The countability condition on M is needed so that L[[M]] remains countable.

For the version without the [Countable M] assumption (but with a naming function already available), see downward_LS_with_naming.

theorem FirstOrder.Language.downward_LS_theory {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (T : L.Theoryω) (M : Type u) [L.Structure M] [Countable M] (hM : T.Model M) (hT_countable : Set.Countable T) : ∃ (N : Type u) (x : L.Structure N) (_ : Countable N), T.Model N

Downward LS for theories: any Lω₁ω theory in a countable language satisfied by a countable model ([Countable M]) has a countable model.