I am reading Andrej Bauer's Five stages of accepting constructive mathematics. Theorem 1.3 proves that the axiom of choice implies excluded middle. Shortly afterwards Bauer implies that the axiom of countable choice is constructively valid. However I can't see why the same proof doesn't show that countable choice also implies excluded middle.

The proof of Theorem 1.3 goes as follows:

For an arbitrary proposition $P$ define $A = \{ x \in \{0,1\} | P \vee (x=0) \}$ and $B = \{ y \in \{0,1\} | P \vee (y=1) \}.$

Since each of $A$ and $B$ is inhabited (by 0 and 1 respectively), by choice there is a function $f \colon \{ A, B\} \rightarrow A \cup B$ such that $f(A) \in A$ and $f(B) \in B$. Since $A, B \subseteq \{0,1\}$, we have exhaustive cases:

  • $f(A) = 1$. Then $1 = f(A) \in A$, so $P \vee (1=0) $ , which is equivalent to $P$.

  • $f(B) = 0$. Then $0 = f(B) \in B$, so $P \vee (0=1) $ , which is equivalent to $P$.

  • $f(A) = 0$ and $f(B) = 1$. Then we have $\neg P$, for if $P$ were true, then $A = B= \{0,1\}$ so $0 = f(A) = f(B) = 1$, which is absurd.

In each case we have decided either $P$ or $\neg P$, so choice implies excluded middle.

Why doesn't the same argument go through with countable choice (``every countable family of inhabited sets has a choice function'')? The set of sets we index over here, $\{A, B\}$, is finite. What's to stop us defining $A_0$ and $A_1$ to be $A$ and $B$ above and then setting, e.g., $A_2 = \{2\}$, $A_3 = \{3\} \ \dots $ and using the choice function given to us by countable choice to run the same argument again looking at the values $f(A_0)$ and $f(A_1)$?

  • 4
    $\begingroup$ Note that Bauer does not say that the axiom of countable choice is constructively provable, but rather that it is adopted [as an axiom] in some flavours of constructive mathematics. $\endgroup$
    – Rob Arthan
    Jan 9, 2020 at 22:20

1 Answer 1


The key point is that, as Bauer mentions, countable choice refers to the statement "every family of inhabited sets indexed by $\mathbb{N}$ has a choice function". In other words, given a family $(A_n)_{n\in\mathbb{N}}$ such that each $A_n$ is inhabited, there exists a function $f:\mathbb{N}\to\bigcup A_n$ such that $f(n)\in A_n$ for each $n$.

Classically, you could deduce the axiom of choice for finite families from this statement by putting your finite family in bijection with the first $n$ natural numbers and then extending the family in some arbitrary way on the rest of the natural numbers. Constructively, however, you can't do this, because there isn't necessarily a natural number $n$ such that your finite set has exactly $n$ elements! Indeed, this is crucially exactly what is going on in the proof of excluded middle from choice: if you knew the set $\{A,B\}$ had a cardinality that was a natural number, that would decide $P$: $P$ is true if $\{A,B\}$ has $1$ element and $\neg P$ is true if it has $2$ elements.

  • $\begingroup$ Thanks! I think I understand, but let me check: is it also true that the axiom of choice holds for families of size $n$ for each finite $n$ constructively, but the union of these axioms ($AC_1, AC_2, \dots$) also doesn't imply excluded middle by the argument above, since we don't know the cardinality of $\{A,B\}$? $\endgroup$
    – h4yz
    Jan 9, 2020 at 11:33
  • 1
    $\begingroup$ In your second paragraph, it's not immediately clear why you need a bijection rather than just a surjection (in the case in point from $\{0, 1\}$ onto $\{A, B\}$). What goes wrong if you only have a surjection is that the choice function $f$ can choose different elements for $f(0)$ and $f(1)$ even if $f(0) = f(1)$. $\endgroup$
    – Rob Arthan
    Jan 9, 2020 at 23:30
  • 1
    $\begingroup$ @h4yz: The usual definition of "finite" in a constructive setting is that there exists a surjection from a natural number. $\endgroup$ Jan 9, 2020 at 23:33
  • 1
    $\begingroup$ @h4yz: That's right. (I believe your parenthetical guess is also right, but I don't know this stuff well enough to say definitively.) $\endgroup$ Jan 9, 2020 at 23:54
  • 2
    $\begingroup$ You may find this ncatlab article helpful, because once you leave the classical setting, subtle distinctions between different notions of finiteness creep in. (I have just been reminding myself of some of them $\ddot{\smile}$.) $\endgroup$
    – Rob Arthan
    Jan 10, 2020 at 0:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .