Teoría de conjuntos constructivos

Axiomatic set theories based on the principles of mathematical constructivism

La teoría de conjuntos constructivos axiomáticos es un enfoque del constructivismo matemático que sigue el programa de la teoría de conjuntos axiomáticos . Se suele utilizar el mismo lenguaje de primer orden con " " y " " de la teoría de conjuntos clásica, 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 los órdenes totales, como el de todos los números ordinales , expresado 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 todos como definibles por orden , 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 demuestra el teorema de buen orden , lo que implica que existen buenos ordenamientos para cualquier conjunto. En particular, esto significa que existen relaciones formalmente que establecen el buen orden 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 orden 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 correspondientes reformulaciones. Se destaca 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 deduzca 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 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 cuantificadores , 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 cualesquiera dos conjuntos 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 conjuntos 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 que acabamos de enunciar 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 se toma como predicado , 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 pura 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. De este modo, la teoría de conjuntos puede 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 desprende 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 aritméticas 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 que tales teorías demuestran existir son solo conjuntos computables . Los teoremas allí 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 debe confundirse 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 sobre 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 tal 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 que 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 que se analizan 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 contable también, 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, 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.}$

Consideremos ahora el caso . Si , digamos, entonces el rango de es un conjunto habitado, contado, por Reemplazo. Sin embargo, no es necesario que sea 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 se pueden 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

Si hay un predicado que distingue dos términos y en el sentido de que , entonces el principio de identidad de indiscernibles implica que los dos no coinciden. Esta noción puede expresarse en teoría de conjuntos: pueden considerarse separados si existe un subconjunto tal que uno es miembro y el otro no. Restringido a subconjuntos separables, esto puede formularse de manera concisa mediante cuantificación sobre funciones . De hecho, ya se rechaza una vez que se establece que no todas las funciones respetan . En ese espíritu, se puede definir en cualquier conjunto la relación de separación lógicamente positiva ${\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 2^{A}}$ ${\displaystyle x=y}$ ${\displaystyle f}$ ${\displaystyle f(x)=f(y)}$ ${\displaystyle A}$

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

Como los naturales son discretos, lo anterior se manifiesta aquí en el teorema

