Lω₁ω Syntax — compatibility facade over the fixed-carrier syntax

BoundedFormulaω, Formulaω and Sentenceω are no longer declared here. They come from Mathlib.ModelTheory.Infinitary.Syntax, where BoundedFormulaω L α n is an abbrev for BoundedFormulaInf L ℕ α n. This file re-exports that syntax under the module path and namespace the project already uses, and adds only what Mathlib does not provide.

Why an abbrev and not a def

The specialization must stay definitional, not merely propositional. Since Lean 4.34 a goal has to be type-correct at implicit transparency before rw/simp will act on it, so a semireducible wrapper around BoundedFormulaInf ℕ would silently break rewriting across the whole ω consumer surface. The probes at the end of this file certify the identification with no change, rewrite, or explicit cast — their absence is the certification.

What this file still owns

• the qualified BoundedFormulaω.* constructor surface, for consumers that name constructors explicitly rather than through dot-notation (dot-notation resolves through the head symbol BoundedFormulaInf and needs no help);
• the derived connectives Mathlib does not define: and, or, iff, with their Min/Max instances;
• the Encodable-indexed connectives einf/esup and their explicit-encoding forms einfWith/esupWith;
• the scoped notation.

Bot, Top, Inhabited, not and ex now come from Mathlib and are deliberately not redeclared. BoundedFormulaInf.verum plays the role of the old top and is definitionally equal to it (not falsum reduces to imp falsum falsum).

Qualified constructor surface

