15
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ For the benefit of the readers, could you please explain what ACC is? I am guessing that you mean the principle introduced by Bridges, Richman and Schuster in their paper you linked to, but it's not really clear from your question. $\endgroup$ – Andrej Bauer Jan 4 '17 at 0:16
  • 5
    $\begingroup$ Pretty much a duplicate of mathoverflow.net/questions/22990/choice-vs-countable-choice, at least my answer would be a duplicate. $\endgroup$ – Andrej Bauer Jan 4 '17 at 7:24
  • 1
    $\begingroup$ Good to see people reading Ye's work. I think those results should be pushed as far as they can go. $\endgroup$ – David Roberts Jan 4 '17 at 10:16
  • 1
    $\begingroup$ @DavidRoberts I think the same. I studied every single letter in this book and find it really impressive. It has everything one would want from constructive analysis: a rigorous statement of a formal logical system, pretty simplistic and transparent proofs and applications to physics. $\endgroup$ – Rubi Shnol Jan 4 '17 at 11:44
  • 2
    $\begingroup$ I repeat: I never said that Ye's proof uses the axiom of countable choice (!!). Ye's lemma is however not the same as Bishop's lemma, since Bishop does not incorporate a witness function in the locatedness of A. In Ye's system countable choice is provable (because witnesses are incorporated into the definitions). Therefore Ye's system is not Bishop's system, and therefore in 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$ – Frank Waaldijk Jan 7 '17 at 19:59
-1
$\begingroup$

The following is a proof in Coq, or am I missing something?

Goal forall (X : Set) (phi : nat -> X -> Prop),
    (forall (n : nat), {x : X | phi n x})
    -> {f : nat -> X | forall n, phi n (f n)}.
Proof.
  intros X phi all.

  exists (fun n => proj1_sig (all n)).
  intros n.
  destruct (all n).
  simpl.
  auto.
Qed.
$\endgroup$
  • 6
    $\begingroup$ This is the axiom of choice in the Type universe, not in Prop. The notation {x : X | phi n x} is a dependent sum $\sum_{x : X} \phi\,n\,x$ whereas you asked about exists x : X, phi n x. $\endgroup$ – Andrej Bauer Jan 9 '17 at 8:13
  • $\begingroup$ In absence of proof_irrelevance or classical reasoning or similar concepts, shouldn't be every proof of non-computational existence correspond directly and canonically to a proof of computational existence? On the other hand, at least as soon as one admits classical reasoning for Prop, it should be possible to set phi to, for example, the graph of some busy bever function, and therefore ACC cannot have computational content? (Not sure what happens when only having proof_irrelevance.) $\endgroup$ – Christoph-Simon Senjak Jan 10 '17 at 5:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.