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.

Is there any literature where these "obvious" questions have been studied? 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.