Lω₁ω Syntax

This file defines the syntax of the infinitary logic Lω₁ω, which extends first-order logic with countable conjunctions and disjunctions.

Main Definitions

• FirstOrder.Language.BoundedFormulaω: The type of Lω₁ω formulas with free variables in α and bound variables in Fin n.
• FirstOrder.Language.Formulaω: Formulas with no bound variables.
• FirstOrder.Language.Sentenceω: Sentences (formulas with no free variables).

Implementation Notes

The formulas are defined inductively with constructors for the standard first-order connectives plus ℕ-indexed conjunction (iInf) and disjunction (iSup). The einf and esup variants handle general countable indices via Encodable.

The derived connectives (and, or, ex) are defined classically via De Morgan laws. This matches Mathlib's BoundedFormula conventions and ensures compatibility with classical semantics.

inductive FirstOrder.Language.BoundedFormulaω (L : Language) (α : Type u') : ℕ → Type (max u v u')

Lω₁ω bounded formulas: first-order formulas extended with countable conjunctions and disjunctions. BoundedFormulaω L α n has free variables indexed by α and n bound variables.

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

  The false formula.

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

  Equality of two terms.

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

  A relation applied to terms.

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

  Implication between formulas.

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

  Universal quantification.

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

  ℕ-indexed disjunction (supremum). Use esup for general countable indices.

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

  ℕ-indexed conjunction (infimum). Use einf for general countable indices.

@[reducible, inline]

abbrev FirstOrder.Language.Formulaω (L : Language) (α : Type u') : Type (max u v u')

Lω₁ω formulas with no bound variables in scope.

Equations

• L.Formulaω α = L.BoundedFormulaω α 0

@[reducible, inline]

abbrev FirstOrder.Language.Sentenceω (L : Language) : Type (max u v)

Lω₁ω sentences: formulas with no free or bound variables in scope.

Equations

• L.Sentenceω = L.Formulaω Empty

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

Equations

• FirstOrder.Language.BoundedFormulaω.instInhabited = { default := FirstOrder.Language.BoundedFormulaω.falsum }

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

Equations

• FirstOrder.Language.BoundedFormulaω.instBot = { bot := FirstOrder.Language.BoundedFormulaω.falsum }

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

The true formula, defined as ¬⊥.

Equations

• FirstOrder.Language.BoundedFormulaω.top = FirstOrder.Language.BoundedFormulaω.falsum.imp FirstOrder.Language.BoundedFormulaω.falsum

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

Equations

• FirstOrder.Language.BoundedFormulaω.instTop = { top := FirstOrder.Language.BoundedFormulaω.top }

@[match_pattern]

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

Negation of a formula.

Equations

• φ.not = φ.imp ⊥

@[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 FirstOrder.Language.BoundedFormulaω.instMin {L : Language} {α : Type u'} {n : ℕ} : Min (L.BoundedFormulaω α n)

Equations

• FirstOrder.Language.BoundedFormulaω.instMin = { 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 FirstOrder.Language.BoundedFormulaω.instMax {L : Language} {α : Type u'} {n : ℕ} : Max (L.BoundedFormulaω α n)

Equations

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

@[match_pattern]

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

Existential quantification.

Equations

• φ.ex = φ.not.all.not

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 => ⊥

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