## How constructive is Doyle-Conway’s ‘Division by three’?

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.

-
For exposition alone, that Doyle+Conway paper is one of my favorites. – Theo Johnson-Freyd Aug 25 2010 at 5:46

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?

-
Thanks, Andrej - this is exactly the sort of thing I was after. In discussion at the nForum it seems like this sort of result could hold in a Boolean \Pi-pretopos, but I think I've worn everyone out with my continual '..but why??'s. – David Roberts Aug 27 2010 at 7:15
"Boolean $\Pi$-pretopos" is just a fancy way of saying "classical logic + set theory without powersets". I don't see an essential use of powersets in the construction, so yes, the proof probably works in that setting. – Andrej Bauer Aug 27 2010 at 20:42

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.

-
Aha - I thought I smelt a rat. Although I wonder if given more constructive input and setup, one could resurrect the proof, or at least the result... – David Roberts Aug 25 2010 at 12:15
It is indeed interesting to ask whether the result can be constructivized. For a start, I'd try to adapt the proof to the case when the sets involved have decidable equality. – Andrej Bauer Aug 25 2010 at 12:30
That was a kind of loose statement on my part but I'll leave it out of honesty. I did add a detail to show where I was heading. My point of view was: even given total knowledge of the ingredient functions(s) and everything pertaining to them, can one construct a desired bijection in a natural way? – Aaron Meyerowitz Aug 25 2010 at 16:10
Toby Bartels tells me privately that even with decidable equality it would be suspicious. For a start, given a vertex on one of the connected components of the (directed) graph, they know whether it is an infinite, doubly infinite or finite component. This smells fishy to me. – David Roberts Aug 25 2010 at 21:45
I am not doing this to collect little green flags. The way to measure the level of (un)constructivity of a statement is to see what sort of non-constructive consequences it has. But I do not understand how one might measure the constructivity level of a proof that uses excluded middle. At the very least, we would have to transform the proof first so that it does not refer directly to excluded middle but to weaker statements (such as "every countable set is finite or infinite"). Anyhow, I am going to spend 10 minutes thinking about this. – Andrej Bauer Aug 26 2010 at 9:39
show 1 more comment

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

-

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

-
 I'm not sure what "sort of" excluded middle means; it is definitely a use of excluded middle, and it thereby makes the proof not constructive in the constructivists' sense. – Mike Shulman Aug 26 2010 at 4:54