The graph language of a first-order language

The graph language L.graphLanguage has no function symbols. Its relation symbols are those of L, at their arities, together with one (k + 1)-ary relation symbol G_f for each k-ary function symbol f of L, standing for the graph f(x₀, …, x_{k-1}) = y of f. Every L-structure becomes an L.graphLanguage-structure on the same carrier, its graph expansion graphExpansion L M.

Formulas of L translate into formulas of the graph language with the same realization in the graph expansion (TauCeti.ModelTheory.Infinitary.GraphTranslation.Relationalize). This is how statements proved for relational languages, in which every closed term of a constant expansion is a constant, reach languages with function symbols.

The relation symbols of the graph language coming from given sets F of function symbols and R of relation symbols of L form the set relSym F R. The two kinds of graph-language symbols are disjoint, so relSym commutes with intersections: the symbols shared by two translated formulas are the translations of the symbols shared by the two formulas (relSym_inter).

Main definitions

• FirstOrder.Language.GraphRelation: the relation symbols of the graph language.
• FirstOrder.Language.graphLanguage: the graph language, which is relational.
• FirstOrder.Language.graphExpansion: the graph expansion of an L-structure.
• FirstOrder.Language.baseRelSym, FirstOrder.Language.graphRelSym: the graph-language symbol of a relation symbol and of a function symbol of L, as arity-tagged symbols.
• FirstOrder.Language.relSym: the graph-language symbols coming from sets of symbols of L.

Main results

• FirstOrder.Language.baseRelSym_injective, FirstOrder.Language.graphRelSym_injective and FirstOrder.Language.baseRelSym_ne_graphRelSym: the two symbol maps are injective with disjoint images.
• FirstOrder.Language.relSym_inter: the shared-vocabulary identity relSym F₁ R₁ ∩ relSym F₂ R₂ = relSym (F₁ ∩ F₂) (R₁ ∩ R₂), with the laws relSym_union and relSym_iUnion.
• FirstOrder.Language.nonempty_equiv_graphExpansion_iff: two structures are isomorphic exactly when their graph expansions are.

References

• The graph language, its expansion, the symbol maps and relSym follow GraphRelation, graphLanguage, graphExpansion, baseRelSym, graphRelSym and relSym of cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, in InfinitaryLogic/Methods/Interpolation/GraphLanguage.lean. Divergences from that source: the graph language lives in the universes of L rather than in Language.{0, 0}, and the graph expansion is defined on carriers in any universe.

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

The relation symbols of the graph language of L: every relation symbol of L is kept at its arity (base), and every k-ary function symbol of L gives a (k + 1)-ary relation symbol (graph) for its graph.

• base {L : Language} {n : ℕ} (R : L.Relations n) : L.GraphRelation n

  A relation symbol of L, kept at its arity.

• graph {L : Language} {k : ℕ} (f : L.Functions k) : L.GraphRelation (k + 1)

  The graph of a k-ary function symbol of L, a (k + 1)-ary relation symbol whose last argument is the value.

@[reducible, inline]

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

The graph language of L: no function symbols, and as relation symbols those of L together with the graph of each function symbol of L. The definition is reducible, so that a relation symbol of the graph language is built and taken apart as a GraphRelation.

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

def FirstOrder.Language.baseRelSym {L : Language} (R : (n : ℕ) × L.Relations n) : (n : ℕ) × L.GraphRelation n

The graph-language symbol of an arity-tagged relation symbol of L.

def FirstOrder.Language.graphRelSym {L : Language} (f : (n : ℕ) × L.Functions n) : (n : ℕ) × L.GraphRelation n

The graph-language symbol of an arity-tagged function symbol of L: the graph relation, of arity one more.

@[simp]

theorem FirstOrder.Language.baseRelSym_mk {L : Language} {n : ℕ} (R : L.Relations n) : baseRelSym ⟨n, R⟩ = ⟨n, GraphRelation.base R⟩

@[simp]

theorem FirstOrder.Language.graphRelSym_mk {L : Language} {n : ℕ} (f : L.Functions n) : graphRelSym ⟨n, f⟩ = ⟨n + 1, GraphRelation.graph f⟩

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

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

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

theorem FirstOrder.Language.baseRelSym_or_graphRelSym {L : Language} (S : (n : ℕ) × L.GraphRelation n) : (∃ (R : (n : ℕ) × L.Relations n), baseRelSym R = S) ∨ ∃ (f : (n : ℕ) × L.Functions n), graphRelSym f = S

A graph-language symbol is the symbol of a relation symbol or of a function symbol of L.

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

The graph language has countably many relation symbols when L has countably many symbols of both sorts.

The symbols coming from sets of symbols of L

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 graph language coming from a set F of function symbols and a set R of relation symbols of L: the base symbols of R and the graph symbols of F.

theorem FirstOrder.Language.relSym_def {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : relSym F R = baseRelSym '' R ∪ graphRelSym '' F

@[simp]

theorem FirstOrder.Language.baseRelSym_mem_relSym {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {r : (n : ℕ) × L.Relations n} : baseRelSym r ∈ relSym F R ↔ r ∈ R

@[simp]

theorem FirstOrder.Language.graphRelSym_mem_relSym {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {f : (n : ℕ) × L.Functions n} : graphRelSym f ∈ relSym F R ↔ f ∈ F

@[simp]

theorem FirstOrder.Language.mk_base_mem_relSym {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {n : ℕ} {r : L.Relations n} : ⟨n, GraphRelation.base r⟩ ∈ relSym F R ↔ ⟨n, r⟩ ∈ R

baseRelSym_mem_relSym for the raw pair, the simp normal form of baseRelSym ⟨n, r⟩.

@[simp]

theorem FirstOrder.Language.mk_graph_mem_relSym {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {n : ℕ} {f : L.Functions n} : ⟨n + 1, GraphRelation.graph f⟩ ∈ relSym F R ↔ ⟨n, f⟩ ∈ F

graphRelSym_mem_relSym for the raw pair, the simp normal form of graphRelSym ⟨n, f⟩.

@[simp]

theorem FirstOrder.Language.preimage_baseRelSym_relSym {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : baseRelSym ⁻¹' relSym F R = R

The relation symbols of L whose base symbol comes from F and R are those of R.

@[simp]

theorem FirstOrder.Language.preimage_graphRelSym_relSym {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : graphRelSym ⁻¹' relSym F R = F

The function symbols of L whose graph symbol comes from F and R are those of F.

@[simp]

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

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

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

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

The shared-vocabulary identity: the graph-language symbols coming from two pairs of symbol sets meet exactly in the symbols coming from the shared symbols.

The graph expansion

@[instance_reducible]

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

The graph expansion of an L-structure: relation symbols of L keep their interpretation, and the graph relation of f holds of (x₀, …, x_{k-1}, y) exactly when f(x₀, …, x_{k-1}) = y. The graph language has no function symbols to interpret.

@[simp]

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

@[simp]

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

theorem FirstOrder.Language.nonempty_equiv_graphExpansion_iff {L : Language} {M : Type w} [L.Structure M] {N : Type w'} [L.Structure N] : Nonempty (L.graphLanguage.Equiv M N) ↔ Nonempty (L.Equiv M N)

Two structures are isomorphic exactly when their graph expansions are: an L-isomorphism preserves the graph of every function symbol, and a bijection preserving these graphs commutes with the function symbols.