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

def FirstOrder.Language.graph : FirstOrder.Language

The language consisting of a single relation representing adjacency.

Equations

• FirstOrder.Language.graph = FirstOrder.Language.mk₂ Empty Empty Empty Empty Unit

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

The symbol representing the adjacency relation.

Equations

• FirstOrder.Language.adj = ()

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

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

Equations

• SimpleGraph.structure G = FirstOrder.Language.Structure.mk₂ Empty.elim Empty.elim Empty.elim Empty.elim fun (x : Unit) => G.Adj

instance FirstOrder.Language.graph.instIsRelational : FirstOrder.Language.IsRelational FirstOrder.Language.graph

Equations

• FirstOrder.Language.graph.instIsRelational = (_ : FirstOrder.Language.IsRelational (FirstOrder.Language.mk₂ Empty Empty Empty Empty Unit))

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

Equations

• (_ : Subsingleton (FirstOrder.Language.graph.Relations n)) = (_ : Subsingleton ((FirstOrder.Language.mk₂ Empty Empty Empty Empty Unit).Relations n))

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

The theory of simple graphs.

Equations

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

@[simp]

theorem FirstOrder.Language.Theory.simpleGraph_model_iff {V : Type w'} [FirstOrder.Language.Structure FirstOrder.Language.graph V] : V ⊨ FirstOrder.Language.Theory.simpleGraph ↔ (Irreflexive fun (x y : V) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) ∧ Symmetric fun (x y : V) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]

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

Equations

• (_ : V ⊨ FirstOrder.Language.Theory.simpleGraph) = (_ : V ⊨ FirstOrder.Language.Theory.simpleGraph)

@[simp]

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

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

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

Equations

• FirstOrder.Language.simpleGraphOfStructure V = SimpleGraph.mk fun (x y : V) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]

@[simp]

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

@[simp]

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

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