First-Ordered 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.
Instances For
The symbol representing the adjacency relation.
Instances For
Any simple graph can be thought of as a structure in the language of graphs.
Instances For
The theory of simple graphs.
Instances For
@[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 => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) ∧ Symmetric fun x y => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]
@[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)
:
def
FirstOrder.Language.simpleGraphOfStructure
(V : Type w')
[FirstOrder.Language.Structure FirstOrder.Language.graph V]
[V ⊨ FirstOrder.Language.Theory.simpleGraph]
:
Any model of the theory of simple graphs represents a simple graph.
Instances For
@[simp]