Documentation

InfinitaryLogic.Methods.Interpolation.BackTranslate

Back-translation from the graph language (Craig Layer 3, Unit 6) #

The translation back into L: G_f(x⃗, y) ↦ f(x⃗) = y, base relation atoms recover the original relations, and — separately — native equality stays equality after term erasure (a relational interpolant may introduce equality even when no G_f occurs, and its back-translation then correctly uses no function symbol).

Everything here holds for every L-structure over its graph expansion — no symbol set, graph axioms, choice, or reconstruction enters.

Main Results #

Term erasure #

source
def FirstOrder.Language.ungraphTerm {L : Language} {β : Type u_1} :
L.graphLanguage.Term β → L.Term β

Erase a graph-language term to an L-term: the graph language has no function symbols, so this is variable-preserving with the function case impossible.

Equations
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.realize_ungraphTerm {L : Language} {M : Type} [L.Structure M] (S : L.graphLanguage.Structure M) {β : Type u_1} (t : L.graphLanguage.Term β) (env : β → M) :
    Term.realize env (ungraphTerm t) = Term.realize env t
    source
    @[simp]
    theorem FirstOrder.Language.functionsIn_ungraphTerm_eq_empty {L : Language} {α : Type} (t : L.graphLanguage.Term α) :
    (ungraphTerm t).functionsIn = ∅

    The back-translation #

    source
    def FirstOrder.Language.backTranslateFormula {L : Language} {α : Type} {n : ℕ} :
    L.graphLanguage.BoundedFormulaω α n → L.BoundedFormulaω α n

    Back-translate a graph-language formula to L: native equality stays equality (after term erasure), a base atom recovers the original relation, a graph atom G_f(x⃗, y) becomes f(x⃗) = y, and all connectives and quantifiers are structural.

    Equations
    Instances For

      Semantics over the graph expansion #

      source
      theorem FirstOrder.Language.realize_backTranslateFormula {L : Language} {α M : Type} [L.Structure M] {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) :
      (backTranslateFormula θ).Realize v xs ↔ θ.Realize v xs

      The back-translation semantics: over the graph expansion of any L-structure, the back-translation realizes exactly as the graph-language formula. No symbol set, graph axioms, choice, or reconstruction.

      source
      theorem FirstOrder.Language.realize_backTranslate_relationalize {L : Language} {α M : Type} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) :
      (backTranslateFormula (relationalizeFormula φ)).Realize v xs ↔ φ.Realize v xs

      Acceptance corollary: back-translating a relationalization is semantically the original formula, in every L-structure (no syntactic identity claimed).

      The exact occurrence identities, in preimage form #

      source
      theorem FirstOrder.Language.functionsIn_backTranslateFormula {L : Language} {α : Type} {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) :
      (backTranslateFormula θ).functionsIn = L.graphRelSym ⁻¹' θ.relationsIn

      The back-translation's function symbols are exactly the graphRelSym-preimage of the formula's relation symbols (native equality contributes nothing — term erasure is function-free).

      source
      theorem FirstOrder.Language.relationsIn_backTranslateFormula {L : Language} {α : Type} {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) :
      (backTranslateFormula θ).relationsIn = L.baseRelSym ⁻¹' θ.relationsIn

      The back-translation's relation symbols are exactly the baseRelSym-preimage of the formula's relation symbols.

      The consumer lemmas for the Craig assembly (Unit 7) #

      source
      theorem FirstOrder.Language.functionsIn_backTranslate_subset {L : Language} {α : Type} {n : ℕ} {θ : L.graphLanguage.BoundedFormulaω α n} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} (h : θ.relationsIn ⊆ L.relSym F R) :
      (backTranslateFormula θ).functionsIn ⊆ F

      An interpolant whose relation symbols lie in relSym L F R back-translates with function symbols in F.

      source
      theorem FirstOrder.Language.relationsIn_backTranslate_subset {L : Language} {α : Type} {n : ℕ} {θ : L.graphLanguage.BoundedFormulaω α n} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} (h : θ.relationsIn ⊆ L.relSym F R) :
      (backTranslateFormula θ).relationsIn ⊆ R

      An interpolant whose relation symbols lie in relSym L F R back-translates with relation symbols in R.