Bound-variable relabelling and weakening of infinitary formulas

A bounded formula with m bound-variable slots can be relabelled along any map f : Fin m → Fin n of slots. A quantifier binds the last slot, so the relabelling extends f past each quantifier by sending the newly quantified slot to the new last slot. Quantified variables therefore move with their binders, and the relabelled formula is realized at a valuation xs exactly when the original is realized at xs ∘ f. The map f need not be injective: relabelling along it may identify bound variables.

Weakening castLE along m ≤ n is relabelling along Fin.castLE. It corresponds to Mathlib's finitary weakening BoundedFormula.liftAt that inserts the new slots after the m existing ones, not to Mathlib's finitary BoundedFormula.castLE, which keeps a quantified variable at its old slot and so preserves realization only when m = n.

Main definitions

• FirstOrder.Language.BoundedFormulaInf.mapBound: relabelling of bound-variable slots.
• FirstOrder.Language.BoundedFormulaInf.castLE: weakening along m ≤ n.

Main results

• FirstOrder.Language.BoundedFormulaInf.realize_mapBound: relabelling along f is realization at xs ∘ f.
• FirstOrder.Language.BoundedFormulaInf.realize_castLE: weakening is realization at xs ∘ Fin.castLE h, for every m ≤ n.
• FirstOrder.Language.BoundedFormulaInf.mapBound_id, FirstOrder.Language.BoundedFormulaInf.mapBound_mapBound, FirstOrder.Language.BoundedFormulaInf.castLE_rfl and FirstOrder.Language.BoundedFormulaInf.castLE_castLE: identity and composition.

References

• cameronfreer/infinitary-logic at commit 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4 has castLE at carrier ℕ in InfinitaryLogic/Lomega1omega/Operations.lean, with realization only for equal slot counts.
• Divergences from that source: weakening is defined for every carrier, through the general relabelling mapBound, which moves quantified variables with their binders, so that realization holds for every m ≤ n.

def FirstOrder.Language.BoundedFormulaInf.mapBound {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} : (Fin m → Fin n) → L.BoundedFormulaInf ι α m → L.BoundedFormulaInf ι α n

Relabel the bound-variable slots of an infinitary formula along f : Fin m → Fin n. Past a quantifier, f is extended by sending the quantified slot to the new last slot, so quantified variables move with their binders.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_falsum {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (f : Fin m → Fin n) : mapBound f falsum = falsum

Relabelling fixes the false formula.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_equal {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (f : Fin m → Fin n) (t₁ t₂ : L.Term (α ⊕ Fin m)) : mapBound f (equal t₁ t₂) = equal (Term.relabel (Sum.map id f) t₁) (Term.relabel (Sum.map id f) t₂)

Relabelling relabels the bound variables of an equation.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_rel {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (f : Fin m → Fin n) {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin m)) : mapBound f (rel R ts) = rel R fun (i : Fin l) => Term.relabel (Sum.map id f) (ts i)

Relabelling relabels the bound variables of a relational atom.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_imp {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (f : Fin m → Fin n) (φ ψ : L.BoundedFormulaInf ι α m) : mapBound f (φ.imp ψ) = (mapBound f φ).imp (mapBound f ψ)

Relabelling commutes with implication.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_all {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (f : Fin m → Fin n) (φ : L.BoundedFormulaInf ι α (m + 1)) : mapBound f φ.all = (mapBound (Fin.snoc (fun (i : Fin m) => (f i).castSucc) (Fin.last n)) φ).all

Past a quantifier, relabelling sends the quantified slot to the new last slot.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_iSup {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (f : Fin m → Fin n) (φs : ι → L.BoundedFormulaInf ι α m) : mapBound f (iSup φs) = iSup fun (i : ι) => mapBound f (φs i)

Relabelling commutes with disjunctions over the carrier.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_iInf {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (f : Fin m → Fin n) (φs : ι → L.BoundedFormulaInf ι α m) : mapBound f (iInf φs) = iInf fun (i : ι) => mapBound f (φs i)

Relabelling commutes with conjunctions over the carrier.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_mapBound {L : Language} {ι : Type uι} {α : Type u'} {M : Type w} [L.Structure M] {m n : ℕ} (f : Fin m → Fin n) (φ : L.BoundedFormulaInf ι α m) (v : α → M) (xs : Fin n → M) : (mapBound f φ).Realize v xs ↔ φ.Realize v (xs ∘ f)

Relabelling is realization along the slot map: the relabelled formula is realized at xs exactly when the original is realized at xs ∘ f.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_id {L : Language} {ι : Type uι} {α : Type u'} {m : ℕ} (φ : L.BoundedFormulaInf ι α m) : mapBound id φ = φ

Relabelling along the identity is the identity.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.mapBound_mapBound {L : Language} {ι : Type uι} {α : Type u'} {k m n : ℕ} (f : Fin k → Fin m) (g : Fin m → Fin n) (φ : L.BoundedFormulaInf ι α k) : mapBound g (mapBound f φ) = mapBound (g ∘ f) φ

Relabelling along f and then g is relabelling along g ∘ f.

Weakening

def FirstOrder.Language.BoundedFormulaInf.castLE {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaInf ι α m) : L.BoundedFormulaInf ι α n

Weakening an infinitary formula from m to n ≥ m bound-variable slots, by relabelling along Fin.castLE. Quantified variables move with their binders, so the result has the same meaning at every valuation of the n slots that agrees on the first m. This corresponds to Mathlib's finitary BoundedFormula.liftAt inserting the new slots after the existing ones, not to Mathlib's finitary BoundedFormula.castLE.

theorem FirstOrder.Language.BoundedFormulaInf.castLE_def {L : Language} {ι : Type uι} {α : Type u'} {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaInf ι α m) : castLE h φ = mapBound (Fin.castLE h) φ

Weakening is relabelling along Fin.castLE.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_castLE {L : Language} {ι : Type uι} {α : Type u'} {M : Type w} [L.Structure M] {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaInf ι α m) (v : α → M) (xs : Fin n → M) : (castLE h φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.castLE h)

Weakening preserves meaning, for every m ≤ n: the weakened formula is realized at xs exactly when the original is realized at the first m slots of xs.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.castLE_rfl {L : Language} {ι : Type uι} {α : Type u'} {m : ℕ} (φ : L.BoundedFormulaInf ι α m) : castLE ⋯ φ = φ

Weakening along m ≤ m is the identity.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.castLE_castLE {L : Language} {ι : Type uι} {α : Type u'} {k m n : ℕ} (h₁ : k ≤ m) (h₂ : m ≤ n) (φ : L.BoundedFormulaInf ι α k) : castLE h₂ (castLE h₁ φ) = castLE ⋯ φ

Weakening twice is weakening once.