feat(model_theory/graph): First-order language and theory of graphs (#13720)
Defines `first_order.language.graph`, the language of graphs
Defines `first_order.Theory.simple_graph`, the theory of simple graphs
Produces models of the theory of simple graphs from simple graphs and vice versa.