En matemáticas, un conjunto está habitado si existe un elemento .
En las matemáticas clásicas, la propiedad de estar habitado es equivalente a no estar vacío . Sin embargo, esta equivalencia no es válida en la lógica constructiva o intuicionista , por lo que esta terminología separada se utiliza principalmente en la teoría de conjuntos de las matemáticas constructivas .
En el lenguaje formal de la lógica de primer orden , un conjunto tiene la propiedad de estar habitado si
Un conjunto tiene la propiedad de estar vacío si , o equivalentemente . Aquí representa la negación .
Un conjunto no es vacío si no está vacío, es decir, si , o equivalentemente .
El modus ponens implica , y tomando cualquier proposición falsa como tal se establece que siempre es válida. Por lo tanto, cualquier conjunto habitado es demostrablemente también no vacío.
En matemáticas constructivas, el principio de eliminación de la doble negación no es automáticamente válido. En particular, un enunciado de existencia es generalmente más fuerte que su forma doblemente negada. Esta última simplemente expresa que la existencia no puede descartarse, en el sentido fuerte de que no puede negarse consistentemente. En una lectura constructiva, para que se cumpla para alguna fórmula , es necesario que se construya o conozca un valor específico de que satisfaga . Del mismo modo, la negación de un enunciado cuantificado universal es en general más débil que una cuantificación existencial de un enunciado negado. A su vez, se puede demostrar que un conjunto no es vacío sin que se pueda demostrar que está habitado.
Los conjuntos como o están habitados, como lo demuestra, por ejemplo , . El conjunto está vacío y, por lo tanto, no está habitado. Naturalmente, la sección de ejemplos se centra en conjuntos no vacíos que no se puede demostrar que estén habitados.
Es fácil dar ejemplos de cualquier propiedad teórica de conjuntos simple, porque los enunciados lógicos siempre pueden expresarse como enunciados teóricos de conjuntos, utilizando un axioma de separación . Por ejemplo, con un subconjunto definido como , la proposición siempre puede enunciarse de manera equivalente como . La afirmación de existencia doblemente negada de una entidad con una determinada propiedad puede expresarse afirmando que el conjunto de entidades con esa propiedad no está vacío.
Definir un subconjunto mediante
Claramente y , y del principio de no contradicción se concluye . Además, y a su vez
La lógica mínima ya prueba , la doble negación para cualquier enunciado de tercero excluido, que aquí es equivalente a . Así que al realizar dos contraposiciones sobre la implicación anterior, se establece . En palabras: No se puede descartar consistentemente que exactamente uno de los números y habita . En particular, este último se puede debilitar a , diciendo que se prueba que no es vacío.
Como ejemplos de enunciados para , considere la infame afirmación demostradamente independiente 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, se eligen para que no se puedan demostrar. Una variante de esto es considerar proposiciones matemáticas que simplemente aún no están establecidas - véase también los contraejemplos brouwerianos . El conocimiento de la validez de o es equivalente al conocimiento sobre como se indicó anteriormente, y no se puede obtener. Dado que ni ni se pueden demostrar en la teoría, tampoco se demostrará que estén habitados por algún número particular. Además, un marco constructivo con la propiedad de disyunción no puede probar ninguno de los dos. No hay evidencia para , ni para , y la imposibilidad de demostrar constructiva de su disyunción refleja esto. No obstante, dado que descartar el tercero excluido es demostradamente siempre inconsistente, también se establece que no está vacío. La lógica clásica adopta axiomáticamente, arruinando una lectura constructiva.
Existen varios conjuntos fácilmente caracterizados cuya existencia no es demostrable en , pero cuya existencia se implica por el axioma completo de elección . Como tal, ese axioma es en sí mismo independiente de . De hecho, contradice otros axiomas potenciales para una teoría de conjuntos. Además, también contradice principios constructivos , en un contexto de teoría de conjuntos. Una teoría que no permite el tercio excluido tampoco valida el principio de existencia de funciones .
En , es equivalente a la afirmación de que para cada espacio vectorial existe una base. De manera más concreta, 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 elusivo en el sentido de que existen diferentes modelos que niegan y validan su existencia. De modo que también es consistente postular simplemente que la existencia no puede descartarse aquí, en el sentido de que no puede negarse consistentemente. Nuevamente, ese postulado puede expresarse diciendo que el conjunto de tales bases de Hamel no está vacío. Sobre una teoría constructiva, tal postulado es más débil que el postulado de existencia simple, pero (por diseño) todavía es lo suficientemente fuerte como para negar todas las proposiciones que implicarían la no existencia de una base de Hamel.
Dado que los conjuntos habitados son lo mismo que los conjuntos no vacíos en la lógica clásica, no es posible producir un modelo en el sentido clásico que contenga un conjunto no vacío pero que no satisfaga " está habitado".
Sin embargo, es posible construir un modelo de Kripke que diferencie entre las dos nociones. Dado que una implicación es verdadera en todo modelo de Kripke si y sólo si es demostrable en lógica intuicionista, esto establece de hecho que no se puede demostrar intuicionistamente que " no está vacío" implica " está habitado".
Este artículo incorpora material del conjunto Inhabited en PlanetMath , que se encuentra bajo la licencia Creative Commons Attribution/Share-Alike License .
