Mathematicians sometimes worry about the Axiom of Choice (AC) and Axiom of Determinancy (AD).

Axiom of Choice: Given any collection ${\cal C}$ of nonempty sets, there is a function $f$ that, given a set $S$ in ${\cal C}$, returns a member of $S$.

Axiom of Determinacy: Let $S$ be a set of infinitely long bit strings. Alice and Bob play a game where Alice picks a 1st bit $b_1$, Bob picks a 2nd bit $b_2$, and so on, until an infinite string $x = b_1 b_2 \cdots $ is constructed. Alice wins the game if $x \in S$, Bob wins the game if $x \not \in S$. The assumption is that for every $S$, there is a winning strategy for one of the players. (For example, if $S$ consists only of the all-ones string, Bob can win in finitely many moves.)

It is known that these two axioms are inconsistent with each other. (Think about it, or go here.)

Other mathematicians pay little or no attention to the use of these axioms in a proof. They would seem to be almost irrelevant to theoretical computer science, since we believe that we work mostly with finite objects. However, because TCS defines computational decision problems to be infinite bit strings, and we measure (for example) the time complexity of an algorithm as an asymptotic function over the naturals, there is always a possibility that the usage of one of these axioms could creep into some proofs.

What is the most striking example in TCS that you know where one of these axioms are required? (Do you know any examples?)

Just to foreshadow a bit, note that a diagonalization argument (over the set of all Turing machines, say) is not an application of the Axiom of Choice. Although the language that a Turing machine defines is an infinite bit string, each Turing machine has a finite description, so we really don't require a choice function for infinitely many infinite sets here.

(I put a lot of tags because I have no idea where the examples will come from.)

  • $\begingroup$ CW ? or not ? not sure. $\endgroup$ Commented Oct 4, 2010 at 21:50
  • $\begingroup$ I'm not sure either... this is one question where I am very unsure about the "complexity" of the answer... $\endgroup$ Commented Oct 4, 2010 at 22:00
  • 5
    $\begingroup$ Other mathematicians pay little or no attention to the use of these axioms in a proof. Do mathematicians really use both axioms carelessly? If you accidentally assume both axioms you can prove anything! $\endgroup$ Commented Oct 4, 2010 at 23:07
  • 1
    $\begingroup$ Harvey Friedman's conjectue. I don't know if it also applies to theoretical computer science. $\endgroup$
    – Kaveh
    Commented Oct 5, 2010 at 0:41
  • 1
    $\begingroup$ I do not know any result in the theoretical computer science which cannot be proved in ZF but can be proved in some interesting extension of ZF. That said, my wild guess is that even such results will not probably require the full axiom of choice (AC) and that they only require some weaker version of AC such as the axiom of dependent choice (DC) or the even weaker axiom of countable choice (AC_ω). As an aside, DC (and hence AC_ω) is consistent with the axiom of determinacy. $\endgroup$ Commented Oct 5, 2010 at 1:06

7 Answers 7


Any arithmetical statement provable in ZFC is provable in ZF, and hence does not "need" the axiom of choice. By an "arithmetical" statement I mean a statement in the first-order language of arithmetic, meaning that it can be stated using only quantifiers over natural numbers ("for all natural numbers x" or "there exists a natural number x"), without quantifying over sets of natural numbers. At first glance it might seem very restrictive to forbid quantification over sets of integers; however, finite sets of integers can be "encoded" using a single integer, so it's O.K. to quantify over finite sets of integers.

Virtually any statement of interest in TCS can, with perhaps a bit of finagling, be phrased as an arithmetical statement, and so doesn't need the axiom of choice. For example, $P\ne NP$ looks at first glance like an assertion about infinite sets of integers, but can be rephrased as, "for every polynomial-time Turing machine, there exists a SAT instance that it gets wrong," which is an arithmetical statement. Thus my answer to Ryan's question is, "There aren't any that I know of."

But wait, you may say, 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. [EDIT: I made a mistake here. As Emil Jeřábek explains, the graph minor theorem—or at least the most natural statement of it in the absence of AC—is provable in ZF. But modulo this mistake, what I say below is still essentially correct.] 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.

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

The example of the chromatic number of the plane is similarly a matter of interpretation. There are various questions you can ask that turn out to be equivalent if you assume AC, but which are distinct questions if you don't assume AC. From a TCS point of view, the combinatorial heart of the question is the colorability of finite subgraphs of the plane, and the fact that you can then (if you want) use a compactness argument (this is where AC comes in) to conclude something about the chromatic number of the whole plane is amusing, but of somewhat tangential interest. So I don't think this is a really good example.

