Análisis constructivo

Análisis matemático

En matemáticas , el análisis constructivo es un análisis matemático realizado de acuerdo con algunos principios de matemáticas constructivas .

Introducción

El nombre de la materia contrasta con el análisis clásico , que en este contexto significa análisis realizado según los principios más comunes de las matemáticas clásicas. Sin embargo, existen varias escuelas de pensamiento y muchas formalizaciones diferentes del análisis constructivo. ^[1] Ya sea clásico o constructivo de alguna manera, cualquier marco de análisis de este tipo axiomatiza la línea de números reales de alguna manera, una colección que extiende los racionales y con una relación de separación definible a partir de una estructura de orden asimétrico. El centro del escenario lo ocupa un predicado de positividad, aquí denotado , que gobierna una igualdad a cero . Los miembros de la colección generalmente se denominan simplemente números reales . Si bien este término está sobrecargado en la materia, todos los marcos comparten un amplio núcleo común de resultados que también son teoremas del análisis clásico. ${\displaystyle x>0}$ ${\displaystyle x\cong 0}$

Los marcos constructivos para su formulación son extensiones de la aritmética de Heyting por tipos, incluyendo , aritmética constructiva de segundo orden , o teorías de topos , tipos o conjuntos constructivos suficientemente fuertes como , una contraparte constructiva de . Por supuesto, también se puede estudiar una axiomatización directa . ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {ZF}}}$

Preliminares lógicos

La lógica básica del análisis constructivo es la lógica intuicionista , lo que significa que el principio del tercero excluido no se asume automáticamente para cada proposición . Si una proposición es demostrable, esto significa exactamente que la afirmación de inexistencia que es demostrable sería absurda, y por lo tanto esta última no puede también ser demostrable en una teoría consistente. La afirmación de existencia doblemente negada es una declaración lógicamente negativa y está implícita en, pero generalmente no es equivalente a la afirmación de existencia en sí. Gran parte de las complejidades del análisis constructivo se pueden enmarcar en términos de la debilidad de las proposiciones de la forma lógicamente negativa , que generalmente es más débil que . A su vez, también una implicación generalmente no puede ser revertida. ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle \neg \neg \exists x.\theta (x)}$ ${\displaystyle \neg \exists x.\theta (x)}$ ${\displaystyle \neg \neg \phi }$ ${\displaystyle \phi }$ ${\displaystyle {\big (}\exists x.\theta (x){\big )}\to \neg \forall x.\neg \theta (x)}$

Si bien una teoría constructiva prueba menos teoremas que su contraparte clásica en su presentación clásica, puede exhibir propiedades metalógicas atractivas. Por ejemplo, si una teoría exhibe la propiedad de disyunción , entonces si prueba una disyunción entonces también o . Ya en la aritmética clásica, esto se viola para las proposiciones más básicas sobre secuencias de números, como se demuestra a continuación. ${\displaystyle {\mathsf {T}}}$ ${\displaystyle {\mathsf {T}}\vdash \phi \lor \psi }$ ${\displaystyle {\mathsf {T}}\vdash \phi }$ ${\displaystyle {\mathsf {T}}\vdash \psi }$

Predicados indecidibles

