Teoría de conjuntos constructivos

Axiomatic set theories based on the principles of mathematical constructivism

La teoría axiomática de conjuntos constructivos es un enfoque del constructivismo matemático que sigue el programa de la teoría axiomática de conjuntos . Se suele utilizar el mismo lenguaje de primer orden con " " y " " de la teoría clásica de conjuntos, por lo que no debe confundirse con un enfoque de tipos constructivos . Por otro lado, algunas teorías constructivas están motivadas de hecho por su interpretabilidad en teorías de tipos . ${\displaystyle =}$ ${\displaystyle \in }$

Además de rechazar el principio del tercero excluido ( ), las teorías de conjuntos constructivos a menudo requieren que algunos cuantificadores lógicos en sus axiomas estén acotados por conjuntos . Esto último está motivado por resultados vinculados con la impredicatividad . ${\displaystyle {\mathrm {PEM} }}$

Introducción

Perspectiva constructiva

Preliminares sobre el uso de la lógica intuicionista

La lógica de las teorías de conjuntos discutidas aquí es constructiva en el sentido de que rechaza el principio del tercero excluido , es decir, que la disyunción se cumple automáticamente para todas las proposiciones . Esto también se suele llamar la ley del tercero excluido ( ) en contextos donde se asume. De manera constructiva, como regla, para probar el tercero excluido para una proposición , es decir, para probar la disyunción particular , o bien debe probarse explícitamente. Cuando se establece cualquiera de esas pruebas, se dice que la proposición es decidible, y esto entonces implica lógicamente que la disyunción se cumple. De manera similar y más comúnmente, se dice que un predicado para en un dominio es decidible cuando el enunciado más intrincado es demostrable. Los axiomas no constructivos pueden permitir pruebas que formalmente afirman la decidibilidad de tal (y/o ) en el sentido de que prueban el tercero excluido para (resp. el enunciado que usa el cuantificador anterior) sin demostrar la verdad de ninguno de los lados de la(s) disyunción(es). Este es a menudo el caso en la lógica clásica. Por el contrario, las teorías axiomáticas consideradas constructivas tienden a no permitir muchas pruebas clásicas de afirmaciones que involucran propiedades que son demostrablemente indecidibles computacionalmente . ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle \phi \lor \neg \phi }$ ${\displaystyle \phi }$ ${\displaystyle {\mathrm {LEM} }}$ ${\displaystyle P}$ ${\displaystyle P\lor \neg P}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle Q(x)}$ ${\displaystyle x}$ ${\displaystyle X}$ ${\displaystyle \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$

La ley de no contradicción es un caso especial de la forma proposicional del modus ponens . Al utilizar la primera con cualquier enunciado negado , una ley de De Morgan válida implica ya en la lógica mínima más conservadora . En palabras, la lógica intuicionista todavía postula: Es imposible descartar una proposición y descartar su negación a la vez, y por lo tanto el rechazo de cualquier enunciado tercero excluido instanciado para una proposición individual es inconsistente. Aquí la doble negación captura que el enunciado de disyunción ahora probadamente nunca puede descartarse o rechazarse, incluso en casos donde la disyunción puede no ser demostrable (por ejemplo, demostrando uno de los disyuntos, decidiendo así ) a partir de los axiomas asumidos. ${\displaystyle \neg P}$ ${\displaystyle \neg \neg (P\lor \neg P)}$ ${\displaystyle P}$

En términos más generales, las teorías matemáticas constructivas tienden a demostrar reformulaciones clásicamente equivalentes de teoremas clásicos. Por ejemplo, en el análisis constructivo no se puede demostrar el teorema del valor intermedio en su formulación de libro de texto, pero sí se pueden demostrar teoremas con contenido algorítmico que, tan pronto como se supone que la eliminación de la doble negación y sus consecuencias son legales, son de inmediato clásicamente equivalentes al enunciado clásico. La diferencia es que las demostraciones constructivas son más difíciles de encontrar.

La lógica intuicionista que subyace a las teorías de conjuntos analizadas aquí, a diferencia de la lógica mínima, todavía permite la eliminación de la doble negación para proposiciones individuales para las que se cumple el principio del tercero excluido. A su vez, las formulaciones de teoremas sobre objetos finitos tienden a no diferir de sus contrapartes clásicas. Dado un modelo de todos los números naturales, el equivalente para predicados, es decir, el principio de Markov , no se cumple automáticamente, pero puede considerarse como un principio adicional. ${\displaystyle P}$

En un dominio habitado y usando explosión , la disyunción implica la afirmación de existencia , que a su vez implica . Clásicamente, estas implicaciones son siempre reversibles. Si una de las primeras es clásicamente válida, puede valer la pena intentar establecerla en la segunda forma. Para el caso especial donde se rechaza , se trata con un contraejemplo afirmación de existencia , que generalmente es constructivamente más fuerte que una afirmación de rechazo : Ejemplificar un tal que es contradictorio significa por supuesto que no es el caso que se cumple para todos los posibles . Pero también se puede demostrar que cumplir para todos conduciría lógicamente a una contradicción sin la ayuda de un contraejemplo específico, e incluso sin poder construir uno. En el último caso, de manera constructiva, aquí no se estipula una afirmación de existencia. ${\displaystyle P\lor \exists (x\in X).\neg Q(x)}$ ${\displaystyle \exists (x\in X).(Q(x)\to P)}$ ${\displaystyle {\big (}\forall (x\in X).Q(x){\big )}\to P}$ ${\displaystyle P}$ ${\displaystyle \exists (x\in X).\neg Q(x)}$ ${\displaystyle \neg \forall (x\in X).Q(x)}$ ${\displaystyle t}$ ${\displaystyle Q(t)}$ ${\displaystyle Q}$ ${\displaystyle x}$ ${\displaystyle Q}$ ${\displaystyle x}$

Restricciones impuestas a una teoría de conjuntos

En comparación con la contraparte clásica, generalmente es menos probable probar la existencia de relaciones que no se pueden realizar. Una restricción a la lectura constructiva de la existencia a priori conduce a requisitos más estrictos con respecto a qué caracterizaciones de un conjunto que involucra colecciones ilimitadas constituyen una función (matemática, y por lo tanto siempre significando total ). Esto se debe a menudo a que el predicado en una posible definición caso por caso puede no ser decidible. Adoptando la definición estándar de igualdad de conjuntos a través de la extensionalidad, el Axioma de Elección completo es un principio no constructivo que implica para las fórmulas permitidas en el esquema de Separación adoptado, por el teorema de Diaconescu . Resultados similares se mantienen para la afirmación de existencia del Axioma de Regularidad , como se muestra a continuación. Este último tiene un sustituto inductivo clásicamente equivalente . Por lo tanto, un desarrollo genuinamente intuicionista de la teoría de conjuntos requiere la reformulación de algunos axiomas estándar a unos clásicamente equivalentes. Además de las demandas de computabilidad y las reservas sobre la calificación de la impredicatividad, ^[1] la cuestión técnica respecto de qué axiomas no lógicos extienden efectivamente la lógica subyacente de una teoría es también un tema de investigación en sí mismo. ${\displaystyle f\subset X\times Y}$ ${\displaystyle {\mathrm {PEM} }}$

Metalógica

Con proposiciones computablemente indecidibles que ya surgen en la aritmética de Robinson , incluso la simple separación predicativa permite definir subconjuntos elusivos fácilmente. En marcado contraste con el marco clásico, las teorías de conjuntos constructivos pueden cerrarse bajo la regla de que cualquier propiedad que sea decidible para todos los conjuntos ya es equivalente a una de las dos triviales, o . También la línea real puede considerarse indecomponible en este sentido. La indecidibilidad de las disyunciones también afecta las afirmaciones sobre órdenes totales como la de todos los números ordinales , expresada por la demostrabilidad y el rechazo de las cláusulas en el orden que define la disyunción . Esto determina si la relación es tricotómica . Una teoría debilitada de los ordinales afecta a su vez la fuerza teórica de la prueba definida en el análisis ordinal . ${\displaystyle \top }$ ${\displaystyle \bot }$ ${\displaystyle (\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )}$

A cambio, las teorías de conjuntos constructivos pueden exhibir propiedades atractivas de disyunción y existencia , como es familiar a partir del estudio de las teorías aritméticas constructivas. Estas son características de una teoría fija que relacionan metalógicamente los juicios de proposiciones demostrables en la teoría. Particularmente bien estudiadas son aquellas características que pueden expresarse en la aritmética de Heyting , con cuantificadores sobre números y que a menudo pueden realizarse mediante números, como se formaliza en la teoría de la prueba . En particular, esas son la propiedad de existencia numérica y la propiedad disyuntiva estrechamente relacionada, además de estar cerradas bajo la regla de Church , lo que atestigua que cualquier función dada es computable . ^[2]

Una teoría de conjuntos no sólo expresa teoremas sobre números, por lo que se puede considerar una propiedad más general llamada de existencia fuerte que es más difícil de obtener, como se discutirá más adelante. Una teoría tiene esta propiedad si se puede establecer lo siguiente: Para cualquier propiedad , si la teoría prueba que existe un conjunto que tiene esa propiedad, es decir, si la teoría afirma la declaración de existencia, entonces también hay una propiedad que describe de manera única tal instancia de conjunto. Más formalmente, para cualquier predicado hay un predicado tal que ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$

${\displaystyle {\mathsf {T}}\vdash \exists x.\phi (x)\implies {\mathsf {T}}\vdash \exists !x.\phi (x)\land \psi (x)}$

En este caso, los conjuntos definidos cuya existencia se ha demostrado por (o según) la teoría desempeñan un papel análogo al de los números realizados en aritmética. Las cuestiones relativas a la solidez de la teoría axiomática de conjuntos y su relación con la construcción de términos son sutiles. Si bien muchas teorías analizadas tienden a tener todas las diversas propiedades numéricas, la propiedad de existencia puede ser fácilmente estropeada, como se analizará más adelante. Se han formulado formas más débiles de propiedades de existencia.

Algunas teorías con una lectura clásica de la existencia pueden, de hecho, también restringirse para exhibir la propiedad de existencia fuerte. En la teoría de conjuntos de Zermelo-Fraenkel, con conjuntos que se toman como definibles ordinalmente , una teoría denotada , no existen conjuntos sin tal definibilidad. La propiedad también se aplica mediante el postulado del universo construible en . En contraste, considere la teoría dada por más el postulado completo del axioma de elección de existencia : Recuerde que esta colección de axiomas prueba el teorema de buen ordenamiento , lo que implica que existen buenos ordenamientos para cualquier conjunto. En particular, esto significa que existen relaciones formalmente que establecen el buen ordenamiento de (es decir, la teoría afirma la existencia de un elemento mínimo para todos los subconjuntos de con respecto a esas relaciones). Esto es a pesar del hecho de que se sabe que la definibilidad de tal ordenamiento es independiente de . Esto último implica que para ninguna fórmula particular en el lenguaje de la teoría, la teoría prueba que el conjunto correspondiente es una relación de buen ordenamiento de los reales. Por lo tanto, se prueba formalmente la existencia de un subconjunto con la propiedad de ser una relación de buen ordenamiento, pero al mismo tiempo no es posible definir ningún conjunto particular para el cual se pueda validar la propiedad. ${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {HOD} })}$ ${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {L} })}$ ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$ ${\displaystyle {\mathbb {R} }}$ ${\displaystyle {\mathbb {R} }}$ ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle \psi }$ ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$ ${\displaystyle W}$

Principios anticlásicos

Como se mencionó anteriormente, una teoría constructiva puede exhibir la propiedad de existencia numérica, , para algún número y donde denota el numeral correspondiente en la teoría formal. Aquí uno debe distinguir cuidadosamente entre implicaciones demostrables entre dos proposiciones, , y las propiedades de una teoría de la forma . Cuando se adopta un esquema metalógicamente establecido del último tipo como regla de inferencia de un cálculo de prueba y no se puede demostrar nada nuevo, uno dice que la teoría está cerrada bajo esa regla. ${\displaystyle {\mathsf {T}}}$ ${\displaystyle {\mathsf {T}}\vdash \exists e.\psi (e)\implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$ ${\displaystyle {\mathrm {e} }}$ ${\displaystyle {\underline {\mathrm {e} }}}$ ${\displaystyle {\mathsf {T}}\vdash P\to Q}$ ${\displaystyle {\mathsf {T}}\vdash P\implies {\mathsf {T}}\vdash Q}$ ${\displaystyle {\mathsf {T}}}$

En cambio, se puede considerar la anexión de la regla correspondiente a la propiedad metateórica como una implicación (en el sentido de " ") a , como un esquema axiomático o en forma cuantificada. Una situación que se estudia comúnmente es la de un fijo que exhibe la propiedad metateórica del siguiente tipo: Para una instancia de alguna colección de fórmulas de una forma particular, aquí capturada mediante y , se estableció la existencia de un número tal que . Aquí se puede entonces postular , donde el límite es una variable numérica en el lenguaje de la teoría. Por ejemplo, la regla de Church es una regla admisible en la aritmética de Heyting de primer orden y, además, el principio de tesis de Church correspondiente puede adoptarse consistentemente como un axioma. La nueva teoría con el principio agregado es anticlásica, en el sentido de que puede no ser consistente ya no adoptar también . De manera similar, anexando el principio del medio excluido a alguna teoría , la teoría así obtenida puede probar nuevas afirmaciones estrictamente clásicas, y esto puede echar a perder algunas de las propiedades metateóricas que se establecieron previamente para . De esta manera, no puede adoptarse la aritmética de Peano , también conocida como aritmética de Peano . ${\displaystyle \to }$ ${\displaystyle {\mathsf {T}}}$ ${\displaystyle {\mathsf {T}}}$ ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle {\mathrm {e} }}$ ${\displaystyle {\mathsf {T}}\vdash \phi \implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$ ${\displaystyle \phi \to \exists (e\in {\mathbb {N} }).\psi (e)}$ ${\displaystyle e}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {CT} }_{0}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {T}}}$ ${\displaystyle {\mathsf {T}}}$ ${\displaystyle {\mathrm {CT} }_{0}}$ ${\displaystyle {\mathsf {HA}}+{\mathrm {PEM} }}$ ${\displaystyle {\mathsf {PA}}}$

En esta subsección nos centraremos en las teorías de conjuntos con cuantificación sobre una noción totalmente formal de un espacio de secuencias infinitas, es decir, un espacio de funciones, como se presentará más adelante. Una traducción de la regla de Church al lenguaje de la teoría en sí puede leerse aquí

${\displaystyle \forall (f\in {\mathbb {N} }^{\mathbb {N} }).\exists (e\in {\mathbb {N} }).{\Big (}\forall (n\in {\mathbb {N} }).\exists (w\in {\mathbb {N} }).T(e,n,w)\land U(w,f(n)){\Big )}}$

El predicado T de Kleene junto con la extracción del resultado expresa que cualquier número de entrada que se mapea al número se atestigua , a través de , como un mapeo computable. Aquí ahora denota un modelo de teoría de conjuntos de los números naturales estándar y es un índice con respecto a una enumeración de programa fija. Se han utilizado variantes más fuertes, que extienden este principio a funciones definidas en dominios de baja complejidad. El principio rechaza la decidibilidad para el predicado definido como , expresando que es el índice de una función computable que se detiene en su propio índice. También se pueden considerar formas más débiles, doblemente negadas del principio, que no requieren la existencia de una implementación recursiva para cada , pero que aún hacen que los principios que afirman la existencia de funciones que probadamente no tienen realización recursiva sean inconsistentes. Algunas formas de una tesis de Church como principio son incluso consistentes con la clásica, débil teoría aritmética de segundo orden , llamada un subsistema de la teoría de primer orden de dos órdenes . ${\displaystyle n}$ ${\displaystyle f(n)}$ ${\displaystyle w}$ ${\displaystyle {\mathbb {N} }}$ ${\displaystyle e}$ ${\displaystyle f\in {\mathbb {N} }^{X}}$ ${\displaystyle X\subset {\mathbb {N} }}$ ${\displaystyle Q(e)}$ ${\displaystyle \exists (w\in {\mathbb {N} }).T(e,e,w)}$ ${\displaystyle e}$ ${\displaystyle f}$ ${\displaystyle {\mathsf {RCA}}_{0}}$ ${\displaystyle {\mathsf {Z}}_{2}}$

La colección de funciones computables es clásicamente subcontable , lo que clásicamente es lo mismo que ser contable. Pero las teorías clásicas de conjuntos generalmente afirmarán que también se cumple con otras funciones además de las computables. Por ejemplo, hay una prueba de que existen funciones totales (en el sentido de la teoría de conjuntos) que no pueden ser capturadas por una máquina de Turing . Si tomamos en serio el mundo computable como ontología, un excelente ejemplo de una concepción anticlásica relacionada con la escuela markoviana es la subcontabilidad permitida de varias colecciones incontables. Al adoptar la subcontabilidad de la colección de todas las secuencias infinitas de números naturales ( ) como un axioma en una teoría constructiva, la "pequeñez" (en términos clásicos) de esta colección, en algunas realizaciones teóricas de conjuntos, ya está capturada por la teoría misma. Una teoría constructiva también puede no adoptar ni axiomas clásicos ni anticlásicos y, por lo tanto, permanecer agnóstica hacia cualquiera de las posibilidades. ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$

Los principios constructivos ya prueban para cualquier . Y así, para cualquier elemento dado de , la correspondiente declaración de tercero excluido para la proposición no puede ser negada. De hecho, para cualquier , por no contradicción es imposible descartar y descartar su negación a la vez, y la regla de De Morgan relevante se aplica como se indicó anteriormente. Pero una teoría también puede, en algunos casos, permitir la afirmación de rechazo . Adoptar esto no requiere proporcionar un particular que atestigua el fracaso del tercero excluido para la proposición particular , es decir, que atestigua lo inconsistente . Los predicados en un dominio infinito corresponden a problemas de decisión . Motivados por problemas demostrablemente computablemente indecidibles , uno puede rechazar la posibilidad de decidibilidad de un predicado sin hacer también ninguna afirmación de existencia en . Como otro ejemplo, tal situación se aplica en el análisis intuicionista brouweriano , en un caso donde el cuantificador abarca infinitas secuencias binarias interminables y afirma que una secuencia es cero en todas partes. Respecto de esta propiedad, de ser identificada concluyentemente como la secuencia que es siempre constante, la adopción del principio de continuidad de Brouwer descarta estrictamente que esto pueda probarse como decidible para todas las secuencias. ${\displaystyle \forall (x\in X).\neg \neg {\big (}Q(x)\lor \neg Q(x){\big )}}$ ${\displaystyle Q}$ ${\displaystyle x}$ ${\displaystyle X}$ ${\displaystyle x}$ ${\displaystyle Q(x)}$ ${\displaystyle \neg \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$ ${\displaystyle t\in X}$ ${\displaystyle Q(t)}$ ${\displaystyle \neg {\big (}Q(t)\lor \neg Q(t){\big )}}$ ${\displaystyle Q(x)}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle Q(x)}$ ${\displaystyle x}$

Por lo tanto, en un contexto constructivo con una lógica denominada no clásica como la que se utiliza aquí, se pueden adoptar sistemáticamente axiomas que están en contradicción con las formas cuantificadas del tercero excluido, pero que también son no constructivos en el sentido computable o tal como se mide por las propiedades de existencia metalógicas discutidas anteriormente. De esa manera, una teoría de conjuntos constructiva también puede proporcionar el marco para estudiar teorías no clásicas, por ejemplo, los anillos que modelan el análisis infinitesimal suave .

Historia y visión general

Históricamente, el tema de la teoría de conjuntos constructivos (a menudo también " ") comenzó con el trabajo de John Myhill sobre las teorías también llamadas y . ^{[3] [4] [5]} En 1973, había propuesto la primera como una teoría de conjuntos de primer orden basada en la lógica intuicionista, tomando el fundamento más común y descartando el axioma de elección, así como el principio del tercero excluido, dejando inicialmente todo lo demás como está. Sin embargo, diferentes formas de algunos de los axiomas que son equivalentes en el contexto clásico son inequivalentes en el contexto constructivo, y algunas formas implican , como se demostrará. En esos casos, se adoptaron en consecuencia las formulaciones intuicionistamente más débiles. El sistema mucho más conservador es también una teoría de primer orden, pero de varios tipos y cuantificación acotada, con el objetivo de proporcionar una base formal para el programa de matemáticas constructivas de Errett Bishop . ${\displaystyle {\mathsf {CST}}}$ ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle {\mathsf {CST}}}$ ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {CST}}}$

La discusión principal presenta una secuencia de teorías en el mismo lenguaje que , que conducen a la bien estudiada , ^[6] de Peter Aczel y más allá. Muchos resultados modernos se remontan a Rathjen y sus estudiantes. también se caracteriza por las dos características presentes también en la teoría de Myhill: por un lado, utiliza la separación predicativa en lugar del esquema de separación completo e ilimitado. La acotación se puede manejar como una propiedad sintáctica o, alternativamente, las teorías se pueden extender de manera conservadora con un predicado de acotació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 muy casualmente en la topología general clásica . Añadiendo a una teoría incluso más débil que recupera , como se detalla a continuación. ^[7] El sistema, que ha llegado a conocerse como teoría de conjuntos intuicionista de Zermelo-Fraenkel ( ), es una teoría de conjuntos fuerte sin . Es similar a , pero menos conservadora o predicativa . La teoría denotada es la versión constructiva de , la teoría clásica de conjuntos de Kripke-Platek sin una forma de conjunto potencia y donde incluso el axioma de colección está acotado. ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {IKP}}}$ ${\displaystyle {\mathsf {KP}}}$

Modelos

Muchas teorías estudiadas en la teoría de conjuntos constructivos son meras restricciones de la teoría de conjuntos de Zermelo-Fraenkel ( ) ${\displaystyle {\mathsf {ZF}}}$ con respecto a su axioma así como a su lógica subyacente. Tales teorías pueden entonces ser interpretadas también en cualquier modelo de . ${\displaystyle {\mathsf {ZF}}}$

La aritmética de Peano es biinterpretable con la teoría dada por menos Infinito y sin conjuntos infinitos, más la existencia de todos los cierres transitivos . (Esto último también está implícito después de promover la Regularidad al esquema de Inducción de Conjuntos , que se analiza más adelante). Del mismo modo, la aritmética constructiva también puede tomarse como una disculpa para la mayoría de los axiomas adoptados en : La aritmética de Heyting es biinterpretable con una teoría de conjuntos constructiva débil, ^{[8] [9]} como también se describe en el artículo sobre . Uno puede caracterizar aritméticamente una relación de pertenencia " " y con ella probar - en lugar de la existencia de un conjunto de números naturales - que todos los conjuntos en su teoría están en biyección con un natural de von Neumann (finito) , un principio denotado . Este contexto valida aún más la Extensionalidad, el Emparejamiento, la Unión, la Intersección Binaria (que está relacionada con el esquema Axioma de separación predicativa ) y el esquema de Inducción de Conjuntos. Tomados como axiomas, los principios antes mencionados constituyen una teoría de conjuntos que ya es idéntica a la teoría dada por menos la existencia de pero más como axioma. Todos esos axiomas se discuten en detalle a continuación. En relación con esto, también se demuestra que los conjuntos finitos hereditarios cumplen todos los axiomas anteriores. Este es un resultado que persiste al pasar a y menos Infinito. ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle \in }$ ${\displaystyle \omega }$ ${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle \omega }$ ${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {ZF}}}$

En lo que se refiere a las realizaciones constructivas, existe una teoría de realizabilidad relevante. En relación con esto, la teoría de Aczel, la teoría constructiva de Zermelo-Fraenkel, ha sido interpretada en teorías de tipo Martin-Löf , como se esboza en la sección sobre . De esta manera, los teoremas demostrables en esta teoría y en teorías de conjuntos más débiles son candidatos para una realización por computadora. ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {CZF}}}$

También se han introducido modelos de prehaz para teorías de conjuntos constructivos. Estos son análogos a los modelos de prehaz para la teoría de conjuntos intuicionista desarrollados por Dana Scott en la década de 1980. ^{[10] [11]} Se han identificado modelos de realizabilidad dentro del topos efectivo , que, por ejemplo, validan a la vez la separación completa, la elección dependiente relativizada , la independencia de premisa para conjuntos, pero también la subcontabilidad de todos los conjuntos, el principio de Markov y la tesis de Church en la formulación para todos los predicados. ^[12] ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathrm {RDC} }}$ ${\displaystyle {\mathrm {IP} }}$ ${\displaystyle {\mathrm {MP} }}$ ${\displaystyle {\mathrm {CT} _{0}}}$

Notación

En una teoría de conjuntos axiomática , los conjuntos son las entidades que exhiben propiedades. Pero existe una relación más intrincada entre el concepto de conjunto y la lógica. Por ejemplo, la propiedad de ser un número natural menor que 100 puede reformularse como un miembro del conjunto de números con esa propiedad. Los axiomas de la teoría de conjuntos gobiernan la existencia de conjuntos y, por lo tanto, gobiernan qué predicados pueden materializarse como entidad en sí mismos, en este sentido. La especificación también está directamente gobernada por los axiomas, como se analiza a continuación. Para una consideración práctica, considere la propiedad de ser una secuencia de resultados de lanzamientos de moneda que, en general, muestran más caras que cruces. Esta propiedad puede usarse para separar un subconjunto correspondiente de cualquier conjunto de secuencias finitas de lanzamientos de moneda. En relación con esto, la formalización teórica de la medida de un evento probabilístico se basa explícitamente en conjuntos y proporciona muchos más ejemplos.

Esta sección presenta el lenguaje objeto y las nociones auxiliares utilizadas para formalizar esta materialización.

Idioma

Los símbolos conectivos proposicionales utilizados para formar fórmulas sintácticas son estándar. Los axiomas de la teoría de conjuntos proporcionan un medio para demostrar la igualdad " " de conjuntos y ese símbolo puede, mediante el abuso de la notación , usarse para clases. Un conjunto en el que el predicado de igualdad es decidible también se llama discreto . La negación " " de la igualdad a veces se llama negación de la igualdad y se escribe comúnmente " ". Sin embargo, en un contexto con relaciones de separación , por ejemplo cuando se trata de secuencias, el último símbolo también se usa a veces para algo diferente. ${\displaystyle =}$ ${\displaystyle \neg }$ ${\displaystyle \neq }$

El tratamiento común, tal como se adopta también aquí, formalmente sólo extiende la lógica subyacente mediante un predicado binario primitivo de la teoría de conjuntos, " ". Al igual que con la igualdad, la negación de la elementabilidad " " se escribe a menudo " ". ${\displaystyle \in }$ ${\displaystyle \in }$ ${\displaystyle \notin }$

Variables

A continuación, el griego denota una proposición o predicado variable en esquemas axiomáticos y o se utiliza para predicados particulares de ese tipo. La palabra "predicado" a veces también se utiliza indistintamente con "fórmulas", incluso en el caso unario . ${\displaystyle \phi }$ ${\displaystyle P}$ ${\displaystyle Q}$

Los cuantificadores solo abarcan conjuntos y se indican con letras minúsculas. Como es habitual, se pueden utilizar corchetes de argumento para expresar predicados, con el fin de resaltar variables libres particulares en su expresión sintáctica, como en " ". La existencia única aquí significa . ${\displaystyle Q(z)}$ ${\displaystyle \exists !x.Q(x)}$ ${\displaystyle \exists x.\forall y.{\big (}y=x\leftrightarrow Q(y){\big )}}$

Clases

