Translating infinitary formulas into the graph language

BoundedFormulaInf.relationalize translates an L_{ω₁ω} formula of L into a formula of the relational graph language L.graphLanguage. Connectives and quantifiers are translated structurally. An atom is flattened through its terms: an equation t₁ = t₂ becomes ∃ y, (t₁ = y) ∧ (t₂ = y), and a relational atom R(t₀, …, t_{l-1}) becomes ∃ y₀ … y_{l-1}, (⋀ᵢ tᵢ = yᵢ) ∧ R(y₀, …, y_{l-1}), where each statement t = y about the value of a term is its term graph Term.graphFormula. The term graph of a variable is an equation, and the term graph of f(s₀, …, s_{k-1}) existentially quantifies one witness for the value of each argument, states the term graphs of the arguments at these witnesses, and applies the graph relation of f to the witnesses and the value.

Over the graph expansion of an L-structure the translation is realized exactly when the original formula is (BoundedFormulaInf.realize_relationalize). The translation mentions no function symbol, and its relation symbols are exactly the graph-language symbols of the symbols of the original formula (BoundedFormulaInf.relationsIn_relationalize). Combined with relSym_inter, this bounds the shared vocabulary of two translated formulas by the translation of their shared vocabulary.

Main definitions

• FirstOrder.Language.Term.graphFormula: the term graph t = y of a term, with the variables of the term read through a map into the variables of the formula.
• FirstOrder.Language.BoundedFormulaInf.relationalize: the translation of formulas.

Main results

• FirstOrder.Language.Term.realize_graphFormula, FirstOrder.Language.BoundedFormulaInf.realize_relationalize: over the graph expansion, the term graph states the value of the term, and the translation of a formula is realized exactly when the formula is.
• FirstOrder.Language.BoundedFormulaInf.relationsIn_relationalize: the exact occurrence identity (relationalize φ).relationsIn = relSym φ.functionsIn φ.relationsIn, with FirstOrder.Language.BoundedFormulaInf.functionsIn_relationalize.

References

• The term graph and the translation follow termGraphAux, equalGraph, relGraph and relationalizeFormula of cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, in InfinitaryLogic/Methods/Interpolation/TermGraph.lean and Relationalize.lean. Divergences from that source: languages, variables and structures live in arbitrary universes; the term graph reads the variables of a term through a map into variables rather than into graph-language terms; finite conjunctions are coded conjunctions iInfAlong; and the atomic translations are not separate declarations.

