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.
• 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.

noncomputable def FirstOrder.Language.Theoryω.conjunction {L : Language} (T : L.Theoryω) (hT : Set.Countable T) : L.Sentenceω

A countable theory as one sentence: the countable conjunction of an enumeration (a tautology for the empty theory). Realization is exactly theory modelhood (realize_conjunction_iff), so single-sentence results transport to countable theories.

Equations

• T.conjunction hT = if h : Set.Nonempty T then FirstOrder.Language.BoundedFormulaω.iInf ⋯.choose else FirstOrder.Language.BoundedFormulaω.falsum.imp FirstOrder.Language.BoundedFormulaω.falsum

theorem FirstOrder.Language.Theoryω.realize_conjunction_iff {L : Language} (T : L.Theoryω) (hT : Set.Countable T) (M : Type w) [L.Structure M] : (T.conjunction hT).Realize M ↔ T.Model M

Realizing the conjunction of a countable theory is modeling the theory.

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.