Weakest choice principle required for Robertson-Seymour Graph Minor Theorem?

Question

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.

---

Discussion

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.)

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$.