I originally intended this to be a comment reply to Gary, but I started to feel the need to include diagrams and such, and so now it’s its own post. Gary suffers from this tragic medical condition (since birth) in which takes every concept he encounters, and tries to apply graph theory to it. He has shared with me, in confidence, his intention to create a separate internet in which he can raise his future child to be free of non-graph distractions. I warned him of the mocking his child will receive from his peers when he realizes that Facebook isn’t actually list of graphs along with relations showing which graphs are “friends” with other graphs (visit Gary’s Facebook prototype before all the graphs mark their profiles as “private”), or that YouTube isn’t just 4 animated GIFs that are somehow graph related, but Gary dismisses my parenting advice as I have yet to successfully raise a child (poor, poor Firebat…)

In this particular situation, though, Gary’s gross mental handicap has proven useful, as one can actually gain significant insight in visualizing formal-proof-systems as directed graphs which may contain cycles. Gary’s first concern is notational. He writes:

One problem with using a simple directed graph is that if there are two edges directed toward one statement, it isn’t clear if this is an “AND” or an “OR” relationship. So we’d generally need something more helpful.

This problem doesn’t seem that difficult to overcome: An edge between two nodes should always indicate implication (so “A -> B” means A implies B, and we can represent equivalence by having a pair of symmetric edges), and so two edges pointing to the same node would represent an “OR” relationship.

In order to represent an “AND” relationship, one would simply need to introduce the concept of nodes containing other nodes: If a supernode “A” contains child nodes “B” and “C”, this indicates that super node A is equivalent to “B and C”. So given a system like “A implies C, B implies C, A and B implies D”, you’d end up with a graph that looks like:

The value in restating logical systems as directed graphs is that it reduces “provability” to “reachability”: A statement S is provable from axioms A1, A2, …, An if and only if there is a path from at least one of the axiom to S. A super node is reachable if and only if all of its direct child nodes are reachable.

Gary then points out that circular reasoning represents itself as cycles in the graph, and Gary goes on to categorize these cycles as being “interesting, superfluous, or misleading”. First of all, I’m not sure Gary and I are interpreting the graphs the same way. I get the impression that Gary sees the graph-as-a-whole as a specific proof, but to me, the graph-as-a-whole represents a logical system. As far as I know, the only logical system most people (mathematicians, logicians, etc.) are interested in is predicate-logic, so in practice, there is only one graph that is interesting, but in principle we could have many such graphs. In contrast, a “proof” is simply one specific connected path in the graph.

A cycle thus simply shows that all the statements in the cycle are equivalent to each other (and so all cycles are actually cliques). This is “useful information” in the sense that if you can prove any one statement (i.e. if there’s a path from axiom to any node in the clique), then you can prove all of them.