Does the specification of a general sequence require the Axiom of Choice?

Many results in elementary analysis require some form of the Axiom of Choice (often weaker forms, such as countable or dependent). My question is a bit more specific, regarding sequences.

For example, consider a standard proof of the boundedness theorem which states that a function continuous on a closed interval $I$ is bounded on that interval. In the first step of the proof, one specifies a sequence as follows:

Suppose for contradiction that $f$ is unbounded. Then for every $n\in\mathbb{N}$ there exists $x_n$ such that $f(x_n) > n$. This specifies a sequence $(x_n)$.

I'm not sure if the above example requires choice. To me, it certainly feels like it does. More specifically, I think that we are specifying a sequence of sets $$A(n) = \left\{x\in I\mid f(x) > n\right\}$$ and claiming the existence of a choice function $g$ such that $g(n) \in A(n)$ so that this example specifically requires the axiom of countable choice. Please clarify whether my reasoning is correct. More specifically, does the construction of any general sequence (such as one defined as above, or perhaps recursively) then require some form of choice? Thanks for any help.

-
I think it's probably equivalent to countable choice. –  tomasz Jun 30 '12 at 23:33
Or a weak form of it. (The existence of the sequence, not boundedness.) –  tomasz Jun 30 '12 at 23:44

Actually, if $f$ is continuous from a closed interval (say $[0,1]$) into $\mathbb R$ then you do not need the axiom of choice to prove it is bounded.

1. First observe that closed and bounded intervals are still compact even without the axiom of choice. The proof of this is quite nice and simple, let $\mathcal B$ be an arbitrary open cover of $[0,1]$, simply consider $x=\sup\{y\in[0,1]\mid [0,y]\text{ has a finite subcover in }\mathcal B\}$, deduce that $[0,x]$ is finitely covered as well, and then argue that we have to have $x=1$ (by the same reason).

2. We can deduce from the above that a subset of $\mathbb R$ is compact if and only if it is closed and bounded. If it is compact it cannot be unbounded, and it has to be closed since $\mathbb R$ is a Hausdorff space; on the other hand, if it is closed and bounded it is a subset of a closed interval, therefore closed in a compact space and thus compact.

3. It is still true that if $f$ is a continuous function from a compact set into a metric space then its image is compact. To see this simply note that every open cover of the image can be translated into an open cover of the compact domain, therefore we can take a finite subcover, and this translate to a finite subcover of the image.

Therefore the image of a continuous image of a closed interval is compact and the image attains minimal and maximal values (since the image is a closed set).

Also note that $A(n)$ as you specified it is simply intersection of $I$ with an open set which is the preimage of $(n,\infty)$. Choosing from open sets is doable without the axiom of choice [3].

In general, when we simply produce one sequence we can sometimes avoid choice if we have a method of calculating the next element in a uniform way (induction is not a uniform way!). If we simply "take another element" then we end up using choice, but we can sometimes avoid these things (for example, instead of arbitrary $\delta$ take $\frac1k$ for the least $k$ fitting). It may even be possible, when needed just one sequence, to use the rational numbers. Those are countable and in particular well-orderable and we can choose from those as much as we want.

However sometimes we want to argue that non-trivial sequences exist, and for this we indeed have to have some choice. For example the proof that $\lim_{x\to a}f(x)=f(a)$ implies $f\colon A\to\mathbb R$ is continuous at $a$ may break, because we need to argue for all sequences and not produce just one.

It may be the case that $A$ itself is Dedekind-finite, and every sequence has only finitely many terms (at least one of those repeating, of course) so in the above case $x_n\to a$ implies that almost always $x_n=a$, but we can make sure that $f$ is not continuous at $a$. Indeed in such $A$ there are only finitely many rational numbers, and pulling the trick of choosing rationals no longer works.

Thank you for the detailed answer Asaf. A few follow-up questions. 1. So does the original argument given in fact require choice? 2. You pointed out that $A(n)$ as I specified is a union of an open pre-image and a closed interval and that you can choose from open sets without choice. How exactly does this translate into a construction of a sequence in this case? (I guess I am asking for an explicit construction of the sequence) –  EuYu Jul 1 '12 at 4:12
@EuYu: First observe that every sequence that can be specified without choice can be simply said to exist without it. The original argument "This specifies a sequence" has a bit of choice in flavour, but adding "we choose from open sets in an interval, so no choice is needed" can be added to remove choice. As for the construction see the third link [part 1 and the addendum talk on choices], and remember that an open set in $[0,1]$ is an open set in $\mathbb R$ intersected with the interval, so it is either empty or it contains an interval so the argument holds. –  Asaf Karagila Jul 1 '12 at 6:36