<p>My understanding is that the known proof for the <a href="http://en.wikipedia.org/wiki/Robertson-Seymour_theorem">Robertson-Seymour theorem</a> 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 <em>exists</em> for certain problems, without actually constructing those algorithms.</p>

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

CC BY-SA 3.0
2013-04-30T20:02:16.003Z
Emil Jeřábek has shown on [MathOverflow](http://mathoverflow.net/questions/129142/weakest-choice-principle-required-for-robertson-seymour-graph-minor-theorem) 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.
Timothy Chow
CC BY-SA 3.0
2017-10-28T17:14:49.053Z
So the accepted answer is actually false?
Andrej Bauer
CC BY-SA 3.0
2017-11-01T02:55:56.483Z
@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.
Timothy Chow
CC BY-SA 3.0
2017-11-01T07:38:58.040Z
That’s ali right. It’s just that people might come along and not read the comments, and will take away the “accepted truth”.
Andrej Bauer
CC BY-SA 2.5
2010-10-05T18:07:14.497Z
This is a good start, since it's not known how to prove the theorem otherwise.
Ryan Williams
CC BY-SA 2.5
2011-01-03T18:48:54.437Z
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.
Timothy Chow
CC BY-SA 2.5
2010-10-05T08:26:06.653Z
2010-10-05T08:26:06.653Z
Janne H. Korhonen
<p>This relates to the answer given by Janne Korhonen.</p>

<p>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. <em>Nonprovability of certain combinatorial properties of finite trees</em>. 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). </p>

<p>In parallel to this stream of results, there was an attempt to connect it to ("Theory B") TCS via <em>rewrite systems</em>. The idea is to construct rewriting systems (think of it as a sort of functional programming, or lambda-calculus programs) for which their <em>termination</em> 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, <em>Complexity bounds for some finite forms of Kruskal's theorem</em>, Journal of Symbolic Computation 18 (1994), 463-488. </p>

CC BY-SA 2.5
2010-10-05T10:25:19.887Z
2010-10-05T10:25:19.887Z
Iddo Tzameret
<p>The <a href="http://en.wikipedia.org/wiki/Hadwiger%E2%80%93Nelson_problem">Hadwiger-Nelson Problem</a> 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.</p>

<p>In <a href="http://www.sciencedirect.com/science?_ob=ArticleURL&amp;_udi=B6WHS-48YVT67-3&amp;_user=10&amp;_coverDate=08/31/2003&amp;_rdoc=1&amp;_fmt=high&amp;_orig=search&amp;_origin=search&amp;_sort=d&amp;_docanchor=&amp;view=c&amp;_acct=C000050221&amp;_version=1&amp;_urlVersion=0&amp;_userid=10&amp;md5=a7237ebe7f1cefd6a2fb5ac8f3f24ef0&amp;searchtype=af">Shelah and Soifer, "Axiom of choice and chromatic number of the plane,"</a> it is shown that if all finite subgraphs of the plane are four-chromatic, then</p>

<ul>
<li>If you assume the axiom of choice, then the plane is four-chromatic.</li>
<li>If you assume the principle of dependent choices and that all sets are Lebesgue measurable, then the plane is five-, six-, or seven-chromatic.</li>
</ul>

CC BY-SA 2.5
2010-10-05T02:39:30.663Z
Isn't this more math-oriented than TCS-oriented?
Sadeq Dousti
CC BY-SA 2.5
2010-10-05T03:33:15.097Z
That's why I said "tangentially" related.  Coloring problems are TCS-oriented, just not this specific one.
Derrick Stolee
CC BY-SA 2.5
2010-10-05T04:18:37.277Z
ahem. This is about coloring geometric objects. Geometers around the world are now preparing $\alpha$-thin slivers to send in your direction :)
Suresh Venkat
CC BY-SA 2.5
2010-10-05T08:44:31.907Z
Excellent. Validation.
Derrick Stolee
CC BY-SA 2.5
2010-10-05T01:59:15.017Z
2010-10-05T01:59:15.017Z
Derrick Stolee
<p>Some of the work of <a href="http://www.logique.jussieu.fr/~finkel/" rel="noreferrer">Olivier Finkel</a> 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 <a href="https://hal.archives-ouvertes.fr/hal-01588572" rel="noreferrer">Incompleteness Theorems, Large Cardinals, and Automata over Finite Words</a>, <em>TAMC 2017</em>, </p>

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

