Análisis constructivo

En la lógica intuicionista, el silogismo disyuntivo en la forma${\displaystyle (\phi \lor \psi )\to (\neg \phi \to \psi )}$generalmente solo va en el${\displaystyle \to }$-dirección. En un pseudoorden, uno tiene

${\displaystyle \neg (x>0\lor 0>x)\to x\cong 0}$

y de hecho, como mucho una de las tres puede cumplirse a la vez. Pero la ley de disyunción de tricotomía más fuerte y lógicamente positiva no se cumple en general , es decir, no es demostrable que para todos los números reales,

${\displaystyle (x>0\lor 0>x)\lor x\cong 0}$

Ver análisis${\displaystyle {\mathrm {LPO} }}$Sin embargo, otras disyunciones se infieren a partir de otros resultados de positividad, por ejemplo:${\displaystyle (x+y>0)\to (x>0\lor y>0)}$Asimismo, el orden asimétrico en la teoría debe cumplir la propiedad de linealidad débil.${\displaystyle (y>x)\to (y>t\lor t>x)}$a pesar de${\displaystyle t}$, relacionado con la ubicación de los reales.

La teoría validará otros axiomas relativos a la relación entre el predicado de positividad${\displaystyle x>0}$y las operaciones algebraicas, incluyendo la inversión multiplicativa, así como el teorema del valor intermedio para polinomios. En esta teoría, entre dos números cualesquiera existen otros números.

En el contexto del análisis, el predicado lógicamente positivo auxiliar

