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

3 totally revised. Would have deleted old one but did not see how

Looks interesting (no surprise there). It claims to be

I didn't beat out every detail but it looks constructive and to me (there is 35 pages longone b which should be a B). A footnote does sayThere are considerations like:

• John Conway collaborated 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 research reported here, and has been listed as an author case. That is sort of excluded middle but simply shows that the constructed bijection (in this work since it was first distributed 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 1994Advances in Mathematics, Volume 113, Number 1, June 1995 , pp. But he has never approved 1-44(0)

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

Gives a careful description of this exposition, which he regards as full the kind of fluff’.construction desired .

2 added 1 characters in body

Looks intresting interesting (no surprise there). It claims to be constructive and is 35 pages long. A footnote does say:

• John Conway collaborated on the research reported here, and has been listed as an author of this work since it was first distributed in 1994. But he has never approved of this exposition, which he regards as full of ‘fluff’.
1