Como también es común, se hace uso de la notación de constructor de conjuntos para clases , que, en la mayoría de los contextos, no son parte del lenguaje objeto pero se usan para una discusión concisa. En particular, se pueden introducir declaraciones de notación de la clase correspondiente mediante " ", con el propósito de expresar cualquier como . Se pueden usar predicados lógicamente equivalentes para introducir la misma clase. También se escribe como abreviatura de . Por ejemplo, se puede considerar y esto también se denota . ${\displaystyle A=\{z\mid Q(z)\}}$ ${\displaystyle Q(a)}$ ${\displaystyle a\in A}$ ${\displaystyle \{z\in B\mid Q(z)\}}$ ${\displaystyle \{z\mid z\in B\land Q(z)\}}$ ${\displaystyle \{z\in B\mid z\notin C\}}$ ${\displaystyle B\setminus C}$

Se abrevia por y por . La noción sintáctica de cuantificación acotada en este sentido puede desempeñar un papel en la formulación de esquemas axiomáticos, como se ve en la discusión de axiomas a continuación. Expresar la afirmación de subclase , es decir , por . Para un predicado , trivialmente . Y así se sigue que . La noción de cuantificadores acotados por subconjuntos, como en , también se ha utilizado en la investigación teórica de conjuntos, pero no se destacará más aquí. ${\displaystyle \forall z.{\big (}z\in A\to Q(z){\big )}}$ ${\displaystyle \forall (z\in A).Q(z)}$ ${\displaystyle \exists z.{\big (}z\in A\land Q(z){\big )}}$ ${\displaystyle \exists (z\in A).Q(z)}$ ${\displaystyle \forall (z\in A).z\in B}$ ${\displaystyle \forall z.(z\in A\to z\in B)}$ ${\displaystyle A\subset B}$ ${\displaystyle Q}$ ${\displaystyle \forall z.{\big (}(z\in B\land Q(z))\to z\in B{\big )}}$ ${\displaystyle \{z\in B\mid Q(z)\}\subset B}$ ${\displaystyle \forall (z\subset A).z\in B}$

Si existe un conjunto dentro de una clase, es decir , , entonces se lo llama habitado . También se puede usar la cuantificación en para expresar esto como . Entonces, se demuestra que la clase no es el conjunto vacío, que se presenta a continuación. Si bien es clásicamente equivalente, constructivamente no vacío es una noción más débil con dos negaciones y debería llamarse no deshabitado . Desafortunadamente, la palabra para la noción más útil de 'habitado' rara vez se usa en las matemáticas clásicas. ${\displaystyle \exists z.(z\in A)}$ ${\displaystyle A}$ ${\displaystyle \exists (z\in A).(z=z)}$ ${\displaystyle A}$

Dos formas de expresar que las clases son disjuntas capturan muchas de las reglas de negación válidas desde el punto de vista intuicionista: . Usando la notación anterior, esta es una equivalencia puramente lógica y en este artículo la proposición se podrá expresar además como . ${\displaystyle {\big (}\forall (x\in A).x\notin B{\big )}\leftrightarrow \neg \exists (x\in A).x\in B}$ ${\displaystyle A\cap B=\{\}}$

Una subclase se denomina separable si el predicado de pertenencia relativizado es decidible, es decir, si se cumple. También se denomina decidible si la superclase se desprende claramente del contexto (a menudo, este es el conjunto de números naturales). ${\displaystyle A\subset B}$ ${\displaystyle B}$ ${\displaystyle \forall (x\in B).x\in A\lor x\notin A}$

Equivalencia extensional

Denote por la afirmación que expresa que dos clases tienen exactamente los mismos elementos, es decir , o equivalentemente . Esto no debe confundirse con el concepto de equinumerosidad que también se utiliza a continuación. ${\displaystyle A\simeq B}$ ${\displaystyle \forall z.(z\in A\leftrightarrow z\in B)}$ ${\displaystyle (A\subset B)\land (B\subset A)}$

Con , la conveniente relación de notación entre y , los axiomas de la forma postulan que la clase de todos los conjuntos para los cuales se cumple en realidad forma un conjunto . De manera menos formal, esto puede expresarse como . Asimismo, la proposición transmite " cuando está entre los conjuntos de la teoría". Para el caso donde es el predicado trivialmente falso, la proposición es equivalente a la negación de la afirmación de existencia anterior, expresando la no existencia de como un conjunto. ${\displaystyle A}$ ${\displaystyle \{z\mid Q(z)\}}$ ${\displaystyle x\in A}$ ${\displaystyle Q(x)}$ ${\displaystyle \exists a.\forall z.{\big (}z\in a\leftrightarrow Q(z){\big )}}$ ${\displaystyle Q}$ ${\displaystyle \exists a.a\simeq A}$ ${\displaystyle \forall a.(a\simeq A)\to P(a)}$ ${\displaystyle P(A)}$ ${\displaystyle A}$ ${\displaystyle P}$ ${\displaystyle A}$

Otras extensiones de la notación de comprensión de clases como las mencionadas anteriormente se utilizan comúnmente en la teoría de conjuntos, dando significado a declaraciones como " ", etc. ${\displaystyle \{f(z)\mid Q(z)\}\simeq \{\langle x,y,z\rangle \mid T(x,y,z)\}}$

Sintácticamente de manera más general, un conjunto también puede caracterizarse utilizando otro predicado 2-ario a través de , donde el lado derecho puede depender de la variable real , y posiblemente incluso de la membresía en sí mismo. ${\displaystyle w}$ ${\displaystyle R}$ ${\displaystyle \forall x.x\in w\leftrightarrow R(x,w)}$ ${\displaystyle w}$ ${\displaystyle w}$

Subteorías de ZF

Se presentan aquí una serie de axiomas conocidos o sus reformulaciones pertinentes. Se enfatiza cómo la ausencia de en la lógica afecta lo que es demostrable y se destacan cuáles axiomas no clásicos son, a su vez, consistentes. ${\displaystyle {\mathrm {PEM} }}$

Igualdad

Usando la notación introducida anteriormente, el siguiente axioma proporciona un medio para demostrar la igualdad " " de dos conjuntos , de modo que a través de la sustitución, cualquier predicado sobre se traduce a uno de . Por las propiedades lógicas de la igualdad, la dirección inversa de la implicación postulada se cumple automáticamente. ${\displaystyle =}$ ${\displaystyle x}$ ${\displaystyle y}$

En una interpretación constructiva, los elementos de una subclase de pueden venir equipados con más información que los de , en el sentido de que ser capaz de juzgar es ser capaz de juzgar . Y (a menos que toda la disyunción se desprenda de axiomas) en la interpretación de Brouwer–Heyting–Kolmogorov , esto significa haberla probado o haberla rechazado. Como puede no ser separable de , es decir, como puede no ser decidible para todos los elementos de , las dos clases y deben distinguirse a priori. ${\displaystyle A=\{z\in B\mid Q(z)\lor \neg Q(z)\}}$ ${\displaystyle B}$ ${\displaystyle B}$ ${\displaystyle b\in A}$ ${\displaystyle Q(b)\lor \neg Q(b)}$ ${\displaystyle Q(b)}$ ${\displaystyle \{z\in B\mid Q(z)\}}$ ${\displaystyle B}$ ${\displaystyle Q}$ ${\displaystyle B}$ ${\displaystyle A}$ ${\displaystyle B}$

Consideremos un predicado que se cumple demostrablemente para todos los elementos de un conjunto , de modo que , y supongamos que se establece que la clase del lado derecho es un conjunto. Nótese que, incluso si este conjunto de la derecha también se vincula 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 derecho se juzga igual al del lado izquierdo. Este análisis anterior también muestra que un enunciado de la forma , que en la notación de clase informal puede expresarse como , se expresa entonces de manera equivalente como . Esto significa que establecer tales teoremas (por ejemplo, los demostrables a partir de la inducción matemática completa) permite sustituir la subclase de del lado izquierdo de la igualdad por solo , en cualquier fórmula. ${\displaystyle Q}$ ${\displaystyle y}$ ${\displaystyle y\simeq \{z\in y\mid Q(z)\}}$ ${\displaystyle Q}$ ${\displaystyle \forall (x\in w).Q(x)}$ ${\displaystyle w\subset \{x\mid Q(x)\}}$ ${\displaystyle \{x\in w\mid Q(x)\}=w}$ ${\displaystyle \forall }$ ${\displaystyle w}$ ${\displaystyle w}$

Nótese que adoptar " " como símbolo en una teoría de lógica de predicados hace que la igualdad de dos términos sea una expresión libre de cuantificadores. ${\displaystyle =}$

Enfoques alternativos

Aunque se adopta con frecuencia, este axioma ha sido criticado en el pensamiento constructivo, ya que efectivamente colapsa las propiedades definidas de manera diferente, o al menos los conjuntos vistos como la extensión de estas propiedades, una noción fregiana .

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 no suele adoptarse en la teoría de tipos. ${\displaystyle \simeq }$

Otros marcos de trabajo para las matemáticas constructivas podrían exigir en cambio una regla particular para la igualdad o separación de los elementos de cada uno de los conjuntos analizados. Pero también en un enfoque de los conjuntos que enfatiza la separación se puede utilizar la definición anterior en términos de subconjuntos para caracterizar una noción de igualdad " " de esos subconjuntos. En relación con esto, se da una noción vaga de complementación de dos subconjuntos y cuando dos miembros cualesquiera y están demostrablemente separados entre sí. La colección de pares complementarios se comporta bien algebraicamente . ${\displaystyle z\in x}$ ${\displaystyle x}$ ${\displaystyle \simeq }$ ${\displaystyle u\subset x}$ ${\displaystyle v\subset x}$ ${\displaystyle s\in u}$ ${\displaystyle t\in v}$ ${\displaystyle \langle u,v\rangle }$

Fusión de conjuntos

Defina la notación de clase para el emparejamiento de unos pocos elementos dados mediante disyunciones. Por ejemplo, es la afirmación sin cuantificador , y también dice , y así sucesivamente. ${\displaystyle z\in \{a,b\}}$ ${\displaystyle (z=a)\lor (z=b)}$ ${\displaystyle z\in \{a,b,c\}}$ ${\displaystyle (z=a)\lor (z=b)\lor (z=c)}$

Otros dos postulados básicos de existencia dados otros conjuntos son los siguientes: En primer lugar,

Dadas las definiciones anteriores, se expande a , por lo que se hace uso de la igualdad y una disyunción. El axioma dice que para dos conjuntos cualesquiera y , hay al menos un conjunto , que contiene al menos esos dos conjuntos. ${\displaystyle \{x,y\}\subset p}$ ${\displaystyle \forall z.(z=x\lor z=y)\to z\in p}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle p}$

Con la separación acotada que se muestra a continuación, la clase también existe como un conjunto. Se denota mediante el modelo de pares ordenados estándar , de modo que eg denota otra fórmula acotada en el lenguaje formal de la teoría. ${\displaystyle \{x,y\}}$ ${\displaystyle \langle x,y\rangle }$ ${\displaystyle \{\{x\},\{x,y\}\}}$ ${\displaystyle q=\langle x,y\rangle }$

Y luego, utilizando la cuantificación existencial y una conjunción,

diciendo que para cualquier conjunto , hay al menos un conjunto , que contiene todos los miembros , de los miembros de . El conjunto mínimo de dichos miembros es la unión . ${\displaystyle x}$ ${\displaystyle u}$ ${\displaystyle z}$ ${\displaystyle x}$ ${\displaystyle y}$

Los dos axiomas se formulan comúnmente de forma más fuerte, en términos de " " en lugar de solo " ", aunque esto es técnicamente redundante en el contexto de : Como el axioma de separación a continuación se formula con " ", para las declaraciones se puede derivar la equivalencia, dado que la teoría permite la separación utilizando . En los casos en que es una declaración existencial, como aquí en el axioma de unión, también hay otra formulación que utiliza un cuantificador universal. ${\displaystyle \leftrightarrow }$ ${\displaystyle \to }$ ${\displaystyle {\mathsf {BCST}}}$ ${\displaystyle \leftrightarrow }$ ${\displaystyle \exists t.\forall z.\phi (z)\to z\in t}$ ${\displaystyle \phi }$ ${\displaystyle \phi }$

También utilizando la separación acotada, los dos axiomas recién enunciados juntos implican la existencia de una unión binaria de dos clases y , cuando se ha establecido que son conjuntos, denotados por o . Para un conjunto fijo , para validar la pertenencia a la unión de dos conjuntos dados y , se necesita validar la parte del axioma, lo que se puede hacer validando la disyunción de los predicados que definen los conjuntos y , para . En términos de los conjuntos asociados, se hace validando la disyunción . ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle \bigcup \{a,b\}}$ ${\displaystyle a\cup b}$ ${\displaystyle z}$ ${\displaystyle z\in a\cup b}$ ${\displaystyle y=a}$ ${\displaystyle y=b}$ ${\displaystyle z\in y}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle z}$ ${\displaystyle z\in a\lor z\in b}$

La unión y otras notaciones que forman conjuntos también se utilizan para las clases. Por ejemplo, la proposición se escribe . Sea ahora . Dado , la decidibilidad de la pertenencia a , es decir, el enunciado potencialmente independiente , también se puede expresar como . Pero, como para cualquier enunciado de tercero excluido, la doble negación de este último se cumple: Esa unión no está habitada por . Esto demuestra que la partición es también una noción más compleja, de manera constructiva. ${\displaystyle z\in A\land z\notin C}$ ${\displaystyle z\in A\setminus C}$ ${\displaystyle B\subset A}$ ${\displaystyle z\in A}$ ${\displaystyle B}$ ${\displaystyle z\in B\lor z\notin B}$ ${\displaystyle z\in B\cup (A\setminus B)}$ ${\displaystyle z}$

Establecer existencia

La propiedad que es falsa para cualquier conjunto corresponde a la clase vacía , que se denota por o cero, . Que la clase vacía es un conjunto se deduce fácilmente de otros axiomas de existencia, como el Axioma de Infinito que se muestra a continuación. Pero si, por ejemplo, uno está explícitamente interesado en excluir conjuntos infinitos en su estudio, en este punto puede adoptar la ${\displaystyle \{\}}$ ${\displaystyle 0}$

La introducción del símbolo (como notación abreviada para expresiones que involucran propiedades caracterizantes) se justifica porque se puede demostrar la unicidad de este conjunto. Como es falso para cualquier , el axioma se lee entonces . ${\displaystyle \{\}}$ ${\displaystyle y\in \{\}}$ ${\displaystyle y}$ ${\displaystyle \exists x.x\simeq \{\}}$

Escriba para , que es igual a , es decir . Asimismo, escriba para , que es igual a , es decir . Una proposición simple y demostrablemente falsa es, por ejemplo, , correspondiente a en el modelo aritmético estándar. Nuevamente, aquí símbolos como se tratan como notación conveniente y cualquier proposición realmente se traduce a una expresión usando solo " " y símbolos lógicos, incluidos los cuantificadores. Acompañado por un análisis metamatemático de que las capacidades de las nuevas teorías son equivalentes de manera efectiva, también se pueden considerar extensiones formales mediante símbolos como . ${\displaystyle 1}$ ${\displaystyle S0}$ ${\displaystyle \{\{\}\}}$ ${\displaystyle \{1\}}$ ${\displaystyle 2}$ ${\displaystyle S1}$ ${\displaystyle \{\{\},\{\{\}\}\}}$ ${\displaystyle \{0,1\}}$ ${\displaystyle \{\}\in \{\}}$ ${\displaystyle 0<0}$ ${\displaystyle \{\}}$ ${\displaystyle \in }$ ${\displaystyle 0}$

En términos más generales, para un conjunto , defina el conjunto sucesor como . La interacción de la operación sucesora con la relación de pertenencia tiene una cláusula recursiva, en el sentido de que . Por reflexividad de igualdad, , y en particular siempre está habitado. ${\displaystyle x}$ ${\displaystyle Sx}$ ${\displaystyle x\cup \{x\}}$ ${\displaystyle (y\in Sx)\leftrightarrow (y\in x\lor y=x)}$ ${\displaystyle x\in Sx}$ ${\displaystyle Sx}$

BCC

A continuación se utilizan esquemas axiomáticos , es decir, axiomas para una determinada colección de predicados. Algunos de los esquemas axiomáticos indicados también deben permitir cualquier colección de parámetros de conjunto (es decir, cualquier variable nombrada en particular ). Es decir, se permiten instancias del esquema en las que el predicado (alguna variable nombrada en particular ) también depende de una serie de variables de conjunto adicionales y la declaración del axioma se entiende con cierres universales externos adicionales correspondientes (como en ). ${\displaystyle v_{0},v_{1},\dots ,v_{n}}$ ${\displaystyle \phi }$ ${\displaystyle \forall v_{0}.\forall v_{1}.\cdots \forall v_{n}.}$

Separación

La 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 el axioma de separación "completo", que se debilita. Además de los cuatro axiomas anteriores, postula la separación predicativa y el esquema de reemplazo. ${\displaystyle {\mathsf {BCST}}}$

Este axioma equivale a postular la existencia de un conjunto obtenido por la intersección de cualquier conjunto y cualquier clase descrita predicativamente . Para cualquier conjunto demostrado, cuando el predicado se toma como , se obtiene la intersección binaria de conjuntos y se escribe . La intersección corresponde a la conjunción de manera análoga a cómo la unión corresponde a la disyunción. ${\displaystyle s}$ ${\displaystyle y}$ ${\displaystyle \{x\mid \phi (x)\}}$ ${\displaystyle z}$ ${\displaystyle \phi (x):=x\in z}$ ${\displaystyle s=y\cap z}$

Cuando el predicado se toma como la negación , se obtiene el principio de diferencia, concediendo la existencia de cualquier conjunto . Nótese que los conjuntos como o siempre están vacíos. Entonces, como se señaló, de la Separación y la existencia de al menos un conjunto (por ejemplo, Infinito a continuación) se seguirá la existencia del conjunto vacío (también denotado ). Dentro de este contexto conservador de , el esquema de Separación Predicativa 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 hace uso de un esquema de fórmula. ${\displaystyle \phi (x):=x\notin z}$ ${\displaystyle y\setminus z}$ ${\displaystyle y\setminus y}$ ${\displaystyle \{x\in y\mid \neg (x=x)\}}$ ${\displaystyle \{\}}$ ${\displaystyle 0}$ ${\displaystyle {\mathsf {BCST}}}$

La separación predicativa es un esquema que tiene en cuenta los aspectos sintácticos de los predicados que definen conjuntos, hasta la equivalencia demostrable. Las fórmulas permitidas se denotan por , el nivel más bajo en la jerarquía de Lévy de la teoría de conjuntos . ^[13] Los predicados generales en la teoría de conjuntos nunca están restringidos sintácticamente de esa manera y, por lo tanto, en la práctica, las subclases genéricas de conjuntos siguen siendo parte del lenguaje matemático. Como el alcance de las subclases que son conjuntos demostrables es sensible a los conjuntos que ya existen, este alcance se expande cuando se agregan más postulados de existencia de conjuntos. ${\displaystyle \Delta _{0}}$

Para una proposición , un tropo recurrente en el análisis constructivo de la teoría de conjuntos es considerar el predicado como la subclase del segundo ordinal . Si es demostrable que se cumple, o , o , entonces está habitado, o vacío (deshabitado), o no vacío (no deshabitado), respectivamente. Claramente, es equivalente tanto a la proposición , como también . Asimismo, es equivalente a y, equivalentemente, también . Entonces, aquí, ser separable de significa exactamente . En el modelo de los naturales, si es un número, también expresa que es menor que . La unión que es parte de la definición de operación sucesora anterior puede usarse para expresar la declaración del medio excluido como . En palabras, es decidible si y solo si el sucesor de es mayor que el ordinal más pequeño . La proposición se decide de cualquier manera al establecer cómo es menor: al ser ya menor que , o al ser el predecesor directo de . Otra forma de expresar el término medio excluido es como la existencia de un número mínimo de miembros de la clase habitada . ${\displaystyle P}$ ${\displaystyle x=0\land P}$ ${\displaystyle B:=\{x\in 1\mid P\}}$ ${\displaystyle 1:=S0=\{0\}}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle \neg \neg P}$ ${\displaystyle B}$ ${\displaystyle P}$ ${\displaystyle 0\in B}$ ${\displaystyle B=1}$ ${\displaystyle \neg P}$ ${\displaystyle B=0}$ ${\displaystyle \neg (0\in B)}$ ${\displaystyle B}$ ${\displaystyle 1}$ ${\displaystyle P\lor \neg P}$ ${\displaystyle B}$ ${\displaystyle 0\in B}$ ${\displaystyle 0}$ ${\displaystyle B}$ ${\displaystyle 0\in SB}$ ${\displaystyle P}$ ${\displaystyle B}$ ${\displaystyle 0}$ ${\displaystyle P}$ ${\displaystyle 0}$ ${\displaystyle 0}$ ${\displaystyle B}$ ${\displaystyle 0}$ ${\displaystyle SB}$ ${\displaystyle P}$ ${\displaystyle b:=B\cup \{1\}}$

Si el axioma de separación de uno permite la separación con , entonces es un subconjunto , que puede llamarse el valor de verdad asociado con . Se puede demostrar que dos valores de verdad son iguales, como conjuntos, demostrando una equivalencia. En términos de esta terminología, la colección de valores de prueba puede entenderse a priori como rica. No es sorprendente que las proposiciones decidibles tengan uno de un conjunto binario de valores de verdad. La disyunción intermedia excluida para eso también está implícita en el enunciado global . ${\displaystyle P}$ ${\displaystyle B}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle \forall b.(0\in b)\lor (0\notin b)}$

No existe un conjunto universal

Cuando se utiliza la terminología informal de clases, cualquier conjunto también se considera una clase. Al mismo tiempo, surgen las llamadas clases propias que no pueden tener extensión como conjunto. Cuando en una teoría hay una prueba de , entonces debe ser propia. (Cuando se adopta la perspectiva de sobre conjuntos, una teoría que tiene separación completa, las clases propias generalmente se consideran como aquellas que son "demasiado grandes" para ser un conjunto. Más técnicamente, son subclases de la jerarquía acumulativa que se extienden más allá de cualquier límite ordinal). ${\displaystyle \neg \exists x.A\subset x}$ ${\displaystyle A}$ ${\displaystyle {\mathsf {ZF}}}$

Por una observación en la sección sobre la fusión de conjuntos, no se puede descartar de manera consistente que un conjunto sea miembro de una clase de la forma . Una prueba constructiva de que está en esa clase contiene información. Ahora bien, si es un conjunto, entonces la clase es demostrablemente apropiada. Lo siguiente demuestra esto en el caso especial cuando está vacío, es decir, cuando el lado derecho es la clase universal. Al ser resultados negativos, se lee como en la teoría clásica. ${\displaystyle A\cup \{x\mid x\notin A\}}$ ${\displaystyle A}$ ${\displaystyle \{x\mid x\notin A\}}$ ${\displaystyle A}$

Lo siguiente es válido para cualquier relación . Da una condición puramente lógica tal que dos términos y no pueden estar relacionados entre sí. ${\displaystyle E}$ ${\displaystyle s}$ ${\displaystyle y}$ ${\displaystyle E}$

${\displaystyle {\big (}\forall x.xEs\leftrightarrow (xEy\land \neg xEx){\big )}\to \neg (yEs\lor sEs\lor sEy)}$

Lo más importante aquí es el rechazo de la disyunción final, . La expresión no implica cuantificación ilimitada y, por lo tanto, se permite en la separación. La construcción de Russel , a su vez, muestra que . Por lo tanto, para cualquier conjunto , la separación predicativa por sí sola implica que existe un conjunto que no es miembro de . En particular, no puede existir ningún conjunto universal en esta teoría. ${\displaystyle \neg sEy}$ ${\displaystyle \neg (x\in x)}$ ${\displaystyle \{x\in y\mid x\notin x\}\notin y}$ ${\displaystyle y}$ ${\displaystyle y}$

En una teoría que adopte además el axioma de regularidad , como , es demostrablemente falso para cualquier conjunto . En ese caso, esto significa que el subconjunto es igual a sí mismo y que la clase es el conjunto vacío. ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle x\in x}$ ${\displaystyle x}$ ${\displaystyle \{x\in y\mid x\notin x\}}$ ${\displaystyle y}$ ${\displaystyle \{x\mid x\in x\}}$

Para cualquier y , el caso especial en la fórmula anterior da ${\displaystyle E}$ ${\displaystyle y}$ ${\displaystyle s=y}$

${\displaystyle \neg {\big (}\forall x.xEy\leftrightarrow \neg xEx{\big )}}$

Esto ya implica que la subclase de la clase universal también es propia. Pero incluso sin Regularidad es consistente que exista una clase propia de singletons que se contengan exactamente a sí mismos. ${\displaystyle \{x\mid x\notin x\}}$ ${\displaystyle {\mathsf {ZF}}}$

Por otra parte, en una teoría con estratificación como la de los Nuevos Fundamentos Intuicionistas , la expresión sintáctica puede ser rechazada en la Separación. A su vez, la prueba anterior de negación de la existencia de un conjunto universal no puede realizarse en esa teoría. ${\displaystyle x\in x}$

Predicatividad

El esquema axiomático de la separación predicativa también se denomina -Separación o Separación limitada, como en la separación solo para cuantificadores limitados por conjuntos . (Nota de advertencia: la nomenclatura de la jerarquía de Lévy es análoga a la de la jerarquía aritmética , aunque la comparación puede ser sutil: la clasificación aritmética a veces se expresa no sintácticamente sino en términos de subclases de los naturales. Además, el nivel inferior de la jerarquía aritmética tiene varias definiciones comunes, algunas de las cuales no permiten el uso de algunas funciones totales. Una distinción similar no es relevante en el nivel o en niveles superiores. Finalmente, tenga en cuenta que una clasificación de una fórmula puede expresarse hasta la equivalencia en la teoría). ${\displaystyle \Delta _{0}}$ ${\displaystyle \Delta _{0}^{0}}$ ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle \Delta _{0}}$

El esquema es también la forma en que Mac Lane debilita un sistema cercano a la teoría de conjuntos de Zermelo , por fundamentos matemáticos relacionados con la teoría de topos . También se utiliza en el estudio de la absolutidad , y allí forma parte de la formulación de la teoría de conjuntos de Kripke-Platek . ${\displaystyle {\mathsf {Z}}}$

La restricción en el axioma también es la de limitar las definiciones impredicativas : en el mejor de los casos, no se debería reclamar la existencia de objetos que no sean explícitamente descriptibles, o cuya definición los involucre a ellos mismos o haga referencia a una clase apropiada, como cuando una propiedad que se debe verificar involucra un cuantificador universal. Por lo tanto, en una teoría constructiva sin el axioma de conjunto de potencias , cuando denota algún predicado 2-ario, generalmente no se debería esperar que una subclase de sea un conjunto, en caso de que se defina, por ejemplo, como en ${\displaystyle R}$ ${\displaystyle s}$ ${\displaystyle y}$

${\displaystyle \{x\in y\mid \forall t.{\big (}(t\subset y)\to R(x,t){\big )}\}}$,

o mediante definiciones similares que impliquen cualquier cuantificación sobre los conjuntos . Nótese que si esta subclase de es demostrablemente un conjunto, entonces este subconjunto en sí mismo también está en el ámbito ilimitado de la variable de conjunto . En otras palabras, como se cumple la propiedad de subclase , este conjunto exacto , definido usando la expresión , jugaría un papel en su propia caracterización. ${\displaystyle t\subset y}$ ${\displaystyle s}$ ${\displaystyle y}$ ${\displaystyle t}$ ${\displaystyle s\subset y}$ ${\displaystyle s}$ ${\displaystyle R(x,s)}$

