Countable choice and term extraction

Question

The constructive Axiom of Countable Choice (ACC) is widely accepted due to its computational content. It states that:

$$ \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)]$$

to mean: if we can (constructively) prove the antecedent than there exists a function that produces $x$'s satisfying the "certificate" $\varphi [n, x]$.

The famous realizability interpretation claims that in order to prove the antecedent, we already have to construct a term (a function) witnessing $\varphi [n, x]$. Therefore, ACC amounts to simple reformatting. However, realizability is a metamathematical concept in which sense it is fair to ask how the claimed functions come into play.

Question: What does a computable realization of ACC precisely mean and how to convert a proof involving ACC into a program?

Answer 1

As I say in the comments to the other question, realizability is described in chapter 4, section 4 of Troelstra and van Dalen Constructivism in Mathematics, Volume I and $\mathbf{q}$-realizability appears in chapter 9, section 7 of Troelstra and van Dalen Constructivism in Mathematics, Volume II. Another reference is Beeson, Foundations of Constructive Mathematics although I don't know the section numbers off hand. There is a variant of $\mathbf{q}$-realizability called realizability with truth in Rathjen, The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory which is used to prove "existence property" results about the constructive set theories $\mathsf{CZF}$ and $\mathsf{IZF}$.

By the way there are in fact several different ways to extract computational information from proofs and a few are compatible with countable choice, but I'll just focus on realizability and $\mathbf{q}$-realizability.

The idea of realizability is to take the Brouwer-Heyting-Kolmogorov interpretation very literally. For each formula $\phi$ we define what it means for a number $e \in \mathbb{N}$ to realize $\phi$. For example, if $\phi$ is of the form $\phi := \phi_1 \rightarrow \phi_2$ then for $e$ to realize $\phi$ means that $e$ codes a computable partial function, $\varphi_e$ such that if $f$ is a realizer for $\phi_1$ then $\varphi_e(f)$ is defined and a realizer for $\phi_2$. We then show that a theory $T$ satisfies a soundness theorem - that is if $T$ proves $\phi$, then $T$ also proves there exists a realizer for $\phi$. If we use $\mathbf{q}$-realizability then there will also be a converse to the soundness theorem - if a formula is realized then it is provable.

To answer the question it happens that it is always very easy to find a realizer for countable choice. A realizer for $(\forall n \in \mathbb{N})(\exists m \in \mathbb{N})\phi(n, m)$ is already a computable function that takes a number as input and returns a (number encoding) a pair $m, e$ such that $e$ is a realizer for $\phi(n, m)$. Finding a choice function is a simple matter of reformatting. There is nothing strange involving random numbers or anything like that.

One final point is that in set theory something slightly subtle happens. We can sometimes have a realizer for $(\exists y) \phi(y)$ without actually knowing what $y$ looks like. However in order to have a realizer for $y \in \mathbb{N}$ we do need to know which natural number it is equal to. So if $\phi(x, y)$ happens to be of the form $y \in \mathbb{N} \wedge \phi'(y)$ we are fine. It turns out that this doesn't matter and the proof that Church's rule holds for set theory still holds. Finding a realizer for countable choice is a simple matter of reformatting as usual. See Rathjen's paper for the details.

Edit: Realizability and similar techniques rely on having complete formal proofs available. This makes it quite hard to give an explicit example of extracting witnesses because formal proofs will usually be pretty long and complicated even for relatively simple statements (independent of whether we assume countable choice or not). In practice we handle formal proofs using proof assistants. I don't know if there are proof assistants that both allow countable choice and witness extraction, but certainly this is something that could be done.

Answer 2

There are a few issues raised in the question, some about the notions of computability and Gödel number. I am just going to focus my answer on the first part of the question, and I'm going to give a very specific answer. So here is what I will attempt to answer:

What does a computable realization of ACC precisely mean and how to convert a proof involving ACC into a working computer program?

Short Answer

Two parts:

• A computable realisation of ACC would mean that it is possible to "look inside" an existential proof and extract the witness, and then use this witness in subsequent constructions e.g. the construction of a function. This would break the paradigm of proof irrelevance.

• It is only possible to convert a proof involving ACC to a working computer program if ACC has some computable realisation. That is, for such a conversion there must be some concrete (non-black-box) program whose type corresponds (by the Curry-Howard correspondence) to ACC. In this case, any proof involving ACC automatically converts to a computer program, as long as the rest of its elements are not black-boxes. Simply replace every application of ACC with an application of its realisation.

Long Answer

I will answer the question as a moderately experienced Coq user. Coq is a proof assistant that is based on the Calculus of (Co)Inductive Constructions. The key underlying feature of Coq is the Curry Howard Isomorphism: a correspondence between the worlds of proofs and programs. In particular, we have the following:

• Every Proposition is a type.
• Every proof is a program. This might also be called a realisation of a type.

