A weak form of countable choice

Question

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}$?

Answer 1

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.