Graph Theory

[Alexander van der Vekens]

I create this topic to (re)start the discussion about graph theory in Metamath.
To allow for a better structured discussion, I will summarize the current state, previous discussions and further proposals in subtopics (replies to this topic).

There are mainly two topics in this Metamath Google Group containing essential material about graph theory (I searched for "graph" (26 hits) and "graph theory" (10 hits)):

• "set.mm update" (Mario Carneiro 16.04.2015 11:10): https://groups.google.com/d/topic/metamath/VAGNmzFkHCs/discussion
  
• "Best way to define things"  (r00nk 16.01.2017 04:21): https://groups.google.com/d/topic/metamath/05rpwBurSmc/discussion
  

In set.mm, definitions and theorems for "graphs" are contained in the following Mathboxes:

• Mathbox of Mario:
• Undirected Multigraphs (~ df-umgra to ~ konigsberg, see also Topic "set.mm update" in the Metamath Google Group)
• Mathbox of FL:
• "Graphs of a deductive system" and "graphs of a morphism"
• These seem to be special cases of graphs

My goal is to prove the friendship theorem from the "100 theorem list" (#83). I started with this before I read the post of r00nk who claimed to prove this theorem, too. However, since my definitions base on df- umgra (r00nk did it the same way), which is still contained only in Mario's mathbox, and Mario indicated that this definition will be reworked, I stop working (after I created an *.mm-file with more than 3000 lines already) until a stable basis is available, which will hopefully be the case after the disussions in this topic.

Regards,

Alexander

[Alexander van der Vekens]

Here is an extract of the topic "set.mm update" (Mario Carneiro 16.04.2015 11:10, https://groups.google.com/d/topic/metamath/VAGNmzFkHCs/discussion), containing the essential parts about graph theory (because this topic is very huge and a lot of various things are discussed there):

 Mario Carneiro 16.04.2015 11:10
....
==Graph Theory==

df-umgra: One thing that worries me about graph theory more than any other field is the fact that they have no uniform foundation to build on, and we don't have the nice "an X is a Y"-type theorems that the structure builders are giving us in abstract algebra. The goal in this section was to prove the Konigsberg Bridge problem, which involves an undirected, non-simple graph. So I defined <. V , E >. e. UMGrph if E is a function from some set to the collection of 1- and 2-element subsets of V.
Note that if this were a directed graph, it would probably be a function into ordered pairs instead, so G e. DMGrph -> G e. UMGrph would be a non-theorem; if I had a simple graph, E might be a subset of V X. V instead of a function, and then G e. SGrph -> G e. UMGrph would be a non-theorem. I'm still not sure how best to address this problem, but for the moment my thoughts are to just ignore the problem and work with each foundation separately, using isomorphism theorems to translate as necessary. That's part of the reason why I made no attempt to work df-umgra into the extensible structure framework, because there is no obvious uniform way to do it.

eupath: The main theorem of Eulerian paths, which says that the number of vertices of odd degree in an Eulerian graph is either 0 or 2, depending on whether the path returns to the starting point.

konigsberg: The Konigsberg Bridge problem, which says that a certain specific graph has no Eulerian paths. In order to concisely state the vertex and edge information I used a similar approach to the decimal arithmetic theorems, with a small collection of "structural induction" theorems on the edge set, stored as an ordered list. For larger graphs a different storage mechanism may be more appropriate. This is also a metamath 100 theorem.
...

Stefan O'Rear 17.04.2015 09:35
...
I've dabbled with that a bit in the past, and tended towards a factoring more like this:

inci = ( f e. _V |-> ( f ` ( 10 + 4 ) ) )
$( either ran ( inci ` s ) or dom ( inci ` s ) has a claim to the word "edge" $)
edgeDir = ( f e. _V |-> ( f ` ( 10 + 5 ) ) )
$( An incidence structure (a multi-hypergraph) is a base set equipped with a family of subsets. $)
InciSy = { s e. _V | ( inci ` s ) : dom ( inci ` s ) --> ~P ( Base ` s ) }
$( A multigraph is an incidence structure where each edge is a pair. $)
Multigraph = { s e. InciSy | A. e e. ran ( inci ` s ) ( e ~~ 1o \/ e ~~ 2o ) }
$( A quiver/multidigraph is an incidence structure with an additional structure of an ordering for each edge. $)
Quiver = { s e. Multigraph | ( ( edgeDir ` s ) : dom ( inci ` s ) --> ( ( Base ` s ) X. ( Base ` s ) ) /\ A. x e. dom ( inci ` s ) ( ( inci ` s ) ` x ) = U. ( ( edgeDir ` s ) ` x ) ) }
$( A hypergraph is an incidence structure with no empty edges and no repeated edges. $)
Hypergraph = { s e. InciSy | ( (/) e/ ran ( inci ` s ) /\ Fun `' ( inci ` s ) ) }
$( A simple graph is a multigraph with no repeated edges or loops $)
SimpleGraph = { s e. InciSy | ( Fun `' ( inci ` s ) /\ A. e e. ran ( inci ` s ) e ~~ 2o ) }
$( there are several natural candidates for "directed graph"; ( SimpleGraph i^i Quiver ) is one $)
$( Undirected connectivity $)
USTCON = ( g e. InciSy |-> [_ ( Base ` g ) / b ]_ |^| { r e. ~P ( b X. b ) | ( ( _I |` b ) C_ r /\ ( r o. r ) C_ r /\ A. x e. b A. y e. b ( E. z e. ran ( inci ` g ) { x , y } C_ z -> x r y ) } )
$( Directed connectivity; see also df-trcl $)
STCON = ( g e. Quiver |-> [_ ( Base ` g ) / b ]_ |^| { r e. ~P ( b X. b ) | ( ( _I |` b ) C_ r /\ ran ( edgeDir ` g ) C_ r /\ ( r o. r ) C_ r ) } )
$( Connected multigraphs $)
ConInci = { g e. InciSy | A. s e. ( Base ` g ) A. t e. ( Base ` g ) s ( USTCON ` g ) t }
$( Convert a graph to a topological space; this creates one arc per vertex/edge pair.  Wrong for graphs with loops since it doesn't account for "incidence multiplicity" / fails to distinguish a loop from a "dangling edge".  For multidigraphs, an obvious alternative is to use one edge per vertex.  Shinichi Mochizuki prefers "semigraphs" with dangling edges to be topologically non-closed... $)
graph2top = ( g e. InciSy |-> [_ ( Base ` g ) / b ]_ [_ ( inci ` g ) / i ]_ ( ( ~P U_ x e. dom i ( { x } X. ( i ` x ) ) tX II ) qTop [_ ( U_ x e. dom i ( { x } X. ( i ` x ) ) X. ( 0 [,] 1 ) ) / s ]_ ( y e. s |-> [ y ] { <. p , q >. | ( ( p e. s /\ q e. s ) /\ ( p = q \/ ( ( 2nd ` p ) = 1 /\ ( 2nd ` q ) = 1 /\ ( 1st ` ( 1st ` p ) ) = ( 1st ` ( 1st ` q ) ) ) \/ ( ( 2nd ` p ) = 0 /\ ( 2nd ` q ) = 0 /\ ( 2nd ` ( 1st ` p ) ) = ( 2nd ` ( 1st ` q ) ) ) ) ) } ) ) )
$( ... you get the picture ... $)

