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)$?
Best Answer
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.