${\displaystyle \neg \neg (x\,\#_{A}\,y)\to \neg (x=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 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 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 esos casos parecen benignos donde, 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 }$- ${\displaystyle \mathrm {AC} }$: A family of sets is better controllable if it comes indexed by a function. A set ${\displaystyle b}$ is a base if all indexed families of sets ${\displaystyle i_{s}\colon b\to s}$ over it, have a choice function ${\displaystyle f_{s}}$, i.e. ${\displaystyle \forall (x\in b).f_{s}(x)\in i_{s}(x)}$. A collection of sets holding ${\displaystyle \omega }$ and its elements and which is closed by taking indexed sums and products (see dependent type) is called ${\displaystyle \Pi \Sigma }$-closed. While the axiom that all sets in the smallest ${\displaystyle \Pi \Sigma }$-closed class are a base does need some work to formulate, it is the strongest choice principle over ${\displaystyle {\mathsf {CZF}}}$ that holds in the type theoretical interpretation ${\displaystyle {\mathsf {ML_{1}V}}}$.
• Axiom of choice ${\displaystyle {\mathrm {AC} }}$: This is the "full" choice function postulate concerning domains that are general sets ${\displaystyle \{z,\dots \}}$ containing inhabited sets, with the codomain given as their general union. Given a collection of sets such that the logic allows to make a choice in each, the axiom grants that there exists a set function that jointly captures a choice in all. It is typically formulated for all sets but has also been studied in classical formulations for sets only up to any particular cardinality. A standard example is choice in all inhabited subsets of the reals, which classically equals the domain ${\displaystyle {\mathcal {P}}_{\mathbb {R} }\setminus 1}$. For this collection there can be no uniform element selection prescription that provably constitutes a choice function on the base of ${\displaystyle {\mathsf {ZF}}}$. Also, when restricted to the Borel algebra of the reals, ${\displaystyle {\mathsf {ZF}}}$ alone does not prove the existence of a function selecting a member from each non-empty such Lebesgue-measurable subset. (The set ${\displaystyle {\mathcal {B}}({\mathbb {R} })}$ is the σ-algebra generated by the intervals ${\displaystyle I:=\{(x,y\,]\mid x,y\in {\mathbb {R} }\}}$. It strictly includes those intervals, in the sense of ${\displaystyle I\subsetneq {\mathcal {B}}({\mathbb {R} })\subsetneq {\mathcal {P}}_{\mathbb {R} }}$, but in ${\displaystyle {\mathsf {ZF}}}$ also only has the cardinality of the reals itself.) Striking existence claims implied by the axiom are abound. ${\displaystyle {\mathsf {ECST}}}$ proves ${\displaystyle \omega }$ exists and then the axiom of choice also implies dependent choice. Critically in the present context, it moreover also implies instances of ${\displaystyle {\mathrm {PEM} }}$ via Diaconescu's theorem. For ${\displaystyle {\mathsf {ECST}}}$ or theories extending it, this means full choice at the very least proves ${\displaystyle {\mathrm {PEM} }}$ for all ${\displaystyle \Delta _{0}}$-formulas, a non-constructive consequence not acceptable, for example, from a computability standpoint. Note that constructively, Zorn's lemma does not imply choice: When membership in function domains fails to be decidable, the extremal function granted by that principle is not provably always a choice function on the whole domain.

Diaconescu's theorem

To highlight the strength of full Choice and its relation to matters of intentionality, one should consider the classes

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

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

from the proof of Diaconescu's theorem. They are as contingent as the proposition ${\displaystyle P}$ involved in their definition and they are not proven finite. Nonetheless, the setup entails several consequences. Referring back to the introductory elaboration on the meaning of such convenient class notation, as well as to the principle of distributivity, ${\displaystyle t\in a\leftrightarrow {\big (}t=0\lor (t=1\land P){\big )}}$. So unconditionally, ${\displaystyle 0\in a}$ as well as ${\displaystyle 1\in b}$, and in particular they are inhabited. As ${\displaystyle \neg (0=1)}$ in any model of Heyting arithmetic, using the disjunctive syllogism both ${\displaystyle 0\in b}$ and ${\displaystyle 1\in a}$ each imply ${\displaystyle P}$. The two statements are indeed equivalent to the proposition, as clearly ${\displaystyle P\to (a=\{0,1\}\land b=\{0,1\})}$. The latter also says that validity of ${\displaystyle P}$ means ${\displaystyle a}$ and ${\displaystyle b}$ share all members, and there are two of these. As ${\displaystyle a}$ are ${\displaystyle b}$ are then sets, also ${\displaystyle P\to (a=b\land \{a,b\}=\{a\})}$ by extensionality. Conversely, assuming they are equal means ${\displaystyle x\in a\leftrightarrow x\in b}$ for any ${\displaystyle x}$, validating all membership statements. So both the membership statements as well as the equalities are found to be equivalent to ${\displaystyle P}$. Using the contrapositive results in the weaker equivalence of disjuncts ${\displaystyle (P\lor \neg P)\leftrightarrow (a=b\lor \neg (a=b))}$. Of course, explicitly ${\displaystyle \neg P\to (a=\{0\}\land b=\{1\})}$ and so one actually finds in which way the sets can end up being different. As functions preserves equality by definition, ${\displaystyle \neg {\big (}g(a)=g(b){\big )}\to \neg P}$ indeed holds for any ${\displaystyle g}$ with domain ${\displaystyle \{a,b\}}$.

In the following assume a context in which ${\displaystyle a,b}$ are indeed established to be sets, and thus subfinite sets. The general axiom of choice claims existence of a function ${\displaystyle f\colon \{a,b\}\to a\cup b}$ with ${\displaystyle f(z)\in z}$. It is important that the elements ${\displaystyle a,b}$ of the function's domain are different than the natural numbers ${\displaystyle 0,1}$ in the sense that a priori less is known about the former. When forming then union of the two classes, ${\displaystyle u=0\lor u=1}$ is a necessary but then also sufficient condition. Thus ${\displaystyle a\cup b=\{0,1\}}$ and one is dealing with functions ${\displaystyle f}$ into a set of two distinguishable values. With choice come the conjunction ${\displaystyle f(a)\in a\land f(b)\in b}$ in the codomain of the function, but the possible function return values are known to be just ${\displaystyle 0}$ or ${\displaystyle 1}$. Using the distributivity, there arises a list of conditions, another disjunction. Expanding what is then established, one finds that either both ${\displaystyle P}$ as well as the sets equality holds, or that the return values are different and ${\displaystyle P}$ can be rejected. The conclusion is that the choice postulate actually implies ${\displaystyle P\lor \neg P}$ whenever a Separation axiom allows for set comprehension using undecidable proposition ${\displaystyle P}$.

Analysis of Diaconescu's theorem

So full choice is non-constructive in set theory as defined here. The issue is that when propositions are part of set comprehension (like when ${\displaystyle P}$ is used to separate, and thereby define, the classes ${\displaystyle a}$ and ${\displaystyle b}$ from ${\displaystyle \{0,1\}}$), the notion of their truth values are ramified into set terms of the theory. Equality defined by the set theoretical axiom of extensionality, which itself is not related to functions, in turn couples knowledge about the proposition to information about function values. To recapitulate the final step in terms function values: On the one hand, witnessing ${\displaystyle f(a)=1}$ implies ${\displaystyle P}$ and ${\displaystyle a=b}$ and this conclusion independently also applies to witnessing ${\displaystyle f(b)=0}$. On the other hand, witnessing ${\displaystyle f(a)=0\land f(b)=1}$ implies the two function arguments are not equal and this rules out ${\displaystyle P}$. There are really only three combinations, as the axiom of extensionality in the given setup makes ${\displaystyle f(a)=1\land f(b)=0}$ inconsistent. So if the constructive reading of existence is to be preserved, full choice may be not adopted in the set theory, because the mere claim of function existence does not realize a particular function.

To better understand why one cannot expect to be granted a definitive (total) choice function with domain ${\displaystyle \{a,b\}}$, consider naive function candidates. Firstly, an analysis of the domain is in order. The surjection ${\displaystyle \{\langle 0,a\rangle ,\langle 1,b\rangle \}}$ witnesses that ${\displaystyle \{a,b\}}$ is finitely indexed. It was noted that its members are subfinite and also inhabited, since regardless of ${\displaystyle P}$ it is the case that ${\displaystyle 0\in a}$ and ${\displaystyle 1\in b}$. So naively, this would seem to make ${\displaystyle f=\{\langle a,0\rangle ,\langle b,1\rangle \}}$ a contender for a choice function. When ${\displaystyle P}$ can be rejected, then this is indeed the only option. But in the case of provability of ${\displaystyle P}$, when ${\displaystyle \{a,b\}=\{a\}}$, there is extensionally only one possible function input to a choice function. So in that situation, a choice function would explicitly have type ${\displaystyle f\colon \{a\}\to \{0,1\}}$, for example ${\displaystyle f=\{\langle a,0\rangle \}}$ and this would rule out the initial contender. For general ${\displaystyle P}$, the domain of a would-be choice function is not concrete but contingent on ${\displaystyle P}$ and not proven finite. When considering the above functional assignment ${\displaystyle f(a)=0}$, then neither unconditionally declaring ${\displaystyle f(b)=1}$ nor ${\displaystyle f(b)=0}$ is necessarily consistent. Having identified ${\displaystyle 1}$ with ${\displaystyle \{0\}}$, the two candidates described above can be represented simultaneously via ${\displaystyle f=\{\langle a,0\rangle ,\langle b,B_{\neg }\rangle \}}$ (which is not proven finite either) with the subfinite "truth value of ${\displaystyle \neg P}$" given as ${\displaystyle B_{\neg }:=\{u\in \{0\}\mid \neg P\}}$. As ${\displaystyle (P\to (B_{\neg }=0))\land (\neg P\to (B_{\neg }=1))}$, postulating ${\displaystyle P}$, or ${\displaystyle \neg P}$, or the classical principle ${\displaystyle P\lor \neg P}$ here would indeed imply that ${\displaystyle B_{\neg }}$ is a natural, so that the latter set ${\displaystyle f}$ constitutes a choice function into ${\displaystyle \{0,1\}}$. And as in the constructive case, given a particular choice function - a set holding either exactly one or exactly two pairs - one could actually infer whether ${\displaystyle P}$ or whether ${\displaystyle \neg P}$ does hold. Vice versa, the third and last candidate ${\displaystyle f=\{\langle b,1\rangle \}}$ can be captured as part of ${\displaystyle f=\{\langle a,B\rangle ,\langle b,1\rangle \}}$, where ${\displaystyle B:=\{u\in \{0\}\mid P\}}$. Such a ${\displaystyle B}$ had already been considered in the early section on the axiom of separation. Again, the latter ${\displaystyle f}$ here is a classical choice function either way also, where ${\displaystyle P}$ functions as a (potentially undecidable) "if-clause". Constructively, the domain and values of such ${\displaystyle P}$-dependent would-be functions are not understood enough to prove them to be a total functional relation into ${\displaystyle \{0,1\}}$.

For computable semantics, set theory axioms postulating (total) function existence lead to the requirement for halting recursive functions. From their function graph in individual interpretations, one can infer the branches taken by the "if-clauses" that were undecided in the interpreted theory. But on the level of the synthetic frameworks, when they broadly become classical from adopting full choice, these extensional set theories theories contradict the constructive Church's rule.

Regularity implies PEM

The axiom of choice grants existence a function associated with every set-sized collection of inhabited elements ${\displaystyle s}$, with which one can then at once pick unique elements ${\displaystyle t}$. The axiom of regularity states that for every inhabited set ${\displaystyle s}$ in the universal collection, there exists an element ${\displaystyle t}$ in ${\displaystyle s}$, which shares no elements with ${\displaystyle s}$. This formulation does not involve functions or unique existence claims, but instead directly guarantees sets ${\displaystyle t\in s}$ with a specific property. As the axiom correlates membership claims at different rank, the axiom also ends up implying ${\displaystyle {\mathrm {PEM} }}$:

The proof from Choice above had used ${\displaystyle 1:=\{0\}}$ and a particular set ${\displaystyle \{a,b\}}$. The proof in this paragraph also assumes Separation applies to ${\displaystyle P}$ and uses ${\displaystyle b}$, for which ${\displaystyle \{0\}\in b}$ by definition. It was already explained that ${\displaystyle P\leftrightarrow 0\in b}$ and so one may prove excluded middle for ${\displaystyle P}$ in the form ${\displaystyle 0\in b\lor 0\notin b}$. Now let ${\displaystyle t\in b}$ be the postulated member with the empty intersection property. The set ${\displaystyle b}$ was defined as a subset of ${\displaystyle \{0,1\}}$ and so any given ${\displaystyle t\in b}$ fulfills the disjunction ${\displaystyle t=0\lor t=1}$. The left clause ${\displaystyle t=0}$ implies ${\displaystyle 0\in b}$, while for the right clause ${\displaystyle t=1}$ one may use that the special non-intersecting element ${\displaystyle t}$ fulfills ${\displaystyle (t=\{0\})\leftrightarrow (0\notin b)}$.

Demanding that the set of naturals is well-ordered with respect to it standard order relation imposes the same condition on the inhabited set ${\displaystyle b\subset \omega }$. So the least number principle has the same non-constructive implication. As with the proof from Choice, the scope of propositions for which these results hold is governed by one's Separation axiom.

Arithmetic

The four Peano axioms for ${\displaystyle 0}$ and ${\displaystyle S}$, characterizing the set ${\displaystyle \omega }$ as a model of the natural numbers in the constructive set theory ${\displaystyle {\mathsf {ECST}}}$, have been discussed. The order " ${\displaystyle <}$" of natural numbers is captured by membership " ${\displaystyle \in }$" in this von Neumann model and this set is discrete, i.e. also ${\displaystyle \phi (n,m):=(n=m)}$ is decidable.

As discussed, induction for arithmetic formulas is a theorem. However, when not assuming full mathematical induction (or stronger axioms like full Separation) in a set theory, there is a pitfall regarding the existence of arithmetic operations. The first-order theory of Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$ has the same signature and non-logical axioms as Peano arithmetic ${\displaystyle {\mathsf {PA}}}$. In contrast, the signature of set theory does not contain addition " ${\displaystyle +}$" or multiplication " ${\displaystyle \times }$". ${\displaystyle {\mathsf {ECST}}}$ does actually not enable primitive recursion in ${\displaystyle \omega }$ for function definitions of what would be ${\displaystyle h\colon (x\times \omega )\to y}$ (where " ${\displaystyle \times }$" here denotes the Cartesian product of set, not to be confused with multiplication above). Indeed, despite having the Replacement axiom, the theory does not prove there to be a set capturing the addition function ${\displaystyle +\colon (\omega \times \omega )\to \omega }$. In the next section, it is clarified which set theoretical axiom may be asserted to prove existence of the latter as a function set, together with their desired relation to zero and successor.

Far beyond just the equality predicate, the obtained model of arithmetic then validates

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

for any quantifier-free formula. Indeed, ${\displaystyle {\mathsf {PA}}}$ is ${\displaystyle \Pi _{2}^{0}}$-conservative over ${\displaystyle {\mathsf {HA}}}$ and double-negation elimination is possible for any Harrop formula.

Arithmetic functions from recursion

Going a step beyond ${\displaystyle {\mathsf {ECST}}}$, the axiom granting definition of set functions via iteration-step set functions must be added: For any set ${\displaystyle y}$, set ${\displaystyle z\in y}$ and ${\displaystyle f\colon y\to y}$, there must also exist a function ${\displaystyle g\colon \omega \to y}$ attained by making use of the former, namely such that ${\displaystyle g(0)=z}$ and ${\displaystyle g(Sn)=f(g(n))}$. This iteration- or recursion principle is akin to the transfinite recursion theorem, except it is restricted to set functions and finite ordinal arguments, i.e. there is no clause about limit ordinals. It functions as the set theoretical equivalent of a natural numbers object in category theory. This then enables a full interpretation of Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$ in our set theory, including addition and multiplication functions.

With this, ${\displaystyle {\mathbb {N} }}$ and ${\displaystyle {\mathbb {Z} }}$ are well-founded, in the sense of the inductive subsets formulation. Further, arithmetic of rational numbers ${\displaystyle {\mathbb {Q} }}$ can then also be defined and its properties, like uniqueness and countability, be proven.

Recursion from set theory axioms

Recall that ${\displaystyle h\simeq y^{x}}$ is short for ${\displaystyle \forall f.{\big (}f\in h\leftrightarrow f\in y^{x}{\big )}}$, where ${\displaystyle f\in y^{x}}$ is short for the total function predicate, a proposition in terms of uses bounded quantifiers. If both sides are sets, then by extensionality this is also equivalent to ${\displaystyle h=y^{x}}$. (Although by slight abuse of formal notation, as with the symbol " ${\displaystyle \in }$", the symbol " ${\displaystyle =}$" is also commonly used with classes anyhow.)

A set theory with the ${\displaystyle {\mathsf {HA}}}$-model enabling recursion principle, spelled out above, will also prove that, for all naturals ${\displaystyle n}$ and ${\displaystyle m}$, the function spaces

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

are sets. Indeed, bounded recursion suffices, i.e. the principle for ${\displaystyle \Delta _{0}}$-defined classes.

Conversely, the recursion principle can be proven from a definition involving the union of recursive functions on finite domains. Relevant for this is the class of partial functions on ${\displaystyle \omega }$ such that all of its members have a return values only up to some natural number bound, which may be expressed by ${\displaystyle \cup _{n\in \omega }y^{\{0,1,\dots ,n-1\}}}$. Existence of this as a set becomes provable assuming that the individual function spaces ${\displaystyle y^{n}}$ all form sets themselves. To this end

With this axiom, any such space is now a set of subsets of ${\displaystyle n\times y}$ and this is strictly weaker than full Separation. Notably, adoption of this principle has genuine set theoretical flavor, in contrast to a direct embedding of arithmetic principles into our theory. And it is a modest principle insofar as these function spaces are tame: When instead assuming full induction or full exponentiation, taking ${\displaystyle y}$ to function spaces ${\displaystyle y^{n}}$, or to n-fold Cartesian products, provably does preserve countability.

In ${\displaystyle {\mathsf {ECTS}}}$ plus finite exponentiation, the recursion principle is a theorem. Moreover, enumerable forms of the pigeon hole principle can now also be proven, e.g. that on a finitely indexed set, every auto-injection is also a surjection. As a consequence, the cardinality of finite sets, i.e. the finite von Neumann ordinal, is provably unique. The finitely indexed discrete sets are just the finite sets. In particular, finitely indexed subsets of ${\displaystyle \omega }$ are finite. Taking quotients or taking the binary union or Cartesian product of two sets preserve finiteness, sub-finiteness and being finitely indexed.

The set theory axioms listed so far incorporates first-order arithemtic and suffices as formalized framework for a good portion of common mathematics. The restriction to finite domains is lifted in the strictly stronger exponentiation axiom below. However, also that axiom does not entail the full induction schema for formulas with unbound quantifiers over the domain of sets, nor a dependent choice principle. Likewise, there are Collection principles that are constructively not implied by Replacement, as discussed further below. A consequence of this is that for some statements of higher complexity or indirection, even if concrete instances of interest may well be provable, the theory may not prove the universal closure. Stronger than this theory with finite exponentiation is ${\displaystyle {\mathsf {ECTS}}}$ plus full induction. It implies the recursion principle even for classes and such that ${\displaystyle g}$ is unique. Already that recursion principle when restricted to ${\displaystyle \Delta _{0}}$ does prove finite exponentiation, and also the existence of a transitive closure for every set with respect to ${\displaystyle \in }$ (since union formation is ${\displaystyle \Delta _{0}}$). With it more common constructions preserve countability. General unions over a finitely indexed set of finitely indexed sets are again finitely indexed, when at least assuming induction for ${\displaystyle \Sigma _{1}}$-predicates (with respect to the set theory language, and this then holds regardless of the decidability of their equality relations.)

Induction without infinite sets

Before discussing even classically uncountable sets, this last section takes a step back to a context more akin to ${\displaystyle {\mathsf {BCST}}}$. The addition of numbers, considered as relation on triples, is an infinite collection, just like collection of natural numbers themselves. But note that induction schemas may be adopted (for sets, ordinals or in conjunction with a natural number sort), without ever postulating that the collection of naturals exists as a set. As noted, Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$ is bi-interpretable with such a constructive set theory, in which all sets are postulated to be in bijection with an ordinal. The BIT predicate is a common means to encode sets in arithmetic.

This paragraph lists a few weak natural number induction principles studied in the proof theory of arithmetic theories with addition and multiplication in their signature. This is the framework where these principles are most well understood. The theories may be defined via bounded formulations or variations on induction schemas that may furthermore only allow for predicates of restricted complexity. On the classical first-order side, this leads to theories between the Robinson arithmetic ${\displaystyle {\mathsf {Q}}}$ and Peano arithmetic ${\displaystyle {\mathsf {PA}}}$: The theory ${\displaystyle {\mathsf {Q}}}$ does not have any induction. ${\displaystyle {\mathsf {PA}}}$ has full mathematical induction for arithmetical formulas and has ordinal ${\displaystyle \varepsilon _{0}}$, meaning the theory lets one encode ordinals of weaker theories as recursive relation on just the naturals. Theories may also include additional symbols for particular functions. Many of the well studied arithmetic theories are weak regarding proof of totality for some more fast growing functions. Some of the most basic examples of arithmetics include elementary function arithmetic ${\displaystyle {\mathsf {EFA}}}$, which includes induction for just bounded arithmetical formulas, here meaning with quantifiers over finite number ranges. The theory has a proof theoretic ordinal (the least not provenly recursive well-ordering) of ${\displaystyle \omega ^{3}}$. The ${\displaystyle \Sigma _{1}^{0}}$-induction schema for arithmetical existential formulas allows for induction for those properties of naturals a validation of which is computable via a finite search with unbound (any, but finite) runtime. The schema is also classically equivalent to the ${\displaystyle \Pi _{1}^{0}}$-induction schema. The relatively weak classical first-order arithmetic which adopts that schema is denoted ${\displaystyle {\mathsf {I\Sigma }}_{1}}$ and proves the primitive recursive functions total. The theory ${\displaystyle {\mathsf {I\Sigma }}_{1}}$ is ${\displaystyle \Pi _{2}^{0}}$-conservative over primitive recursive arithmetic ${\displaystyle {\mathsf {PRA}}}$. Note that the ${\displaystyle \Sigma _{1}^{0}}$-induction is also part of the second-order reverse mathematics base system ${\displaystyle {\mathsf {RCA}}_{0}}$, its other axioms being ${\displaystyle {\mathsf {Q}}}$ plus ${\displaystyle \Delta _{1}^{0}}$-comprehension of subsets of naturals. The theory ${\displaystyle {\mathsf {RCA}}_{0}}$ is ${\displaystyle \Pi _{1}^{1}}$-conservative over ${\displaystyle {\mathsf {I\Sigma }}_{1}}$. Those last mentioned arithmetic theories all have ordinal ${\displaystyle \omega ^{\omega }}$.

Let us mention one more step beyond the ${\displaystyle \Sigma _{1}^{0}}$-induction schema. Lack of stronger induction schemas means, for example, that some unbounded versions of the pigeon hole principle are unprovable. One relatively weak one being the Ramsey theorem type claim here expressed as follows: For any ${\displaystyle m>0}$ and coding of a coloring map ${\displaystyle f}$, associating each ${\displaystyle n\in \omega }$ with a color ${\displaystyle \{0,1,\dots ,m-1\}}$, it is not the case that for every color ${\displaystyle c<m}$ there exists a threshold input number ${\displaystyle n_{c}}$ beyond which ${\displaystyle c}$ is not ever the mappings return value anymore. (In the classical context and in terms of sets, this claim about coloring may be phrased positively, as saying that there always exists at least one return value ${\displaystyle k}$ such that, in effect, for some unbounded domain ${\displaystyle K\subset \omega }$ it holds that ${\displaystyle \forall (n\in K).f(n)=k}$. In words, when ${\displaystyle f}$ provides infinite enumerated assignments, each being of one of ${\displaystyle m}$ different possible colors, it is claimed that a particular ${\displaystyle k}$ coloring infinitely many numbers always exists and that the set can thus be specified, without even having to inspect properties of ${\displaystyle f}$. When read constructively, one would want ${\displaystyle k}$ to be concretely specifiable and so that formulation is a stronger claim.) Higher indirection, than in induction for mere existential statements, is needed to formally reformulate such a negation (the Ramsey theorem type claim in the original formulation above) and prove it. Namely to restate the problem in terms of the negation of the existence of one joint threshold number, depending on all the hypothetical ${\displaystyle n_{c}}$'s, beyond which the function would still have to attain some color value. More specifically, the strength of the required bounding principle is strictly between the induction schema in ${\displaystyle {\mathsf {I\Sigma }}_{1}^{0}}$ and ${\displaystyle {\mathsf {I\Sigma }}_{2}^{0}}$. For properties in terms of return values of functions on finite domains, brute force verification through checking all possible inputs has computational overhead which is larger for larger domains, but always finite. Acceptance of an induction schema as in ${\displaystyle {\mathsf {I\Sigma }}_{2}^{0}}$ validates the former so called infinite pigeon hole principle, which concerns unbounded domains, and so is about mappings with infinitely many inputs.

It is worth noting that in the program of predicative arithmetic, even the mathematical induction schema has been criticized as possibly being impredicative, when natural numbers are defined as the object which fulfill this schema, which itself is defined in terms of all naturals.

Exponentiation

Classical ${\displaystyle {\mathsf {ZFC}}}$ without the Powerset axiom has natural models in classes of sets of hereditary size less than certain uncountable cardinals.^[21] In particular, it is still consistent with all existing sets (including sets holding reals) being subcountable, and there even countable. Such a theory essentially amounts to second-order arithmetic. All sets being subcountable can constructively be consistent even in the present of uncountable sets, as introduced now.

Possible choice principles were discussed, a weakened form of the Separation schema was already adopted, and more of the standard ${\displaystyle {\mathsf {ZFC}}}$ axioms shall be weakened for a more predicative and constructive theory. The first one of those is the Powerset axiom, which is adopted in the form of the space of characteristic functions. The following axiom ${\displaystyle {\mathrm {Exp} }}$ is strictly stronger than its pendant for finite domains discussed above:

The formulation here again uses the convenient notation for function spaces, as discussed above. In words, the axiom says that given two sets ${\displaystyle x,y}$, the class ${\displaystyle y^{x}}$ of all functions is, in fact, also a set. This is certainly required, for example, to formalize the object map of an internal hom-functor like ${\displaystyle {\mathrm {hom} }({\mathbb {N} },-).}$

Adopting such an existence statement also the quantification ${\displaystyle \forall f}$ over the elements of certain classes of (total) functions now only range over sets. Consider the collection of pairs ${\displaystyle \langle a,b\rangle \in x\times x}$ validating the apartness relation ${\displaystyle \exists (f\in {\mathbb {N} }^{x}).f(a)\neq f(b)}$. Via bounded Separation, this now constitutes a subset of ${\displaystyle x\times x}$. This examples shows that the Exponentiation axiom not only enriches the domain of sets directly, but via separation also enables the derivation of yet more sets, and this then furthermore also strengthens other axioms.

Notably, these bounded quantifiers now range over function spaces that are provably uncountable, and hence even classically uncountable. E.g. the collection of all functions ${\displaystyle f\colon \omega \to 2}$ where ${\displaystyle 2:=SS0=\{0,1\}}$, i.e. the set ${\displaystyle 2^{\mathbb {N} }}$ of points underlying the Cantor space, is uncountable, by Cantor's diagonal argument, and can at best be taken to be a subcountable set. In this theory one may now also quantify over subspaces of spaces like ${\displaystyle 2^{\mathbb {N} }}$, which is a third order notion on the naturals. (In this section and beyond, the symbol for the semiring of natural numbers in expressions like ${\displaystyle y^{\mathbb {N} }}$ is used, or written ${\displaystyle \omega \to y}$, just to avoid conflation of cardinal- with ordinal exponentiation.) Roughly, classically uncountable sets, like for example these function spaces, tend to not have computably decidable equality.

By taking the general union over an ${\displaystyle x}$-indexed family ${\displaystyle \{y_{i}\}_{i}}$, also the dependent or indexed product, written ${\displaystyle \Pi _{i\in x}\,y_{i}}$, is now a set. For constant ${\displaystyle y_{i}}$, this again reduces to the function space ${\displaystyle y^{x}}$. And taking the general union over function spaces themselves, whenever the powerclass of ${\displaystyle x}$ is a set, then also the superset ${\displaystyle \cup _{s\subset x}y^{s}}$ of ${\displaystyle y^{x}}$ is now a set - giving a means to talk about the space of partial functions on ${\displaystyle x}$.

Unions and countability

With Exponentiation, the theory proves the existence of any primitive recursive function in ${\displaystyle x\times \omega \to y}$, and in particular in the uncountable function spaces out of ${\displaystyle \omega }$. Indeed, with function spaces and the finite von Neumann ordinals as domains, we can model ${\displaystyle {\mathsf {HA}}}$ as discussed, and thus encode ordinals in the arithmetic. One then furthermore obtains the ordinal-exponentiated number ${\displaystyle \omega ^{\omega }}$ as a set, which may be characterized as ${\displaystyle \cup _{n\in \omega }\omega ^{n}}$, the counted set of words over an infinite alphabet. The union of all finite sequences over a countable set is now a countable set. Further, for any countable family of counting functions together with their ranges, the theory proves the union of those ranges to be countable. In contrast, not assuming countable choice, even ${\displaystyle {\mathsf {ZF}}}$ is consistent with the uncountable set ${\displaystyle {\mathbb {R} }}$ being the union of a countable set of countable sets.

The list here is by no means complete. Many theorems about the various function existence predicates hold, especially when assuming countable choice - which as noted is never implicitly assumed in this discussion.

At last, with Exponentiation, any finitely indexed union of a family of subfinitely indexed resp. subcountable sets is itself subfinitely indexed resp. subcountable as well. The theory also proves the collection of all the countable subsets of any set ${\displaystyle x}$ to be a set itself. Concerning this subset of the powerclass ${\displaystyle {\mathcal {P}}_{x}}$, some natural cardinality questions can also classically only be settled with Choice, at least for uncountable ${\displaystyle x}$.

The class of all subsets of a set

Given a sequence of sets, one may define new such sequences, e.g. in ${\displaystyle \langle a,b\rangle \mapsto \langle \langle \rangle ,\langle a\rangle ,\langle b\rangle ,\langle a,b\rangle \rangle }$. But notably, in a mathematical set theory framework, the collection of all subsets of a set is defined not in a bottom-up construction from its constituents but via a comprehension over all sets in the domain of discourse. The standard, standalone characterization of the powerclass of a set ${\displaystyle x}$ involves unbounded universal quantification, namely ${\displaystyle \forall u.\left(u\in {\mathcal {P}}_{x}\leftrightarrow u\subset x\right)}$, where ${\displaystyle \subset }$ was previously defined also in terms of the membership predicate ${\displaystyle \in }$. Here, a statement expressed as ${\displaystyle \forall (u\in {\mathcal {P}}_{x}).Q(x)}$ must a priori be taken for ${\displaystyle \forall u.{\big (}u\subset x\to Q(x){\big )}}$ and is not equivalent to a set-bounded proposition. Indeed, the statement ${\displaystyle y={\mathcal {P}}_{x}}$ itself is ${\displaystyle \Pi _{1}}$. If ${\displaystyle {\mathcal {P}}_{x}}$ is a set, then the defining quantification even ranges across ${\displaystyle {\mathcal {P}}_{x}}$, which makes the axiom of powerset impredicative.

Recall that a member of the set of characteristic functions ${\displaystyle 2^{x}}$ corresponds to a predicate that is decidable on a set ${\displaystyle x}$, which it thus determines a detachable subset ${\displaystyle s\subset x}$. In turn, the class ${\displaystyle {\mathcal {D}}_{x}\subset {\mathcal {P}}_{x}}$ of all detachable subsets of ${\displaystyle x}$ is now also a set, via Replacement. However, ${\displaystyle {\mathcal {D}}_{x}}$ may fail to provably have desirable properties, e.g. being closed under unending operations such as the unions over countably infinite index sets: For a countable sequence ${\displaystyle u_{n}\in {\mathcal {D}}_{x}}$, the subset ${\displaystyle U:=\cup _{k\in \omega }u_{k}}$ of ${\displaystyle x}$ validating ${\displaystyle (a\in U)\leftrightarrow \exists (m\in \omega ).a\in u_{m}}$ for all ${\displaystyle a\in x}$ does exist as a set. But it may fail to be detachable and is therefore then not necessarily provably itself a member of ${\displaystyle {\mathcal {D}}_{x}}$. Meanwhile, over classical logic, all subsets of a set ${\displaystyle x}$ are trivially detachable, meaning ${\displaystyle {\mathcal {D}}_{x}={\mathcal {P}}_{x}}$ and then ${\displaystyle {\mathcal {D}}_{x}}$ of course holds any subset. Over classical logic, this furthermore means that Exponentiation turns the power class into a set.

Translating results of set theory based mathematical theories like point-set topology or measure theory to a constructive framework is a subtle back and forth. For example, while ${\displaystyle {\mathcal {D}}_{x}}$ is a field of sets, for it to form a σ-algebra per definition also requires the above mentioned closedness under unions. But while a domain of subsets may fail to exhibit such closure property constructively, classically a measure ${\displaystyle \mu }$ is continuous from below and so its value on an infinite union can in any case also be expressed without reference to that set as function input, namely as ${\displaystyle \lim _{n\to \infty }}$ of the growing sequence ${\displaystyle \mu (\cup _{k\leq n}u_{k})}$ of the function's values at finite unions.

Apart from the class of detachable sets, also various other subclasses of any powerclass are now provenly sets. For example, the theory also proves this for the collection of all the countable subsets of any set.

The richness of the full powerclass in a theory without excluded middle can best be understood by considering small classically finite sets. For any proposition ${\displaystyle P}$, consider the subclass ${\displaystyle B:=\{x\in 1\mid P\}}$ of ${\displaystyle 1}$ (i.e. ${\displaystyle \{0\}}$ or ${\displaystyle S0}$). It equals ${\displaystyle B=0}$ when ${\displaystyle P}$ can be rejected and it equals ${\displaystyle B=1}$ (i.e. ${\displaystyle B=S0}$), when ${\displaystyle P}$ can be proven. But ${\displaystyle P}$ may also not be decidable at all. Consider three different undecidable proposition, none of which provenly imply another. They can be used to define three subclasses of the singleton ${\displaystyle 1}$, none of which are provenly the same. In this view, the powerclass ${\displaystyle {\mathcal {P}}_{1}}$ of the singleton, usually denoted by ${\displaystyle \Omega }$, is called the truth value algebra and does not necessarily provenly have only two elements.

With Exponentiation, the powerclass of the singleton, ${\displaystyle {\mathcal {P}}_{1}}$, being a set already implies Powerset for sets in general. The proof is via replacement for the association of ${\displaystyle f\in {{\mathcal {P}}_{1}}^{x}}$ to ${\displaystyle \{z\in x\mid 0\in f(z)\}\in {\mathcal {P}}_{x}}$, and an argument why all subsets are covered. The set ${\displaystyle 2^{x}}$ injects into the function space ${\displaystyle {{\mathcal {P}}_{1}}^{x}}$ also.

If the theory proves ${\displaystyle B}$ above a set (as for example ${\displaystyle {\mathsf {IZF}}}$ unconditionally does), then the subset ${\displaystyle b:=\{\langle 0,B\rangle \}}$ of ${\displaystyle 1\times {\mathcal {P}}_{1}}$ is a function ${\displaystyle b\colon 1\to {\mathcal {P}}_{1}}$ with ${\displaystyle {\big (}b(0)=1{\big )}\leftrightarrow P}$. To claim that ${\displaystyle {\mathcal {P}}_{1}=2}$ is to claim that excluded middle holds for ${\displaystyle P}$.

It has been pointed out that the empty set ${\displaystyle 0}$ and the set ${\displaystyle 1}$ itself are of course two subsets of ${\displaystyle 1}$, meaning ${\displaystyle 2\subset {\mathcal {P}}_{1}}$. Whether also ${\displaystyle {\mathcal {P}}_{1}\subset 2}$ is true in a theory is contingent on a simple disjunction:

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

So assuming ${\displaystyle {\mathrm {PEM} }}$ for just bounded formulas, predicative Separation then lets one demonstrate that the powerclass ${\displaystyle {\mathcal {P}}_{1}}$ is a set. And so in this context, also full Choice proves Powerset. (In the context of ${\displaystyle {\mathsf {IZF}}}$, bounded excluded middle in fact already turns set theory classical, as discussed further below.)

Full Separation is equivalent to just assuming that each individual subclass of ${\displaystyle 1}$ is a set. Assuming full Separation, both full Choice and Regularity prove ${\displaystyle {\mathrm {PEM} }}$.

Assuming ${\displaystyle {\mathrm {PEM} }}$ in this theory, Set induction becomes equivalent to Regularity and Replacement becomes capable of proving full Separation.

Note that cardinal relations involving uncountable sets are also elusive in ${\displaystyle {\mathsf {ZFC}}}$, where the characterization of uncountability simplifies to ${\displaystyle |\omega |<|x|}$. For example, regarding the uncountable power ${\displaystyle 2^{|\omega |}}$, it is independent of that classical theory whether all such ${\displaystyle x}$ have ${\displaystyle 2^{|\omega |}\leq |x|}$, nor does it prove that ${\displaystyle 2^{|\omega |}<2^{|x|}}$. See continuum hypothesis and the related Easton's theorem.

Category and type theoretic notions

So in this context with Exponentiation, first-order arithmetic has a model and all function spaces between sets exist. The latter are more accessible than the classes containing all subsets of a set, as is the case with exponential objects resp. subobjects in category theory. In category theoretical terms, the theory ${\displaystyle {\mathsf {BCST}}+{\mathrm {Exp} }}$ essentially corresponds to constructively well-pointed Cartesian closed Heyting pretoposes with (whenever Infinity is adopted) a natural numbers object. Existence of powerset is what would turn a Heyting pretopos into an elementary topos.^[22]Every such topos that interprets ${\displaystyle {\mathsf {ZF}}}$ is of course a model of these weaker theories, but locally Cartesian closed pretoposes have been defined that e.g. interpret theories with Exponentiation but reject full Separation and Powerset. A form of ${\displaystyle {\mathrm {PEM} }}$ corresponds to any subobject having a complement, in which case we call the topos Boolean. Diaconescu's theorem in its original topos form says that this hold iff any coequalizer of two nonintersecting monomorphisms has a section. The latter is a formulation of choice. Barr's theorem states that any topos admits a surjection from a Boolean topos onto it, relating to classical statements being provable intuitionistically.

In type theory, the expression " ${\displaystyle x\to y}$" exists on its own and denotes function spaces, a primitive notion. These types (or, in set theory, classes or sets) naturally appear, for example, as the type of the currying bijection between ${\displaystyle (z\times x)\to y}$ and ${\displaystyle z\to y^{x}}$, an adjunction. A typical type theory with general programming capability - and certainly those that can model ${\displaystyle {\mathsf {CZF}}}$, which is considered a constructive set theory - will have a type of integers and function spaces representing ${\displaystyle {\mathbb {Z} }\to {\mathbb {Z} }}$, and as such also include types that are not countable. This is just to say, or implies, that among the function terms ${\displaystyle f\colon {\mathbb {Z} }\to ({\mathbb {Z} }\to {\mathbb {Z} })}$, none have the property of being a surjection.

Constructive set theories are also studied in the context of applicative axioms.

Metalogic

While the theory ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ does not exceed the consistency strength of Heyting arithmetic, adding Excluded Middle gives a theory proving the same theorems as classical ${\displaystyle {\mathsf {ZF}}}$ minus Regularity! Thus, adding Regularity as well as either ${\displaystyle {\mathrm {PEM} }}$ or full Separation to ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ gives full classical ${\displaystyle {\mathsf {ZF}}}$. Adding full Choice and full Separation gives ${\displaystyle {\mathsf {ZFC}}}$ minus Regularity. So this would thus lead to a theory beyond the strength of typical type theory.

The presented theory does not prove a function space like ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$ to be not enumerable, in the sense of injections out of it. Without further axioms, intuitionistic mathematics has models in recursive functions but also forms of hypercomputation.

Analysis

In this section the strength of ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$ is elaborated on. For context, possible further principles are mentioned, which are not necessarily classical and also not generally considered constructive. Here a general warning is in order: When reading proposition equivalence claims in the computable context, one shall always be aware which choice, induction and comprehension principles are silently assumed. See also the related constructive analysis,^[23] feasible analysis and computable analysis.

The theory so far proves uniqueness of Archimedean, Dedekind complete (pseudo-)ordered fields, with equivalence by a unique isomorphism. The prefix "pseudo" here highlights that the order will, in any case, constructively not always be decidable. This result is relevant assuming complete such models exist as sets.

Topology

Regardless of the choice of model, the characteristic flavor of a constructive theory of numbers can be explicated using an independent proposition ${\displaystyle P}$. Consider a counter-example to the constructive provability of the well-orderedness of the naturals, but now embedded in the reals. Say

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

The infimum metric distance between some point and such a subset, what may be expressed as ${\displaystyle \rho (0,M)}$ for example, may constructively fail to provably exist. More generally, this locatedness property of subsets governs the well-developed constructive metric space theory.

Whether Cauchy or Dedekind reals, among others, also fewer statements about the arithmetic of the reals are decidable, compared to the classical theory.

Cauchy sequences

Exponentiation implies recursion principles and so in ${\displaystyle {\mathsf {ECST}}+{\mathrm {Exp} }}$, one can comfortably reason about sequences ${\displaystyle s\colon \omega \to {\mathbb {Q} }}$, their regularity properties such as ${\displaystyle |s_{n}-s_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}$, or about shrinking intervals in ${\displaystyle \omega \to ({\mathbb {Q} }\times {\mathbb {Q} })}$. So this enables speaking of Cauchy sequences and their arithmetic. This is also the approach to analysis taken in ${\displaystyle {\mathsf {Z}}_{2}}$.

Cauchy reals

Any Cauchy real number is a collection of such sequences, i.e. a subset of a set of functions on ${\displaystyle \omega }$ constructed with respect to an equivalence relation. Exponentiation together with bounded separation prove the collection of Cauchy reals to be a set, thus somewhat simplifying the logically treatment of the reals.

Even in the strong theory ${\displaystyle {\mathsf {IZF}}}$ with a strengthened form of Collection, the Cauchy reals are poorly behaved when not assuming a form of countable choice, and ${\displaystyle {\mathrm {AC} _{\omega ,2}}}$ suffices for most results. This concerns completeness of equivalence classes of such sequences, equivalence of the whole set to the Dedekind reals, existence of a modulus of convergence for all Cauchy sequences and the preservation of such a modulus when taking limits.^[24] An alternative approach that is slightly better behaved is to work a collection of Cauchy reals together a choice of modulus, i.e. not with just the real numbers but with a set of pairs, or even with a fixed modulus shared by all real numbers.

Towards the Dedekind reals

As in the classical theory, Dedekind cuts are characterized using subsets of algebraic structures such as ${\displaystyle {\mathbb {Q} }}$: The properties of being inhabited, numerically bounded above, "closed downwards" and "open upwards" are all bounded formulas with respect to the given set underlying the algebraic structure. A standard example of a cut, the first component indeed exhibiting these properties, is the representation of ${\displaystyle {\sqrt {2}}}$ given by

${\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} }}}$