I think ultimately you may have more luck asking whether there are any TCS questions that require large cardinal axioms for their resolution (rather than AC). Work of Harvey Friedman has shown that certain finitary statements in graph theory can require large cardinal axioms (or at least the 1-consistency of such axioms). Friedman's examples so far are slightly artificial, but I wouldn't be surprised to see similar examples cropping up "naturally" in TCS within our lifetimes.

  • 9
    $\begingroup$ Proving normalization for typed lambda calculus with polymorphism requires at least 2nd-order arithmetic, and showing the same for the more generous type theories can require large cardinal axioms, albeit fairly modest ones. IIRC, Coq's normalization proof needs countably many inaccessibles, since you can use it to code Grothendieck-style universe arguments. $\endgroup$ Commented Dec 30, 2010 at 21:42
  • 3
    $\begingroup$ @Neel: Good point, though IMO these examples "cheat" because it's sort of obvious that you might need strong logical axioms to prove the consistency of a logical system. $\endgroup$ Commented Dec 30, 2010 at 22:08
  • 4
    $\begingroup$ I like this answer because it explains why the use of the axiom of choice in TCS seems extremely rare. $\endgroup$ Commented Dec 30, 2010 at 23:42
  • 11
    $\begingroup$ @Tsuyoshi: actually it is even more difficult, to find an example one needs to go above not just the arithmetical hierarchy but also above $\Pi^1_3$, since all $\Pi^1_3$ consequences of $ZFC$ are already provable in $ZF$. $\endgroup$
    – Kaveh
    Commented Jan 2, 2011 at 6:42
  • 3
    $\begingroup$ @Kaveh Long after the fact, but that's not really accurate: Shoenfield absoluteness works for $\Sigma^1_3$, not $\Pi^1_3$. For example, "Every real is constructible" is a $\Pi^1_3$ theorem of ZFC+V=L which is not provable in ZFC, let alone ZF. That said, there may be a more subtle argument applicable to AC specifically: for example, it's not hard to show that ZFC is projectively conservative over ZF+DC. Whether DC can be eliminated is something I don't know yet. $\endgroup$ Commented Dec 29, 2019 at 19:14

