Documentation

InfinitaryLogic.Methods.Interpolation.Relationalize

Relationalization of formulas (Craig Layer 3, Unit 4) #

The formula translation into the relationalized language: relationalizeFormula sends an L_{ω₁ω} formula over L to one over graphLanguage L, replacing every atom by its term-graph flattening and transporting the connectives and quantifiers structurally.

Atomic translation #

equalGraph t u — one witness, not two: ∃ y, termGraph(t, y) ∧ termGraph(u, y). Smaller than two witnesses plus an equality atom, and its relation-symbol set is exactly the graph symbols occurring in t or u.
relGraph R ts — ∃ y⃗, (⋀ᵢ termGraph(tᵢ, yᵢ)) ∧ R^base(y⃗).

Both consume existsBlock directly, with the context-polymorphic termGraphAux fed by the lifted variable embedding ctxLiftEmb (no term relabeling of built formulas).

Main Results #

realize_equalGraph / realize_relGraph — the atomic realization lemmas, kept separate so a failure downstream distinguishes term-flattening trouble from connective transport.
realize_relationalizeFormula — over the graph expansion, the translation is realization-equivalent to the original formula.
relationsIn_relationalizeFormula — the exact occurrence identity (relationalizeFormula φ).relationsIn = relSym L φ.functionsIn φ.relationsIn; it composes immediately with relSym_inter, making the final sharp occurrence bound essentially algebraic. functionsIn_relationalizeFormula is ∅ (the graph language is relational).
The nested-formula pilot R(f(g(x), h(c))).

The lifted variable embedding and the atomic translations #

def FirstOrder.Language.ctxLiftEmb {L : Language} {α : Type} {n : ℕ} (k : ℕ) (z : α ⊕ Fin n) :

L.graphLanguage.Term (α ⊕ Fin (n + k))

The variable embedding of the ambient context into the context extended by k fresh bound variables — what termGraphAux reads the atom's term variables through.

Equations

FirstOrder.Language.ctxLiftEmb k z = FirstOrder.Language.var (Sum.map id (Fin.castAdd k) z)

Instances For

def FirstOrder.Language.equalGraph {L : Language} {α : Type} {n : ℕ} (t u : L.Term (α ⊕ Fin n)) :

L.graphLanguage.BoundedFormulaω α n

The equality atom, relationalized with one witness: ∃ y, termGraph(t,y) ∧ termGraph(u,y).

Equations

One or more equations did not get rendered due to their size.

Instances For

def FirstOrder.Language.relGraph {L : Language} {α : Type} {n k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) :

L.graphLanguage.BoundedFormulaω α n

The relation atom, relationalized: ∃ y⃗, (⋀ᵢ termGraph(tᵢ, yᵢ)) ∧ R^base(y⃗).

Equations

One or more equations did not get rendered due to their size.

Instances For

The structural translation #

def FirstOrder.Language.relationalizeFormula {L : Language} {α : Type} {n : ℕ} :

L.BoundedFormulaω α n → L.graphLanguage.BoundedFormulaω α n

Relationalize a formula: atoms via their term-graph flattenings (equalGraph/relGraph), connectives and quantifiers structurally.

Equations

Instances For

Stable rewrite points for Units 5–7 (all definitional).

@[simp]

theorem FirstOrder.Language.relationalizeFormula_falsum {L : Language} {α : Type} {n : ℕ} :

relationalizeFormula BoundedFormulaω.falsum = BoundedFormulaω.falsum

@[simp]

theorem FirstOrder.Language.relationalizeFormula_equal {L : Language} {α : Type} {n : ℕ} (t u : L.Term (α ⊕ Fin n)) :

relationalizeFormula (BoundedFormulaω.equal t u) = equalGraph t u

@[simp]

theorem FirstOrder.Language.relationalizeFormula_rel {L : Language} {α : Type} {n k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) :

relationalizeFormula (BoundedFormulaω.rel R ts) = relGraph R ts

@[simp]

