Lω₁ω Theories and Semantic Entailment

This file defines theories, models, semantic entailment, and elementary equivalence in Lω₁ω (countable infinitary logic with countable conjunctions/disjunctions).

Main Definitions

• Theoryω: A theory in Lω₁ω is a set of sentences.
• Theoryω.Model: A structure M is a model of theory T if it satisfies all sentences in T.
• Theoryω.IsSatisfiableIn: T has a model in a selected carrier universe.
• LomegaEquiv: Lω₁ω-elementary equivalence between structures.

Main Results

• Theoryω.Model.empty: The empty theory has every structure as a model.
• Theoryω.Model.mono: Models are monotone: if T ⊆ T' and M ⊨ T', then M ⊨ T.
• LomegaEquiv.refl, LomegaEquiv.symm, LomegaEquiv.trans: LomegaEquiv is an equivalence relation.
• LomegaEquiv.of_equiv: Isomorphic structures are Lω₁ω-equivalent.

References

• [Mar16]
• [KK04]

Theories

@[reducible, inline]

abbrev FirstOrder.Language.Theoryω (L : Language) : Type (max u v)

A theory in Lω₁ω is a set of Lω₁ω sentences.

Equations

• L.Theoryω = Set L.Sentenceω

def FirstOrder.Language.Theoryω.Model {L : Language} (T : L.Theoryω) (M : Type w) [L.Structure M] : Prop

A structure M is a model of theory T if it satisfies all sentences in T.

Equations

• T.Model M = ∀ φ ∈ T, φ.Realize M

theorem FirstOrder.Language.Theoryω.Model.empty {L : Language} (M : Type w) [L.Structure M] : ∅.Model M

The empty theory has every structure as a model.

theorem FirstOrder.Language.Theoryω.Model.mono {L : Language} {T T' : L.Theoryω} (h : T ⊆ T') {M : Type w} [L.Structure M] (hM : T'.Model M) : T.Model M

If T ⊆ T' and M ⊨ T', then M ⊨ T.

def FirstOrder.Language.Theoryω.IsSatisfiableIn {L : Language} (T : L.Theoryω) : Prop

Satisfiability in a selected carrier universe.

The final universe parameter is part of the semantic specification: IsSatisfiableIn.{u, v, w} T asks for a model whose carrier lies in Type w, independently of the universes u, v of the language. Use this form when a construction chooses the model universe; the older IsSatisfiable below is its universe-zero specialization.

Equations

• T.IsSatisfiableIn = ∃ (M : Type ?u.1) (x : L.Structure M) (_ : Nonempty M), T.Model M

def FirstOrder.Language.Theoryω.IsFinitelySatisfiableIn {L : Language} (T : L.Theoryω) : Prop

Finite satisfiability in a selected carrier universe — every ordinarily finite subtheory has a model in Type w.

Equations

• T.IsFinitelySatisfiableIn = ∀ T₀ ⊆ T, Set.Finite T₀ → T₀.IsSatisfiableIn

def FirstOrder.Language.Theoryω.IsSatisfiable {L : Language} (T : L.Theoryω) : Prop

Satisfiability, named rather than written out. The existential-model statement was repeated at every compactness site; spelling it out invites confusing ordinary finite satisfiability with the A-finite kind, which are different hypotheses. Named after Mathlib's Theory.IsSatisfiable for the finitary case.

This published predicate retains its original universe-zero meaning. Constructions that select a different model universe should use IsSatisfiableIn.

Equations

• T.IsSatisfiable = ∃ (M : Type) (x : L.Structure M) (_ : Nonempty M), T.Model M

def FirstOrder.Language.Theoryω.IsFinitelySatisfiable {L : Language} (T : L.Theoryω) : Prop

Finite satisfiability — every ordinarily finite subtheory has a model. Contrast AFinitelySatisfiable, the Barwise premise, which quantifies over A-finite subtheories instead; at A = HF the two coincide, and nowhere else.

Equations

• T.IsFinitelySatisfiable = ∀ T₀ ⊆ T, Set.Finite T₀ → T₀.IsSatisfiable

theorem FirstOrder.Language.Theoryω.IsSatisfiableIn.mono {L : Language} {T T' : L.Theoryω} (h : T ⊆ T') (hT' : T'.IsSatisfiableIn) : T.IsSatisfiableIn

Satisfiability in a fixed carrier universe is monotone under shrinking the theory.

theorem FirstOrder.Language.Theoryω.IsSatisfiable.mono {L : Language} {T T' : L.Theoryω} (h : T ⊆ T') (hT' : T'.IsSatisfiable) : T.IsSatisfiable

Isomorphism Invariance of Realization

theorem FirstOrder.Language.BoundedFormulaω.realize_equiv {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] (e : L.Equiv M N) {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) : φ.Realize v xs ↔ φ.Realize (⇑e ∘ v) (⇑e ∘ xs)

Realization of Lω₁ω formulas is preserved by language isomorphisms.

Given an isomorphism e : M ≃[L] N, a formula realized in M with variable assignments v and xs is also realized in N with the transported assignments e ∘ v and e ∘ xs.

Lω₁ω Elementary Equivalence

def FirstOrder.Language.LomegaEquiv (L : Language) (M : Type u_1) (N : Type u_2) [L.Structure M] [L.Structure N] : Prop

Two structures are Lω₁ω-elementarily equivalent if they satisfy the same Lω₁ω sentences.

Equations

• L.LomegaEquiv M N = ∀ (φ : L.Sentenceω), φ.Realize M ↔ φ.Realize N

theorem FirstOrder.Language.LomegaEquiv.refl {L : Language} {M : Type w} [L.Structure M] : L.LomegaEquiv M M

Lω₁ω-equivalence is reflexive.

theorem FirstOrder.Language.LomegaEquiv.symm {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] (h : L.LomegaEquiv M N) : L.LomegaEquiv N M

Lω₁ω-equivalence is symmetric.

theorem FirstOrder.Language.LomegaEquiv.trans {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] {P : Type u_1} [L.Structure P] (h₁ : L.LomegaEquiv M N) (h₂ : L.LomegaEquiv N P) : L.LomegaEquiv M P

Lω₁ω-equivalence is transitive.

theorem FirstOrder.Language.LomegaEquiv.of_equiv {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] (e : L.Equiv M N) : L.LomegaEquiv M N

Isomorphic structures are Lω₁ω-equivalent.

The proof transports variable assignments along the isomorphism using BoundedFormulaω.realize_equiv, then observes that e ∘ Empty.elim = Empty.elim and e ∘ Fin.elim0 = Fin.elim0 since both domains are empty.

Invariance under Isomorphism

theorem FirstOrder.Language.Theoryω.Model.of_equiv {L : Language} {T : L.Theoryω} {M N : Type w} [L.Structure M] [L.Structure N] (hM : T.Model M) (e : L.Equiv M N) : T.Model N

Models of a theory are preserved under isomorphism.