My understanding is that the known proof for the Robertson-Seymour theorem uses the Axiom of Choice (via Kruskal's tree theorem). This is considerably interesting from TCS viewpoint, as Robertson-Seymour theorem implies that membership testing in any given minor-closed family of graphs can be done in polynomial time. In other words, the Axiom of Choice can be used indirectly to prove that polynomial time algorithms exists for certain problems, without actually constructing those algorithms.

This might, though, not be exactly what you are looking for, as it's not clear whether AC is actually required here.

  • $\begingroup$ This is a good start, since it's not known how to prove the theorem otherwise. $\endgroup$ Commented Oct 5, 2010 at 18:07
  • 7
    $\begingroup$ As mentioned on the Wikipedia page, the paper by Friedman, Robertson, and Seymour on the metamathematics of the graph minor theorem shows that the graph minor theorem implies (a form of) Kruskal's tree theorem over the base theory RCA_0, so this establishes that Kruskal's tree theorem is required for the graph minor theorem in a strong sense. However, whether this means that the axiom of choice is required for the graph minor theorem is a slightly tricky question. It depends in a subtle way on how you choose to state the graph minor theorem. See my answer for more details. $\endgroup$ Commented Jan 3, 2011 at 18:48
  • 10
    $\begingroup$ Emil Jeřábek has shown on MathOverflow how to prove the Robertson-Seymour theorem without the axiom of choice. This was surprising to me because I was also under the impression that the Robertson-Seymour for unlabeled graphs required AC, but that was evidently a misimpression. $\endgroup$ Commented Apr 30, 2013 at 20:02
  • $\begingroup$ So the accepted answer is actually false? $\endgroup$ Commented Oct 28, 2017 at 17:14
  • $\begingroup$ @AndrejBauer : If you're referring to my answer, you're right that what I said about Robertson-Seymour is wrong. I tried to edit my answer just now but couldn't. Maybe I don't have enough reputation to edit such an old post. $\endgroup$ Commented Nov 1, 2017 at 2:55

This relates to the answer given by Janne Korhonen.

There was a stream of results in the 80's and 90's that tried to characterize the axiom systems (in other words, the arithmetic theory) needed to prove extensions of Kruskal Tree Theorem (KTT; the original KTT is from 1960). In particular, Harvey Friedman proved several results following this line (see S. G. Simpson. Nonprovability of certain combinatorial properties of finite trees. In L. A. Harrington et al., editor, Harvey Friedman's Research on Foundations of Mathematics. Elsevier, North-Holland, 1985). These results showed that (certain extensions of) KTT must use "strong" Comprehension Axioms (i.e., axioms saying that certain sets of high logical complexity exist). I don't know precisely about the provability of extensions of KTT in ZF (without the axiom of choice).

In parallel to this stream of results, there was an attempt to connect it to ("Theory B") TCS via rewrite systems. The idea is to construct rewriting systems (think of it as a sort of functional programming, or lambda-calculus programs) for which their termination depend on certain (extensions) of KTT (the original connection between KTT and rewrite systems termination was proved by N. Dershowitz (1982)). This implies that to show that certain programs terminate one needs strong axioms (since extensions of KTT need such axioms). For this type of results, see e.g. A. Weiermann, Complexity bounds for some finite forms of Kruskal's theorem, Journal of Symbolic Computation 18 (1994), 463-488.


The Hadwiger-Nelson Problem is tangentially related and asks for the minimum number of colors required to color the plane ${\mathbb R}^2$ where points at distance exactly 1 are given different colors. There exist finite subgraphs which require four colors and there is a constructible seven-coloring by tiling the plane with hexagons.

In Shelah and Soifer, "Axiom of choice and chromatic number of the plane," it is shown that if all finite subgraphs of the plane are four-chromatic, then

  • If you assume the axiom of choice, then the plane is four-chromatic.
  • If you assume the principle of dependent choices and that all sets are Lebesgue measurable, then the plane is five-, six-, or seven-chromatic.
  • $\begingroup$ Isn't this more math-oriented than TCS-oriented? $\endgroup$ Commented Oct 5, 2010 at 2:39
  • $\begingroup$ That's why I said "tangentially" related. Coloring problems are TCS-oriented, just not this specific one. $\endgroup$ Commented Oct 5, 2010 at 3:33
  • 4
    $\begingroup$ ahem. This is about coloring geometric objects. Geometers around the world are now preparing $\alpha$-thin slivers to send in your direction :) $\endgroup$ Commented Oct 5, 2010 at 4:18
  • $\begingroup$ Excellent. Validation. $\endgroup$ Commented Oct 5, 2010 at 8:44

Some of the work of Olivier Finkel seems related to the question---though not necessarily explicitly about the Axiom of Choice itself---and in line with Timothy Chow's answer. For instance, quoting the abstract of Incompleteness Theorems, Large Cardinals, and Automata over Finite Words, TAMC 2017,

one can construct various kinds of automata over finite words for which some elementary properties are actually independent from strong set theories like $T_n := ZFC + \text{``There exist (at least) $n$ inaccessible cardinals''}$, for integers $n \geq 0$.

[This is not a direct answer to your question, yet it might be suggestive and/or informative for some people.]

William Gasarch's P vs. NP Poll gives some statistics on "how P vs. NP will be resolved":

  1. 61 thought P≠NP.
  2. 9 thought P=NP.
  3. 4 thought that it is independent. While no particular axiom system was mentioned, I assume they think it is independent of ZFC.
  4. 3 just stated that it is NOT independent of Primitive Recursive Arithmetic.
  5. 1 said it would depend on the model.
  6. 22 offered no opinion.

Wikipedia has an interesting take on independence:

...These barriers have also led some computer scientists to suggest that the P versus NP problem may be independent of standard axiom systems like ZFC (cannot be proved or disproved within them). The interpretation of an independence result could be that either no polynomial-time algorithm exists for any NP-complete problem, and such a proof cannot be constructed in (e.g.) ZFC, or that polynomial-time algorithms for NP-complete problems may exist, but it's impossible to prove in ZFC that such algorithms are correct [1]. However, if it can be shown, using techniques of the sort that are currently known to be applicable, that the problem cannot be decided even with much weaker assumptions extending the Peano axioms (PA) for integer arithmetic, then there would necessarily exist nearly-polynomial-time algorithms for every problem in NP [2]. Therefore, if one believes (as most complexity theorists do) that not all problems in NP have efficient algorithms, it would follow that proofs of independence using those techniques cannot be possible. Additionally, this result implies that proving independence from PA or ZFC using currently known techniques is no easier than proving the existence of efficient algorithms for all problems in NP.


My impression reading this question is that no suitable example of a problem that requires more than just PA (let alone ZF) has been given, and the excellent answer by Timothy Chow explains why it's so hard to find examples. However, there are some examples of TCS extending beyond the realm of arithmetic, so I thought I would give a theorem that requires strictly more than $ZF$. Although it doesn’t require the full axiom of choice, it does require a weaker version.

The De Bruijin-Erdos Theorem in graph theory states that the chromatic number of a graph, $G$, is the sup of $\chi(H)$ as $H$ ranges over all finite subgraphs of $G$. Notice that the conclusion is trivially satisfied for finite $G$, so this is an interesting statement about infinite graphs. This theorem has many different proofs, but my favorite is to evoke Tychonov's Theorem.

As mentioned in the Wikipedia article I linked to, this theorem really and truly requires more than $ZF$, however it doesn't go as far as requiring the "full axiom of choice." There's a horribly unreadable proof of this on the Wikipedia page, but basically the theorem falls in the Solovay Model due to a clever constructions involving measure theory.

  • $\begingroup$ Nice example. I think Timothy Chow did address this kind of example in the paragraph about the chromatic number of the plane. $\endgroup$ Commented Oct 28, 2017 at 20:57
  • $\begingroup$ @SashoNikolov The colorability of graphs is, in my mind, clearly a TCS Problem even when the graphs are infinite. The Hadwiger-Nelson Problem is much less obviously within the realm of TCS, as commenters pointed out and the OP of that answer agreed. In contrast, I don’t think there’s anyone who would look at this theorem and go “that’s not really a CS problem” $\endgroup$ Commented Oct 28, 2017 at 21:24
  • $\begingroup$ I don't see the distinction at all: Hadwiger-Nelson is about coloring an infinite geometric graph too. In any case, I actually like and upvoted both examples and I think it's pointless to try to draw too fine a distinction between TCS and other areas of Math. $\endgroup$ Commented Oct 28, 2017 at 22:59

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.