CC BY-SA 3.0
2017-10-27T20:45:14.577Z
2017-10-28T12:42:07.900Z
2017-10-28T12:42:07.900Z
Sylvain
<p>[This is not a direct answer to your question, yet it might be suggestive and/or informative for some people.]</p>

<p>William Gasarch's <a href="http://www.cs.umd.edu/~gasarch/papers/poll.pdf" rel="nofollow">P vs. NP Poll</a> gives some statistics on "how P vs. NP will be resolved":</p>

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

<p><a href="http://en.wikipedia.org/wiki/P_versus_NP_problem" rel="nofollow">Wikipedia</a> has an interesting take on independence:</p>

<p>...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 [<a href="http://www.scottaaronson.com/papers/pnp.pdf" rel="nofollow">1</a>]. 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 [<a href="http://www.cs.technion.ac.il/~shai/ph.ps.gz" rel="nofollow">2</a>]. 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.</p>

CC BY-SA 3.0
2011-09-09T20:17:57.120Z
Note that Bill is taking another poll, which is open for another month or so: http://blog.computationalcomplexity.org/2011/06/i-am-conducing-new-poll-on-p-vs-np.html
Charles
CC BY-SA 3.0
2011-09-10T02:32:03.473Z
@Charles: Thanks for the update. I'm really eager to know the community's most recent consensus.
Sadeq Dousti
CC BY-SA 2.5
2010-10-04T23:45:29.620Z
Another interesting fact (also from Wikipedia) is that, the main (only?) general technique for proving independence in ZFC, forcing, cannot prove that P=?NP is independent of ZFC. This is a corollary of Shoenfield's absoluteness theorem.
Travis Service
CC BY-SA 2.5
2010-10-05T02:36:02.227Z
Thanks Travis. Here's the pointer: http://en.wikipedia.org/wiki/Absoluteness. See also http://www.cs.uwaterloo.ca/~shai/P%20vs%20NP-2.ppt and http://blog.computationalcomplexity.org/2009/09/is-pnp-ind-of-zfc-respectable-viewpoint.html.
Sadeq Dousti
CC BY-SA 2.5
2010-10-04T22:51:21.133Z
2010-10-04T22:51:21.133Z
Sadeq Dousti
<p>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.</p>

<p>The <a href="https://en.wikipedia.org/wiki/De_Bruijn%E2%80%93Erd%C5%91s_theorem_(graph_theory)" rel="nofollow noreferrer">De Bruijin-Erdos Theorem</a> 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.</p>

<p>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 <a href="https://en.wikipedia.org/wiki/Solovay_model" rel="nofollow noreferrer">Solovay Model</a> due to a clever constructions involving measure theory.</p>

CC BY-SA 3.0
2017-10-28T20:57:39.420Z
Nice example. I think Timothy Chow did address this kind of example in the paragraph about the chromatic number of the plane.
Sasho Nikolov
CC BY-SA 3.0
2017-10-28T21:24:00.680Z
@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”
Stella Biderman
CC BY-SA 3.0
2017-10-28T22:59:29.147Z
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.
Sasho Nikolov
CC BY-SA 3.0
2017-10-27T18:28:02.057Z
2017-10-28T15:20:15.173Z
2017-10-28T15:20:15.173Z
Stella Biderman
<p>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 <i>sets</i> of natural numbers.  At first glance it might seem very restrictive to forbid quantification over sets of integers; however, <i>finite</i> sets of integers can be "encoded" using a single integer, so it's O.K. to quantify over finite sets of integers.</p>