I'm not sure how well this addresses your problems.  It probably introduces a few of its own.

I can't think of any natural example of something that is both an algebraic structure and a graph (not counting the graph structures that can be drawn on some algebraic structures, like Hasse diagrams and Cayley graphs); however graph theory has some natural notions of extensibility within itself, like weightings and constraint decorations.

Mario Carneiro     17.04.2015 10:43
Hmm, I kind of like that approach. One nice thing is that your approach is compatible with mine in the sense that the edge function is stored the same way, so that we have the theorem:

( <. V , E >. e. UMGra <-> { <. ( Base ` ndx ) , V >. , <. ( inci ` ndx ) , E >. } e. Multigraph )

Comparing to other graph definitions in set.mm:

( <. D , C , U >. e. DGra <-> { <. ( Base ` ndx ) , U >. ,
   <. ( inci ` ndx ) , ( x e. dom D |-> { ( D ` x ) , ( C ` x ) } ) >.
   <. ( edgeDir ` ndx ) , ( D oF _I C ) >. } e. Quiver )

( E : D -1-1-> ( _V \ A ) -> ( <. A , ran E >. e. HypGrph <->
 { <. ( Base ` ndx ) , A >. , <. ( inci ` ndx ) , E >. } e. Hypergraph ) )

PsGrph doesn't have an equivalent, although it's a very strange structure - the edges can either have one end or they can be directed with two ends (a one-vertex edge is distinct from a self-loop).

( E : D -1-1-> ( _V \ A ) -> ( <. A , ran E >. e. SmpGrph <->
 { <. ( Base ` ndx ) , A >. , <. ( inci ` ndx ) , E >. } e. SimpleGraph ) )
(assuming df-sgra is fixed according to the comment)

(By the way, a nice recently discovered idiom: Assuming F : A --> B and G : A --> C, ( F oF _I G ) : A --> ( B X. C ) is the function sometimes called (F x G) in math prose which satisfies ( ( F oF _I G ) ` x ) = <. ( F ` x ) , ( G ` x ) >. .)

The counting of VDeg is a bit difficult to generalize, though. It is designed so that a self-loop contributes 2 to the degree of a vertex, which makes sense for Multigraph but not for Hypergraph, when it would probably make more sense for an edge to contribute 1 to each vertex it is incident with, so that a self-loop (or is it a dangling edge?) only adds 1 to the vertex degree.

Regarding actual changes, though, I'd rather hold off on all that machinery until we need it for something concrete like the Szemerédi regularity lemma or something.

[savask]

If it's not a secret, what is your proof idea for this problem? As far as I know, most proofs incorporate linear algebra (eigenvalues) in some form, and set.mm lacks that theory now. 3000 lines seems like a lot, so maybe actually proving some facts about matrices first would yield a shorter path.

[Alexander van der Vekens]

As Mario mentioned in "set.mm update" (https://groups.google.com/d/topic/metamath/VAGNmzFkHCs/discussion) and "Best way to define things"  (https://groups.google.com/d/topic/metamath/05rpwBurSmc/discussion), the definitions of (undirected multi)graphs should be based on the extensible structure framework. Are there already any efforts made in this direction?

In my opinion, a definition can be as follows:

  $c 11 $.
  $c edg $.
  $c UMGrphStr $.

  $( Extend class notation to include the number 11. $)
  c11 $a class 11 $.

  $( Extend class notation with graph edge function. $)
  cedg $a class edg $.

  $( Extend class notation with undirected multiple graphs (with loops)
     as extensible structure. $)
  cumgs $a class UMGrphStr $.

  $( Define the number 11.
  df-11 $a |- 11 = ( 10 + 1 ) $.

  $( Define edge function for graphs.
  df-edg $a |- edg = Slot 11 $.

  ${
    $d e g v x $.
    $( Definition of undirected multigraphs (with loops) as structure.
    df-umgrastr $a |- UMGrphStr
     = { g | [. ( Base ` g ) / v ]. [. ( edg ` g ) / e ].
             e : dom e --> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } } $.
  $}

@Mario: would this be the right approach? What do you plan for this? Can this basic definition (together with some basic theorems) included into the main part of set.mm, so that r00nk and I (and mybe others) can rely on it? Or is it better to move the existing definition df-umgra to the main part of set.mm and continue working with this definition? However, a transformation into extensible structures would be more difficult as more and more theorems are based on the current definition. Or is there an easy way/automatism to perform this transformation?

Regards,
Alexander

[Alexander van der Vekens]

On Monday, October 2, 2017 at 9:38:33 AM UTC+2, savask wrote:

If it's not a secret, what is your proof idea for this problem? As far as I know, most proofs incorporate linear algebra (eigenvalues) in some form, and set.mm lacks that theory now. 3000 lines seems like a lot, so maybe actually proving some facts about matrices first would yield a shorter path.

The first proof of the friendship theorem by P. Erdös et al. used linear algebra. However, there are other proofs availabe now which do not require linear algebra.

My goal is to formailze the proof published in the paper "The friendship problem on graphs" of G.B. Mertizios and W. Unger (ROGICS'08, 12-17 May 2008, Mahida, Tunisia, pp 152-158), which is based on a purely combinatorial approach. Nevertheless, you are right: a lot of auxiliary theorems required for this proof are not available in set.mm yet, so it was not (and will not be) easy to formalize this proof with Metamath.

[Mario Carneiro]

1. Don't define 11, use ; 1 1 instead

2. Don't use 11, we already have structure indexes up to 15 (see http://us.metamath.org/mpeuni/mmtheorems133.html), so make it 16, unless this slot is mutually exclusive with some other slot.

3. Unless you plan on actually reworking graph theory yourself, with the ability to handle most if not all of the variations that Stefan mentions in his post, I wouldn't attempt to modify UMGrph. The fact that it is sitting in my mathbox is no impediment - we can just move it to main if/when someone like yourself wants to use it in their own work.

In other words, just keep doing what you were: If UMGrph as stated is sufficient for your needs, then use it as is. If and when we eventually move to extensible structures, I would like it to be motivated by an actual use case that goes beyond the applicability of the current definition. Just shuffling the parts of UMGrph into slots doesn't actually make it any more useful - if the slots are all new and have no relation to anything else, and there are no combination structures like a ring which is an undirected graph as well, then it's just a complicated way to write ordered pairs.

Mario

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Alexander van der Vekens]

Hi Mario,
thanks for responding so quickly. So I will not do anything regarding extensible structures, but continue working with the current definitions. Actually, my work does not rely on df-umgra (and other definitions of your Mathbox), because I use a special definition for (undirected) simple graphs (as r00nk also did - I will provide details later):

  $( Undirected Simple Graph. This definition is loosely based on the UMGrph definition $)
  ${
    $d e v x $.
    df-usgra $a |- USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } } $.
  $}

I use df-umgra only to show
usisumgra $p |- ( V USGrph E -> V UMGrph E ) $=

Therefore, it is not required (at least for me) that the part from ~ df-umgra to ~ konigsberg is moved from your Mathbox into the main part of set.mm.
However, I would strongly prefer to move this part into the main part, because we cannot honestly say that #54 of the "100 theorem list" is proven by Metamath unless ~ konigsberg is in the main part ;-).

Regards,
Alexander

[Mario Carneiro]

On Mon, Oct 2, 2017 at 5:07 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

However, I would strongly prefer to move this part into the main part, because we cannot honestly say that #54 of the "100 theorem list" is proven by Metamath unless ~ konigsberg is in the main part ;-).

Hm, I don't think we've been using this criterion - there are quite a few of the 100 theorems in mathboxes, and since they tend to be endpoint theorems anyway there is less of a need for them to be shared with the main part. That's not to say that the 100 theorems don't belong in main, only that the criteria for inclusion doesn't really depend on this so much as other factors like maintainability and reusability. That UMGrph is getting related to other topics is a strong argument for inclusion in main, which we didn't have before.

Mario

[Benoit]

As for the definition of graphs, I propose the following version, which is more economical and closer to mathematical practice. Any thoughts ?

${
$d x y z A $.
$( Define the class of subsets of cardinality 2 of a given class. (symbol: \mathcal{P}_2) $)
df-calP_2 $a |- calP_2 A = { x | E. y e. A E. z e. A ( x = { y , z } /\ y =/= z ) } $.
$}

${
$d v e G $.
$( Define the predicate ``is an (undirected, simple, loopfree) graph''. $)
df-isGraph $a |- ( isGraph G <-> E. v E. e ( G = <. v , e >. /\ e C_ ( calP_2 ` v ) ) ) $.
$}

--
Benoit

[Mario Carneiro]

The main problem with definitions of this sort is that they don't generalize well. That is, if you care about simple graphs, you write down one definition, and then if you later care about non-simple graphs then you have a new definition that does not generalize the original (in the sense that a simple graph will not be a graph under the new definition). I need not point out that this definition already runs into this issue when comparing to UMGrph and the theorems around it. Are the theories of simple graphs and multigraphs to develop independently? The idea behind extensible structures is to minimize such fracturing and provide lots of transfer theorems like "a simple graph is a multigraph" that allow usage of one theory in the other.

Mario

--

[Alexander van der Vekens]

Hi Benoit,

On Monday, October 2, 2017 at 12:50:13 PM UTC+2, Benoit wrote:

As for the definition of graphs, I propose the following version, which is more economical and closer to mathematical practice. Any thoughts ?

${
$d x y z A $.
$( Define the class of subsets of cardinality 2 of a given class. (symbol: \mathcal{P}_2) $)
df-calP_2 $a |- calP_2 A = { x | E. y e. A E. z e. A ( x = { y , z } /\ y =/= z ) } $.
$}

${
$d v e G $.
$( Define the predicate ``is an (undirected, simple, loopfree) graph''. $)
df-isGraph $a |- ( isGraph G <-> E. v E. e ( G = <. v , e >. /\ e C_ ( calP_2 ` v ) ) ) $.
$}

--
Benoit

I also experimented with an alternative definition, in some extend similar to your proposal:

  ${
    $d e v x $.
    $( Define the class of all undirected simple graphs without loops.
       An undirected simple graph without loops is a special undirected simple
       graph ` <. V , E >. ` where ` E ` is an injective (one-to-one) function
       into subsets of ` V ` of cardinality two, representing the two
       vertices incident to the edge.
    df-ausgra $a |- AUSGrph = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } } $.

$}

This definition does not use an edge function, but simply represents the edges by unordered pairs (of vertices). However, for the sake of generalizability, as Mario mentioned in his reply, I did not use this definition. Nevertheless, the following can be proven, so the definitions are kind of equivalent:

ausisusgra $p |- ( ( V e. X /\ E e. Y ) -> ( V AUSGrph E <-> V USGrph ( _I |` E ) ) ) $=

Regards,
Alexander

[David A. Wheeler]

On October 2, 2017 5:07:49 AM EDT, 'Alexander van der Vekens'

>However, I would strongly prefer to move this part into the main part,
>because we cannot honestly say that #54 of the "100 theorem list" is
>proven
>by Metamath unless ~ konigsberg is in the main part ;-).

I disagree. In fact, being included in a mathbox is a far stronger criteria than many other systems use. In many other systems, there are proofs that can no longer be used because of changes in the underlying system. In contrast, once something is in a mathbox it will be adjusted as necessary to stay verifiable using Metamath.

I think we should move more things from mathboxes into the main section, but that is because I want to encourage reuse. Something proven in a mathbox is clearly proven by Metamath.


--- David A.Wheeler

[Benoit]

Hi Mario and Alexander,

On Monday, October 2, 2017 at 12:58:47 PM UTC+2, Mario Carneiro wrote:

The main problem with definitions of this sort is that they don't generalize well. That is, if you care about simple graphs, you write down one definition, and then if you later care about non-simple graphs then you have a new definition that does not generalize the original (in the sense that a simple graph will not be a graph under the new definition).

Indeed, if you care about graphs, you write a definition, and if you care about multigraphs, you write another definition. This is all very common. If you want to "consider a graph as a special kind of multigraph", then you define something like

|- GraphToUndirMultiGraph = ( g e. Graph |-> <. ( 1st ` g ) , ( _I |` ( 2nd ` g ) ) >. )

(similar to what Alexander wrote). Similarly, when you want to "consider a ring as a group", you use the "underlying additive group" functor.

I know you know all that, and I understand that my proposal might result sometimes in longer typing. But I think that closeness to mathematical practice is important, and that the statements of metamath should look as much as possible like textbook statements. In other words, I understand that there is a balance to find between "ease of coding" and "closeness to mathematical practice". I can ask around my colleagues what a graph is, but I doubt many will tell me "it is a set with an injective function from some domain to the set of 2-element subsets of that set". Furthermore, explicit writing of the "conversion" functor has advantages in terms of clarity.

--
Benoit
 

I need not point out that this definition already runs into this issue when comparing to UMGrph and the theorems around it. Are the theories of simple graphs and multigraphs to develop independently? The idea behind extensible structures is to minimize such fracturing and provide lots of transfer theorems like "a simple graph is a multigraph" that allow usage of one theory in the other.

Mario

On Mon, Oct 2, 2017 at 6:50 AM, Benoit <benoit...@gmail.com> wrote:

As for the definition of graphs, I propose the following version, which is more economical and closer to mathematical practice. Any thoughts ?

${
$d x y z A $.
$( Define the class of subsets of cardinality 2 of a given class. (symbol: \mathcal{P}_2) $)
df-calP_2 $a |- calP_2 A = { x | E. y e. A E. z e. A ( x = { y , z } /\ y =/= z ) } $.
$}

${
$d v e G $.
$( Define the predicate ``is an (undirected, simple, loopfree) graph''. $)
df-isGraph $a |- ( isGraph G <-> E. v E. e ( G = <. v , e >. /\ e C_ ( calP_2 ` v ) ) ) $.
$}

--
Benoit

On Monday, October 2, 2017 at 11:32:29 AM UTC+2, Mario Carneiro wrote:




On Mon, Oct 2, 2017 at 5:07 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

However, I would strongly prefer to move this part into the main part, because we cannot honestly say that #54 of the "100 theorem list" is proven by Metamath unless ~ konigsberg is in the main part ;-).



Hm, I don't think we've been using this criterion - there are quite a few of the 100 theorems in mathboxes, and since they tend to be endpoint theorems anyway there is less of a need for them to be shared with the main part. That's not to say that the 100 theorems don't belong in main, only that the criteria for inclusion doesn't really depend on this so much as other factors like maintainability and reusability. That UMGrph is getting related to other topics is a strong argument for inclusion in main, which we didn't have before.



Mario

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[Alexander van der Vekens]

To prove the friendship theorem, the concepts of paths and cycles within a graph are essential. Therefore, corresponding definitions are required.

I woud propose the following definitions:

    $( Define the set of all n-paths in an undirected graph.
       According to Wikipedia ("Path (graph theory)",
       https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017):
       A path is a trail in which all vertices (except possibly the first and
       last) are distinct. A trail is a walk in which all edges are distinct.
       A walk of length k in a graph is an alternating sequence of vertices and
       edges, v0 , e0 , v1 , e1 , v2 , ... , v(k−1) , e(k−1) , v(k) which
       begins and ends with vertices. If the graph is undirected, then the
       endpoints of e(i) are v(i) and v(i+1).
       An n-path is a path of length n, i.e. a trail consisting of n+1 vertices
       and n edges.
       Therefore, an n-path can be represented by two mappings f from
       { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the
       (indices of the) edges, and p enumerates the vertices. So the path is
       represented by the following sequence:
       p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)
       (Contributed by Alexander van der Vekens, 11-Aug-2017.) $)
    df-path $a |- Paths = ( n e. NN , g e. _V |-> { <. f , p >. | 
       ( ( f : ( 1 ... n ) -1-1-> dom  ( 2nd ` g )
       /\ p : ( 0 ... n ) --> ( 1st ` g ) )
       /\ ( p |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( 1st ` g ) )
      /\ ( A. k e. ( 1 ... n ) ( e ` ( f ` k ) )
                                 = { ( p ` ( k - 1 ) ) , ( p ` k ) } ) ) } ) $.

    $( Define the set of all n-cycles in a graph.
       According to Wikipedia ("Cycle (graph theory)",
       https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017):
       A (simple) cycle is a closed walk without repeated vertices (other than
       the repetition of the starting and ending vertex) or edges.
       A walk is an alternating sequence of vertices and edges, starting and
       ending at a vertex, in which each edge is adjacent in the sequence to
       its two endpoints.
       An n-cycle is a cycle of length n (having n vertices and n edges).
       Therefore, an n-cycle can be represented by two mappings f and p from
       { 0 , ... , n }, where f enumerates the (indices of the) edges, and p
       enumerates the vertices. So the cycle is represented by the following
       sequence: ... p(n-1) e(f(n)) p(n) e(f(0)) p(0) e(f(1)) p(1) e(f(2)) ...
       In an undirected graph, only cycles of length greater than 2 are
       meaningful.
    df-cycl $a |- Cycles = ( n e. NN , g e. V |-> { <. f , p >. |
      ( ( f : ( 0 ... ( n - 1 ) ) -1-1-> dom ( 2nd ` g )
        /\ p : ( 0 ... ( n - 1 ) ) -1-1-> ( 1st ` g ) )
      /\ ( A. k e. ( 1 ... ( n - 1 ) ) ( e ` ( f ` k ) )
           = { ( p ` ( k - 1 ) ) , ( p ` k ) }
           /\ ( e ` ( f ` 0 ) ) = { ( p ` ( n - 1 ) ) , ( p ` 0 ) } ) ) } ) $.

