First-Order Structures in Graph Theory

This file defines first-order languages, structures, and theories in graph theory.

Main Definitions

• FirstOrder.Language.graph is the language consisting of a single relation representing adjacency.
• SimpleGraph.structure is the first-order structure corresponding to a given simple graph.
• FirstOrder.Language.Theory.simpleGraph is the theory of simple graphs.
• FirstOrder.Language.simpleGraphOfStructure gives the simple graph corresponding to a model of the theory of simple graphs.

Simple Graphs

inductive FirstOrder.Language.graphRel : ℕ → Type

The type of relations for the language of graphs, consisting of a single binary relation adj.

• adj : graphRel 2

def FirstOrder.Language.instDecidableEqGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : graphRel a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.Language.instDecidableEqGraphRel.decEq FirstOrder.Language.graphRel.adj FirstOrder.Language.graphRel.adj = isTrue FirstOrder.Language.instDecidableEqGraphRel.decEq._proof_1

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqGraphRel {a✝ : ℕ} : DecidableEq (graphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqGraphRel = FirstOrder.Language.instDecidableEqGraphRel.decEq

def FirstOrder.Language.graph : Language

The language consisting of a single relation representing adjacency.

Equations

• FirstOrder.Language.graph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.graphRel }

instance FirstOrder.Language.instIsRelationalGraph : Language.graph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.adj : Language.graph.Relations 2

The symbol representing the adjacency relation.

Equations

• FirstOrder.Language.adj = FirstOrder.Language.graphRel.adj

@[instance_reducible]

def SimpleGraph.structure {V : Type u} (G : SimpleGraph V) : FirstOrder.Language.graph.Structure V

Any simple graph can be thought of as a structure in the language of graphs.

Equations

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

instance FirstOrder.Language.graph.instSubsingleton {n : ℕ} : Subsingleton (Language.graph.Relations n)

def FirstOrder.Language.Theory.simpleGraph : Language.graph.Theory

The theory of simple graphs.

Equations

• FirstOrder.Language.Theory.simpleGraph = {FirstOrder.Language.adj.irreflexive, FirstOrder.Language.adj.symmetric}

@[simp]

theorem FirstOrder.Language.Theory.simpleGraph_model_iff {V : Type u} [Language.graph.Structure V] : V ⊨ Theory.simpleGraph ↔ (Std.Irrefl fun (x y : V) => Structure.RelMap adj ![x, y]) ∧ Std.Symm fun (x y : V) => Structure.RelMap adj ![x, y]

instance FirstOrder.Language.simpleGraph_model {V : Type u} (G : SimpleGraph V) : V ⊨ Theory.simpleGraph

def FirstOrder.Language.simpleGraphOfStructure (V : Type u) [Language.graph.Structure V] [V ⊨ Theory.simpleGraph] : SimpleGraph V

Any model of the theory of simple graphs represents a simple graph.

Equations

• FirstOrder.Language.simpleGraphOfStructure V = { Adj := fun (x y : V) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y], symm := ⋯, loopless := ⋯ }

@[simp]

theorem FirstOrder.Language.simpleGraphOfStructure_adj (V : Type u) [Language.graph.Structure V] [V ⊨ Theory.simpleGraph] (x y : V) : (simpleGraphOfStructure V).Adj x y = Structure.RelMap adj ![x, y]

@[simp]

theorem SimpleGraph.simpleGraphOfStructure {V : Type u} (G : SimpleGraph V) : FirstOrder.Language.simpleGraphOfStructure V = G

@[simp]

theorem FirstOrder.Language.structure_simpleGraphOfStructure {V : Type u} [S : Language.graph.Structure V] [V ⊨ Theory.simpleGraph] : (simpleGraphOfStructure V).structure = S

theorem FirstOrder.Language.Theory.simpleGraph_isSatisfiable : Theory.simpleGraph.IsSatisfiable