Karp Completeness

This file states the completeness theorem for Lω₁ω: a sentence that belongs to some consistency property has a model.

Main Results

• karp_completeness: If φ belongs to some consistency property, then φ has a model.
• omitting_types: The omitting types theorem for Lω₁ω.

References

• [Mar16]
• [KK04]

theorem FirstOrder.Language.karp_completeness {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) (h : ∃ (C : L.ConsistencyPropertyEq), {φ} ∈ C.sets) : ∃ (M : Type u) (x : L.Structure M) (_ : Countable M), φ.Realize M

Karp Completeness: A sentence in a countable language that belongs to some consistency property with equality axioms has a countable model.

This is a sentence-level consequence of the model existence theorem.

def FirstOrder.Language.OmitsType {L : Language} (M : Type u_1) [L.Structure M] (p : Set (L.Formulaω (Fin 1))) : Prop

A type (set of formulas in one free variable) is omitted by a structure M if no element of M realizes all formulas in the type simultaneously.

Equations

• FirstOrder.Language.OmitsType M p = ∀ (m : M), ∃ φ ∈ p, ¬φ.Realize fun (x : Fin 1) => m

theorem FirstOrder.Language.omitting_types {L : Language} [Countable ((l : ℕ) × L.Functions l)] [Countable ((l : ℕ) × L.Relations l)] (T : L.Theoryω) (_hT_countable : Set.Countable T) (Γ : Set (Set (L.Formulaω (Fin 1)))) (hT : ∃ (C : L.ConsistencyPropertyEq), T ∈ C.sets) (_hΓ : Γ.Countable) (h_not_isolated : ∀ p ∈ Γ, ∀ (C : L.ConsistencyPropertyEq) (φ : L.Formulaω (Fin 1)), T ∪ {(BoundedFormulaω.relabel Sum.inr φ).ex} ∈ C.sets → ∃ ψ ∈ p, T ∪ {(BoundedFormulaω.relabel Sum.inr (BoundedFormulaω.and φ (BoundedFormulaω.not ψ))).ex} ∈ C.sets) : ∃ (M : Type u) (x : L.Structure M) (_ : Countable M), T.Model M ∧ ∀ p ∈ Γ, OmitsType M p

Omitting Types Theorem for Lω₁ω.

Given a countable consistent theory T in a countable language and a countable collection of types to omit (each of which is not isolated by any formula consistent with T), there exists a countable model of T that omits all the given types.

This is a powerful generalization of the standard omitting types theorem from first-order logic to the countable infinitary setting.