Aunque la separación predicativa lleva a que menos definiciones de clase dadas sean conjuntos, se puede enfatizar que muchas definiciones de clase que son clásicamente equivalentes no lo son cuando se restringe uno mismo a la lógica más débil. Debido a la potencial indecidibilidad de los predicados generales, la noción de subconjunto y subclase es automáticamente más elaborada en las teorías de conjuntos constructivos que en las clásicas. Así que de esta manera se ha obtenido una teoría más amplia. Esto sigue siendo cierto si se adopta la separación completa, como en la teoría , que sin embargo estropea la propiedad de existencia así como las interpretaciones teóricas de tipo estándar, y de esta manera estropea una visión de abajo hacia arriba de los conjuntos constructivos. Como acotación al margen, como la subtipificación no es una característica necesaria de la teoría de tipos constructivos , se puede decir que la teoría de conjuntos constructivos difiere bastante de ese marco. ${\displaystyle {\mathsf {IZF}}}$

Reemplazo

Consideremos a continuación el

Se trata de conceder la existencia, como conjuntos, de la gama de predicados de tipo función, obtenidos a través de sus dominios. En la formulación anterior, el predicado no está restringido de manera similar al esquema de separación, pero este axioma ya implica un cuantificador existencial en el antecedente. Por supuesto, también podrían considerarse esquemas más débiles.

Por medio del reemplazo, la existencia de cualquier par también se sigue de la de cualquier otro par particular, como . Pero como la unión binaria utilizada en ya hizo uso del axioma de emparejamiento, este enfoque requiere postular la existencia de sobre la de . En una teoría con el axioma impredicativo de conjunto de potencias, la existencia de también se puede demostrar utilizando la separación. ${\displaystyle \{x,y\}}$ ${\displaystyle \{0,1\}=2=SS0}$ ${\displaystyle S}$ ${\displaystyle 2}$ ${\displaystyle 0}$ ${\displaystyle 2\subset {\mathcal {P}}{\mathcal {P}}0}$

Con el esquema de reemplazo, la teoría esbozada hasta ahora 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. A su vez, para cualquier número fijo (en la metateoría), la expresión del producto correspondiente, digamos , puede construirse como un conjunto. Los requisitos axiomáticos para los conjuntos definidos recursivamente en el lenguaje se discuten más adelante. Un conjunto es discreto, es decir, la igualdad de elementos dentro de un conjunto es decidible, si la relación correspondiente como un subconjunto de es decidible. ${\displaystyle x\times x\times x\times x}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x\times x}$

El reemplazo es relevante para la comprensión de funciones y puede verse como una forma de comprensión de manera más general. Solo cuando se asume que el reemplazo ya implica una separación completa. En , el reemplazo es principalmente importante para demostrar la existencia de conjuntos de alto rango , es decir, a través de instancias del esquema axiomático donde relaciona conjuntos relativamente pequeños con conjuntos más grandes, . ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle \phi (x,y)}$ ${\displaystyle x}$ ${\displaystyle y}$

Las teorías de conjuntos constructivos suelen tener un esquema axiomático de reemplazo, a veces restringido a fórmulas acotadas. Sin embargo, cuando se descartan otros axiomas, este esquema en realidad suele reforzarse, no más allá de , sino simplemente para recuperar cierta fuerza demostrativa. Existen axiomas más fuertes que no estropean las propiedades de existencia fuerte de una teoría, como se analiza más adelante. ${\displaystyle {\mathsf {ZF}}}$

Si es una función de y está dotada de un codominio (todo lo cual se analiza en detalle a continuación), entonces la imagen de es un subconjunto de . En otros enfoques del concepto de conjunto, la noción de subconjuntos se define en términos de "operaciones", de esta manera. ${\displaystyle i_{X}}$ ${\displaystyle X}$ ${\displaystyle Y}$ ${\displaystyle i_{X}}$ ${\displaystyle Y}$

Conjuntos finitos hereditarios

Los elementos de la clase de conjuntos finitos hereditarios se pueden implementar en cualquier lenguaje de programación común. Los axiomas discutidos anteriormente se abstraen de operaciones comunes en el tipo de datos del conjunto : el emparejamiento y la unión están relacionados con el anidamiento y el aplanamiento , o tomados en conjunto con la concatenación. El reemplazo está relacionado con la comprensión y la separación se relaciona entonces con el filtrado, a menudo más simple . El reemplazo junto con la inducción de conjuntos (introducida a continuación) es suficiente para axiomizar de manera constructiva y esa teoría también se estudia sin infinito. ${\displaystyle H_{\aleph _{0}}}$ ${\displaystyle H_{\aleph _{0}}}$

Una especie de mezcla entre emparejamiento y unión, un axioma más fácilmente relacionado con el sucesor es el Axioma de adjunción . ^{[14] [15]} Tales principios son relevantes para el modelado estándar de ordinales de Neumann individuales . También existen formulaciones de axiomas que emparejan Unión y Reemplazo en uno. Si bien postular el Reemplazo no es una necesidad en el diseño de una teoría de conjuntos constructiva débil que sea biinterpretable con la aritmética de Heyting , alguna forma de inducción lo es. A modo de comparación, 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. ${\displaystyle {\mathsf {HA}}}$

La discusión continúa ahora con axiomas que conceden la existencia de objetos que, en forma diferente pero relacionada, también se encuentran en teorías de tipos dependientes , a saber, productos y la colección de números naturales como un conjunto completo. Los conjuntos infinitos son particularmente útiles para razonar sobre operaciones aplicadas a secuencias definidas en dominios de índice no acotados , por ejemplo, la diferenciación formal de una función generadora o la adición de dos secuencias de Cauchy.

CETS

Para un predicado fijo y un conjunto , el enunciado expresa que es el más pequeño (en el sentido de " ") entre todos los conjuntos para los que es cierto, y que siempre es un subconjunto de tales . El objetivo del axioma de infinito es obtener eventualmente el único conjunto inductivo más pequeño . ${\displaystyle I}$ ${\displaystyle a}$ ${\displaystyle I(a)\land {\big (}\forall y.I(y)\to a\subset y{\big )}}$ ${\displaystyle a}$ ${\displaystyle \subset }$ ${\displaystyle y}$ ${\displaystyle I(y)}$ ${\displaystyle y}$

En el contexto de los axiomas comunes de la teoría de conjuntos, una afirmación de infinitud es afirmar que una clase está habitada y también incluye una cadena de miembros (o alternativamente una cadena de superconjuntos). Es decir,

${\displaystyle {\big (}\exists z.z\in A{\big )}\land \forall (x\in A).\exists (s\in A).x\in s}$.

Más concretamente, denotamos por la propiedad inductiva, ${\displaystyle \mathrm {Ind} _{A}}$

${\displaystyle (0\in A)\land \forall (x\in A).Sx\in A}$.

En términos de un predicado subyacente a la clase de modo que , este último se traduce a . ${\displaystyle Q}$ ${\displaystyle \forall x.(x\in A)\leftrightarrow Q(x)}$ ${\displaystyle Q(0)\land \forall x.{\big (}Q(x)\to Q(Sx){\big )}}$

Escriba para la intersección general . (Se puede considerar una variante de esta definición que requiere , pero solo usamos esta noción para la siguiente definición auxiliar). ${\displaystyle \bigcap B}$ ${\displaystyle \{x\mid \forall (y\in B).x\in y\}}$ ${\displaystyle \cap B\subset \cup B}$

Se suele definir una clase , la intersección de todos los conjuntos inductivos. (Las variantes de este tratamiento pueden funcionar en términos de una fórmula que depende de un parámetro del conjunto, de modo que ). La clase contiene exactamente todos los que cumplen la propiedad ilimitada . La intención es que si existen conjuntos inductivos, entonces la clase comparte cada número natural común con ellos, y luego la proposición , por definición de " ", implica que se cumple para cada uno de estos naturales. Si bien la separación acotada no es suficiente para demostrar que es el conjunto deseado, el lenguaje aquí forma la base para el siguiente axioma, que otorga la inducción de números naturales para predicados que constituyen un conjunto. ${\displaystyle \omega =\bigcap \{y\mid \mathrm {Ind} _{y}\}}$ ${\displaystyle w}$ ${\displaystyle \omega \subset w}$ ${\displaystyle \omega }$ ${\displaystyle x}$ ${\displaystyle \forall y.\mathrm {Ind} _{y}\to x\in y}$ ${\displaystyle \omega }$ ${\displaystyle \omega \subset A}$ ${\displaystyle \subset }$ ${\displaystyle Q}$ ${\displaystyle \omega }$

La teoría de conjuntos constructiva elemental tiene el axioma de así como el postulado ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle {\mathsf {BCST}}}$

Continuando, se toma el símbolo para denotar el único conjunto inductivo más pequeño, un ordinal de von Neumann ilimitado . Contiene el conjunto vacío y, para cada conjunto en , otro conjunto en que contiene un elemento más. ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$

Los símbolos llamados cero y sucesor están en la firma de la teoría de Peano . En , el sucesor definido anteriormente de cualquier número que también está en la clase se sigue directamente de la caracterización de los naturales naturales por nuestro modelo de von Neumann. Dado que el sucesor de tal conjunto se contiene a sí mismo, también se encuentra que ningún sucesor es igual a cero. Por lo tanto, dos de los axiomas de Peano con respecto a los símbolos cero y el relacionado con la clausura de se cumplen fácilmente. En cuarto lugar, en , donde es un conjunto, se puede demostrar que on es una operación inyectiva. ${\displaystyle {\mathsf {BCST}}}$ ${\displaystyle \omega }$ ${\displaystyle S}$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle \omega }$ ${\displaystyle S}$ ${\displaystyle \omega }$

Para algún predicado de conjuntos , el enunciado afirma que es válido para todos los subconjuntos del conjunto de los naturales. Y el axioma prueba ahora que dichos conjuntos existen. Dicha cuantificación también es posible en la aritmética de segundo orden . ${\displaystyle P}$ ${\displaystyle \forall S.(S\subset \omega \to P(S))}$ ${\displaystyle P}$

El orden por pares " " en los naturales se captura por su relación de pertenencia " ". La teoría prueba que el orden, así como la relación de igualdad en este conjunto, son decidibles. No solo ningún número es menor que , sino que la inducción implica que entre los subconjuntos de , es exactamente el conjunto vacío el que no tiene el menor miembro. El contrapositivo de esto prueba la existencia del menor número doblemente negado para todos los subconjuntos no vacíos de . Otro principio válido también clásicamente equivalente a él es la existencia del menor número para todos los subconjuntos habitados separables. Dicho esto, la afirmación de existencia desnuda para el subconjunto habitado de es equivalente al medio excluido para , y, por lo tanto, una teoría constructiva no demostrará estar bien ordenada . ${\displaystyle <}$ ${\displaystyle \in }$ ${\displaystyle 0}$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle b:=\{z\in 1\mid P\}\cup \{1\}}$ ${\displaystyle \omega }$ ${\displaystyle P}$ ${\displaystyle \omega }$

Formulaciones más débiles del infinito

Si fuera necesaria una motivación, la conveniencia de postular un conjunto ilimitado de números en relación con otras propiedades inductivas se hace evidente en la discusión de la aritmética en la teoría de conjuntos que se presenta más adelante. Pero, como es familiar en la teoría de conjuntos clásica, también se pueden formular formas débiles de Infinito. Por ejemplo, se puede simplemente postular la existencia de algún conjunto inductivo; dicho postulado de existencia es suficiente cuando se puede utilizar la Separación completa para extraer el subconjunto inductivo de los números naturales, el subconjunto compartido de todas las clases inductivas. Alternativamente, se pueden adoptar postulados de mera existencia más específicos. De cualquier manera, el conjunto inductivo cumple entonces la siguiente propiedad de existencia predecesora en el sentido del modelo de von Neumann : ${\displaystyle \exists y.\mathrm {Ind} _{y}}$ ${\displaystyle w}$ ${\displaystyle \Delta _{0}}$

${\displaystyle \forall m.(m\in w)\leftrightarrow {\big (}m=0\lor \exists (p\in w).Sp=m{\big )}}$

Sin hacer uso de la notación para la notación sucesora definida previamente, la igualdad extensional con un sucesor se captura mediante . Esto expresa que todos los elementos son iguales a o tienen ellos mismos un conjunto predecesor que comparte todos los demás miembros con . ${\displaystyle Sp=m}$ ${\displaystyle \forall n.(n\in m)\leftrightarrow (n=p\lor n\in p)}$ ${\displaystyle m}$ ${\displaystyle 0}$ ${\displaystyle p\in w}$ ${\displaystyle m}$

Obsérvese que a través de la expresión " " en el lado derecho, la propiedad que caracteriza a sus miembros aquí sintácticamente nuevamente contiene el símbolo mismo. Debido a la naturaleza ascendente de los números naturales, esto es fácil aquí. Suponiendo que la inducción de conjuntos se suma a , no hay dos conjuntos diferentes que tengan esta propiedad. Observe también que también hay formulaciones más largas de esta propiedad, evitando " " en favor de cuantificadores ilimitados. ${\displaystyle \exists (p\in w)}$ ${\displaystyle w}$ ${\displaystyle m}$ ${\displaystyle w}$ ${\displaystyle \Delta _{0}}$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle \exists (p\in w)}$

Límites numéricos

Al adoptar un axioma de infinitud, la cuantificación limitada por conjuntos legal en los predicados utilizados en -Separación permite entonces explícitamente cuantificadores numéricamente ilimitados - los dos significados de "limitado" no deben confundirse. Con lo que tenemos a mano, llamamos a una clase de números limitada si se cumple la siguiente declaración de existencia ${\displaystyle \Delta _{0}}$ ${\displaystyle \omega }$ ${\displaystyle I\subset \omega }$

${\displaystyle \exists (m\in \omega ).\forall (n\in \omega ).(n\in I\to n<m)}$

Se trata de una afirmación de finitud, también formulada de manera equivalente mediante . De manera similar, para reflejar más de cerca el análisis de las funciones a continuación, considere la condición anterior en la forma . Para las propiedades decidibles, estas son afirmaciones en aritmética, pero con el axioma de infinito, los dos cuantificadores están limitados por conjuntos. ${\displaystyle m\leq n\to n\notin I}$ ${\displaystyle \exists (m\in \omega ).\forall (n\in I).(n<m)}$ ${\displaystyle \Sigma _{2}^{0}}$

Para una clase , la declaración de ilimitación lógicamente positiva ${\displaystyle C}$

${\displaystyle \forall (k\in \omega ).\exists (j\in \omega ).(k\leq j\land j\in C)}$

ahora también es una propiedad de infinitud. Está en el caso aritmético decidible. Para validar la infinitud de un conjunto, esta propiedad funciona incluso si el conjunto contiene otros elementos además de una cantidad infinita de miembros de . ${\displaystyle \Pi _{2}^{0}}$ ${\displaystyle \omega }$

Inducción moderada en ECST

A continuación, un segmento inicial de los números naturales, es decir, para cualquier conjunto vacío incluido, se denota por . Este conjunto es igual y, por lo tanto, en este punto " " es una mera notación para su predecesor (es decir, no implica una función de sustracción). ${\displaystyle \{n\in \omega \mid n<m\}}$ ${\displaystyle m\in \omega }$ ${\displaystyle \{0,1,\dots ,m-1\}}$ ${\displaystyle m}$ ${\displaystyle m-1}$

Es instructivo recordar la forma en que una teoría con comprensión de conjuntos y extensionalidad termina codificando la lógica de predicados. Como cualquier clase en la teoría de conjuntos, un conjunto puede leerse como correspondiente a predicados sobre conjuntos. Por ejemplo, un entero es par si es miembro del conjunto de enteros pares, o un número natural tiene un sucesor si es miembro del conjunto de números naturales que tienen un sucesor. Para un ejemplo menos primitivo, fijemos un conjunto y denotemos el enunciado existencial de que existe el espacio de funciones sobre el ordinal finito en . El predicado se denotará a continuación, y aquí el cuantificador existencial no es meramente uno sobre números naturales, ni está acotado por ningún otro conjunto. Ahora bien, una proposición como el principio de exponenciación finita y, de manera menos formal, la igualdad son solo dos formas de formular el mismo enunciado deseado, a saber, una conjunción indexada de proposiciones existenciales donde se extiende sobre el conjunto de todos los naturales. Mediante la identificación extensional, la segunda forma expresa la afirmación utilizando notación para la comprensión de subclases y el objeto entre corchetes en el lado derecho puede no constituir ni siquiera un conjunto. Si esa subclase no es demostrablemente un conjunto, puede que no se la utilice en muchos principios de la teoría de conjuntos en las demostraciones, y puede que no sea posible establecer la clausura universal como teorema. La teoría de conjuntos puede así reforzarse con más axiomas de existencia de conjuntos, que se pueden utilizar con separación predicativa acotada , pero también simplemente postulando enunciados más fuertes. ${\displaystyle y}$ ${\displaystyle Q(n)}$ ${\displaystyle y}$ ${\displaystyle \exists h.h\simeq y^{\{0,1,\dots ,n-1\}}}$ ${\displaystyle \forall (n\in \omega ).Q(n)}$ ${\displaystyle \omega =\{n\in \omega \mid Q(n)\}}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle \forall (n\in \omega ).Q(n)}$ ${\displaystyle \forall }$

El segundo conjunto cuantificado universalmente en el axioma fuerte de Infinito expresa la inducción matemática para todos en el universo del discurso, es decir, para los conjuntos. Esto se debe a que el consecuente de esta cláusula, , establece que todos cumplen el predicado asociado. Al poder usar la separación predicativa para definir subconjuntos de , la teoría prueba la inducción para todos los predicados que involucran solo cuantificadores acotados por conjuntos. Este papel de los cuantificadores acotados por conjuntos también significa que más axiomas de existencia de conjuntos impactan la fuerza de este principio de inducción, motivando aún más el espacio de funciones y los axiomas de colección que serán el foco del resto del artículo. En particular, ya valida la inducción con cuantificadores sobre los naturales y, por lo tanto, la inducción como en la teoría aritmética de primer orden . El llamado axioma de inducción matemática completa para cualquier predicado (es decir, clase) expresado a través del lenguaje de la teoría de conjuntos es mucho más fuerte que el principio de inducción acotado válido en . El principio de inducción anterior podría adoptarse directamente, reflejando más de cerca la aritmética de segundo orden. En la teoría de conjuntos, también se deduce de la separación completa (es decir, ilimitada), que dice que todos los predicados de son conjuntos. La inducción matemática también es reemplazada por el axioma de inducción de conjuntos (completo). ${\displaystyle y}$ ${\displaystyle \omega \subset y}$ ${\displaystyle n\in \omega }$ ${\displaystyle \omega }$ ${\displaystyle \phi (n)}$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle \forall }$

Nota de advertencia: Al nombrar los enunciados de inducción, hay que tener cuidado de no mezclar la terminología con las teorías aritméticas. El esquema de inducción de primer orden de la teoría aritmética de números naturales afirma la inducción para todos los predicados definibles en el lenguaje de la aritmética de primer orden , es decir, predicados de solo números. Así que para interpretar el esquema axiomático de , se interpretan estas fórmulas aritméticas. En ese contexto, la cuantificación acotada significa específicamente cuantificación sobre un rango finito de números. También se puede hablar de la inducción en la teoría de primer orden pero de dos ordenaciones de la llamada aritmética de segundo orden , en una forma explícitamente expresada para subconjuntos de los naturales. Esa clase de subconjuntos puede tomarse como correspondiente a una colección más rica de fórmulas que las definibles por la aritmética de primer orden. En el programa de matemáticas inversas , todos los objetos matemáticos discutidos se codifican como naturales o subconjuntos de naturales. Los subsistemas de comprensión de complejidad muy baja estudiados en ese marco tienen un lenguaje que no solo expresa conjuntos aritméticos , mientras que todos los conjuntos de naturales particulares cuya existencia demuestran tales teorías son solo conjuntos computables . Los teoremas allí contenidos pueden ser un punto de referencia relevante para las teorías de conjuntos débiles con un conjunto de naturales, separación predicativa y solo alguna forma más restringida de inducción. Las matemáticas inversas constructivas existen como campo, pero están menos desarrolladas que su contraparte clásica. ^[16] Además, no se debe confundir con la formulación de segundo orden de la aritmética de Peano . Las teorías de conjuntos típicas como la que se analiza aquí también son de primer orden, pero esas teorías no son aritméticas y, por lo tanto, las fórmulas también pueden cuantificar sobre los subconjuntos de los naturales. Al discutir la fuerza de los axiomas relacionados con los números, también es importante tener en cuenta que el marco teórico aritmético y de conjuntos no comparten una firma común . Asimismo, siempre se debe tener cuidado con las ideas sobre la totalidad de las funciones. En la teoría de la computabilidad , el operador μ habilita todas las funciones recursivas generales parciales (o programas, en el sentido de que son computables por Turing), incluidas, por ejemplo, las recursivas no primitivas pero -totales, como la función de Ackermann . La definición del operador implica predicados sobre los naturales y, por lo tanto, el análisis teórico de las funciones y su totalidad depende del marco formal y del cálculo de pruebas en cuestión. ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {Z}}_{2}}$ ${\displaystyle {\mathsf {Z}}_{2}}$ ${\displaystyle {\mathsf {Z}}_{2}}$ ${\displaystyle {\mathsf {PA}}_{2}}$ ${\displaystyle {\mathsf {PA}}}$

Funciones

Nota general sobre programas y funciones

Naturalmente, el significado de las afirmaciones de existencia es un tema de interés en el constructivismo, ya sea para una teoría de conjuntos o para cualquier otro marco. Expresemos una propiedad de modo que un marco matemático valide lo que equivale a la afirmación ${\displaystyle R}$

${\displaystyle \forall (a\in A).\exists (c\in C).R(a,c)}$

Un cálculo de prueba constructiva puede validar tal juicio en términos de programas sobre dominios representados y algún objeto que represente una asignación concreta , proporcionando una elección particular de valor en (una única ), para cada entrada de . Expresado a través de la reescritura , este objeto de función puede entenderse como testigo de la proposición. Consideremos, por ejemplo, las nociones de prueba en la teoría de realizabilidad o los términos de función en una teoría de tipos con una noción de cuantificadores. Esta última captura la prueba de la proposición lógica a través de programas mediante la correspondencia de Curry-Howard . ${\displaystyle a\mapsto c_{a}}$ ${\displaystyle C}$ ${\displaystyle A}$ ${\displaystyle \forall (a\in A).R(a,c_{a})}$

Dependiendo del contexto, la palabra "función" puede usarse en asociación con un modelo particular de computación , y esto es a priori más restringido que lo que se discute en el contexto de la teoría de conjuntos actual. Una noción de programa se formaliza mediante "funciones" recursivas parciales en la teoría de la computabilidad . Pero tenga cuidado de que aquí la palabra "función" se usa de una manera que también comprende funciones parciales , y no solo "funciones totales". Las comillas se usan aquí para mayor claridad, ya que en un contexto de teoría de conjuntos técnicamente no hay necesidad de hablar de funciones totales , porque este requisito es parte de la definición de una función teórica de conjuntos y los espacios de funciones parciales se pueden modelar mediante uniones. Al mismo tiempo, cuando se combina con una aritmética formal, los programas de funciones parciales brindan una noción particularmente nítida de totalidad para funciones. Por el teorema de la forma normal de Kleene , cada función recursiva parcial sobre los naturales calcula, para los valores en los que termina, lo mismo que , para algún índice de programa de función parcial , y cualquier índice constituirá alguna función parcial. Un programa puede asociarse con un y puede decirse que es -total siempre que una teoría demuestre , donde equivale a un programa recursivo primitivo y está relacionado con la ejecución de . Kreisel demostró que la clase de funciones recursivas parciales demostradas como -totales por no se enriquece cuando se añade . ^[17] Como predicado en , esta totalidad constituye un subconjunto indecidible de índices, lo que pone de relieve que el mundo recursivo de funciones entre los naturales ya está capturado por un conjunto dominado por . Como tercera advertencia, tenga en cuenta que esta noción se refiere realmente a programas y que varios índices constituirán de hecho la misma función, en el sentido extensional . ${\displaystyle a\mapsto U(\mu w.T_{1}(e,a,w))}$ ${\displaystyle e\in {\mathbb {N} }}$ ${\displaystyle e}$ ${\displaystyle T_{1}}$ ${\displaystyle \forall a.\exists w.T_{1}(e,a,w)}$ ${\displaystyle T_{1}}$ ${\displaystyle w}$ ${\displaystyle e}$ ${\displaystyle T_{1}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle e}$ ${\displaystyle {\mathbb {N} }}$

Una teoría en lógica de primer orden , como las teorías de conjuntos axiomáticos discutidas aquí, viene con una noción conjunta de total y funcional para un predicado binario , a saber . Tales teorías se relacionan con programas solo indirectamente. Si denota la operación sucesora en un lenguaje formal de una teoría que se está estudiando, entonces cualquier número, p. ej. (el número tres), puede relacionarse metalógicamente con el numeral estándar, p. ej . . De manera similar, los programas en el sentido recursivo parcial pueden desarrollarse en predicados y los supuestos débiles son suficientes para que dicha traducción respete la igualdad de sus valores de retorno. Entre las subteorías finitamente axiomizables de , la aritmética clásica de Robinson cumple exactamente esto. Sus afirmaciones de existencia pretenden referirse solo a los números naturales y, en lugar de utilizar el esquema de inducción matemática completo para fórmulas aritméticas, los axiomas de las teorías postulan que cada número es cero o que existe un número predecesor para él. Centrándonos aquí en las funciones recursivas -totales, es un metateorema que el lenguaje de la aritmética las expresa mediante -predicados que codifican su gráfico de tal manera que las representa , en el sentido de que prueba o rechaza correctamente para cualquier par de números de entrada-salida y en la metateoría. Ahora bien, dado un que representa correctamente , el predicado definido por representa la función recursiva igualmente bien, y como esto explícitamente solo valida el valor de retorno más pequeño, la teoría también prueba la funcionalidad para todas las entradas en el sentido de . Dado un predicado que representa, entonces a costa de hacer uso de , uno siempre puede también probar sistemáticamente (es decir, con un ) que el gráfico es totalmente funcional. ^[18] ${\displaystyle R}$ ${\displaystyle \forall a.\exists !c.R(a,c)}$ ${\displaystyle S}$ ${\displaystyle {\mathrm {SSS0} }}$ ${\displaystyle {\underline {\mathrm {SSS0} }}=SSS0}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {Q}}}$ ${\displaystyle T_{1}}$ ${\displaystyle \Sigma _{1}}$ ${\displaystyle G}$ ${\displaystyle {\mathsf {Q}}}$ ${\displaystyle G({\underline {\mathrm {a} }},{\underline {\mathrm {c} }})}$ ${\displaystyle \mathrm {a} }$ ${\displaystyle \mathrm {c} }$ ${\displaystyle G}$ ${\displaystyle G_{\mathrm {least} }(a,c)}$ ${\displaystyle G(a,c)\land \forall (n<c).\neg G(a,n)}$ ${\displaystyle {\mathrm {a} }}$ ${\displaystyle {\mathsf {Q}}\vdash \exists !c.G_{\mathrm {least} }({\underline {\mathrm {a} }},c)}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle \forall a.}$

