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. Consequently BoundedFormulaInf L ι α n : Type (max u v u' uι) 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.

Terms are Mathlib's Term, and bound variables are the slots Fin n, as for the finitary BoundedFormula. A quantifier binds the last slot. The derived binary connectives follow Mathlib's finitary conventions: φ ⊓ ψ is (φ.imp ψ.not).not, φ ⊔ ψ is φ.not.imp ψ, and φ.iff ψ is φ.imp ψ ⊓ ψ.imp φ.

Infinitary formulas are not modelled by extending Mathlib's finitary BoundedFormula, whose iInf/iSup range over finite index types. The two syntaxes are related only by the embedding BoundedFormula.toInf. Structural recursion and induction use the recursor BoundedFormulaInf.rec, with one case per constructor.

Main definitions

• FirstOrder.Language.BoundedFormulaInf: infinitary formulas with carrier ι, free variables in α, and n bound-variable slots.
• FirstOrder.Language.BoundedFormulaω: the ι := ℕ specialization, an abbreviation, so all BoundedFormulaInf API applies definitionally; FormulaInf, SentenceInf, Formulaω and Sentenceω.
• The derived connectives not, ⊤, ⊥, ⊓, ⊔, iff and ex, the quantifier closures alls and exs, and the existential quantification exsLast k of the last k slots.
• FirstOrder.Language.BoundedFormulaInf.IsAtomic: equations and relational atoms.
• FirstOrder.Language.BoundedFormula.toInf: the carrier-generic embedding of finitary formulas, with its ι := ℕ case BoundedFormula.toOmega.

References

• Ported from cameronfreer/infinitary-logic at commit 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, whose infinitary syntax is Mathlib/ModelTheory/Infinitary/Syntax.lean in leanprover-community/mathlib4#42758 (Apache 2.0) at commit 2264c2c872bb642ab519aa2288d53110f07af37d.
• Divergences from these sources: the binary connectives ⊓, ⊔ and iff and the predicate IsAtomic are added; the definition bodies are not exposed, except those of the match patterns not and ex, and are used through the defining equations bot_def, top_def, inf_def, sup_def, iff_def, alls_zero, alls_succ, exs_zero, exs_succ, exsLast_zero, exsLast_succ and the toInf_* equations.

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.

@[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 bound-variable slots.

@[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.

@[reducible, inline]

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

An L_{ω₁ω} formula.

It is routed through BoundedFormulaω rather than stated as FormulaInf ℕ α, although the two are the same type: dot-notation resolution unfolds an abbreviation chain one step at a time, trying each head constant's namespace, so declarations in a BoundedFormulaω namespace stay reachable as φ.op on an L_{ω₁ω} formula.

@[reducible, inline]

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

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

@[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.

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

The true formula.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

The conjunction of two infinitary formulas, (φ.imp ψ.not).not, as for finitary formulas.

@[instance_reducible]

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

The disjunction of two infinitary formulas, φ.not.imp ψ, as for finitary formulas.

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

The biconditional of two infinitary formulas.

@[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.

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

Places universal quantifiers on all bound-variable slots of an infinitary bounded formula, as BoundedFormula.alls does for finitary formulas.

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

Places existential quantifiers on all bound-variable slots of an infinitary bounded formula, as BoundedFormula.exs does for finitary formulas.

def FirstOrder.Language.BoundedFormulaInf.exsLast {L : Language} {ι : Type uι} {α : Type u'} {n k : ℕ} : L.BoundedFormulaInf ι α (n + k) → L.BoundedFormulaInf ι α n

Existential quantification over the last k bound-variable slots, keeping the first n.

Defining equations

theorem FirstOrder.Language.BoundedFormulaInf.bot_def {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} : ⊥ = falsum

⊥ is the false formula.

theorem FirstOrder.Language.BoundedFormulaInf.top_def {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} : ⊤ = falsum.not

⊤ is the negation of the false formula.

theorem FirstOrder.Language.BoundedFormulaInf.inf_def {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : φ ⊓ ψ = (φ.imp ψ.not).not

The conjunction φ ⊓ ψ is (φ.imp ψ.not).not.

theorem FirstOrder.Language.BoundedFormulaInf.sup_def {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : φ ⊔ ψ = φ.not.imp ψ

The disjunction φ ⊔ ψ is φ.not.imp ψ.

theorem FirstOrder.Language.BoundedFormulaInf.iff_def {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) : φ.iff ψ = φ.imp ψ ⊓ ψ.imp φ

The biconditional φ.iff ψ is φ.imp ψ ⊓ ψ.imp φ.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.alls_zero {L : Language} {ι : Type uι} {α : Type u'} (φ : L.BoundedFormulaInf ι α 0) : φ.alls = φ

With no bound-variable slots, alls leaves a formula unchanged.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.alls_succ {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) : φ.alls = φ.all.alls

alls quantifies the last slot universally, then closes the remaining slots.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.exs_zero {L : Language} {ι : Type uι} {α : Type u'} (φ : L.BoundedFormulaInf ι α 0) : φ.exs = φ

With no bound-variable slots, exs leaves a formula unchanged.

@[simp]

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

exs quantifies the last slot existentially, then closes the remaining slots.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.exsLast_zero {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 0)) : φ.exsLast = φ

Quantifying no slots leaves a formula unchanged.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.exsLast_succ {L : Language} {ι : Type uι} {α : Type u'} {n k : ℕ} (φ : L.BoundedFormulaInf ι α (n + (k + 1))) : φ.exsLast = φ.ex.exsLast

exsLast quantifies the last slot existentially, then the remaining k slots.

inductive FirstOrder.Language.BoundedFormulaInf.IsAtomic {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} : L.BoundedFormulaInf ι α n → Prop

An infinitary formula is atomic when it is an equation between terms or a relation symbol applied to terms, as for Mathlib's finitary BoundedFormula.IsAtomic.

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

  An equation between terms is atomic.

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

  A relation symbol applied to terms is atomic.

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. Finitary formulas have no infinitary nodes, so the target carrier is arbitrary: one embedding serves every carrier and universe.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_falsum {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} : falsum.toInf = BoundedFormulaInf.falsum

The embedding sends the finitary false formula to the false formula.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_equal {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : (equal t₁ t₂).toInf = BoundedFormulaInf.equal t₁ t₂

The embedding sends an equation to the same equation.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_rel {L : Language} {ι : Type uι} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : (rel R ts).toInf = BoundedFormulaInf.rel R ts

The embedding sends a relational atom to the same atom.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_imp {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormula α n) : (φ.imp ψ).toInf = φ.toInf.imp ψ.toInf

The embedding commutes with implication.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_all {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : φ.all.toInf = φ.toInf.all

The embedding commutes with universal quantification.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_not {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) : φ.not.toInf = φ.toInf.not

The embedding commutes with negation.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_ex {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : φ.ex.toInf = φ.toInf.ex

The embedding commutes with existential quantification.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_alls {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) : toInf φ.alls = φ.toInf.alls

The embedding commutes with the universal closure of all bound-variable slots.

@[simp]

theorem FirstOrder.Language.BoundedFormula.toInf_exs {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.BoundedFormula α n) : toInf φ.exs = φ.toInf.exs

The embedding commutes with the existential closure of all bound-variable slots.

@[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_{ω₁ω}.