Conjunto habitado

Defina un subconjunto${\displaystyle A\subseteq \{0,1\}}$a través de

${\displaystyle A:=\{n\in \{0,1\}\mid (P\land n=0)\lor (\neg P\land n=1)\}}$

Claramente${\displaystyle P\leftrightarrow 0\in A}$y${\displaystyle (\neg P)\leftrightarrow 1\in A}$y del principio de no contradicción se concluye${\displaystyle \neg (0\in A\land 1\in A)}$. Más,${\displaystyle (P\lor \neg P)\leftrightarrow (0\in A\lor 1\in A)}$y a su vez

${\displaystyle (P\lor \neg P)\to \exists$ !(n\in \{0,1\})\ n\in A}

La lógica mínima ya demuestra${\displaystyle \neg \neg (P\lor \neg P)}$, la doble negación para cualquier enunciado de tercero excluido, que aquí es equivalente a${\displaystyle \neg (0\notin A\land 1\notin A)}$. Así, al realizar dos contraposiciones sobre la implicación anterior, se establece${\displaystyle \neg \neg \exists$ !(n\in \{0,1\})\ n\in A} . En palabras: No se puede descartar consistentemente que exactamente uno de los números${\displaystyle 0}$y${\displaystyle 1}$habita${\displaystyle A}$. En particular, este último puede debilitarse a${\displaystyle \neg \neg \exists n\ n\in A}$, dicho${\displaystyle A}$Se ha demostrado que no es vacío.

Como ejemplos de declaraciones para${\displaystyle P}$Consideremos las infames afirmaciones demostrablemente independientes de la teoría, como la hipótesis del continuo , la consistencia de la teoría sólida en cuestión o, informalmente, una afirmación incognoscible sobre el pasado o el futuro. Por diseño, estas se eligen para que sean indemostrables. Una variante de esto es considerar proposiciones matemáticas que simplemente aún no están establecidas; véanse también los contraejemplos brouwerianos . El conocimiento de la validez de cualquiera de ellas${\displaystyle 0\in A}$o${\displaystyle 1\in A}$es equivalente al conocimiento sobre${\displaystyle P}$como se indicó anteriormente, y no se puede obtener. Dado que no${\displaystyle P}$ni${\displaystyle \neg P}$Aunque pueda probarse en teoría, tampoco lo demostrará.${\displaystyle A}$estar habitado por algún número particular. Además, un marco constructivo con la propiedad de disyunción no puede demostrar${\displaystyle P\lor \neg P}$tampoco. No hay ninguna evidencia${\displaystyle 0\in A}$ni para${\displaystyle 1\in A}$y la imposibilidad constructiva de demostrar su disyunción refleja esto. No obstante, dado que descartar el tercero excluido es demostrablemente siempre inconsistente, también se establece que${\displaystyle A}$no está vacío. La lógica clásica adopta${\displaystyle P\lor \neg P}$Por definición, arruinar una lectura constructiva.

Hay varios conjuntos fácilmente caracterizables cuya existencia no es demostrable en${\displaystyle {\mathsf {ZF}}}$, pero que se da por sentado que existen por el axioma completo de elección${\displaystyle {\mathrm {AC} }}$. Por lo tanto, ese axioma es en sí mismo independiente de${\displaystyle {\mathsf {ZF}}}$De hecho, contradice otros posibles axiomas de una teoría de conjuntos. Además, también contradice principios constructivos en el contexto de la teoría de conjuntos. Una teoría que no permite el principio del tercero excluido tampoco valida el principio de existencia de funciones.${\displaystyle {\mathrm {AC} }}$.

En${\displaystyle {\mathsf {ZF}}}$, el${\displaystyle {\mathrm {AC} }}$es equivalente a la afirmación de que todo espacio vectorial tiene una base . Así pues, más concretamente, consideremos la cuestión de la existencia de una base de Hamel de los números reales sobre los números racionales . Este objeto es esquivo en el sentido de que existen diferentes${\displaystyle {\mathsf {ZF}}}$modelos que niegan y validan su existencia. Por lo tanto, también es consistente postular que la existencia no puede descartarse aquí, en el sentido de que no puede negarse de forma consistente. Nuevamente, ese postulado puede expresarse diciendo que el conjunto de tales bases de Hamel no es vacío. Sobre una teoría constructiva, dicho postulado es más débil que el postulado de existencia simple, pero (por diseño) sigue siendo lo suficientemente fuerte como para negar todas las proposiciones que implicarían la no existencia de una base de Hamel.