Hidden usage of countable choice

Question

In some variations of constructive mathematics, Countable Choice can be even proven (example $-$ this relatively fresh book). In formal terms, the statement is as following:

$$ \forall x \exists y . \varphi[x, y] \implies \exists f \forall x . \varphi[x, f(x)].$$

In the Countable Choice, $x$ is a natural number unlike in usual the Axiom of Choice where $x$ may be anything. In constructive math, there needs to be an algorithm producing $y$ from the given $x$ with the property $\varphi[x, y]$. More details in here.

Now let us recall in which cases we really need the Choice. The answer is, when we deal with infinite sets and the object, that we seek, is not uniquely defined.

My questions thus is: Can we turn any proof of a theorem that uses the Countable Choice into a working computer program?

Answer 1

(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.

Answer 2

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.

Answer 3

I would just like to point out that computing the maximum of two real numbers is constructive in every sense of the word. As soon as one is able to calculate absolute values (exercise), the maximum can be defined as $\max(x,y) = (x + y + |x - y|)/2$. Thus, computing the maximum of finitely many reals is not a problem at all, and in particular does not involve any kind of choice. Note that this is different from saying that we can tell which number is the maximal one (we cannot do that constructively).