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

  • $\begingroup$ What's an example of a topos in which $AC_{0,0}$ fails? $\endgroup$ Commented Mar 7, 2021 at 17:55
  • $\begingroup$ I think constructive-mathematics fits very well with your question. $\endgroup$
    – Hanul Jeon
    Commented Mar 7, 2021 at 18:02
  • $\begingroup$ @HanulJeon Thanks, I added it. $\endgroup$ Commented Mar 7, 2021 at 18:03
  • 5
    $\begingroup$ @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. $\endgroup$ Commented Mar 7, 2021 at 18:04
  • 2
    $\begingroup$ 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. $\endgroup$
    – aws
    Commented Mar 8, 2021 at 16:07

1 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.

  • 1
    $\begingroup$ 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. $\endgroup$ Commented Mar 23, 2021 at 18:13
  • $\begingroup$ Right, that works! $\endgroup$
    – aws
    Commented Mar 23, 2021 at 20:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.