# Literature about most basic existence proofs in graph theory

I'm writing a MIZAR article about foundations in graph theory e.g. constructing a supergraph from a given graph by adding a vertex to it. The main theorem of the article will be that any graph drawable by hand (i.e. with finitely many vertices and edges) actually exists mathematically and can be constructed inductively.

Question: Is there any literature where these "obvious" questions have been studied? I'm looking for references. Any textbook I encountered just gave one mathematical definition of graphs (e.g. pair of vertex set and subset of the set of all 2-element subsets of the vertex set) and then just printed examples in picture form. A more concrete example: the path graph ._ ._ ._ ... _. is often pictured, sometimes with length $n$ as I just did, sometimes with certain lengths to avoid "..." in the pictures. Sometimes it is said to be constructed by starting with the trivial graph and just adding an edge and vertex to one of its endpoints, which is closest to a formal definition of the path graph, but the process of this adding itself is never justified, allegedly because it is so obvious. But set theory was obvious too for quite some time, so I'm hoping something has been done on this matter. On the other hand, of course it would be quite fulfilling to be a pioneer in this field, but frankly I don't want to end up writing things like "a topic that is so natural to mathematicians that hardly anyone bothers to mention it explicitly at all".

For me to know that I should have read a lot of books of graph theory and I haven't. Most are for undergraduate students in mathematics and computer science and are all quite similar. Even advanced books like "Selected topics in graph theory" (Ed. Lowell W. Beineke, 1978) don't cover this subject. So I'm hoping someone here knows such a book or paper by chance.

• You want to prove that a finite graph $G=(E, V)$ is obtainable from a subgraph $(E', V')$ by sucessive inclusions of subgraphs of G? You are basically asking for some "filtration" of G? This shouldn't be difficult to prove, especially since G is finite. – Ali Caglayan Dec 23 '17 at 9:30
• @AliCaglayan The proofs are done already, cumbersome, but only because they are technical and made for multigraphs $G=(V,E,S,T)$. I'm asking for literature having done that before. Filtration is a good key word, always avoided that topic until now. I'll have a look at it. – SK19 Dec 23 '17 at 9:56
• @AliCaglayan Now I remember why I omitted it. Seems to use some Algebra (Groups/Rings/etc) and that field isn't exactly my favourite. The proofs of the examples above can be done without any algebra of rings/groups etc, but works closely with the definitions of the graphs. If you however know a reference, where filtration results are applied to Graph theory, I would like to know. – SK19 Dec 23 '17 at 10:03
• It is still rather unclear to me what you are looking for. What does it mean for a graph to "exist mathematically"? The way I read your question, your "Theorem" is that for any finite graph $G$ there exists a sequence $G_0, G_1, \ldots, G_n$ of graphs $G_i$ such that $G_0$ is the empty graph, $G_n = G$ and $G_{i+1}$ is obtained from $G_i$ by adding a single vertex and some edges to vertices of $G_i$. But that seems to be a triviality, unless you work in some severely restricted logical universe. Please clarify what you have in mind. – monkeymaths Dec 31 '17 at 12:37
• @monkeymaths "unless you work in some severely restricted logical universe" Yes, restricted in the sense that common sense cannot be applied. In my Analysis III course back in the days there have been some very obvious but still cumbersome to prove theorems in Lebesgue integration. This is the same situation here in graph theory. It is obvious, yes, but to do it "purely mathematically", you have to define what "adding an edge" etc. is, with the $G=(V,E)$ definition (or whatever you use). Cumbersome. My question: Do you know where this has been done in detail before? – SK19 Dec 31 '17 at 21:51