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

`constructive-mathematics`

fits very well with your question. $\endgroup$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. $\endgroup$1more comment