La teoría constructiva de conjuntos es un enfoque del constructivismo matemático que sigue el programa de la teoría axiomática de conjuntos . El mismo idioma de primer orden con "" y ""de la teoría de conjuntos clásica se utiliza habitualmente, por lo que no debe confundirse con un enfoque de tipos constructivos . Por otro lado, algunas teorías constructivas están de hecho motivadas por su interpretabilidad en las teorías de tipos .
Además de rechazar la ley del medio excluido , las teorías de conjuntos constructivos a menudo requieren que algunos cuantificadores lógicos en sus axiomas estén delimitados , motivados por resultados ligados a la impredicatividad .
Introducción
panorama
La lógica de las teorías discutidas aquí es constructiva en el sentido de que rechaza, es decir, que la disyunción se mantiene automáticamente para todas las proposiciones. Esto requiere el rechazo de principios de elección sólidos y la reformulación de algunos axiomas estándar. Por ejemplo, el axioma de elección implicapara las fórmulas en el esquema de separación adoptado por uno, por el teorema de Diaconescu . Resultados similares son válidos para el axioma de regularidad en su forma estándar. A su vez, las teorías constructivas a menudo no permiten pruebas clásicas de propiedades que, por ejemplo, son demostrablemente indecidibles computacionalmente . En comparación con la contraparte clásica, también es menos probable que se pruebe la existencia de relaciones que no se pueden realizar. Esto también afecta la demostrabilidad de enunciados sobre órdenes totales como el de todos los números ordinales , expresados por la verdad y la negación de los términos en el orden que define la disyunción.. Y esto, a su vez, afecta la fuerza teórica de la prueba definida en el análisis ordinal . Dicho esto, teorías sintienden a probar reformulaciones clásicamente equivalentes de teoremas clásicos. Por ejemplo, en el análisis constructivo no se puede probar el teorema del valor intermedio en su formulación de libro de texto, pero se pueden probar teoremas con contenido algorítmico que, tan pronto comose supone, son a la vez clásicamente equivalentes al enunciado clásico. La diferencia es que las pruebas constructivas son más difíciles de encontrar.
En modelos
Muchas teorías estudiadas en la teoría de conjuntos constructiva son meras restricciones, con respecto a su axioma así como a su lógica subyacente, de la teoría de conjuntos de Zermelo-Fraenkel () . Estas teorías también pueden interpretarse en cualquier modelo de. En lo que respecta a las realizaciones constructivas, existe una teoría de la realizabilidad y la teoría de Aczelha sido interpretado en teorías tipo Martin-Löf , como se describe a continuación. De esta manera, los teoremas de la teoría de conjuntos demostrables eny las teorías más débiles son candidatas a una realización informática. Más recientemente, se han introducido modelos de preheaf para teorías de conjuntos constructivos. Estos son análogos a los modelos de Presheaf inéditos para la teoría de conjuntos intuicionista desarrollados por Dana Scott en la década de 1980. [1] [2]
Descripción general
El tema de la teoría de conjuntos constructiva iniciado por el trabajo de John Myhill sobre lateoría de conjuntos, una teoría de varios tipos y cuantificación limitada, cuyo objetivo es proporcionar una base formal para el programa de matemáticas constructivas de Errett Bishop . A continuación, enumeramos una secuencia de teorías en el mismo idioma que, lo que conduce al bien estudiado constructivo Zermelo-Fraenkel de Peter Aczel , [3] y más allá. también se caracteriza por las dos características presentes también en la teoría de Myhill: por un lado, está utilizando la Separación Predicativa en lugar del esquema de Separación completo e ilimitado. La delimitación puede manejarse como una propiedad sintáctica o, alternativamente, las teorías pueden extenderse de forma conservadora con un predicado de limitación superior y sus axiomas. En segundo lugar, se descarta el axioma impredicativo de Powerset , generalmente a favor de axiomas relacionados pero más débiles. La forma fuerte se usa de manera muy casual en la topología general clásica . Las teorías constructivas también vienen con requisitos más estrictos sobre qué conjuntos constituyen una función. Añadiendo a una teoría incluso más débil que recupera , como se detalla a continuación. El sistema, que ha llegado a conocerse como teoría de conjuntos intuicionista de Zermelo-Fraenkel,, es una teoría de conjuntos sólida sin . Esto es similar a, pero menos conservador o predicativo . La teoría denotada es la versión constructiva de , la clásica teoría de conjuntos de Kripke-Platek donde incluso el axioma de colección está limitado.
Subteorías de ZF
En esta sección discutimos candidatos a axiomas comunes que crean marcos en los que todas las pruebas son también pruebas en .
Notación
A continuación usamos el griego como una variable de predicado en esquemas de axioma y uso o para predicados particulares.
Los cuantificadores van por encima del conjunto y se indican con letras minúsculas. Como es común en el estudio de la teoría de conjuntos, se utiliza la notación del constructor de conjuntos para las clases , que, en la mayoría de los contextos, no forman parte del lenguaje de objetos, pero se utilizan para una discusión concisa. En particular, se pueden introducir declaraciones de notación de la clase correspondiente a través de "", con el fin de expresar como . Se pueden usar predicados lógicamente equivalentes para introducir la misma clase. También se escribe como abreviatura de .
Como es común, podemos abreviar por y expresar el reclamo de subclase , es decir , por . Para una propiedad, trivialmente . Y así sigue que.
Tenga en cuenta que en una interpretación constructiva, los elementos de una subclase de pueden venir equipados con más información que las de . Tambien como puede no ser decidible para todos los elementos en , las dos clases son a priori para ser distinguidas.
Axiomas comunes
Empezamos con axiomas que virtualmente siempre se consideran indiscutibles y que forman parte de todas las teorías consideradas en este artículo.
Denotamos por la declaración que expresa que dos clases tienen exactamente los mismos elementos, es decir , o equivalente .
El siguiente axioma da un medio para demostrar la igualdad ""de dos conjuntos, de modo que a través de la sustitución, cualquier predicado sobre se traduce en uno de .
|
Por las propiedades lógicas de la igualdad, la dirección inversa se mantiene automáticamente.
Considere una propiedad que se aplica a todos los elementos de un conjunto , así que eso y suponga que la clase del lado izquierdo se establece como un conjunto. Tenga en cuenta que, incluso si este conjunto de la izquierda también se relaciona informalmente con información relevante para la prueba sobre la validez de para todos los elementos, el axioma de extensionalidad postula que, en nuestra teoría de conjuntos, el conjunto del lado izquierdo se considera igual al del lado derecho.
Las teorías de tipos modernas pueden, en cambio, apuntar a definir la equivalencia exigida "En términos de funciones, véase, por ejemplo, equivalencia de tipos . El concepto relacionado de extensionalidad de funciones a menudo no se adopta en la teoría de tipos. Otros marcos para las matemáticas constructivas podrían exigir en cambio una regla particular para la igualdad o la separación con todos y cada uno de los conjuntos.
|
y
|
Los dos axiomas también pueden formularse con más fuerza en términos de "", por ejemplo, en el contexto de Esto no es necesario.
Juntos, estos dos axiomas implican la existencia de la unión binaria de dos clases y cuando se han establecido para ser conjuntos, y esto se denota o . Definir la notación de clase para elementos finitos mediante disyunciones (p. Ej. dice ) y definir el conjunto sucesor como . Una especie de mezcla entre emparejamiento y unión, un axioma que se relaciona más fácilmente con el sucesor es el axioma de adjunción . Es relevante para el modelado estándar de ordinales de Neumann individuales . Este axioma también sería aceptado fácilmente, pero no es relevante en el contexto de axiomas más fuertes a continuación. Denotamos porel modelo de par ordenado estándar.
La propiedad que es falsa para cualquier conjunto corresponde a la clase vacía, denotada por o . Que este es un conjunto se sigue fácilmente de otros axiomas, como el Axioma del Infinito a continuación. Pero si, por ejemplo, uno está explícitamente interesado en excluir conjuntos infinitos en su estudio, uno puede en este punto adoptar la
Conjunto vacio |
BCST
A continuación, haremos uso de esquemas de axiomas , es decir, postularemos axiomas para alguna colección de predicados. Tenga en cuenta que algunos de los esquemas de axiomas establecidos a menudo se presentan con parámetros establecidos también, es decir, variantes con cierres universales adicionales tal que el puede depender de los parámetros.
Teoría de conjuntos constructiva básica consta de varios axiomas que también forman parte de la teoría de conjuntos estándar, excepto que el axioma de separación se debilita. Más allá de los tres axiomas anteriores, adopta el
Esquema de axioma de separación predicativa : para cualquier predicado acotado con no libre en eso, |
también llamada Separación acotada , es decir, la Separación solo para cuantificadores acotados. Esto equivale a postular la existencia de un conjunto obtenido por la intersección de cualquier conjunto y cualquier clase descrita predicativamente . Cuando el predicado se toma como por demostrado ser un conjunto, uno obtiene la intersección binaria de conjuntos y escribe .
La restricción en el axioma también es el mantenimiento de definiciones impredicativas . Por ejemplo, sin el Axioma de poder establecido , uno no debe esperar una clase definido como ser un set, donde denota algún predicado 2-ario. Tenga en cuenta que si esta subclase es probablemente un conjunto, entonces el término así definida también está en el alcance del término variable utilizado para definirlo.
Si bien, de esta manera, la Separación predicativa conduce a que se establezcan menos definiciones de clases dadas, se debe enfatizar que muchas definiciones de clases que son clásicamente equivalentes no lo son cuando se restringe a la lógica constructiva. Así, de esta manera, se obtiene una teoría de conjuntos más rica de manera constructiva. Debido a la indecidibilidad potencial de los predicados generales, la noción de subconjunto es mucho más elaborada en las teorías de conjuntos constructivos que en las clásicas, como veremos.
Como se señaló, a partir de la Separación y la existencia de cualquier conjunto (por ejemplo, Infinito a continuación) y el predicado que es falso de cualquier conjunto seguirá la existencia del conjunto vacío.
En virtud del teorema puramente lógico , La construcción de Russel muestra que la Separación Predicativa por sí sola implica que. En particular, no existe un conjunto universal .
A continuación, consideramos el
Esquema axiomático de reemplazo : para cualquier predicado, |
dónde denota existencia única. Es otorgar la existencia, como conjuntos, del rango de predicados similares a funciones, obtenidos a través de sus dominios.
Con el esquema de Reemplazo, esta teoría prueba que las clases de equivalencia o sumas indexadas son conjuntos. En particular, el producto cartesiano , que contiene todos los pares de elementos de dos conjuntos, es un conjunto.
El reemplazo y el axioma de inducción de conjuntos (presentado a continuación) son suficientes para axiomizar conjuntos finitos hereditariamente de manera constructiva y esa teoría también se estudia sin Infinito. Para comparar, considere la teoría clásica muy débil llamada teoría general de conjuntos que interpreta la clase de números naturales y su aritmética a través de solo extensionalidad, adjunción y separación completa. Solo al asumir ¿Reemplazo ya implica Separación total?
En , el Reemplazo es principalmente importante para probar la existencia de conjuntos de alto rango , es decir, a través de instancias del esquema de axioma donde se relaciona conjunto relativamente pequeño a los más grandes, .
Las teorías de conjuntos constructivos comúnmente tienen un esquema de Axioma de reemplazo, a veces restringido a fórmulas acotadas. Sin embargo, cuando se eliminan otros axiomas, este esquema a menudo se refuerza, no más allá de, sino simplemente para recuperar algo de fuerza demostrable.
Dentro de este contexto conservador de , el esquema de Separación acotada es en realidad equivalente a Conjunto vacío más la existencia de la intersección binaria para dos conjuntos cualesquiera. La última variante de axiomatización no utiliza un esquema.
Funciones
Naturalmente, el significado lógico de las afirmaciones de existencia es un tema de interés en la lógica intuicionista. El cálculo de prueba de una teoría constructiva de enunciados como
podría configurarse en términos de programas en dominios representados y posiblemente tener que ser testigo del reclamo (en el sentido de, informalmente hablando, , dónde denota el valor de un programa como se mencionó, pero esto entra en cuestiones de teoría de la realizabilidad ). Ahora, en la discusión actual, queremos hablar de una relación funcional total cuando probablemente
- ,
lo que, en particular, implica un cuantificador existencial. También se han definido variantes de la definición de predicado funcional que utilizan relaciones de separación en setoides .
Dejar (también escrito ) denotan la clase de tales funciones de conjunto. Cuando las funciones se entienden simplemente como gráficas de funciones como arriba, la proposición de pertenencia también está escrito .
Escribir por . Dado cualquier, ahora se nos lleva a razonar sobre clases como
Las funciones características con valores booleanos se encuentran entre esas clases, que pueden considerarse correspondientes a funciones de terminación. Pero ten en cuenta que puede no ser decidible.
Usando la terminología de clase estándar, uno puede hacer uso de funciones libremente, dado que su dominio es un conjunto. Las funciones en su conjunto se establecerán si su codominio es.
ECST
Denotamos por la propiedad inductiva, p. ej. . En términos de un predicado subordinado de la clase, esto se traduciría como . Tenga en cuenta quedenota una variable de conjunto genérica aquí. Escribir por . Definir una clase.
Para algún predicado fijo , la declaración expresa que es el conjunto más pequeño de todos los conjuntos para cual se mantiene cierto. La teoría de conjuntos constructiva elemental tiene el axioma de así como
Infinito fuerte |
El segundo conjunto cuantificado universalmente expresa inducción matemática para todos en el universo del discurso, es decir, para conjuntos. De esta manera, los principios discutidos en esta sección brindan medios para probar que algunos predicados son válidos al menos para todos los elementos de. Tenga en cuenta que incluso el axioma relativamente fuerte de la inducción matemática completa (inducción para cualquier predicado, discutido a continuación) también puede adoptarse y usarse sin postular nunca que forma un conjunto.
Se pueden formular formas débiles de axiomas de infinito, todas postulando que existe algún conjunto con las propiedades comunes de los números naturales. Entonces se puede usar la Separación completa para obtener el conjunto "disperso", el conjunto de números naturales. En el contexto de sistemas de axiomas por lo demás más débiles, un axioma de infinito debe fortalecerse para implicar la existencia de un conjunto tan disperso por sí solo. Una forma más débil de Infinity lee
que también se puede escribir de manera más concisa usando . El conjunto así postulado para existir se denota generalmente por, el ordinal infinito de von Neumann más pequeño . Para elementos de este conjunto, el reclamo es decidible.
Con este, prueba la inducción para todos los predicados dados por fórmulas acotadas. Los dos de los cinco axiomas de Peano con respecto a y uno sobre el cierre de con respecto a se siguen bastante directamente de los axiomas del infinito. Finalmente, puede demostrarse que es una operación inyectiva.
Elección
Ser finito significa que hay una función biyectiva en lo natural. Ser subfinito significa ser un subconjunto de un conjunto finito. La afirmación de que ser un conjunto finito es equivalente a ser subfinito es equivalente a.
Si , podemos formar el conjunto de relaciones de uno a muchos . El axioma de elección contable concedería que siempre que, podemos formar una función mapeando cada número a un valor único. La elección contable está implícita en el axioma más general de elección dependiente . Esto, a su vez, está implícito en el axioma de elección relativo a funciones en dominios generales.
Concluimos con un comentario para resaltar la fuerza de la elección y su relación con cuestiones de Intencionalidad . Considere los conjuntos subfinitos
Aquí el axioma de elección completo, otorgando la existencia de un mapa en elementos distinguibles (la igualdad en el codominio es decidible), implica que . Entonces, la afirmación de existencia de la elección general funciona con no es constructivo.
Para comprender mejor este fenómeno, tenga en cuenta que los conjuntos y son tan contingentes como los predicados involucrados en su definición. La diferencia entre el codominio discreto de algunos números naturales y el dominioradica en el hecho de que a priori se sabe poco sobre estos últimos. Ahora considere casos de implicaciones lógicas como. Tenemos y , a pesar de . Pero en el caso de, como implica , hay extensionalmente solo una entrada de función posible a una función de elección de elección, ahora solo . Entonces, al considerar la asignación funcional, luego declarando incondicionalmente no sería consistente. De esta manera, el axioma de separación vincula los predicados para establecer la igualdad y, a su vez, a la información sobre las funciones.
Aritmética
En , se pueden probar muchos enunciados por conjunto individual (a diferencia de las expresiones que involucran un cuantificador universal, como por ejemplo, disponible con un axioma de inducción) y los objetos de interés matemático se pueden utilizar a nivel de clase en bases individuales. Como tales, los axiomas enumerados hasta ahora son suficientes como teoría de trabajo para una buena parte de las matemáticas básicas.
Sin embargo, la teoría aún no interpreta la recursividad primitiva completa . De hecho, a pesar de tener el axioma de Reemplazo, la teoría aún no prueba que la adición sea una función establecida. Con este fin, se debe agregar el axioma que otorga la definición de funciones de conjunto a través de funciones de conjunto de pasos de iteración. Nos gustaría que una teoría interpretara la aritmética de Peano o, más precisamente, la aritmética de Heyting , es decir, las cuatro reglas relativas a la suma y la multiplicación. Lo que es necesario para esto es un principio de iteración que es el equivalente teórico establecido de un objeto de números naturales . El principio está implícito al suponer que la clase de funciones
en dominios finitos en conjuntos la forma se establece a sí misma. Este, a su vez, es un caso especial del axioma de exponenciación a continuación. El uso de esos axiomas se deriva del hecho de que los espacios de funciones al ser conjuntos significa que la cuantificación de sus funciones es una noción acotada, que permite el uso de Separación. Sin embargo, el principio de inducción obtenido de esta manera no prueba una inducción matemática completa para todos los predicados.
Sin embargo, con esta aritmética acotada dada en , aritmética de números racionales Entonces también se puede definir y probar sus propiedades, como la unicidad y la contabilidad.
Exponenciación
Ya consideramos una forma debilitada del esquema de Separación, y más del estándar los axiomas se debilitarán para una teoría más predicativa y constructiva. El primero de ellos es el axioma de Powerset , que, de hecho, adoptamos para subconjuntos decidibles. La caracterización de la clase de todos los subconjuntos de un conjunto implica cuantificación universal ilimitada, a saber . Aquí se ha definido en términos del predicado de pertenencia sobre. Entonces, en tal marco teórico establecido, la clase de poder no se define en una construcción de abajo hacia arriba a partir de sus constituyentes (como un algoritmo en una lista, por ejemplo,) sino a través de una comprensión de todos los conjuntos. La-funciones valoradas en un conjunto inyectar en y por tanto corresponden a sus subconjuntos decidibles.
Ahora consideramos el axioma :
Exponenciación |
En palabras, los axiomas dicen que dados dos conjuntos , la clase de todas las funciones es, de hecho, también un conjunto. Ciertamente, tales implicaciones son necesarias, por ejemplo, para formalizar el mapa de objetos de un hom-functor interno como.
Para cualquier fórmula , la clase es igual a Cuándo puede ser rechazado y Cuándo puede ser probado, pero también puede no ser decidible en absoluto. En este punto de vista, la clase de poder del singleton, es decir o informalmente y generalmente denotado por , se llama álgebra de valores de verdad. Suponiendo que todas las fórmulas son decidibles, es decir, asumiendo, se puede demostrar no solo que es un conjunto, pero más concretamente que es este conjunto de dos elementos. Asumiendopara fórmulas limitadas, Separación permite demostrar que cualquier clase de potencia es un conjunto. Alternativamente, Powerset completo es equivalente a simplemente asumir que la clase de todos los subconjuntos deforma un conjunto. La separación completa equivale a suponer que cada subclase de es un conjunto.
Entonces, en este contexto, los espacios funcionales son más accesibles que las clases de subconjuntos , como es el caso de los objetos exponenciales resp. subobjetos en la teoría de categorías. En teoría de tipos, la expresión ""existe por sí mismo y denota espacios de función , una noción primitiva. Estas clases aparecen naturalmente, por ejemplo, como el tipo de biyección curry entre y , un complemento . Las teorías de conjuntos constructivos también se estudian en el contexto de axiomas aplicativos . En términos teóricos de categoría , la teoríacorresponde esencialmente a una forma constructiva así puntas cartesiano cerrado Heyting pre toposes con (siempre que se adoptó Infinity) un objeto números naturales . La existencia de powerset es lo que convertiría un pretopos de Heyting en un topos elemental . Cada uno de esos topos que interpreta es por supuesto un modelo de estas teorías más débiles, pero localmente se han definido pretopos cerrados cartesianos que, por ejemplo, interpretan pero rechace la Separación completa y el Powerset.
La exponenciación no implica una inducción matemática completa.
Hacia los Reales
Como se mencionó, la exponenciación implica principios de recursividad y así en , se puede razonar sobre secuencias o acerca de la reducción de intervalos en y esto también permite hablar de secuencias de Cauchy y su aritmética. Cualquier número real de Cauchy es una colección de secuencias, es decir, un subconjunto de un conjunto de funciones en. Se requieren más axiomas para garantizar siempre la integridad de las clases de equivalencia de tales secuencias y es necesario postular principios sólidos para implicar la existencia de un módulo de convergencia para todas las secuencias de Cauchy. La elección contable débil es generalmente el contexto para demostrar la unicidad de los reales de Cauchy como campo completo (pseudo) ordenado. "Pseudo-" aquí destaca que el orden, en cualquier caso, no siempre será decidible de manera constructiva.
Como en la teoría clásica, los cortes de Dedekind se caracterizan utilizando subconjuntos de estructuras algebraicas como: Las propiedades del ser están habitadas, numéricamente limitadas arriba, "cerradas hacia abajo" y "abiertas hacia arriba" son todas fórmulas acotadas con respecto al conjunto dado que subyace a la estructura algebraica. Un ejemplo estándar de un corte, el primer componente de hecho exhibe estas propiedades, es la representación de dada por
(Dependiendo de la convención para cortes, cualquiera de las dos partes o ninguna, como aquí, puede hacer uso del signo .)
La teoría dada por los axiomas hasta ahora valida que un campo pseudoordenado que también es completo de Arquímedes y Dedekind , si es que existe, se caracteriza de esta manera de manera única, hasta el isomorfismo. Sin embargo, la existencia de solo espacios funcionales como no concede ser un conjunto, por lo que tampoco lo es la clase de todos los subconjuntos de que cumplen con las propiedades nombradas. Lo que se requiere para que la clase de reales de Dedekind sea un conjunto es un axioma con respecto a la existencia de un conjunto de subconjuntos.
En cualquiera de los casos, un menor número de declaraciones sobre la aritmética de los números reales son decidible , en comparación con la teoría clásica.
Inducción
Inducción matemática
El principio de iteración para las funciones de conjunto mencionado anteriormente también está implícito en la inducción completa sobre la estructura de uno modelando los naturales (p. Ej. ). Lecturas de inducciónpara cualquier clase. A menudo se formula directamente en términos de predicados.
Esquema de axioma de inducción matemática completa : para cualquier predicado en , |
Aquí denota y el set denota el conjunto sucesor de , con . Por Axiom of Infinity arriba, es nuevamente un miembro de.
El axioma de inducción está implícito en el esquema de Separación completo. Se puede ver que se relaciona con él, ya que la inducción conduce a una conclusión sobre la clase..
Los principios de inducción también están implícitos en varias formas de principios de elección. Aproximadamente, las formulaciones del axioma de elección dependiente en términos de predicados binarios en algún nivel de la jerarquía (de nuevo, solo se pueden considerar fórmulas acotadas) pueden usarse para probar la inducción matemática para predicados en ese nivel.
Nótese que en el programa de Aritmética Predicativa , incluso el esquema de inducción matemática ha sido criticado por ser posiblemente impredicativo, cuando los números naturales se definen como el objeto que cumple este esquema.
Establecer inducción
Inducción de conjunto completo en demuestra una inducción matemática completa sobre los números naturales. De hecho, da inducción sobre ordinales y aritmética ordinal. No se requiere reemplazo para probar la inducción sobre el conjunto de naturales, pero sí lo es para su aritmética modelada dentro de la teoría de conjuntos.
El Axioma luego dice lo siguiente
Esquema de axioma de inducción de conjuntos : para cualquier predicado, |
Tenga en cuenta que se sostiene trivialmente y corresponde al "caso inferior" en el marco estándar. La variante del Axioma solo para fórmulas acotadas también se estudia de forma independiente y puede derivarse de otros axiomas.
El axioma de regularidad junto con la separación (acotada) implica la inducción de conjuntos pero también (acotada), por lo que la regularidad no es constructiva. En cambio, junto con la inducción de conjuntos implica regularidad.
Metalogic
Esto ahora cubre variantes de los ocho axiomas de Zermeolo-Freankel. La extensionalidad, el emparejamiento, la unión y el reemplazo son de hecho idénticos. Infinity se expresa en una formulación fuerte e implica Emty Set, como en el caso clásico. La separación, clásicamente declarada de forma redundante, no está implícita de manera constructiva en Reemplazo. Sin la Ley del Medio Excluido , la teoría aquí carece de Separación completa, Powerset y Regularidad en su forma común.
La teoría no es más fuerte que la aritmética de Heyting, pero sumaen esta etapa conduciría a una teoría más allá de la fuerza de la teoría de tipos típica : asumir la separación en forma irrestricta, luego agregar a da una teoría que demuestra los mismos teoremas que menos Regularidad! Por lo tanto, agregando a ese marco da y agregarle Elección da .
La fuerza teórica de la prueba adicional obtenida con la inducción en el contexto constructivo es significativa, incluso si se elimina la regularidad en el contexto de no reduce la fuerza teórica de la prueba. Tenga en cuenta que Aczel también fue uno de los principales desarrolladores de la teoría de conjuntos no bien fundada , que rechaza este último axioma.
Colección fuerte
Con todos los axiomas debilitados de y ahora yendo más allá de esos axiomas también vistos en el enfoque mecanografiado de Myhill, la teoría llamada (una teoría con exponenciación) fortalece el esquema de colección de la siguiente manera:
Esquema axiomático de Strong Collection: para cualquier predicado , |
Dice que si es una relación entre conjuntos que es total sobre un determinado conjunto de dominios (es decir, tiene al menos un valor de imagen para cada elemento del dominio), entonces existe un conjunto que contiene al menos una imagen debajo de cada elemento del dominio. Y esta formulación afirma además que sólo tales imágenes de elementos del dominio. La última cláusula hace que el axioma, en este contexto constructivo, sea más fuerte que la formulación estándar de Colección. Está garantizando que no sobrepasa el codominio de y así el axioma expresa algún poder de un procedimiento de Separación.
El axioma es una alternativa al esquema de Reemplazo y de hecho lo reemplaza, debido a que no requiere que la definición de relación binaria sea funcional.
Por regla general, las cuestiones de cardinalidad moderada son más sutiles en un entorno constructivo. Como la aritmética está bien disponible en, la teoría tiene productos dependientes, prueba que la clase de todos los subconjuntos de números naturales no puede ser subcontable y también prueba que las uniones contables de los espacios funcionales de los conjuntos contables siguen siendo contables.
Metalogic
Esta teoría sin , separación ilimitada y "ingenuo" Power set disfruta de varias propiedades agradables. Por ejemplo, tiene la propiedad de existencia : si, para cualquier propiedad, la teoría prueba que existe un conjunto que tiene esa propiedad, es decir, si la teoría prueba el enunciado , entonces también hay una propiedad que describe de forma única una instancia de conjunto de este tipo. Es decir, la teoría también prueba. Esto se puede comparar con la aritmética de Heyting, donde los teoremas se realizan mediante números naturales concretos y tienen estas propiedades. En la teoría de conjuntos, el papel lo desempeñan los conjuntos definidos. Por el contrario, recuerde que en, el axioma de elección implica el teorema del buen orden , de modo que los ordenamientos totales con el mínimo elemento para conjuntos como se ha demostrado formalmente que existen, incluso si es probable que no se pueda describir tal ordenamiento.
Constructivo Zermelo – Fraenkel
Se puede acercar más al conjunto de poder sin perder una interpretación teórica de tipo. La teoría conocida como es más una forma más fuerte de exponenciación. Es adoptando la siguiente alternativa, que nuevamente puede verse como una versión constructiva del axioma de Power set :
Esquema de axioma de la colección de subconjuntos: para cualquier predicado , |
Este esquema de axioma de la colección de subconjuntos es equivalente a un axioma alternativo de plenitud único y algo más claro. Con este fin, dejemoses la clase de todas las relaciones totales entre una y b , esta clase se da como
Con esto, podemos afirmar , una alternativa a la colección de subconjuntos. Garantiza que existe al menos algún conjuntomanteniendo una buena cantidad de las relaciones deseadas. Más concretamente, entre dos conjuntos cualesquiera y , hay un conjunto que contiene una subrelación total para cualquier relación total de a .
- Axioma de plenitud:
El axioma de Plenitud está a su vez implícito en el llamado Axioma de Presentación sobre secciones, que también se puede formular categoría teóricamente .
La plenitud implica la propiedad de refinamiento binario necesaria para demostrar que la clase de cortes de Dedekind es un conjunto. Esto no requiere inducción o recolección.
En esta teoría no se pueden derivar ni la linealidad de los ordinales ni la existencia de conjuntos de potencia de conjuntos finitos. Asumir cualquiera implica Poder en este contexto.
Metalogic
Esta teoría carece de la propiedad de existencia debida al esquema, pero en 1977 Aczel demostró que todavía se puede interpretar en la teoría de tipos de Martin-Löf , [4] (utilizando el enfoque de proposiciones como tipos ) proporcionando lo que ahora se ve un modelo estándar deen teoría de tipos. [5] Esto se hace en términos de imágenes de sus funciones, así como una justificación constructiva y predicativa bastante directa, mientras se conserva el lenguaje de la teoría de conjuntos. Como tal, tiene una modesta fuerza teórica de la prueba, ver I K PAG {\ Displaystyle {\ mathsf {IKP}}} : Ordinal de Bachmann-Howard .
Rompiendo con ZF
Se puede agregar además el axioma no clásico de que todos los conjuntos son subcontables . Luego es un conjunto (por infinito y exponenciación) mientras que la clase o incluso Probablemente no es un conjunto, según el argumento diagonal de Cantor. Entonces, esta teoría rechaza lógicamente a Powerset y.
En 1989 Ingrid Lindström demostró que los conjuntos no bien fundados obtenidos al reemplazar el equivalente del Axioma de Fundación (Inducción) encon el axioma anti-fundación de Aczel () también se puede interpretar en la teoría de tipos de Martin-Löf. [6]
Zermelo-Fraenkel intuicionista
La teoría es con el conjunto estándar de separación y potencia .
Aquí, en lugar del esquema Axiom de reemplazo , podemos usar el
Esquema de axioma de colección : para cualquier predicado, |
Mientras que el axioma de reemplazo requiere la relación ser funcional sobre el set (como en, para cada en hay asociado exactamente uno ), el axioma de colección no lo hace. Simplemente requiere que haya asociado al menos una, y afirma la existencia de un conjunto que recopila al menos uno de esos para cada uno de esos . junto con la Colección implica Reemplazo.
Como tal, puede verse como la variante más sencilla de sin .
Metalogic
Cambiando el esquema de Axioma de Reemplazo al esquema de Axioma de Colección, la teoría resultante tiene la Propiedad de Existencia .
Incluso sin , la fuerza teórica de la prueba de es igual a la de .
Tiempo se basa en la lógica intuicionista más que en la clásica, se considera impredicativo . Permite la formación de conjuntos utilizando el axioma de separación con cualquier proposición, incluidos los que contienen cuantificadores que no están acotados. Por tanto, se pueden formar nuevos conjuntos en términos del universo de todos los conjuntos. Además, el axioma del conjunto de poder implica la existencia de un conjunto de valores de verdad . En presencia del medio excluido, este conjunto existe y tiene dos elementos. En ausencia de él, el conjunto de valores de verdad también se considera impredicativo.
Historia
En 1973, John Myhill propuso un sistema de teoría de conjuntos basado en la lógica intuicionista [7] tomando la base más común,, y desechando el axioma de la elección y la ley del medio excluido , dejando todo lo demás como está. Sin embargo, diferentes formas de algunas de las axiomas que son equivalentes en el escenario clásico no son equivalentes en el escenario constructivo, y algunas formas implican . En esos casos, las formulaciones intuicionísticamente más débiles se adoptaron para la teoría de conjuntos constructiva.
Z intuicionista
Nuevamente en el extremo más débil, como con su contraparte histórica de la teoría de conjuntos de Zermelo , uno puede denotar por la teoría intuicionista establecida como pero sin Reemplazo, Recolección o Inducción.
KP intuicionista
Mencionemos otra teoría muy débil que ha sido investigada, a saber, la teoría de conjuntos intuicionista (o constructiva) de Kripke-Platek. . La teoría no solo tiene la Separación sino también la Colección restringida, es decir, es similar apero con inducción en lugar de reemplazo completo. Es especialmente débil cuando se estudia sin Infinity. La teoría no encaja en la jerarquía presentada anteriormente, simplemente porque tiene el esquema Axiom de Inducción de conjuntos desde el principio. Esto permite teoremas que involucran la clase de ordinales.
Teorías ordenadas
Teoría de conjuntos constructiva
Tal como lo presentó, el sistema de Myhill es una lógica constructiva de primer orden con identidad y tres tipos , a saber, conjuntos, números naturales , funciones :
- El axioma de extensionalidad habitual para conjuntos, así como uno para funciones, y el axioma habitual de unión .
- El axioma de separación restringida o predicativa, que es una forma debilitada del axioma de separación en la teoría de conjuntos clásica, que requiere que cualquier cuantificación esté limitada a otro conjunto.
- Una forma del axioma del infinito que afirma que la colección de números naturales (para la que introduce una constante) es de hecho un conjunto.
- El axioma de exponenciación , afirmando que para dos conjuntos cualesquiera, hay un tercer conjunto que contiene todas (y sólo) las funciones cuyo dominio es el primer conjunto y cuyo rango es el segundo conjunto. Ésta es una forma muy debilitada del axioma de poder establecido en la teoría de conjuntos clásica, a la que Myhill, entre otros, objetó sobre la base de su impredicatividad .
- Un axioma de elección dependiente , que es mucho más débil que el axioma de elección habitual .
Y además:
- Los axiomas habituales de Peano para los números naturales.
- Axiomas que afirman que el dominio y el rango de una función son ambos conjuntos. Además, un axioma de no elección afirma la existencia de una función de elección en los casos en que la elección ya está hecha. Juntos, estos actúan como el axioma de reemplazo habitual en la teoría de conjuntos clásica.
Teoría de conjuntos del estilo Bishop
La teoría de conjuntos en el sabor de la escuela constructivista de Errett Bishop refleja la de Myhill, pero está configurada de una manera que los conjuntos vienen equipados con relaciones que gobiernan su discreción. Comúnmente, se adopta la elección dependiente.
Teorías de categorías
No todas las teorías lógicas formales de conjuntos necesitan axiomizar el predicado de pertenencia binaria ""directamente. Y una teoría elemental de las categorías de conjunto (), por ejemplo, capturar pares de asignaciones componibles entre objetos, también se puede expresar con una lógica de fondo constructiva ().
Los buenos modelos de teorías de conjuntos constructivos en la teoría de categorías son los pretopos mencionados en la sección Exponenciación, que posiblemente también requieran suficientes proyectivos , un axioma sobre las "presentaciones" sobreyectivas de conjuntos, que implica la elección dependiente contable.
Más allá de eso, los topoi también tienen lenguajes internos que pueden ser intuicionistas y capturar una noción de conjuntos .
Ver también
- Matemáticas constructivas
- Teoría de tipos intuicionistas
- Análisis ordinal
- La impredicatividad
- Propiedad de existencia
- Ley del medio excluido
- Responsabilidad
Referencias
- ^ Gambino, N. (2005). "MODELOS PREPESADOS PARA TEORÍAS DE CONJUNTOS CONSTRUCTIVOS" (PDF) . En Laura Crosilla y Peter Schuster (ed.). De conjuntos y tipos a topología y análisis (PDF) . págs. 62–96. doi : 10.1093 / acprof: oso / 9780198566519.003.0004 . ISBN 9780198566519.
- ^ Scott, DS (1985). Modelos teóricos de categorías para la teoría intuicionista de conjuntos. Diapositivas del manuscrito de una charla impartida en la Universidad Carnegie-Mellon
- ^ Peter Aczel y Michael Rathjen, Notas sobre la teoría de conjuntos constructivos , Informes Institut Mittag-Leffler, Lógica matemática - 2000/2001, No. 40
- ^ Aczel, Peter: 1978. La interpretación teórica de tipos de la teoría de conjuntos constructiva. En: A. MacIntyre et al. (eds.), Logic Colloquium '77, Amsterdam: North-Holland, 55–66.
- ^ Rathjen, M. (2004), "Predicativity, Circularity, and Anti-Foundation" (PDF) , en Link, Godehard (ed.), Cien años de la paradoja de Russell: Matemáticas, lógica, filosofía , Walter de Gruyter, ISBN 978-3-11-019968-0
- ^ Lindström, Ingrid: 1989. Una construcción de conjuntos no bien fundamentados dentro de la teoría de tipos de Martin-Löf . Journal of Symbolic Logic 54: 57–64.
- ^ Myhill, " Algunas propiedades de la teoría de conjuntos intuicionista de Zermelo-Fraenkel " , Actas de la Escuela de verano de Cambridge de 1971 en lógica matemática (Notas de conferencia en matemáticas 337) (1973) pp 206-231
Otras lecturas
- Troelstra, Anne ; van Dalen, Dirk (1988). Constructivismo en matemáticas, vol. 2 . Estudios de Lógica y Fundamentos de las Matemáticas. pag. 619 . ISBN 978-0-444-70358-3.
- Aczel, P. y Rathjen, M. (2001). Notas sobre la teoría de conjuntos constructiva . Informe técnico 40, 2000/2001. Instituto Mittag-Leffler, Suecia.
enlaces externos
- Laura Crosilla, Teoría de conjuntos: ZF constructiva e intuicionista , Enciclopedia de filosofía de Stanford , 20 de febrero de 2009
- Benno van den Berg, Teoría de conjuntos constructiva: una descripción general , diapositivas de Heyting dag, Ámsterdam, 7 de septiembre de 2012