In the (whimsically written) article Division by three, Doyle and Conway describe a proof, (apparently) not using Choice, that an isomorphism $A \times 3 \simeq B\times 3$ of sets (where $3$ is a given three-element set) gives an isomorphism $A \simeq B$. The result is easy for well-ordered $A$ and $B$, but clearly assuming this isn't constructive. However, the authors seem (to me) to use excluded middle. Also, I don't know if I'm entirely convinced they avoid all forms of choice – it may be they are relying on some weak form of choice (aside from excluded middle).
Has anyone given this any thought? The article is from the mid-90s despite its ArXiV date, and purports to have discovered a lost proof of Lindenbaum from the 1920s which predates a different proof given by Tarski in 1949.
Best Answer
The construction in the paper seems to rely on two non-constructive assumptions:
(By "infinite" I mean "contains an infinite sequence of pairwise distinct elements".) In computability theory the second assumption corresponds to Turing degree $0''$.
To see where the second assumption is used, consider the proof of Lemma 2 on page 26. There one is given an infinite sequence of 0's, 1's and 2's and one must decide whether there are infinitely many 0's in the sequence (and if not, whether there are infinitely many 1's). Let us show that such a decision procedure is equivalent to the second assumption. In one direction, a ternary sequence contains infinitely many 0's iff the set of indices at which the 0's appear is infinite. Conversely, given a countable subset $A \subseteq \mathbb{N}$ enumerated by $e$, consider the sequence $a_0, a_1, \ldots$ where
The sequence has infinitely many 0's iff $A$ is infinite.
Another kind of a typical construction in the paper requires one to determine whether the orbit of an element $x$ under a bijection is finite or infinite. We can do this using our assumptions as follows. Given $x \in A$ and a bijection $f : A \to A$, construct a sequence $a_0, a_1, \ldots$ as follows:
Here we assumed that $A$ has decidable equality. The sequence $a_k$ contains a zero iff it contains infinitely many zeroes (thus we only require a $0'$ oracle to perform the following steps). If it contains a zero, say $ak = 0$ then the orbit $\lbrace x, f(x), f^2(x), \ldots \rbrace$ is finite with at most $k$ elements. If it does not contain a zero then the orbit is infinite because $f^k(x) \neq f^j(x)$ for all $k \neq j$, as otherwise we would have $f^{|k-j|+1}(x) = x$.
Let me just remark that one might be tempted to consider a non-constructive assumption such as:
(This would certainly allow us to determine whether orbits of elements under bijections are finite or infinite.) In fact division by 3 follows, but for a rather strange reason, namely that such a principle implies the law of excluded middle. Suppose $p$ is an arbitrary thruth value, and consider the Abelian group $G$ freely generated by the generators $p$ and $\top$ (true). Consider the subgroup of $G$ generated by the element $\top - p$. If it is infinite then there is $n \in \mathbb{N}$ such that $n \top \neq n p$, hence $\top \neq p$ and so $\lnot p$ holds. If the subgroup is finite then there is $n > 0$ such that $n \top = n p$, hence $\top = p$ and $p$ holds. (I hope I got this right, we have to be careful because finite sets need not have definite sizes.)
This hopefully gives us some idea about how non-constructive are the techniques employed in the proof of division by three (essentially it looks like a $0''$ oracle). It seems hard to quantify how non-constructive the theorem itself is. Knowing that I can divide by 3 does not obviously allow me to derive non-constructive consequences. For all I know, some suitably constructivized version of division by 3 might actually be constructively valid.
Can I have a green flag now, please?