Una estrategia común de formalización de números reales es en términos de secuencias o racionales, y por eso extraemos la motivación y los ejemplos en términos de ellos. Entonces, para definir términos, considere un predicado decidible sobre los naturales, que en el vernáculo constructivo significa que es demostrable, y sea la función característica definida para ser exactamente igual a donde es verdadera. La secuencia asociada es monótona, con valores que no crecen estrictamente entre los límites y . Aquí, a los efectos de la demostración, definiendo una igualdad extensional a la secuencia cero , se sigue que . Nótese que el símbolo " " se usa en varios contextos aquí. Para cualquier teoría que capture la aritmética, hay muchas afirmaciones de este tipo aún no decididas e incluso demostrablemente independientes . Dos ejemplos son la conjetura de Goldbach y la oración de Rosser de una teoría. ${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$ ${\displaystyle \forall n.{\big (}Q(n)\lor \neg Q(n){\big )}}$ ${\displaystyle \chi _{Q}\colon {\mathbb {N} }\to \{0,1\}}$ ${\displaystyle 0}$ ${\displaystyle Q}$ ${\displaystyle q_{n}\,:=\,{\textstyle \sum }_{k=0}^{n}\chi _{Q}(n)/2^{n+1}}$ ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle (q\cong _{\mathrm {ext} }0)\,:=\,\forall n.q_{n}=0}$ ${\displaystyle q\cong _{\mathrm {ext} }0\leftrightarrow \forall n.Q(n)}$ ${\displaystyle 0}$ ${\displaystyle \forall n.Q(n)}$ ${\displaystyle \Pi _{1}^{0}}$

Consideremos cualquier teoría con cuantificadores que se extiendan a secuencias recursivas primitivas de valores racionales. La lógica mínima ya prueba la afirmación de no contradicción para cualquier proposición, y que la negación del tercero excluido para cualquier proposición dada sería absurda. Esto también significa que no hay ninguna teoría consistente (aunque sea anticlásica) que rechace la disyunción del tercero excluido para cualquier proposición dada. De hecho, sostiene que ${\displaystyle {\mathsf {T}}}$

${\displaystyle {\mathsf {T}}\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,\neg \neg {\big (}(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0){\big )}}$

Este teorema es lógicamente equivalente a la afirmación de inexistencia de una secuencia para la cual la disyunción del medio excluido sobre la igualdad con cero sería refutable. No se puede demostrar ninguna secuencia con esa disyunción rechazada. Supongamos que las teorías en cuestión son consistentes y aritméticamente sólidas. Ahora bien, los teoremas de Gödel significan que hay una secuencia explícita tal que, para cualquier precisión fija, demuestra que la secuencia cero es una buena aproximación a , pero también se puede establecer metalógicamente que así como . ^[2] Aquí esta proposición equivale nuevamente a la proposición de forma cuantificada universal. Trivialmente ${\displaystyle g\in {\mathbb {Q} }^{\mathbb {N} }}$ ${\displaystyle {\mathsf {T}}}$ ${\displaystyle g}$ ${\displaystyle {\mathsf {T}}\,\nvdash \,(g\cong _{\mathrm {ext} }0)}$ ${\displaystyle {\mathsf {T}}\,\nvdash \,\neg (g\cong _{\mathrm {ext} }0)}$ ${\displaystyle g\cong _{\mathrm {ext} }0}$

${\displaystyle {\mathsf {T}}+{\mathrm {PEM} }\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0)}$

Incluso si estas afirmaciones de disyunción aquí no contienen ninguna información. En ausencia de otros axiomas que rompan las propiedades metalógicas, la implicación constructiva en cambio generalmente refleja demostrabilidad. Las afirmaciones tabú que no deberían ser decidibles (si el objetivo es respetar la interpretación de demostrabilidad de las afirmaciones constructivas) también pueden diseñarse para definiciones de una equivalencia personalizada " " en las formalizaciones que se indican a continuación. Para las implicaciones de las disyunciones de proposiciones aún no probadas o refutadas, se habla de contraejemplos brouwerianos débiles . ${\displaystyle \cong }$

Orden vs. disyunciones

La teoría del cuerpo cerrado real puede axiomatizarse de modo que todos los axiomas no lógicos estén de acuerdo con principios constructivos. Esto concierne a un anillo conmutativo con postulados para un predicado de positividad , con una unidad positiva y un cero no positivo, es decir, y . En cualquier anillo de este tipo, se puede definir , que constituye un orden total estricto en su formulación constructiva (también llamado orden lineal o, para ser explícitos sobre el contexto, un pseudoorden ). Como es habitual, se define como . ${\displaystyle x>0}$ ${\displaystyle 1>0}$ ${\displaystyle \neg (0>0)}$ ${\displaystyle y>x\,:=\,(y-x>0)}$ ${\displaystyle x<0}$ ${\displaystyle 0>x}$

