Teoría constructiva de conjuntos

Con proposiciones computacionalmente indecidibles que ya surgen en la aritmética de Robinson , incluso la separación predicativa permite definir fácilmente subconjuntos esquivos. En marcado contraste con el marco clásico, las teorías constructivas de conjuntos 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,${\displaystyle \top }$o${\displaystyle \bot }$. Asimismo, la recta real puede considerarse indescomponible en este sentido. La indecidibilidad de las disyunciones también afecta a 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.${\displaystyle (\alpha \in \beta )\lor (\alpha =\beta )\lor (\beta \in \alpha )}$Esto determina si la relación es tricotómica . Una teoría debilitada de los ordinales a su vez afecta la fuerza teórica de la prueba definida en el análisis ordinal .

A cambio, las teorías constructivas de conjuntos pueden exhibir atractivas propiedades de disyunción y existencia , como es familiar en el estudio de las teorías aritméticas constructivas. Estas son características de una teoría fija que relacionan metalógicamente juicios sobre 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 demostración . En particular, estas son la propiedad de existencia numérica y la propiedad disyuntiva estrechamente relacionada, así como ser cerradas bajo la regla de Church , lo que demuestra que cualquier función dada es computable . ^{[ 2 ]}

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

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

El papel análogo al de los números realizados en aritmética lo desempeñan aquí los conjuntos definidos cuya existencia se demuestra mediante (o de acuerdo con) la teoría. 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 de las teorías analizadas tienden a poseer diversas propiedades numéricas, la propiedad de existencia puede verse fácilmente comprometida, como se explicará 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 también pueden, de hecho, estar restringidas de manera que exhiban la propiedad de existencia fuerte. En la teoría de conjuntos de Zermelo-Fraenkel, con todos los conjuntos considerados definibles por orden , una teoría denotada${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {HOD} })}$, no existen conjuntos sin tal definibilidad. La propiedad también se impone a través del postulado del universo construible en${\displaystyle {\mathsf {ZF}}+({\mathrm {V} }={\mathrm {L} })}$. En contraste, consideremos la teoría${\displaystyle {\mathsf {ZFC}}}$dado por${\displaystyle {\mathsf {ZF}}}$más el postulado completo del axioma de elección de existencia : Recordemos que esta colección de axiomas prueba el teorema del buen ordenamiento , lo que implica que existen buenos ordenamientos para cualquier conjunto. En particular, esto significa que las relaciones${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$formalmente existen que establecen el buen orden de${\displaystyle {\mathbb {R} }}$(es decir, la teoría afirma la existencia de un elemento mínimo para todos los subconjuntos de${\displaystyle {\mathbb {R} }}$con respecto a esas relaciones). Esto a pesar de que se sabe que la definibilidad de tal ordenamiento es independiente de${\displaystyle {\mathsf {ZFC}}}$Esto último implica que para ninguna fórmula en particular${\displaystyle \psi }$En el lenguaje de la teoría, ¿demuestra la teoría que el conjunto correspondiente es una relación de buen orden de los números reales? Entonces${\displaystyle {\mathsf {ZFC}}}$prueba formalmente la existencia de un subconjunto${\displaystyle W\subset {\mathbb {R} }\times {\mathbb {R} }}$con la propiedad de ser una relación bien ordenada, pero al mismo tiempo ningún conjunto particular${\displaystyle W}$es posible definir para qué propiedad podría validarse.

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

En cambio, se puede considerar adjuntar la regla correspondiente a la propiedad metateórica como una implicación (en el sentido de "${\displaystyle \to }$") a${\displaystyle {\mathsf {T}}}$, como un esquema axiomático o en forma cuantificada. Una situación comúnmente estudiada es la de un fijo${\displaystyle {\mathsf {T}}}$exhibiendo la propiedad metateórica del siguiente tipo: Por ejemplo, de alguna colección de fórmulas de una forma particular, aquí capturada mediante${\displaystyle \phi }$y${\displaystyle \psi }$, uno estableció la existencia de un número${\displaystyle {\mathrm {e} }}$de modo que${\displaystyle {\mathsf {T}}\vdash \phi \implies {\mathsf {T}}\vdash \psi ({\underline {\mathrm {e} }})}$Aquí se puede postular entonces${\displaystyle \phi \to \exists (e\in {\mathbb {N} }).\psi (e)}$donde el límite${\displaystyle e}$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.${\displaystyle {\mathsf {HA}}}$y, además, el principio de tesis correspondiente de la Iglesia${\displaystyle {\mathrm {CT} }_{0}}$puede adoptarse consistentemente como un axioma. La nueva teoría con el principio añadido es anticlásica, en el sentido de que puede que ya no sea consistente adoptar también${\displaystyle {\mathrm {PEM} }}$De manera similar, adhiriéndose al principio del tercero excluido${\displaystyle {\mathrm {PEM} }}$Según alguna teoría${\displaystyle {\mathsf {T}}}$, la teoría así obtenida puede probar nuevos enunciados estrictamente clásicos, y esto puede estropear algunas de las propiedades metateóricas que se habían establecido previamente para${\displaystyle {\mathsf {T}}}$De esta manera,${\displaystyle {\mathrm {CT} }_{0}}$puede que no se adopte en${\displaystyle {\mathsf {HA}}+{\mathrm {PEM} }}$, también conocida como aritmética de Peano${\displaystyle {\mathsf {PA}}}$.

El enfoque en esta subsección estará en las teorías de conjuntos con cuantificación sobre una noción completamente formal de un espacio de secuencias infinitas, es decir, un espacio de funciones, como se introducirá más adelante. Una traducción de la regla de Church al lenguaje de la propia teoría 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${\displaystyle n}$siendo asignado al número${\displaystyle f(n)}$es, a través de${\displaystyle w}$, se comprobó que era un mapeo computable. Aquí${\displaystyle {\mathbb {N} }}$ahora denota un modelo de teoría de conjuntos de los números naturales estándar y${\displaystyle e}$es un índice con respecto a una enumeración de programa fija. Se han utilizado variantes más fuertes que extienden este principio a las funciones.${\displaystyle f\in {\mathbb {N} }^{X}}$definidos en dominios${\displaystyle X\subset {\mathbb {N} }}$de baja complejidad. El principio rechaza la decidibilidad para el predicado.${\displaystyle Q(e)}$definido como${\displaystyle \exists (w\in {\mathbb {N} }).T(e,e,w)}$, expresando que${\displaystyle e}$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${\displaystyle f}$pero que aún así hacen que los principios sean inconsistentes al afirmar la existencia de funciones que, según se ha demostrado, no tienen realización recursiva. Algunas formas de la tesis de Church como principio son incluso consistentes con la teoría aritmética clásica, débil y denominada de segundo orden.${\displaystyle {\mathsf {RCA}}_{0}}$, un subsistema de la teoría de primer orden de dos tipos${\displaystyle {\mathsf {Z}}_{2}}$.

La colección de funciones computables es clásicamente subcontable , lo cual clásicamente es lo mismo que ser contable. Pero las teorías clásicas de conjuntos generalmente afirmarán que${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$También posee otras funciones además de las computables. Por ejemplo, hay una demostración en${\displaystyle {\mathsf {ZF}}}$que existen funciones totales (en el sentido de la teoría de conjuntos) que no pueden ser capturadas por una máquina de Turing . Tomando en serio el mundo computable como ontología, un ejemplo primordial 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 interminables de números naturales (${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$Como axioma en una teoría constructiva, la pequeñez (en términos clásicos) de esta colección, en algunas realizaciones de la teoría de conjuntos, queda ya implícita en la propia teoría. Una teoría constructiva también puede no adoptar axiomas clásicos ni anticlásicos, manteniéndose así neutral respecto a ambas posibilidades.

Los principios constructivos ya lo demuestran${\displaystyle \forall (x\in X).\neg \neg {\big (}Q(x)\lor \neg Q(x){\big )}}$para cualquier${\displaystyle Q}$. Y así para cualquier elemento dado${\displaystyle x}$de${\displaystyle X}$, la afirmación del tercero excluido correspondiente para la proposición no puede ser negada. De hecho, para cualquier dado${\displaystyle x}$, por no contradicción es imposible descartar${\displaystyle Q(x)}$y descartar su negación de una vez por todas, y la regla de De Morgan pertinente se aplica como se indicó anteriormente. Pero una teoría también puede, en algunos casos, permitir la afirmación de rechazo.${\displaystyle \neg \forall (x\in X).{\big (}Q(x)\lor \neg Q(x){\big )}}$. Adoptar esto no requiere proporcionar una en particular${\displaystyle t\in X}$presenciar el fracaso del tercero excluido para la proposición en particular${\displaystyle Q(t)}$, es decir, presenciar la inconsistencia${\displaystyle \neg {\big (}Q(t)\lor \neg Q(t){\big )}}$Predicados${\displaystyle Q(x)}$en un dominio infinito${\displaystyle X}$corresponder a problemas de decisión . Motivados por problemas que se ha demostrado que son computacionalmente indecidibles , se puede rechazar la posibilidad de decidibilidad de un predicado sin hacer también ninguna afirmación de existencia en${\displaystyle X}$. Como otro ejemplo, tal situación se impone en el análisis intuicionista brouweriano , en un caso donde el cuantificador abarca infinitas secuencias binarias sin fin y${\displaystyle Q(x)}$indica que una secuencia${\displaystyle x}$es cero en todas partes. En cuanto a esta propiedad, de ser identificada de manera concluyente como la secuencia que es siempre constante, adoptar el principio de continuidad de Brouwer descarta estrictamente que esto pueda ser probado decidible para todas las secuencias.

Así pues, en un contexto constructivo con una lógica denominada no clásica, como la que se utiliza aquí, se pueden adoptar consistentemente axiomas que, además de contradecir las formas cuantificadas del principio del tercero excluido, resultan no constructivos en el sentido computable o según lo determinado por las propiedades de existencia metalógicas previamente analizadas. De este modo, una teoría constructiva de conjuntos también puede proporcionar el marco para estudiar teorías no clásicas, como por ejemplo, los anillos que modelan el análisis infinitesimal suave .

Muchas teorías estudiadas en la teoría constructiva de conjuntos 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. Dichas teorías también pueden interpretarse en cualquier modelo de${\displaystyle {\mathsf {ZF}}}$.

Comparando la aritmética con las teorías en el lenguaje de la teoría de conjuntos, por un lado, la aritmética clásica de Peano, por otro.${\displaystyle {\mathsf {PA}}}$es biinterpretable con la teoría dada por${\displaystyle {\mathsf {ZF}}}$menos infinito y sin conjuntos infinitos, más la existencia de todos los cierres transitivos . (Esto último también se deduce después de promover la regularidad al esquema de inducción de conjuntos , que se analiza más adelante). Asimismo, la aritmética constructiva también puede tomarse como una disculpa por la mayoría de los axiomas adoptados en${\displaystyle {\mathsf {CZF}}}$Aritmética de Heyting${\displaystyle {\mathsf {HA}}}$es biinterpretable con una teoría de conjuntos constructiva débil, ^{[ 8 ] [ 9 ]} como también se describe en el artículo sobre${\displaystyle {\mathsf {HA}}}$. Se puede caracterizar aritméticamente una relación de pertenencia "${\displaystyle \in }$"y con ello demostrar, en lugar de la existencia de un conjunto de números naturales,${\displaystyle \omega }$- que todos los conjuntos en su teoría están en biyección con un natural de von Neumann (finito) , un principio denotado${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$Este contexto valida aún más la Extensionalidad, el Emparejamiento, la Unión, la Intersección Binaria (que está relacionada con el esquema axiomático de separación predicativa ) y el esquema de Inducción de Conjuntos. Tomados como axiomas, los principios mencionados constituyen una teoría de conjuntos que ya es idéntica a la teoría dada por${\displaystyle {\mathsf {CZF}}}$menos la existencia de${\displaystyle \omega }$pero además${\displaystyle {\mathrm {V} }={\mathrm {Fin} }}$como axioma. Todos esos axiomas se discuten en detalle a continuación. Relativamente,${\displaystyle {\mathsf {CZF}}}$También demuestra que los conjuntos hereditariamente finitos cumplen todos los axiomas anteriores. Este es un resultado que persiste al pasar a${\displaystyle {\mathsf {PA}}}$y${\displaystyle {\mathsf {ZF}}}$menos infinito. Por otro lado,${\displaystyle {\mathsf {CZF}}}$Además, la separación total no es más fuerte que la aritmética clásica de segundo orden.

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

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

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 .${\displaystyle =}$" de conjuntos y ese símbolo puede, por abuso de notación , usarse para clases. Un conjunto en el que el predicado de igualdad es decidible también se llama discreto . Negación "${\displaystyle \neg }$" de igualdad a veces se llama negación de la igualdad, y comúnmente se escribe "${\displaystyle \neq }$Sin embargo, en un contexto con relaciones de separación , por ejemplo al tratar con secuencias, este último símbolo también se utiliza a veces para algo diferente.

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

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

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

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

Uno abrevia${\displaystyle \forall z.{\big (}z\in A\to Q(z){\big )}}$por${\displaystyle \forall (z\in A).Q(z)}$y${\displaystyle \exists z.{\big (}z\in A\land Q(z){\big )}}$por${\displaystyle \exists (z\in A).Q(z)}$La noción sintáctica de cuantificación limitada 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${\displaystyle \forall (z\in A).z\in B}$, es decir${\displaystyle \forall z.(z\in A\to z\in B)}$, por${\displaystyle A\subset B}$. Para un predicado${\displaystyle Q}$trivialmente${\displaystyle \forall z.{\big (}(z\in B\land Q(z))\to z\in B{\big )}}$Y por lo tanto se deduce que${\displaystyle \{z\in B\mid Q(z)\}\subset B}$. La noción de cuantificadores acotados por subconjuntos, como en${\displaystyle \forall (z\subset A).z\in B}$También se ha utilizado en investigaciones de teoría de conjuntos, pero no se destacará más aquí.

Si existe de forma comprobada un conjunto dentro de una clase, es decir${\displaystyle \exists z.(z\in A)}$, entonces se le llama habitado . También se puede utilizar la cuantificación en${\displaystyle A}$para expresar esto como${\displaystyle \exists (z\in A).(z=z)}$La clase${\displaystyle A}$Entonces, se demuestra que no es el conjunto vacío, que se introduce más adelante. Si bien es clásicamente equivalente, la noción de no vacío constructivo es más débil, con dos negaciones, y debería llamarse « no deshabitado ». Desafortunadamente, el término para la noción más útil de «habitado» rara vez se usa en matemáticas clásicas.

El hecho de que existan dos maneras de expresar que las clases son disjuntas sí refleja muchas de las reglas de negación válidas desde una perspectiva intuicionista:${\displaystyle {\big (}\forall (x\in A).x\notin B{\big )}\leftrightarrow \neg \exists (x\in A).x\in B}$. Utilizando la notación anterior, se trata de una equivalencia puramente lógica y en este artículo la proposición será además expresable como${\displaystyle A\cap B=\{\}}$.

Una subclase${\displaystyle A\subset B}$se llama desmontable de${\displaystyle B}$si el predicado de pertenencia relativizado es decidible, es decir, si${\displaystyle \forall (x\in B).x\in A\lor x\notin A}$Se considera decidible si la superclase es clara a partir del contexto; a menudo, este es el conjunto de los números naturales.

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

Con${\displaystyle A}$de pie por${\displaystyle \{z\mid Q(z)\}}$, la conveniente relación de notación entre${\displaystyle x\in A}$y${\displaystyle Q(x)}$, axiomas de la forma${\displaystyle \exists a.\forall z.{\big (}z\in a\leftrightarrow Q(z){\big )}}$postular que la clase de todos los conjuntos para los cuales${\displaystyle Q}$contiene en realidad forma un conjunto . De manera menos formal, esto puede expresarse como${\displaystyle \exists a.a\simeq A}$. Asimismo, la proposición${\displaystyle \forall a.(a\simeq A)\to P(a)}$transmite "${\displaystyle P(A)}$cuando${\displaystyle A}$está entre los conjuntos de la teoría." Para el caso en que${\displaystyle P}$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${\displaystyle A}$como un conjunto.

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

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

Aunque se adopta con frecuencia, este axioma ha sido criticado en el pensamiento constructivo, ya que en la práctica reduce a la mínima expresión las propiedades definidas de manera diferente, o al menos los conjuntos considerados como la extensión de estas propiedades, una noción fregiana .

Las teorías de tipos modernas podrían, en cambio, tener como objetivo definir la equivalencia requerida.${\displaystyle \simeq }$"En términos de funciones, véase, por ejemplo, la equivalencia de tipos . El concepto relacionado de extensionalidad de funciones a menudo no se adopta en la teoría de tipos."

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

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

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

Teoría constructiva básica de conjuntos${\displaystyle {\mathsf {BCST}}}$Consta de varios axiomas que también forman parte de la teoría de conjuntos estándar, salvo que el llamado axioma de Separación "completa" se ve debilitado. Además de los cuatro axiomas anteriores, postula la Separación Predicativa, así como el esquema de Reemplazo.

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

Cuando el predicado se toma como la negación${\displaystyle \phi (x):=x\notin z}$, se obtiene el principio de diferencia, que garantiza la existencia de cualquier conjunto${\displaystyle y\setminus z}$. Tenga en cuenta que conjuntos como${\displaystyle y\setminus y}$o${\displaystyle \{x\in y\mid \neg (x=x)\}}$siempre están vacíos. Por lo tanto, como se ha señalado, de la Separación y la existencia de al menos un conjunto (por ejemplo, el Infinito a continuación) se deduce la existencia del conjunto vacío.${\displaystyle \{\}}$(también denotado${\displaystyle 0}$). Dentro de este contexto conservador de${\displaystyle {\mathsf {BCST}}}$El esquema de Separación Predicativa es, en realidad, equivalente al Conjunto Vacío más la existencia de la intersección binaria para cualquier par de conjuntos. Esta última variante de axiomatización no utiliza un esquema de fórmulas.

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${\displaystyle \Delta _{0}}$, 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 praxis, las subclases genéricas de conjuntos siguen siendo parte del lenguaje matemático. Como el alcance de las subclases que son demostrablemente conjuntos es sensible a los conjuntos que ya existen, este alcance se amplía cuando se agregan más postulados de existencia de conjuntos.

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

Si el axioma de separación de uno permite la separación con${\displaystyle P}$, entonces${\displaystyle B}$es un subconjunto , que puede llamarse el valor de verdad asociado con${\displaystyle P}$Dos valores de verdad pueden demostrarse iguales, como conjuntos, mediante la demostración de una equivalencia. En términos de esta terminología, el conjunto de valores de prueba puede entenderse a priori como rico. Como era de esperar, las proposiciones decidibles tienen uno de un conjunto binario de valores de verdad. La disyunción del tercero excluido para eso${\displaystyle P}$Esto también queda implícito en la declaración global.${\displaystyle \forall b.(0\in b)\lor (0\notin b)}$.

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 un conjunto. Cuando en una teoría hay una demostración de${\displaystyle \neg \exists x.A\subset x}$, entonces${\displaystyle A}$debe ser apropiado. (Al adoptar la perspectiva de${\displaystyle {\mathsf {ZF}}}$En la teoría de conjuntos, que posee separación completa, las clases propias se consideran generalmente aquellas que son "demasiado grandes" para ser un conjunto. (Técnicamente, son subclases de la jerarquía acumulativa que se extienden más allá de cualquier límite ordinal).

Según una observación en la sección sobre la fusión de conjuntos, no se puede descartar consistentemente que un conjunto sea miembro de una clase de la forma${\displaystyle A\cup \{x\mid x\notin A\}}$. Una prueba constructiva de que pertenece a esa clase contiene información. Ahora bien, si${\displaystyle A}$es un conjunto, entonces la clase${\displaystyle \{x\mid x\notin A\}}$es demostrablemente correcto. Lo siguiente demuestra esto en el caso especial cuando${\displaystyle A}$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.

Lo siguiente se aplica a cualquier relación${\displaystyle E}$. Da una condición puramente lógica tal que dos términos${\displaystyle s}$y${\displaystyle y}$no puede ser${\displaystyle E}$-relacionados entre sí.

${\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 del disyunto final,${\displaystyle \neg sEy}$. La expresión${\displaystyle \neg (x\in x)}$no implica cuantificación ilimitada y, por lo tanto, está permitida en Separación. La construcción de Russel a su vez muestra que${\displaystyle \{x\in y\mid x\notin x\}\notin y}$. Así que para cualquier conjunto${\displaystyle y}$, La separación predicativa por sí sola implica que existe un conjunto que no es miembro de${\displaystyle y}$En particular, en esta teoría no puede existir ningún conjunto universal .

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

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

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

Esto ya implica que ningún conjunto${\displaystyle y}$es igual a la subclase${\displaystyle \{x\mid x\notin x\}}$de la clase universal, es decir, que la subclase también es propia. Pero incluso en${\displaystyle {\mathsf {ZF}}}$Sin regularidad, es consistente que exista una clase propia de singletons que se contengan exactamente a sí mismos.

Como nota al margen, en una teoría con estratificación como Intuitionistic New Foundations , la expresión sintáctica${\displaystyle x\in x}$Esto puede ser desadmisible en la Separación. A su vez, la demostración anterior de la negación de la existencia de un conjunto universal no puede realizarse en esa teoría.

El esquema axiomático de separación predicativa también se denomina${\displaystyle \Delta _{0}}$-Separación o Separación Acotada, como en Separación solo para cuantificadores acotados por conjuntos . (Nota de advertencia: la nomenclatura de la jerarquía de Lévy es análoga a${\displaystyle \Delta _{0}^{0}}$En 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${\displaystyle \Sigma _{1}^{0}}$o superior. Finalmente, tenga en cuenta que un${\displaystyle \Delta _{0}}$La clasificación de una fórmula puede expresarse hasta la equivalencia en la teoría.

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

La restricción en el axioma también controla las definiciones impredicativas : la existencia no debería, en el mejor de los casos, afirmarse para objetos que no son explícitamente descriptibles, o cuya definición los involucra a ellos mismos o la referencia a una clase propia, como cuando una propiedad a verificar involucra un cuantificador universal. Así, en una teoría constructiva sin el axioma del conjunto potencia , cuando${\displaystyle R}$denota algún predicado 2-ario, generalmente no se debe esperar una subclase${\displaystyle s}$de${\displaystyle y}$ser un conjunto, en caso de que esté definido, por ejemplo, como en

${\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${\displaystyle t\subset y}$. Tenga en cuenta que si esta subclase${\displaystyle s}$de${\displaystyle y}$Si se demuestra que es un conjunto, entonces este subconjunto también está dentro del ámbito ilimitado de la variable de conjunto.${\displaystyle t}$En otras palabras, como la propiedad de la subclase${\displaystyle s\subset y}$Se cumple este conjunto exacto${\displaystyle s}$, definido mediante la expresión${\displaystyle R(x,s)}$desempeñaría un papel en su propia caracterización.

Si bien la Separación predicativa conduce a que menos definiciones de clases dadas sean conjuntos, puede enfatizarse que muchas definiciones de clases que son clásicamente equivalentes no lo son cuando uno se restringe a la lógica más débil. Debido a la posible indecidibilidad de los predicados generales, la noción de subconjunto y subclase es automáticamente más elaborada en las teorías constructivas de conjuntos que en las clásicas. 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${\displaystyle {\mathsf {IZF}}}$Sin embargo, esto perjudica tanto la propiedad de existencia como las interpretaciones estándar de la teoría de tipos, y de esta manera, invalida una visión ascendente de los conjuntos constructivos. Cabe mencionar que, dado que la subtipificación no es una característica necesaria de la teoría de tipos constructiva , se puede afirmar que la teoría de conjuntos constructiva difiere considerablemente de dicho marco.

A continuación, considere el

Consiste en otorgar existencia, como conjuntos, al rango de predicados con características de función, obtenidos a través de sus dominios. En la formulación anterior, el predicado no está restringido de forma 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.

Mediante reemplazo, la existencia de cualquier par${\displaystyle \{x,y\}}$También se deduce de cualquier otro par en particular, como por ejemplo:${\displaystyle \{0,1\}=2=SS0}$. Pero como la unión binaria utilizada en${\displaystyle S}$Como ya se ha utilizado el axioma de emparejamiento, este enfoque requiere postular la existencia de${\displaystyle 2}$sobre el de${\displaystyle 0}$. En una teoría con el axioma impredicativo del conjunto de potencias, la existencia de${\displaystyle 2\subset {\mathcal {P}}{\mathcal {P}}0}$También se puede demostrar mediante la separación.

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

La sustitución es relevante para la comprensión de funciones y puede considerarse una forma de comprensión más general. Solo cuando se asume${\displaystyle {\mathrm {PEM} }}$¿El reemplazo ya implica una separación total?${\displaystyle {\mathsf {ZF}}}$, El reemplazo es principalmente importante para probar la existencia de conjuntos de alto rango , es decir, a través de instancias del esquema axiomático donde${\displaystyle \phi (x,y)}$relaciona un conjunto relativamente pequeño${\displaystyle x}$a los más grandes,${\displaystyle y}$.

Las teorías constructivas de conjuntos suelen tener un esquema axiomático de reemplazo, a veces restringido a fórmulas acotadas. Sin embargo, cuando se eliminan otros axiomas, este esquema a menudo se fortalece, no más allá de${\displaystyle {\mathsf {ZF}}}$sino simplemente para recuperar cierta fuerza demostrable. Existen axiomas más fuertes que no menoscaban las propiedades de existencia fuerte de una teoría, como se explica más adelante.

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

Colgantes de los elementos de la clase de conjuntos hereditariamente finitos${\displaystyle H_{\aleph _{0}}}$puede implementarse en cualquier lenguaje de programación común. Los axiomas discutidos anteriormente abstraen de operaciones comunes en el tipo de datos de conjunto : el emparejamiento y la unión están relacionados con el anidamiento y el aplanamiento , o tomados juntos, la concatenación. El reemplazo está relacionado con la comprensión y la separación está relacionada con el filtrado, a menudo más simple . El reemplazo junto con la inducción de conjuntos (introducida más adelante) es suficiente para axiomatizar${\displaystyle H_{\aleph _{0}}}$De forma constructiva, y esa teoría también se estudia sin el infinito.

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 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${\displaystyle {\mathsf {HA}}}$, alguna forma de inducción lo es. Para comparar, consideremos 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 solo mediante Extensionalidad, Adjunción y Separación completa.

La discusión continúa ahora con axiomas que garantizan la existencia de objetos que, de 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 conjunto completo. Los conjuntos infinitos son particularmente útiles para razonar sobre operaciones aplicadas a secuencias definidas en dominios de índices no acotados , por ejemplo, la diferenciación formal de una función generadora o la suma de dos secuencias de Cauchy.

Si se necesita 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 más adelante. Pero como es familiar en la teoría clásica de conjuntos, también se pueden formular formas débiles de infinito. Por ejemplo, uno puede simplemente postular la existencia de algún conjunto inductivo,${\displaystyle \exists y.\mathrm {Ind} _{y}}$- dicho postulado de existencia es suficiente cuando la separación completa puede utilizarse para delimitar el subconjunto inductivo.${\displaystyle w}$de los números naturales, el subconjunto común 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 lo siguiente${\displaystyle \Delta _{0}}$propiedad de existencia de predecesores en el sentido del modelo de von Neumann :

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

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

Obsérvese que a través de la expresión "${\displaystyle \exists (p\in w)}$"en el lado derecho, la propiedad que caracteriza${\displaystyle w}$por sus miembros${\displaystyle m}$Aquí, sintácticamente, contiene de nuevo el símbolo${\displaystyle w}$por sí mismo. Debido a la naturaleza ascendente de los números naturales, esto es dócil aquí. Suponiendo${\displaystyle \Delta _{0}}$-coloque la inducción encima de${\displaystyle {\mathsf {ECST}}}$, no hay dos conjuntos diferentes que tengan esta propiedad. También tenga en cuenta que existen formulaciones más largas de esta propiedad, evitando "${\displaystyle \exists (p\in w)}$"a favor de los cuantificadores no acotados."

Adoptando un axioma de infinito, la cuantificación acotada por conjuntos es válida en los predicados utilizados en${\displaystyle \Delta _{0}}$-La separación permite entonces explícitamente cuantificadores numéricamente ilimitados; no deben confundirse los dos significados de "limitado". Con${\displaystyle \omega }$a mano, llame a una clase de números${\displaystyle I\subset \omega }$limitado si se cumple la siguiente condición de existencia

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

Esta es una afirmación de finitud, formulada también de forma equivalente mediante${\displaystyle m\leq n\to n\notin I}$. De manera similar, para reflejar con mayor precisión la discusión de funciones que se presenta a continuación, considere la condición anterior en la forma${\displaystyle \exists (m\in \omega ).\forall (n\in I).(n<m)}$. Para las propiedades decidibles, estas son${\displaystyle \Sigma _{2}^{0}}$-enunciados en aritmética, pero con el Axioma del Infinito, los dos cuantificadores están ligados a un conjunto.

Para una clase${\displaystyle C}$, la afirmación de no acotación lógicamente positiva

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

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

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

Resulta instructivo recordar cómo una teoría con comprensión de conjuntos y extensionalidad termina codificando la lógica de predicados. Al igual que cualquier clase en la teoría de conjuntos, un conjunto puede interpretarse como correspondiente a predicados sobre conjuntos. Por ejemplo, un número entero es par si pertenece al conjunto de los números enteros pares, o un número natural tiene sucesor si pertenece al conjunto de los números naturales que tienen sucesor. Para un ejemplo menos primitivo, fijemos algún conjunto.${\displaystyle y}$y dejar${\displaystyle Q(n)}$denota la afirmación existencial de que el espacio de funciones en el ordinal finito en${\displaystyle y}$existen. El predicado se denotará${\displaystyle \exists h.h\simeq y^{\{0,1,\dots ,n-1\}}}$Más abajo, y aquí el cuantificador existencial no es simplemente uno sobre los números naturales, ni está acotado por ningún otro conjunto. Ahora bien, una proposición como el principio de exponenciación finita${\displaystyle \forall (n\in \omega ).Q(n)}$y, de manera menos formal, la igualdad${\displaystyle \omega =\{n\in \omega \mid Q(n)\}}$son solo dos maneras de formular la misma declaración deseada, a saber, una${\displaystyle n}$-conjunción indexada de proposiciones existenciales donde${\displaystyle n}$abarca el conjunto de todos los naturales. Mediante la identificación extensional, la segunda forma expresa la afirmación utilizando la notación para la comprensión de subclases y el objeto entre corchetes del lado derecho puede incluso no constituir un conjunto. Si esa subclase no es demostrablemente un conjunto, en realidad no puede utilizarse en muchos principios de la teoría de conjuntos en las demostraciones, y establecer el cierre universal${\displaystyle \forall (n\in \omega ).Q(n)}$como un teorema puede no ser posible. La teoría de conjuntos puede reforzarse mediante más axiomas de existencia de conjuntos, para ser utilizados con la Separación acotada predicativa , pero también simplemente postulando axiomas más fuertes.${\displaystyle \forall }$-declaraciones.

El segundo conjuntivo cuantificado universalmente en el axioma fuerte del infinito expresa la inducción matemática para todo${\displaystyle y}$en el universo del discurso, es decir, para conjuntos. Esto se debe a que el consecuente de esta cláusula,${\displaystyle \omega \subset y}$, afirma que todos${\displaystyle n\in \omega }$cumplir el predicado asociado. Ser capaz de utilizar la separación predicativa para definir subconjuntos de${\displaystyle \omega }$La teoría demuestra la inducción para todos los predicados.${\displaystyle \phi (n)}$involucrando únicamente 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 los axiomas de espacio de funciones y de colección que serán el foco del resto del artículo. En particular,${\displaystyle {\mathsf {ECST}}}$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.${\displaystyle {\mathsf {HA}}}$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 acotada válido en${\displaystyle {\mathsf {ECST}}}$. El principio de inducción anterior podría adoptarse directamente, reflejando más de cerca la aritmética de segundo orden. En teoría de conjuntos también se deduce de la Separación completa (es decir, no acotada), que dice que todos los predicados en${\displaystyle \forall }$son conjuntos. La inducción matemática también es reemplazada por el axioma de inducción de conjuntos (completo).

Nota de advertencia: Al nombrar enunciados de inducción, se debe tener cuidado de no confundir 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 números justos. Por lo tanto, para interpretar el esquema axiomático de${\displaystyle {\mathsf {HA}}}$, uno interpreta 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 tipos de la llamada aritmética de segundo orden.${\displaystyle {\mathsf {Z}}_{2}}$, en una forma expresada explícitamente para subconjuntos de los naturales. Esa clase de subconjuntos puede considerarse que corresponde a una colección de fórmulas más rica que las definibles de 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. Subsistemas de${\displaystyle {\mathsf {Z}}_{2}}$Con una comprensión de complejidad muy baja , estudiada en ese marco, se tiene un lenguaje que no se limita a expresar conjuntos aritméticos , mientras que todos los conjuntos de números naturales que tales teorías demuestran que existen son simplemente conjuntos computables . Los teoremas allí presentes pueden ser un punto de referencia relevante para teorías de conjuntos débiles con un conjunto de números naturales, separación predicativa y solo alguna forma restringida adicional de inducción. La matemática inversa constructiva existe como campo, pero está menos desarrollada que su contraparte clásica. ^{[ 16 ]}${\displaystyle {\mathsf {Z}}_{2}}$Además, no debe confundirse con la formulación de segundo orden de la aritmética de Peano.${\displaystyle {\mathsf {PA}}_{2}}$. Typical set theories like the one discussed here are also first-order, but those theories are not arithmetics and so formulas may also quantify over the subsets of the naturals. When discussing the strength of axioms concerning numbers, it is also important to keep in mind that the arithmetical and the set theoretical framework do not share a common signature. Likewise, care must always be taken with insights about totality of functions. In computability theory, the μ operator enables all partial general recursive functions (or programs, in the sense that they are Turing computable), including ones e.g. non-primitive recursive but ${\displaystyle {\mathsf {PA}}}$-total, such as the Ackermann function. The definition of the operator involves predicates over the naturals and so the theoretical analysis of functions and their totality depends on the formal framework and proof calculus at hand.