Lω₁ω Semantics — compatibility facade over the fixed-carrier semantics

The three realization definitions are no longer given here. They come from Mathlib.ModelTheory.Infinitary.Semantics, whose BoundedFormulaInf.Realize is the single structural recursion serving every index carrier. This file re-exports that semantics under the qualified names the project already uses, and keeps only what Mathlib does not provide.

Why the definitions had to be adopted, not merely paralleled

Lomega1omega/Syntax.lean already identifies BoundedFormulaω with BoundedFormulaInf ℕ definitionally. Keeping a separate recursive Realize here would leave two definitionally distinct semantics for one and the same formula type: dot-notation φ.Realize resolves through the head symbol to BoundedFormulaInf.Realize, while the qualified BoundedFormulaω.Realize would name the other one. Every later operation would then have to pick, and would pick wrong.

What this file still owns

• the qualified Realize names, as reducible aliases — 100-odd files name BoundedFormulaω.Realize / Formulaω.Realize / Sentenceω.Realize explicitly, many in @-applied form, so the aliases reproduce Mathlib's semantics at the project's historical argument order;
• compatibility wrappers carrying the project's realization theorem names, with the project's explicit argument convention (Mathlib states these with implicit arguments);
• realization for the connectives Mathlib does not define: and/or/iff and the Encodable-indexed einf/esup with their explicit-encoding forms;
• the ⊨ω notation.

The gates at the end certify by Iff.rfl — no rewriting, no casts — that each alias is the Mathlib semantics, and that the historical Fin.elim0 spellings of the arity-0 cases still agree with Mathlib's default.

@[reducible, inline]

abbrev FirstOrder.Language.BoundedFormulaω.Realize {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) : Prop

Realization of a bounded Lω₁ω formula, as a qualified name. Mathlib's BoundedFormulaInf.Realize is the definition; this alias is @[reducible] and reproduces the project's historical argument order L M inst α n φ v xs.

Equations

• φ.Realize v xs = FirstOrder.Language.BoundedFormulaInf.Realize φ v xs

Primitive connectives

Mathlib states each of these with implicit arguments; the project's consumers supply them explicitly (realize_rel R ts, realize_imp φ ψ, …), so the wrappers keep that convention.

theorem FirstOrder.Language.BoundedFormulaω.realize_falsum {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} : falsum.Realize v xs ↔ False

theorem FirstOrder.Language.BoundedFormulaω.realize_bot {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} : ⊥.Realize v xs ↔ False

