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 — see Infinitary/Reindex.lean. 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.

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

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.

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

  The false formula.

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

  Equality of two terms.

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

  A relation symbol applied to terms.

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

  Implication.

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

  Universal quantification over the last bound variable.

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

  Infinitary disjunction over the carrier.

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

  Infinitary conjunction over the carrier.

@[reducible, inline]

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

A bounded formula of L_{ω₁ω}: the definitional ι := ℕ specialization of BoundedFormulaInf. Its universe is exactly that of the finitary BoundedFormula.

Equations

• L.BoundedFormulaω α n = L.BoundedFormulaInf ℕ α n

@[reducible, inline]

abbrev FirstOrder.Language.FormulaInf (L : Language) (ι : Type uι) (α : Type u') : Type (max u v u' uι)

An L_{∞ω} formula: a bounded formula with no free bound variables.

Equations

• L.FormulaInf ι α = L.BoundedFormulaInf ι α 0

@[reducible, inline]

abbrev FirstOrder.Language.SentenceInf (L : Language) (ι : Type uι) : Type (max u v uι)

An L_{∞ω} sentence: a formula with no free variables at all.

Equations

• L.SentenceInf ι = L.FormulaInf ι Empty

@[reducible, inline]

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

An L_{ω₁ω} formula.

Routed through BoundedFormulaω rather than stated as FormulaInf ℕ α, though the two are the same type. Dot-notation resolution walks an abbreviation chain one unfolding at a time, trying each head constant's namespace in turn, so this routing keeps declarations in a downstream BoundedFormulaω namespace reachable as φ.op on an L_{ω₁ω} formula while the generic BoundedFormulaInf namespace stays reachable at the end of the chain.

Equations

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

@[reducible, inline]

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

An L_{ω₁ω} sentence. Routed through Formulaω for the reason given there.

Equations

• L.Sentenceω = L.Formulaω Empty

@[match_pattern]

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

The negation of an infinitary formula.

Equations

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

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

The true formula.

Equations

• FirstOrder.Language.BoundedFormulaInf.verum = FirstOrder.Language.BoundedFormulaInf.falsum.not

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[match_pattern]

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

Existential quantification over the last bound variable.

Equations

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

def FirstOrder.Language.BoundedFormulaInf.alls {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} : L.BoundedFormulaInf ι α n → L.FormulaInf ι α

Places universal quantifiers on all in-scope bound variables of an infinitary bounded formula (mirrors the finitary BoundedFormula.alls).

Equations

• φ.alls = φ
• φ.alls = φ.all.alls

def FirstOrder.Language.BoundedFormulaInf.exs {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} : L.BoundedFormulaInf ι α n → L.FormulaInf ι α

Places existential quantifiers on all in-scope bound variables of an infinitary bounded formula (mirrors the finitary BoundedFormula.exs).

Equations

• φ.exs = φ
• φ.exs = φ.ex.exs

def FirstOrder.Language.BoundedFormula.toInf {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} : L.BoundedFormula α n → L.BoundedFormulaInf ι α n

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.

Equations

• FirstOrder.Language.BoundedFormula.falsum.toInf = FirstOrder.Language.BoundedFormulaInf.falsum
• (FirstOrder.Language.BoundedFormula.equal t₁ t₂).toInf = FirstOrder.Language.BoundedFormulaInf.equal t₁ t₂
• (FirstOrder.Language.BoundedFormula.rel R ts).toInf = FirstOrder.Language.BoundedFormulaInf.rel R ts
• (φ.imp ψ).toInf = φ.toInf.imp ψ.toInf
• φ.all.toInf = φ.toInf.all

@[reducible, inline]

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

The embedding of finitary bounded formulas into L_{ω₁ω}.

Equations

• φ.toOmega = φ.toInf