In previous posts about graph minors, we reviewed the definitions of graph minors and topological minors, then looked at a relationship between the two; and explored whether there was a relationship between the computational hardness of a set of forbidden subgraphs and the graph class defined as all graphs that avoid the set of forbidden subgraphs. Both of those questions are fundamentally related to the Graph Minor Theorem of Robertson and Seymour. Today, I’d like to take a step back and look big-picture at the Graph Minor Theorem, and its relationship to computer science, by featuring an answer Timothy Chow gave to a question Ryan Williams asked about the role of the Axiom of Choice in TCS.

Ryan’s question, which he asked in October 2010, was, “What interesting theorems in TCS rely on the Axiom of Choice (or, alternatively the Axiom of Determinacy)?” The Axiom of Choice, of course, is a (sometimes controversial) axiom extending Zermelo-Fraenkel set theory, and at this point is generally accepted as part of the foundations of mathematics. Intuitively, the Axiom of Choice says that anytime you have a mathematical construction in which there is a set of nonempty bins, then it is legal to produce a set that contains exactly one item from each bin. While this might seem “obviously true,” once this intuition is applied to infinitely-many bins, there are nonconstructive and perhaps counter intuitive consequences. So it is natural to wonder, in the world of TCS where the sets of bins we encounter are unlikely to be “pathologically infinite,” whether we really need the Axiom of Choice to prove anything. (I won’t discuss the Axiom of Determinacy, except to say that it is consistent with the Zermelo-Fraenkel axioms, but inconsistent with the Axiom of Choice, and set theorists sometimes put it forth as a “better” axiom, but it has not been widely accepted by mathematicians outside of logic.)

Janne Korhonen answered Ryan’s question by noting that the proof of the Graph Minor Theorem fundamentally uses Kruskal’s Tree Theorem, which in turn uses the Axiom of Choice. A fine answer, and one might think that was the end of the story — but one would be wrong, as Timothy Chow demonstrated in a followup answer which I will now quote from.

What about arithmetical statements whose proof requires something like Koenig’s lemma or Kruskal’s tree theorem? Don’t these require a weak form of the axiom of choice? The answer is that it depends on exactly how you state the result in question. For example, if you state the graph minor theorem in the form, “given any infinite set of unlabeled graphs, there must exist two of them such that one is a minor of the other,” then some amount of choice is needed to march through your infinite set of data, picking out vertices, subgraphs, etc. However, if instead you write down a particular encoding by natural numbers of the minor relation on labeled finite graphs, and phrase the graph minor theorem as a statement about this particular partial order, then the statement becomes arithmetical and doesn’t require AC in the proof.

So the question comes down to, “What do we really mean in theoretical computer science when we talk about a mathematical proof of an infinitary statement?” To quote from Chow’s answer again:

Most people feel that the “combinatorial essence” of the graph minor theorem is already captured by the version that fixes a particular encoding, and that the need to invoke AC to label everything, in the event that you’re presented with the general set-theoretic version of the problem, is sort of an irrelevant artifact of a decision to use set theory rather than arithmetic as one’s logical foundation. If you feel the same way, then the graph minor theorem doesn’t require AC. (See also this post by Ali Enayat to the Foundations of Mathematics mailing list, written in response to a similar question that I once had.)

So, in the final analysis, at least in Chow’s opinion, there appears to be no example of a TCS theorem that requires the Axiom of Choice to prove. His final suggestion to Ryan is that it may be more fruitful to ask whether there are TCS statements that require large cardinal axioms to prove, instead of the Axiom of Choice. Harvey Friedman has apparently demonstrated some artificial examples of finitary graph theory statements that require the consistency of large cardinals to prove. So if artificial examples exist already, perhaps natural examples are around the corner.

Filed under Answer of the Week

Tagged: axiom of choice, graph minor, graph theory, reverse mathematics

That is undoubtedly a very good question and a very good answer. However, because this was posted as a blog (and also because it was filed under “Answer of the Week”), I expected that something new happened to the question, and I have to say that I was disappointed by the lack of new progress. There is nothing wrong with reviewing old questions and answers, but I would prefer if such reviews are clearly marked as such.

Thanks for the feedback, Tsuyoshi. I will be clearer about the dates in future posts. As a practical matter, it seems unavoidable that we will feature more “old” questions than “new” questions, because we feature at most one question a week, and the site generates more than one great answer per week. So we will never “catch up.” Also, personally, I am interested in publicizing some of the great answers and discussions from the beta period of the site, which you know well, but most people following, eg, the TOC Aggregator, do not. Some of these posts will just be “refreshers” for the more dedicated users of the site.

Aaron, thanks for the reply. I understand the intent. Maybe calling it “answer of the week” might be a little misleading. Something like “digging the treasure trove” (not sure if this is correct English) seems more accurate for this kind of posts. I should have said in my comment that I like both this post and the general idea of publicizing great questions and answers which were posted a while ago. Keep up the good work.

The need (if indeed it is necessary) to use full choice is almost certainly a side effect of the application of the theorem to uncountable graphs. If you want the theorem for merely countable graphs you probably can get away with countable choice (which is entailed by both choice and determinacy).

Also note that definable sets all admit choice (if I is definable, the function going from i \in I to S_i is definable then there is a definable choice function for the collection S_i). This follows from the fact that L (the definable sets) is a model of ZFC.

Note that it is DEFINABILITY not the fixing of some means of coding vertices/minors by natural numbers that does the work. It’s not enough to code up your infinite graphs using a nice coding function since some relations on vertexes are simply not possible to code arithmetically. Similar point applies for definable.

Of course any graph which can be specified in the language of arithmetic is fine.

Quick proof: Let G be the graph containing vertexes v_{-1},v_0…v_n… (countably infinite) and for i > 0 v_i has edges to v_0…v_{i-1}. Also v_i has an edge to v_{-1} iff i is in Kleene’s O. Now any reasonable means of coding this graph as a set yields a representation for the graph that’s non-arithmetic since otherwise we could arithmetically recover v_{-1} (only node with infinitely many edges) and each v_i and then check if i \in O which would make O arithmetic. Contradiction. Same reasoning to code in a graph which has no coded representation in L.

(sane here means the existence of edges between two nodes is arithmetic in the coded representation)

To be clear the claim that for a graph with some particular fixed arithmetic graph minor relation (whether v1…vn is minor of w1…wm is an arithmetic property) is provable in ZF since there will always be an arithmetic graph exhibiting that minor relation. This is probably what Chow was saying, rather than my earlier interpretation which took him to just be requiring that you code up the graphs/minor relation using some nice primitive recursive system.

However, this is a bit of a cheat since that has the effect of bounding the total height of the minor relation to some fixed computable ordinal. As we know claims that go all the way up the computable ordinals can become crazily more complicated that any of the bounded versions, e.g., Kleene O is \Pi^1_1 complete while any initial segment is r.e. However, even though the claim that the minor theorem holds for all arithmetic graphs is not itself arithmetic Chow is right that this will still be provable from ZF.

For all my quibling ultimately the stronger closure conditions for constructable sets mean that the minor theorem restricted to those graphs that can be specified by use of the language of set theory is provable in ZF. So Chow is ultimately right that the TCS aspect can ignore choice.