Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

Question

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

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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.

Answer 5

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

Answer 6

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

Answer 7

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.