Qué predicados son demostrablemente funcionales para varias entradas, o incluso funcionales totales en su dominio, generalmente depende de los axiomas adoptados de una teoría y un cálculo de prueba. Por ejemplo, para el problema de detención diagonal , que no puede tener un índice -total, es -independiente si el predicado del grafo correspondiente en (un problema de decisión ) es totalmente funcional, pero implica que lo es. Las jerarquías de funciones teóricas de prueba proporcionan ejemplos de predicados que se ha demostrado que son totalmente funcionales en sistemas que van más allá de . Qué conjuntos se ha demostrado que existen constituyen una función total, en el sentido introducido a continuación, también depende siempre de los axiomas y del cálculo de prueba. Finalmente, nótese que la solidez de las afirmaciones de detención es una propiedad metalógica más allá de la consistencia, es decir, una teoría puede ser consistente y a partir de ella se puede demostrar que algún programa se detendrá eventualmente, a pesar de que esto nunca ocurra realmente cuando se ejecuta dicho programa. Más formalmente, suponer la consistencia de una teoría no implica que también sea aritméticamente -sólida . ${\displaystyle T_{1}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathbb {N} }\times \{0,1\}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \Sigma _{1}}$

Relaciones funcionales totales

En el lenguaje de la teoría de conjuntos, aquí se habla de una clase de función cuando y comprobadamente ${\displaystyle f\subset A\times C}$

${\displaystyle \forall (a\in A).\,\exists !(c\in C).\langle a,c\rangle \in f}$.

En particular, esta definición implica que el cuantificador pida explícitamente existencia, un aspecto que es particularmente importante en el contexto constructivo. En palabras: para cada , exige la existencia única de un de modo que . En el caso de que esto se cumpla, se puede usar la notación de corchetes de aplicación de funciones y escribir . La propiedad anterior puede entonces enunciarse como . Esta notación puede extenderse a la igualdad de valores de funciones. Algunas conveniencias de notación que involucran la aplicación de funciones solo funcionarán cuando un conjunto haya sido establecido como una función. Sea (también escrito ) la clase de conjuntos que cumplen la propiedad de función. Esta es la clase de funciones de a en una teoría de conjuntos pura. A continuación, también se usa la notación para , con el fin de distinguirla de la exponenciación ordinal. Cuando las funciones se entienden como simples gráficos de funciones como aquí, la proposición de pertenencia también se escribe . Los valores booleanos se encuentran entre las clases discutidas en la siguiente sección. ${\displaystyle a}$ ${\displaystyle c}$ ${\displaystyle \langle a,c\rangle \in f}$ ${\displaystyle f(a)=c}$ ${\displaystyle \forall (a\in A).\,\exists !(c\in C).f(a)=c}$ ${\displaystyle C^{A}}$ ${\displaystyle ^{A}C}$ ${\displaystyle A}$ ${\displaystyle C}$ ${\displaystyle x\to y}$ ${\displaystyle y^{x}}$ ${\displaystyle f\in C^{A}}$ ${\displaystyle f\colon A\to C}$ ${\displaystyle \chi _{B}\colon A\to \{0,1\}}$

Por construcción, cualquier función de este tipo respeta la igualdad en el sentido de que , para cualquier entrada de . Vale la pena mencionar esto ya que también existen conceptos más amplios de "rutinas de asignación" u "operaciones" en la literatura matemática, que en general pueden no respetar esto. También se han definido variantes de la definición de predicado funcional que utilizan relaciones de separación en setoides . Un subconjunto de una función sigue siendo una función y el predicado de la función también puede probarse para conjuntos de codominios elegidos ampliados. Como se señaló, se debe tener cuidado con la nomenclatura "función", una palabra que se usa en la mayoría de los marcos matemáticos. Cuando un conjunto de funciones en sí no está ligado a un codominio particular, entonces este conjunto de pares también es miembro de un espacio de funciones con un codominio más grande. Esto no sucede cuando con la palabra se denota el subconjunto de pares emparejados con un conjunto de codominios, es decir, una formalización en términos de . Esto es principalmente una cuestión de contabilidad, pero afecta cómo se definen otros predicados, cuestión de tamaño. Esta elección también se aplica simplemente en algunos marcos matemáticos. Consideraciones similares se aplican a cualquier tratamiento de funciones parciales y sus dominios. ${\displaystyle (x=y)\to f(x)=f(y)}$ ${\displaystyle A}$ ${\displaystyle (A\times C)\times \{C\}}$

Si tanto el dominio como el codominio considerado son conjuntos, entonces el predicado de función anterior solo involucra cuantificadores acotados. Nociones comunes como inyectividad y sobreyectividad también se pueden expresar de manera acotada, y por lo tanto también lo es la biyectividad . Ambas se vinculan con nociones de tamaño. Es importante destacar que la existencia de inyección entre dos conjuntos proporciona un preorden . Una clase de potencia no inyecta en su conjunto subyacente y este último no se asigna al primero. La sobreyectividad es formalmente una definición más compleja. Nótese que la inyectividad se definirá positivamente, no por su contrapositivo, que es una práctica común en las matemáticas clásicas. La versión sin negaciones a veces se llama débilmente inyectiva. La existencia de colisiones de valores es una noción fuerte de no inyectividad. Y con respecto a la sobreyectividad, existen consideraciones similares para la producción de valores atípicos en el codominio. ${\displaystyle A}$ ${\displaystyle C}$

El que una subclase (o predicado, para el caso) pueda juzgarse como un conjunto de funciones, o incluso como funcional total para empezar, dependerá de la fuerza de la teoría, es decir, de los axiomas que se adopten. Y, en particular, una clase general también podría cumplir el predicado definitorio anterior sin ser una subclase del producto , es decir, la propiedad no expresa más ni menos que funcionalidad con respecto a las entradas de . Ahora bien, si el dominio es un conjunto, el principio de comprensión de funciones, también llamado axioma de elección única o no elección, dice que una función como conjunto, con algún codominio, existe bien. (Y este principio es válido en una teoría como . Compárese también con el axioma de reemplazo ). Es decir, la información de mapeo existe como conjunto y tiene un par para cada elemento en el dominio. Por supuesto, para cualquier conjunto de alguna clase, siempre se puede asociar un elemento único del singleton , lo que demuestra que el mero hecho de que un rango elegido sea un conjunto no basta para que se le conceda un conjunto de funciones. Es un metateorema para las teorías que contienen que agregar un símbolo de función para una función de clase total probada es una extensión conservadora, a pesar de que esto cambia formalmente el alcance de la separación acotada . En resumen, en el contexto de la teoría de conjuntos, el enfoque está en capturar relaciones totales particulares que son funcionales. Para delinear la noción de función en las teorías de la subsección anterior (un predicado lógico 2-ario definido para expresar un gráfico de funciones, junto con una proposición de que es total y funcional) a partir de la noción teórica de conjuntos "material" aquí, uno puede llamar explícitamente al último gráfico de una función , una función o función de conjunto . El esquema axiomático de Reemplazo también puede formularse en términos de los rangos de tales funciones de conjunto. ${\displaystyle A\times C}$ ${\displaystyle A}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle 1}$ ${\displaystyle {\mathsf {BCST}}}$

Finitud

Se definen tres nociones distintas que involucran sobreyecciones. Para que un conjunto general sea ( Bishop -) finito significará que hay una función biyectiva para un natural. Si se prueba que la existencia de tal biyección es imposible, el conjunto se llama no finito . En segundo lugar, para una noción más débil que finito, estar indexado finitamente (o Kuratowski -finito) significará que hay una sobreyección de un número natural de von Neumann sobre él. En términos de programación, los elementos de tal conjunto son accesibles en un bucle for (final) , y solo aquellos, mientras que puede no ser decidible si ocurrió repetición. En tercer lugar, llame a un conjunto subfinito si es el subconjunto de un conjunto finito, que por lo tanto inyecta en ese conjunto finito. Aquí, un bucle for accederá a todos los miembros del conjunto, pero también posiblemente a otros. Para otra noción combinada, una más débil que la de indexación finita, estar indexado subfinitamente significa estar en la imagen sobreyectiva de un conjunto subfinito, y en este caso simplemente significa ser el subconjunto de un conjunto indexado finitamente, lo que significa que el subconjunto también puede tomarse en el lado de la imagen en lugar del lado del dominio. Un conjunto que exhibe cualquiera de esas nociones puede entenderse como mayorizado por un conjunto finito, pero en el segundo caso la relación entre los miembros del conjunto no se entiende necesariamente por completo. En el tercer caso, validar la pertenencia al conjunto es generalmente más difícil, y ni siquiera es necesario entender por completo la pertenencia de su miembro con respecto a algún superconjunto del conjunto. La afirmación de que ser finito es equivalente a ser subfinito, para todos los conjuntos, es equivalente a . Se pueden definir más propiedades de finitud para un conjunto , por ejemplo, expresando la existencia de algún natural lo suficientemente grande como para que una cierta clase de funciones sobre los naturales siempre no se asignen a elementos distintos en . Una definición considera alguna noción de no inyectividad en . Otras definiciones consideran funciones como un superconjunto fijo con más elementos. ${\displaystyle {\mathsf {ETCS}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle X}$

La terminología para las condiciones de finitud e infinitud puede variar. En particular, los conjuntos indexados subfinitamente (una noción que necesariamente implica sobreyecciones) a veces se denominan subfinitos (que se pueden definir sin funciones). La propiedad de estar indexado finitamente también podría denotarse como "finitamente contable", para ajustarse a la lógica de denominación, pero algunos autores también la denominan finitamente enumerable (lo que puede resultar confuso, ya que sugiere una inyección en la otra dirección). En relación con esto, la existencia de una biyección con un conjunto finito no se ha establecido; se puede decir que un conjunto no es finito, pero este uso del lenguaje es entonces más débil que afirmar que el conjunto no es finito. La misma cuestión se aplica a los conjuntos contables (no contable demostrado frente a no contable demostrado), etcétera. Una función sobreyectiva también puede denominarse enumeración.

Infinitud

El conjunto en sí es claramente ilimitado. De hecho, para cualquier sobreyección desde un rango finito sobre , se puede construir un elemento que sea diferente de cualquier elemento en el rango de funciones. Cuando sea necesario, esta noción de infinitud también se puede expresar en términos de una relación de apartamiento en el conjunto en cuestión. No ser finito de Kuratowski implica ser no finito y, de hecho, los naturales no serán finitos en ningún sentido. Comúnmente, la palabra infinito se usa para la noción negativa de ser no finito. Además, observe que , a diferencia de cualquiera de sus miembros, se puede poner en biyección con algunos de sus subconjuntos no acotados propios, por ejemplo, aquellos de la forma para cualquier . Esto valida las formulaciones de infinito de Dedekind . Entonces, de manera más general que la propiedad de infinitud en la sección anterior sobre límites numéricos, se puede llamar a un conjunto infinito en el sentido lógico positivo si se puede inyectar en él. Un conjunto que está incluso en biyección con puede llamarse infinito contable. Un conjunto es Tarski-infinito si hay una cadena de subconjuntos -crecientes del mismo. Aquí cada conjunto tiene nuevos elementos comparados con su predecesor y la definición no habla de conjuntos que crecen en rango. De hecho, hay muchas propiedades que caracterizan la infinitud incluso en la teoría clásica y esa teoría no prueba que todos los conjuntos no finitos sean infinitos en el sentido de existencia de inyección, aunque se cumple cuando se supone además una elección contable. sin ninguna elección incluso permite cardinales aparte de los números aleph , y entonces puede haber conjuntos que nieguen ambas propiedades anteriores, es decir, son tanto no-Dedekind-infinitos como no finitos (también llamados conjuntos infinitos Dedekind-finitos). ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle w_{m}:=\{k\in \omega \mid k>m\}}$ ${\displaystyle m\in \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \subset }$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {ZF}}}$

Llamemos a un conjunto habitado contable si existe una sobreyección de sobre él y subcontable si esto puede hacerse a partir de algún subconjunto de . Llamemos a un conjunto enumerable si existe una inyección a , que hace que el conjunto sea discreto. Cabe destacar que todas estas son afirmaciones de existencia de funciones. El conjunto vacío no está habitado, pero generalmente se considera también contable, y observemos que el conjunto sucesor de cualquier conjunto contable es contable. El conjunto es trivialmente infinito, contable y enumerable, como lo atestigua la función identidad. También aquí, en las teorías clásicas fuertes muchas de estas nociones coinciden en general y, como resultado, las convenciones de nomenclatura en la literatura son inconsistentes. Un conjunto infinito y contable es equinumeros a . ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$

También hay varias formas de caracterizar lógicamente la noción negativa. La noción de incontabilidad, en el sentido de no ser contable, también se analiza junto con el axioma de exponenciación más adelante. Otra noción de incontabilidad de se da cuando se puede producir un miembro en el complemento de cualquiera de los subconjuntos contables de . Se pueden definir más propiedades de finitud como negaciones de tales propiedades, etcétera. ${\displaystyle X}$ ${\displaystyle X}$

Funciones características

La separación nos permite eliminar subconjuntos de productos , al menos cuando se describen de manera acotada. Dado cualquier , ahora se llega a razonar sobre clases como ${\displaystyle A\times C}$ ${\displaystyle B\subset A}$

${\displaystyle X_{B}:={\big \{}\langle x,y\rangle \in A\times \{0,1\}\mid (x\in B\land y=1)\lor (x\notin B\land y=0){\big \}}.}$

Desde entonces , uno tiene ${\displaystyle \neg (0=1)}$

${\displaystyle {\big (}a\in B\ \leftrightarrow \,\langle a,1\rangle \in X_{B}{\big )}\,\land \,{\big (}a\notin B\ \leftrightarrow \,\langle a,0\rangle \in X_{B}{\big )}}$

y entonces

${\displaystyle {\big (}a\in B\lor a\notin B{\big )}\ \leftrightarrow \ \exists !(y\in \{0,1\}).\langle a,y\rangle \in X_{B}}$.

Pero tenga en cuenta que en ausencia de cualquier axioma no constructivo puede en general no ser decidible , ya que se requiere una prueba explícita de cualquiera de los dos disyuntos. Constructivamente, cuando no se puede presenciar para todos los , o no se puede probar la unicidad de los términos asociados con cada uno , entonces no se puede juzgar que la colección comprendida sea totalmente funcional. Caso en cuestión: la derivación clásica de Schröder-Bernstein se basa en el análisis de casos, pero para constituir una función , los casos particulares deben ser realmente especificables, dada cualquier entrada del dominio. Se ha establecido que Schröder-Bernstein no puede tener una prueba sobre la base de principios constructivos adicionales. ^[19] Entonces, en la medida en que la inferencia intuicionista no vaya más allá de lo que se formaliza aquí, no hay una construcción genérica de una biyección a partir de dos inyecciones en direcciones opuestas. ${\displaystyle a\in B}$ ${\displaystyle \exists (y\in \{0,1\}).\langle x,y\rangle \in X_{B}}$ ${\displaystyle x\in A}$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle {\mathsf {IZF}}}$

Pero siendo compatible con , el desarrollo en esta sección todavía siempre permite que "función en " sea interpretada como un objeto completo que tampoco está necesariamente dado como una secuencia similar a una ley . Se pueden encontrar aplicaciones en los modelos comunes para afirmaciones sobre probabilidad, por ejemplo, afirmaciones que involucran la noción de "recibir" una secuencia aleatoria interminable de lanzamientos de moneda, incluso si muchas predicciones también se pueden expresar en términos de diferenciales . ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle \omega }$

Si de hecho se da una función , es la función característica la que realmente decide la pertenencia a algún subconjunto separable y ${\displaystyle \chi _{B}\colon A\to \{0,1\}}$ ${\displaystyle B\subset A}$

${\displaystyle B=\{n\in \omega \mid \chi _{B}(n)=1\}.}$

Por convención, el subconjunto desprendible , así como cualquier equivalente de las fórmulas y (con libre) puede denominarse propiedad decidible o conjunto en . ${\displaystyle B}$ ${\displaystyle \chi _{B}}$ ${\displaystyle n\in B}$ ${\displaystyle \chi _{B}(n)=1}$ ${\displaystyle n}$ ${\displaystyle A}$

Se puede decir que una colección es buscable si la existencia es realmente decidible, ${\displaystyle A}$ ${\displaystyle \chi _{B}}$

${\displaystyle \exists (x\in A).\chi _{B}(x)=1\ \lor \ \forall (x\in A).\chi _{B}(x)=0.}$

Ahora consideremos el caso . Si , digamos, entonces el rango de es un conjunto habitado, contado, por Reemplazo. Sin embargo, no necesita ser de nuevo un conjunto decidible en sí mismo, ya que la afirmación es equivalente a la bastante fuerte . Además, también es equivalente a y por lo tanto uno puede enunciar proposiciones indecidibles sobre también cuando la pertenencia a es decidible. Esto también se desarrolla así clásicamente en el sentido de que las afirmaciones sobre pueden ser independientes , pero cualquier teoría clásica afirma no obstante la proposición conjunta . Consideremos el conjunto de todos los índices de pruebas de una inconsistencia de la teoría en cuestión, en cuyo caso la afirmación universalmente cerrada es una afirmación de consistencia. En términos de principios aritméticos, suponiendo la decidibilidad de esto sería - o aritmética - . Esto y el relacionado más fuerte , o aritmética - , se analizan a continuación. ${\displaystyle A=\omega }$ ${\displaystyle \chi _{B}(0)=0}$ ${\displaystyle \{0\}\subset R\subset \{0,1\}}$ ${\displaystyle \chi _{B}}$ ${\displaystyle R}$ ${\displaystyle R=\{0\}}$ ${\displaystyle \forall n.\chi _{B}(n)=0}$ ${\displaystyle R=\{0\}}$ ${\displaystyle B=\{\}}$ ${\displaystyle B}$ ${\displaystyle B}$ ${\displaystyle B}$ ${\displaystyle B=\{\}\lor \neg (B=\{\})}$ ${\displaystyle B}$ ${\displaystyle B=\{\}}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle \forall }$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {LPO} }}$ ${\displaystyle \exists }$ ${\displaystyle {\mathrm {PEM} }}$

Testigo de la separación

La identidad de indiscernibles , que en el contexto de primer orden es un principio de orden superior, sostiene que la de dos términos y requiere que todos los predicados concuerden en ellos. Y entonces, si existe un predicado que distingue dos términos y en el sentido de que , entonces el principio de identidad de indiscernibles implica que los dos términos no coinciden. Una forma de esto puede expresarse teóricamente en conjuntos: pueden considerarse separados si existe un subconjunto tal que uno es miembro y el otro no. Restringido a subconjuntos separables, esto también puede formularse de manera concisa utilizando funciones características . De hecho, esto último no depende realmente de que el codominio sea un conjunto binario: Se rechaza la igualdad, es decir, se prueba, tan pronto como se establece que no todas las funciones en validan , una condición lógicamente negativa. ${\displaystyle x=y}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle P(x)\land \neg P(y)}$ ${\displaystyle x,y\in A}$ ${\displaystyle B\subset A}$ ${\displaystyle \chi _{B}\in \{0,1\}^{A}}$ ${\displaystyle x\neq y}$ ${\displaystyle f}$ ${\displaystyle A}$ ${\displaystyle f(x)=f(y)}$

Se puede definir en cualquier conjunto la relación de separación lógicamente positiva ${\displaystyle A}$

${\displaystyle x\,\#_{A}\,y\,:=\,\exists (f\in {\mathbb {N} }^{A}).f(x)\neq f(y)}$

Como los naturales son discretos, para estas funciones la condición negativa es equivalente a la más débil . Nuevamente, en palabras, la igualdad de y implica que ninguna coloración puede distinguirlas, y por lo tanto, para descartar la primera (es decir, para probar ), uno simplemente debe descartar la segunda. ${\displaystyle \neg \neg (x\,\#_{A}\,y)}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle f\in {\mathbb {N} }^{A}}$ ${\displaystyle x\neq y}$

Conjuntos computables

Volviendo a una mayor generalidad, dado un predicado general sobre los números (digamos uno definido a partir del predicado T de Kleene ), sea nuevamente ${\displaystyle Q}$

${\displaystyle B:=\{n\in \omega \mid Q(n)\}.}$

Dado cualquier natural , entonces ${\displaystyle n\in \omega }$

${\displaystyle {\big (}Q(n)\lor \neg Q(n){\big )}\leftrightarrow {\big (}n\in B\lor n\notin B{\big )}.}$

En la teoría clásica de conjuntos, por y por tanto el medio excluido también es válido para la pertenencia a una subclase. Si la clase no tiene límite numérico, entonces recorrer sucesivamente los números naturales y, por tanto, "enumerar" todos los números en simplemente omitiendo aquellos con , clásicamente siempre constituye una secuencia sobreyectiva creciente . Allí, se puede obtener una función biyectiva . De esta manera, la clase de funciones en las teorías de conjuntos clásicas típicas es probadamente rica, ya que también contiene objetos que están más allá de lo que sabemos que es efectivamente computable , o programáticamente enumerable en la praxis. ${\displaystyle \forall (n\in \omega ).Q(n)\lor \neg Q(n)}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle B}$ ${\displaystyle n}$ ${\displaystyle B}$ ${\displaystyle n\notin B}$ ${\displaystyle b\colon \omega \twoheadrightarrow B}$

En la teoría de la computabilidad , los conjuntos computables son rangos de funciones totales no decrecientes en el sentido recursivo , en el nivel de la jerarquía aritmética , y no más arriba. Decidir un predicado en ese nivel equivale a resolver la tarea de encontrar eventualmente un certificado que valide o rechace la membresía. Como no todos los predicados son computablemente decidibles, también la teoría por sí sola no afirmará (probará) que todos los no acotados son el rango de alguna función biyectiva con dominio . Véase también el esquema de Kripke. Nótese que la Separación acotada, no obstante, prueba que los predicados aritméticos más complicados todavía constituyen conjuntos, siendo el siguiente nivel los computablemente enumerables en . ${\displaystyle \Sigma _{1}^{0}\cap \Pi _{1}^{0}=\Delta _{1}^{0}}$ ${\displaystyle Q}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle B\subset \omega }$ ${\displaystyle \omega }$ ${\displaystyle \Sigma _{1}^{0}}$

Existe un amplio corpus de nociones de teoría de la computabilidad sobre cómo se relacionan entre sí los subconjuntos generales de los números naturales. Por ejemplo, una forma de establecer una biyección de dos de esos conjuntos es relacionándolos mediante un isomorfismo computable , que es una permutación computable de todos los números naturales. Este último puede, a su vez, establecerse mediante un par de inyecciones particulares en direcciones opuestas.

Criterios de acotación

Cualquier subconjunto se inyecta en . Si es decidible y está habitado por , la secuencia ${\displaystyle B\subset \omega }$ ${\displaystyle \omega }$ ${\displaystyle B}$ ${\displaystyle y_{0}\in B}$

${\displaystyle q:={\big \{}\langle x,y\rangle \in \omega \times B\mid (x\in B\land y=x)\lor (x\notin B\land y=y_{0}){\big \}}}$

es decir

${\displaystyle q(x):={\begin{cases}x&x\in B\\y_{0}&x\notin B\\\end{cases}}}$

es sobreyectiva sobre , lo que la convierte en un conjunto contable. Esa función también tiene la propiedad . ${\displaystyle B}$ ${\displaystyle \forall (x\in B).q(x)=x}$

Consideremos ahora un conjunto numerable que está acotado en el sentido definido anteriormente. Cualquier secuencia que tome valores en también está limitada numéricamente y, en particular, no excede la función identidad en sus índices de entrada. Formalmente, ${\displaystyle R\subset \omega }$ ${\displaystyle R}$

${\displaystyle \forall (r\colon \omega \to R).\exists (m\in \omega ).\forall (k\in \omega ).k>m\to r(k)<k}$

Un conjunto tal que esta afirmación de delimitación flexible se cumple para todas las secuencias que toman valores en (o una formulación equivalente de esta propiedad) se llama pseudo-limitado . La intención de esta propiedad sería capturar que finalmente se agote, aunque ahora esto se expresa en términos del espacio de funciones (que es más grande que en el sentido de que siempre inyecta en ). La noción relacionada familiar de la teoría del espacio vectorial topológico se formula en términos de proporciones que tienden a cero para todas las secuencias ( en la notación anterior). Para un conjunto habitado y decidible, la validez de la pseudo-limitación, junto con la secuencia de conteo definida anteriormente, otorga un límite para todos los elementos de . ${\displaystyle I}$ ${\displaystyle I}$ ${\displaystyle I\subset \omega }$ ${\displaystyle I^{\omega }}$ ${\displaystyle I}$ ${\displaystyle I}$ ${\displaystyle I^{\omega }}$ ${\displaystyle {\tfrac {r(k)}{k}}}$ ${\displaystyle I}$

El principio de que cualquier subconjunto habitado y pseudoacotado de eso es simplemente contable (pero no necesariamente decidible) siempre es también acotado se llama - . El principio también se cumple en general en muchos marcos constructivos, como la teoría de base markoviana , que es una teoría que postula exclusivamente secuencias similares a leyes con buenas propiedades de terminación de búsqueda de números. Sin embargo, - es independiente de . ${\displaystyle \omega }$ ${\displaystyle \mathrm {BD} }$ ${\displaystyle {\mathbb {N} }}$ ${\displaystyle {\mathsf {HA}}+{\mathrm {ECT} }_{0}+{\mathrm {MP} }}$ ${\displaystyle \mathrm {BD} }$ ${\displaystyle {\mathbb {N} }}$ ${\displaystyle {\mathsf {IZF}}}$

Funciones de elección

Ni siquiera la teoría clásica prueba que cada unión de un conjunto numerable de conjuntos de dos elementos sea nuevamente numerable. De hecho, se han definido modelos de que niegan la numerabilidad de tal unión numerable de pares. Suponiendo que la elección es numerable, se descarta ese modelo como interpretación de la teoría resultante. Este principio sigue siendo independiente de - Una estrategia de prueba ingenua para esa afirmación falla al explicar infinitas instancias existenciales . ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {ZF}}}$

Un principio de elección postula que ciertas selecciones siempre pueden hacerse de manera conjunta en el sentido de que también se manifiestan como una función de conjunto única en la teoría. Como con cualquier axioma independiente, esto aumenta las capacidades de prueba al tiempo que restringe el alcance de las posibles interpretaciones (teóricas de modelos) de la teoría (sintáctica). Una afirmación de existencia de función a menudo puede traducirse a la existencia de inversas, ordenaciones, etc. Además, la elección implica afirmaciones sobre cardinalidades de diferentes conjuntos, por ejemplo, implican o descartan la numerabilidad de conjuntos. Agregar la elección completa a no prueba ningún teorema nuevo , pero es estrictamente no constructivo, como se muestra a continuación. El desarrollo aquí procede de una manera agnóstica a cualquiera de las variantes descritas a continuación. ^[20] ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle \Pi _{4}^{1}}$

