Hidden usage of countable choice

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?

• Those are a lot of questions. Sep 7 '15 at 13:05
• I assume that you're interested in the context of constructive mathematics a-la Bishop and others mentioned in your post. That takes me off the list of potential answerers. I can remark that it seems very unlikely that (2) is true, but I am oblivious to the fine pitfalls of constructive analysis of this type. Sep 7 '15 at 13:55

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

• That third bullet point is mystifying me. Are we not assuming that the numbers $a_1,\cdots,a_n$ are pairwise distinct? Sep 8 '15 at 15:19
• This answer got me interested in the constructive mathematics. Could you provide a reference for the statement that we can't constructively show existence of maximum of finite set of reals? I'd have thought that standard proof of existence of maximum by induction would be constructive. Sep 8 '15 at 15:38
• @ValerySaharov I'm not sure if this has what you want, but there's a section on realizability in Troelstra, van Dalen, Constructivism in Mathematics which is chapter 4, section 4. I slightly glossed over some details. To get existence properties such as the numerical existence property and Church's rule (that I alluded to) we use a more sophisticated form of realizability - q realizability. This is in volume II of Troelstra, van Dalen (chapter 9, section 7).
– aws
Sep 8 '15 at 16:28
• @CameronBuie I'm not assuming they are pairwise distinct - I guess I should have said finitely enumerable rather than finite. (Note that if the set is obtained by evaluating a function at finitely many points they might not be pairwise distinct)
– aws
Sep 8 '15 at 16:30
• @Wojowu In fact you can't even show that the supremum of $\{0, x \}$ is attained for every $x$ because this would imply $x \leq 0$ or $x \geq 0$ which can't be done constructively. In chapter 6, 1.10 in Troelstra, van Dalen Constructivism in Mathematics they show that the supremum of the range of $f : [a, b] \rightarrow \mathbb{R}$ is not always attained, but if you look at the proof it also applies to finite sets of the form $\{0, x\}$. (By the same argument I said but in more detail)
– aws
Sep 8 '15 at 16:36

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.

• Ok, I see now what you mean. But what exactly does countable choice do? It picks the index somehow "randomly"? And does it mean that you can't pick a number from a finite sequence which is an approximate maximum without choice? Because by Lemma 1.24 in here it seems possible. Jan 4 '17 at 22:07
• No, as I explained in that other MO answer, countable choice can be explained in terms of computing canonical representatives of elements. There is no randomness. Jan 4 '17 at 23:36
• Lemma 1.24 has nothing to do with countable choice. I feel like I have now done my share trying to explain things. I respectfully suggest that you spend some time going over the proofs and check the details of how things work. Jan 4 '17 at 23:39
• So there is a set of "approximately maximizing" indices, which are natural numbers, but there is no smallest such natural number ... O-kay ... But, still, if you could give a single practical example of program extraction with ACC, that'd still be much appreciated. Jan 5 '17 at 0:04
• You're not going to get such a non-trivial example because whenever you have a set with canonical representatives, people actually use them, so the realizer for countable choice does not have to do anything. For instance, nobody represents numbers in binary with leading zeroes, they want a canonical representation. And with that the ACC has nothing to do, it just returns the $\forall \exists$ witness because it already is extensional. Jan 5 '17 at 7:23

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

• (1) What smallest index? If you are asking whether, given $x_1, \ldots, x_k \in \mathbb{R}$ and $\epsilon > 0$ there exists $i$ such that $|x_i - \max(x_1, \ldots, x_k)| < \epsilon$ then the answer is positive. And this has nothing to do with choice. (2) Because to find the said sequence in the blog post, one has to choose for each $n \in \mathbb{N}$ a number $x_n$ such that $f(x_n) > n$. Jan 4 '17 at 9:08
• I don't quite follow what you're talking about, but it looks to me lik your choice of "smallest index" depends on the choice of the data for $f$. Jan 4 '17 at 12:52
• Nope, you can't do that (assuming $f$ here is real-valued). It is not decidable whether $f(x_i)$ is greater than a given number. Again, there is an index $i$ such that $f(x_i)$ is close to the supremum, but the index cannot be chosen canonically, for instance you can't say "the smallest such $i$". The set of indices $i$ for which $f(x_i)$ is close to the supremum is inhabited, and its elements can be enumerated by an infinite sequence, but not by a finite one. Jan 4 '17 at 13:13
• This is mathematics, I don't have to explain why your suggestions don't work, you have to make them work. But since you asked, I am going to answer in a separate answer. Jan 4 '17 at 17:11