empty graph in nLab
Context
Graph theory
Properties
Extra properties
Extra structure
Contents
Idea
The empty graph is the graph with empty set of vertices and empty set of edges.
Properties
The empty graph is the initial object in any reasonable category of graphs (such as a category of simple graphs).
The free category on the empty graph is the empty category.
Some notions of non-empty graphs
For concreteness let us consider the topos of quivers. The inhabited graphs, i.e. those satisfying ⊤⊢(∃x)⊤\top\vdash (\exists x)\top are precisely the graphs GG having an edge since the formula on the right is interpreted as the image of the composite G↪idG→1G\overset{id}{\hookrightarrow} G\to 1 but 11 being the loop graph and in order to validate the sequent, its loop must be contained in the image requiring an edge in the source. This notion of being inhabited is stronger than being non-empty ≠∅\neq\empty but weaker as having a (global) element 1→G1\to G which corresponds to graphs containing a loop. A uninhabited graph satisfying (∃x)⊤⊢⊥(\exists x)\top\vdash \bot is necessarily empty whence edgeless graphs with a node are internally neither inhabited nor uninhabited.