Semantics of infinitary first-order formulas

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

Quantification extends the bound-variable valuation at the last slot, with Fin.snoc, as for finitary formulas.

Main definitions

• FirstOrder.Language.BoundedFormulaInf.Realize: realization with free-variable and bound-variable valuations.
• FirstOrder.Language.FormulaInf.Realize and FirstOrder.Language.SentenceInf.Realize, with the low-priority simp lemmas FormulaInf.realize_def and SentenceInf.realize_def reducing them to bounded-formula realization once no formula- or sentence-level lemma applies.

Main results

• One simp lemma per constructor and derived connective, each generic in the carrier and its universe: realize_iSup, realize_iInf, realize_inf, realize_iff, realize_alls, ….
• FirstOrder.Language.BoundedFormula.realize_toInf: the finitary embedding preserves realization, at every carrier.
• FirstOrder.Language.Sentence.realize_toInf: the sentence-level finitary embedding preserves satisfaction.

References

• The finite conjunction lemma BoundedFormulaInf.realize_foldr_inf follows Mathlib's BoundedFormula.realize_foldr_inf in Mathlib/ModelTheory/Semantics.lean (Aaron Anderson).
• Ported from cameronfreer/infinitary-logic at commit 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, whose infinitary semantics is Mathlib/ModelTheory/Infinitary/Semantics.lean in leanprover-community/mathlib4#42758 (Apache 2.0) at commit 2264c2c872bb642ab519aa2288d53110f07af37d.
• Divergences from these sources: realization laws for the added binary connectives (realize_inf, realize_sup, realize_iff); FormulaInf.Realize and SentenceInf.Realize are not exposed, with the simp bridges FormulaInf.realize_def and SentenceInf.realize_def (at priority low, so default-priority facts stated at the formula or sentence level are tried first) in their place; realize_alls and realize_exs are stated for bounded realization at the empty valuation of the bound-variable slots, their simp-normal form.

Implementation notes

BoundedFormulaInf.Realize is exposed, as in the sources. Its pattern-matching definition compiles through an auxiliary matcher, which is named BoundedFormulaInf.Realize.match_1 only when the body is exposed (otherwise the matcher gets a private, module-specific name). Exposing it keeps that name stable, so that a downstream restatement of the same definition can be compared with this one constant by constant.

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.

@[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

@[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₂

@[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)

@[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

@[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)

@[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 statement, generic in the carrier and its universe.

@[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 statement, generic in the carrier and its universe.

@[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

@[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

@[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

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_inf {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φ ψ : L.BoundedFormulaInf ι α n} : (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_foldr_inf {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} (l : List (L.BoundedFormulaInf ι α n)) : (List.foldr (fun (x1 x2 : L.BoundedFormulaInf ι α n) => x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs

A finite conjunction holds exactly when every formula in the list holds.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_sup {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φ ψ : L.BoundedFormulaInf ι α n} : (φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_iff {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {φ ψ : L.BoundedFormulaInf ι α n} : (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

@[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)

@[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.

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, which has no bound-variable slots.

@[simp]

theorem FirstOrder.Language.FormulaInf.realize_def {L : Language} {ι : Type uι} {α : Type u'} {M : Type w} [L.Structure M] (φ : L.FormulaInf ι α) (v : α → M) : φ.Realize v ↔ BoundedFormulaInf.Realize φ v default

A formula is realized when it is realized as a bounded formula with no bound variables, so the realization lemmas for bounded formulas apply to formulas. The priority is low so that simp tries default-priority facts stated at the formula level (hypotheses passed to simp, downstream simp lemmas) before descending to bounded realization.

@[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} : Realize φ.alls v default ↔ ∀ (xs : Fin n → M), φ.Realize v xs

Closing all bound-variable slots universally realizes as universal quantification over the valuations of those slots.

@[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} : Realize φ.exs v default ↔ ∃ (xs : Fin n → M), φ.Realize v xs

Closing all bound-variable slots existentially realizes as existential quantification over the valuations of those slots.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_exsLast {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {k : ℕ} {φ : L.BoundedFormulaInf ι α (n + k)} {v : α → M} {xs : Fin n → M} : φ.exsLast.Realize v xs ↔ ∃ (ys : Fin k → M), φ.Realize v (Fin.append xs ys)

Quantifying the last k slots existentially realizes as existential quantification over the valuations ys of those slots, appended to the valuation of the remaining slots.

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.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_def {L : Language} {ι : Type uι} (φ : L.SentenceInf ι) (M : Type w) [L.Structure M] : φ.Realize M ↔ FormulaInf.Realize φ Empty.elim

A sentence is realized in a structure when it is realized as a formula under the empty valuation of its free variables. The priority is low for the same reason as FormulaInf.realize_def.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_inf {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] {φ ψ : L.SentenceInf ι} : (φ ⊓ ψ).Realize M ↔ φ.Realize M ∧ ψ.Realize M

A conjunction of sentences holds exactly when both sentences hold.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_sup {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] {φ ψ : L.SentenceInf ι} : (φ ⊔ ψ).Realize M ↔ φ.Realize M ∨ ψ.Realize M

A disjunction of sentences holds exactly when one of the sentences holds.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_iInf {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] {φs : ι → L.SentenceInf ι} : Realize (BoundedFormulaInf.iInf φs) M ↔ ∀ (i : ι), (φs i).Realize M

An infinitary conjunction of sentences holds exactly when every sentence holds.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_not {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] {φ : L.SentenceInf ι} : Realize (BoundedFormulaInf.not φ) M ↔ ¬φ.Realize M

The negation of a sentence holds exactly when the sentence does not hold.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_imp {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] {φ ψ : L.SentenceInf ι} : Realize (BoundedFormulaInf.imp φ ψ) M ↔ φ.Realize M → ψ.Realize M

An implication of sentences holds exactly when its conclusion holds whenever its hypothesis does.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_equal_self {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] (t : L.Term (Empty ⊕ Fin 0)) : Realize (BoundedFormulaInf.equal t t) M

Every closed term equals itself in every structure.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_bot {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] : ⊥.Realize M ↔ False

The false sentence holds in no structure.

@[simp]

theorem FirstOrder.Language.SentenceInf.realize_iSup {L : Language} {ι : Type uι} {M : Type w} [L.Structure M] {φs : ι → L.SentenceInf ι} : Realize (BoundedFormulaInf.iSup φs) M ↔ ∃ (i : ι), (φs i).Realize M

An infinitary disjunction of sentences holds exactly when some sentence holds.

@[simp]

theorem FirstOrder.Language.Sentence.realize_toInf {L : Language} {ι : Type uι} (φ : L.Sentence) (M : Type w) [L.Structure M] : SentenceInf.Realize (BoundedFormula.toInf φ) M ↔ M ⊨ φ

The finitary embedding of a sentence preserves satisfaction, at every branching carrier.