Esta teoría de primer orden es relevante ya que las estructuras que se analizan a continuación son modelos de la misma. ^[3] Sin embargo, esta sección no aborda aspectos relacionados con la topología y las subestructuras aritméticas relevantes no se pueden definir en ella.

Como se explicó, varios predicados no serán decidibles en una formulación constructiva, como los que se forman a partir de relaciones de teoría del orden. Esto incluye " ", que se convertirá en equivalente a una negación. A continuación se analizan explícitamente las disyunciones cruciales. ${\displaystyle \cong }$

Tricotomía

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

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

y, de hecho, como máximo, uno de los tres puede cumplirse a la vez. Pero la ley más fuerte, lógicamente positiva, de la disyunción tricotomía 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}$

Véase analítica ${\displaystyle {\mathrm {LPO} }}$ . Sin embargo, se implican otras disyunciones basadas en otros resultados de positividad, por ejemplo . Asimismo, el orden asimétrico en la teoría debería cumplir con la propiedad de linealidad débil para todos los , relacionada con la localización de los números reales. ${\displaystyle (x+y>0)\to (x>0\lor y>0)}$ ${\displaystyle (y>x)\to (y>t\lor t>x)}$ ${\displaystyle t}$

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

Apartamiento

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

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

puede definirse independientemente y constituye una relación de separación . Con ella, la sustitución de los principios anteriores da hermeticidad.

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

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

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

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

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

Es importante destacar que una prueba de la disyunción conlleva información positiva ${\displaystyle x\#y}$ , en ambos sentidos de la palabra. A través de ella también se sigue que . En 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 no es cero. Pero constructivamente no se sigue que la afirmación doblemente negativa implicaría . En consecuencia, muchas afirmaciones clásicamente equivalentes se bifurcan en afirmaciones distintas. Por ejemplo, para un polinomio fijo y fijo , la afirmación de que el 'ésimo coeficiente de es distinto de cero es más fuerte que la mera afirmación de que no es cero. Una demostración de la primera explica cómo y cero están relacionados, con respecto al predicado ordenador de los reales, mientras que una demostración de la segunda muestra cómo la negación de tales condiciones implicaría una contradicción. A su vez, existe entonces también una noción fuerte y otra más laxa de, por ejemplo, ser un polinomio de tercer orden. ${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$ ${\displaystyle x\#0\to \neg (x\cong 0)}$ ${\displaystyle \neg (x\cong 0)}$ ${\displaystyle x\#0}$ ${\displaystyle p\in {\mathbb {R} }[x]}$ ${\displaystyle k\in {\mathbb {N} }}$ ${\displaystyle k}$ ${\displaystyle a_{k}}$ ${\displaystyle p}$ ${\displaystyle a_{k}}$

Por lo tanto, el tercero excluido para es a priori más fuerte que el de . Sin embargo, véase el análisis de otros posibles principios axiomáticos relacionados con la fuerza de " " más adelante. ${\displaystyle x\#0}$ ${\displaystyle x\cong 0}$ ${\displaystyle \cong }$

Orden parcial no estricta

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

Por una ley de De Morgan válida , la conjunción de tales enunciados también se convierte en una negación de la separación, y por lo tanto

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

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

Variaciones

Exigir buenas propiedades de orden como las anteriores pero fuertes propiedades de completitud al mismo tiempo implica . En particular, 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. Si bien se emplea con menos frecuencia, también esta construcción se simplifica a los números reales clásicos al suponer . ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathrm {PEM} }}$

Invertibilidad

En el anillo conmutativo de los números reales, un elemento demostrablemente no invertible es igual a cero. Esta y la estructura de localidad más básica se abstraen en la teoría de los campos de Heyting .

Formalización

Secuencias racionales

