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.
Best Answer
The following is a proof in Coq, or am I missing something?