(Depending on the convention for cuts, either of the two parts or neither, like here, may makes use of the sign ${\displaystyle \leq }$.)

The theory given by the axioms so far validates that a pseudo-ordered field that is also Archimedean and Dedekind complete, if it exists at all, is in this way characterized uniquely, up to isomorphism. However, the existence of just function spaces such as ${\displaystyle \{0,1\}^{\mathbb {Q} }}$ does not grant ${\displaystyle {{\mathcal {P}}_{\mathbb {Q} }}}$ to be a set, and so neither is the class of all subsets of ${\displaystyle {\mathbb {Q} }}$ that do fulfill the named properties. What is required for the class of Dedekind reals to be a set is an axiom regarding existence of a set of subsets and this is discussed further below in the section on Binary refinement. In a context without ${\displaystyle {\mathrm {PEM} }}$ or Powerset, countable choice into finite sets is assumed to prove the uncountability of the set of all Dedekind reals.

Constructive schools

Most schools for constructive analysis validate some choice and also ${\displaystyle \mathrm {BD} }$- ${\displaystyle {\mathbb {N} }}$, as defined in the second section on number bounds. Here are some other propositions employed in theories of constructive analysis that are not provable using just base intuitionistic logic:

• On the recursive mathematics side (the "Russian" or "Markovian" constructive framework with many abbreviations, e.g. ${\displaystyle {\mathsf {RUSS}}}$), first one has Markov's principle ${\displaystyle {\mathrm {MP} }}$, which is a form of proof by contradiction motivated by (unbound memory capacity) computable search. This has notable impact on statements about real numbers, as touched upon below. In this school one further even has the anti-classical constructive Church's thesis principle ${\displaystyle {\mathrm {CT} }}$, generally adopted for number-theoretic functions. Church's thesis principle expressed in the language of set theory and formulated for set functions postulates that these all correspond to computable programs that eventually halt on any argument. In computability theory, the natural numbers corresponding to indices of codes of the computable functions which are total are ${\displaystyle \Pi _{2}^{0}}$ in the arithmetical hierarchy, meaning membership of any index is affirmed by validating a ${\displaystyle \forall x\,\exists y}$ proposition. This is to say that such a collection of functions is still a mere subclass of the naturals and so is, when put in relation to some classical function spaces, conceptually small. In this sense, adopting ${\displaystyle {\mathrm {CT} }}$ postulate makes ${\displaystyle \omega \to \omega }$ into a "sparse" set, as viewed from classical set theory. Subcountability of sets can also be postulated independently.
• So on another end, on the Brouwerian intuitionist side ( ${\displaystyle {\mathsf {INT}}}$), there are bar induction, the decidable fan theorem ${\displaystyle {\mathrm {FAN} }_{\Delta }}$ saying decidable bars are uniform, which are amongst the weakest often discussed principles, Kripke's schema (with countable choice turning all subclasses of ${\displaystyle \omega }$ countable), or even Brouwer's anti-classical continuity principle, determining return values of what is established a function on unending sequences already through just finite initial segments.