<p>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, <span class="math-container">$P\ne NP$</span> 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."</p>

<p>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. <b>[EDIT:</b> I made a mistake here. As <a href="https://mathoverflow.net/a/129211/3106">Emil Jeřábek explains</a>, the  graph minor theorem&mdash;or at least the most natural statement of it in the absence of AC&mdash;is provable in ZF.  But modulo this mistake, what I say below is still essentially correct.<b>]</b> 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.</p>

<p>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 <a href="http://cs.nyu.edu/pipermail/fom/2008-September/013050.html" rel="noreferrer">this post by Ali Enayat</a> to the Foundations of Mathematics mailing list, written in response to a similar question that I once had.)</p>

<p>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 <i>whole</i> plane is amusing, but of somewhat tangential interest.  So I don't think this is a really good example.</p>

<p>I think ultimately you may have more luck asking whether there are any TCS questions that require <i>large cardinal axioms</i> 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.</p>

CC BY-SA 3.0
2011-09-01T02:03:43.450Z
This answer is [featured](http://cstheory.blogoverflow.com/2011/09/what-does-it-really-mean-to-prove-the-graph-minor-theorem/) on the community blog.
Aaron Sterling
CC BY-SA 4.0
2019-12-29T19:14:29.783Z
@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.](https://math.stackexchange.com/questions/3491349/projective-conservativity-of-choice)
Noah Schweber
CC BY-SA 2.5
2010-12-30T21:42:46.383Z
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.
Neel Krishnaswami
CC BY-SA 2.5
2010-12-30T22:08:24.957Z
@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.
Timothy Chow
CC BY-SA 2.5
2010-12-30T23:42:23.783Z
I like this answer because it explains why the use of the axiom of choice in TCS seems extremely rare.
Tsuyoshi Ito
CC BY-SA 2.5
2011-01-02T06:42:50.467Z
@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$](http://en.wikipedia.org/wiki/Absoluteness#Shoenfield.27s_absoluteness_theorem).
Kaveh
CC BY-SA 4.0
2010-12-30T20:10:40.070Z
2019-02-20T03:43:23.077Z
2019-02-20T03:43:23.077Z
Timothy Chow
<p>Mathematicians sometimes worry about the Axiom of Choice (AC) and Axiom of Determinancy (AD). </p>

<p><strong>Axiom of Choice</strong>: 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$.</p>

<p><strong>Axiom of Determinacy</strong>: 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 <em>every</em> $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.)</p>

<p>It is known that these two axioms are inconsistent with each other. (Think about it, or <a href="http://en.wikipedia.org/wiki/Axiom_of_determinacy">go here</a>.)</p>

<p>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. </p>

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

<p>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.</p>

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

