Hidden usage of countable choice

(1) One possible reason for explicitly drawing attention to uses of countable choice is that Bishop style constructive mathematics should be as "universal" as possible. Not only should proofs hold in the well known varieties of constructive mathematics, but they should still be valid in $\mathsf{ZF}$. It's also nice if the theorems hold in the internal language of toposes, but there are many examples of toposes where countable choice fails.

(2)-(4) I don't think Schwichtenberg's proof uses countable choice at all. Regarding maximums, we have the following

• Supremums are always unique when they exist.
• Supremums of finite sets of reals exist.
• Maximums of finite sets of integers or rationals exist. That is, given rationals $a_1,\ldots,a_n$, there is an $i$ such that $a_i = \sup \{a_1,\ldots,a_n\}$. However, this $i$ might not be unique, but that's okay because we can just take the largest such $i$.
• Constructively we cannot prove that supremums of finite sets of reals are always attained so the maximum might not exist.

So we may assume that the $j$ in Schwichtenberg's proof is unique. However it turns out that in this case we don't even need $j$ to be unique. This is because we only need one $j$ but countable choice would only be used if we wanted an infinite sequence. The key point is that we have modulus of continuity functions built into the definition of continuous function, which we use to make sure we pick a suitable $j$ first time. If I recall correctly this is quite a common technique when working constructively without countable choice.

In Bauer's proof something slightly different happens. He is proving something slightly different and perhaps he has in mind simpler, more natural definitions of sequence and continuous function. In his proof, $f(x_1),\ldots,f(x_n)$ is a finite list of real numbers that aren't necessarily rational. The maximum of a finite set of real numbers might not be attained constructively. That is, there might not exist an $i$ such that $f(x_i) = \max(f(x_1),\ldots,f(x_n))$. To get round this, Bauer uses the following trick. It turns out that we only need $i$ such that $f(x_i) \geq \max(f(x_1),\ldots,f(x_n)) - 1$. Such a number exists but is not uniquely defined, so to get a sequence of such numbers as Bauer's proof requires, we need to use countable choice.

(5) Bauer is most likely referring to realizability models and in particular the effective topos. If we can prove that a function exists constructively then we can do so internally in the effective topos. But this implies that we can find a computable witness. Since countable choice holds in the effective topos, we can assume it in our proofs and still get computable witnesses.

The OP is suggesting that it is possible to do the following constructively:

Conjecture: Let $x_1, \ldots, x_n \in \mathbb{R}$ and $M = \max(x_1, \ldots, x_n)$. For every $\epsilon > 0$ the set $\{i \in \mathbb{N} \mid |M - x_i| < \epsilon\}$ has a smallest element.

I will show that the case $n = 3$, $\epsilon = 2$ implies LLPO, which is not constructively valid. Let $(a_k)_k$ be an infinite binary sequence which contains at most one $1$. We would like to decide whether $a_{2 k} = 0$ for all $k$, or $a_{2 k + 1} = 0$ for all $k$. For this purpose define the numbers $$x_1 = \sum_{k=0}^\infty a_{2 k} \cdot 2^{-k}$$ and $$x_2 = \sum_{k=0}^\infty a_{2 k + 1} \cdot 2^{-k}$$ and $$x_3 = 2$$ Note that $0 \leq x_1, x_2 \leq 2$, therefore $\max(x_1, x_2, x_3) = 2$. By the conjecture, the set $\{i \in \{1, 2, 3\} \mid |2 - x_i| < 2\}$ has a smallest element $j$:

• If $j = 1$ then $x_1 > 0$ therefore for some $k \in \mathbb{N}$ we have $a_{2 k} = 1$, from which it follows that $a_{2 k + 1} = 0$ for all $k$.
• If $j = 2$ or $j = 3$ then $x_1 = 0$ therefore $a_{2 k} = 0$ for all $k$.

We are done.