Estoy tratando de caminar a través de la prueba de Diaconescu el teorema de que el axioma de elección implica la ley de medio excluido en http://plato.stanford.edu/entries/intuitionism/#ChoAxi. Parafraseando:
Deje $A$ ser una declaración (que vamos a pensar como uno que no podría haber constructiva de la prueba o refutación). Vamos $$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\}\\{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 $$ holds. Thus $A\v \neg$.
También me miró a través de la prueba de Wikipedia. Las cosas que no entiendo:
¿Por qué no podemos simplemente dejar $f(X) = 0$$f(Y) = 1$. No podemos decir $T \vee P = T$ en intuitionistic lógica? La Wikipedia versión no tiene este problema porque sólo tienen la segunda parte de la instrucción lógica en la definición de los conjuntos.
Más al punto, ¿esto no es una prueba implícitamente el uso de la ley de medio excluido? Si $P = (f(X) = f(Y))$, prueba de ello es el uso de $P \vee \neg P \iff T$, ¿no?
Estoy suponiendo que mi lógica es errónea en este último punto, de alguna manera. Paradójicamente, mi intuición acerca de intuitionistic lógica es inexistente, porque nunca sé si estoy en secreto con la ley del medio excluido (sobre todo desde que estoy capacitado para utilizar de forma automática todo el tiempo).