• Axioma de elección contable (o ): Si , se puede formar el conjunto de relaciones uno-a-muchos . El axioma de elección contable concedería que siempre que , se puede formar una función que asigne cada número a un valor único. La existencia de tales secuencias no es generalmente demostrable sobre la base de y la elección contable no es -conservadora sobre esa teoría. La elección contable en conjuntos generales también se puede debilitar aún más. Una consideración común es restringir las posibles cardinalidades del rango de , dando la elección contable débil en conjuntos contables, finitos o incluso simplemente binarios ( ). Se puede considerar la versión de elección contable para funciones en (llamada o ), como lo implica el principio de tesis de Church constructivo , es decir, postulando que todas las relaciones aritméticas totales son recursivas. en aritmética puede entenderse como una forma de axioma de elección. Otro medio de debilitar la elección contable es restringiendo las definiciones involucradas con respecto a su lugar en las jerarquías sintácticas (por ejemplo, - ). El lema débil de König , que rompe las matemáticas estrictamente recursivas como se analiza más adelante, es más fuerte que - y a veces se lo considera como la captura de una forma de elección contable. En presencia de una forma débil de elección contable, el lema se vuelve equivalente al principio no constructivo de sabor más lógico, . Constructivamente, se requiere una forma débil de elección para los reales de Cauchy que se comportan bien . La elección contable no es válida en la lógica interna de un topos general , que puede verse como modelos de teorías de conjuntos constructivas. ${\displaystyle {\mathrm {AC} _{\omega }}}$ ${\displaystyle {\mathrm {CC} }}$ ${\displaystyle g\colon \omega \to z}$ ${\displaystyle \{\langle n,u\rangle \mid n\in \omega \land u\in g(n)\}}$ ${\displaystyle \forall (n\in \omega ).\exists u.u\in g(n)}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle \Sigma _{4}^{1}}$ ${\displaystyle g}$ ${\displaystyle {\mathrm {AC} _{\omega ,2}}}$ ${\displaystyle \omega }$ ${\displaystyle {\mathrm {AC} _{\omega ,\omega }}}$ ${\displaystyle {\mathrm {AC} _{00}}}$ ${\displaystyle {\mathrm {CT} _{0}}}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {AC} _{\omega ,2}}}$ ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {AC} _{\omega ,2}}}$ ${\displaystyle {\mathrm {LLPO} }}$
• Axioma de elección dependiente : La elección contable está implícita en el axioma más general de elección dependiente, que extrae una secuencia en un habitado , dada cualquier relación entera . En la teoría de conjuntos, esta secuencia es nuevamente un conjunto infinito de pares, un subconjunto de . Por lo tanto, se permite pasar de varias declaraciones de existencia a la existencia de funciones, que en sí misma otorga declaraciones de existencia única, para cada natural. Una formulación apropiada de elección dependiente se adopta en varios marcos constructivos, por ejemplo, por algunas escuelas que entienden las secuencias interminables como construcciones en curso en lugar de objetos completados. Al menos parecen benignos aquellos casos en los que, para cualquier , la existencia del siguiente valor puede validarse de manera computable. La función recursiva correspondiente , si existe, se conceptualiza entonces como capaz de devolver un valor en infinitas entradas potenciales , pero estas no tienen que evaluarse todas juntas a la vez. También se cumple en muchos modelos de realizabilidad . En la condición del teorema de recursión formalmente similar , ya se nos da una elección única en cada paso, y ese teorema nos permite combinarlas en una función en . Así también con se pueden considerar formas del axioma con restricciones en . A través del axioma de separación acotada en , el principio también es equivalente a un esquema en dos variables de predicado acotadas: Manteniendo todos los cuantificadores que abarcan , se puede limitar aún más este dominio de conjunto utilizando una variable de predicado unario, mientras que también se utiliza cualquier predicado 2-ario en lugar del conjunto de relación . ${\displaystyle {\mathrm {DC} }}$ ${\displaystyle z}$ ${\displaystyle R\subset z\times z}$ ${\displaystyle \omega \times z}$ ${\displaystyle x\in z}$ ${\displaystyle \exists (y\in z).xRy}$ ${\displaystyle \omega \to z}$ ${\displaystyle n\in \omega }$ ${\displaystyle \omega }$ ${\displaystyle {\mathrm {DC} }}$ ${\displaystyle R}$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle z}$ ${\displaystyle \Delta _{0}}$ ${\displaystyle \Delta _{0}}$ ${\displaystyle R}$
• Elección dependiente relativizada : este es el esquema que utiliza solo dos clases generales, en lugar de requerir que y sean conjuntos. El dominio de la función de elección que se le otorga a la existencia sigue siendo solo . Sobre , implica una inducción matemática completa, que, a su vez, permite la definición de la función en a través del esquema de recursión. Cuando se restringe a -definiciones, todavía implica una inducción matemática para -predicados (con un cuantificador existencial sobre conjuntos) así como . En , el esquema es equivalente a . ${\displaystyle {\mathrm {RDC} }}$ ${\displaystyle z}$ ${\displaystyle R}$ ${\displaystyle \omega }$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle \omega }$ ${\displaystyle {\mathrm {RDC} }}$ ${\displaystyle \Delta _{0}}$ ${\displaystyle \Sigma _{1}}$ ${\displaystyle {\mathrm {DC} }}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathrm {RDC} }}$ ${\displaystyle {\mathrm {DC} }}$
• ${\displaystyle \Pi \Sigma }$- : Una familia de conjuntos es más controlable si viene indexada por una función. Un conjunto es una base si todas las familias indexadas de conjuntos sobre él tienen una función de elección , es decir . Una colección de conjuntos que contiene y sus elementos y que está cerrada tomando sumas y productos indexados (ver tipo dependiente ) se llama -cerrada. Si bien el axioma de que todos los conjuntos en la clase -cerrada más pequeña son una base necesita algo de trabajo para formularse, es el principio de elección más fuerte sobre el que se cumple en la interpretación teórica del tipo . ${\displaystyle \mathrm {AC} }$ ${\displaystyle b}$ ${\displaystyle i_{s}\colon b\to s}$ ${\displaystyle f_{s}}$ ${\displaystyle \forall (x\in b).f_{s}(x)\in i_{s}(x)}$ ${\displaystyle \omega }$ ${\displaystyle \Pi \Sigma }$ ${\displaystyle \Pi \Sigma }$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {ML_{1}V}}}$
• Axioma de elección : Este es el postulado de la función de elección "completa" que concierne a los dominios que son conjuntos generales que contienen conjuntos habitados, con el codominio dado como su unión general. Dada una colección de conjuntos tales que la lógica permite hacer una elección en cada uno, el axioma garantiza que existe una función de conjunto que captura conjuntamente una elección en todos. Se formula típicamente para todos los conjuntos, pero también se ha estudiado en formulaciones clásicas para conjuntos solo hasta cualquier cardinalidad particular. Un ejemplo estándar es la elección en todos los subconjuntos habitados de los reales, que clásicamente es igual al dominio . Para esta colección no puede haber una prescripción de selección de elementos uniforme que constituya demostrablemente una función de elección sobre la base de . Además, cuando se restringe al álgebra de Borel de los reales, por sí solo no prueba la existencia de una función que seleccione un miembro de cada subconjunto no vacío medible por Lebesgue . (El conjunto es el σ-álgebra generada por los intervalos . Estrictamente incluye esos intervalos, en el sentido de , pero en también solo tiene la cardinalidad de los propios números reales.) Abundan las sorprendentes afirmaciones de existencia implicadas por el axioma. prueba que existe y entonces el axioma de elección también implica elección dependiente. Críticamente en el presente contexto, además también implica instancias de a través del teorema de Diaconescu. Para o teorías que lo extienden, esto significa que la elección completa al menos prueba para todas las -fórmulas, una consecuencia no constructiva no aceptable, por ejemplo, desde un punto de vista de computabilidad. Nótese que constructivamente, el lema de Zorn no implica elección: cuando la pertenencia a dominios de funciones no es decidible, la función extremal otorgada por ese principio no es siempre demostrablemente una función de elección en todo el dominio. ${\displaystyle {\mathrm {AC} }}$ ${\displaystyle \{z,\dots \}}$ ${\displaystyle {\mathcal {P}}_{\mathbb {R} }\setminus 1}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathcal {B}}({\mathbb {R} })}$ ${\displaystyle I:=\{(x,y\,]\mid x,y\in {\mathbb {R} }\}}$ ${\displaystyle I\subsetneq {\mathcal {B}}({\mathbb {R} })\subsetneq {\mathcal {P}}_{\mathbb {R} }}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle \omega }$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle \Delta _{0}}$

Teorema de Diaconescu

Para resaltar la fuerza de la Elección completa y su relación con cuestiones de intencionalidad , se deben considerar las clases

${\displaystyle a=\{u\in \{0,1\}\mid (u=0)\lor P\}}$

${\displaystyle b=\{u\in \{0,1\}\mid (u=1)\lor P\}}$

de la prueba del teorema de Diaconescu . Son tan contingentes como la proposición involucrada en su definición y no se ha demostrado que sean finitos. No obstante, la configuración implica varias consecuencias. Volviendo a la elaboración introductoria sobre el significado de dicha notación de clase conveniente, así como al principio de distributividad , . Por lo tanto, incondicionalmente, así como , y en particular están habitados. Como en cualquier modelo de aritmética de Heyting, utilizando el silogismo disyuntivo tanto y cada uno implica . Los dos enunciados son de hecho equivalentes a la proposición, como claramente . Este último también dice que la validez de significa y comparte todos los miembros, y hay dos de estos. Como son son entonces conjuntos, también por extensionalidad. A la inversa, suponiendo que son medios iguales para cualquier , validando todos los enunciados de pertenencia. Por lo tanto, se encuentra que tanto los enunciados de pertenencia como las igualdades son equivalentes a . El uso de los resultados contrapositivos en la equivalencia más débil de disyuntos . Por supuesto, explícitamente y de esta manera se encuentra realmente de qué manera los conjuntos pueden llegar a ser diferentes. Como las funciones conservan la igualdad por definición, de hecho se cumple para cualquier función con dominio . ${\displaystyle P}$ ${\displaystyle t\in a\leftrightarrow {\big (}t=0\lor (t=1\land P){\big )}}$ ${\displaystyle 0\in a}$ ${\displaystyle 1\in b}$ ${\displaystyle \neg (0=1)}$ ${\displaystyle 0\in b}$ ${\displaystyle 1\in a}$ ${\displaystyle P}$ ${\displaystyle P\to (a=\{0,1\}\land b=\{0,1\})}$ ${\displaystyle P}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle P\to (a=b\land \{a,b\}=\{a\})}$ ${\displaystyle x\in a\leftrightarrow x\in b}$ ${\displaystyle x}$ ${\displaystyle P}$ ${\displaystyle (P\lor \neg P)\leftrightarrow (a=b\lor \neg (a=b))}$ ${\displaystyle \neg P\to (a=\{0\}\land b=\{1\})}$ ${\displaystyle \neg {\big (}g(a)=g(b){\big )}\to \neg P}$ ${\displaystyle g}$ ${\displaystyle \{a,b\}}$

En lo que sigue, supongamos un contexto en el que se establece que son conjuntos, y por lo tanto conjuntos subfinitos. El axioma general de elección afirma la existencia de una función con . Es importante que los elementos del dominio de la función sean diferentes de los números naturales en el sentido de que a priori se sabe menos sobre los primeros. Al formar entonces la unión de las dos clases, es una condición necesaria pero también suficiente. Por lo tanto y se trata de funciones en un conjunto de dos valores distinguibles . Con la elección viene la conjunción en el codominio de la función, pero se sabe que los posibles valores de retorno de la función son solo o . Usando la distributividad, surge una lista de condiciones, otra disyunción. Ampliando lo que se establece entonces, se encuentra que tanto la igualdad como los conjuntos se cumplen, o que los valores de retorno son diferentes y pueden rechazarse. La conclusión es que el postulado de elección en realidad implica siempre que un axioma de separación permite la comprensión de conjuntos usando la proposición indecidible . ${\displaystyle a,b}$ ${\displaystyle f\colon \{a,b\}\to a\cup b}$ ${\displaystyle f(z)\in z}$ ${\displaystyle a,b}$ ${\displaystyle 0,1}$ ${\displaystyle u=0\lor u=1}$ ${\displaystyle a\cup b=\{0,1\}}$ ${\displaystyle f}$ ${\displaystyle f(a)\in a\land f(b)\in b}$ ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P\lor \neg P}$ ${\displaystyle P}$

Análisis del teorema de Diaconescu

Por lo tanto, la elección completa no es constructiva en la teoría de conjuntos tal como se define aquí. El problema es que cuando las proposiciones son parte de la comprensión de conjuntos (como cuando se usa para separar, y por lo tanto definir, las clases y de ), la noción de sus valores de verdad se ramifica en términos de conjunto de la teoría. La igualdad definida por el axioma teórico de conjuntos de extensionalidad , que en sí mismo no está relacionado con las funciones, a su vez acopla el conocimiento sobre la proposición a la información sobre los valores de la función. Para recapitular el paso final en términos de valores de función: por un lado, atestiguar implica y y esta conclusión también se aplica independientemente a atestiguar . Por otro lado, atestiguar implica que los dos argumentos de función no son iguales y esto descarta . En realidad, solo hay tres combinaciones, ya que el axioma de extensionalidad en la configuración dada hace que sea inconsistente. Entonces, si se debe preservar la lectura constructiva de la existencia, la elección completa puede no adoptarse en la teoría de conjuntos, porque la mera afirmación de la existencia de la función no realiza una función particular. ${\displaystyle P}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle \{0,1\}}$ ${\displaystyle f(a)=1}$ ${\displaystyle P}$ ${\displaystyle a=b}$ ${\displaystyle f(b)=0}$ ${\displaystyle f(a)=0\land f(b)=1}$ ${\displaystyle P}$ ${\displaystyle f(a)=1\land f(b)=0}$

Para entender mejor por qué no se puede esperar que se le conceda una función de elección definitiva (total) con dominio , considere candidatos a funciones ingenuas. En primer lugar, es necesario un análisis del dominio. La sobreyección atestigua que está indexado finitamente. Se observó que sus miembros son subfinitos y también habitados, ya que independientemente de que sea el caso de que y . Entonces, ingenuamente, esto parecería hacer un contendiente para una función de elección. Cuando se puede rechazar, entonces esta es de hecho la única opción. Pero en el caso de la demostrabilidad de , cuando , hay extensionalmente solo una posible entrada de función a una función de elección. Entonces, en esa situación, una función de elección tendría explícitamente tipo , por ejemplo y esto descartaría al contendiente inicial. Para general , el dominio de una posible función de elección no es concreto sino contingente y no probado finito. Al considerar la asignación funcional anterior , entonces ni declarar incondicionalmente ni es necesariamente consistente. Habiéndose identificado con , los dos candidatos descritos anteriormente pueden representarse simultáneamente mediante (lo cual tampoco se ha demostrado que sea finito) con el "valor de verdad de " subfinito dado como . Como , postular , o , o el principio clásico aquí implicaría de hecho que es un natural, de modo que el último conjunto constituye una función de elección en . Y como en el caso constructivo, dada una función de elección particular (un conjunto que contiene exactamente uno o exactamente dos pares), uno podría realmente inferir si o si se cumple. Viceversa, el tercer y último candidato puede capturarse como parte de , donde . Tal ya se había considerado en la sección anterior sobre el axioma de separación. Nuevamente, este último aquí es una función de elección clásica en cualquier caso también, donde funciona como una "cláusula if" (potencialmente indecidible). De manera constructiva, el dominio y los valores de tales funciones potenciales dependientes de - no se entienden lo suficiente como para demostrar que son una relación funcional total en . ${\displaystyle \{a,b\}}$ ${\displaystyle \{\langle 0,a\rangle ,\langle 1,b\rangle \}}$ ${\displaystyle \{a,b\}}$ ${\displaystyle P}$ ${\displaystyle 0\in a}$ ${\displaystyle 1\in b}$ ${\displaystyle f=\{\langle a,0\rangle ,\langle b,1\rangle \}}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle \{a,b\}=\{a\}}$ ${\displaystyle f\colon \{a\}\to \{0,1\}}$ ${\displaystyle f=\{\langle a,0\rangle \}}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle f(a)=0}$ ${\displaystyle f(b)=1}$ ${\displaystyle f(b)=0}$ ${\displaystyle 1}$ ${\displaystyle \{0\}}$ ${\displaystyle f=\{\langle a,0\rangle ,\langle b,B_{\neg }\rangle \}}$ ${\displaystyle \neg P}$ ${\displaystyle B_{\neg }:=\{u\in \{0\}\mid \neg P\}}$ ${\displaystyle (P\to (B_{\neg }=0))\land (\neg P\to (B_{\neg }=1))}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle P\lor \neg P}$ ${\displaystyle B_{\neg }}$ ${\displaystyle f}$ ${\displaystyle \{0,1\}}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle f=\{\langle b,1\rangle \}}$ ${\displaystyle f=\{\langle a,B\rangle ,\langle b,1\rangle \}}$ ${\displaystyle B:=\{u\in \{0\}\mid P\}}$ ${\displaystyle B}$ ${\displaystyle f}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle \{0,1\}}$

Para la semántica computable, los axiomas de la teoría de conjuntos que postulan la existencia (total) de funciones conducen al requisito de detener las funciones recursivas. A partir de su gráfico de funciones en interpretaciones individuales, se pueden inferir las ramas tomadas por las "cláusulas if" que no estaban decididas en la teoría interpretada. Pero en el nivel de los marcos sintéticos, cuando se vuelven ampliamente clásicos al adoptar la elección completa, estas teorías de conjuntos extensionales contradicen la regla constructiva de Church.

La regularidad implica PEM

El axioma de elección otorga a la existencia una función asociada con cada colección de elementos habitados del tamaño de un conjunto , con la que se pueden elegir inmediatamente elementos únicos . El axioma de regularidad establece que para cada conjunto habitado en la colección universal, existe un elemento en , que no comparte elementos con . Esta formulación no implica funciones ni afirmaciones de existencia única, sino que garantiza directamente conjuntos con una propiedad específica. Como el axioma correlaciona afirmaciones de pertenencia en diferentes rangos, el axioma también termina implicando : ${\displaystyle s}$ ${\displaystyle t}$ ${\displaystyle s}$ ${\displaystyle t}$ ${\displaystyle s}$ ${\displaystyle s}$ ${\displaystyle t\in s}$ ${\displaystyle {\mathrm {PEM} }}$

La prueba de Choice anterior había usado y un conjunto particular . La prueba en este párrafo también supone que la separación se aplica a y usa , para lo cual por definición. Ya se explicó que y por lo tanto se puede probar que es medio excluido para en la forma . Ahora sea el miembro postulado con la propiedad de intersección vacía. El conjunto se definió como un subconjunto de y por lo tanto cualquier dado cumple la disyunción . La cláusula izquierda implica , mientras que para la cláusula derecha se puede usar que el elemento especial que no se interseca cumple . ${\displaystyle 1:=\{0\}}$ ${\displaystyle \{a,b\}}$ ${\displaystyle P}$ ${\displaystyle b}$ ${\displaystyle \{0\}\in b}$ ${\displaystyle P\leftrightarrow 0\in b}$ ${\displaystyle P}$ ${\displaystyle 0\in b\lor 0\notin b}$ ${\displaystyle t\in b}$ ${\displaystyle b}$ ${\displaystyle \{0,1\}}$ ${\displaystyle t\in b}$ ${\displaystyle t=0\lor t=1}$ ${\displaystyle t=0}$ ${\displaystyle 0\in b}$ ${\displaystyle t=1}$ ${\displaystyle t}$ ${\displaystyle (t=\{0\})\leftrightarrow (0\notin b)}$

Exigir que el conjunto de los naturales esté bien ordenado con respecto a su relación de orden estándar impone la misma condición al conjunto habitado . Por lo tanto, el principio del número mínimo tiene la misma implicación no constructiva. Al igual que con la prueba de la elección, el alcance de las proposiciones para las que se cumplen estos resultados está regido por el axioma de separación. ${\displaystyle b\subset \omega }$

Aritmética

Se han analizado los cuatro axiomas de Peano para y , que caracterizan al conjunto como modelo de los números naturales en la teoría de conjuntos constructivos . El orden " " de los números naturales se captura por la pertenencia " " en este modelo de von Neumann y este conjunto es discreto, es decir, también es decidible. ${\displaystyle 0}$ ${\displaystyle S}$ ${\displaystyle \omega }$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle <}$ ${\displaystyle \in }$ ${\displaystyle \phi (n,m):=(n=m)}$

Como se ha comentado, la inducción de fórmulas aritméticas es un teorema. Sin embargo, cuando no se asume la inducción matemática completa (o axiomas más fuertes como la separación completa) en una teoría de conjuntos, existe un escollo con respecto a la existencia de operaciones aritméticas. La teoría de primer orden de la aritmética de Heyting tiene la misma firma y axiomas no lógicos que la aritmética de Peano . Por el contrario, la firma de la teoría de conjuntos no contiene la adición " " o la multiplicación " ". en realidad no permite la recursión primitiva en las definiciones de función de lo que sería (donde " " aquí denota el producto cartesiano del conjunto, que no debe confundirse con la multiplicación anterior). De hecho, a pesar de tener el axioma de reemplazo, la teoría no prueba que haya un conjunto que capture la función de adición . En la siguiente sección, se aclara qué axioma teórico de conjuntos puede afirmarse para probar la existencia de este último como un conjunto de funciones, junto con su relación deseada con cero y sucesor. ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle +}$ ${\displaystyle \times }$ ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle \omega }$ ${\displaystyle h\colon (x\times \omega )\to y}$ ${\displaystyle \times }$ ${\displaystyle +\colon (\omega \times \omega )\to \omega }$

Mucho más allá del predicado de igualdad, el modelo aritmético obtenido valida

${\displaystyle {\mathsf {HA}}\vdash \forall n.\forall m.{\big (}\phi (n,m)\lor \neg \phi (n,m){\big )}}$

para cualquier fórmula sin cuantificadores. De hecho, es -conservativa sobre y la eliminación de doble negación es posible para cualquier fórmula de Harrop . ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \Pi _{2}^{0}}$ ${\displaystyle {\mathsf {HA}}}$

Funciones aritméticas de recursión

Yendo un paso más allá , se debe agregar el axioma que otorga la definición de funciones de conjunto mediante funciones de conjunto de pasos de iteración: Para cualquier conjunto , conjunto y , también debe existir una función obtenida haciendo uso del primero, a saber, tal que y . Este principio de iteración o recursión es similar al teorema de recursión transfinita , excepto que está restringido a funciones de conjunto y argumentos ordinales finitos, es decir, no hay una cláusula sobre ordinales límite . Funciona como el equivalente teórico de conjuntos de un objeto de números naturales en la teoría de categorías . Esto permite una interpretación completa de la aritmética de Heyting en nuestra teoría de conjuntos, incluidas las funciones de suma y multiplicación. ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle y}$ ${\displaystyle z\in y}$ ${\displaystyle f\colon y\to y}$ ${\displaystyle g\colon \omega \to y}$ ${\displaystyle g(0)=z}$ ${\displaystyle g(Sn)=f(g(n))}$ ${\displaystyle {\mathsf {HA}}}$

Con esto, y están bien fundamentados, en el sentido de la formulación inductiva de subconjuntos . Además, también se puede definir la aritmética de números racionales y demostrar sus propiedades, como la unicidad y la numerabilidad. ${\displaystyle {\mathbb {N} }}$ ${\displaystyle {\mathbb {Z} }}$ ${\displaystyle {\mathbb {Q} }}$

Recursión a partir de axiomas de la teoría de conjuntos

Recordemos que es la abreviatura de , donde es la abreviatura del predicado de función total, una proposición en términos de utiliza cuantificadores acotados. Si ambos lados son conjuntos, entonces por extensionalidad esto también es equivalente a . (Aunque por un ligero abuso de la notación formal, como con el símbolo " ", el símbolo " " también se usa comúnmente con clases de todos modos). ${\displaystyle h\simeq y^{x}}$ ${\displaystyle \forall f.{\big (}f\in h\leftrightarrow f\in y^{x}{\big )}}$ ${\displaystyle f\in y^{x}}$ ${\displaystyle h=y^{x}}$ ${\displaystyle \in }$ ${\displaystyle =}$

Una teoría de conjuntos con el principio de recursión que permite el modelo , explicado anteriormente, también demostrará que, para todos los números naturales y , los espacios de funciones ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle n}$ ${\displaystyle m}$

${\displaystyle {\{0,1,\dots ,n-1\}}\to {\{0,1,\dots ,m-1\}}}$

son conjuntos. De hecho, basta la recursión acotada, es decir, el principio para las clases definidas. ${\displaystyle \Delta _{0}}$

Por el contrario, el principio de recursión se puede demostrar a partir de una definición que implica la unión de funciones recursivas en dominios finitos. Para ello es relevante la clase de funciones parciales en tales que todos sus miembros tienen valores de retorno solo hasta un límite de número natural, que puede expresarse por . La existencia de esto como un conjunto se vuelve demostrable suponiendo que todos los espacios de funciones individuales forman conjuntos. Para este fin ${\displaystyle \omega }$ ${\displaystyle \cup _{n\in \omega }y^{\{0,1,\dots ,n-1\}}}$ ${\displaystyle y^{n}}$

Con este axioma, cualquier espacio de este tipo es ahora un conjunto de subconjuntos de y esto es estrictamente más débil que la separación completa. Cabe destacar que la adopción de este principio tiene un sabor genuino de teoría de conjuntos, en contraste con una incorporación directa de principios aritméticos en nuestra teoría. Y es un principio modesto en la medida en que estos espacios de funciones son mansos: cuando en cambio se supone una inducción completa o una exponenciación completa, tomando espacios de funciones o productos cartesianos de n-veces, es demostrable que sí preserva la contabilidad. ${\displaystyle n\times y}$ ${\displaystyle y}$ ${\displaystyle y^{n}}$

En la exponenciación finita, el principio de recursión es un teorema. Además, ahora también se pueden demostrar formas enumerables del principio del palomar , por ejemplo, que en un conjunto de índice finito, cada autoinyección es también una sobreyección. En consecuencia, la cardinalidad de los conjuntos finitos, es decir, el ordinal de von Neumann finito, es demostrablemente único. Los conjuntos discretos de índice finito son simplemente los conjuntos finitos. En particular, los subconjuntos de índice finito son finitos. Tomando cocientes o tomando la unión binaria o el producto cartesiano de dos conjuntos se conserva la finitud, la subfinitud y el índice finito. ${\displaystyle {\mathsf {ECTS}}}$ ${\displaystyle \omega }$

Los axiomas de la teoría de conjuntos enumerados hasta ahora incorporan aritmética de primer orden y son suficientes como marco formalizado para una buena parte de las matemáticas comunes. La restricción a los dominios finitos se levanta en el axioma de exponenciación estrictamente más fuerte que se muestra a continuación. Sin embargo, ese axioma tampoco implica el esquema de inducción completo para fórmulas con cuantificadores no ligados sobre el dominio de conjuntos, ni un principio de elección dependiente. Asimismo, hay principios de colección que constructivamente no están implícitos por el reemplazo, como se analiza más adelante. Una consecuencia de esto es que para algunos enunciados de mayor complejidad o indirección, incluso si bien pueden demostrarse casos concretos de interés, la teoría puede no demostrar el cierre universal. Más fuerte que esta teoría con exponenciación finita es la inducción completa plus. Implica el principio de recursión incluso para clases y cosas que son únicas. Ya ese principio de recursión cuando se restringe a sí demuestra la exponenciación finita, y también la existencia de un cierre transitivo para cada conjunto con respecto a (ya que la formación de la unión es ). Con él, las construcciones más comunes preservan la contabilidad. Las uniones generales sobre un conjunto finitamente indexado de conjuntos finitamente indexados son a su vez finitamente indexadas, al menos cuando se supone la inducción para -predicados (con respecto al lenguaje de la teoría de conjuntos, y esto entonces se cumple independientemente de la decidibilidad de sus relaciones de igualdad). ${\displaystyle {\mathsf {ECTS}}}$ ${\displaystyle g}$ ${\displaystyle \Delta _{0}}$ ${\displaystyle \in }$ ${\displaystyle \Delta _{0}}$ ${\displaystyle \Sigma _{1}}$

