Documentation

TauCeti.ModelTheory.Infinitary.Substitution

Substitution and free-variable relabelling of infinitary formulas #

BoundedFormulaInf.subst substitutes terms for free variables, leaving bound slots unchanged. BoundedFormulaInf.relabel can instead send free variables to free variables or to newly introduced bound slots. These operations preserve the branching carrier and work without countability assumptions. Their realization laws describe the resulting valuations, including under quantifiers and infinitary connectives.

Relabelling follows Mathlib's FirstOrder.Language.BoundedFormula.relabel: the new slots come before the old slots. In particular, a map α → β ⊕ Fin m sends a formula with n slots to one with m + n slots. We reuse Mathlib's BoundedFormula.relabelAux and its valuation law rather than implementing the finite-index arithmetic again. Substitution similarly follows BoundedFormula.subst and reuses Term.subst.

The corresponding operations in Cameron Freer's cameronfreer/infinitary-logic, InfinitaryLogic/Lomega1omega/Operations.lean at checkpoint 9f82bd572af2d79a043c6bc3f1b745f14e0bcaa4, are specialized to the carrier ℕ. Here both operations and their realization laws are carrier-generic, and relabelling allows an arbitrary map into free variables and bound slots, not just a free-variable map.

source
def TauCeti.BoundedFormulaInf.subst {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} :
L.BoundedFormulaInf ι α n → (α → L.Term β) → L.BoundedFormulaInf ι β n

Substitute terms for the free variables of an infinitary formula. The substituted terms have only free variables, so no bound variable can capture one of their variables.

