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:

- $C$ is known to be a theorem of ZFC,
- the Graph Minor Theorem is a theorem of ZF+$C$, and
- 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 inﬁnite family of ﬁnite 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.)