Now, the ACC, as stated in the question, is as follows:

$$ \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)]$$

By the Curry-Howard correspondence, Coq does not distinguish between the function type and logical implication. There is also no difference between $\forall$ and the dependent product function type $\Pi x \in X. T(x)$, where $T$ is some dependent type. This is a generalisation of the common function type $A \rightarrow B$, where the return type $B$ is constant with respect to the argument of type $A$. I will not expand the existential quantifiers as it would be too messy, but these two are actually just types too. So the above statement in Coq would be:

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

That is, the axiom is a function type. OK, but what exactly is the range and domain of this function? The domain is a function type and the range is an existential type.

• The range is the function type $(\Pi n\in \mathbb{N} . \exists x \in X . \varphi [n, x])$. Let $g$ be an element of this type. Given a natural number, $g$ returns a witness for the existential. This witness contains both an $x$ and a realisation (or element, or proof) of $\varphi [n, x]$. Remember $\varphi [n, x]$ is a Proposition, which is treated as a type.

• The domain of the axiom function is the existential type $(\exists f: \mathbb{N} \longrightarrow X . \Pi n \in \mathbb{N} . \varphi [n, f(n)])$. An element of this type is a witness. The witness contains a function $f: \mathbb{N} \longrightarrow X$ and a realisation (proof, element) of the type $\Pi n \in \mathbb{N} . \varphi [n, f(n)])$. The latter is itself a function type (I'm starting to get dizzy) taking a natural number $n$ and giving back an element of $\varphi [n, f(n)])$. At this point you might take a breadth and marvel at the expressive power of dependent types.

OK, so back to the question above.

What does a computable realization of ACC precisely mean and how to convert a proof involving ACC into a working computer program?

It actually has two parts:

1. What does a computable realization of ACC precisely mean?
2. How can one convert a proof involving ACC into a working computer program?

To answer $(1)$ we unwind the notions of "computable" and "realisation" (yes, I've deliberately changed to UK spelling, they ruled us for ~700 years). First, a realisation of a type is an element of that type. Second, this realisation is computable if it can be constructed, as opposed to just shown to exist. So a "computable realisation" is a construction of an element of the type specified by ACC. In other words, it is the construction of a function that takes any function in the domain and returns an existential in the range. Can such a realisation of ACC be constructed? The answer is: I've lied to you above. Or at least I've withheld the truth. Coq does distinguish between types and propositions; the latter are treated as types but they are black boxes cannot be used to construct types. In particular, propositions "live" in a "universe" called Prop and types live in one called... well... Type. So strictly, the ACC cannot be constructed in Coq. However, if you relax the constraint and flatten everything to a type world, the construction is possible. In fact, I've defined it in Coq myself:

Definition ACC (X : Type) (P : nat -> X -> Type) (f : (forall n : nat, {x:X & (P n x)})) (n : nat) : X := match f n with (existT x P) => x end.

Theorem ACC_full (X : Type) (P : nat -> X -> Type) (f : (forall n : nat, {x:X & (P n x)})) : {f : nat -> X & (forall n : nat, P n (f n))}. exists (ACC X P f). intros. unfold ACC. remember (f n). destruct s. assumption. Qed.

Please copy & past to the Coq IDE because it renders awfully here. So what a computable realisation of ACC means is that we can look inside the original existential produced by the function on the LHS to construct the RHS term. Normally, this is not allowed, because the existential is a Prop while the RHS is a Type. However, if you relax the statement a bit and define things in terms of the Sig type, as I have done, it works. The Sig type is just the existential type, but in the Type world rather than in the Prop world.

It's now easy to answer the second question, namely: How can one convert a proof involving ACC into a working computer program? If the ACC you use is the strict version, with the existential from Prop on the LHS, then you can't convert such a proof into a program, because your ACC will just be a "black box". But if you relax this to the Type version of ACC, you automatically get a program: simply apply my Coq program above to any program of the LHS type and it will give you a program of the RHS type. Intuitively, what the program ACC does is "cracks open" the existential, "looks inside" and uses what it finds to define a function- this is the function $f$ mentioned in the axiom. The theorem ACC_full then augments this function with the proof that the function is correct, i.e. that the proposition $\varphi$ is respected. It does this by cracking open the first function and applying the hypothesis, using the fact that the first function uses the function from the LHS, which automatically respects $\varphi$. In other words, ACC_full corresponds to the full axiom of computable choice, albeit restricted to the Type world only, while ACC simply defines the function $f$ to be used in the axiom. Note that I'm using P in the place of $\varphi$ in my Coq code.

I realise at the end of my answer that it's a bit messy because I changed my mind about certain things along the way, but I think it is in OK shape. Please, comment with any questions you have though, as I'm sure some of this may not be all that clear.

Answer 3

We are looking at the scheme $$(\forall n\in \mathbb{N})(\exists x \in X)\psi(n,x) \to (\exists f \in X^{\mathbb{N}})(\forall n) \psi(n,f(n)).$$

There are two viewpoints: from pure (classical) computability theory, and from a constructive viewpoint.

In computability theory

The classical computability of the choice scheme depends greatly on the set $X$ and the class of formulas that $\psi$ comes from. In general, $f$ need not be computable, even when $X$ is just $\mathbb{N}$.

• When $X = \mathbb{N}$ and $\psi$ is $\Sigma^0_1$, the function $f$ obtained is always computable. We can define $f(n) = (\mu m)\psi(n,m)$, and this will be computable because $\phi$ is $\Sigma^0_1$.

• If $X = \mathbb{N}$ and $\psi$ is $\Pi^0_2$, then the function $f$ is not computable in general. For example, if we let $\phi_n$ be a standard enumeration of the computable functions, we might let $$\psi_0(m,k) \equiv [(\phi_{n}(n) \text{ halts in $k$ steps}) \Leftrightarrow (\exists s) (\phi_{n}(n) \text{ halts in $s$ steps})].$$ Certainly we have $(\forall n)(\exists k)\psi_0(n,k)$, but there is no computable selector $f$.

Quite a bit is known about the strength of the scheme for the cases $X = \mathbb{N}$, $X = \mathbb{N}^\mathbb{N}$, and $X = P(\mathbb{N})$, when $\psi$ comes from various classes in the arithmetical or analytical hierarchy. Depending on these choices, the strength can vary enormously. In come cases, the choice function may require strong axioms in second-order arithmetic. In other cases, as we have seen, $f$ may be computable.

In constructive mathematics

In constructive mathematics, the situation can be quite different. The reason for this difference is that a proof of $(\forall m)(\exists k)\psi(m,k)$ must be more uniform in constructive mathematics, in various ways, than in classical mathematics. The classical proof of $(\forall m)(\exists k)\psi_0(m,k)$ from above requires a nonconstructive choice between two cases (whether $\phi_n(n)$ halts or not). Such a choice is impossible in constructive systems.

Bishop seems to have thought, essentially, that the right side of the choice scheme is a synonym for the left side, in his perspective on constructivism. This is evident in his comment about the choice scheme following from "the very meaning of existence". Similarly, the BHK interpretation validates the choice scheme, as do several kinds of realizability.

In these settings, I would not view the choice scheme as a "mere existence claim". Instead, I would view as stating an equivalence that follows directly from the meanings that its components have been given, much like the classical equivalence $$\lnot (\exists x)\phi(x) \Leftrightarrow (\forall x)\lnot \phi(x)$$ follows directly from the meanings of its components.

Answer 4

I understand that my expertise in this field is quite low, but I try to answer my own question (in layman's terms).

First of all, I completely agree with @aws's insightful answer and comments. The only subtlety, in my view, is that we are talking about metamathematical concepts here that leads to a bit of confusion. Nevertheless, the question that I asked is, I think, legitimate.

So,

1. Either we consider only so called modulated Cauchy reals which are essentially pairs of maps one of which computes $n$-th rational approximation and another control the speed of convergence like this:

$$ \left( x \in \mathbb{R} \right) \triangleq \left( \forall k \forall n,m \geq M_x(k) . \big| x(n) - x(m) \big| \leq 2^{-k} \right), $$

where (with little abuse of notation) $x: \mathbb{N} \longrightarrow \mathbb{Q} $ and $ M_x: \mathbb{Z} \longrightarrow \mathbb{N} - $ Cauchy modulus.

2. Or we remove $k$ from $M_x(k)$ from the definition and consider generic Cauchy sequences, either modulated or unmodulated ones.

As pointed out by Lubarsky, reals defined in the way 1. are not even Cauchy complete. They are, however, complete in the following sense:

Theorem. Every modulated Cauchy sequence of modulated reals converges to a modulated real.

To provide full Cauchy completeness, Axiom of Countable Choice (ACC) is needed to jump from

$$ \left( \forall k \exists M_x \forall n,m \geq M_x . \big| x(n) - x(m) \big| \leq 2^{-k} \right) $$

to

$$ \left( \exists M_x:\mathbb{Z} \longrightarrow \mathbb{N}. \forall k \forall n,m \geq M_x(k) . \big| x(n) - x(m) \big| \leq 2^{-k} \right) $$

The trick is, as @aws correctly mentioned, to treat the realizability interpretation literally. There literally needs to be a (computable) function $M_x(k)$ behind any proof involving a generic Cauchy real and ACC. The question is, what is that function? What can be said about it? It turns out that little to none can be said. Following Richman and A. Bauer in A Computable Universe: Understanding and Exploring, it is merely a black box obliged to spit out some numbers satisfying the certificate $\varphi(x, f(x))$. No guarantee can be given that such a box would emit the same output for the same input $-$ it might well depend on some internal state unknown.