L∞ω Syntax

This file defines the syntax of the infinitary logic L∞ω, which extends first-order logic with arbitrary (possibly uncountable) conjunctions and disjunctions.

Main Definitions

• FirstOrder.Language.BoundedFormulaInf: The type of L∞ω formulas with free variables in α and bound variables in Fin n. Allows arbitrary index types for iSup/iInf.
• FirstOrder.Language.FormulaInf: Formulas with no bound variables.
• FirstOrder.Language.SentenceInf: Sentences (formulas with no free variables).

Implementation Notes

L∞ω is the union of all Lκω for cardinals κ. Each formula belongs to some Lκω where κ bounds the cardinality of all index sets used in infinitary connectives. The IsKappa predicate characterizes membership in Lκω; IsCountable is the special case for Lω₁ω.

The formulas are parameterized by a universe uι for index types. All index types in iSup/iInf must live in Type uι. Choose uι large enough for your application; for countable logic, uι = 0 suffices.

inductive FirstOrder.Language.BoundedFormulaInf (L : Language) (α : Type u') : ℕ → Type (max u v u' (uι + 1))

L∞ω bounded formulas: first-order formulas extended with arbitrary conjunctions and disjunctions. BoundedFormulaInf L α n has free variables indexed by α and n bound variables. The index type ι for iSup/iInf lives in universe uι.

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

  The false formula.

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

  Equality of two terms.

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

  A relation applied to terms.

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

  Implication between formulas.

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

  Universal quantification.

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

  Arbitrary-indexed disjunction (supremum). The index type lives in universe uι.

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

  Arbitrary-indexed conjunction (infimum). The index type lives in universe uι.

@[reducible, inline]

abbrev FirstOrder.Language.FormulaInf (L : Language) (α : Type u') : Type (max u v u' (u_1 + 1))

L∞ω formulas with no bound variables in scope.

Equations

• L.FormulaInf α = L.BoundedFormulaInf α 0

@[reducible, inline]

abbrev FirstOrder.Language.SentenceInf (L : Language) : Type (max u v (u_1 + 1))

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

Equations

• L.SentenceInf = L.FormulaInf Empty

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

Equations

• FirstOrder.Language.BoundedFormulaInf.instInhabited = { default := FirstOrder.Language.BoundedFormulaInf.falsum }

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

Equations

• FirstOrder.Language.BoundedFormulaInf.instBot = { bot := FirstOrder.Language.BoundedFormulaInf.falsum }

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

The true formula, defined as ¬⊥.

Equations

• FirstOrder.Language.BoundedFormulaInf.top = FirstOrder.Language.BoundedFormulaInf.falsum.imp FirstOrder.Language.BoundedFormulaInf.falsum

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

Equations

• FirstOrder.Language.BoundedFormulaInf.instTop = { top := FirstOrder.Language.BoundedFormulaInf.top }

@[match_pattern]

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

Negation of a formula.

Equations

• φ.not = φ.imp ⊥

@[match_pattern]

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

Conjunction of two formulas, defined via De Morgan.

Equations

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

instance FirstOrder.Language.BoundedFormulaInf.instMin {L : Language} {α : Type u'} {n : ℕ} : Min (L.BoundedFormulaInf α n)

Equations

• FirstOrder.Language.BoundedFormulaInf.instMin = { min := FirstOrder.Language.BoundedFormulaInf.and }

@[match_pattern]

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

Disjunction of two formulas.

Equations

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

instance FirstOrder.Language.BoundedFormulaInf.instMax {L : Language} {α : Type u'} {n : ℕ} : Max (L.BoundedFormulaInf α n)

Equations

• FirstOrder.Language.BoundedFormulaInf.instMax = { max := FirstOrder.Language.BoundedFormulaInf.or }

@[match_pattern]

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

Existential quantification.

Equations

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

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

Biconditional between formulas.

Equations

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

def FirstOrder.Language.BoundedFormulaInf.emptyiSup {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormulaInf α n

Empty disjunction (equivalent to ⊥).

Equations

• FirstOrder.Language.BoundedFormulaInf.emptyiSup = FirstOrder.Language.BoundedFormulaInf.iSup fun (e : Empty) => e.elim

def FirstOrder.Language.BoundedFormulaInf.emptyiInf {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormulaInf α n

Empty conjunction (equivalent to ⊤).

Equations

• FirstOrder.Language.BoundedFormulaInf.emptyiInf = FirstOrder.Language.BoundedFormulaInf.iInf fun (e : Empty) => e.elim

def Linfomega.«term_⟹∞_» : Lean.TrailingParserDescr

Equations

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

def Linfomega.«term∀'∞_» : Lean.ParserDescr

Equations

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

def Linfomega.«term∼∞_» : Lean.ParserDescr

Equations

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

def Linfomega.«term∃'∞_» : Lean.ParserDescr

Equations

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

def Linfomega.«term_⇔∞_» : Lean.TrailingParserDescr

Equations

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