Relationalization of a language: the graph language and its structures (Craig Layer 3, Unit 1)

The first gated unit of the functions→relations relationalization (audit §9b): the relationalized language graphLanguage L — no function symbols, each n-ary function f replaced by an (n+1)-ary graph relation G_f with intended meaning G_f(x⃗, y) ↔ f(x⃗) = y — its graph expansion of an L-structure, and the σ-level embeddings of the original symbols into the graph language's relation symbols.

The disjoint indexed constructors of GraphRelation keep base relations and function graphs apart definitionally, which is exactly what makes the shared-vocabulary identity

relSym L F₁ R₁ ∩ relSym L F₂ R₂ = relSym L (F₁ ∩ F₂) (R₁ ∩ R₂)

(the early correctness gate for the eventual sharp occurrence bound) a clean image/injectivity computation.

Contents

• GraphRelation, graphLanguage, graphLanguage_isRelational;
• graphExpansion (the G_f(x⃗,y) ↔ f(x⃗)=y structure) with relMap_base/relMap_graph simp lemmas;
• baseRelSym/graphRelSym σ-embeddings, their injectivity and cross-disjointness;
• relSym and the intersection identity relSym_inter.

The relationalized language

inductive FirstOrder.Language.GraphRelation (L : Language) : ℕ → Type

Relation symbols of the relationalization of L: every base relation is kept at its arity, and every n-ary function symbol becomes an (n+1)-ary graph relation. The two constructors are disjoint by construction.

• base {L : Language} {n : ℕ} : L.Relations n → L.GraphRelation n
• graph {L : Language} {n : ℕ} : L.Functions n → L.GraphRelation (n + 1)

@[reducible]

def FirstOrder.Language.graphLanguage (L : Language) : Language

The relationalization of L: no function symbols, relation symbols GraphRelation L.

Marked @[reducible] so that (graphLanguage L).Relations n unfolds to GraphRelation L n at implicit transparency. The whole relationalization tower already treats the two as interchangeable — baseRelSym/graphRelSym below take their codomain in GraphRelation L n precisely so the constructors' injectivity and no-confusion lemmas apply directly, and the companion graphExpansion is @[reducible] for the same reason. Since Lean 4.34 requires goals to be type-correct at implicit transparency before rw/simp will act, that pre-existing identification has to hold there too; otherwise every generic lemma about graphLanguage formulas needs a specialized copy with the symbol spelled GraphRelation.base/.graph. This is a direct structure literal with no proof content, so reducibility costs nothing.

Equations

• L.graphLanguage = { Functions := fun (x : ℕ) => Empty, Relations := fun (n : ℕ) => L.GraphRelation n }

instance FirstOrder.Language.graphLanguage_isRelational (L : Language) : L.graphLanguage.IsRelational

Graph-symbol countability

instance FirstOrder.Language.graphLanguage_countable_relations {L : Language} [Countable ((l : ℕ) × L.Relations l)] [Countable ((n : ℕ) × L.Functions n)] : Countable ((n : ℕ) × L.graphLanguage.Relations n)

The graph language's relation sigma is countable when both symbol sigmas of L are.

The graph expansion of an L-structure

def FirstOrder.Language.graphRelMap {L : Language} (M : Type) [L.Structure M] {n : ℕ} : L.GraphRelation n → (Fin n → M) → Prop

Realization of a graph-language relation symbol in the graph expansion of an L-structure: base relations unchanged, and G_f(x⃗, y) reads f(x⃗) = y (the first n coordinates feed f, the last is its value).

Equations

• FirstOrder.Language.graphRelMap M (FirstOrder.Language.GraphRelation.base r) x✝ = FirstOrder.Language.Structure.RelMap r x✝
• FirstOrder.Language.graphRelMap M (FirstOrder.Language.GraphRelation.graph f) v = (FirstOrder.Language.Structure.funMap f (Fin.init v) = v (Fin.last n))

@[reducible]

def FirstOrder.Language.graphExpansion (L : Language) (M : Type) [L.Structure M] : L.graphLanguage.Structure M

The graph expansion of an L-structure to a graphLanguage L-structure: G_f(x⃗, y) ↔ f(x⃗) = y, base relations preserved, and no function symbols to interpret.

Equations

• L.graphExpansion M = { funMap := fun {n : ℕ} (f : L.graphLanguage.Functions n) (x : Fin n → M) => nomatch f, RelMap := fun {n : ℕ} => FirstOrder.Language.graphRelMap M }

@[simp]

theorem FirstOrder.Language.graphExpansion_relMap_base {L : Language} (M : Type) [L.Structure M] {n : ℕ} (r : L.Relations n) (v : Fin n → M) : Structure.RelMap (GraphRelation.base r) v ↔ Structure.RelMap r v

@[simp]