Certain laws in both of those schools contradict ${\displaystyle {\mathrm {WLPO} }}$, so that choosing to adopt all principles from either school disproves theorems from classical analysis. ${\displaystyle {\mathrm {CT} }_{0}}$ is still consistent with some choice, but contradicts the classical ${\displaystyle {\mathrm {WKL} }}$ and ${\displaystyle {\mathrm {LLPO} }}$, explained below. The independence of premise rule with set existence premises is not fully understood, but as a number theoretic principle it is in conflict with the Russian school axioms in some frameworks. Notably, ${\displaystyle {\mathrm {CT} }_{0}}$ also contradicts ${\displaystyle {\mathrm {FAN} }_{\Delta }}$, meaning the constructive schools also cannot be combined in full. Some of the principles cannot be combined constructively to the extent that together they imply forms of ${\displaystyle {\mathrm {PEM} }}$ - for example ${\displaystyle {\mathrm {MP} }}$ plus the countability of all subsets of the naturals. These combinations are then naturally also not consistent with further anti-classical principles.

Indecomposability

Denote the class of all sets by ${\displaystyle {\mathcal {V}}}$. Decidability of membership in a class ${\displaystyle R}$ can be expressed as membership in ${\displaystyle R\cup ({\mathcal {V}}\setminus R)}$. We also note that, by definition, the two extremal classes ${\displaystyle {\mathcal {V}}}$ and ${\displaystyle \{\}}$ are trivially decidable. Membership in those two is equivalent to the trivial propositions ${\displaystyle x=x}$ resp. ${\displaystyle \neg (x=x)}$.