Inducción sin conjuntos infinitos

Antes de discutir incluso los conjuntos clásicamente incontables, esta última sección da un paso atrás hacia un contexto más parecido a . La suma de números, considerada como relación sobre ternas, es una colección infinita, al igual que la colección de números naturales en sí. Pero tenga en cuenta que se pueden adoptar esquemas de inducción (para conjuntos, ordinales o en conjunción con una clasificación de números naturales), sin postular nunca que la colección de naturales existe como un conjunto. Como se señaló, la aritmética de Heyting es biinterpretable con una teoría de conjuntos constructiva de este tipo, en la que se postula que todos los conjuntos están en biyección con un ordinal. El predicado BIT es un medio común para codificar conjuntos en aritmética. ${\displaystyle {\mathsf {BCST}}}$ ${\displaystyle {\mathsf {HA}}}$

Este párrafo enumera algunos principios débiles de inducción de números naturales estudiados en la teoría de la prueba de las teorías aritméticas con la adición y la multiplicación en su firma. Este es el marco donde estos principios se entienden mejor. Las teorías pueden definirse mediante formulaciones acotadas o variaciones en los esquemas de inducción que, además, pueden permitir solo predicados de complejidad restringida. En el lado clásico de primer orden, esto conduce a teorías entre la aritmética de Robinson y la aritmética de Peano : La teoría no tiene ninguna inducción. tiene inducción matemática completa para fórmulas aritméticas y tiene ordinal , lo que significa que la teoría permite codificar ordinales de teorías más débiles como relación recursiva solo en los naturales. Las teorías también pueden incluir símbolos adicionales para funciones particulares. Muchas de las teorías aritméticas bien estudiadas son débiles con respecto a la prueba de totalidad para algunas funciones de crecimiento más rápido . Algunos de los ejemplos más básicos de aritmética incluyen la aritmética de funciones elementales , que incluye la inducción para fórmulas aritméticas acotadas, es decir, con cuantificadores sobre rangos de números finitos. La teoría tiene un ordinal teórico de prueba (el menos no comprobado recursivo de buen ordenamiento ) de . El esquema de -inducción para fórmulas existenciales aritméticas permite la inducción para aquellas propiedades de los naturales cuya validación es computable mediante una búsqueda finita con tiempo de ejecución no acotado (cualquiera, pero finito). El esquema también es clásicamente equivalente al esquema de -inducción. La aritmética clásica de primer orden relativamente débil que adopta ese esquema se denota y prueba las funciones recursivas primitivas totales. La teoría es -conservadora sobre la aritmética recursiva primitiva . Nótese que la -inducción también es parte del sistema base de matemáticas inversas de segundo orden , siendo sus otros axiomas más -comprensión de subconjuntos de naturales. La teoría es -conservadora sobre . Todas las últimas teorías aritméticas mencionadas tienen ordinales . ${\displaystyle {\mathsf {Q}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {Q}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \varepsilon _{0}}$ ${\displaystyle {\mathsf {EFA}}}$ ${\displaystyle \omega ^{3}}$ ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathsf {I\Sigma }}_{1}}$ ${\displaystyle {\mathsf {I\Sigma }}_{1}}$ ${\displaystyle \Pi _{2}^{0}}$ ${\displaystyle {\mathsf {PRA}}}$ ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle {\mathsf {RCA}}_{0}}$ ${\displaystyle {\mathsf {Q}}}$ ${\displaystyle \Delta _{1}^{0}}$ ${\displaystyle {\mathsf {RCA}}_{0}}$ ${\displaystyle \Pi _{1}^{1}}$ ${\displaystyle {\mathsf {I\Sigma }}_{1}}$ ${\displaystyle \omega ^{\omega }}$

Mencionemos un paso más allá del esquema de inducción. La falta de esquemas de inducción más fuertes significa, por ejemplo, que algunas versiones ilimitadas del principio del agujero de paloma son indemostrables. Una relativamente débil es la afirmación del tipo del teorema de Ramsey expresada aquí de la siguiente manera: Para cualquier codificación y de un mapa de colores , asociando cada uno con un color , no es el caso de que para cada color exista un número de entrada umbral más allá del cual ya no es el valor de retorno de las asignaciones. (En el contexto clásico y en términos de conjuntos, esta afirmación sobre la coloración puede expresarse positivamente, diciendo que siempre existe al menos un valor de retorno tal que, en efecto, para algún dominio no acotado se cumple que . En palabras, cuando proporciona asignaciones enumeradas infinitas, cada una de las cuales es de uno de los diferentes colores posibles, se afirma que siempre existe una coloración particular de infinitos números y que, por lo tanto, el conjunto puede especificarse, sin siquiera tener que inspeccionar las propiedades de . Cuando se lee de forma constructiva, uno querría que fuera concretamente especificable y, por lo tanto, esa formulación es una afirmación más fuerte). Se necesita una indirección más alta que en la inducción para meros enunciados existenciales para reformular formalmente dicha negación (la afirmación del tipo del teorema de Ramsey en la formulación original anterior) y demostrarla. Es decir, para reformular el problema en términos de la negación de la existencia de un número umbral conjunto, dependiendo de todos los hipotéticos , más allá del cual la función todavía tendría que alcanzar algún valor de color. Más específicamente, la fuerza del principio de delimitación requerido está estrictamente entre el esquema de inducción en y . En el caso de las propiedades en términos de valores de retorno de funciones en dominios finitos, la verificación por fuerza bruta a través de la comprobación de todas las entradas posibles tiene una sobrecarga computacional que es mayor para dominios más grandes, pero siempre finita. La aceptación de un esquema de inducción como en valida el antiguo principio del casillero infinito, que se refiere a dominios ilimitados y, por lo tanto, a asignaciones con infinitas entradas. ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle m>0}$ ${\displaystyle f}$ ${\displaystyle n\in \omega }$ ${\displaystyle \{0,1,\dots ,m-1\}}$ ${\displaystyle c<m}$ ${\displaystyle n_{c}}$ ${\displaystyle c}$ ${\displaystyle k}$ ${\displaystyle K\subset \omega }$ ${\displaystyle \forall (n\in K).f(n)=k}$ ${\displaystyle f}$ ${\displaystyle m}$ ${\displaystyle k}$ ${\displaystyle f}$ ${\displaystyle k}$ ${\displaystyle n_{c}}$ ${\displaystyle {\mathsf {I\Sigma }}_{1}^{0}}$ ${\displaystyle {\mathsf {I\Sigma }}_{2}^{0}}$ ${\displaystyle {\mathsf {I\Sigma }}_{2}^{0}}$

Vale la pena señalar que en el programa de la 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, que a su vez está definido en términos de todos los naturales.

Exponenciación

La teoría clásica sin el axioma de conjunto potencia tiene modelos naturales en clases de conjuntos de tamaño hereditario menor que ciertos cardinales incontables. ^[21] En particular, sigue siendo coherente con que todos los conjuntos existentes (incluidos los conjuntos que contienen números reales) sean subcontables , e incluso contables. Una teoría de este tipo equivale esencialmente a una aritmética de segundo orden . Todos los conjuntos que son subcontables pueden ser coherentes de manera constructiva incluso en el presente de los conjuntos incontables, como se introduce ahora. ${\displaystyle {\mathsf {ZFC}}}$

Se discutieron los posibles principios de elección, ya se adoptó una forma debilitada del esquema de separación y se debilitarán más axiomas estándar para lograr una teoría más predicativa y constructiva. El primero de ellos es el axioma del conjunto potencia, que se adopta en la forma del espacio de funciones características. El siguiente axioma es estrictamente más fuerte que su contraparte para los dominios finitos discutidos anteriormente: ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle {\mathrm {Exp} }}$

La formulación aquí vuelve a utilizar la notación conveniente para espacios de funciones, como se explicó anteriormente. En palabras, el axioma dice que dados dos conjuntos , la clase de todas las funciones es, de hecho, también un conjunto. Esto es ciertamente necesario, por ejemplo, para formalizar el mapa de objetos de un hom-funtor interno como ${\displaystyle x,y}$ ${\displaystyle y^{x}}$ ${\displaystyle {\mathrm {hom} }({\mathbb {N} },-).}$

Al adoptar una declaración de existencia de este tipo, la cuantificación sobre los elementos de ciertas clases de funciones (totales) ahora solo abarca conjuntos. Considere la colección de pares que validan la relación de separación . A través de la separación acotada, esto ahora constituye un subconjunto de . Este ejemplo muestra que el axioma de exponenciación no solo enriquece el dominio de conjuntos directamente, sino que a través de la separación también permite la derivación de aún más conjuntos, y esto, además, también fortalece otros axiomas. ${\displaystyle \forall f}$ ${\displaystyle \langle a,b\rangle \in x\times x}$ ${\displaystyle \exists (f\in {\mathbb {N} }^{x}).f(a)\neq f(b)}$ ${\displaystyle x\times x}$

En particular, estos cuantificadores acotados ahora abarcan espacios de funciones que son demostrablemente incontables y, por lo tanto, incluso clásicamente incontables. Por ejemplo, la colección de todas las funciones donde , es decir, el conjunto de puntos subyacentes al espacio de Cantor , es incontable, por el argumento diagonal de Cantor , y, en el mejor de los casos, puede tomarse como un conjunto subcontable. En esta teoría, ahora también se puede cuantificar sobre subespacios de espacios como , que es una noción de tercer orden en los naturales. (En esta sección y más allá, el símbolo para el semianillo de números naturales en expresiones como se usa, o se escribe , solo para evitar la confusión de cardinal- con exponenciación ordinal). Aproximadamente, los conjuntos clásicamente incontables, como por ejemplo estos espacios de funciones, tienden a no tener igualdad computablemente decidible. ${\displaystyle f\colon \omega \to 2}$ ${\displaystyle 2:=SS0=\{0,1\}}$ ${\displaystyle 2^{\mathbb {N} }}$ ${\displaystyle 2^{\mathbb {N} }}$ ${\displaystyle y^{\mathbb {N} }}$ ${\displaystyle \omega \to y}$

Al tomar la unión general sobre una familia indexada , también el producto dependiente o indexado, escrito , es ahora un conjunto. Para constante , esto se reduce nuevamente al espacio de funciones . Y al tomar la unión general sobre los espacios de funciones mismos, siempre que la clase de potencia de sea un conjunto, entonces también el superconjunto de sea ahora un conjunto, lo que brinda un medio para hablar sobre el espacio de funciones parciales en . ${\displaystyle x}$ ${\displaystyle \{y_{i}\}_{i}}$ ${\displaystyle \Pi _{i\in x}\,y_{i}}$ ${\displaystyle y_{i}}$ ${\displaystyle y^{x}}$ ${\displaystyle x}$ ${\displaystyle \cup _{s\subset x}y^{s}}$ ${\displaystyle y^{x}}$ ${\displaystyle x}$

Sindicatos y rendición de cuentas

Con la exponenciación, la teoría prueba la existencia de cualquier función recursiva primitiva en , y en particular en los espacios de funciones incontables de . De hecho, con espacios de funciones y los ordinales de von Neumann finitos como dominios, podemos modelar como se discutió, y así codificar ordinales en la aritmética. Uno entonces además obtiene el número ordinal -exponenciado como un conjunto, que puede ser caracterizado como , el conjunto contado de palabras sobre un alfabeto infinito . La unión de todas las secuencias finitas sobre un conjunto contable es ahora un conjunto contable. Además, para cualquier familia contable de funciones de conteo junto con sus rangos, la teoría prueba que la unión de esos rangos es contable. Por el contrario, no asumiendo una elección contable, incluso es consistente con que el conjunto incontable sea la unión de un conjunto contable de conjuntos contables. ${\displaystyle x\times \omega \to y}$ ${\displaystyle \omega }$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle \omega ^{\omega }}$ ${\displaystyle \cup _{n\in \omega }\omega ^{n}}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathbb {R} }}$

La lista que se incluye aquí no es, de ninguna manera, completa. Muchos teoremas sobre los diversos predicados de existencia de funciones son válidos, especialmente cuando se supone una elección contable, que, como se ha señalado, nunca se supone implícitamente en este análisis.

Por último, con la exponenciación, cualquier unión finitamente indexada de una familia de conjuntos subfinitamente indexados o subcontables es en sí misma subfinitamente indexada o subcontable también. La teoría también demuestra que la colección de todos los subconjuntos contables de cualquier conjunto es un conjunto en sí misma. Con respecto a este subconjunto de la clase de potencia , algunas cuestiones de cardinalidad natural también pueden resolverse clásicamente solo con elección, al menos para incontables . ${\displaystyle x}$ ${\displaystyle {\mathcal {P}}_{x}}$ ${\displaystyle x}$

La clase de todos los subconjuntos de un conjunto

Dada una secuencia de conjuntos, se pueden definir nuevas secuencias de este tipo, p. ej., en . Pero, en particular, en un marco de teoría de conjuntos matemáticos, la colección de todos los subconjuntos de un conjunto no se define en una construcción de abajo hacia arriba a partir de sus constituyentes, sino a través de una comprensión de todos los conjuntos en el dominio del discurso. La caracterización estándar e independiente de la clase de potencia de un conjunto implica una cuantificación universal ilimitada, a saber , , donde se definió previamente también en términos del predicado de pertenencia . Aquí, una afirmación expresada como debe tomarse a priori por y no es equivalente a una proposición limitada por el conjunto. De hecho, la afirmación en sí es . Si es un conjunto, entonces la cuantificación definitoria incluso abarca , lo que hace que el axioma de conjunto de potencia sea impredicativo . ${\displaystyle \langle a,b\rangle \mapsto \langle \langle \rangle ,\langle a\rangle ,\langle b\rangle ,\langle a,b\rangle \rangle }$ ${\displaystyle x}$ ${\displaystyle \forall u.\left(u\in {\mathcal {P}}_{x}\leftrightarrow u\subset x\right)}$ ${\displaystyle \subset }$ ${\displaystyle \in }$ ${\displaystyle \forall (u\in {\mathcal {P}}_{x}).Q(x)}$ ${\displaystyle \forall u.{\big (}u\subset x\to Q(x){\big )}}$ ${\displaystyle y={\mathcal {P}}_{x}}$ ${\displaystyle \Pi _{1}}$ ${\displaystyle {\mathcal {P}}_{x}}$ ${\displaystyle {\mathcal {P}}_{x}}$

Recordemos que un miembro del conjunto de funciones características corresponde a un predicado que es decidible en un conjunto , que por tanto determina un subconjunto separable . A su vez, la clase de todos los subconjuntos separables de ahora también es un conjunto, mediante el reemplazo. Sin embargo, puede no tener propiedades deseables de manera demostrable, por ejemplo, estar cerrado bajo operaciones interminables como las uniones sobre conjuntos de índices infinitos numerables: Para una secuencia numerable , el subconjunto de que valida para todos existe como un conjunto. Pero puede no ser separable y, por lo tanto, no es necesariamente demostrable en sí mismo un miembro de . Mientras tanto, sobre la lógica clásica, todos los subconjuntos de un conjunto son trivialmente separables, lo que significa que y entonces, por supuesto, contiene cualquier subconjunto. Sobre la lógica clásica, esto significa además que la exponenciación convierte la clase de potencia en un conjunto. ${\displaystyle 2^{x}}$ ${\displaystyle x}$ ${\displaystyle s\subset x}$ ${\displaystyle {\mathcal {D}}_{x}\subset {\mathcal {P}}_{x}}$ ${\displaystyle x}$ ${\displaystyle {\mathcal {D}}_{x}}$ ${\displaystyle u_{n}\in {\mathcal {D}}_{x}}$ ${\displaystyle U:=\cup _{k\in \omega }u_{k}}$ ${\displaystyle x}$ ${\displaystyle (a\in U)\leftrightarrow \exists (m\in \omega ).a\in u_{m}}$ ${\displaystyle a\in x}$ ${\displaystyle {\mathcal {D}}_{x}}$ ${\displaystyle x}$ ${\displaystyle {\mathcal {D}}_{x}={\mathcal {P}}_{x}}$ ${\displaystyle {\mathcal {D}}_{x}}$

La traducción de los resultados de teorías matemáticas basadas en la teoría de conjuntos, como la topología de conjuntos puntuales o la teoría de la medida, a un marco constructivo es un sutil ir y venir. Por ejemplo, mientras que es un cuerpo de conjuntos , para que forme una σ-álgebra por definición también se requiere la clausura mencionada anteriormente bajo uniones. Pero mientras que un dominio de subconjuntos puede no exhibir dicha propiedad de clausura de manera constructiva, clásicamente una medida es continua desde abajo y, por lo tanto, su valor en una unión infinita puede, en cualquier caso, expresarse también sin referencia a ese conjunto como entrada de la función, es decir, a partir de la secuencia creciente de los valores de la función en uniones finitas. ${\displaystyle {\mathcal {D}}_{x}}$ ${\displaystyle \mu }$ ${\displaystyle \lim _{n\to \infty }}$ ${\displaystyle \mu (\cup _{k\leq n}u_{k})}$

Además de la clase de conjuntos desprendibles, también varias otras subclases de cualquier clase de potencia son ahora conjuntos comprobados. Por ejemplo, la teoría también prueba esto para la colección de todos los subconjuntos numerables de cualquier conjunto.

La riqueza de la clase de potencia completa en una teoría sin tercero excluido se puede entender mejor considerando pequeños conjuntos clásicamente finitos. Para cualquier proposición , considere la subclase de (ie o ). Es igual a cuando puede rechazarse y es igual a (ie ), cuando puede probarse. Pero también puede no ser decidible en absoluto. Considere tres proposiciones indecidibles diferentes, ninguna de las cuales implica de manera demostrable a otra. Se pueden usar para definir tres subclases del singleton , ninguna de las cuales es demostrablemente la misma. En esta visión, la clase de potencia del singleton, generalmente denotada por , se llama álgebra de valores de verdad y no necesariamente tiene de manera demostrable solo dos elementos. ${\displaystyle P}$ ${\displaystyle B:=\{x\in 1\mid P\}}$ ${\displaystyle 1}$ ${\displaystyle \{0\}}$ ${\displaystyle S0}$ ${\displaystyle B=0}$ ${\displaystyle P}$ ${\displaystyle B=1}$ ${\displaystyle B=S0}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle 1}$ ${\displaystyle {\mathcal {P}}_{1}}$ ${\displaystyle \Omega }$

Con la exponenciación, la clase potencia del singleton, , al ser un conjunto ya implica un conjunto potencia para los conjuntos en general. La prueba se realiza mediante el reemplazo de la asociación de con , y un argumento por el cual se cubren todos los subconjuntos. El conjunto también se inyecta en el espacio de funciones . ${\displaystyle {\mathcal {P}}_{1}}$ ${\displaystyle f\in {{\mathcal {P}}_{1}}^{x}}$ ${\displaystyle \{z\in x\mid 0\in f(z)\}\in {\mathcal {P}}_{x}}$ ${\displaystyle 2^{x}}$ ${\displaystyle {{\mathcal {P}}_{1}}^{x}}$

Si la teoría se demuestra por encima de un conjunto (como por ejemplo lo hace incondicionalmente), entonces el subconjunto de es una función con . Afirmar eso es afirmar que el término medio excluido se cumple para . ${\displaystyle B}$ ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle b:=\{\langle 0,B\rangle \}}$ ${\displaystyle 1\times {\mathcal {P}}_{1}}$ ${\displaystyle b\colon 1\to {\mathcal {P}}_{1}}$ ${\displaystyle {\big (}b(0)=1{\big )}\leftrightarrow P}$ ${\displaystyle {\mathcal {P}}_{1}=2}$ ${\displaystyle P}$

Se ha señalado que el conjunto vacío y el conjunto mismo son, por supuesto, dos subconjuntos de , es decir . Que también sea cierto en una teoría depende de una simple disyunción: ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle 1}$ ${\displaystyle 2\subset {\mathcal {P}}_{1}}$ ${\displaystyle {\mathcal {P}}_{1}\subset 2}$

${\displaystyle {\big (}\forall (x\in {\mathcal {P}}_{1}).(0\in x\lor 0\notin x){\big )}\to \,{\mathcal {P}}_{1}\subset 2}$.

Por lo tanto, suponiendo que se trate de fórmulas acotadas, la separación predicativa permite demostrar que la clase-potencia es un conjunto. Y, por lo tanto, en este contexto, también la elección completa demuestra que es un conjunto-potencia. (En el contexto de , el medio excluido acotado de hecho ya convierte la teoría de conjuntos en clásica, como se analiza más adelante). ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathcal {P}}_{1}}$ ${\displaystyle {\mathsf {IZF}}}$

La separación completa equivale a suponer simplemente que cada subclase individual de es un conjunto. Suponiendo la separación completa, tanto la elección completa como la regularidad demuestran que . ${\displaystyle 1}$ ${\displaystyle {\mathrm {PEM} }}$

Suponiendo en esta teoría que la inducción de conjuntos se vuelve equivalente a la regularidad y el reemplazo se vuelve capaz de probar la separación completa. ${\displaystyle {\mathrm {PEM} }}$

Obsérvese que las relaciones cardinales que involucran conjuntos incontables también son difíciles de alcanzar en , donde la caracterización de la incontabilidad se simplifica a . Por ejemplo, con respecto a la potencia incontable , es independiente de esa teoría clásica si todos ellos tienen , ni prueba que . Véase la hipótesis del continuo y el teorema de Easton relacionado . ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle |\omega |<|x|}$ ${\displaystyle 2^{|\omega |}}$ ${\displaystyle x}$ ${\displaystyle 2^{|\omega |}\leq |x|}$ ${\displaystyle 2^{|\omega |}<2^{|x|}}$

Nociones teóricas de categorías y tipos

Así, en este contexto con la exponenciación, la aritmética de primer orden tiene un modelo y existen todos los espacios de funciones entre conjuntos. Estos últimos son más accesibles que las clases que contienen todos los subconjuntos de un conjunto, como es el caso de los objetos exponenciales o subobjetos en la teoría de categorías. En términos de la teoría de categorías , la teoría corresponde esencialmente a pretopos de Heyting cerrados cartesianos constructivamente bien apuntados con (siempre que se adopte el Infinito) un objeto de números naturales . La existencia de un conjunto potencia es lo que convertiría a un pretopos de Heyting en un topos elemental . ^[22] Cada uno de estos topos que interpreta es, por supuesto, un modelo de estas teorías más débiles, pero se han definido pretopos cerrados cartesianos locales que, por ejemplo, interpretan teorías con exponenciación pero rechazan la separación completa y el conjunto potencia. Una forma de corresponde a cualquier subobjeto que tenga un complemento, en cuyo caso llamamos al topos booleano. El teorema de Diaconescu en su forma original de topos dice que esto se cumple si cualquier coecualizador de dos monomorfismos que no se intersecan tiene una sección. Esta última es una formulación de elección . El teorema de Barr establece que cualquier topos admite una sobreyección de un topos booleano sobre él, en relación con los enunciados clásicos que son demostrables intuicionistamente. ${\displaystyle {\mathsf {BCST}}+{\mathrm {Exp} }}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathrm {PEM} }}$

En teoría de tipos, la expresión " " existe por sí sola y denota espacios de funciones , una noción primitiva. Estos tipos (o, en teoría de conjuntos, clases o conjuntos) aparecen naturalmente, por ejemplo, como el tipo de la biyección currificante entre y , una adjunción . Una teoría de tipos típica con capacidad de programación general -y ciertamente aquellas que pueden modelar , lo que se considera una teoría de conjuntos constructiva- tendrá un tipo de enteros y espacios de funciones que representan , y como tal también incluirá tipos que no son contables. Esto es solo para decir, o implica, que entre los términos de función , ninguno tiene la propiedad de ser una sobreyección. ${\displaystyle x\to y}$ ${\displaystyle (z\times x)\to y}$ ${\displaystyle z\to y^{x}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathbb {Z} }\to {\mathbb {Z} }}$ ${\displaystyle f\colon {\mathbb {Z} }\to ({\mathbb {Z} }\to {\mathbb {Z} })}$

Las teorías de conjuntos constructivos también se estudian en el contexto de los axiomas aplicativos .

Metalógica

Si bien la teoría no excede la fuerza de consistencia de la aritmética de Heyting, al agregar el medio excluido se obtiene una teoría que prueba los mismos teoremas que la clásica menos la regularidad. Por lo tanto, al agregar la regularidad y la separación completa se obtiene la clásica completa . Al agregar la elección completa y la separación completa se obtiene la regularidad negativa. Por lo tanto, esto conduciría a una teoría más allá de la fuerza de la teoría de tipos típica . ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {ZFC}}}$

La teoría presentada no prueba que un espacio de funciones como tal no sea enumerable, en el sentido de inyecciones fuera de él. Sin más axiomas, las matemáticas intuicionistas tienen modelos en funciones recursivas pero también formas de hipercomputación . ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$

Análisis

En esta sección se desarrolla la fuerza de . Para el contexto, se mencionan otros posibles principios, que no son necesariamente clásicos y tampoco se consideran generalmente constructivos. Aquí conviene hacer una advertencia general: al leer afirmaciones de equivalencia de proposiciones en el contexto computable, siempre se debe tener en cuenta qué principios de elección , inducción y comprensión se asumen en silencio. Véase también el análisis constructivo relacionado , ^[23] el análisis factible y el análisis computable . ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$

La teoría hasta ahora demuestra la unicidad de los cuerpos completos ( pseudo ) ordenados de Arquímedes y Dedekind , con equivalencia por un único isomorfismo. El prefijo "pseudo" aquí resalta que el orden, en cualquier caso, no siempre será decidible de manera constructiva. Este resultado es relevante suponiendo que tales modelos completos existan como conjuntos.

Topología

Independientemente de la elección del modelo, el sabor característico de una teoría constructiva de números se puede explicar utilizando una proposición independiente . Consideremos un contraejemplo de la demostrabilidad constructiva del buen orden de los números naturales, pero ahora incorporado a los reales. Digamos ${\displaystyle P}$

${\displaystyle M:=\{x\in {\mathbb {R} }\mid (x=0\land P)\lor (x=1)\}}$.

La distancia métrica ínfima entre un punto y un subconjunto de este tipo, que puede expresarse como, por ejemplo, puede no demostrarse de manera constructiva. En términos más generales, esta propiedad de localización de los subconjuntos rige la teoría del espacio métrico constructivo, bien desarrollada. ${\displaystyle \rho (0,M)}$

Ya se trate de números reales de Cauchy o de Dedekind, entre otros, también son decidibles menos enunciados sobre la aritmética de los números reales , en comparación con la teoría clásica.

Secuencias de Cauchy

La exponenciación implica principios de recursión y, por lo tanto, en , se puede razonar cómodamente sobre secuencias , sus propiedades de regularidad como , o sobre intervalos decrecientes en . Esto permite hablar de secuencias de Cauchy y su aritmética. Este es también el enfoque de análisis adoptado en . ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ ${\displaystyle s\colon \omega \to {\mathbb {Q} }}$ ${\displaystyle |s_{n}-s_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}$ ${\displaystyle \omega \to ({\mathbb {Q} }\times {\mathbb {Q} })}$ ${\displaystyle {\mathsf {Z}}_{2}}$

Reales de Cauchy

