Documentation

Mathlib.ModelTheory.Infinitary.Semantics

Semantics of infinitary first-order formulas #

This file defines realization of L_{∞ω} formulas in a structure, with simp lemmas for every constructor and derived connective. Because the branching carrier is a type parameter, each realization lemma is a single statement generic in the carrier and its universe — there is no separate L_{ω₁ω} semantics, and no universe-specialized lemma set.

Main definitions #

Main statements #

Realization of the coded connectives and of carrier transport is in Infinitary/Reindex.lean.

source
def FirstOrder.Language.BoundedFormulaInf.Realize {L : Language} {ι : Type uι} {α : Type u'} {M : Type w} [L.Structure M] {n : ℕ} :
L.BoundedFormulaInf ι α n → (α → M) → (Fin n → M) → Prop

Realization of an infinitary bounded formula in a structure, given valuations of the free and bound variables. One recursion serves every carrier.

Equations
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_falsum {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} :
    falsum.Realize v xs ↔ False
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_equal {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {t₁ t₂ : L.Term (α ⊕ Fin n)} :
    (equal t₁ t₂).Realize v xs ↔ Term.realize (Sum.elim v xs) t₁ = Term.realize (Sum.elim v xs) t₂
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_rel {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {l : ℕ} {R : L.Relations l} {ts : Fin l → L.Term (α ⊕ Fin n)} :
    (rel R ts).Realize v xs ↔ Structure.RelMap R fun (i : Fin l) => Term.realize (Sum.elim v xs) (ts i)
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_imp {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φ ψ : L.BoundedFormulaInf ι α n} :
    (φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_all {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φ : L.BoundedFormulaInf ι α (n + 1)} :
    φ.all.Realize v xs ↔ ∀ (y : M), φ.Realize v (Fin.snoc xs y)
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_iSup {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φs : ι → L.BoundedFormulaInf ι α n} :
    (iSup φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs

    Realization of an infinitary disjunction: one equation, generic in the carrier and its universe.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_iInf {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φs : ι → L.BoundedFormulaInf ι α n} :
    (iInf φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

    Realization of an infinitary conjunction: one equation, generic in the carrier and its universe.

    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_not {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φ : L.BoundedFormulaInf ι α n} :
    φ.not.Realize v xs ↔ ¬φ.Realize v xs
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_top {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} :
    ⊤.Realize v xs ↔ True
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_bot {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} :
    ⊥.Realize v xs ↔ False
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormulaInf.realize_ex {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φ : L.BoundedFormulaInf ι α (n + 1)} :
    φ.ex.Realize v xs ↔ ∃ (y : M), φ.Realize v (Fin.snoc xs y)
    source
    @[simp]
    theorem FirstOrder.Language.BoundedFormula.realize_toInf {L : Language} {ι : Type uι} {α : Type u'} {M : Type w} [L.Structure M] {n : ℕ} (φ : L.BoundedFormula α n) (v : α → M) (xs : Fin n → M) :
    φ.toInf.Realize v xs ↔ φ.Realize v xs

    The finitary embedding preserves realization, at every carrier.

    source
    def FirstOrder.Language.FormulaInf.Realize {L : Language} {ι : Type uι} {α : Type u'} {M : Type w} [L.Structure M] (φ : L.FormulaInf ι α) (v : α → M) :
    Prop

    Realization of an L_{∞ω} formula (no free bound variables).

    Equations
    Instances For
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.realize_alls {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {φ : L.BoundedFormulaInf ι α n} {v : α → M} :
      φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.realize_exs {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {φ : L.BoundedFormulaInf ι α n} {v : α → M} :
      φ.exs.Realize v ↔ ∃ (xs : Fin n → M), φ.Realize v xs
      source
      def FirstOrder.Language.SentenceInf.Realize {L : Language} {ι : Type uι} (φ : L.SentenceInf ι) (M : Type w) [L.Structure M] :
      Prop

      Realization of an L_{∞ω} sentence in a structure.

      Equations
      Instances For