The construction in the paper seems to rely on two non-constructive assumptions:
- We can decide whether two elements in a set (involved in the division by 3) are equal.
- 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?
This is only a partial answer because I'm having trouble reconstructing something I think I figured out seven years ago...
It would seem the Dual Cantor-Bernstein implies Countable Choice. In a post in sci.math in March 2003 discussing the dual of Cantor-Bernstein, Herman Rubin essentially points out that if the dual of Cantor-Bernstein holds, then every infinite set has a denumerable subset; this is equivalent, I believe, to Countable Choice.
Let $U$ be an infinite set. Let $A$ be the set of all $n$-tuples of elements of $U$ with $n\gt 0$ and even, and let $B$ be the set of all $n$-tuples of $U$ with $n$ odd. There are surjections from $A$ onto $B$ (delete the first element of the tuple) and from $B$ onto $A$ (for the $1$-tuples, map to a fixed element of $A$; for the rest, delete the first element of the tuple). If we assume the dual of Cantor-Bernstein holds, then there exists a one-to-one function from $f\colon B\to A$ (in fact, a bijection). Rubin writes that "a 1-1 mapping from $B$ to $A$ quickly gives a countable subset of $U$", but right now I'm not quite seeing it...
Best Answer
There is no constructive proof.
To show this, let $A = \mathbb{N}$ and let $B = \{ n \in \mathbb{N}\; |\; \varphi_n(0) \uparrow \}$, where $\varphi_n(0) \uparrow$ means that the $n$th Turing machine is undefined on input 0. There are computable injections $f:A \rightarrow B$ and $g:B \rightarrow A$ (the identity), but no computable surjection from $A$ to $B$ because $B$ is not a c.e. set.
To see why Konig's proof is nonconstructive, let's say that we want to know what the image of $n \in A$ is under the bijection. In order to do this we need to know whether we apply $f$ or $g^{-1}$. But to know this we need to decide whether $n$ is an $A$-stopper, a $B$-stopper, or neither. However we can't do this constructively because it would require checking the entire possibly infinite sequence to see if it ever stops. In fact, in the example above, being able to decide whether or not $g^{-1}$ is defined is the same as deciding the halting problem, so at odd stages we don't even know whether or not the sequence extends any further back at all.