# 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 #

The language consisting of a single relation representing adjacency.

Equations
Instances For

The symbol representing the adjacency relation.

Equations
Instances For
def SimpleGraph.structure {V : Type w'} (G : ) :

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

Equations
Instances For

The theory of simple graphs.

Equations
Instances For
@[simp]
theorem FirstOrder.Language.Theory.simpleGraph_model_iff {V : Type w'} [FirstOrder.Language.graph.Structure V] :
(Irreflexive fun (x y : V) => ) Symmetric fun (x y : V) =>
instance FirstOrder.Language.simpleGraph_model {V : Type w'} (G : ) :
Equations
• =
@[simp]
theorem FirstOrder.Language.simpleGraphOfStructure_adj (V : Type w') [FirstOrder.Language.graph.Structure V] (x : V) (y : V) :

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

Equations
• = { Adj := fun (x y : V) => , symm := , loopless := }
Instances For
@[simp]
theorem SimpleGraph.simpleGraphOfStructure {V : Type w'} (G : ) :
@[simp]