L∞ω Theories and Semantic Entailment #

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

Main Definitions #

TheoryInf: A theory in L∞ω is a set of sentences.
TheoryInf.Model: A structure M is a model of theory T if it satisfies all sentences in T.
LinfEquiv: L∞ω-elementary equivalence between structures.

Main Results #

LinfEquiv.refl, LinfEquiv.symm, LinfEquiv.trans: LinfEquiv is an equivalence relation.
LinfEquiv.of_equiv: Isomorphic structures are L∞ω-equivalent.

References #

Theories #

source

@[reducible, inline]

abbrev FirstOrder.Language.TheoryInf (L : Language) :

Type (max (max u v) (u_1 + 1))

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

Equations

L.TheoryInf = Set L.SentenceInf

Instances For

source

def FirstOrder.Language.TheoryInf.Model {L : Language} (T : L.TheoryInf) (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

Instances For

source

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

∅.Model M

The empty theory has every structure as a model.

source

theorem FirstOrder.Language.TheoryInf.Model.mono {L : Language} {T T' : L.TheoryInf} (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.

source

def FirstOrder.Language.TheoryInf.Valid {L : Language} (φ : L.SentenceInf) :

Prop

Semantic entailment from the empty theory: valid sentences.

Equations

FirstOrder.Language.TheoryInf.Valid φ = ∀ (M : Type) [inst : L.Structure M], φ.Realize M

Instances For

Isomorphism Invariance of Realization #

source

theorem FirstOrder.Language.BoundedFormulaInf.realize_equiv {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] (e : L.Equiv M N) {α : Type u_1} {n : ℕ} (φ : L.BoundedFormulaInf α 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 #

source

def FirstOrder.Language.LinfEquiv (L : Language) (M N : Type w) [L.Structure M] [L.Structure N] :

Prop

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

The current definition quantifies over BoundedFormulaInf.{u, v, 0, 0}, pinning the free-variable universe (u') and index-type universe (uι) to 0 for practicality. The uι = 0 choice ensures compatibility with qrank : Ordinal.{0} (whose suprema at iSup/iInf nodes must live in a fixed universe) and suffices for all standard applications (any countable or Type 0 index type falls within this definition).

Equations

L.LinfEquiv M N = ∀ (φ : L.BoundedFormulaInf Empty 0), FirstOrder.Language.SentenceInf.Realize φ M ↔ FirstOrder.Language.SentenceInf.Realize φ N

Instances For

source

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

L.LinfEquiv M M

L∞ω-equivalence is reflexive.

source

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

L.LinfEquiv N M

L∞ω-equivalence is symmetric.

source

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

L.LinfEquiv M P

L∞ω-equivalence is transitive.

source

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

L.LinfEquiv M N

Isomorphic structures are L∞ω-equivalent.

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

Universe-correct L∞ω Elementary Equivalence #

source

def FirstOrder.Language.LinfEquivW (L : Language) (M N : Type w) [L.Structure M] [L.Structure N] :

Prop

L∞ω-elementary equivalence with index types matching the structure universe.

Unlike LinfEquiv which pins uι = 0, this version uses BoundedFormulaInf.{u, v, 0, w} so that index types for iSup/iInf may be any Type w. The backward direction of Karp's theorem constructs formulas with iInf indexed by N : Type w, which needs uι = w.

Equations