CC BY-SA 2.5
2010-10-04T21:50:08.507Z
CW ? or not ? not sure.
Suresh Venkat
CC BY-SA 2.5
2010-10-04T22:00:31.330Z
I'm not sure either... this is one question where I am very unsure about the "complexity" of the answer...
Ryan Williams
CC BY-SA 2.5
2010-10-04T22:12:20.947Z
Good idea. I'll add it
Ryan Williams
CC BY-SA 2.5
2010-10-04T22:58:59.933Z
Interesting. Do you know a proof that those axioms are inconsistent that's more elementary (no transfinite induction)?
Warren Schudy
CC BY-SA 2.5
2010-10-04T23:07:34.550Z
*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!
Warren Schudy
CC BY-SA 2.5
2010-10-05T00:04:19.310Z
My impression is that the axiom of determinacy does not come up too often for most mathematicians.
Ryan Williams
CC BY-SA 2.5
2010-10-05T00:19:25.620Z
Here's a different proof of inconsistency: http://www.brics.dk/RS/94/24/BRICS-RS-94-24.pdf . It unfortunately still uses transfinite induction (indirectly in the proof of Zorn's Lemma).
Warren Schudy
CC BY-SA 2.5
2010-10-05T00:41:22.397Z
[Harvey Friedman's conjectue](http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture). I don't know if it also applies to theoretical computer science.
Kaveh
CC BY-SA 2.5
2010-10-05T01:06:39.110Z
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](http://mathoverflow.net/questions/23246/peculiar-examples-with-axiom-of-countable-choice/23249#23249).
Tsuyoshi Ito
CC BY-SA 2.5
2010-10-05T11:27:14.347Z
@Ryan: There seems to be a bug with latex math rendering (or is it just me?). In the definition of the Axiom of Determinacy, you wrote "Bob wins the game if x \not \in S", but it is rendered as if you had written "... if x \in S". It can be fixed though by writing "... if x \notin S".
Serge Gaspers
CC BY-SA 2.5
2010-10-05T18:04:50.353Z
@Serge: I don't know, it renders fine for me...
Ryan Williams
CC BY-SA 2.5
2010-10-06T15:13:32.643Z
@Ryan: Indeed, on my other computer, it renders fine as well...
Serge Gaspers
<cc.complexity-theory><lo.logic><pl.programming-languages><big-picture><set-theory>
Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)
Ryan Williams
# Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