theorem FirstOrder.Language.relationalizeFormula_imp {L : Language} {α : Type} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) :

relationalizeFormula (φ.imp ψ) = (relationalizeFormula φ).imp (relationalizeFormula ψ)

@[simp]

theorem FirstOrder.Language.relationalizeFormula_all {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) :

relationalizeFormula φ.all = (relationalizeFormula φ).all

@[simp]

theorem FirstOrder.Language.relationalizeFormula_iSup {L : Language} {α : Type} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) :

relationalizeFormula (BoundedFormulaω.iSup φs) = BoundedFormulaω.iSup fun (i : ℕ) => relationalizeFormula (φs i)

@[simp]

theorem FirstOrder.Language.relationalizeFormula_iInf {L : Language} {α : Type} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) :

relationalizeFormula (BoundedFormulaω.iInf φs) = BoundedFormulaω.iInf fun (i : ℕ) => relationalizeFormula (φs i)

Semantics over the graph expansion #

@[simp]

theorem FirstOrder.Language.realize_ctxLiftEmb {L : Language} {α : Type} {n : ℕ} {M : Type} [L.Structure M] {k : ℕ} (z : α ⊕ Fin n) (v : α → M) (xs : Fin n → M) (ws : Fin k → M) :

Term.realize (Sum.elim v (Fin.append xs ws)) (ctxLiftEmb k z) = Sum.elim v xs z

theorem FirstOrder.Language.realize_equalGraph {L : Language} {α : Type} {n : ℕ} {M : Type} [L.Structure M] (t u : L.Term (α ⊕ Fin n)) (v : α → M) (xs : Fin n → M) :

(equalGraph t u).Realize v xs ↔ Term.realize (Sum.elim v xs) t = Term.realize (Sum.elim v xs) u

Atomic realization, equality: the one-witness translation of t = u realizes to value equality.

theorem FirstOrder.Language.realize_relGraph {L : Language} {α : Type} {n : ℕ} {M : Type} [L.Structure M] {k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) (v : α → M) (xs : Fin n → M) :

(relGraph R ts).Realize v xs ↔ Structure.RelMap R fun (i : Fin k) => Term.realize (Sum.elim v xs) (ts i)

Atomic realization, relations: the translation of R(t₀, …, t_{k-1}) realizes to the base relation on the terms' values.

theorem FirstOrder.Language.realize_relationalizeFormula {L : Language} {α M : Type} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) :

(relationalizeFormula φ).Realize v xs ↔ φ.Realize v xs

The realize bridge: over the graph expansion, the relationalized formula is realization-equivalent to the original.

The nested-formula pilot: `R(f(g(x), h(c)))` #

The exact occurrence identities #

theorem FirstOrder.Language.relationsIn_equalGraph {L : Language} {α : Type} {n : ℕ} (t u : L.Term (α ⊕ Fin n)) :

(equalGraph t u).relationsIn = L.graphRelSym '' (t.functionsIn ∪ u.functionsIn)

The equality atom's relation symbols: exactly the graph relations of the function symbols occurring in t or u.

theorem FirstOrder.Language.relationsIn_relGraph {L : Language} {α : Type} {n k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) :

(relGraph R ts).relationsIn = L.relSym (⋃ (i : Fin k), (ts i).functionsIn) {⟨k, R⟩}

The relation atom's relation symbols: exactly the relationalization of its own symbols — the base relation R plus the graph relations of the arguments' function symbols.

theorem FirstOrder.Language.relationsIn_relationalizeFormula {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :

(relationalizeFormula φ).relationsIn = L.relSym φ.functionsIn φ.relationsIn

The exact occurrence identity: the relationalized formula's relation symbols are exactly the relationalization relSym of the original formula's symbols. Composes immediately with relSym_inter for the sharp shared-vocabulary bound.

theorem FirstOrder.Language.functionsIn_relationalizeFormula {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) :

(relationalizeFormula φ).functionsIn = ∅

No function symbol occurs in a relationalized formula (the graph language is relational).