The constructors live in the BoundedFormulaInf namespace. Dot-notation on a BoundedFormulaω already resolves there, but consumers naming a constructor explicitly as BoundedFormulaω.falsum need these. Each is an abbrev, so it unfolds by rfl, and each is @[match_pattern], so it may still be used in pattern position.

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.falsum {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormulaω α n

Equations

• FirstOrder.Language.BoundedFormulaω.falsum = FirstOrder.Language.BoundedFormulaInf.falsum

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.equal {L : Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : L.BoundedFormulaω α n

Equations

• FirstOrder.Language.BoundedFormulaω.equal t₁ t₂ = FirstOrder.Language.BoundedFormulaInf.equal t₁ t₂

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.rel {L : Language} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : L.BoundedFormulaω α n

Equations

• FirstOrder.Language.BoundedFormulaω.rel R ts = FirstOrder.Language.BoundedFormulaInf.rel R ts

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.imp {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Equations

• φ.imp ψ = FirstOrder.Language.BoundedFormulaInf.imp φ ψ

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.all {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : L.BoundedFormulaω α n

Equations

• φ.all = FirstOrder.Language.BoundedFormulaInf.all φ

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.iSup {L : Language} {α : Type u'} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Equations

• FirstOrder.Language.BoundedFormulaω.iSup φs = FirstOrder.Language.BoundedFormulaInf.iSup φs

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.iInf {L : Language} {α : Type u'} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Equations

• FirstOrder.Language.BoundedFormulaω.iInf φs = FirstOrder.Language.BoundedFormulaInf.iInf φs

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.not {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Negation, as a qualified name. BoundedFormulaInf.not is the definition.

Equations

• φ.not = FirstOrder.Language.BoundedFormulaInf.not φ

@[reducible, match_pattern, inline]

abbrev FirstOrder.Language.BoundedFormulaω.ex {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : L.BoundedFormulaω α n

Existential quantification, as a qualified name.

Equations

• φ.ex = FirstOrder.Language.BoundedFormulaInf.ex φ

@[reducible, inline]

abbrev FirstOrder.Language.BoundedFormulaω.top {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormulaω α n

The true formula. Mathlib calls it verum; this is the project's historical name for it, and the two are definitionally equal (not falsum reduces to imp falsum falsum).

Equations

• FirstOrder.Language.BoundedFormulaω.top = FirstOrder.Language.BoundedFormulaInf.verum

Production's not and ex were @[match_pattern]; Mathlib's are not, and the attribute cannot be added downstream ("cannot add attribute to a declaration in an imported module"). The qualified BoundedFormulaω.not/.ex above are declared here and so do carry it, which covers consumers that name them explicitly; dot-notation patterns (| .not φ => …) resolve through the head symbol to BoundedFormulaInf.not and are therefore not available. If a consumer needs them, the fix belongs upstream on the fork, not here.

Derived connectives Mathlib does not provide

@[match_pattern]

def FirstOrder.Language.BoundedFormulaω.and {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Conjunction of two formulas, defined via De Morgan.

Equations

• φ.and ψ = (φ.imp ψ.not).not

@[instance_reducible]

instance FirstOrder.Language.BoundedFormulaω.instMin_infinitaryLogic {L : Language} {α : Type u'} {n : ℕ} : Min (L.BoundedFormulaω α n)

Equations

• FirstOrder.Language.BoundedFormulaω.instMin_infinitaryLogic = { min := FirstOrder.Language.BoundedFormulaω.and }

@[match_pattern]

def FirstOrder.Language.BoundedFormulaω.or {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Disjunction of two formulas.

Equations

• φ.or ψ = φ.not.imp ψ

@[instance_reducible]

instance FirstOrder.Language.BoundedFormulaω.instMax_infinitaryLogic {L : Language} {α : Type u'} {n : ℕ} : Max (L.BoundedFormulaω α n)

Equations

• FirstOrder.Language.BoundedFormulaω.instMax_infinitaryLogic = { max := FirstOrder.Language.BoundedFormulaω.or }

def FirstOrder.Language.BoundedFormulaω.iff {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Biconditional between formulas.

Equations

• φ.iff ψ = φ.imp ψ ⊓ ψ.imp φ

def FirstOrder.Language.BoundedFormulaω.einf {L : Language} {α : Type u'} {n : ℕ} {ι : Type u_1} [Encodable ι] (φs : ι → L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Indexed conjunction over any Encodable type. This extends iInf from ℕ-indexed to general countable indices by encoding.

Equations

• FirstOrder.Language.BoundedFormulaω.einf φs = FirstOrder.Language.BoundedFormulaω.iInf fun (k : ℕ) => match Encodable.decode k with | some i => φs i | none => ⊤

def FirstOrder.Language.BoundedFormulaω.esup {L : Language} {α : Type u'} {n : ℕ} {ι : Type u_1} [Encodable ι] (φs : ι → L.BoundedFormulaω α n) : L.BoundedFormulaω α n

Indexed disjunction over any Encodable type. This extends iSup from ℕ-indexed to general countable indices by encoding.

Equations

• FirstOrder.Language.BoundedFormulaω.esup φs = FirstOrder.Language.BoundedFormulaω.iSup fun (k : ℕ) => match Encodable.decode k with | some i => φs i | none => ⊥

Explicit-encoding forms

einf/esup take their encoding by instance search. A consumer that must use a specific enumeration — one supplied as data rather than found — is otherwise forced into a local letI, which is fragile and makes the resulting syntax look instance-dependent when it is not.

These are thin wrappers, deliberately: einf/esup are not redefined in terms of them. Reversing that dependency would disturb definitional reductions across many existing consumers.

def FirstOrder.Language.BoundedFormulaω.einfWith {L : Language} {α : Type u'} {n : ℕ} {ι : Type u_1} (e : Encodable ι) (φs : ι → L.BoundedFormulaω α n) : L.BoundedFormulaω α n

einf along an explicitly supplied encoding.

Equations

• FirstOrder.Language.BoundedFormulaω.einfWith e φs = FirstOrder.Language.BoundedFormulaω.einf φs

def FirstOrder.Language.BoundedFormulaω.esupWith {L : Language} {α : Type u'} {n : ℕ} {ι : Type u_1} (e : Encodable ι) (φs : ι → L.BoundedFormulaω α n) : L.BoundedFormulaω α n

esup along an explicitly supplied encoding.

Equations

• FirstOrder.Language.BoundedFormulaω.esupWith e φs = FirstOrder.Language.BoundedFormulaω.esup φs

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.einfWith_eq {L : Language} {α : Type u'} {n : ℕ} {ι : Type u_1} (e : Encodable ι) (φs : ι → L.BoundedFormulaω α n) : einfWith e φs = einf φs

@[simp]

theorem FirstOrder.Language.BoundedFormulaω.esupWith_eq {L : Language} {α : Type u'} {n : ℕ} {ι : Type u_1} (e : Encodable ι) (φs : ι → L.BoundedFormulaω α n) : esupWith e φs = esup φs

def Lomega1omega.«term_⟹ω_» : Lean.TrailingParserDescr

Equations

• Lomega1omega.«term_⟹ω_» = Lean.ParserDescr.trailingNode `Lomega1omega.«term_⟹ω_» 62 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ω ") (Lean.ParserDescr.cat `term 62))

def Lomega1omega.«term∀'ω_» : Lean.ParserDescr

Equations

• Lomega1omega.«term∀'ω_» = Lean.ParserDescr.node `Lomega1omega.«term∀'ω_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀'ω ") (Lean.ParserDescr.cat `term 110))

def Lomega1omega.«term∼ω_» : Lean.ParserDescr

Equations

• Lomega1omega.«term∼ω_» = Lean.ParserDescr.node `Lomega1omega.«term∼ω_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼ω") (Lean.ParserDescr.cat `term 1023))

def Lomega1omega.«term∃'ω_» : Lean.ParserDescr

Equations

• Lomega1omega.«term∃'ω_» = Lean.ParserDescr.node `Lomega1omega.«term∃'ω_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃'ω ") (Lean.ParserDescr.cat `term 110))

def Lomega1omega.«term_⇔ω_» : Lean.TrailingParserDescr

Equations

• Lomega1omega.«term_⇔ω_» = Lean.ParserDescr.trailingNode `Lomega1omega.«term_⇔ω_» 61 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ω ") (Lean.ParserDescr.cat `term 62))

Facade transparency gates

These must elaborate with no change, rewrite, or explicit cast. That is precisely what certifies that the ω names remain a definitional specialization — the property Lean 4.34's implicit-transparency requirement makes load-bearing for every rw/simp in the ω tower.