The main Robertson-Seymour Theorem states that finite graphs form a well-quasi-ordering under the graph minor relation. In other words, in every infinite set of finite graphs, there exist two graphs $G$ and $H$ such that $G$ is a minor of $H$.

My question is:

What is a weakest consequence $C$ of the Axiom of Choice that is sufficient in ZF to imply the Graph Minor Theorem?

A little more precisely, what is a sentence $C$ of an appropriate logic (such as a form of second-order logic) such that:

  1. $C$ is known to be a theorem of ZFC,
  2. the Graph Minor Theorem is a theorem of ZF+$C$, and
  3. there is no known sentence $D$ that is a theorem of ZF+$C$ with the Graph Minor Theorem being a theorem of ZF+$D$?

Ideally $C$ should be one of the already studied consequences of AC, and the quantification over "known" $D$ can also be restricted to such consequences.


Another way to make my question precise would be to say that it is about the "first form" of the Graph Minor Theorem, rather than the "second form", in analogy with Ali Enayat writing about König's Lemma. Forster and Truss showed that König's Lemma is equivalent to a rather weak choice principle:

Every countably infinite family of finite non-empty sets has a choice function.

and I am asking which choice principle is a weakest one that is known to be sufficient to prove the Graph Minor Theorem: some stronger form of choice seems to be needed than for König's Lemma.

  • T. E. Forster and J. K. Truss, Ramsey's theorem and König's Lemma, Archive for Mathematical Logic 46, 2007, 37–42. doi:10.1007/s00153-006-0025-z

I am waiting for the following possibly relevant paper, although hopefully something has been written about this in the intervening 26 years:

  • H. Friedman, N. Robertson, and P. D. Seymour, The metamathematics of the graph minor theorem, in (S. G. Simpson, ed.) Logic and Combinatorics, Contemporary Mathematics 65, AMS, 1987, 229–261.

I am also aware of Timothy Chow's answer to a question of Ryan Williams which suggests rephrasing the Graph Minor Theorem as a statement of arithmetic (which therefore can be proved in ZF, with no notion of choice required). However, I find it unsatisfactory to finesse away choice by only allowing graphs over vertices from $\mathbb{N}$, and encoding the graph minor relation as a particular relation over the natural numbers, about which we then ask the whether a particular arithmetical sentence is true. To my mind, the key difficulty seems to be precisely that if we don't have canonization, then these questions require additional machinery. (In fact, I would naively be tempted to use $C$ and $D$ as measures of just what we gain from canonization, in some sense.)

Harvey Friedman recently commented:

wqo statements, which are Pi-1-1. E.g., Kruskal's Theorem, graph minor theorem, Hilbert's basis theorem (appropriately formalized), etcetera. These are equivalent over RCA_0 to the well orderedness of familiar ordinal notations (in the case of GMT, the exact ordinal has not been determined, but has been determined for the important restriction to graphs of finite tree width).

Hence, I expect that we currently do not know $C$ such that ZF+$C$ can prove GMT, while ZF+GMT can also prove $C$. But surely something is known about how "strong" a notion is needed? For instance, which choice principle is Friedman referring to above in the bounded tree-width case? This would suggest a candidate for $D$.

(See also a related question by Joe Shipman.)

  • $\begingroup$ The wiki article you link to says the theorem is about all (not just finite) graphs. $\hspace{1.7 in}$ By Shoenfield Absoluteness, ZF on its own proves the version for finite graphs. $\:$ $\endgroup$
    – user5810
    Apr 29, 2013 at 19:33
  • $\begingroup$ The $\Pi^1_1$ formulation of the GMT in Friedman’s comment is the one with integer vertices. These are the only finite graphs you can talk about in arithmetical theories like $\mathrm{RCA}_0$. $\endgroup$ Apr 29, 2013 at 19:42
  • 1
    $\begingroup$ @Ricky: You are misreading the article, they just omit the adjective finite at some places as being understood (but it is explicitly given e.g. in en.wikipedia.org/wiki/…). The theorem is false for infinite graphs (it is quite easy to construct an infinite decreasing chain). $\endgroup$ Apr 29, 2013 at 19:56
  • 1
    $\begingroup$ Also, the proper definition of wqo in the absense of choice is that every set has a finite basis. The reformulation of this in terms of countable sequences already requires some choice. $\endgroup$ Apr 29, 2013 at 20:00
  • $\begingroup$ I take back the “quite easy” part, but anyway, the theorem is false for infinite graphs: people.math.gatech.edu/~thomas/PAP/cntrexwagner.pdf $\endgroup$ Apr 29, 2013 at 20:17

