Axioma de la opción implica la ley de medio excluido

Question

Diaconescu el Teorema de los estados de CA que implica la Ley de Medio Excluido. Esencialmente, la prueba va definiendo $A = \{x \in \{0,1\} : x = 0 \lor p\}$, e $B = \{x \in \{0,1\} : x = 1 \lor p\}$, para una determinada proposición $p$, y la definición de una función de elección $f : \{A,B\} \rightarrow \{0,1\}$. A continuación, muestran que no importa lo que los valores de $f$ es, $p$ o $\lnot p$ mantiene. El pleno de la prueba se puede encontrar aquí.

Lo que me confunde es por eso que el Axioma de Elección es necesaria, ya que sólo estamos eligiendo entre dos conjuntos finitos elección es comprobable en el estándar de ZF. Además, he oído que los contables de elección no implica medio excluido, pero claramente no estamos eligiendo entre más de countably muchos conjuntos en esta prueba.

Answer 1

La elección de un número finito de conjuntos no vacíos es de hecho comprobable en el estándar de ZF, pero el estándar de ZF se basa en la lógica clásica, que incluye la ley del medio excluido.

También, en Diaconescu de la prueba, el conjunto $\{A,B\}$ no puede ser afirmado de ser un elemento del conjunto. Se admite un surjective mapa de, digamos, $\{0,1\}$, el standard de dos element set, pero que el mapa puede no ser bijective desde $A$ podría igualdad de $B$. Si tuviéramos la lógica clásica (medio excluido) disponible, entonces se podría decir que el $\{A,B\}$ tiene dos elementos o de un elemento, y es finito en cualquiera de los casos. Pero sin la ley del medio excluido, no podemos decir que.

En intuitionistic la teoría de conjuntos, hay varios no equivalentes las nociones de la finitud. Los más populares (como lo que puedo decir) equivale a "surjective imagen de $\{0,1,\dots,n-1\}$ para algún número natural $n$." Con esta definición, $\{A,B\}$ es finito, pero no se puede probar la elección de un número finito habitada conjuntos. El segundo más popular de la noción de finito de cantidades "bijective imagen de $\{0,1,\dots,n-1\}$ para algún número natural $n$." Con esta definición, se puede (a menos que yo estoy con vistas a algo) demuestran que la elección de un número finito habitada conjuntos (como en la clásica ZF), sino $\{A,B\}$ no puede ser demostrado ser finito.

(Comentario: escribí "habitada", donde se podría haber esperado que "no vacío". La razón es que "no vacío", tomado literalmente, significa que el conjunto no es vacío, es decir, que no es el caso de que el conjunto no tiene elementos. Esa es la doble negación de "tiene un elemento". Intuitionistically, la doble negación de una afirmación es más débil que la declaración en sí. En la discusión de la elección, yo quería los sets que en realidad tienen los elementos, no sólo no tienen elementos. "Habitada" se ha convertido en el estándar de la terminología de "tener al menos un elemento" en contextos donde el "vacío" no hacer el trabajo.)

Answer 2

El fondo de la teoría es un tema importante. No es del todo correcto decir que la ley del medio excluido es comprobable desde el axioma de elección. Hay dos detalles importantes:

1. Estamos hablando de provability constructivas conjunto de teorías que incluyen la separación de los axiomas para indecidible fórmulas.

2. Estamos hablando de que el axioma de elección como se expresa en la teoría de conjuntos.

Hay otros sistemas constructivos, tales como el tipo constructivo de las teorías, donde el pertinente formulario del axioma de elección no implica la ley del medio excluido. La implicación en Diaconescu del teorema es particular para contribuir a la teoría de conjuntos.

Por separado, como se describe en la universidad de Stanford artículo de la Enciclopedia en http://plato.stanford.edu/entries/set-theory-constructive/index.html#ConChoPri el axioma de contables elección no implica la ley de medio excluido, incluso en la construcción de la teoría de conjuntos.

Si tratamos de aplicar el axioma de contables de elección para el conjunto de Diaconescu el teorema de, nada extraño sucede, porque es fácil escribir una función de elección si vemos la $\{A, B\}$ como una secuencia de dos conjuntos. El truco en Diaconescu del teorema es que si aplicamos la elección a la familia de las $\{A, B\}$, la función de elección tiene que ser extensional, y el teorema aprovecha la extensionality. La sustitución de la familia con una secuencia de dos conjuntos de $A$ $B$ hace que sea más fácil para escribir una fórmula para un extensional función de elección.