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



A weak form of countable choice
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.


