How constructive is Doyle-Conway's 'Division by three'?

Question

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.

Answer 1

The construction in the paper seems to rely on two non-constructive assumptions:

1. We can decide whether two elements in a set (involved in the division by 3) are equal.
2. A countable subset of $\mathbb{N}$ is infinite or not infinite.

(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

$a_k = 0$ if $e$ enumerates a new element at step $k$, and $a_k = 1$ otherwise.

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:

$a_k = 0$ if there is $m \leq k$ such that $x = f^m(x)$, and $a_k = 1$ otherwise.

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:

A group generated by a single element is either infinite or finite.

(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?

Answer 2

The proof is not constructive, it is done in something like ZF (with classical logic). For example, the proof of Tarski's Lemma on page 27 starts with:

"If $A \succeq B$ (there is an injection $B \to A$) then there is $C$ such that $A \cong B + C$ (there is a bijection $A \to B + C$), namely the complement of the image of $B$ under some injection from $B$ into $A$."

This is a thoroughly classical step, as it can easily happen intuitionistically that there is an injection $B \to A$ such that the complement of its image is empty, but there is no bijection between $B$ and $A$. The whole paper has many such classical steps. I disagree with Aaron's statement that the proof "shows that the constructed bijections (...) are as explicit as the ingredients but not more so". You can't parametrize classical proofs like that, at least not easily.

Answer 3

(I'm cutting and pasting and slightly modifying some comments taken from a discussion on this question currently taking place at the nForum. It's based on my memory of their paper, which I do not have in front of me, so it's possible I have misremembered something, or that I'm projecting something onto the paper when I conjecture that "constructive" for Conway and Doyle really means "natural".)

Near the beginning of the paper, Conway and Doyle explain what they mean by 'constructive' by means of an example:

If $A$, $B$, and $C$ are finite sets, show that $A + C = B + C$ implies $A = B$ constructively.

The authors then give what is essentially a categorified proof which may have been first observed by Joyal. The idea is that there is a general notion of "trace" (which was later formalized by Joyal, Street, and Verity in their notion of traced monoidal category: something like the structure which would remain if you took all the structure present in a tortile or ribboned category and then never mentioned dual objects). The trace is an transformation

$$\phi_{A, B; C}: \hom(A \otimes C, B \otimes C) \to \hom(A, B)$$

which is natural in $A$ and $B$ and extranatural in $C$, satisfying axioms expected of a partial trace. In particular, the symmetric monoidal category of finite sets and bijections (with monoidal product $+$) admits a traced monoidal structure which maps a bijection $f: A + C \to B + C$ to a bijection $g: A \to B$ obtained by feedback (feed back values of $f$ which land in $C$ back into $f$, and iterate until you land out of $C$).

This gave me the clue that for Conway and Doyle, 'constructive' really means 'natural' in the technical sense of category theory. My memory is that "constructive" for them means "no unnatural choices" (such as a choice of bijection $A \cong $ {1, ..., $n$}), making their proofs "coordinate-free", as it were, and this is effectively formalized by the categorical sense of naturality.

So in other words, Conway and Doyle are in essence defining a natural transformation of the form

$$\hom(3A, 3B) \to \hom(A, B),$$

where $A$ and $B$ are construed as objects in the category of sets and bijections, and I think this is the essential content of the "constructivity" they are after.

Standard proofs of the Cantor-Schroeder-Bernstein theorem, also mentioned by Conway and Doyle by way of illustration, are also natural in the categorical sense.

Answer 4

I didn't beat out every detail but it looks constructive to me (there is one b which should be a B). There are considerations like: Each component (in a directed graph with outdegree 1 and maximum indegree 1) is a cycle, a one way infinite directed path or a bi-infinite directed path so do a,b or c depending on the case. That is sort of excluded middle but simply shows that the constructed bijection (in this case constructed from injections A->B and B->A for the Cantor–Bernstein–Schroeder theorem) are as explicit as the ingredients but not more so (I'm not sure if that captures your question).

The well written article

Producing New Bijections from Old by Feldman D.; Propp J. in Advances in Mathematics, Volume 113, Number 1, June 1995 , pp. 1-44(0)

(available in postscript from http://faculty.uml.edu/jpropp/articles.html)

Gives a careful description of the kind of construction desired . One killer example from that paper: If P is the permutations of a set and L the linear orders of that set then there is no natural bijection from L to P (even if the set has 3 elements) because there is a distinguished permutation (the identity) but no distinguished linear order. However, there is a natural bijection from LxL to PxL using the 2 line notation.

The paper is written in a relaxed style and has a footnote indicating that Conway might not be that committed every remark and detail of the exposition.

Actually the remark that

• since 3a=3b implies a=b in finite arithmetic...for finite sets a bijection from Ax3 to Bx3 should yield one from A to B

is suspicious to me (because of the example above).