Un enfoque común es identificar los números reales con secuencias no volátiles en . Las secuencias constantes corresponden a números racionales. Las operaciones algebraicas como la suma y la multiplicación se pueden definir componente por componente, junto con una reindexación sistemática para acelerar. La definición en términos de secuencias permite además la definición de un orden estricto " " que cumple los axiomas deseados. Otras relaciones discutidas anteriormente pueden definirse en términos de ella. En particular, cualquier número aparte de , es decir , eventualmente tiene un índice más allá del cual todos sus elementos son invertibles. ^[4] Luego se pueden probar varias implicaciones entre las relaciones, así como entre secuencias con varias propiedades. ${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$ ${\displaystyle >}$ ${\displaystyle x}$ ${\displaystyle 0}$ ${\displaystyle x\#0}$

Módulos

Como el máximo en un conjunto finito de números racionales es decidible, se puede definir un mapa de valores absolutos en los números reales y la convergencia de Cauchy y los límites de secuencias de números reales se pueden definir como de costumbre.

En el estudio constructivo de las sucesiones de Cauchy de números reales se suele emplear un módulo de convergencia , lo que significa que se requiere la asociación de cualquier a un índice apropiado (más allá del cual las sucesiones están más cerca que ) en forma de una función explícita y estrictamente creciente . Se puede considerar un módulo de este tipo para una sucesión de números reales, pero también para todos los números reales en sí, en cuyo caso se trata realmente de una sucesión de pares. ${\displaystyle \varepsilon >0}$ ${\displaystyle \varepsilon }$ ${\displaystyle \varepsilon \mapsto N(\varepsilon )}$

Límites y supremacía

Dado un modelo de este tipo, se pueden definir nociones más teóricas de conjuntos. Para cualquier subconjunto de números reales, se puede hablar de un límite superior , caracterizado negativamente mediante . Se puede hablar de límites superiores mínimos con respecto a " ". Un supremo es un límite superior dado a través de una secuencia de números reales, caracterizado positivamente mediante " ". Si un subconjunto con un límite superior se comporta bien con respecto a " " (discutido más adelante), tiene un supremo. ${\displaystyle b}$ ${\displaystyle x\leq b}$ ${\displaystyle \leq }$ ${\displaystyle <}$ ${\displaystyle <}$

Formalización del obispo

Una formalización del análisis constructivo, que modela las propiedades de orden descritas anteriormente, demuestra teoremas para secuencias de racionales que cumplen la condición de regularidad . Una alternativa es usar el más estricto en lugar de , y en el último caso se deben usar índices distintos de cero. No hay dos de las entradas racionales en una secuencia regular que estén más separadas que y, por lo tanto, 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 , donde la relación en el 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 testigo natural. Además, , que es lógicamente equivalente a la negació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 se consideran equivalentes a la secuencia cero. Tales definiciones son, por supuesto, compatibles con las investigaciones clásicas y las variaciones de las mismas también se estudiaron bien antes. Uno tiene como . También puede definirse a partir de una propiedad numérica de no negatividad, como para todos los , pero luego demostrarse que es equivalente a la negación lógica del anterior. ^{[5] [6]} ${\displaystyle x}$ ${\displaystyle |x_{n}-x_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}$ ${\displaystyle 2^{-n}}$ ${\displaystyle {\tfrac {1}{n}}}$ ${\displaystyle {\tfrac {3}{2}}}$ ${\displaystyle x>0\,:=\,\exists n.x_{n}>{\tfrac {1}{n}}}$ ${\displaystyle x\cong y\,:=\,\forall n.|x_{n}-y_{n}|\leq {\tfrac {2}{n}}}$ ${\displaystyle \neg \exists n.|x_{n}-y_{n}|>{\tfrac {2}{n}}}$ ${\displaystyle |x_{n}|\leq {\tfrac {2}{n}}}$ ${\displaystyle y>x}$ ${\displaystyle (y-x)>0}$ ${\displaystyle x\geq 0}$ ${\displaystyle x_{n}\geq -{\tfrac {1}{n}}}$ ${\displaystyle n}$

Variaciones

La definición anterior de utiliza un límite común . Otras formalizaciones toman directamente como definición que para cualquier límite fijo , los números y deben eventualmente estar siempre al menos tan cerca. También se utilizan límites exponencialmente descendentes, también digamos en una condición de número real , y lo mismo para la igualdad de dos reales de ese tipo. Y también se puede requerir que las secuencias de racionales tengan un módulo de convergencia. Las propiedades de positividad pueden definirse como estar eventualmente separados para siempre por algún racional. ${\displaystyle x\cong y}$ ${\displaystyle {\tfrac {2}{n}}}$ ${\displaystyle {\tfrac {2}{N}}}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle 2^{-n}}$ ${\displaystyle \forall n.|x_{n}-x_{n+1}|<2^{-n}}$

La elección de funciones o principios más fuertes ayudan a estos marcos. ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$

Codificación

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

Teoría de conjuntos

Reales de Cauchy

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

Por el contrario, en una teoría de conjuntos que modela los naturales y valida la existencia incluso de espacios de funciones clásicamente incontables (y ciertamente digamos o incluso ) los números equivalentes con respecto a " " en pueden agruparse en un conjunto y entonces esto se llama el número real de Cauchy . En ese lenguaje, las secuencias racionales regulares se degradan a un mero representante de un real de Cauchy. La igualdad de esos reales está entonces dada por la igualdad de conjuntos, que está gobernada por el axioma teórico de extensionalidad de conjuntos. Un resultado es que la teoría de conjuntos probará propiedades para los reales, es decir, para esta clase de conjuntos, expresadas usando la igualdad lógica. Los reales constructivos en presencia de axiomas de elección apropiados serán Cauchy-completos pero no automáticamente orden-completos. ^[7] ${\displaystyle {\mathbb {N} }}$ ${\displaystyle {\mathsf {CZF}}}$ ${\displaystyle {\mathsf {ZFC}}}$ ${\displaystyle \cong }$ ${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$

Reales de Dedekind

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

Aritmética de intervalos

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

Incontabilidad

Recordemos que el preorden de los cardinales " " 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 o algunos modelos de los números reales pueden considerarse subcontables . ${\displaystyle \leq }$ ${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$

Dicho esto, la construcción diagonal de Cantor que demuestra la incontabilidad de conjuntos de potencias como y espacios de funciones simples como es válida desde el punto de vista intuicionista . Suponiendo o alternativamente el axioma de elección contable , los modelos de son siempre incontables también en un marco constructivo. ^[8] Una variante de la construcción diagonal relevante para el presente contexto puede formularse de la siguiente manera, demostrada utilizando la elección contable y para los números reales como secuencias de racionales: ^[9] ${\displaystyle {\mathcal {P}}{\mathbb {N} }}$ ${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$ ${\displaystyle {\mathrm {PEM} }}$ ${\displaystyle {\mathbb {R} }}$

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

Las formulaciones de los reales ayudadas por 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 aparecía en la obra de Cantor. ^[10]

Teoría de categorías y tipos

Todas estas consideraciones también pueden llevarse a cabo en un topos o teoría de tipos dependientes apropiada.

Principios

Para las matemáticas prácticas, en varias escuelas se adopta el axioma de elección dependiente .

El principio de Markov se adopta en la escuela rusa de matemáticas recursivas. Este principio refuerza el impacto de la negación demostrada de la igualdad estricta. Una forma denominada analítica del mismo otorga o . Se pueden formular formas más débiles. ${\displaystyle \neg (x\leq 0)\to x>0}$ ${\displaystyle \neg (x\cong 0)\to x\#0}$

La escuela brouweriana razona en términos de spreads y adopta la inducción de barra, clásicamente válida .

Escuelas anticlásicas

Mediante la adopción opcional de otros axiomas consistentes, la negación de la decidibilidad puede ser demostrable. Por ejemplo, la igualdad a cero se rechaza como decidible cuando se adoptan los principios de continuidad de Brouwer o la tesis de Church en matemáticas recursivas. ^[11] El principio de continuidad débil así como incluso refuta . La existencia de una secuencia de Specker se demuestra a partir de . Tales fenómenos también ocurren en los topos de realizabilidad . Cabe destacar que hay dos escuelas anticlásicas por ser incompatibles entre sí. Este artículo analiza los principios compatibles con la teoría clásica y se hace explícita la elección. ${\displaystyle {\mathrm {CT} _{0}}}$ ${\displaystyle x\geq 0\lor 0\geq x}$ ${\displaystyle {\mathrm {CT} _{0}}}$

Teoremas

Muchos teoremas clásicos solo pueden demostrarse en una formulación que sea lógicamente equivalente , en comparación con la lógica clásica . En términos generales, la formulación de teoremas en el análisis constructivo refleja la teoría clásica más cercana en espacios separables . Algunos teoremas solo pueden formularse en términos de aproximaciones .

El teorema del valor intermedio

Para un ejemplo simple, considere el teorema del valor intermedio (IVT). En el análisis clásico, el IVT implica que, dada cualquier función continua f desde un intervalo cerrado [ a , b ] hasta la línea real R , si f ( a ) es negativa mientras que f ( b ) es positiva , entonces existe un número real c en el intervalo tal que f ( c ) es exactamente cero . En el análisis constructivo, esto no se cumple, porque la interpretación constructiva de la cuantificación existencial ("existe") requiere que uno sea capaz de construir el número real c (en el sentido de que puede ser aproximado a cualquier precisión deseada por un número racional ). Pero si f ronda cerca de cero durante un tramo a lo largo de su dominio, entonces esto no necesariamente puede hacerse.

Sin embargo, el análisis constructivo proporciona varias formulaciones alternativas de la TFI, todas las cuales son equivalentes a la forma usual en el análisis clásico, pero no en el análisis constructivo. Por ejemplo, bajo las mismas condiciones en f que en el teorema clásico, dado cualquier número natural n (no importa cuán grande sea), existe (es decir, podemos construir) un número real c _n en el intervalo tal que el valor absoluto de f ( c _n ) es menor que 1/ n . Es decir, podemos acercarnos a cero tanto como queramos, incluso si no podemos construir una c que nos dé exactamente cero.

Como alternativa, podemos mantener la misma conclusión que en la IVT clásica (una única c tal que f ( c ) es exactamente cero) al tiempo que reforzamos las condiciones de f . Requerimos que f sea localmente distinto de cero , lo que significa que dado cualquier punto x en el intervalo [ a , b ] y cualquier número natural m , existe (podemos construir) un número real y en el intervalo tal que | y - x | < 1/ m y | f ( y )| > 0. En este caso, se puede construir el número deseado c . Esta es una condición complicada, pero hay varias otras condiciones que la implican y que se cumplen comúnmente; por ejemplo, cada función analítica es localmente distinta de cero (asumiendo que ya satisface f ( a ) < 0 y f ( b ) > 0).

Para ver este ejemplo de otra manera, observe que, según la lógica clásica , si la condición localmente distinta de cero falla, entonces debe fallar en algún punto específico x ; y entonces f ( x ) será igual a 0, de modo que la TVI es válida automáticamente. Por lo tanto, en el análisis clásico, que utiliza la lógica clásica, para probar la TVI completa, es suficiente probar la versión constructiva. Desde esta perspectiva, la TVI completa falla en el análisis constructivo simplemente porque el análisis constructivo no acepta la lógica clásica. Por el contrario, se puede argumentar que el verdadero significado de la TVI, incluso en matemáticas clásicas, es la versión constructiva que involucra la condición localmente distinta de cero , con la TVI completa seguida de "lógica pura" después. Algunos lógicos, aunque aceptan que las matemáticas clásicas son correctas, aún creen que el enfoque constructivo brinda una mejor comprensión del verdadero significado de los teoremas, de manera muy similar.

El principio del límite superior mínimo y los conjuntos compactos

Otra diferencia entre el análisis clásico y el constructivo es que el análisis constructivo no prueba el principio del mínimo límite superior , es decir, que cualquier subconjunto de la recta real R tendría un mínimo límite superior (o supremo), posiblemente infinito. Sin embargo, como con el teorema del valor intermedio, sobrevive una versión alternativa; en el análisis constructivo, cualquier subconjunto localizado de la recta real tiene un supremo. (Aquí un subconjunto S de R está localizado si, siempre que x < y sean números reales, existe un elemento s de S tal que x < s , o y es un límite superior de S .) De nuevo, esto es clásicamente equivalente al principio del mínimo límite superior completo, ya que todo conjunto está localizado en las matemáticas clásicas. Y de nuevo, aunque la definición de conjunto localizado es complicada, no obstante se satisface por muchos conjuntos comúnmente estudiados, incluidos todos los intervalos y todos los conjuntos compactos .

En estrecha relación con esto, en matemáticas constructivas, menos caracterizaciones de espacios compactos son constructivamente válidas; o, desde otro punto de vista, hay varios conceptos diferentes que son clásicamente equivalentes pero no constructivamente equivalentes. De hecho, si el intervalo [ a , b ] fuera secuencialmente compacto en el análisis constructivo, entonces la IVT clásica se seguiría de la primera versión constructiva en el ejemplo; uno podría encontrar c como un punto de agrupamiento de la secuencia infinita ( c _n ) _{n ∈ N} .

Véase también

• Portal de matemáticas

• Análisis computable
• Análisis constructivo no estándar
• Campo de Heyting
• Indecomponibilidad (matemática constructiva)
• Pseudo-orden

Referencias

1. Troelstra, AS, van Dalen D., Constructivismo en matemáticas: una introducción 1 ; Estudios en lógica y fundamentos de las matemáticas; Springer, 1988;
2. Smith, Peter (2007). Introducción a los teoremas de Gödel. Cambridge, Reino Unido: Cambridge University Press. ISBN 978-0-521-67453-9.Sr. 2384958  .
3. Erik Palmgren, Una axiomatización intuicionista de campos cerrados reales , Mathematical Logic Quarterly, Volumen 48, Número 2, Páginas: 163-320, febrero de 2002
4. Bridges D., Ishihara H., Rathjen M., Schwichtenberg H. (Editores), Manual de matemáticas constructivas ; Estudios de lógica y fundamentos de las matemáticas; (2023) págs. 201-207
5. Errett Bishop, Fundamentos del análisis constructivo , julio de 1967
6. Stolzenberg, Gabriel (1970). "Reseña: Errett Bishop, Fundamentos del análisis constructivo". Bull. Amer. Math. Soc. 76 (2): 301–323. doi : 10.1090/s0002-9904-1970-12455-7 .
7. Robert S. Lubarsky, Sobre la completitud de Cauchy de los reales de Cauchy constructivos, julio de 2015
8. Bauer, A., Hanson, JA "Los reales contables", 2022
9. Véase, por ejemplo, el Teorema 1 en Bishop, 1967, pág. 25.
10. Akihiro Kanamori , "El desarrollo matemático de la teoría de conjuntos de Cantor a Cohen", Boletín de lógica simbólica / Volumen 2 / Número 01 / marzo de 1996, págs. 1-71
11. Diener, Hannes (2020). "Matemática inversa constructiva". arXiv : 1804.05495 ​​[math.LO].

Lectura adicional

• Bishop, Errett (1967). Fundamentos del análisis constructivo . ISBN 4-87187-714-0.
• Bridger, Mark (2007). Análisis real: un enfoque constructivo . Hoboken: Wiley. ISBN 0-471-79230-6.