Cualquier número real de Cauchy es una colección de tales secuencias, es decir, un subconjunto de un conjunto de funciones en construido con respecto a una relación de equivalencia . La exponenciación junto con la separación acotada prueban que la colección de números reales de Cauchy es un conjunto, simplificando así un poco el tratamiento lógico de los números reales. ${\displaystyle \omega }$

Incluso en la teoría fuerte con una forma reforzada de Colección, los reales de Cauchy se comportan mal cuando no se supone una forma de elección contable , y es suficiente para la mayoría de los resultados. Esto concierne a la completitud de las clases de equivalencia de tales secuencias, la equivalencia de todo el conjunto con los reales de Dedekind, la existencia de un módulo de convergencia para todas las secuencias de Cauchy y la preservación de dicho módulo al tomar límites. ^[24] Un enfoque alternativo que se comporta ligeramente mejor es trabajar una colección de reales de Cauchy juntos con una elección de módulo, es decir, no solo con los números reales sino con un conjunto de pares, o incluso con un módulo fijo compartido por todos los números reales. ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle {\mathrm {AC} _{\omega ,2}}}$

Hacia los reales de Dedekind

Al igual que en la teoría clásica, los cortes de Dedekind se caracterizan utilizando subconjuntos de estructuras algebraicas como : Las propiedades de estar habitado, numéricamente acotado por arriba, "cerrado por abajo" y "abierto por arriba" son todas fórmulas acotadas con respecto al conjunto dado subyacente a la estructura algebraica. Un ejemplo estándar de un corte, cuyo primer componente exhibe de hecho estas propiedades, es la representación de dado por ${\displaystyle {\mathbb {Q} }}$ ${\displaystyle {\sqrt {2}}}$

${\displaystyle {\big \langle }\{x\in {\mathbb {Q} }\mid x<0\lor x^{2}<2\},\,\{x\in {\mathbb {Q} }\mid 0<x\land 2<x^{2}\}{\big \rangle }\,\ \in \,\ {{\mathcal {P}}_{\mathbb {Q} }}\times {{\mathcal {P}}_{\mathbb {Q} }}}$

(Dependiendo de la convención para cortes, cualquiera de las dos partes o ninguna, como aquí, puede hacer uso del signo .) ${\displaystyle \leq }$

La teoría dada por los axiomas hasta ahora valida que un cuerpo pseudo-ordenado que también es arquimediano y Dedekind completo, si es que existe, se caracteriza de esta manera de manera única, hasta el isomorfismo. Sin embargo, la existencia de espacios de funciones como no garantiza que sea un conjunto, y por lo tanto tampoco lo es la clase de todos los subconjuntos de que cumplen las propiedades nombradas. Lo que se requiere para que la clase de reales de Dedekind sea un conjunto es un axioma sobre la existencia de un conjunto de subconjuntos y esto se analiza más adelante en la sección sobre refinamiento binario. En un contexto sin o conjunto potencia, se supone que la elección numerable en conjuntos finitos prueba la incontabilidad del conjunto de todos los reales de Dedekind. ${\displaystyle \{0,1\}^{\mathbb {Q} }}$ ${\displaystyle {{\mathcal {P}}_{\mathbb {Q} }}}$ ${\displaystyle {\mathbb {Q} }}$ ${\displaystyle {\mathrm {PEM} }}$

Escuelas constructivas

La mayoría de las escuelas de análisis constructivo validan alguna elección y también - , como se define en la segunda sección sobre límites numéricos. A continuación se presentan otras proposiciones empleadas en las teorías del análisis constructivo que no se pueden demostrar utilizando únicamente la lógica intuicionista básica: ${\displaystyle \mathrm {BD} }$ ${\displaystyle {\mathbb {N} }}$

• En el lado de las matemáticas recursivas (el marco constructivo "ruso" o "markoviano" con muchas abreviaturas, por ejemplo ), primero se tiene el principio de Markov , que es una forma de prueba por contradicción motivada por la búsqueda computable (capacidad de memoria ilimitada). Esto tiene un impacto notable en las afirmaciones sobre números reales, como se menciona más adelante. En esta escuela, se tiene incluso el principio de tesis de Church, constructivo y anticlásico , generalmente adoptado para funciones de teoría de números. El principio de tesis de Church, expresado en el lenguaje de la teoría de conjuntos y formulado para funciones de conjuntos, postula que todas ellas corresponden a programas computables que eventualmente se detienen en cualquier argumento. En la teoría de la computabilidad, los números naturales correspondientes a los índices de los códigos de las funciones computables que son totales están en la jerarquía aritmética , lo que significa que la pertenencia a cualquier índice se afirma validando una proposición. Esto quiere decir que dicha colección de funciones sigue siendo una mera subclase de los naturales y, por lo tanto, cuando se pone en relación con algunos espacios de funciones clásicas, es conceptualmente pequeña. En este sentido, la adopción del postulado convierte a los conjuntos en "dispersos", tal como se los ve desde la teoría clásica de conjuntos. La subcontabilidad de los conjuntos también se puede postular de forma independiente. ${\displaystyle {\mathsf {RUSS}}}$ ${\displaystyle {\mathrm {MP} }}$ ${\displaystyle {\mathrm {CT} }}$ ${\displaystyle \Pi _{2}^{0}}$ ${\displaystyle \forall x\,\exists y}$ ${\displaystyle {\mathrm {CT} }}$ ${\displaystyle \omega \to \omega }$
• Así que en otro extremo, en el lado intuicionista de Brouwer ( ), están la inducción de barras , el teorema del abanico decidible que dice que las barras decidibles son uniformes, que están entre los principios más débiles y a menudo discutidos, el esquema de Kripke (con la elección contable convirtiendo todas las subclases de contables), o incluso el principio de continuidad anticlásico de Brouwer, que determina los valores de retorno de lo que se establece como una función en secuencias infinitas ya a través de solo segmentos iniciales finitos. ${\displaystyle {\mathsf {INT}}}$ ${\displaystyle {\mathrm {FAN} }_{\Delta }}$ ${\displaystyle \omega }$

Ciertas leyes en ambas escuelas contradicen , de modo que elegir adoptar todos los principios de cualquiera de las dos escuelas refuta los teoremas del análisis clásico. sigue siendo coherente con alguna elección, pero contradice el clásico y , explicado a continuación. La independencia de la regla de premisas con las premisas de existencia de conjuntos no se entiende completamente, pero como principio teórico de números está en conflicto con los axiomas de la escuela rusa en algunos marcos. En particular, también contradice , lo que significa que las escuelas constructivas tampoco pueden combinarse en su totalidad. Algunos de los principios no pueden combinarse constructivamente en la medida en que juntos implican formas de - por ejemplo más la contabilidad de todos los subconjuntos de los naturales. Estas combinaciones naturalmente tampoco son consistentes con otros principios anticlásicos. ${\displaystyle {\mathrm {WLPO} }}$ ${\displaystyle {\mathrm {CT} }_{0}}$ ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle {\mathrm {LLPO} }}$ ${\displaystyle {\mathrm {CT} }_{0}}$ ${\displaystyle {\mathrm {FAN} }_{\Delta }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {MP} }}$

Indecomponibilidad

Denotemos la clase de todos los conjuntos por . La decidibilidad de la pertenencia a una clase se puede expresar como pertenencia a . También notamos que, por definición, las dos clases extremas y son trivialmente decidibles. La pertenencia a esas dos es equivalente a las proposiciones triviales respectivamente . ${\displaystyle {\mathcal {V}}}$ ${\displaystyle R}$ ${\displaystyle R\cup ({\mathcal {V}}\setminus R)}$ ${\displaystyle {\mathcal {V}}}$ ${\displaystyle \{\}}$ ${\displaystyle x=x}$ ${\displaystyle \neg (x=x)}$

Llame a una clase indecomponible o cohesiva si, para cualquier predicado , ${\displaystyle R}$ ${\displaystyle \chi }$

${\displaystyle {\big (}\forall (x\in R).\chi (x)\lor \neg \chi (x){\big )}\to {\Big (}{\big (}\forall (x\in R).\chi (x){\big )}\lor {\big (}\forall (x\in R).\neg \chi (x){\big )}{\Big )}}$

Esto expresa que las únicas propiedades que son decidibles son las propiedades triviales. Esto se ha estudiado ampliamente en el análisis intuicionista. ${\displaystyle R}$

El llamado esquema de indecomponibilidad (Unzerlegbarkeit) para la teoría de conjuntos es un principio posible que establece que toda la clase es indecomponible. Hablando en términos extensionales, postula que las dos clases triviales son las únicas clases que son decidibles con respecto a la clase de todos los conjuntos. Para un predicado motivador simple, considere la pertenencia a la primera clase no trivial, es decir, la propiedad de estar vacío. Esta propiedad es no trivial en la medida en que separa algunos conjuntos: el conjunto vacío es un miembro de , por definición, mientras que una plétora de conjuntos no son, de manera demostrable, miembros de . Pero, utilizando la separación, uno puede, por supuesto, también definir varios conjuntos para los cuales el vacío no es decidible en absoluto en una teoría constructiva, es decir, la pertenencia a no es demostrable para todos los conjuntos. Entonces, aquí la propiedad del vacío no divide el dominio teórico de conjuntos del discurso en dos partes decidibles. Para cualquier propiedad no trivial de este tipo, el contrapositivo de dice que no puede ser decidible sobre todos los conjuntos. ${\displaystyle {\mathrm {UZ} }}$ ${\displaystyle {\mathcal {V}}}$ ${\displaystyle {\mathrm {UZ} }}$ ${\displaystyle x\in 1}$ ${\displaystyle x=\{\}}$ ${\displaystyle 1}$ ${\displaystyle 1}$ ${\displaystyle 1\cup ({\mathcal {V}}\setminus 1)}$ ${\displaystyle {\mathrm {UZ} }}$

${\displaystyle {\mathrm {UZ} }}$está implícito en el principio de uniformidad , que es coherente y se analiza a continuación. ${\displaystyle {\mathrm {UP} }}$ ${\displaystyle {\mathsf {CZF}}}$

Principios no constructivos

Por supuesto , y muchos principios que definen lógicas intermedias no son constructivos. y , que es solo para proposiciones negadas, puede presentarse como las reglas de De Morgan . Más específicamente, esta sección se ocupará de las declaraciones en términos de predicados, especialmente los más débiles, expresados ​​en términos de unos pocos cuantificadores sobre conjuntos, además de predicados decidibles sobre números. Volviendo a la sección sobre funciones características, se puede decir que una colección es buscable si es buscable para todos sus subconjuntos separables, lo que a su vez corresponde a . Esta es una forma de - para . Nótese que en el contexto de la exponenciación, tales proposiciones sobre conjuntos ahora están limitadas por conjuntos. ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {WPEM} }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle A}$ ${\displaystyle \{0,1\}^{A}}$ ${\displaystyle \exists }$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle A}$

Particularmente valiosas en el estudio del análisis constructivo son las afirmaciones no constructivas formuladas comúnmente en términos de la colección de todas las secuencias binarias y las funciones características en el dominio aritmético están bien estudiadas. Aquí hay una proposición decidible en cada numeral , pero, como se demostró anteriormente, las afirmaciones cuantificadas en términos de pueden no serlo. Como se sabe a partir del teorema de incompletitud y sus variaciones, ya en aritmética de primer orden, las funciones de ejemplo en pueden caracterizarse de tal manera que si es consistente, las disyunciones en competencia - , de baja complejidad, son cada una - indemostrables (incluso si prueba la disyunción de las dos axiomáticamente). ${\displaystyle f}$ ${\displaystyle A=\omega }$ ${\displaystyle f({\underline {\mathrm {n} }})=0}$ ${\displaystyle {\mathrm {n} }}$ ${\displaystyle f}$ ${\displaystyle {\mathbb {N} }}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \exists }$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {PA}}}$

De manera más general, la aritmética - , una declaración esencialmente lógica y no constructiva más prominente se conoce con el nombre de principio limitado de omnisciencia . En la teoría de conjuntos constructiva presentada a continuación, implica - , , la versión - del teorema del abanico, pero también se analiza a continuación. Recordemos ejemplos de oraciones famosas que se pueden escribir de manera - , es decir, de tipo Goldbach: la conjetura de Goldbach , el último teorema de Fermat pero también la hipótesis de Riemann se encuentran entre ellas. Suponiendo una elección dependiente relativizada y el sobre clásico no permite pruebas de más declaraciones - . postula una propiedad disyuntiva, al igual que la declaración de decidibilidad más débil para funciones que son constantes ( - oraciones) , la aritmética - . Los dos están relacionados de manera similar como es versus y difieren esencialmente en . a su vez implica la llamada versión "menor" . Esta es la versión (aritmética) - de la regla de De Morgan no constructiva para una conjunción negada. Existen, por ejemplo, modelos de la teoría de conjuntos fuertes que separan tales afirmaciones, en el sentido de que pueden validar pero rechazar . ${\displaystyle \exists }$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {LPO} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathrm {BD} }}$ ${\displaystyle {\mathbb {N} }}$ ${\displaystyle {\mathrm {MP} }}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {RDP} }}$ ${\displaystyle {\mathrm {LPO} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle \Pi _{0}^{2}}$ ${\displaystyle {\mathrm {LPO} }}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {WLPO} }}$ ${\displaystyle \forall }$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {WPEM} }}$ ${\displaystyle {\mathrm {MP} }}$ ${\displaystyle {\mathrm {WLPO} }}$ ${\displaystyle {\mathrm {LLPO} }}$ ${\displaystyle \exists }$ ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle {\mathrm {LLPO} }}$ ${\displaystyle {\mathrm {WLPO} }}$

Los principios disyuntivos sobre oraciones - generalmente apuntan a formulaciones equivalentes que deciden la separación en el análisis en un contexto con elección suave o . La afirmación expresada por traducida a números reales es equivalente a la afirmación de que la igualdad o la separación de dos reales cualesquiera es decidible (de hecho, decide la tricotomía). Entonces también es equivalente a la afirmación de que todo real es racional o irracional, sin el requisito o la construcción de un testigo para ninguno de los disyuntos. Del mismo modo, la afirmación expresada por para números reales es equivalente a que el orden de dos reales cualesquiera es decidible (dicotomía). Entonces también es equivalente a la afirmación de que si el producto de dos reales es cero, entonces cualquiera de los reales es cero, nuevamente sin un testigo. De hecho, las formulaciones de los tres principios de omnisciencia son entonces cada una equivalente a teoremas de la separación, igualdad u orden de dos reales de esta manera. Aún se puede decir más sobre las secuencias de Cauchy que se aumentan con un módulo de convergencia. ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {MP} }}$ ${\displaystyle {\mathrm {LPO} }}$ ${\displaystyle {\mathrm {LLPO} }}$ ${\displaystyle \leq }$

Una fuente famosa de indecidibilidad computable -y a su vez también de una amplia gama de proposiciones indecidibles- es el predicado que expresa que un programa de computadora es total.

Árboles infinitos

A través de la relación entre computabilidad y jerarquía aritmética, los conocimientos de este estudio clásico también son reveladores para consideraciones constructivas. Un conocimiento básico de las matemáticas inversas se refiere a árboles binarios computables infinitos de ramificación finita. Un árbol de este tipo puede, por ejemplo, codificarse como un conjunto infinito de conjuntos finitos.

${\displaystyle T\,\subset \,\bigcup _{n\in \omega }\{0,1\}^{\{0,1,\dots ,n-1\}}}$,

con membresía decidible, y esos árboles entonces contienen de manera probada elementos de tamaño finito arbitrario. El llamado lema de König débil establece: Para tal , siempre existe un camino infinito en , es decir, una secuencia infinita tal que todos sus segmentos iniciales son parte del árbol. En matemáticas inversas, el subsistema aritmético de segundo orden no prueba . Para entender esto, note que hay árboles computables para los cuales no existe tal camino computable a través de él. Para probar esto, uno enumera las secuencias computables parciales y luego diagonaliza todas las secuencias computables totales en una secuencias computables parciales . Luego uno puede desplegar un cierto árbol , uno exactamente compatible con los valores aún posibles de en todas partes, que por construcción es incompatible con cualquier camino computable total. ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle T}$ ${\displaystyle \omega \to \{0,1\}}$ ${\displaystyle {\mathsf {RCA}}_{0}}$ ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle K}$ ${\displaystyle d}$ ${\displaystyle K}$ ${\displaystyle d}$

En , el principio implica y - , una forma muy modesta de elección contable introducida anteriormente. Los dos primeros son equivalentes suponiendo que el principio de elección ya está en el contexto aritmético más conservador. también es equivalente al teorema del punto fijo de Brouwer y otros teoremas sobre valores de funciones continuas en los números reales. El teorema del punto fijo a su vez implica el teorema del valor intermedio , pero siempre tenga en cuenta que estas afirmaciones pueden depender de la formulación, ya que los teoremas clásicos sobre los números reales codificados pueden traducirse en diferentes variantes cuando se expresan en un contexto constructivo. ^[25] ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle {\mathrm {LLPO} }}$ ${\displaystyle \Pi _{1}^{0}}$ ${\displaystyle {\mathrm {AC} }_{\omega ,2}}$ ${\displaystyle {\mathrm {WKL} }}$

El , y algunas variantes del mismo, se refieren a grafos infinitos y, por lo tanto, sus contrapositivos dan una condición para la finitud. Nuevamente para conectar con el análisis, sobre la teoría aritmética clásica , la afirmación de es, por ejemplo, equivalente a la compacidad de Borel con respecto a las subcubiertas finitas del intervalo unitario real. es una afirmación de existencia estrechamente relacionada que involucra secuencias finitas en un contexto infinito. Sobre , son en realidad equivalentes. En aquellos son distintos, pero, después de asumir nuevamente alguna elección, aquí entonces implica . ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle {\mathsf {RCA}}_{0}}$ ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle {\mathrm {FAN} }_{\Delta }}$ ${\displaystyle {\mathsf {RCA}}_{0}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathrm {WKL} }}$ ${\displaystyle {\mathrm {FAN} }_{\Delta }}$

Inducción

Inducción matemática

Se observó que en el lenguaje de conjuntos, los principios de inducción pueden leerse , con el antecedente definido como más arriba, y con el significado donde el conjunto siempre denota el modelo estándar de números naturales. A través del axioma fuerte de Infinito y la Separación predicativa, la validez de la inducción para definiciones o -acotadas por conjuntos ya se estableció y se discutió a fondo. Para aquellos predicados que involucran solo cuantificadores sobre , valida la inducción en el sentido de la teoría aritmética de primer orden. En un contexto de teoría de conjuntos donde es un conjunto, este principio de inducción se puede usar para probar que las subclases definidas predicativamente de son el conjunto mismo. El llamado esquema de inducción matemática completa ahora postula la igualdad del conjunto de con todas sus subclases inductivas. Como en la teoría clásica, también está implícito cuando se pasa al esquema de Separación completo impredicativo. Como se indicó en la sección sobre Elección, los principios de inducción como este también están implícitos en varias formas de principios de elección. ${\displaystyle \mathrm {Ind} _{A}\to \omega \subset A}$ ${\displaystyle \mathrm {Ind} _{A}}$ ${\displaystyle \omega \subset A}$ ${\displaystyle \forall (n\in \omega ).n\in A}$ ${\displaystyle \omega }$ ${\displaystyle \Delta _{0}}$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle \omega }$

El principio de recursión para funciones de conjuntos mencionado en la sección dedicada a la aritmética también está implícito en el esquema de inducción matemática completo sobre la estructura que modela los números naturales (por ejemplo, ). Por lo tanto, para ese teorema, al otorgar un modelo de aritmética de Heyting, representa una alternativa a los principios de exponenciación. ${\displaystyle \omega }$

Las fórmulas de predicado utilizadas con el esquema deben entenderse como fórmulas en la teoría de conjuntos de primer orden. El cero denota el conjunto como se indicó anteriormente, y el conjunto denota el conjunto sucesor de , con . Por el axioma de infinito anterior, es nuevamente un miembro de . Tenga en cuenta que, a diferencia de lo que ocurre en una teoría aritmética, los naturales aquí no son los elementos abstractos en el dominio del discurso, sino elementos de un modelo. Como se ha observado en discusiones anteriores, al aceptar , ni siquiera para todos los conjuntos definidos predicativamente es necesariamente decidible la igualdad con un ordinal de von Neumann finito. ${\displaystyle 0}$ ${\displaystyle \{\}}$ ${\displaystyle Sn}$ ${\displaystyle n\in \omega }$ ${\displaystyle n\in Sn}$ ${\displaystyle \omega }$ ${\displaystyle {\mathsf {ECST}}}$

Establecer inducción

Más allá de los principios de inducción anteriores, se tiene la inducción de conjuntos completos, que se puede comparar con la inducción bien fundada . Al igual que la inducción matemática anterior, el siguiente axioma se formula como un esquema en términos de predicados y, por lo tanto, tiene un carácter diferente a los principios de inducción demostrados a partir de los axiomas de la teoría de conjuntos predicativos. También se estudia de forma independiente una variante del axioma solo para fórmulas acotadas y puede derivarse de otros axiomas.

En este caso, la cuestión es trivial y, por lo tanto, se aplica hasta el "caso inferior" del marco estándar. Esto (así como la inducción de números naturales) puede restringirse nuevamente a las fórmulas de conjuntos acotados, en cuyo caso la aritmética no se ve afectada. ${\displaystyle \forall (z\in \{\}).\phi (z)}$ ${\displaystyle \phi (\{\})}$

En , el axioma prueba la inducción en conjuntos transitivos y, en particular, también para conjuntos transitivos de conjuntos transitivos. Esta última es, entonces, una definición adecuada de los ordinales, e incluso una -formulación. La inducción de conjuntos, a su vez, permite la aritmética ordinal en este sentido. Además, permite definiciones de funciones de clase por recursión transfinita . El estudio de los diversos principios que otorgan definiciones de conjuntos por inducción, es decir, definiciones inductivas, es un tema principal en el contexto de la teoría de conjuntos constructiva y sus fortalezas comparativamente débiles . Esto también es válido para sus contrapartes en la teoría de tipos. No se requiere el reemplazo para probar la inducción sobre el conjunto de naturales a partir de la inducción de conjuntos, pero ese axioma es necesario para su aritmética modelada dentro de la teoría de conjuntos. ${\displaystyle {\mathsf {ECST}}}$ ${\displaystyle \Delta _{0}}$

El axioma de regularidad es un enunciado único con cuantificador universal sobre conjuntos y no un esquema. Como se muestra, implica , y por lo tanto no es constructivo. Ahora bien, para que se tome como la negación de algún predicado y se escriba para la clase , la inducción se lee ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle \phi }$ ${\displaystyle \neg S}$ ${\displaystyle \Sigma }$ ${\displaystyle \{y\mid S(y)\}}$

${\displaystyle \forall (x\in \Sigma ).\neg (x\cap \Sigma =\{\})\,\,\leftrightarrow \,\,\Sigma =\{\}}$

Por la vía contrapositiva, la inducción de conjuntos implica todas las instancias de regularidad pero solo con existencia doblemente negada en la conclusión. En la otra dirección, dados suficientes conjuntos transitivos , la regularidad implica cada instancia de inducción de conjuntos.

Metalógica

La teoría formulada anteriormente puede expresarse como si se descartaran los axiomas de conjunto en favor de los axiomas más débiles de reemplazo y exponenciación. Demuestra que los reales de Cauchy son un conjunto, pero no la clase de los reales de Dedekind. ${\displaystyle {\mathsf {CZF}}}$

Llamemos a un ordinal en sí mismo tricotómico si la relación de pertenencia irreflexiva " " entre sus miembros es tricotómica . Al igual que el axioma de regularidad, la inducción de conjuntos restringe los modelos posibles de " " y, por lo tanto, los de una teoría de conjuntos, como fue la motivación para el principio en los años 20. Pero la teoría constructiva aquí no prueba una tricotomía para todos los ordinales, mientras que los ordinales tricotómicos no se comportan bien con respecto a la noción de sucesor y rango. ${\displaystyle \in }$ ${\displaystyle \in }$

La fuerza teórica de prueba adicional lograda con la inducción en el contexto constructivo es significativa, incluso si la eliminación de la regularidad en el contexto de no reduce la fuerza teórica de prueba. Incluso sin exponenciación, la teoría actual con inducción de conjuntos tiene la misma fuerza teórica de prueba que y prueba las mismas funciones recursivamente. Específicamente, su ordinal contable grande de prueba teórica es el ordinal de Bachmann-Howard . Este es también el ordinal de la teoría de conjuntos clásica o intuicionista de Kripke-Platek . Es consistente incluso con asumir que la clase de ordinales tricotómicos forman un conjunto. La teoría actual aumentada con este postulado de existencia de conjuntos ordinales prueba la consistencia de . ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {IZF}}}$ ${\displaystyle {\mathsf {CZF}}}$

Aczel también fue uno de los principales desarrolladores de la teoría de conjuntos no bien fundados , que rechaza la inducción de conjuntos.

Relación con ZF

La teoría también constituye una presentación de la teoría de conjuntos de Zermelo-Fraenkel en el sentido de que están presentes variantes de todos sus ocho axiomas. Extensionalidad, Apareamiento, Unión y Reemplazo son, de hecho, idénticos. La separación se adopta en una forma predicativa débil, mientras que la infinitud se enuncia en una formulación fuerte. De manera similar a la formulación clásica, este axioma de separación y la existencia de cualquier conjunto ya prueban el axioma del conjunto vacío. La exponenciación para dominios finitos y la inducción matemática completa también están implícitas en sus variantes adoptadas más fuertes. Sin el principio del tercero excluido, la teoría aquí carece, en su forma clásica, de separación completa, conjunto potencia y regularidad. Aceptar ahora exactamente conduce a la teoría clásica. ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathrm {PEM} }}$

The following highlights the different readings of a formal theory. Let ${\displaystyle \mathrm {CH} }$ denote the continuum hypothesis and ${\displaystyle B:=\{z\in 1\mid \mathrm {CH} \}}$ so that ${\displaystyle 0\in B\leftrightarrow \mathrm {CH} }$. Then ${\displaystyle b:=B\cup \{1\}}$ is inhabited by ${\displaystyle 1}$ and any set that is established to be a member of ${\displaystyle b}$ either equals ${\displaystyle 0}$ or ${\displaystyle 1}$. Induction on ${\displaystyle \omega }$ implies that it cannot consistently be negated that ${\displaystyle b}$ has some least natural number member. The value of such a member can be shown to be independent of theories such as ${\displaystyle {\mathsf {ZFC}}}$. Nonetheless, any classical set theory like ${\displaystyle {\mathsf {ZFC}}}$ also proves there exists such a number.

Strong Collection

Having discussed all the weakened forms of the classical set theory axioms, Replacement and Exponentiation can be further strengthened without losing a type theoretical interpretation, and in a way that is not going beyond ${\displaystyle {\mathsf {ZF}}}$.

So firstly, one may reflect upon the strength of the axiom of replacement, also in the context of the classical set theory. For any set ${\displaystyle y}$ and any natural ${\displaystyle n}$, there exists the product ${\displaystyle y^{n}}$ recursively given by ${\displaystyle y^{n-1}\times y}$, which have ever deeper rank. Induction for unbound predicates proves that these sets exist for all of the infinitely many naturals. Replacement "for ${\displaystyle n\mapsto y^{n}}$" now moreover states that this infinite class of products can be turned into the infinite set, ${\displaystyle \{p\mid \exists (n\in \omega ).p=y^{n}\}}$. This is also not a subset of any previously established set.