Call a class ${\displaystyle R}$ indecomposable or cohesive if, for any predicate ${\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 )}}$

This expresses that the only properties that are decidable on ${\displaystyle R}$ are the trivial properties. This is well studied in intuitionistic analysis.

The so called indecomposability schema ${\displaystyle {\mathrm {UZ} }}$ (Unzerlegbarkeit) for set theory is a possible principle which states that the whole class ${\displaystyle {\mathcal {V}}}$ is indecomposable. Extensionally speaking, ${\displaystyle {\mathrm {UZ} }}$ postulates that the two trivial classes are the only classes that are decidable with respect to the class of all sets. For a simple motivating predicate, consider membership ${\displaystyle x\in 1}$ in the first non-trivial class, which is to say the property ${\displaystyle x=\{\}}$ of being empty. This property is non-trivial to the extent that it separates some sets: The empty set is a member of ${\displaystyle 1}$, by definition, while a plethora of sets are provenly not members of ${\displaystyle 1}$. But, using Separation, one may of course also define various sets for which emptiness is not decidable in a constructive theory at all, i.e. membership in ${\displaystyle 1\cup ({\mathcal {V}}\setminus 1)}$ is not provable for all sets. So here the property of emptiness does not partition the set theoretical domain of discourse into two decidable parts. For any such non-trivial property, the contrapositive of ${\displaystyle {\mathrm {UZ} }}$ says that it cannot be decidable over all sets.