(Asked by: username_0 on 2010-10-04)

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](http://en.wikipedia.org/wiki/Axiom_of_determinacy).)

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

**Tags:** cc.complexity-theory, lo.logic, pl.programming-languages, big-picture, set-theory

> **Comments:**
> **username_1**: CW ? or not ? not sure.  
> **username_0**: I'm not sure either... this is one question where I am very unsure about the "complexity" of the answer...  
> **username_0**: Good idea. I'll add it  
> **username_2**: Interesting. Do you know a proof that those axioms are inconsistent that's more elementary (no transfinite induction)?  
> **username_2**: *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!  
> **username_0**: My impression is that the axiom of determinacy does not come up too often for most mathematicians.  
> **username_2**: Here's a different proof of inconsistency: http://www.brics.dk/RS/94/24/BRICS-RS-94-24.pdf . It unfortunately still uses transfinite induction (indirectly in the proof of Zorn's Lemma).  
> **username_3**: [Harvey Friedman's conjectue](http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture). I don't know if it also applies to theoretical computer science.  
> **username_4**: 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](http://mathoverflow.net/questions/23246/peculiar-examples-with-axiom-of-countable-choice/23249#23249).  
> **username_5**: @Ryan: There seems to be a bug with latex math rendering (or is it just me?). In the definition of the Axiom of Determinacy, you wrote "Bob wins the game if x \not \in S", but it is rendered as if you had written "... if x \in S". It can be fixed though by writing "... if x \notin S".  
> **username_0**: @Serge: I don't know, it renders fine for me...  
> **username_5**: @Ryan: Indeed, on my other computer, it renders fine as well...  

---

## 7 answers

### Answer by username_7 on 2010-12-30. Score: 51 | Accepted answer

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](https://mathoverflow.net/a/129211/3106), 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](http://cs.nyu.edu/pipermail/fom/2008-September/013050.html) 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.

> **Comments:**
> **username_19**: 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.  
> **username_7**: @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.  
> **username_4**: I like this answer because it explains why the use of the axiom of choice in TCS seems extremely rare.  
> **username_3**: @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$](http://en.wikipedia.org/wiki/Absoluteness#Shoenfield.27s_absoluteness_theorem).  
> **username_17**: This answer is [featured](http://cstheory.blogoverflow.com/2011/09/what-does-it-really-mean-to-prove-the-graph-minor-theorem/) on the community blog.  
> **username_18**: @username_3 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.](https://math.stackexchange.com/questions/3491349/projective-conservativity-of-choice)  

---

### Answer by username_6 on 2010-10-05. Score: 39

My understanding is that the known proof for the [Robertson-Seymour theorem](http://en.wikipedia.org/wiki/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.

> **Comments:**
> **username_0**: This is a good start, since it's not known how to prove the theorem otherwise.  
> **username_7**: 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.  
> **username_7**: Emil Jeřábek has shown on [MathOverflow](http://mathoverflow.net/questions/129142/weakest-choice-principle-required-for-robertson-seymour-graph-minor-theorem) 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.  
> **username_8**: So the accepted answer is actually false?  
> **username_7**: @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.  
> **username_8**: That’s ali right. It’s just that people might come along and not read the comments, and will take away the “accepted truth”.  

---

### Answer by username_9 on 2010-10-05. Score: 21

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 by username_10 on 2010-10-05. Score: 17

The [Hadwiger-Nelson Problem](http://en.wikipedia.org/wiki/Hadwiger%E2%80%93Nelson_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,"](http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6WHS-48YVT67-3&_user=10&_coverDate=08/31/2003&_rdoc=1&_fmt=high&_orig=search&_origin=search&_sort=d&_docanchor=&view=c&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=a7237ebe7f1cefd6a2fb5ac8f3f24ef0&searchtype=af) 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.

> **Comments:**
> **username_11**: Isn't this more math-oriented than TCS-oriented?  
> **username_10**: That's why I said "tangentially" related.  Coloring problems are TCS-oriented, just not this specific one.  
> **username_1**: ahem. This is about coloring geometric objects. Geometers around the world are now preparing $\alpha$-thin slivers to send in your direction :)  
> **username_10**: Excellent. Validation.  

---

### Answer by username_12 on 2017-10-27. Score: 6

Some of the work of [Olivier Finkel](http://www.logique.jussieu.fr/~finkel/) seems related to the question---though not necessarily explicitly about the Axiom of Choice itself---and in line with username_7's answer. For instance, quoting the abstract of [Incompleteness Theorems, Large Cardinals, and Automata over Finite Words](https://hal.archives-ouvertes.fr/hal-01588572), *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 by username_11 on 2010-10-04. Score: 3

[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](http://www.cs.umd.edu/~gasarch/papers/poll.pdf) 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](http://en.wikipedia.org/wiki/P_versus_NP_problem) 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](http://www.scottaaronson.com/papers/pnp.pdf)]. 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](http://www.cs.technion.ac.il/~shai/ph.ps.gz)]. 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.

> **Comments:**
> **username_14**: Another interesting fact (also from Wikipedia) is that, the main (only?) general technique for proving independence in ZFC, forcing, cannot prove that P=?NP is independent of ZFC. This is a corollary of Shoenfield's absoluteness theorem.  
> **username_11**: Thanks Travis. Here's the pointer: http://en.wikipedia.org/wiki/Absoluteness. See also http://www.cs.uwaterloo.ca/~shai/P%20vs%20NP-2.ppt and http://blog.computationalcomplexity.org/2009/09/is-pnp-ind-of-zfc-respectable-viewpoint.html.  
> **username_13**: Note that Bill is taking another poll, which is open for another month or so: http://blog.computationalcomplexity.org/2011/06/i-am-conducing-new-poll-on-p-vs-np.html  
> **username_11**: @username_13: Thanks for the update. I'm really eager to know the community's most recent consensus.  

---

### Answer by username_15 on 2017-10-27. Score: 2

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 username_7 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](https://en.wikipedia.org/wiki/De_Bruijn%E2%80%93Erd%C5%91s_theorem_(graph_theory)) 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](https://en.wikipedia.org/wiki/Solovay_model) due to a clever constructions involving measure theory.

> **Comments:**
> **username_16**: Nice example. I think username_7 did address this kind of example in the paragraph about the chromatic number of the plane.  
> **username_15**: @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”  
> **username_16**: 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.  

---

