11
$\begingroup$

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

$\endgroup$
5
$\begingroup$

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$".

$\endgroup$
  • $\begingroup$ "If $X=Y$ then the quoted definition would not give a function." Thanks, I think this was the key point I was missing. $\endgroup$ – asmeurer Dec 15 '13 at 4:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.