Going beyond those axioms also seen in Myhill's typed approach, consider the discussed constructive theory with Exponentiation and Induction, but now strengthened by the collection schema. In ${\displaystyle {\mathsf {ZF}}}$ it is equivalent to Replacement, unless the powerset axiom is dropped. In the current context the strong axiom presented supersedes Replacement, due to not requiring the binary relation definition to be functional, but possibly multi-valued.

In words, for every total relation, there exists an image set ${\displaystyle b}$ such that the relation is total in both directions. Expressing this via a raw first-order formulation leads to a somewhat repetitive format. The antecedent states that one considers relation ${\displaystyle \phi }$ between sets ${\displaystyle x}$ and ${\displaystyle y}$ that are total over a certain domain set ${\displaystyle a}$, that is, ${\displaystyle \phi }$ has at least one "image value" ${\displaystyle y}$ for every element ${\displaystyle x}$ in the domain. This is more general than an inhabitance condition ${\displaystyle x\in y}$ in a set theoretical choice axiom, but also more general than the condition of Replacement, which demands unique existence ${\displaystyle \exists !y}$. In the consequent, firstly, the axioms states that then there exists a set ${\displaystyle b}$ which contains at least one "image" value ${\displaystyle y}$ under ${\displaystyle \phi }$, for every element of the domain. Secondly, in this axioms formulation it then moreover states that only such images ${\displaystyle y}$ are elements of that new codomain set ${\displaystyle b}$. It is guaranteeing that ${\displaystyle b}$ does not overshoot the codomain of ${\displaystyle \phi }$ and thus the axiom is also expressing some power akin to a Separation procedure. The principle may be used in the constructive study of larger sets beyond the everyday need of analysis.

Metalogic

This theory without ${\displaystyle {\mathrm {PEM} }}$, without unbounded separation and without "naive" Power set enjoys various nice properties. For example, as opposed to ${\displaystyle {\mathsf {CZF}}}$ with its subset collection schema below, it has the existence property.

Constructive Zermelo–Fraenkel

Binary refinement

The so called binary refinement axiom says that for any ${\displaystyle a}$ there exists a set ${\displaystyle {\mathcal {B}}_{a}\subset {\mathcal {P}}_{a}}$ such that for any covering ${\displaystyle a=x\cup y}$, the set ${\displaystyle {\mathcal {B}}_{a}}$ holds two subsets ${\displaystyle c\subset x}$ and ${\displaystyle d\subset y}$ that also do this covering job, ${\displaystyle a=c\cup d}$. It is a weakest form of the powerset axiom and at the core of some important mathematical proofs. Fullness below, for relations between the set ${\displaystyle a}$ and the finite ${\displaystyle \{0,1\}}$, implies that this is indeed possible.

Taking another step back, ${\displaystyle {\mathsf {ECST}}}$ plus Recursion and plus Binary refinement already proves that there exists an Archimedean, Dedekind complete pseudo-ordered field. That set theory also proves that the class of left Dedekind cuts is a set, not requiring Induction or Collection. And it moreover proves that function spaces into discrete sets are sets (there e.g. ${\displaystyle \omega \to \omega }$), without assuming ${\displaystyle {\mathrm {Exp} }}$. Already over the weak theory ${\displaystyle {\mathsf {BCST}}}$ (which is to say without Infinity) does binary refinement prove that function spaces into discrete sets are sets, and therefore e.g. the existence of all characteristic function spaces ${\displaystyle \{0,1\}^{a}}$.

Subset Collection

The theory known as ${\displaystyle {\mathsf {CZF}}}$ adopts the axioms of the previous sections plus a stronger form of Exponentiation. It is by adopting the following alternative to Exponentiation, which can again be seen as a constructive version of the Power set axiom:

An alternative that is not a schema is elaborated on below.

Fullness

For given ${\displaystyle a}$ and ${\displaystyle b}$, let ${\displaystyle {\mathcal {R}}_{ab}}$ be the class of all total relations between ${\displaystyle a}$ and ${\displaystyle b}$. This class is given as

${\displaystyle r\in {\mathcal {R}}_{ab}\leftrightarrow {\Big (}{\big (}\forall (x\in a).\exists (y\in b).\langle x,y\rangle \in r{\big )}\,\land \,{\big (}\forall (p\in r).\exists (x\in a).\exists (y\in b).p=\langle x,y\rangle {\big )}{\Big )}}$

As opposed to the function definition, there is no unique existence quantifier in ${\displaystyle \exists !(y\in b)}$. The class ${\displaystyle {\mathcal {R}}_{ab}}$ represents the space of "non-unique-valued functions" or "multivalued functions" from ${\displaystyle a}$ to ${\displaystyle b}$, but as set of individual pairs with right projection in ${\displaystyle b}$. The second clause says that one is concerned with only these relations, not those which are total on ${\displaystyle a}$ but also extend their domain beyond ${\displaystyle a}$.

One does not postulate ${\displaystyle {\mathcal {R}}_{ab}}$ to be a set, since with Replacement one can use this collection of relations between a set ${\displaystyle a}$ and the finite ${\displaystyle b=\{0,1\}}$, i.e. the "bi-valued functions on ${\displaystyle a}$", to extract the set ${\displaystyle {\mathcal {P}}_{a}}$ of all its subsets. In other words ${\displaystyle {\mathcal {R}}_{ab}}$ being a set would imply the Powerset axiom.

Over ${\displaystyle {\mathsf {ECTS}}+{\text{Strong Collection}}}$, there is a single, somewhat clearer alternative axiom to the Subset Collection schema. It postulates the existence of a sufficiently large set ${\displaystyle {\mathcal {S}}_{ab}}$ of total relations between ${\displaystyle a}$ and ${\displaystyle b}$.

This says that for any two sets ${\displaystyle a}$ and ${\displaystyle b}$, there exists a set ${\displaystyle {\mathcal {S}}_{ab}\subset {\mathcal {R}}_{ab}}$ which among its members inhabits a still total relation ${\displaystyle s\in {\mathcal {S}}_{ab}}$ for any given total relation ${\displaystyle r\in {\mathcal {R}}_{ab}}$.

On a given domain ${\displaystyle a}$, the functions are exactly the sparsest total relations, namely the unique valued ones. Therefore, the axiom implies that there is a set such that all functions are in it. In this way, Fullness implies Exponentiation. It further implies binary refinement, already over ${\displaystyle {\mathsf {BCST}}}$.

The Fullness axiom, as well as dependent choice, is in turn also implied by the so-called Presentation Axiom about sections, which can also be formulated category theoretically.

Metalogic of CZF

${\displaystyle {\mathsf {CZF}}}$ has the numerical existence property and the disjunctive property, but there are concessions: ${\displaystyle {\mathsf {CZF}}}$ lacks the existence property due to the Subset Collection Schema or Fullness axiom. The schema can also be an obstacle for realizability models. The existence property is not lacking when the weaker Exponentiation or the stronger but impredicative Powerset axiom axiom is adopted instead. The latter is in general lacking a constructive interpretation.

Unprovable claims

The theory is consistent with some anti-classical assertions, but on its own proves nothing not provable in ${\displaystyle {\mathsf {ZF}}}$. Some prominent statements not proven by the theory (nor by ${\displaystyle {\mathsf {IZF}}}$, for that matter) are part of the principles listed above, in the sections on constructive schools in analysis, on the Cauchy construction and on non-constructive principles. What follows concerns set theoretical concepts:

The bounded notion of a transitive set of transitive sets is a good way to define ordinals and enables induction on ordinals. But notably, this definition includes some ${\displaystyle \Delta _{0}}$-subsets in ${\displaystyle {\mathsf {CZF}}}$. So assuming that the membership of ${\displaystyle 0}$ is decidable in all successor ordinals ${\displaystyle S\alpha }$ proves ${\displaystyle {\mathrm {PEM} }}$ for bounded formulas in ${\displaystyle {\mathsf {CZF}}}$. Also, neither linearity of ordinals, nor existence of power sets of finite sets are derivable in this theory, as assuming either implies Power set. The circumstance that ordinals are better behaved in the classical than in the constructive context manifests in a different theory of large set existence postulates.

Consider the functions the domain of which is ${\displaystyle \omega }$ or some ${\displaystyle n\in \omega }$. These are sequences and their ranges are counted sets. Denote by ${\displaystyle C}$ the class characterized as the smallest codomain such that the ranges of the aforementioned functions into ${\displaystyle C}$ are also itself members of ${\displaystyle C}$. In ${\displaystyle {\mathsf {ZF}}}$, this is the set ${\displaystyle H_{\aleph _{1}}}$ of hereditarily countable sets and has ordinal rank at most ${\displaystyle \omega _{2}}$. In ${\displaystyle {\mathsf {ZF}}}$, it is uncountable (as it also contains all countable ordinals, the cardinality of which is denoted ${\displaystyle \aleph _{1}}$) but its cardinality is not necessarily that of ${\displaystyle {\mathbb {R} }}$. Meanwhile, ${\displaystyle {\mathsf {CZF}}}$ does not prove ${\displaystyle C}$ even constitutes a set, even when countable choice is assumed.

Finally, the theory does not prove that all function spaces formed from sets in the constructible universe ${\displaystyle L}$ are sets inside ${\displaystyle L}$, and this holds even when assuming Powerset instead of the weaker Exponentiation axiom. So this is a particular statement preventing ${\displaystyle {\mathsf {CZF}}}$ from proving the class ${\displaystyle L}$ to be a model of ${\displaystyle {\mathsf {CZF}}}$.

Ordinal analysis

Taking ${\displaystyle {\mathsf {CZF}}}$ and dropping set induction gives a theory that is conservative over ${\displaystyle {\mathsf {HA}}}$ for arithmetic statements, in that sense that it proves the same arithmetical statements for its ${\displaystyle {\mathsf {HA}}}$-model ${\displaystyle \omega }$. Adding back just mathematical induction gives a theory with proof theoretic ordinal ${\displaystyle \varphi (\varepsilon _{0},0)}$, which is the first common fixed point of the Veblen functions ${\displaystyle \varphi _{\beta }}$ for ${\displaystyle \beta <\varepsilon _{0}}$. This is the same ordinal as for ${\displaystyle {\mathsf {ML_{1}}}}$ and is below the Feferman–Schütte ordinal ${\displaystyle \Gamma _{0}}$. Exhibiting a type theoretical model, the full theory ${\displaystyle {\mathsf {CZF}}}$ goes beyond ${\displaystyle \Gamma _{0}}$, its ordinal still being the modest Bachmann–Howard ordinal. Assuming the class of trichotomous ordinals is a set raises the proof theoretical strength of ${\displaystyle {\mathsf {CZF}}}$ (but not of ${\displaystyle {\mathsf {IZF}}}$).

Being related to inductive definitions or bar induction, the regular extension axiom ${\displaystyle {\mathrm {REA} }}$ raises the proof theoretical strength of ${\displaystyle {\mathsf {CZF}}}$. This large set axiom, granting the existence of certain nice supersets for every set, is proven by ${\displaystyle {\mathsf {ZFC}}}$.

Models

The category of sets and functions of ${\displaystyle {\mathsf {CZF}}+{\mathrm {REA} }}$ is a ${\displaystyle \Pi W}$-pretopos. Without diverging into topos theory, certain extended such ${\displaystyle \Pi W}$-pretopoi contain models of ${\displaystyle {\mathsf {CZF}}+{\mathrm {REA} }}$. The effective topos contains a model of this ${\displaystyle {\mathsf {CZF}}+{\mathrm {REA} }}$ based on maps characterized by certain good subcountability properties.

Separation, stated redundantly in a classical context, is constructively not implied by Replacement. The discussion so far only committed to the predicatively justified bounded Separation. Note that full Separation (together with ${\displaystyle {\mathrm {RDC} }}$, ${\displaystyle {\mathrm {MP} }}$ and also ${\displaystyle {\mathrm {IP} }}$ for sets) is validated in some effective topos models, meaning the axiom does not spoil cornerstones of the restrictive recursive school.

Related are type theoretical interpretations. In 1977 Aczel showed that ${\displaystyle {\mathsf {CZF}}}$ can still be interpreted in Martin-Löf type theory,^[26] using the propositions-as-types approach. More specifically, this uses one universe and ${\displaystyle W}$-types, providing what is now seen a standard model of ${\displaystyle {\mathsf {CZF}}}$ in ${\displaystyle {\mathsf {ML_{1}V}}}$.^[27]This is done in terms of the images of its functions and has a fairly direct constructive and predicative justification, while retaining the language of set theory. Roughly, there are two "big" types ${\displaystyle U,V}$, the sets are all given through any ${\displaystyle f\colon A\to V}$ on some ${\displaystyle A\colon U}$, and membership of a ${\displaystyle x}$ in the set is defined to hold when ${\displaystyle \exists (a\colon A).f(a)=x}$. Conversely, ${\displaystyle {\mathsf {CZF}}}$ interprets ${\displaystyle {\mathsf {ML_{1}V}}}$. All statements validated in the subcountable model of the set theory can be proven exactly via ${\displaystyle {\mathsf {CZF}}}$ plus the choice principle ${\displaystyle \Pi \Sigma }$- ${\displaystyle \mathrm {AC} }$, stated further above. As noted, theories like ${\displaystyle {\mathsf {CZF}}}$, and also together with choice, have the existence property for a broad class of sets in common mathematics. Martin-Löf type theories with additional induction principles validate corresponding set theoretical axioms.

Soundness and Completeness theorems of ${\displaystyle {\mathsf {CZF}}}$, with respect to realizability, have been established.

Breaking with ZF

One may of course add a Church's thesis.

One may postulate the subcountability of all sets. This already holds true in the type theoretical interpretation and the model in the effective topos. By Infinity and Exponentiation, ${\displaystyle \omega \to \omega }$ is an uncountable set, while the class ${\displaystyle {\mathcal {P}}_{\omega }}$ or even ${\displaystyle {\mathcal {P}}_{1}}$ is then provenly not a set, by Cantor's diagonal argument. So this theory then logically rejects Powerset and of course ${\displaystyle {\mathrm {PEM} }}$. Subcountability is also in contradiction with various large set axioms. (On the other hand, also using ${\displaystyle {\mathsf {CZF}}}$, some such axioms imply the consistency of theories such as ${\displaystyle {\mathsf {ZF}}}$ and stronger.)

As a rule of inference, ${\displaystyle {\mathsf {CZF}}}$ is closed under Troelstra's general uniformity for both ${\displaystyle z=\omega }$ and ${\displaystyle z=\{0,1\}}$. One may adopt it as an anti-classical axiom schema, the uniformity principle which may be denoted ${\displaystyle {\mathrm {UP} }}$,

${\displaystyle \forall z.{\big (}\forall x.\exists (y\in z).\phi (x,y){\big )}\to \exists (y\in z).\forall x.\phi (x,y)}$

This also is incompatible with the powerset axiom. The principle is also often formulated for ${\displaystyle z=\omega }$. Now for a binary set of labels ${\displaystyle z=\{0,1\}}$, ${\displaystyle {\mathrm {UP} }}$ implies the indecomposability schema ${\displaystyle {\mathrm {UZ} }}$, as noted.

In 1989 Ingrid Lindström showed that non-well-founded sets can also be interpreted in Martin-Löf type theory, which are obtained by replacing Set Induction in ${\displaystyle {\mathsf {CZF}}}$ with Aczel's anti-foundation axiom.^[28] The resulting theory ${\displaystyle {\mathsf {CZFA}}}$ may be studied by also adding back the ${\displaystyle \omega }$-induction schema or relativized dependent choice, as well as the assertion that every set is member of a transitive set.

Intuitionistic Zermelo–Fraenkel

The theory ${\displaystyle {\mathsf {IZF}}}$ is ${\displaystyle {\mathsf {CZF}}}$ adopting both the standard Separation as well as Power set and, as in ${\displaystyle {\mathsf {ZF}}}$, one conventionally formulates the theory with Collection below. As such, ${\displaystyle {\mathsf {IZF}}}$ can be seen as the most straight forward variant of ${\displaystyle {\mathsf {ZF}}}$ without PEM. So as noted, in ${\displaystyle {\mathsf {IZF}}}$, in place of Replacement, one may use the

While the axiom of replacement requires the relation ϕ to be functional over the set z (as in, for every x in z there is associated exactly one y), the Axiom of Collection does not. It merely requires there be associated at least one y, and it asserts the existence of a set which collects at least one such y for each such x. In classical ${\displaystyle {\mathsf {ZFC}}}$, the Collection schema implies the Axiom schema of replacement. When making use of Powerset (and only then), they can be shown to be classically equivalent.

While ${\displaystyle {\mathsf {IZF}}}$ is based on intuitionistic rather than classical logic, it is considered impredicative. It allows formation of sets via a power set operation and using the general Axiom of Separation with any proposition, including ones which contain quantifiers which are not bounded. Thus new sets can be formed in terms of the universe of all sets, distancing the theory from the bottom-up constructive perspective. So it is even easier to define sets ${\displaystyle \{x\in B\mid Q(x)\}}$ with undecidable membership, namely by making use of undecidable predicates defined on a set. The power set axiom further implies the existence of a set of truth values. In the presence of excluded middle, this set has two elements. In the absence of it, the set of truth values is also considered impredicative. The axioms of ${\displaystyle {\mathsf {IZF}}}$ are strong enough so that full PEM is already implied by PEM for bounded formulas. See also the previous discussion in the section on the Exponentiation axiom. And by the discussion about Separation, it is thus already implied by the particular formula ${\displaystyle \forall x.{\big (}0\in x\lor 0\notin x{\big )}}$, the principle that knowledge of membership of ${\displaystyle 0}$ shall always be decidable, no matter the set.

Metalogic

As implied above, the subcountability property cannot be adopted for all sets, given the theory proves ${\displaystyle {\mathcal {P}}_{\omega }}$ to be a set. The theory has many of the nice numerical existence properties and is e.g. consistent with Church's thesis principle as well as with ${\displaystyle \omega \to \omega }$ being subcountable. It also has the disjunctive property.

${\displaystyle {\mathsf {IZF}}}$ with Replacement instead of Collection has the general existence property, even when adopting relativized dependent choice on top of it all. But just ${\displaystyle {\mathsf {IZF}}}$ as formulated does not. The combination of schemas including full separation spoils it.

Even without PEM, the proof theoretic strength of ${\displaystyle {\mathsf {IZF}}}$ equals that of ${\displaystyle {\mathsf {ZF}}}$. And ${\displaystyle {\mathsf {HA}}}$ proves them equiconsistent and they prove the same ${\displaystyle \Pi _{1}^{0}}$-sentences.

Intuitionistic Z

Again on the weaker end, as with its historical counterpart Zermelo set theory, one may denote by ${\displaystyle {\mathsf {IZ}}}$ the intuitionistic theory set up like ${\displaystyle {\mathsf {IZF}}}$ but without Replacement, Collection or Induction.

Intuitionistic KP

Let us mention another very weak theory that has been investigated, namely Intuitionistic (or constructive) Kripke–Platek set theory ${\displaystyle {\mathsf {IKP}}}$. It has not only Separation but also Collection restricted to ${\displaystyle \Delta _{0}}$-formulas, i.e. it is similar to ${\displaystyle {\mathsf {BCST}}}$ but with Induction instead of full Replacement. The theory does not fit into the hierarchy as presented above, simply because it has Axiom schema of Set Induction from the start. This enables theorems involving the class of ordinals. The theory has the disjunction property. Of course, weaker versions of ${\displaystyle {\mathsf {IKP}}}$ are obtained by restricting the induction schema to narrower classes of formulas, say ${\displaystyle \Sigma _{1}}$. The theory is especially weak when studied without Infinity.

Sorted theories

Constructive set theory

As he presented it, Myhill's system ${\displaystyle {\mathsf {CST}}}$ is a theory using constructive first-order logic with identity and two more sorts beyond sets, namely natural numbers and functions. Its axioms are:

• The usual Axiom of Extensionality for sets, as well as one for functions, and the usual Axiom of union.
• The Axiom of restricted, or predicative, separation, which is a weakened form of the Separation axiom from classical set theory, requiring that any quantifications be bounded to another set, as discussed.
• A form of the Axiom of Infinity asserting that the collection of natural numbers (for which he introduces a constant ${\displaystyle \omega }$) is in fact a set.
• The axiom of Exponentiation, asserting that for any two sets, there is a third set which contains all (and only) the functions whose domain is the first set, and whose range is the second set. This is a greatly weakened form of the Axiom of power set in classical set theory, to which Myhill, among others, objected on the grounds of its impredicativity.

And furthermore:

• The usual Peano axioms for natural numbers.
• Axioms asserting that the domain and range of a function are both sets. Additionally, an Axiom of non-choice asserts the existence of a choice function in cases where the choice is already made. Together these act like the usual Replacement axiom in classical set theory.

One can roughly identify the strength of this theory with a constructive subtheories of ${\displaystyle {\mathsf {ZF}}}$ when comparing with the previous sections.

And finally the theory adopts

• An Axiom of dependent choice, which is much weaker than the usual Axiom of choice.

Bishop style set theory

Set theory in the flavor of Errett Bishop's constructivist school mirrors that of Myhill, but is set up in a way that sets come equipped with relations that govern their discreteness. Commonly, Dependent Choice is adopted.

A lot of analysis and module theory has been developed in this context.

Category theories

Not all formal logic theories of sets need to axiomize the binary membership predicate " ${\displaystyle \in }$" directly. A theory like the Elementary Theory of the Categories Of Set ( ${\displaystyle {\mathsf {ETCS}}}$), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic. Category theory can be set up as a theory of arrows and objects, although first-order axiomatizations only in terms of arrows are possible.

Beyond that, topoi also have internal languages that can be intuitionistic themselves and capture a notion of sets.

Good models of constructive set theories in category theory are the pretoposes mentioned in the Exponentiation section. For some good set theory, this may require enough projectives, an axiom about surjective "presentations" of set, implying Countable and Dependent Choice.

See also

• Axiom schema of predicative separation
• Constructive mathematics
• Constructive analysis
• Constructive Church's thesis rule and principle
• Computable set
• Diaconescu's theorem
• Disjunction and existence properties
• Epsilon-induction
• Hereditarily finite set
• Heyting arithmetic
• Impredicativity
• Intuitionistic type theory
• Law of excluded middle
• Ordinal analysis
• Set theory
• Subcountability

References

1. Feferman, Solomon (1998), In the Light of Logic, New York: Oxford University Press, pp. 280–283, 293–294, ISBN 0-195-08030-0
2. Troelstra, A. S., van Dalen D., Constructivism in mathematics: an introduction 1; Studies in Logic and the Foundations of Mathematics; Springer, 1988;
3. Bridges D., Ishihara H., Rathjen M., Schwichtenberg H. (Editors), Handbook of Constructive Mathematics; Studies in Logic and the Foundations of Mathematics; (2023) pp. 20-56
4. Myhill, "Some properties of Intuitionistic Zermelo-Fraenkel set theory", Proceedings of the 1971 Cambridge Summer School in Mathematical Logic (Lecture Notes in Mathematics 337) (1973) pp. 206-231
5. Crosilla, Laura; Set Theory: Constructive and Intuitionistic ZF; Stanford Encyclopedia of Philosophy; 2009
6. Peter Aczel and Michael Rathjen, Notes on Constructive Set Theory, Reports Institut Mittag-Leffler, Mathematical Logic - 2000/2001, No. 40
7. John L. Bell, Intuitionistic Set Theorys, 2018
8. Jeon, Hanul (2022), "Constructive Ackermann's interpretation", Annals of Pure and Applied Logic, 173 (5): 103086, arXiv:2010.04270, doi:10.1016/j.apal.2021.103086, S2CID 222271938
9. Shapiro, S., McCarty, C. & Rathjen, M., Intuitionistic sets and numbers: small set theory and Heyting arithmetic, https://doi.org/10.1007/s00153-024-00935-4, Arch. Math. Logic (2024)
10. Gambino, N. (2005). "Presheaf models for constructive set theories" (PDF). In Laura Crosilla and Peter Schuster (ed.). From Sets and Types to Topology and Analysis (PDF). pp. 62–96. doi:10.1093/acprof:oso/9780198566519.003.0004. ISBN 9780198566519.
11. Scott, D. S. (1985). Category-theoretic models for Intuitionistic Set Theory. Manuscript slides of a talk given at Carnegie-Mellon University
12. Benno van den Berg, Predicative topos theory and models for constructive set theory, Netherlands University, PhD thesis, 2006
13. Jech, Thomas (2003), Set Theory, Springer Monographs in Mathematics (Third Millennium ed.), Berlin, New York: Springer-Verlag, p. 642, ISBN 978-3-540-44085-7, Zbl 1007.03002
14. Gert Smolka, Set Theory in Type Theory, Lecture Notes, Saarland University, Jan. 2015
15. Gert Smolka and Kathrin Stark, Hereditarily Finite Sets in Constructive Type Theory, Proc. of ITP 2016, Nancy, France, Springer LNCS, May 2015
16. Diener, Hannes (2020). "Constructive Reverse Mathematics". arXiv:1804.05495 [math.LO].
17. Sørenson, Morten; Urzyczyn, Paweł (1998), Lectures on the Curry-Howard Isomorphism, CiteSeerX 10.1.1.17.7385, p. 239
18. Smith, Peter (2007). An introduction to Gödel's Theorems (PDF). Cambridge, U.K.: Cambridge University Press. ISBN 978-0-521-67453-9. MR 2384958., p. 297
19. Pradic, Pierre; Brown, Chad E. (2019). "Cantor-Bernstein implies Excluded Middle". arXiv:1904.09193 [math.LO].
20. Michael Rathjen, Choice principles in constructive and classical set theories, Cambridge University Press: 31 March 2017
21. Gitman, Victoria (2011), What is the theory ZFC without power set, arXiv:1110.2430
22. Shulman, Michael (2019), "Comparing material and structural set theories", Annals of Pure and Applied Logic, 170 (4): 465-504, arXiv:1808.05204, doi:10.1016/j.apal.2018.11.002
23. Errett Bishop, Foundations of Constructive Analysis, July 1967
24. Robert S. Lubarsky, On the Cauchy Completeness of the Constructive Cauchy Reals, July 2015
25. Matthew Ralph John Hendtlass, Constructing fixed points and economic equilibria, PhD Thesis, University of Leeds, April 2013
26. Aczel, Peter: 1978. The type theoretic interpretation of constructive set theory. In: A. MacIntyre et al. (eds.), Logic Colloquium '77, Amsterdam: North-Holland, 55–66.
27. Rathjen, M. (2004), "Predicativity, Circularity, and Anti-Foundation" (PDF), in Link, Godehard (ed.), One Hundred Years of Russell ́s Paradox: Mathematics, Logic, Philosophy, Walter de Gruyter, ISBN 978-3-11-019968-0
28. Lindström, Ingrid: 1989. A construction of non-well-founded sets within Martin-Löf type theory. Journal of Symbolic Logic 54: 57–64.

Further reading

• Troelstra, Anne; van Dalen, Dirk (1988). Constructivism in Mathematics, Vol. 2. Studies in Logic and the Foundations of Mathematics. p. 619. ISBN 978-0-444-70358-3.
• Aczel, P. and Rathjen, M. (2001). Notes on constructive set theory. Technical Report 40, 2000/2001. Mittag-Leffler Institute, Sweden.

External links

• Crosilla, Laura (13 February 2019). "Set Theory: Constructive and Intuitionistic ZF". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
• Van den Berg, Benno (7 September 2012). "Constructive set theory – an overview" (PDF). Slides from Heyting dag, Amsterdam