Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?) 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.)
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&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.] 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.