Bolzano-Weierstrass Theorem Proof Abbott (Ax. of Choice) In Abbott's Proof of the Bolzano-Weierstrass Theorem, does Abbott use any form of the Axiom of Choice ? 
I think he is since he chooses an $a_{n_k} \in I_k$ where there are multiple such $a_{n_k}$. 

 A: I think it should be clearly understood that most non-logicians don't care so much whether they use AC or not, so it is difficult to say whether they are unaware that they are using AC or whether they know how to avoid AC but just never say it.
Here, for example, one could 'argue' that "select a half" uses DC (dependent choice), because the English indefinite determiner "a" does not stipulate any specific choice, and each selection depends on the previous selections. However, as we ought to know, the use of DC here is trivially eliminated by saying "select the leftmost half" instead.
Similarly, the choice of each $n_k$ in the proof exactly as written can be argued to use DC, again because of the use of indefinite determiners "some" and "an", and since each choice depends on the previous one. In other words, there is no clue that the author is aware of the use of DC, but also no evidence that the author is not. As before, this use of DC is easily eliminated by saying "select $n_k$ to be the least natural number greater than $n_{k-1}$ such that $a_{n_k} ∈ I_k$". Once we do that, the sequence $(n_k)_{k∈\mathbb{N}}$ can be constructed by a trivial application of the recursion theorem, which does not need any choice whatsoever.
A: Choice is not used to "select a half for which this is the case", because we can just pick the lower half if we need to make a choice.
Choice is not used to select an $a_{n_1}$ because we can pick the least $n$ such that $a_n \in I_1$. However, to select all of the $n_i$ together, we use the axiom of dependent choice (which is a very weak choice principle, but it implies countable choice).
