There is a widely accepted opinion that the Axiom of Countable Choice (further, **ACC**)

$$ \forall n\in \mathbb{N} . \exists x \in X . \varphi [n, x] \implies \exists f: \mathbb{N} \longrightarrow X . \forall n \in \mathbb{N} . \varphi [n, f(n)] $$

is justified constructively due to certain interpretations of intuitionistic logic (for example, **BHK**). For example, this question already highlights interpretation of **ACC**. My question is more of a "practical" one: the best I hope for is to see an example of algorithm extraction from a constructive theorem which used **ACC**.

**ACC** means that if for any natural $n$ and any $x$ of *any* set $X$ there is a proof that $\varphi [n, x]$ holds, then there exists a *function* that produces $x$'s such that $\varphi [n, x]$ holds for any given $n$ as input. The catch is, a constructive proof already means a certain procedure of finding $x$ with the property $\varphi [n, x]$.

There have been, however, doubts in accepting **ACC** (or dependent choice) in constructive mathematics (see, for example, 1, 2, 3, 4, 5, 6). Since the question whether to accept **ACC** (or dependent choice) is rather methamatematical, I'd like to discuss its meaning in terms of algorithms (or computer programs).

Roughly speaking, if you "put" a proof on paper and everything is constructive, and say you used **ACC**, does it mean that it somehow hinders programming this proof?

The things I learned from the literature are:

**(1)** Some important constructive results rely on **ACC** or even dependent choice. It concerns the Fundamental Theorem of Algebra, existence of bases of Hilbert spaces, existence of square roots of complex numbers, some facts about complete metric spaces. For example, Bridges, Richman and Schuster showed that the Bishop's lemma used at least a certain weaker form of **ACC**:

**Lemma**. Let $A$ be a non-empty located complete subset of a metric space $X$ and $x$ some point in $X$. Then, there exists a point $a \in A$ such that $\rho(x, a) > 0 \implies \rho(x, A) > 0$.

**(2)** There is a distinction between general Cauchy sequences and the so called *modulated* Cauchy sequences. The former have the form:

$$ \forall n \in \mathbb{N}. \exists N \in \mathbb{N}. \forall k,m \ge N. |x_k - x_m | \le \frac{1}{n} $$

whereas the letter have the so called *convergence modulus* $\mathcal{N}: \mathbb{N} \rightarrow \mathbb{N}$:

$$ \forall n \in \mathbb{N}. \forall k,m \ge \mathcal{N}(n). |x_k - x_m | \le \frac{1}{n} $$

It is easy to see that both are equivalent as long as **ACC** holds. In particular, Cauchy and Dedekind reals are isomorphic. Consequently, Cauchy reals are Cauchy complete. It not the case if **ACC** does not hold as was pointed out by Lubarsky. However, every modulated Cauchy sequence of modulated Cauchy reals converges to a modulated Cauchy real.

**(3)** **ACC** was given various interpretations. For example, non-deterministic algorithm, black-box etc. Some even claimed that **ACC** is in some sense responsible for "discontinuities" in computation.

**(4)** There does not seem to be a proof assistant which allows program extraction under **ACC**. In Coq, one can define **ACC** in the `Type`

universe, but in `Prop`

it has to be an axiom and Coq cannot crack it open to extract a program. I am aware only of results on "computational" content of **ACC** which use bar induction/recursion, fan theorem, Gödel numbering etc.

**(5)** In some formal systems, **ACC** and even stronger axioms of choice can be proven. For example, in Martin-Löf's type theory. Another example is this system of Ye which is even weaker than Bishop's constructive mathematics. Theorem 11, item 16 has a form similar to a choice axiom. Consequently, Ye, Lemma 27 is the Bishop's lemma.

## Now, my question is

What exactly is **ACC** and what exactly is an extracted program from **ACC**? Are there any practical examples? What does it mean for a "realized" **ACC** to be a "black box" program?

**Particular question**: why does one need **ACC** to prove the Bishop's lemma? Take, for example, construction in Lemma 27 of Ye.
He explicitly constructs a Cauchy sequence, which is even modulated in an evident way, and shows the implication. Where exactly is an ambiguity of choices?

**Remark**: variations of this question may already be found here and SE (for example, my own questions 1 and 2), but I still do not fully understand how to interpret **ACC** constructively.

becausewitnesses are incorporated into the definitions). Therefore Ye's system is not Bishop's system, andthereforein BISH I do not see how to avoid the axiom of countable choice in the proof of Bishop's lemma. I am quitting this question now, my efforts to help seem not to help at all. $\endgroup$2more comments