theorem FirstOrder.Language.BoundedFormulaω.realize_equal {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {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₂

theorem FirstOrder.Language.BoundedFormulaω.realize_rel {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {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)

theorem FirstOrder.Language.BoundedFormulaω.realize_imp {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaω α n) : (φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs

theorem FirstOrder.Language.BoundedFormulaω.realize_all {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormulaω α (n + 1)) : φ.all.Realize v xs ↔ ∀ (x : M), φ.Realize v (Fin.snoc xs x)

theorem FirstOrder.Language.BoundedFormulaω.realize_iSup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φs : ℕ → L.BoundedFormulaω α n) : (iSup φs).Realize v xs ↔ ∃ (i : ℕ), (φs i).Realize v xs

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

theorem FirstOrder.Language.BoundedFormulaω.realize_top {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} : ⊤.Realize v xs ↔ True

theorem FirstOrder.Language.BoundedFormulaω.realize_not {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormulaω α n) : φ.not.Realize v xs ↔ ¬φ.Realize v xs

theorem FirstOrder.Language.BoundedFormulaω.realize_ex {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ : L.BoundedFormulaω α (n + 1)) : φ.ex.Realize v xs ↔ ∃ (x : M), φ.Realize v (Fin.snoc xs x)

Connectives the project owns

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.realize_and {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} (φ ψ : L.BoundedFormulaω α n) : (φ.and ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.realize_einf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {ι : Type u_1} [Encodable ι] (φs : ι → L.BoundedFormulaω α n) : (einf φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.realize_esup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {v : α → M} {xs : Fin n → M} {ι : Type u_1} [Encodable ι] (φs : ι → L.BoundedFormulaω α n) : (esup φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs

@[reducible, inline]

abbrev FirstOrder.Language.Formulaω.Realize {L : Language} {M : Type w} [L.Structure M] {α : Type u'} (φ : L.Formulaω α) (v : α → M) : Prop

Realization of an Lω₁ω formula, as a qualified name. Mathlib's FormulaInf.Realize is the definition; it fills the arity-0 valuation with default, which is definitionally the project's historical Fin.elim0 (gated below).

Equations

• φ.Realize v = FirstOrder.Language.FormulaInf.Realize φ v

theorem FirstOrder.Language.Formulaω.realize_def {L : Language} {M : Type w} [L.Structure M] {α : Type u'} (φ : L.Formulaω α) (v : α → M) : φ.Realize v ↔ BoundedFormulaω.Realize φ v Fin.elim0

The level-crossing lemma: formula realization is bounded-formula realization at the empty tuple.

FormulaInf.Realize is a plain definition upstream, not a reducible abbreviation (matching the finitary Formula.Realize), so neither rw nor simp can see a BoundedFormulaω realization lemma through it. Supply this lemma explicitly — simp only [Formulaω.realize_def, realize_not] — instead of crossing that abstraction boundary. Deliberately not @[simp]: the formula-level lemmas below are the normal interface, and this escape hatch should be visible where it is used.

@[simp]

theorem FirstOrder.Language.Formulaω.realize_not {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {φ : L.Formulaω α} {v : α → M} : Realize (BoundedFormulaω.not φ) v ↔ ¬φ.Realize v

@[simp]

theorem FirstOrder.Language.Formulaω.realize_bot {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} : ⊥.Realize v ↔ False

@[simp]

theorem FirstOrder.Language.Formulaω.realize_top {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} : ⊤.Realize v ↔ True

@[simp]

theorem FirstOrder.Language.Formulaω.realize_imp {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} (φ ψ : L.Formulaω α) : Realize (BoundedFormulaω.imp φ ψ) v ↔ φ.Realize v → ψ.Realize v

@[simp]

theorem FirstOrder.Language.Formulaω.realize_inf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} (φ ψ : L.Formulaω α) : (φ ⊓ ψ).Realize v ↔ φ.Realize v ∧ ψ.Realize v

@[simp]

theorem FirstOrder.Language.Formulaω.realize_sup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} (φ ψ : L.Formulaω α) : (φ ⊔ ψ).Realize v ↔ φ.Realize v ∨ ψ.Realize v

@[simp]

theorem FirstOrder.Language.Formulaω.realize_einf {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {ι : Type u_1} [Encodable ι] (φs : ι → L.Formulaω α) : Realize (BoundedFormulaω.einf φs) v ↔ ∀ (i : ι), (φs i).Realize v

@[simp]

theorem FirstOrder.Language.Formulaω.realize_esup {L : Language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {ι : Type u_1} [Encodable ι] (φs : ι → L.Formulaω α) : Realize (BoundedFormulaω.esup φs) v ↔ ∃ (i : ι), (φs i).Realize v

@[reducible, inline]

abbrev FirstOrder.Language.Sentenceω.Realize {L : Language} (φ : L.Sentenceω) (M : Type w) [L.Structure M] : Prop

Truth of an Lω₁ω sentence in a structure, as a qualified name. Mathlib's SentenceInf.Realize is the definition.

Equations

• φ.Realize M = FirstOrder.Language.SentenceInf.Realize φ M

theorem FirstOrder.Language.Sentenceω.realize_def {L : Language} (φ : L.Sentenceω) (M : Type w) [L.Structure M] : φ.Realize M ↔ BoundedFormulaω.Realize φ Empty.elim Fin.elim0

The level-crossing lemma: sentence truth is bounded-formula realization at the empty valuation and the empty tuple. See Formulaω.realize_def for why this is needed and why it is not a simp lemma.

def FirstOrder.Language.Sentenceω.«term_⊨ω_» : Lean.TrailingParserDescr

Notation for a structure satisfying a sentence.

Equations

• One or more equations did not get rendered due to their size.

Facade semantics gates

Each must close by Iff.rfl — no change, no rewriting, no explicit cast. That is what certifies that the qualified ω names are Mathlib's semantics rather than a parallel copy of it, and that the arity-0 spellings the project has used throughout (Fin.elim0, Empty.elim) still agree with Mathlib's default.