These definitions ( ( n Paths g ) and ( n Cycles g ) ) should be meaningful for undirected simple graphs (g e. USGrph) as well as for undirected multigraphs (g e. UMGrph).

Furthermore, they should be compatible with each other ( c e. ( n Cycles g ) -> c e. ( n Paths g ) ) as well as with the existing definition of an Eulerian path
 ( p e. ( V EulPaths E ) -> E. n e. NN p e. ( n Paths <. V , E >. ) ) .

Are there any objections/improvements/remarks?

[Alexander van der Vekens]

I found out that we have to be careful about repeated vertices, so in my previous proposal  ( p e. ( V EulPaths E ) -> E. n e. NN p e. ( n Paths <. V , E >. ) ) would not hold!
Since we must exclude repeated vertices for the friendship theorem, but repeated vertices are required for Eulerian paths (and to prove ~ konigsberg ), I modify my proposal es follows:

    $( Define the set of all n-trails in an undirected graph.

       According to Wikipedia ("Path (graph theory)",
       https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017):

       "A trail is a walk in which all edges are distinct.
       A walk of length k in a graph is an alternating sequence of vertices and
       edges, v0 , e0 , v1 , e1 , v2 , ... , v(k−1) , e(k−1) , v(k) which
       begins and ends with vertices. If the graph is undirected, then the
       endpoints of e(i) are v(i) and v(i+1)."

       An n-trail is a walk of length n, i.e. a trail consisting of n+1
       vertices and n edges.
       Therefore, an n-trail can be represented by two mappings f from

       { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the

       (indices of the) edges, and p enumerates the vertices. So the trail is

       represented by the following sequence:
       p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)

       (Contributed by Alexander van der Vekens, 3-Oct-2017.) $)
    df-ntrl $a |- Trails = ( n e. NN , g e. V |-> { <. f , p >. |

          ( f : ( 1 ... n ) -1-1-> dom ( 2nd ` g )
         /\ p : ( 0 ... n ) --> ( 1st ` g ) )

         /\ ( A. k e. ( 1 ... n ) ( ( 2nd ` g ) ` ( f ` k ) )

                                 = { ( p ` ( k - 1 ) ) , ( p ` k ) } ) ) } ) $.

    $( Define the set of all (simple) n-paths in an undirected graph.

       According to Wikipedia ("Path (graph theory)",
       https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017):
       "A path is a trail in which all vertices (except possibly the first and

       last) are distinct. ... use the term simple path to refer to a path
       which contains no repeated vertices."
       (Contributed by Alexander van der Vekens, 3-Oct-2017.) $)
    df-npth $a |- Paths = ( n e. NN , g e. V |-> { <. f , p >. |
      ( <. f , p >. e. ( n Trails g )
           /\ ( p |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( 1st ` g ) ) } ) $.

    $( Define the set of all n-circuit in a graph.

       According to Wikipedia ("Cycle (graph theory)",
       https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017):

       "A circuit can be a closed walk allowing repetitions of vertices but not
       edges;"
       An n-circuit is a closed walk without repeated edges of length n (having

       n vertices and n edges).

       Therefore, an n-circuit can be represented by two mappings f and p from

       { 0 , ... , n }, where f enumerates the (indices of the) edges, and p

       enumerates the vertices. So the circuit is represented by the following

       sequence: ... p(n-1) e(f(n)) p(n) e(f(0)) p(0) e(f(1)) p(1) e(f(2)) ...

       (Contributed by Alexander van der Vekens, 3-Oct-2017.) $)
    df-ncrct $a |- Circuits = ( n e. NN , g e. V |-> { <. f , p >. |

       ( f : ( 0 ... ( n - 1 ) ) -1-1-> dom ( 2nd ` g )

      /\ p : ( 0 ... ( n - 1 ) ) --> ( 1st ` g )
      /\ ( A. k e. ( 1 ... ( n - 1 ) ) (  ( 2nd ` g ) ` ( f ` k ) )

           = { ( p ` ( k - 1 ) ) , ( p ` k ) }

           /\ (  ( 2nd ` g ) ` ( f ` 0 ) ) = { ( p ` ( n - 1 ) ) , ( p ` 0 ) } ) ) } ) $.

    $( Define the set of all (simple) n-cycles in a graph.

       According to Wikipedia ("Cycle (graph theory)",
       https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017):

       "A simple cycle may be defined either as a closed walk with no
       repetitions of vertices and edges allowed, other than the repetition of
       the starting and ending vertex,"

       An n-cycle is a cycle of length n (having n vertices and n edges).
       Therefore, an n-cycle can be represented by two mappings f and p from
       { 0 , ... , n }, where f enumerates the (indices of the) edges, and p
       enumerates the vertices. So the cycle is represented by the following
       sequence: ... p(n-1) e(f(n)) p(n) e(f(0)) p(0) e(f(1)) p(1) e(f(2)) ...

       (Contributed by Alexander van der Vekens, 3-Oct-2017.) $)
    df-ncycl $a |- Cycles = ( n e. NN , g e. ( _V X. _V ) |-> { <. f , p >. |

         ( f : ( 0 ... ( n - 1 ) ) -1-1-> dom ( 2nd ` g )
        /\ p : ( 0 ... ( n - 1 ) ) -1-1-> ( 1st ` g )

        /\ ( A. k e. ( 1 ... ( n - 1 ) ) (  ( 2nd ` g ) ` ( f ` k ) )

             = { ( p ` ( k - 1 ) ) , ( p ` k ) }

           /\ ( ( 2nd ` g ) ` ( f ` 0 ) ) = { ( p ` ( n - 1 ) ) , ( p ` 0 ) } ) ) } ) $.

With these definitions, the following theorems should be valid:

    npthntrl $p |- ( P e. ( N Paths G ) -> P e. ( N Trails G ) $=
    ncyclncrct $p |- ( C e. ( N Cycles G ) -> C e. ( N Circuits G ) $=
    ncrctntrl $p |- ( C e. ( N Circuits G ) -> C e. ( N Trails G ) $=
    ncyclnpth $p |- ( C e. ( N Cycles G ) -> C e. ( N Paths G ) $=
    eupantrl $p |- ( P e. ( V EulPaths E ) -> E. n e. NN P e. ( n Trails <. V , E >. ) ) $=

[Mario Carneiro]

Let's cut down on the duplication here.

On Tue, Oct 3, 2017 at 11:25 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

    df-trl $a |- Trails = ( n e. NN , g e. V |-> { <. f , p >. |

          ( f : ( 1 ... n ) -1-1-> dom ( 2nd ` g )
         /\ p : ( 0 ... n ) --> ( 1st ` g ) )

         /\ ( A. k e. ( 1 ... n ) ( e ` ( f ` k ) )

                                 = { ( p ` ( k - 1 ) ) , ( p ` k ) } ) ) } ) $.

Watch your V, that should be _V (although mmj2 definition checker will also point this out). But for a general theory, I suggest starting where Wikipedia does, at "walk":

    df-wks $a |- Walks = ( v e. _V , e e. _V |-> { <. f , p >. |
          E. n e. NN0 ( f : ( 1 ... n ) --> dom e /\ p : ( 0 ... n ) --> v )
         /\ A. k e. ( 1 ... n ) ( e ` ( f ` k ) ) = { ( p ` ( k - 1 ) ) , ( p ` k ) } ) } ) $.

This is an important starting point because it has none of the restrictions of the other kinds of things, but it has the same type as the others, so you can define things like "start point", "length", "subwalk" on this and they will continue to make sense on paths, trails, cycles, eulerian paths etc. (Looking back at the definition of df-eupa, I see how you may have gotten the idea to build in the UMGrph restriction into the paths. I probably sent a mixed message there, but now that we have more than one kind of graph I would not do that kind of thing, and just keep "V UMGrph E" separate from "F ( V EulPaths E ) P".) But I also want to make a small change to this definition to make f have domain (0..^n) instead of 1...n:

 

    df-wks $a |- Walks = ( v e. _V , e e. _V |-> { <. f , p >. |
       ( ( f e. Word dom e /\ p : ( 0 ... ( # ` f ) ) --> v )
         /\ A. k e. ( 0 ..^ ( # ` f ) ) ( e ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } ) $.

This way both f and p are "Word"s, so the word operations like concat work on them.

Also useful is the collection of walks with particular endpoints:

 

    df-wkon $a |- WalkOn = ( v e. _V , e e. _V |-> ( a e. v , b e. v |->

       { <. f , p >. |  ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) ) $.

We can write paths as walks in which all vertices are distinct except that the first and last may be equal:

 

    df-wks $a |- Paths = ( v e. _V , e e. _V |-> { <. f , p >. |
       ( f ( v Walks e ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\

         ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) } ) $.

Another way to write the condition (suitable as a second definitional theorem):

|- ( F ( V Paths E ) P <-> ( F ( V Walks E ) P /\

 A. x e. ( 0 ... ( # ` F ) ) A. y e. ( 0 ... ( # ` F ) )

   ( ( P ` x ) = ( P ` y ) -> ( x = y \/ { x , y } = { 0 , ( # ` F ) } ) ) )

The condition `' Fun ( p |` ( 1 ... n ) ) (or ( p |` ( 1 ... n ) ) : ( 1 ... n ) -1-1-> ( 1st ` g ) as you wrote it) is insufficient because this allows the possibility that the first vertex is equal to some other vertex in the middle of the path, which would allow a path in the shape of a 9, say.

Alternatively, we can base the definition on WalkOn instead:

    df-pthon $a |- PathOn = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { <. f , p >. |
       ( f ( a ( v Walks e ) b ) p /\ Fun `' ( p |` ( 1 ..^ ( # ` f ) ) ) /\ ( { a , b } i^i ( p " ( 1 ..^ ( # ` f ) ) ) ) = (/) ) } ) $.

I would not use both of these definitions (for the time being), just pick the one that most suits your purposes. The nice thing about this one is that it makes the definition of a cycle easy to state:

    df-cycl $a |- Cycles = ( v e. _V , e e. _V |->

      ran ( a e. v , p e. ( a ( v PathOn e ) a ) |-> ran ( 1st ` p ) ) ) $.

After unpacking this, it says that a cycle is defined as the set of edges of some path from a vertex to itself. Note that it is not the path itself, so that for example a cyclic permutation of the cycle corresponds to the same cycle. The length of the cycle is the size of the set.

I had difficulty finding a source for "circuit", but it can be similarly defined with "trail" in place of "path".

Trails seem not so useful for the friendship theorem, but Eulerian paths (trails) are a special case, so this is how I would write it:

    df-trlon $a |- TrailOn = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { w e. ( a ( v Walks e ) b ) | Fun `' ( 1st ` w ) } ) ) $.

These are all just suggestions, but maybe there are things in here you hadn't thought of.

Mario

[Alexander van der Vekens]

Hi Mario,
thanks again for your valuable remarks and proposals:

• I like the definition of Walks as general concept, thought about it by myself, but dropped it to "save" definitions. But your pros for it are convincing.
• I was not aware of the availablitity of ..^ which helps avoiding the ( n - 1 ) as upper limit.
• The usage of Word as basic concept also convinced me (after I looked at the definition df-word - I was a little bit puzzled before)
• I needed a collection of path/walks with particular endpoints, and created ugly constructs with my definitions. So I am happy about your proposal of WalkOn
• My definition of Paths was actually erroneous - thanks for your hint.
• I require statements about paths/circles of a certain length (2-paths, 4-cycles), therefore I included the length in my definitions. However, these definitions do not cover infinite cases. Therefore, your proposals are more general.  How exactly is the statement "p is a path of length n" formalized with your definitions?
• Although your definition of Cycles is quite pretty, I do not know yet if I need a definition allowing for a cycle to be a path. I'll see/decide when I proceed with my work.

Unfortunately, my holidays are over now, and I do not know how much time I have to proceed with Graph Theory in Metamath, especially because a lot of basic work must be done with all these new definitions...

Regards,

Alexander

[Mario Carneiro]

On Wed, Oct 4, 2017 at 6:59 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

• I require statements about paths/circles of a certain length (2-paths, 4-cycles), therefore I included the length in my definitions. However, these definitions do not cover infinite cases. Therefore, your proposals are more general.  How exactly is the statement "p is a path of length n" formalized with your definitions?

Actually, my definition doesn't really allow for the infinite case, in the sense that all paths and cycles described here are finite (although the containing graph may be infinite). There is a reasonable definition of a NN-path or a ZZ-path (where the set of vertices is ordered like NN or ZZ respectively) but for uncountable sets it's not even clear what a path means. One way to get at these kind of paths is by saying something like "a subgraph such that all finite connected subgraphs are path graphs", although you should be able to prove that such a set is always a finite path, or an NN or ZZ-path, and hence is always countable.

The length of a path <. F , P >. is ( # ` F ), so a path of length n is something like ( F ( V Paths E ) P /\ ( # ` F ) = N ).

• Although your definition of Cycles is quite pretty, I do not know yet if I need a definition allowing for a cycle to be a path. I'll see/decide when I proceed with my work.

If you need cycles in the sense of paths from a vertex to itself (in which different start points and orientation for the same cycle are distinguished), I would suggest simply ( A ( V PathsOn E ) A ) for some fixed A e. V. In a sense, this corresponds to the fact that once you want to prove something about a cycle, you want a concrete path which generates the cycle, and the ran ( ... ) definition gives you exactly that.

Mario

[David A. Wheeler]

On October 4, 2017 6:59:04 AM EDT, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

>Unfortunately, my holidays are over now, and I do not know how much
>time I
>have to proceed with Graph Theory in Metamath, especially because a lot
>of
>basic work must be done with all these new definitions...

I really like Mario's definitions. Could one of you please include those in one of your mail boxes? These definitions look very promising and I would hate for them to be lost in a stream of email.


--- David A.Wheeler

[Alexander van der Vekens]

Yes, I plan to put these definitions into my Mathbox, but I want to prove some basic theorems for them first. However, it could take a while, because I want to finish my work regarding USGraph and (basics for the) friendship theorem first. @Mario: If you want to do this, I have no objections.

[Alexander van der Vekens]

The definitions for walks, trails, paths, circuits and cycles (and some more) together with some basic theorems are available in my mathbox now, see http://us.metamath.org/mpeuni/mmtheorems283.html#mm28253s. Any comments (and additional theorems about or using these definitions) are welcome.

[David A. Wheeler]

cwlkon, ctrlon, and cpthon are all described as PLEASE PUT DESCRIPTION HERE. Can you add more explanation and maybe some hypertext links?



--- David A.Wheeler

[Alexander van der Vekens]

yes, that's not nice - I will add something meaningful on my next commit.

[Alexander van der Vekens]

Hopefully, many of you recognized already that I contributed a lot of "material" (definitions, theorems, explanations, discussions, auxiliary theorems) regarding Graph Theory to set.mm within my mathbox (see section "18.22.4  Graph theory"). After my latest contribution yesterday (which is available in the develop branch of the git repository, but not published on http://us2.metamath.org:88 yet), I think it is time now to think about moving the section "Graph Theory" out of my mathbox into the main part of set.mm.

I would propose to provide an own "Part" for it in set.mm, at least after PART 6  ELEMENTARY NUMBER THEORY, but maybe better after PART 7  BASIC STRUCTURES (there were hints in the previous discussions to make a "graph" an extensible structure with the vertices as base set and the edge function as second component. But it is still open, and I have no idea, how to add more components to such a structure in a meaningful way. Therefore, I think graphs will remain "ordered pairs" also in the future). But I also have no problems with adding the new part for Graph Theory at the very end (after PART 13  BASIC REAL AND COMPLEX FUNCTIONS).

Although my goal, the proof of the friendship theorem, is not reached yet (I am making progress, but very slowly... I'll provide more details in the correspondig discussion thread), I think the basic definitions and a lot of theorems for them are already available and stable, and could be used also by others. In a personal email, Gérard Lang encouraged me to ask for making Graph Theory an official part of set.mm.

Before performing this step, two things have to be considered:

1. The proofs of the theorems are based on about 100 auxiliary theorems belonging to classical first order logic with equality, ZF set theory and theory of real and complex numbers (Parts 1-5 of set.mm), see section "18.22.3  Auxiliary theorems for graph theory" in my mathbox. These theorems have to be moved to the main part, too, merging them into the corresponing sections, and finding a good place for them within the right section. Also renaming them my be useful in some cases.
2. The definitions and theorems about graph theory currently contained in Mario's mathbox should be moved into this new part, too. Although the definition of Undirected Multigraphs (df-umgra) and related theorems can be moved without changes, the definition of  Eulerian paths (df-eupa) must be adapted to the general definition of path (as Mario himself suggested), and the definition of vertex degree (df-vdgr) should be replaced by the definition df-vdgre which also supports infinite degrees. The affected theorems/proofs must also be adapted then (is there an easy way to do this?). Regarding df-vdgr, however, we could leave this definition in set.mm (in addition to df-vdgre) and mark it as deprecated ("New usage is discouraged"). In general, we could move the definitions and theorems of section "18.4.10  Undirected multigraphs" into the new part without changes first and perform the alignment later.

Now I want to ask everybody if there are any reasons against moving the graph theory into the main part of set.mm (excluding the section about friendship graphs - I will continue working on that within my mathbox). If there are no objections, I want to ask Norman (and the other "administrators" of set.mm) how we/I should proceed. I could make a proposal in my own git-fork which could be disussed in the pull request.

I am very keen to hear your opinion on that matter.

Best regards,

Alexander

[David A. Wheeler]

I love the idea of putting the key definitions and theorems of graph Theory into the main body. By putting things there, we reduce the risk of duplicated and inconsistent work. Whether or not they are ready I leave to Norm and Mario. Good luck on the Friendship theorem.
--- David A.Wheeler

[Norman Megill]

On Sunday, January 14, 2018 at 9:23:41 AM UTC-5, Alexander van der Vekens wrote:

Hopefully, many of you recognized already that I contributed a lot of "material" (definitions, theorems, explanations, discussions, auxiliary theorems) regarding Graph Theory to set.mm within my mathbox (see section "18.22.4  Graph theory"). After my latest contribution yesterday (which is available in the develop branch of the git repository, but not published on http://us2.metamath.org:88 yet), I think it is time now to think about moving the section "Graph Theory" out of my mathbox into the main part of set.mm.

I would propose to provide an own "Part" for it in set.mm, at least after PART 6  ELEMENTARY NUMBER THEORY, but maybe better after PART 7  BASIC STRUCTURES (there were hints in the previous discussions to make a "graph" an extensible structure with the vertices as base set and the edge function as second component. But it is still open, and I have no idea, how to add more components to such a structure in a meaningful way. Therefore, I think graphs will remain "ordered pairs" also in the future). But I also have no problems with adding the new part for Graph Theory at the very end (after PART 13  BASIC REAL AND COMPLEX FUNCTIONS).

Although my goal, the proof of the friendship theorem, is not reached yet (I am making progress, but very slowly... I'll provide more details in the correspondig discussion thread), I think the basic definitions and a lot of theorems for them are already available and stable, and could be used also by others. In a personal email, Gérard Lang encouraged me to ask for making Graph Theory an official part of set.mm.

Before performing this step, two things have to be considered:

1. The proofs of the theorems are based on about 100 auxiliary theorems belonging to classical first order logic with equality, ZF set theory and theory of real and complex numbers (Parts 1-5 of set.mm), see section "18.22.3  Auxiliary theorems for graph theory" in my mathbox. These theorems have to be moved to the main part, too, merging them into the corresponing sections, and finding a good place for them within the right section. Also renaming them my be useful in some cases.
2. The definitions and theorems about graph theory currently contained in Mario's mathbox should be moved into this new part, too. Although the definition of Undirected Multigraphs (df-umgra) and related theorems can be moved without changes, the definition of  Eulerian paths (df-eupa) must be adapted to the general definition of path (as Mario himself suggested), and the definition of vertex degree (df-vdgr) should be replaced by the definition df-vdgre which also supports infinite degrees. The affected theorems/proofs must also be adapted then (is there an easy way to do this?). Regarding df-vdgr, however, we could leave this definition in set.mm (in addition to df-vdgre) and mark it as deprecated ("New usage is discouraged"). In general, we could move the definitions and theorems of section "18.4.10  Undirected multigraphs" into the new part without changes first and perform the alignment later.

Now I want to ask everybody if there are any reasons against moving the graph theory into the main part of set.mm (excluding the section about friendship graphs - I will continue working on that within my mathbox). If there are no objections, I want to ask Norman (and the other "administrators" of set.mm) how we/I should proceed. I could make a proposal in my own git-fork which could be disussed in the pull request.

I am agreeable to this.  Go ahead and make the changes you suggest as a pull request that we can discuss.

Thanks,
Norm

[Alexander van der Vekens]

OK, I have some minor improvements/enhancements which I will submit to my Mathbox first. Afterwards, I will make a proposal for an integration of graph theory and the auxiliary theorems into the main part of set.mm.

[Alexander van der Vekens]

I just want to report that the movement of the definitions and theorems for Graph Theory into the main part of set.mm is finished. You can find them in Part 14 GRAPH THEORY, already on the official server http://us.metamath.org/mpeuni/mmtheorems.html.

By this, I want to close this discussion thread. If there are any new aspects about graph theory to be discussed, please open a new thread. However, I want to concentrate on making progress proving the friendship theorem...

Regards,
Alexander