${\displaystyle x\#y\,:=\,(x>y\lor y>x)}$

puede definirse de forma independiente y constituye una relación de separación . Con ella, el sustituto de los principios anteriores da cohesión.

${\displaystyle \neg (x\#0)\leftrightarrow (x\cong 0)}$

Por lo tanto, la separación también puede funcionar como una definición de "${\displaystyle \cong }$", convirtiéndolo en una negación. Todas las negaciones son estables en la lógica intuicionista y, por lo tanto,

${\displaystyle \neg \neg (x\cong y)\leftrightarrow (x\cong y)}$

La esquiva disyunción de la tricotomía se lee entonces

${\displaystyle (x\#0)\lor \neg (x\#0)}$

Es importante destacar una prueba de la disyunción.${\displaystyle x\#y}$conlleva información positiva , en ambos sentidos de la palabra. Vía${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$También se deduce que${\displaystyle x\#0\to \neg (x\cong 0)}$En otras palabras: Una demostración de que un número es de alguna manera distinto de cero es también una demostración de que este número es distinto de cero. Pero, constructivamente, no se deduce que la afirmación doblemente negativa${\displaystyle \neg (x\cong 0)}$implicaría${\displaystyle x\#0}$. En consecuencia, muchas afirmaciones clásicamente equivalentes se bifurcan en afirmaciones distintas. Por ejemplo, para un polinomio fijo${\displaystyle p\in {\mathbb {R} }[x]}$y fijo${\displaystyle k\in {\mathbb {N} }}$, la declaración de que el${\displaystyle k}$coeficiente 'enésimo${\displaystyle a_{k}}$de${\displaystyle p}$La afirmación de que es distinto de cero es más fuerte que la mera afirmación de que no es cero. Una demostración de lo anterior explica cómo${\displaystyle a_{k}}$y cero están relacionados, con respecto al predicado de ordenación sobre los números reales, mientras que una demostración de este último muestra cómo la negación de tales condiciones implicaría una contradicción. A su vez, existe también una noción estricta y otra más flexible de, por ejemplo, ser un polinomio de tercer grado.

Entonces, el término medio excluido para${\displaystyle x\#0}$¿Es Apriori más fuerte que eso?${\displaystyle x\cong 0}$. Sin embargo, véase la discusión de posibles principios axiomáticos adicionales con respecto a la fuerza de "${\displaystyle \cong }$" abajo.

Por último, la relación${\displaystyle 0\geq x}$puede definirse mediante o demostrarse equivalente a la afirmación lógicamente negativa${\displaystyle \neg (x>0)}$, y luego${\displaystyle x\leq 0}$se define como${\displaystyle 0\geq x}$La decidibilidad de la positividad puede expresarse, por lo tanto, como${\displaystyle x>0\lor 0\geq x}$, lo cual, como se ha señalado, no será demostrable en general. Pero tampoco lo será la disyunción de la totalidad.${\displaystyle x\geq 0\lor 0\geq x}$, véase también analítico${\displaystyle {\mathrm {LLPO} }}$.

Según una ley válida de De Morgan , la conjunción de tales enunciados también se convierte en una negación de la separación, y así

${\displaystyle (x\geq y\land y\geq x)\leftrightarrow (x\cong y)}$

La disyunción${\displaystyle x>y\lor x\cong y}$implica${\displaystyle x\geq y}$, pero la otra dirección tampoco es demostrable en general. En un cuerpo real cerrado constructivo, la relación "${\displaystyle \geq }$" es una negación y no es equivalente a la disyunción en general .

Exigir buenas propiedades de orden como las anteriores, pero al mismo tiempo fuertes propiedades de completitud implica${\displaystyle {\mathrm {PEM} }}$Cabe destacar que la completitud de MacNeille tiene mejores propiedades de completitud como colección, pero una teoría más intrincada de su relación de orden y, a su vez, peores propiedades de localización. Aunque menos comúnmente empleada, esta construcción también se simplifica a los números reales clásicos cuando se asume${\displaystyle {\mathrm {PEM} }}$.

Dado que el máximo en un conjunto finito de números racionales es decidible, se puede definir una aplicación de valor absoluto en los números reales y la convergencia de Cauchy y los límites de sucesiones de números reales se pueden definir como de costumbre.

Un módulo de convergencia se emplea a menudo en el estudio constructivo de secuencias de Cauchy de números reales, lo que significa la asociación de cualquier${\displaystyle \varepsilon >0}$a un índice apropiado (más allá del cual las secuencias están más cerca que${\displaystyle \varepsilon }$) se requiere en forma de una función explícita y estrictamente creciente.${\displaystyle \varepsilon \mapsto N(\varepsilon )}$Dicho módulo puede considerarse para una sucesión de números reales, pero también puede considerarse para todos los números reales mismos, en cuyo caso realmente se está tratando con una sucesión de pares.

Dicho modelo permite definir más nociones de teoría de conjuntos. Para cualquier subconjunto de números reales, se puede hablar de una cota superior.${\displaystyle b}$, caracterizado negativamente usando${\displaystyle x\leq b}$. Se puede hablar de límites superiores mínimos con respecto a "${\displaystyle \leq }$". Un supremo es una cota superior dada a través de una sucesión de números reales, caracterizada positivamente mediante "${\displaystyle <}$". Si un subconjunto con un límite superior se comporta bien con respecto a "${\displaystyle <}$" (discutido más adelante), tiene un supremo.

Una formalización del análisis constructivo, que modela las propiedades de orden descritas anteriormente, demuestra teoremas para secuencias de números racionales.${\displaystyle x}$cumplir la condición de regularidad${\displaystyle |x_{n}-x_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}$. Una alternativa es utilizar el más ajustado${\displaystyle 2^{-n}}$en lugar de${\displaystyle {\tfrac {1}{n}}}$y en este último caso se deben usar índices distintos de cero. Ningún par de las entradas racionales en una secuencia regular son más que${\displaystyle {\tfrac {3}{2}}}$aparte y así se pueden calcular números naturales que excedan cualquier real. Para las secuencias regulares, se define la propiedad de positividad suelta lógicamente positiva como${\displaystyle x>0\,:=\,\exists n.x_{n}>{\tfrac {1}{n}}}$, donde la relación del lado derecho está en términos de números racionales. Formalmente, un real positivo en este lenguaje es una secuencia regular junto con una positividad de testimonio natural. Además,${\displaystyle x\cong y\,:=\,\forall n.|x_{n}-y_{n}|\leq {\tfrac {2}{n}}}$, lo cual es lógicamente equivalente a la negación${\displaystyle \neg \exists n.|x_{n}-y_{n}|>{\tfrac {2}{n}}}$. Esto es demostrablemente transitivo y, a su vez, una relación de equivalencia . A través de este predicado, las secuencias regulares en la banda${\displaystyle |x_{n}|\leq {\tfrac {2}{n}}}$se consideran equivalentes a la secuencia cero. Tales definiciones son, por supuesto, compatibles con las investigaciones clásicas y sus variaciones fueron bien estudiadas también anteriormente. Uno tiene${\displaystyle y>x}$como${\displaystyle (y-x)>0}$. También,${\displaystyle x\geq 0}$puede definirse a partir de una propiedad numérica de no negatividad, como${\displaystyle x_{n}\geq -{\tfrac {1}{n}}}$a pesar de${\displaystyle n}$, pero luego se demostró que era equivalente a la negación lógica de la anterior. ^{[ 5 ] [ 6 ]}

La definición anterior de${\displaystyle x\cong y}$utiliza un límite común${\displaystyle {\tfrac {2}{n}}}$Otras formalizaciones toman directamente como definición que para cualquier límite fijo${\displaystyle {\tfrac {2}{N}}}$, los números${\displaystyle x}$y${\displaystyle y}$eventualmente deben estar para siempre al menos igual de cerca. Límites que disminuyen exponencialmente${\displaystyle 2^{-n}}$También se utilizan, también se dice en una condición de número real.${\displaystyle \forall n.|x_{n}-x_{n+1}|<2^{-n}}$y de igual modo para la igualdad de dos de esos números reales. Además, puede requerirse que las sucesiones de racionales tengan un módulo de convergencia. Las propiedades de positividad pueden definirse como estar eventualmente separadas para siempre por algún racional.

Elección de función en${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$o principios más sólidos respaldan dichos marcos.

Vale la pena señalar que las secuencias en${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$se pueden codificar de forma bastante compacta, ya que cada uno puede asignarse a una subclase única de${\displaystyle {\mathbb {N} }}$Una secuencia de racionales${\displaystyle i\mapsto {\tfrac {n_{i}}{d_{i}}}(-1)^{s_{i}}}$puede codificarse como un conjunto de cuádruples${\displaystyle \langle i,n_{i},d_{i},s_{i}\rangle \in {\mathbb {N} }^{4}}$. A su vez, esto puede codificarse como números naturales únicos.${\displaystyle 2^{i}\cdot 3^{n_{i}}\cdot 5^{d_{i}}\cdot 7^{s_{i}}}$utilizando el teorema fundamental de la aritmética . También existen funciones de emparejamiento más económicas, o etiquetas de codificación de extensión o metadatos. Por ejemplo, utilizando esta codificación, la secuencia${\displaystyle i\mapsto {\textstyle \sum }_{k=0}^{i}{\tfrac {1}{k!}}}$, o${\displaystyle 1,2,{\tfrac {5}{2}},{\tfrac {8}{3}},\dots }$, puede utilizarse para calcular el número de Euler y con la codificación anterior se asigna a la subclase${\displaystyle \{15,90,24300,6561000,\dots \}}$de${\displaystyle {\mathbb {N} }}$Si bien este ejemplo, una secuencia explícita de sumas, es una función recursiva total desde el principio, la codificación también implica que estos objetos están dentro del alcance de los cuantificadores en la aritmética de segundo orden.

En algunos marcos de análisis, el nombre de números reales se da a tales secuencias bien comportadas o racionales, y relaciones tales como${\displaystyle x\cong y}$se denominan igualdad o números reales . Sin embargo, tenga en cuenta que existen propiedades que pueden distinguir entre dos${\displaystyle \cong }$-reales relacionados.

Por el contrario, en una teoría de conjuntos que modela los naturales${\displaystyle {\mathbb {N} }}$y valida la existencia incluso de espacios de funciones clásicamente no numerables (y ciertamente decir${\displaystyle {\mathsf {CZF}}}$o incluso${\displaystyle {\mathsf {ZFC}}}$) los números equivalentes con respecto a "${\displaystyle \cong }$" en${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$Los números reales pueden agruparse en un conjunto, que se denomina número real de Cauchy . En este lenguaje, las secuencias racionales regulares se reducen a una mera representación de un número real de Cauchy. La igualdad de estos números reales viene dada por la igualdad de conjuntos, que se rige por el axioma de extensionalidad de la teoría de conjuntos . En consecuencia, la teoría de conjuntos demuestra propiedades para los números reales, es decir, para esta clase de conjuntos, expresadas mediante la igualdad lógica. Los números reales constructivos, en presencia de axiomas de elección apropiados, serán completos en Cauchy, pero no automáticamente completos en orden. ^{[ 7 ]}

En este contexto también puede ser posible modelar una teoría o números reales en términos de cortes de Dedekind de${\displaystyle {\mathbb {Q} }}$. Al menos cuando se asume${\displaystyle {\mathrm {PEM} }}$o elección dependiente, estas estructuras son isomorfas.

Otro enfoque es definir un número real como un cierto subconjunto de${\displaystyle {\mathbb {Q} }\times {\mathbb {Q} }}$, que contienen pares que representan intervalos habitados que se intersecan por pares.

Recuerde que el pedido anticipado de los cardenales "${\displaystyle \leq }$" en la teoría de conjuntos es la noción primaria definida como existencia de inyección . Como resultado, la teoría constructiva del orden cardinal puede divergir sustancialmente de la clásica. Aquí, conjuntos como${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$o algunos modelos de los números reales pueden considerarse subcontables .

Dicho esto, la construcción diagonal de Cantor demuestra la incontableza de conjuntos potencia como${\displaystyle {\mathcal {P}}{\mathbb {N} }}$y espacios funcionales simples como${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$es intuicionistamente válido. Suponiendo${\displaystyle {\mathrm {PEM} }}$o alternativamente el axioma de elección contable , modelos de${\displaystyle {\mathbb {R} }}$son siempre incontables también sobre un marco constructivo. ^{[ 8 ]} Una variante de la construcción diagonal relevante para el presente contexto puede formularse de la siguiente manera, demostrada usando elección contable y para reales como secuencias de racionales: ^{[ 9 ]}

Para cualquier par de números reales${\displaystyle a<b}$y cualquier secuencia de números reales${\displaystyle x_{n}}$, existe una real${\displaystyle z}$con${\displaystyle a<z<b}$y${\displaystyle \forall (n\in {\mathbb {N} }).x_{n}\,\#\,z}$.

Las formulaciones de los números reales, con la ayuda de módulos explícitos, permiten tratamientos separados.

Según Kanamori , "se ha perpetuado una tergiversación histórica que asocia la diagonalización con la no constructividad" y un componente constructivo del argumento diagonal ya apareció en la obra de Cantor. ^{[ 10 ]}