Inspired by a recent Math.SE question entitled [Where do we need the axiom of choice in Riemannian geometry?](https://math.stackexchange.com/questions/10102/where-do-we-need-the-axiom-of-choice-in-riemannian-geometry), I was thinking of the [Arzelà--Ascoli theorem](http://en.wikipedia.org/wiki/Arzel%C3%A0%E2%80%93Ascoli_theorem). Let's state a very simple version:



> 
> **Theorem.** Let $\{f\_n : [a,b] \to [0,1]\}$ be an equicontinuous sequence of functions. Then a subsequence $\{f\_{n(i)}\}$ converges uniformly on $[a,b]$.
> 
> 
> 


The proofs I have seen operate as follows: Take a countable dense subset $E$ of $[a,b]$. Use a "diagonalization argument" to find a subsequence converging pointwise on $E$. Use equicontinuity to conclude that this subsequence actually converges uniformly on $[a,b]$.


The "diagonalization" step goes like this: Enumerate $E$ as $x\_1, x\_2, \dots$. $\{f\_n(x\_1)\}$ is a sequence in $[0,1]$, hence has a convergent subsequence $\{f\_{n\_1(i)}(x\_1)\}$. $\{f\_{n\_1(i)}(x\_2)\}$ now has a convergent subsequence $\{f\_{n\_2(i)}(x\_2)\}$, and so on. Then $\{f\_{n\_i(i)}\}$ converges at all points of $E$.


Of course, to do this, at each step $k$ we had to choose one of the (possibly uncountably many) convergent subsequences of $\{f\_{n\_{k-1}(i)}(x\_k)\}$, so some sort of choice is needed here (I guess dependent choice is enough? I am not a set theorist (IANAST)). Indeed, we have proved that $[0,1]^E$ is sequentially compact (it is metrizable so it is also compact).


On the other hand, we have not used (equi)continuity in this step, so perhaps there is a clever way to make use of it to avoid needing a choice axiom.


So the question is this:



> 
> Can the Arzelà--Ascoli theorem be proved in ZF? If not, is it equivalent to DC or some similar choice axiom?
> 
> 
> 



Does Arzelà-Ascoli require choice?
There is a canonical way of checking the literature for most questions of this kind. Since they come up with some frequency, I think having the reference here may be useful.



> 
> First, look at "Consequences of
>  the Axiom of Choice" by Paul Howard
>  and Jean E. Rubin, Mathematical
>  Surveys and Monographs, vol 59, AMS,
>  (1998). 
> 
> 
> If the question is not there, but has
>  been studied, there is a fair chance
>  that it is in the database of the book
>  that is maintained online,
>  <http://consequences.emich.edu/conseq.htm>
> 
> 
> 


Typing "Ascola" on the last entry at the page just linked, tells me this is form 94 Q. Note the statement they provide is usually called the classical Ascoli theorem: 



> 
> For any set $F$ of continuous functions 
>  from ${\mathbb R}$ to ${\mathbb R}$, the following conditions
>  are equivalent:  
> 
>  1. Each sequence in $F$ has a subsequence that converges
>  continuously to some continuous
>  function (not necessarily in $F$ ).  
> 
>  2. (a) For each $x \in{\mathbb R}$ the set $F (x) =\{f (x) \mid f \in F \}$ is bounded, and  
> 
>  (b) $F$ is equicontinuous.
> 
> 
> 


To see the other equivalent forms of entry 94, type "94" on the line immediately above. 


From there we learn: Form 94 is "Every denumerable family of non-empty sets of reals has a choice function."


There are some other equivalent forms that may be of interest. For example: 


* (94 E) Every second countable topological space is Lindelöf.
* (94 G) Every subset of ${\mathbb R}$ is separable.
* (94 R) Weak Determinacy. *If* $A$ is a subset of ${\mathbb N}^{\mathbb N}$ with the property that 
$\forall a \in A\forall x \in{\mathbb N}^{\mathbb N}($ if $x(n) = a(n)$ for $n = 0$ and $n$ odd, then $x\in A)$, *then* in the game [$G(A)$](http://en.wikipedia.org/wiki/Determinacy#Games) one of the two players has a winning strategy.
* (94 X) Every countable family of dense subsets of ${\mathbb R}$ has a choice function.


Proofs and references are provided by the website and the book. A reference that comes up with some frequency in form 94 is Rhineghost, Y. T. "The naturals are Lindelöf iff Ascoli holds". Categorical perspectives (Kent, OH, 1998), 191–196, Trends Math., Birkhäuser Boston, Boston, MA (2001).