${\displaystyle {\mathrm {UZ} }}$ is implied by the uniformity principle ${\displaystyle {\mathrm {UP} }}$, which is consistent with ${\displaystyle {\mathsf {CZF}}}$ and discussed below.

Non-constructive principles

Of course ${\displaystyle {\mathrm {PEM} }}$ and many principles defining intermediate logics are non-constructive. ${\displaystyle {\mathrm {PEM} }}$ and ${\displaystyle {\mathrm {WPEM} }}$, which is ${\displaystyle {\mathrm {PEM} }}$ for just negated propositions, can be presented as De Morgan's rules. More specifically, this section shall be concerned with statements in terms of predicates - especially weaker ones, expressed in terms of a few quantifiers over sets, on top of decidable predicates on numbers. Referring back to the section on characteristic functions, one may call a collection ${\displaystyle A}$ searchable if it is searchable for all its detachable subsets, which itself corresponds to ${\displaystyle \{0,1\}^{A}}$. This is a form of ${\displaystyle \exists }$- ${\displaystyle {\mathrm {PEM} }}$ for ${\displaystyle A}$. Note that in the context of Exponentiation, such proposition on sets are now set-bound.

Particularly valuable in the study of constructive analysis are non-constructive claims commonly formulated in terms of the collection of all binary sequences and the characteristic functions ${\displaystyle f}$ on the arithmetic domain ${\displaystyle A=\omega }$ are well studied. Here ${\displaystyle f({\underline {\mathrm {n} }})=0}$ is a decidable proposition at each numeral ${\displaystyle {\mathrm {n} }}$, but, as demonstrated previously, quantified statements in terms of ${\displaystyle f}$ may not be. As is known from the incompleteness theorem and its variations, already in first-order arithmetic, example functions on ${\displaystyle {\mathbb {N} }}$ can be characterized such that if ${\displaystyle {\mathsf {PA}}}$ is consistent, the competing ${\displaystyle \exists }$- ${\displaystyle {\mathrm {PEM} }}$ disjuncts, of low complexity, are each ${\displaystyle {\mathsf {PA}}}$-unprovable (even if ${\displaystyle {\mathsf {PA}}}$ proves the disjunction of the two axiomatically.)