Instances For
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_falsum {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (f : α → L.Term β) :
    subst FirstOrder.Language.BoundedFormulaInf.falsum f = FirstOrder.Language.BoundedFormulaInf.falsum
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_equal {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) (f : α → L.Term β) :
    subst (FirstOrder.Language.BoundedFormulaInf.equal t₁ t₂) f = FirstOrder.Language.BoundedFormulaInf.equal (t₁.subst (Sum.elim (FirstOrder.Language.Term.relabel Sum.inl ∘ f) (FirstOrder.Language.var ∘ Sum.inr))) (t₂.subst (Sum.elim (FirstOrder.Language.Term.relabel Sum.inl ∘ f) (FirstOrder.Language.var ∘ Sum.inr)))
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_rel {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) (f : α → L.Term β) :
    subst (FirstOrder.Language.BoundedFormulaInf.rel R ts) f = FirstOrder.Language.BoundedFormulaInf.rel R fun (i : Fin k) => (ts i).subst (Sum.elim (FirstOrder.Language.Term.relabel Sum.inl ∘ f) (FirstOrder.Language.var ∘ Sum.inr))
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_imp {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) :
    subst (φ.imp ψ) f = (subst φ f).imp (subst ψ f)
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_all {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) (f : α → L.Term β) :
    subst φ.all f = (subst φ f).all
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_iSup {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) (f : α → L.Term β) :
    subst (FirstOrder.Language.BoundedFormulaInf.iSup φs) f = FirstOrder.Language.BoundedFormulaInf.iSup fun (i : ι) => subst (φs i) f
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_iInf {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φs : ι → L.BoundedFormulaInf ι α n) (f : α → L.Term β) :
    subst (FirstOrder.Language.BoundedFormulaInf.iInf φs) f = FirstOrder.Language.BoundedFormulaInf.iInf fun (i : ι) => subst (φs i) f
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_not {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) :
    subst φ.not f = (subst φ f).not
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_ex {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ : L.BoundedFormulaInf ι α (n + 1)) (f : α → L.Term β) :
    subst φ.ex f = (subst φ f).ex
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_bot {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (f : α → L.Term β) :
    subst ⊥ f = ⊥
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_top {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (f : α → L.Term β) :
    subst ⊤ f = ⊤
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_inf {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) :
    subst (φ ⊓ ψ) f = subst φ f ⊓ subst ψ f
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_sup {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) :
    subst (φ ⊔ ψ) f = subst φ f ⊔ subst ψ f
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.subst_iff {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ ψ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) :
    subst (φ.iff ψ) f = (subst φ f).iff (subst ψ f)
    source
    @[simp]
    theorem TauCeti.BoundedFormulaInf.realize_subst {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} {M : Type w} [L.Structure M] (φ : L.BoundedFormulaInf ι α n) (f : α → L.Term β) (v : β → M) (xs : Fin n → M) :
    (subst φ f).Realize v xs ↔ φ.Realize (fun (a : α) => FirstOrder.Language.Term.realize v (f a)) xs

    Substitution is realized by assigning to each original free variable the value of its substituted term. The bound-variable valuation is unchanged.

    source
    def TauCeti.BoundedFormulaInf.relabel {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m : ℕ} (g : α → β ⊕ Fin m) {n : ℕ} :
    L.BoundedFormulaInf ι α n → L.BoundedFormulaInf ι β (m + n)

    Relabel free variables by free variables or new bound slots. The m new slots are placed before the original n slots, and quantifiers continue to bind the last slot.

    Instances For
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_falsum {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) :
      relabel g FirstOrder.Language.BoundedFormulaInf.falsum = FirstOrder.Language.BoundedFormulaInf.falsum
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_equal {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (t₁ t₂ : L.Term (α ⊕ Fin n)) :
      relabel g (FirstOrder.Language.BoundedFormulaInf.equal t₁ t₂) = FirstOrder.Language.BoundedFormulaInf.equal (FirstOrder.Language.Term.relabel (FirstOrder.Language.BoundedFormula.relabelAux g n) t₁) (FirstOrder.Language.Term.relabel (FirstOrder.Language.BoundedFormula.relabelAux g n) t₂)
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_rel {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) {k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) :
      relabel g (FirstOrder.Language.BoundedFormulaInf.rel R ts) = FirstOrder.Language.BoundedFormulaInf.rel R fun (i : Fin k) => FirstOrder.Language.Term.relabel (FirstOrder.Language.BoundedFormula.relabelAux g n) (ts i)
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_imp {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ ψ : L.BoundedFormulaInf ι α n) :
      relabel g (φ.imp ψ) = (relabel g φ).imp (relabel g ψ)
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_all {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ : L.BoundedFormulaInf ι α (n + 1)) :
      relabel g φ.all = (relabel g φ).all
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_iSup {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φs : ι → L.BoundedFormulaInf ι α n) :
      relabel g (FirstOrder.Language.BoundedFormulaInf.iSup φs) = FirstOrder.Language.BoundedFormulaInf.iSup fun (i : ι) => relabel g (φs i)
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_iInf {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φs : ι → L.BoundedFormulaInf ι α n) :
      relabel g (FirstOrder.Language.BoundedFormulaInf.iInf φs) = FirstOrder.Language.BoundedFormulaInf.iInf fun (i : ι) => relabel g (φs i)
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_not {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ : L.BoundedFormulaInf ι α n) :
      relabel g φ.not = (relabel g φ).not
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_ex {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ : L.BoundedFormulaInf ι α (n + 1)) :
      relabel g φ.ex = (relabel g φ).ex
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_bot {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) :
      relabel g ⊥ = ⊥
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_top {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) :
      relabel g ⊤ = ⊤
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_inf {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ ψ : L.BoundedFormulaInf ι α n) :
      relabel g (φ ⊓ ψ) = relabel g φ ⊓ relabel g ψ
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_sup {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ ψ : L.BoundedFormulaInf ι α n) :
      relabel g (φ ⊔ ψ) = relabel g φ ⊔ relabel g ψ
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_iff {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ ψ : L.BoundedFormulaInf ι α n) :
      relabel g (φ.iff ψ) = (relabel g φ).iff (relabel g ψ)
      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.realize_relabel {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} {M : Type w} [L.Structure M] (g : α → β ⊕ Fin m) (φ : L.BoundedFormulaInf ι α n) (v : β → M) (xs : Fin (m + n) → M) :
      (relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ Fin.castAdd n) ∘ g) (xs ∘ Fin.natAdd m)

      Relabelling evaluates each original free variable at its image under g. The first m slots evaluate newly bound variables and the remaining n slots evaluate the original slots.

      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.subst_toInf {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {n : ℕ} (φ : L.BoundedFormula α n) (f : α → L.Term β) :
      subst φ.toInf f = (φ.subst f).toInf

      Embedding a substituted finitary formula is the same as substituting in its embedding.

      source
      @[simp]
      theorem TauCeti.BoundedFormulaInf.relabel_toInf {L : FirstOrder.Language} {ι : Type uι} {α : Type uα} {β : Type uβ} {m n : ℕ} (g : α → β ⊕ Fin m) (φ : L.BoundedFormula α n) :
      relabel g φ.toInf = (FirstOrder.Language.BoundedFormula.relabel g φ).toInf

      Embedding a relabelled finitary formula is the same as relabelling its embedding.