feat(ModelTheory): add syntax and semantics for infinitary logic

Mathlib.lean

@@ -5725,6 +5725,8 @@ public import Mathlib.ModelTheory.Equivalence
 public import Mathlib.ModelTheory.FinitelyGenerated
 public import Mathlib.ModelTheory.Fraisse
 public import Mathlib.ModelTheory.Graph
+public import Mathlib.ModelTheory.Infinitary.Semantics
+public import Mathlib.ModelTheory.Infinitary.Syntax
 public import Mathlib.ModelTheory.LanguageMap
 public import Mathlib.ModelTheory.Order
 public import Mathlib.ModelTheory.PartialEquiv

Mathlib/ModelTheory/Infinitary/Semantics.lean

@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2026 Cameron Freer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Cameron Freer
+-/
+module
+
+public import Mathlib.ModelTheory.Semantics
+public import Mathlib.ModelTheory.Infinitary.Syntax
+
+/-!
+# 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
+
+- `FirstOrder.Language.BoundedFormulaInf.Realize`: realization with free-variable and
+  bound-variable valuations.
+- `FirstOrder.Language.FormulaInf.Realize`, `FirstOrder.Language.SentenceInf.Realize`.
+
+## Main statements
+
+- One `@[simp]` realization lemma per constructor and derived connective, each a single
+  statement generic in the carrier and its universe (`realize_iInf`, `realize_alls`, …).
+- `BoundedFormula.realize_toInf`: the carrier-generic finitary embedding preserves
+  realization.
+
+Realization of the coded connectives and of carrier transport arrives with the follow-up
+transport layer.
+-/
+
+@[expose] public section
+
+universe u v u' uι w
+
+namespace FirstOrder
+
+namespace Language
+
+variable {L : Language.{u, v}} {ι : Type uι} {α : Type u'} {n : ℕ}
+
+namespace BoundedFormulaInf
+
+/-- Realization of an infinitary bounded formula in a structure, given valuations of the free
+and bound variables. One recursion serves every carrier. -/
+def Realize {M : Type w} [L.Structure M] :
+    ∀ {n}, L.BoundedFormulaInf ι α n → (α → M) → (Fin n → M) → Prop
+  | _, .falsum, _, _ => False
+  | _, .equal t₁ t₂, v, xs => t₁.realize (Sum.elim v xs) = t₂.realize (Sum.elim v xs)
+  | _, .rel R ts, v, xs => Structure.RelMap R fun i ↦ (ts i).realize (Sum.elim v xs)
+  | _, .imp φ ψ, v, xs => Realize φ v xs → Realize ψ v xs
+  | _, .all φ, v, xs => ∀ y : M, Realize φ v (Fin.snoc xs y)
+  | _, .iSup φs, v, xs => ∃ i, Realize (φs i) v xs
+  | _, .iInf φs, v, xs => ∀ i, Realize (φs i) v xs
+
+variable {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M}
+
+@[simp]
+theorem realize_falsum : (falsum : L.BoundedFormulaInf ι α n).Realize v xs ↔ False :=
+  Iff.rfl
+
+@[simp]
+theorem realize_equal {t₁ t₂ : L.Term (α ⊕ Fin n)} :
+    (equal t₁ t₂ : L.BoundedFormulaInf ι α n).Realize v xs ↔
+      t₁.realize (Sum.elim v xs) = t₂.realize (Sum.elim v xs) :=
+  Iff.rfl
+
+@[simp]
+theorem realize_rel {l : ℕ} {R : L.Relations l} {ts : Fin l → L.Term (α ⊕ Fin n)} :
+    (rel R ts : L.BoundedFormulaInf ι α n).Realize v xs ↔
+      Structure.RelMap R fun i ↦ (ts i).realize (Sum.elim v xs) :=
+  Iff.rfl
+
+@[simp]
+theorem realize_imp {φ ψ : L.BoundedFormulaInf ι α n} :
+    (φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs :=
+  Iff.rfl
+
+@[simp]
+theorem realize_all {φ : L.BoundedFormulaInf ι α (n + 1)} :
+    φ.all.Realize v xs ↔ ∀ y : M, φ.Realize v (Fin.snoc xs y) :=
+  Iff.rfl
+
+/-- Realization of an infinitary disjunction: one equation, generic in the carrier and its
+universe. -/
+@[simp]
+theorem realize_iSup {φs : ι → L.BoundedFormulaInf ι α n} :
+    (iSup φs).Realize v xs ↔ ∃ i, (φs i).Realize v xs :=
+  Iff.rfl
+
+/-- Realization of an infinitary conjunction: one equation, generic in the carrier and its
+universe. -/
+@[simp]
+theorem realize_iInf {φs : ι → L.BoundedFormulaInf ι α n} :
+    (iInf φs).Realize v xs ↔ ∀ i, (φs i).Realize v xs :=
+  Iff.rfl
+
+@[simp]
+theorem realize_not {φ : L.BoundedFormulaInf ι α n} :
+    φ.not.Realize v xs ↔ ¬φ.Realize v xs :=
+  Iff.rfl
+
+@[simp]
+theorem realize_top : (⊤ : L.BoundedFormulaInf ι α n).Realize v xs ↔ True := by
+  simp [Top.top, BoundedFormulaInf.verum, BoundedFormulaInf.not, Realize]
+
+@[simp]
+theorem realize_bot : (⊥ : L.BoundedFormulaInf ι α n).Realize v xs ↔ False :=
+  Iff.rfl
+
+@[simp]
+theorem realize_ex {φ : L.BoundedFormulaInf ι α (n + 1)} :
+    φ.ex.Realize v xs ↔ ∃ y : M, φ.Realize v (Fin.snoc xs y) := by
+  simp only [BoundedFormulaInf.ex, realize_not, realize_all, not_forall, not_not]
+
+end BoundedFormulaInf
+
+namespace BoundedFormula
+
+/-- The finitary embedding preserves realization, at every carrier. -/
+@[simp]
+theorem realize_toInf {M : Type w} [L.Structure M] :
+    ∀ {n} (φ : L.BoundedFormula α n) (v : α → M) (xs : Fin n → M),
+      (toInf (ι := ι) φ).Realize v xs ↔ φ.Realize v xs := by
+  intro n φ
+  induction φ with
+  | falsum | equal | rel => intro v xs; exact Iff.rfl
+  | imp φ ψ ihφ ihψ =>
+    intro v xs
+    simpa only [toInf, BoundedFormulaInf.realize_imp, BoundedFormula.realize_imp] using
+      imp_congr (ihφ v xs) (ihψ v xs)
+  | all φ ih =>
+    intro v xs
+    simpa only [toInf, BoundedFormulaInf.realize_all, BoundedFormula.realize_all] using
+      forall_congr' fun y ↦ ih v (Fin.snoc xs y)
+
+end BoundedFormula
+
+/-- Realization of an `L_{∞ω}` formula (no free bound variables). -/
+def FormulaInf.Realize {M : Type w} [L.Structure M] (φ : L.FormulaInf ι α) (v : α → M) : Prop :=
+  BoundedFormulaInf.Realize φ v default
+
+section AllsExs
+
+variable {M : Type w} [L.Structure M]
+
+@[simp]
+theorem BoundedFormulaInf.realize_alls {φ : L.BoundedFormulaInf ι α n} {v : α → M} :
+    φ.alls.Realize v ↔ ∀ xs : Fin n → M, φ.Realize v xs := by
+  induction n with
+  | zero => exact Unique.forall_iff.symm
+  | succ n ih =>
+    simp only [BoundedFormulaInf.alls, ih, BoundedFormulaInf.realize_all]
+    exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩
+
+@[simp]
+theorem BoundedFormulaInf.realize_exs {φ : L.BoundedFormulaInf ι α n} {v : α → M} :
+    φ.exs.Realize v ↔ ∃ xs : Fin n → M, φ.Realize v xs := by
+  induction n with
+  | zero => exact Unique.exists_iff.symm
+  | succ n ih =>
+    simp only [BoundedFormulaInf.exs, ih, BoundedFormulaInf.realize_ex]
+    constructor
+    · rintro ⟨xs, x, h⟩; exact ⟨_, h⟩
+    · rintro ⟨xs, h⟩
+      exact ⟨Fin.init xs, xs (Fin.last n), by rwa [Fin.snoc_init_self]⟩
+
+end AllsExs
+
+/-- Realization of an `L_{∞ω}` sentence in a structure. -/
+def SentenceInf.Realize (φ : L.SentenceInf ι) (M : Type w) [L.Structure M] : Prop :=
+  FormulaInf.Realize (M := M) φ Empty.elim
+
+end Language
+
+end FirstOrder

Mathlib/ModelTheory/Infinitary/Syntax.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2026 Cameron Freer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Cameron Freer
+-/
+module
+
+public import Mathlib.ModelTheory.Syntax
+
+/-!
+# Infinitary first-order formulas
+
+This file defines the syntax of `L_{∞ω}`: first-order formulas with conjunctions and
+disjunctions indexed by a *fixed branching carrier* `ι`, one per formula. `L_{ω₁ω}` is the
+definitional specialization `ι := ℕ`.
+
+## Design
+
+The infinitary constructors `iSup`/`iInf` branch over the single type parameter `ι` rather than
+quantifying over a fresh index type at every node. Consequences:
+
+- `BoundedFormulaInf L ι α n : Type (max u v u' uι)` — the syntax lives in the `max` of its
+  parameters' universes, with no `+ 1` bump. In particular
+  `BoundedFormulaω L α n := BoundedFormulaInf L ℕ α n` has exactly the universe
+  `Type (max u v u')` of the finitary `BoundedFormula`.
+- An `ι`-indexed conjunction at a larger carrier `κ`, and transport of whole formulas
+  between carriers, are expressed through codings, arriving with the follow-up transport
+  layer. In particular, Karp's theorem, the consumer that forces arbitrary index types, needs
+  only the single carrier `M ⊕ N`.
+
+## Main definitions
+
+- `FirstOrder.Language.BoundedFormulaInf`: infinitary formulas with carrier `ι`, free variables
+  in `α`, and `n` free *bound-variable* slots.
+- `FirstOrder.Language.BoundedFormulaω`: the `ι := ℕ` specialization (an `abbrev`, so all
+  `BoundedFormulaInf` API applies definitionally).
+- Derived connectives and quantifier closures (`not`, `⊤`/`⊥`, `ex`, `alls`, `exs`), and the
+  carrier-generic finitary embedding `BoundedFormula.toInf`.
+-/
+
+@[expose] public section
+
+universe u v u' uι w
+
+namespace FirstOrder
+
+namespace Language
+
+variable (L : Language.{u, v})
+
+/-- An infinitary bounded formula of `L_{∞ω}`, with infinitary conjunctions and disjunctions
+branching over the fixed carrier `ι`, free variables indexed by `α`, and `n` additional bound
+variables available. -/
+inductive BoundedFormulaInf (ι : Type uι) (α : Type u') : ℕ → Type (max u v u' uι) where
+  /-- The false formula. -/
+  | falsum {n} : BoundedFormulaInf ι α n
+  /-- Equality of two terms. -/
+  | equal {n} (t₁ t₂ : L.Term (α ⊕ Fin n)) : BoundedFormulaInf ι α n
+  /-- A relation symbol applied to terms. -/
+  | rel {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) :
+      BoundedFormulaInf ι α n
+  /-- Implication. -/
+  | imp {n} (φ ψ : BoundedFormulaInf ι α n) : BoundedFormulaInf ι α n
+  /-- Universal quantification over the last bound variable. -/
+  | all {n} (φ : BoundedFormulaInf ι α (n + 1)) : BoundedFormulaInf ι α n
+  /-- Infinitary disjunction over the carrier. -/
+  | iSup {n} (φs : ι → BoundedFormulaInf ι α n) : BoundedFormulaInf ι α n
+  /-- Infinitary conjunction over the carrier. -/
+  | iInf {n} (φs : ι → BoundedFormulaInf ι α n) : BoundedFormulaInf ι α n
+
+/-- A bounded formula of `L_{ω₁ω}`: the definitional `ι := ℕ` specialization of
+`BoundedFormulaInf`. Its universe is exactly that of the finitary `BoundedFormula`. -/
+abbrev BoundedFormulaω (α : Type u') (n : ℕ) := L.BoundedFormulaInf ℕ α n
+
+/-- An `L_{∞ω}` formula: a bounded formula with no free bound variables. -/
+abbrev FormulaInf (ι : Type uι) (α : Type u') := L.BoundedFormulaInf ι α 0
+
+/-- An `L_{∞ω}` sentence: a formula with no free variables at all. -/
+abbrev SentenceInf (ι : Type uι) := L.FormulaInf ι Empty
+
+/-- An `L_{ω₁ω}` formula. -/
+abbrev Formulaω (α : Type u') := L.FormulaInf ℕ α
+
+/-- An `L_{ω₁ω}` sentence. -/
+abbrev Sentenceω := L.SentenceInf ℕ
+
+variable {L} {ι : Type uι} {α : Type u'} {n : ℕ}
+
+namespace BoundedFormulaInf
+
+/-- The negation of an infinitary formula. -/
+protected def not (φ : L.BoundedFormulaInf ι α n) : L.BoundedFormulaInf ι α n :=
+  φ.imp .falsum
+
+/-- The true formula. -/
+protected def verum : L.BoundedFormulaInf ι α n :=
+  BoundedFormulaInf.not .falsum
+
+instance : Bot (L.BoundedFormulaInf ι α n) :=
+  ⟨.falsum⟩
+
+instance : Top (L.BoundedFormulaInf ι α n) :=
+  ⟨BoundedFormulaInf.verum⟩
+
+instance : Inhabited (L.BoundedFormulaInf ι α n) :=
+  ⟨⊥⟩
+
+/-- Existential quantification over the last bound variable. -/
+protected def ex (φ : L.BoundedFormulaInf ι α (n + 1)) : L.BoundedFormulaInf ι α n :=
+  φ.not.all.not
+
+/-- Places universal quantifiers on all in-scope bound variables of an infinitary bounded
+formula (mirrors the finitary `BoundedFormula.alls`). -/
+def alls : ∀ {n}, L.BoundedFormulaInf ι α n → L.FormulaInf ι α
+  | 0, φ => φ
+  | _ + 1, φ => φ.all.alls
+
+/-- Places existential quantifiers on all in-scope bound variables of an infinitary bounded
+formula (mirrors the finitary `BoundedFormula.exs`). -/
+def exs : ∀ {n}, L.BoundedFormulaInf ι α n → L.FormulaInf ι α
+  | 0, φ => φ
+  | _ + 1, φ => φ.ex.exs
+
+end BoundedFormulaInf
+
+namespace BoundedFormula
+
+/-- The embedding of finitary bounded formulas into the infinitary syntax. Since finitary
+formulas have no infinitary nodes, the target carrier is arbitrary: there is one embedding for
+all carriers and universes, rather than an embedding into `L_{ω₁ω}` followed by a lift. -/
+def toInf : ∀ {n}, L.BoundedFormula α n → L.BoundedFormulaInf ι α n
+  | _, .falsum => .falsum
+  | _, .equal t₁ t₂ => .equal t₁ t₂
+  | _, .rel R ts => .rel R ts
+  | _, .imp φ ψ => (toInf φ).imp (toInf ψ)
+  | _, .all φ => (toInf φ).all
+
+/-- The embedding of finitary bounded formulas into `L_{ω₁ω}`. -/
+abbrev toOmega (φ : L.BoundedFormula α n) : L.BoundedFormulaω α n :=
+  toInf φ
+
+end BoundedFormula
+
+end Language
+
+end FirstOrder

MathlibTest/InfinitarySyntax.lean

@@ -0,0 +1,49 @@
+import Mathlib.ModelTheory.Infinitary.Semantics
+
+/-!
+Regression probes for the carrier-parameterized infinitary syntax. Each example is stated so
+that it fails to elaborate if the design regresses: the universe ascriptions ARE the claims,
+the `simp only` probes detect lemmas that only close by definitional unfolding, and the
+induction probe guards structural recursion through the `ι := ℕ` abbreviation.
+-/
+
+universe u v u' uι w
+
+namespace FirstOrder.Language
+
+open BoundedFormulaInf
+
+/-- The syntax lives at `max` of its parameters' universes: no `+ 1` bump. -/
+example (L : Language.{u, v}) (ι : Type uι) (α : Type u') (n : ℕ) :
+    Type (max u v u' uι) :=
+  L.BoundedFormulaInf ι α n
+
+/-- The `ι := ℕ` specialization has EXACTLY the finitary `BoundedFormula` universe. -/
+example (L : Language.{u, v}) (α : Type u') (n : ℕ) : Type (max u v u') :=
+  L.BoundedFormulaω α n
+
+/-- Realization applies by `simp only` at a literal nonzero index universe. -/
+example {L : Language.{u, v}} {α : Type u'} {M : Type w} [L.Structure M] {n : ℕ}
+    {ι : Type 1} (φs : ι → L.BoundedFormulaInf ι α n) (v : α → M) (xs : Fin n → M) :
+    (iInf φs).Realize v xs ↔ ∀ i, (φs i).Realize v xs := by
+  simp only [realize_iInf]
+
+/-- The finitary embedding is carrier-generic: realization is preserved even at an
+uncountable carrier in a higher universe. -/
+example {L : Language.{u, v}} {α : Type u'} {M : Type w} [L.Structure M] {n : ℕ}
+    (φ : L.BoundedFormula α n) (v : α → M) (xs : Fin n → M) :
+    (φ.toInf (ι := Type)).Realize v xs ↔ φ.Realize v xs :=
+  BoundedFormula.realize_toInf φ v xs
+
+/-- Structural induction still yields all seven cases, with `ℕ`-indexed induction
+hypotheses, through the `BoundedFormulaω` abbreviation; dot-notation elaborates. -/
+example {L : Language.{u, v}} {α : Type u'} {M : Type w} [L.Structure M] {k : ℕ}
+    (φ : L.BoundedFormulaω α k) (v : α → M) (xs : Fin k → M) :
+    φ.Realize v xs ∨ ¬φ.Realize v xs := by
+  induction φ <;> exact Classical.em _
+
+example {L : Language.{u, v}} {α : Type u'} (φs : ℕ → L.BoundedFormulaω α 0) :
+    L.BoundedFormulaω α 0 :=
+  .iInf φs
+
+end FirstOrder.Language