Understanding a proof of Diaconescu's theorem

I am trying to walk through the proof of Diaconescu's theorem that the axiom of choice implies the law of excluded middle at http://plato.stanford.edu/entries/intuitionism/#ChoAxi. To paraphrase:

Let $A$ be a statement (which we will think of as one which might not have a constructive proof or disproof). Let $$X = \{x\in \{0, 1\}|x = 0 \vee (x = 1 \wedge A)\},$$ $$Y= \{x\in \{0, 1\}| x = 1 \vee (x = 0 \wedge A)\}.$$ Let $f:\{X, Y\}\to \{0, 1\}$ be a choice function. Then if $f(X) \neq f(Y)$, then $X \neq Y$, giving $\neg A$, whereas if $f(X) = f(Y)$, then $A$ holds. Thus $A\vee \neg A$.

I also looked through the proof on Wikipedia. The things I don't get:

• Why can't we just let $f(X) = 0$ and $f(Y) = 1$. Can we not say $T \vee P = T$ in intuitionistic logic? The Wikipedia version doesn't have this problem because they just have the second part of the logical statement in the definition of the sets.

• More to the point, doesn't this proof implicitly use the law of excluded middle? If $P = (f(X) = f(Y))$, the proof is using $P \vee \neg P \iff T$, isn't it?

I'm assuming that my logic is flawed in that last point somehow. Paradoxically, my intuition about intuitionistic logic is nonexistent, because I never know if I am secretly using the law of the excluded middle (especially since I am trained to use it automatically all the time).

Why can't we just let $f(X)=0$ and $f(Y)=1$.
Because the function has to be extensional. If $X = Y$ then the quoted definition would not give a function.
The proof is using $P∨¬P⟺T$, isn't it?
Yes, because equality for natural numbers is decidable: given two natural numbers $n,m$, the constructive systems to which Diaconescu's theorems applies will prove "$n = m \lor m \not = n$".
• "If $X=Y$ then the quoted definition would not give a function." Thanks, I think this was the key point I was missing. – asmeurer Dec 15 '13 at 4:34