1 Answer 1


As far as I can see, the Robertson–Seymour theorem is provable in plain ZF.

First, the restricted version of the theorem for graphs whose vertices are natural numbers can be written as a $\Pi^1_1$ second-order arithmetical sentence, hence its provability in ZF follows from its provability in ZFC by the Schoenfield absoluteness theorem. (Note that the set of all such finite graphs is countable, hence well-orderable, thus all the common definitions of wqo coincide in this case without the need for any choice.)

Second, ZF proves that the general case is equivalent to the restricted case. I will take the definition of wqo requiring that every subset has a finite basis: this is the most natural formulation in set theory without choice, and it implies in ZF both the property given in the original question, and the property that for every sequence $\{x_i:i\in\mathbb N\}$, there exist $i< j$ with $x_i\le x_j$.

So, assume that $X$ is a set of finite graphs. Let $X'$ be the set of all graphs with integer vertices isomorphic to some graph in $X$. By the restricted version of the theorem, we can find a finite basis $B'\subseteq X'$, say $B'=\{G_i':i< n\}$. In ZF, we have choice for finite families, hence we can find $B:=\{G_i:i< n\}\subseteq X$ such that $G_i\simeq G_i'$ for each $i< n$. Then $B$ is a finite basis for $X$: if $G\in X$, there exists $G'\in X'$ isomorphic to $G$ (as the vertex set of $G$ is finite, it is in bijection with some $\{0,\dots,m-1\}\subseteq\mathbb N$, and we can lift the graph along this bijection). Since $B'$ is a basis of $X'$, some $G_i'\in B'$ is a minor of $G'$, hence $G_i\in B$ is a minor of $G$.

  • 2
    $\begingroup$ I'm confused about something here. R-S includes Kruskal's tree theorem, which as usually formulated requires a weak form of AC, doesn't it? How are you getting around this? It must be some subtlety in the definition of wqo that you're using? $\endgroup$ Apr 30, 2013 at 15:00
  • 1
    $\begingroup$ Can you state exactly which form of Kruskal’s theorem you have in mind? In particular, the formulation on Wikipedia allows labelled trees, where the labels may come from an arbitrary wqo. I don’t see how to reduce this to R–S. I can well imagine that this might require some choice, and in particular the argument I’m using does not work as there is no obvious way how to handle the labels, but this does not seem to contradict anything I say about R–S. $\endgroup$ Apr 30, 2013 at 15:43
  • $\begingroup$ Emil, I think Timothy was just trying to say that (some form of) Kruskal's Tree Theorem is a special case of (some form of) Graph Minor Theorem, yet KTT usually does seem to need some form of choice. $\endgroup$ Apr 30, 2013 at 15:53
  • 2
    $\begingroup$ Yes, I claim that Kruskal’s theorem for unlabelled finite trees is provable without AC. More generally, the same kind of argument should apply to Kruskal’s theorem for finite trees with labels coming from a countable wqo. $\endgroup$ Apr 30, 2013 at 17:51
  • 1
    $\begingroup$ Nash-Williams's proof probably does use AC. Since ZFC is conservative over ZF for $\Pi^1_1$ statements, this does no harm and the result is still provable without AC. The key is that if $r$ codes a counterexample in $V$, then that must be a counterexample in $L[r]$ too, but AC is true in $L[r]$ so the Nash-Williams proof works in there. Furthermore, in this analysis, the definition of wqo being used is immaterial. $\endgroup$ Apr 30, 2013 at 19:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.