More generally, the arithmetic ${\displaystyle \exists }$- ${\displaystyle {\mathrm {PEM} }}$, a most prominent non-constructive, essentially logical statement goes by the name limited principle of omniscience ${\displaystyle {\mathrm {LPO} }}$. In the constructive set theory ${\displaystyle {\mathsf {CZF}}}$ introduced below, it implies ${\displaystyle {\mathrm {BD} }}$- ${\displaystyle {\mathbb {N} }}$, ${\displaystyle {\mathrm {MP} }}$, the ${\displaystyle \Pi _{1}^{0}}$-version of the fan theorem, but also ${\displaystyle {\mathrm {WKL} }}$ discussed below. Recall examples of famous sentences that can be written down in a ${\displaystyle \Pi _{1}^{0}}$-fashion, i.e. of Goldbach-type: Goldbach conjecture, Fermat's last theorem but also the Riemann hypothesis are among them. Assuming relativized dependent choice ${\displaystyle {\mathrm {RDP} }}$ and the classical ${\displaystyle {\mathrm {LPO} }}$ over ${\displaystyle {\mathsf {CZF}}}$ does not enable proofs of more ${\displaystyle \Pi _{0}^{2}}$-statements. ${\displaystyle {\mathrm {LPO} }}$ postulates a disjunctive property, as does the weaker decidability statement for functions being constant ( ${\displaystyle \Pi _{1}^{0}}$-sentences) ${\displaystyle {\mathrm {WLPO} }}$, the arithmetic ${\displaystyle \forall }$- ${\displaystyle {\mathrm {PEM} }}$. The two are related in a similar way as is ${\displaystyle {\mathrm {PEM} }}$ versus ${\displaystyle {\mathrm {WPEM} }}$ and they essentially differ by ${\displaystyle {\mathrm {MP} }}$. ${\displaystyle {\mathrm {WLPO} }}$ in turn implies the so-called "lesser" version ${\displaystyle {\mathrm {LLPO} }}$. This is the (arithmetic) ${\displaystyle \exists }$-version of the non-constructive De Morgan's rule for a negated conjunction. There are, for example, models of the strong set theory ${\displaystyle {\mathsf {IZF}}}$ which separate such statements, in the sense that they may validate ${\displaystyle {\mathrm {LLPO} }}$ but reject ${\displaystyle {\mathrm {WLPO} }}$.

Disjunctive principles about ${\displaystyle \Pi _{1}^{0}}$-sentences generally hint at equivalent formulations deciding apartness in analysis in a context with mild choice or ${\displaystyle {\mathrm {MP} }}$. The claim expressed by ${\displaystyle {\mathrm {LPO} }}$ translated to real numbers is equivalent to the claim that either equality or apartness of any two reals is decidable (it in fact decides the trichotomy). It is then also equivalent to the statement that every real is either rational or irrational - without the requirement for or construction of a witness for either disjunct. Likewise, the claim expressed by ${\displaystyle {\mathrm {LLPO} }}$ for real numbers is equivalent that the ordering ${\displaystyle \leq }$ of any two reals is decidable (dichotomy). It is then also equivalent to the statement that if the product of two reals is zero, then either of the reals is zero - again without a witness. Indeed, formulations of the three omniscience principles are then each equivalent to theorems of the apartness, equality or order of two reals in this way. Yet more can be said about the Cauchy sequences that are augmented with a modulus of convergence.

A famous source of computable undecidability - and in turn also of a broad range of undecidable propositions - is the predicate expressing a computer program to be total.

Infinite trees

Through the relation between computability and the arithmetical hierarchy, insights in this classical study are also revealing for constructive considerations. A basic insight of reverse mathematics concerns computable infinite finitely branching binary trees. Such a tree may e.g. be encoded as an infinite set of finite sets

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

