A weak form of countable choice

Let $$\Omega$$ be the set/type of truth values. We're using constructive logic. Define

$$AC_{0, 0} = \forall P : \mathbb{N}^2 \to \Omega, (\forall n \in \mathbb{N}, \exists m \in \mathbb{N}, P(n, m)) \to \exists f : \mathbb{N} \to \mathbb{N}, \forall n \in \mathbb{N}, P(n, f(n))$$.

It is well-known that $$AC_{0, 0}$$ is sufficient to prove that the Cauchy and Dedekind reals coincide. I have determined that a weaker form of this axiom also suffices.

$$AC_{weak} = \forall P : \mathbb{N} \times 2 \to \Omega, (\forall n \in \mathbb{N}, \exists m \in 2, P(n, m)) \to \exists f : \mathbb{N} \to 2, \forall n \in \mathbb{N}, P(n, f(n))$$

Or to put it another way,

$$\forall P : \mathbb{N} \to \Omega, \forall Q : \mathbb{N} \to \Omega, (\forall n \in \mathbb{N}, P(n) \lor Q(n)) \to \exists f : \mathbb{N} \to 2, \forall n \in \mathbb{N}, (f(n) = 0 \to P(n)) \land (f(n) = 1 \to Q(n))$$

Why does $$AC_{weak}$$ suffice? Consider the locatedness axiom for a Dedekind cut $$(L, U)$$, which states

$$\forall a, b \in \mathbb{Q}, a < b \to (a \in L \lor b \in U)$$.

Clearly, $$S = \{(a, b) \in \mathbb{Q}^2 : a < b\}$$ is a decidable infinite subset of $$\mathbb{Q}$$; hence, it can be put into bijection with $$\mathbb{N}$$. Then by $$AC_{weak}$$, we will have a choice function $$f : S \to 2$$ such that $$f(a, b) = 0$$ implies $$a \in L$$, and $$f(a, b) = 1$$ implies $$b \in U$$.

This allows us to use the classic "trisect the interval" trick to get a Cauchy sequence.

My primary question is this. Does $$AC_{weak}$$ imply $$AC_{0, 0}$$? My intuition says no. It's clear that $$AC_{weak}$$ easily allows us to prove something similar about predicates $$P : \mathbb{N} \times k \to \Omega$$, where $$k$$ is any finite set. This can be shown by induction. But extending to the case where $$k$$ is infinite doesn't seem possible.

If $$AC_{weak}$$ does not imply $$AC_{0, 0}$$, does anyone know of a topos in which $$AC_{weak}$$ holds but not $$AC_{0, 0}$$?

• What's an example of a topos in which $AC_{0,0}$ fails? Commented Mar 7, 2021 at 17:55
• I think constructive-mathematics fits very well with your question. Commented Mar 7, 2021 at 18:02
• @HanulJeon Thanks, I added it. Commented Mar 7, 2021 at 18:03
• @AlexKruckman The topos of sheaves over $\mathbb{R}$ is one where the Dedekind and Cauchy reals are not isomorphic. Thus, over this topos, $AC_{0, 0}$ cannot hold. Of course, $AC_{weak}$ must also not hold there too. Commented Mar 7, 2021 at 18:04
• There are some related independence proofs in Rathjen & Swan, Lifschitz realizability as a topological construction (Corollary 7.5), although that is for even weaker versions of countable choice, so it doesn't quite answer the question.
– aws
Commented Mar 8, 2021 at 16:07

It turns out, I believe, that there's actually a fairly simple counterexample.

The example is sheaves on the topological space given by the product of countably many copies of $$\mathbb{N}$$ with downwards closed set topology. Explicitly, the underlying set of the space is $$\mathbb{N}^\mathbb{N}$$ and a set $$U \subset \mathbb{N}^\mathbb{N}$$ is open when it is downwards closed (according to the pointwise ordering) and for every $$f \in U$$ there exists $$n \in \mathbb{N}$$ such that $$g \in U$$ whenever $$g|_n = f|_n$$. For each open set $$U \subseteq \mathbb{N}^\mathbb{N}$$ and each $$f \in U$$, write $$U_f$$ for the open neighbourhood defined as below, where $$n$$ is least ensuring that $$U_f \subseteq U$$. $$U_f := \{ g \in \mathbb{N}^\mathbb{N} \;|\; g(i) \leq f(i) \text{ for } i \leq n \}$$

Observe that the space is locally connected in the very strong sense that any inhabited open set contains the function $$\lambda n.0$$, so any two inhabited open sets have an inhabited intersection. We also have the following lemma.

