Documentation

TauCeti.ModelTheory.Infinitary.GraphTranslation.BackTranslate

Translating formulas of the graph language back into the original language #

BoundedFormulaInf.backTranslate sends an infinitary formula of the graph language L.graphLanguage to a formula of L: an atom G_f(x₀, …, x_{k-1}, y) of the graph relation of a function symbol f becomes the equation f(x₀, …, x_{k-1}) = y, a base atom R(xs) becomes R(xs), and connectives and quantifiers are translated structurally. The graph language has no function symbols, so its terms are variables and are sent to the same variables (Term.backTranslate). The translation works over any branching carrier.

Over the graph expansion of an L-structure, the back-translation of a formula is realized exactly when the formula is (BoundedFormulaInf.realize_backTranslate). The function symbols of the back-translation are the f whose graph relation occurs in the formula, and its relation symbols are the base symbols occurring in it (BoundedFormulaInf.functionsIn_backTranslate, BoundedFormulaInf.relationsIn_backTranslate). So a formula of the graph language all of whose relation symbols lie in relSym F R back-translates to a formula of L whose function symbols lie in F and whose relation symbols lie in R.

This is how a formula found in the graph language, for example an interpolant produced by a theorem about relational languages, returns to L with control of its symbols. Composed with the translation BoundedFormulaInf.relationalize, it gives back a formula with the same realization as the original in every L-structure (BoundedFormulaInf.realize_backTranslate_relationalize) and, by the occurrence calculus with relationsIn_relationalize, the same symbols; the two formulas are not claimed to be syntactically equal.

Main definitions #

Main results #

References #

source
def FirstOrder.Language.Term.backTranslate {L : Language} {β : Type uβ} :
L.graphLanguage.Term β → L.Term β

A term of the graph language as a term of L. The graph language has no function symbols, so every one of its terms is a variable, and it is sent to the same variable.

Instances For
    source
    @[simp]
    theorem FirstOrder.Language.Term.backTranslate_var {L : Language} {β : Type uβ} (b : β) :
    (var b).backTranslate = var b
    source
    @[simp]
    theorem FirstOrder.Language.Term.realize_backTranslate {L : Language} {β : Type uβ} {M : Type w} [L.Structure M] (t : L.graphLanguage.Term β) (v : β → M) :
    realize v t.backTranslate = realize v t

    A term of the graph language takes the same value as its back-translation, over the graph expansion.

    source
    @[simp]
    theorem FirstOrder.Language.Term.functionsIn_backTranslate {L : Language} {β : Type uβ} (t : L.graphLanguage.Term β) :
    t.backTranslate.functionsIn = ∅

    The back-translation of a term of the graph language mentions no function symbol.

    source
    def FirstOrder.Language.BoundedFormulaInf.backTranslate {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
    L.graphLanguage.BoundedFormulaInf ι α n → L.BoundedFormulaInf ι α n

    The back-translation of an infinitary formula of the graph language of L into L. The graph relation G_f of a k-ary function symbol f, applied to x₀, …, x_{k-1}, y, becomes the equation f(x₀, …, x_{k-1}) = y; base atoms and equations keep their symbols, and connectives and quantifiers are translated structurally.

    Instances For
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_falsum {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
      falsum.backTranslate = falsum
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_equal {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (t₁ t₂ : L.graphLanguage.Term (α ⊕ Fin n)) :
      (equal t₁ t₂).backTranslate = equal t₁.backTranslate t₂.backTranslate
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_rel_base {L : Language} {ι : Type uι} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.graphLanguage.Term (α ⊕ Fin n)) :
      (rel (GraphRelation.base R) ts).backTranslate = rel R fun (i : Fin l) => (ts i).backTranslate

      A base atom R(ts) back-translates to the atom R(ts) of L.

      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_rel_graph {L : Language} {ι : Type uι} {α : Type u'} {n k : ℕ} (f : L.Functions k) (ts : Fin (k + 1) → L.graphLanguage.Term (α ⊕ Fin n)) :
      (rel (GraphRelation.graph f) ts).backTranslate = equal (func f fun (i : Fin k) => (ts i.castSucc).backTranslate) (ts (Fin.last k)).backTranslate

      A graph atom G_f(t₀, …, t_{k-1}, t_k) back-translates to the equation f(t₀, …, t_{k-1}) = t_k.

      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_imp {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ ψ : L.graphLanguage.BoundedFormulaInf ι α n) :
      (φ.imp ψ).backTranslate = φ.backTranslate.imp ψ.backTranslate
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_all {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.graphLanguage.BoundedFormulaInf ι α (n + 1)) :
      φ.all.backTranslate = φ.backTranslate.all
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_iSup {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φs : ι → L.graphLanguage.BoundedFormulaInf ι α n) :
      (iSup φs).backTranslate = iSup fun (i : ι) => (φs i).backTranslate
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_iInf {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φs : ι → L.graphLanguage.BoundedFormulaInf ι α n) :
      (iInf φs).backTranslate = iInf fun (i : ι) => (φs i).backTranslate
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_not {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.graphLanguage.BoundedFormulaInf ι α n) :
      φ.not.backTranslate = φ.backTranslate.not
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_bot {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
      ⊥.backTranslate = ⊥
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_top {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} :
      ⊤.backTranslate = ⊤
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_inf {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ ψ : L.graphLanguage.BoundedFormulaInf ι α n) :
      (φ ⊓ ψ).backTranslate = φ.backTranslate ⊓ ψ.backTranslate
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_sup {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ ψ : L.graphLanguage.BoundedFormulaInf ι α n) :
      (φ ⊔ ψ).backTranslate = φ.backTranslate ⊔ ψ.backTranslate
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_ex {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.graphLanguage.BoundedFormulaInf ι α (n + 1)) :
      φ.ex.backTranslate = φ.backTranslate.ex
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.backTranslate_iff {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ ψ : L.graphLanguage.BoundedFormulaInf ι α n) :
      (φ.iff ψ).backTranslate = φ.backTranslate.iff ψ.backTranslate
      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.realize_backTranslate {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] (φ : L.graphLanguage.BoundedFormulaInf ι α n) (v : α → M) (xs : Fin n → M) :
      φ.backTranslate.Realize v xs ↔ φ.Realize v xs

      The back-translation preserves truth: over the graph expansion of an L-structure, the back-translation of a formula of the graph language is realized exactly when the formula is.

      source
      theorem FirstOrder.Language.BoundedFormulaInf.realize_backTranslate_relationalize {L : Language} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] (φ : L.BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) :
      (backTranslate (relationalize φ)).Realize v xs ↔ Realize φ v xs

      Translating a formula of L into the graph language and back preserves its realization in every L-structure.

      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_backTranslate {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.graphLanguage.BoundedFormulaInf ι α n) :
      φ.backTranslate.functionsIn = graphRelSym ⁻¹' φ.relationsIn

      The function symbols of the back-translation of a formula are the function symbols whose graph relation occurs in it.

      source
      @[simp]
      theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_backTranslate {L : Language} {ι : Type uι} {α : Type u'} {n : ℕ} (φ : L.graphLanguage.BoundedFormulaInf ι α n) :
      φ.backTranslate.relationsIn = baseRelSym ⁻¹' φ.relationsIn

      The relation symbols of the back-translation of a formula are the relation symbols whose base symbol occurs in it. Graph atoms become equations, which contribute no relation symbol.