def FirstOrder.Language.Term.graphFormula {L : Language} {α : Type u'} {β : Type uβ} {n : ℕ} : L.Term β → (β → α ⊕ Fin n) → α ⊕ Fin n → L.graphLanguage.BoundedFormulaω α n

The term graph of a term t of L: the formula of the graph language stating that the value of t, whose variables are read through ρ, is the value of the variable y. A variable gives an equation; an application f(s₀, …, s_{k-1}) quantifies k new slots existentially, states the term graph of each sᵢ at the i-th new slot, and applies the graph relation of f to the new slots and y.

@[simp]

theorem FirstOrder.Language.Term.graphFormula_var {L : Language} {α : Type u'} {β : Type uβ} {n : ℕ} (b : β) (ρ : β → α ⊕ Fin n) (y : α ⊕ Fin n) : (var b).graphFormula ρ y = BoundedFormulaInf.equal (var (ρ b)) (var y)

The term graph of a variable is an equation.

theorem FirstOrder.Language.Term.graphFormula_func {L : Language} {α : Type u'} {β : Type uβ} {n k : ℕ} (f : L.Functions k) (ts : Fin k → L.Term β) (ρ : β → α ⊕ Fin n) (y : α ⊕ Fin n) : (func f ts).graphFormula ρ y = ((BoundedFormulaInf.iInfAlong (TauCeti.IndexCoding.ofEncodable (Fin k)) fun (i : Fin k) => (ts i).graphFormula (Sum.map id (Fin.castAdd k) ∘ ρ) (Sum.inr (Fin.natAdd n i))) ⊓ BoundedFormulaInf.rel (GraphRelation.graph f) (Fin.snoc (fun (i : Fin k) => var (Sum.inr (Fin.natAdd n i))) (var (Sum.map id (Fin.castAdd k) y)))).exsLast

The term graph of an application quantifies one new slot for the value of each argument.

@[simp]

theorem FirstOrder.Language.Term.realize_graphFormula {L : Language} {α : Type u'} {β : Type uβ} {M : Type w} [L.Structure M] {n : ℕ} (t : L.Term β) (ρ : β → α ⊕ Fin n) (y : α ⊕ Fin n) (v : α → M) (xs : Fin n → M) : BoundedFormulaInf.Realize (t.graphFormula ρ y) v xs ↔ realize (Sum.elim v xs ∘ ρ) t = Sum.elim v xs y

Over the graph expansion, the term graph of t holds exactly when the value of t, with its variables read through ρ, is the value of y.

@[simp]

theorem FirstOrder.Language.Term.relationsIn_graphFormula {L : Language} {α : Type u'} {β : Type uβ} {n : ℕ} (t : L.Term β) (ρ : β → α ⊕ Fin n) (y : α ⊕ Fin n) : BoundedFormulaInf.relationsIn (t.graphFormula ρ y) = graphRelSym '' t.functionsIn

The relation symbols of a term graph are exactly the graph relations of the function symbols of the term.

def FirstOrder.Language.BoundedFormulaInf.relationalize {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormulaω α n → L.graphLanguage.BoundedFormulaω α n

The translation into the graph language of an L_{ω₁ω} formula of L. Connectives and quantifiers are translated structurally. An equation t₁ = t₂ becomes ∃ y, (t₁ = y) ∧ (t₂ = y), and a relational atom R(t₀, …, t_{l-1}) becomes ∃ y₀ … y_{l-1}, (⋀ᵢ tᵢ = yᵢ) ∧ R(y₀, …, y_{l-1}), where each t = y is a term graph.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_falsum {L : Language} {α : Type u'} {n : ℕ} : falsum.relationalize = falsum

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_equal {L : Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : (equal t₁ t₂).relationalize = (t₁.graphFormula (Sum.map id (Fin.castAdd 1)) (Sum.inr (Fin.natAdd n 0)) ⊓ t₂.graphFormula (Sum.map id (Fin.castAdd 1)) (Sum.inr (Fin.natAdd n 0))).exsLast

The translation of an equation t₁ = t₂ is ∃ y, (t₁ = y) ∧ (t₂ = y).

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_rel {L : Language} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : (rel R ts).relationalize = ((iInfAlong (TauCeti.IndexCoding.ofEncodable (Fin l)) fun (i : Fin l) => (ts i).graphFormula (Sum.map id (Fin.castAdd l)) (Sum.inr (Fin.natAdd n i))) ⊓ rel (GraphRelation.base R) fun (i : Fin l) => var (Sum.inr (Fin.natAdd n i))).exsLast

The translation of a relational atom R(t₀, …, t_{l-1}) is ∃ y₀ … y_{l-1}, (⋀ᵢ tᵢ = yᵢ) ∧ R(y₀, …, y_{l-1}).

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_imp {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : (imp φ ψ).relationalize = imp (relationalize φ) (relationalize ψ)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_all {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : (all φ).relationalize = all (relationalize φ)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_iSup {L : Language} {α : Type u'} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) : (iSup φs).relationalize = iSup fun (i : ℕ) => relationalize (φs i)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_iInf {L : Language} {α : Type u'} {n : ℕ} (φs : ℕ → L.BoundedFormulaω α n) : (iInf φs).relationalize = iInf fun (i : ℕ) => relationalize (φs i)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_not {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) : (BoundedFormulaInf.not φ).relationalize = BoundedFormulaInf.not (relationalize φ)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_bot {L : Language} {α : Type u'} {n : ℕ} : relationalize ⊥ = ⊥

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_top {L : Language} {α : Type u'} {n : ℕ} : relationalize ⊤ = ⊤

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_inf {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : relationalize (φ ⊓ ψ) = relationalize φ ⊓ relationalize ψ

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_sup {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : relationalize (φ ⊔ ψ) = relationalize φ ⊔ relationalize ψ

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_ex {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : (BoundedFormulaInf.ex φ).relationalize = BoundedFormulaInf.ex (relationalize φ)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationalize_iff {L : Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : (BoundedFormulaInf.iff φ ψ).relationalize = BoundedFormulaInf.iff (relationalize φ) (relationalize ψ)

@[simp]

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

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

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.relationsIn_relationalize {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) : relationsIn (relationalize φ) = relSym (functionsIn φ) (relationsIn φ)

The exact occurrence identity: the relation symbols of the translation of φ are exactly the graph-language symbols of the function and relation symbols of φ.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.functionsIn_relationalize {L : Language} {α : Type u'} {n : ℕ} (φ : L.BoundedFormulaω α n) : functionsIn (relationalize φ) = ∅

No function symbol occurs in the translation of a formula: the graph language has none.