Revision of PART 16 GRAPH THEORY in set.mm

[Alexander van der Vekens]

In October 2020, I started the revision of the definitions and theorems for Graph Theory (PART 16 of set.mm), based on the discussion in Github issue #1418:

Since the beginning of dealing with graph theory in set.mm, the question if graphs shall be represented as ordered pairs (of a set of vertices and a set of edges) or as extensible structures (the set of vertices as base set, and a special slot for the edges) was open (the current graph theory in PART 16 is based on the representation by ordered pairs).

The new approach is based on the definitions ~df-vtx and ~df-iedg for functions Vtx and iEdg to get the vertices and (indexed) edges of graphs represented by an arbitrary class G, and this works for G being either an ordered pair or an extensible structure (and some other, maybe degenerated cases). If required, other representations could be supported by extending the two definitions in the future (with no changes of the other definitions and theorems!). The revised graph theory is build on these two functions (usually setting V = ( Vtx ` G )and E = ( iEdg ` G ) and using V and E in the definitions and theorems only), disregarding the concrete representation of a graph. Therefore, a decision how to represent a graph will be not necessary anymore.

This was the main objective for the revision of the graph theory. Additional motivations were:

• Provision of a general framework for graphs
• Alignment of Eulerian Paths with the general concepts of walks, trails and paths

During the revision, a lot of additional improvements could be achieved:

• simplifications, generalisations and alignments of definitions and theorems,
• many proof shortenings
• improvement/enhancement of comments
• additional bibliographic references

The revision of PART 16 is currently contained in section "21.34.8 Graph theory (revised)" of my mathbox.

In the following, the main changes are explained in more detail:

• definition of functions Vtx and iEdg which provides the vertices resp. indexed edges of an arbitrary class regarded as graph. This allows representations of graphs as ordered pairs <. V , E >. as well as extensible structures { <. ( Base ndx ) , V >. , <. ( .ef ndx ) , E >. , ...}, see sections 21.34.8.1 and 21.34.8.2.
• revision of the definitions for hyper-/pseudo-/multi-/simple graphs based on the functions Vtx and iEdg , see sections 21.34.8.3, 21.34.8.4 and 21.34.8.7
• relationship between graphs and "incidence structures", see section 21.34.8.3
• the graphs formerly called "multigraphs" are now called "pseudographs", whereas "multigraphs" are special pseudographs (still with multiedges, but without loops) now, see section 21.34.8.4
• more systematic usage of the definition of (not indexed) edges, see section 21.34.8.6
• provison of a definition for subgraphs, see section 21.34.8.9
• provison of a definition for finite graphs, see section 21.34.8.10
• revision of the definitions for neighbors, complete graphs, universal vertices and connected graphs based on the functions Vtx and iEdg , see sections 21.34.8.11 and 21.34.8.25
• definition NN0* and related theorems for extended nonnegative integers added, see section 21.34.7.19
• revision of the definition for the vertex degree based on the functions Vtx and iEdg and to be appropriate for arbitrary hypergraphs, see section 21.34.8.12
• revision of the definition for regular graphs (including regular graphs with infinite degree) based on the functions Vtx and iEdg and to be appropriate for arbitrary hypergraphs, see section 21.34.8.13
• revision of the definition for walks, closed walks, walks in regular graphs, trails, (simple) paths, circuits and circles based on the functions Vtx and iEdg and to be appropriate for arbitrary hypergraphs, see sections 21.34.8.14, 21.34.8.16, 21.34.8.17, 21.34.8.18, 21.34.8.19 and 21.34.8.22
• special theorems for loop-free graphs and walks in loop-free graphs, see sections 21.34.8.5 and 21.34.8.15
• examples for short walks, trails, etc. (up to a length of 4) added and revised, mainly based on "words", see section 21.34.8.24
• revision of the definition for (closed) walks as words based on the functions Vtx and iEdg and to be appropriate for arbitrary hypergraphs, see sections 21.34.8.20 and 21.34.8.23
• equivalence of walks represented as words and the "usual way" for pseudographs (which can have multiple edges between two vertices) shown by using the Axiom of Choice (not required for the corresponding theorem for simple pseudographs!), see section 21.34.8.20.
• replacement of "Walks/paths of length 2 as ordered triples" by "Walks/paths of length 2 (as length 3 strings)", see section 21.34.8.21
• revision of the definition of Eulerian paths based on the definition of walks and trails, see section 21.34.8.26
• revision of the Koenigsberg Bridge problem, based on the revised definition of eulerian paths (and other, required concepts), see section 21.34.8.27
• revision of the definition of friendship graphs, the friendship theorem and its proof following Huneke's approach, based on the revised defintion of friendship graphs, see sections 21.34.8.29, 21.34.8.30 and 21.34.8.31

The next main step will be to replace "PART 16 GRAPH THEORY" entirely by section
"21.34.8 Graph theory (revised)" of my mathbox. Everything contained in PART 16 is
contained in section 21.34.8, so there will be no loss of information/knowledge.
On the contrary, section 21.34.8 (about 1300 statements) provides more information/knowledge than PART 16 (about 800 statements).

The names I used for class symbols and labels are in part temporary, because they overlap with the current names in PART 16. They will be adjusted after PART 16 is replaced by the revised material. However, suggestions for improved names are always welcome.

I want to ask everybody who is interested in graph theory, and who has some spare time, to have a look at the revised definitions and theorems in section 21.34.8 of my mathbox, and to provide advices and suggestions for further improvements before I continue.
Please give feedback until end of July, I plan to perform the replacement starting in August.

In the meantime, I will perform some minor additinal improvements/adjustments, and I will clean up section 21.34.9 of my mathbox, which is almost completely covered by section 21.34.9. The remaining theorems will be revised and moved to section 21.34.9. before the replacement of PART 16.

[David A. Wheeler]

> On Jun 5, 2021, at 8:31 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
>
> In October 2020, I started the revision of the definitions and theorems for Graph Theory (PART 16 of set.mm), based on the discussion in Github issue #1418:
>
> Since the beginning of dealing with graph theory in set.mm, the question if graphs shall be represented as ordered pairs (of a set of vertices and a set of edges) or as extensible structures (the set of vertices as base set, and a special slot for the edges) was open (the current graph theory in PART 16 is based on the representation by ordered pairs).
>
> The new approach is based on the definitions ~df-vtx and ~df-iedg for functions Vtx and iEdg to get the vertices and (indexed) edges of graphs represented by an arbitrary class G, and this works for G being either an ordered pair or an extensible structure (and some other, maybe degenerated cases). If required, other representations could be supported by extending the two definitions in the future (with no changes of the other definitions and theorems!). The revised graph theory is build on these two functions (usually setting V = ( Vtx ` G )and E = ( iEdg ` G ) and using V and E in the definitions and theorems only), disregarding the concrete representation of a graph. Therefore, a decision how to represent a graph will be not necessary anymore.

It all makes sense to me. I think it’s important that this explanation be in set.mm itself, either as part of the new PART 16 header description, or as part of a key definition (like df-vtx). A brief description on “why is this representation being used” would help people understand it.

--- David A. Wheeler