theorem FirstOrder.Language.graphExpansion_relMap_graph {L : Language} (M : Type) [L.Structure M] {n : ℕ} (f : L.Functions n) (v : Fin (n + 1) → M) : Structure.RelMap (GraphRelation.graph f) v ↔ Structure.funMap f (Fin.init v) = v (Fin.last n)

σ-level embeddings of the original symbols

def FirstOrder.Language.baseRelSym (L : Language) : (n : ℕ) × L.Relations n → (n : ℕ) × L.GraphRelation n

Embed an original relation symbol as a base graph-language relation symbol. (Codomain uses GraphRelation L n, definitionally (graphLanguage L).Relations n, so the constructor's injectivity/no-confusion lemmas apply directly.)

Equations

• L.baseRelSym p = ⟨p.fst, FirstOrder.Language.GraphRelation.base p.snd⟩

def FirstOrder.Language.graphRelSym (L : Language) : (n : ℕ) × L.Functions n → (n : ℕ) × L.GraphRelation n

Embed an original n-ary function symbol as its (n+1)-ary graph relation symbol.

Equations

• L.graphRelSym p = ⟨p.fst + 1, FirstOrder.Language.GraphRelation.graph p.snd⟩

theorem FirstOrder.Language.baseRelSym_injective {L : Language} : Function.Injective L.baseRelSym

theorem FirstOrder.Language.graphRelSym_injective {L : Language} : Function.Injective L.graphRelSym

theorem FirstOrder.Language.baseRelSym_ne_graphRelSym {L : Language} (p : (n : ℕ) × L.Relations n) (q : (n : ℕ) × L.Functions n) : L.baseRelSym p ≠ L.graphRelSym q

Singleton preimages of the two embeddings — the Sigma-free interface the back-translation occurrence calculus computes with.

theorem FirstOrder.Language.baseRelSym_preimage_base_singleton {L : Language} (p : (n : ℕ) × L.Relations n) : L.baseRelSym ⁻¹' {L.baseRelSym p} = {p}

theorem FirstOrder.Language.graphRelSym_preimage_graph_singleton {L : Language} (q : (n : ℕ) × L.Functions n) : L.graphRelSym ⁻¹' {L.graphRelSym q} = {q}

theorem FirstOrder.Language.graphRelSym_preimage_base_singleton {L : Language} (p : (n : ℕ) × L.Relations n) : L.graphRelSym ⁻¹' {L.baseRelSym p} = ∅

theorem FirstOrder.Language.baseRelSym_preimage_graph_singleton {L : Language} (q : (n : ℕ) × L.Functions n) : L.baseRelSym ⁻¹' {L.graphRelSym q} = ∅

The relation-symbol set of the relationalization, and its intersection identity

def FirstOrder.Language.relSym (L : Language) (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : Set ((n : ℕ) × L.GraphRelation n)

The relation symbols of the relationalization coming from a function-symbol set F and a relation-symbol set R: base relations from R, graph relations from F.

Equations

• L.relSym F R = L.baseRelSym '' R ∪ L.graphRelSym '' F

theorem FirstOrder.Language.baseRelSym_image_inter_graphRelSym_image {L : Language} (R : Set ((n : ℕ) × L.Relations n)) (F : Set ((n : ℕ) × L.Functions n)) : L.baseRelSym '' R ∩ L.graphRelSym '' F = ∅

theorem FirstOrder.Language.graphRelSym_image_inter_baseRelSym_image {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : L.graphRelSym '' F ∩ L.baseRelSym '' R = ∅

theorem FirstOrder.Language.relSym_inter {L : Language} (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) : L.relSym F₁ R₁ ∩ L.relSym F₂ R₂ = L.relSym (F₁ ∩ F₂) (R₁ ∩ R₂)

The shared-vocabulary identity (Unit 1 correctness gate): the relation-symbol sets of two relationalizations meet exactly in the relationalization of the shared symbols.

@[simp]

theorem FirstOrder.Language.relSym_empty {L : Language} : L.relSym ∅ ∅ = ∅

theorem FirstOrder.Language.relSym_union {L : Language} (F₁ F₂ : Set ((n : ℕ) × L.Functions n)) (R₁ R₂ : Set ((n : ℕ) × L.Relations n)) : L.relSym (F₁ ∪ F₂) (R₁ ∪ R₂) = L.relSym F₁ R₁ ∪ L.relSym F₂ R₂

relSym turns unions of symbol sets into unions — the algebra the exact occurrence identity of the formula translation steps through at binary connectives.

theorem FirstOrder.Language.relSym_iUnion {L : Language} {ι : Sort u_1} (F : ι → Set ((n : ℕ) × L.Functions n)) (R : ι → Set ((n : ℕ) × L.Relations n)) : L.relSym (⋃ (i : ι), F i) (⋃ (i : ι), R i) = ⋃ (i : ι), L.relSym (F i) (R i)

relSym commutes with indexed unions — the countable-connective step of the exact occurrence identity.