with decidable membership, and those trees then provenly contain elements of arbitrary big finite size. The so called Weak Kőnig's lemma ${\displaystyle {\mathrm {WKL} }}$ states: For such ${\displaystyle T}$, there always exists an infinite path in ${\displaystyle \omega \to \{0,1\}}$, i.e. an infinite sequence such that all its initial segments are part of the tree. In reverse mathematics, the second-order arithmetic subsystem ${\displaystyle {\mathsf {RCA}}_{0}}$ does not prove ${\displaystyle {\mathrm {WKL} }}$. To understand this, note that there are computable trees ${\displaystyle K}$ for which no computable such path through it exists. To prove this, one enumerates the partial computable sequences and then diagonalizes all total computable sequences in one partial computable sequences ${\displaystyle d}$. One can then roll out a certain tree ${\displaystyle K}$, one exactly compatible with the still possible values of ${\displaystyle d}$ everywhere, which by construction is incompatible with any total computable path.

In ${\displaystyle {\mathsf {CZF}}}$, the principle ${\displaystyle {\mathrm {WKL} }}$ implies ${\displaystyle {\mathrm {LLPO} }}$ and ${\displaystyle \Pi _{1}^{0}}$- ${\displaystyle {\mathrm {AC} }_{\omega ,2}}$, a very modest form of countable choice introduced above. The former two are equivalent assuming that choice principle already in the more conservative arithmetic context. ${\displaystyle {\mathrm {WKL} }}$ is also equivalent to the Brouwer fixed point theorem and other theorems regarding values of continuous functions on the reals. The fixed point theorem in turn implies the intermediate value theorem, but always be aware that these claims may depend on the formulation, as the classical theorems about encoded reals can translate to different variants when expressed in a constructive context.^[25]

The ${\displaystyle {\mathrm {WKL} }}$, and some variants thereof, concerns infinite graphs and so its contrapositives gives a condition for finiteness. Again to connect to analysis, over the classical arithmetic theory ${\displaystyle {\mathsf {RCA}}_{0}}$, the claim of ${\displaystyle {\mathrm {WKL} }}$ is for example equivalent to the Borel compactness regarding finite subcovers of the real unit interval. ${\displaystyle {\mathrm {FAN} }_{\Delta }}$ is a closely related existence claim involving finite sequences in an infinite context. Over ${\displaystyle {\mathsf {RCA}}_{0}}$, they are actually equivalent. In ${\displaystyle {\mathsf {CZF}}}$ those are distinct, but, after again assuming some choice, here then ${\displaystyle {\mathrm {WKL} }}$ implies ${\displaystyle {\mathrm {FAN} }_{\Delta }}$.

Induction

Mathematical induction

It was observed that in set language, induction principles can read ${\displaystyle \mathrm {Ind} _{A}\to \omega \subset A}$, with the antecedent ${\displaystyle \mathrm {Ind} _{A}}$ defined as further above, and with ${\displaystyle \omega \subset A}$ meaning ${\displaystyle \forall (n\in \omega ).n\in A}$ where the set ${\displaystyle \omega }$ always denotes the standard model of natural numbers. Via the strong axiom of Infinity and predicative Separation, the validity of induction for set-bounded or ${\displaystyle \Delta _{0}}$-definitions was already established and thoroughly discussed. For those predicates involving only quantifiers over ${\displaystyle \omega }$, it validates induction in the sense of the first-order arithmetic theory. In a set theory context where ${\displaystyle \omega }$ is a set, this induction principle can be used to prove predicatively defined subclasses of ${\displaystyle \omega }$ to be the set ${\displaystyle \omega }$ itself. The so called full mathematical induction schema now postulates set equality of ${\displaystyle \omega }$ to all its inductive subclasses. As in the classical theory, it is also implied when passing to the impredicative full Separation schema. As stated in the section on Choice, induction principles such as this are also implied by various forms of choice principles.

The recursion principle for set functions mentioned in the section dedicated to arithmetic is also implied by the full mathematical induction schema over one's structure modeling the naturals (e.g. ${\displaystyle \omega }$). So for that theorem, granting a model of Heyting arithmetic, it represents an alternative to exponentiation principles.

Predicate formulas used with the schema are to be understood as formulas in first-order set theory. The zero ${\displaystyle 0}$ denotes the set ${\displaystyle \{\}}$ as above, and the set ${\displaystyle Sn}$ denotes the successor set of ${\displaystyle n\in \omega }$, with ${\displaystyle n\in Sn}$. By Axiom of Infinity above, it is again a member of ${\displaystyle \omega }$. Beware that unlike in an arithmetic theory, the naturals here are not the abstract elements in the domain of discourse, but elements of a model. As has been observed in previous discussions, when accepting ${\displaystyle {\mathsf {ECST}}}$, not even for all predicatively defined sets is the equality to such a finite von Neumann ordinal necessarily decidable.

Set Induction

Going beyond the previous induction principles, one has full set induction, which is to be compared to well-founded induction. Like mathematical induction above, the following axiom is formulated as a schema in terms of predicates, and thus has a different character than induction principles proven from predicative set theory axioms. A variant of the axiom just for bounded formulas is also studied independently and may be derived from other axioms.

Here ${\displaystyle \forall (z\in \{\}).\phi (z)}$ holds trivially and so this covers to the "bottom case" ${\displaystyle \phi (\{\})}$ in the standard framework. This (as well as natural number induction) may again be restricted to just the bounded set formulas, in which case arithmetic is not impacted.

In ${\displaystyle {\mathsf {ECST}}}$, the axiom proves induction in transitive sets and so in particular also for transitive sets of transitive sets. The latter then is an adequate definition of the ordinals, and even a ${\displaystyle \Delta _{0}}$-formulation. Set induction in turn enables ordinal arithmetic in this sense. It further allows definitions of class functions by transfinite recursion. The study of the various principles that grant set definitions by induction, i.e. inductive definitions, is a main topic in the context of constructive set theory and their comparatively weak strengths. This also holds for their counterparts in type theory. Replacement is not required to prove induction over the set of naturals from set induction, but that axiom is necessary for their arithmetic modeled within the set theory.

The axiom of regularity is a single statement with universal quantifier over sets and not a schema. As show, it implies ${\displaystyle {\mathrm {PEM} }}$, and so is non-constructive. Now for ${\displaystyle \phi }$ taken to be the negation of some predicate ${\displaystyle \neg S}$ and writing ${\displaystyle \Sigma }$ for the class ${\displaystyle \{y\mid S(y)\}}$, induction reads

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

Via the contrapositive, set induction implies all instances of regularity but only with double-negated existence in the conclusion. In the other direction, given enough transitive sets, regularity implies each instance of set induction.

Metalogic

The theory formulated above can be expressed as ${\displaystyle {\mathsf {CZF}}}$ with its collection axioms discarded in favour of the weaker Replacement and Exponentiation axioms. It proves the Cauchy reals to be a set, but not the class of Dedekind reals.

Call an ordinal itself trichotomous if the irreflexive membership relation " ${\displaystyle \in }$" among its members is trichotomous. Like the axiom of regularity, set induction restricts the possible models of " ${\displaystyle \in }$" and thus that of a set theory, as was the motivation for the principle in the 20's. But the constructive theory here does not prove a trichotomy for all ordinals, while the trichotomous ordinals are not well behaved with respect to the notion of successor and rank.

The added proof-theoretical strength attained with Induction in the constructive context is significant, even if dropping Regularity in the context of ${\displaystyle {\mathsf {ZF}}}$ does not reduce the proof-theoretical strength. Even without Exponentiation, the present theory with set induction has the same proof theoretic strength as ${\displaystyle {\mathsf {CZF}}}$ and proves the same functions recursive. Specifically, its proof-theoretic large countable ordinal is the Bachmann–Howard ordinal. This is also the ordinal of classical or intuitionistic Kripke–Platek set theory. It is consistent even with ${\displaystyle {\mathsf {IZF}}}$ to assume that the class of trichotomous ordinals form a set. The current theory augmented with this ordinal set existence postulate proves the consistency of ${\displaystyle {\mathsf {CZF}}}$.

Aczel was also one of the main developers or Non-well-founded set theory, which rejects set induction.

Relation to ZF

The theory also constitutes a presentation of Zermelo–Fraenkel set theory ${\displaystyle {\mathsf {ZF}}}$ in the sense that variants of all its eight axioms are present. Extensionality, Pairing, Union and Replacement are indeed identical. Separation is adopted in a weak predicative form while Infinity is stated in a strong formulation. Akin to the classical formulation, this Separation axiom and the existence of any set already proves the Empty Set axiom. Exponentiation for finite domains and full mathematical induction are also implied by their stronger adopted variants. Without the principle of excluded middle, the theory here is lacking, in its classical form, full Separation, Powerset as well as Regularity. Accepting ${\displaystyle {\mathrm {PEM} }}$ now exactly leads into the classical theory.

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