Lemma Whenever $$U_f$$, as above, is the union of two open subsets $$U_f = V \cup W$$, either $$V = U_f$$, or $$W = U_f$$.

Proof We show the contrapositive. Suppose $$g \in U_f \setminus V$$ and $$h \in U_f \setminus W$$. Note $$U_f$$ is closed under binary joint (wrt the pointwise order), and so $$g \vee h \in U_f \setminus (V \cup W)$$.

We first check that $$\mathbf{AC}_{\mathbb{N}, 2}$$ holds in sheaves. Suppose $$R : \mathbb{N} \times 2 \to \Omega$$ is a total relation over an open set $$U$$. Let $$f \in U$$. Then restricting $$R$$ to $$U_f$$, for each $$n \in \mathbb{N}$$ we have $$U_f = [[ R(n, 0) ]] \cup [[ R(n, 1) ]]$$. Hence by the lemma we have either $$[[ R(n, 0) ]] = U_f$$ or $$[[ R(n, 1) ]] = U_f$$. Applying countable choice externally gives us a function $$c : \mathbb{N} \to 2$$ such that $$[[ R(n, c(n)) ]] = U_f$$, which we can then use to give an internal function over $$U_f$$. However, $$U$$ is covered by open sets of the form $$U_f$$, so we have choice functions everywhere in $$U$$, as required.

We now show that $$\mathbf{AC}_{\mathbb{N}, \mathbb{N}}$$ does not hold in the topos. Define $$R : \mathbb{N} \times \mathbb{N} \to \Omega$$ so that $$[[R(n, m)]] = \{ f : \mathbb{N} \to \mathbb{N} \;|\; f(i) \leq m \text{ for } i \leq n \}$$. Observe that we do have $$\bigcup_{m \in \mathbb{N}} [[R(n, m)]] = \mathbb{N}^\mathbb{N}$$ for each $$n$$, and so this does give a total relation in the topos. Write $$d$$ for the identity function $$\mathbb{N} \to \mathbb{N}$$. We will show that there is no open neighbourhood $$V$$ of $$d$$ with a choice function for $$R$$ defined everywhere on $$V$$. By restricting to $$V_d$$, we may assume without loss of generality that $$V$$ is of the form $$\{ g \in \mathbb{N}^\mathbb{N} \;|\; g(i) \leq i \text{ for } i \leq n \}$$ for some $$n$$. Suppose that $$C$$ is a choice function defined on $$V$$ internally in the topos. Since $$V$$ is connected, we in fact have an external underlying function $$c : \mathbb{N} \to \mathbb{N}$$ such that for all $$i$$ we have $$[[ R(i, c(i)) ]] = V$$. In particular we have $$[[ R(n + 1, c(n + 1)) ]] = V$$ for the $$n$$ above. However, this gives a contradiction, since $$[[ R(n + 1, c(n + 1)) ]]$$ does not contain the element $$g$$ of $$V$$ defined below: $$g(i) := \begin{cases} i & i \leq n \\ c(n + 1) + 1 & \text{otherwise} \end{cases}$$

Hence we have confirmed the topos of sheaves on $$\mathbb{N}^\mathbb{N}$$ satisfies $$\mathbf{AC}_{\mathbb{N}, 2}$$ but not $$\mathbf{AC}_{\mathbb{N}, \mathbb{N}}$$.

Finally, regarding the implication $$\mathbf{AC}_{\mathbb{N}, 2} \Rightarrow \mathbb{R}_c = \mathbb{R}_d$$, I'll say the same as Andrej Bauer: I've seen the result before, and I think it's fairly well known, but I can't point to anywhere specific in the literature where it is mentioned.

• Great answer! It seems we can apply your argument to the function $z = \lambda n . 0$ to show that there is no choice function for $R$ in any neighbourhood of $z$, since $[[R(n + 1, c(n + 1)]]$ does not contain the function $g(i) = 0$ when $i \leq n$, $c(n + 1) + 1$ otherwise. Thus, $\mathbf{AC}_{\mathbb{N}, \mathbb{N}}$ doesn't hold locally in any inhabited $V$ (since all inhabited $V$ contain $z$), and we see that $\neg \mathbf{AC}_{\mathbb{N}, \mathbb{N}}$ is satisfied in sheaves, which is even stronger than $\mathbf{AC}_{\mathbb{N}, \mathbb{N}}$ not being satisfied. Commented Mar 23, 2021 at 18:13
• Right, that works!
– aws
Commented Mar 23, 2021 at 20:16