# Prueba constructiva

En matemáticas, una prueba constructiva es un método de demostración para constatar la existencia de un objeto matemático creando o proporcionando un método para crear el objeto. Esto contrasta con una prueba no constructiva (también conocida como prueba de existencia o teorema de existencia pura), que prueba la existencia de un tipo particular de objeto sin proporcionar un ejemplo. Para evitar confusiones con el concepto más fuerte que se trata a continuación, tal prueba constructiva a veces se denomina prueba efectiva.
Una prueba constructiva también puede referirse al concepto más fuerte de una prueba que es válida según los criterios de la matemática constructiva. El constructivismo es una filosofía matemática que rechaza todos los métodos de prueba que implican la existencia de objetos que no se construyen explícitamente. Esto excluye, en particular, el uso del principio del tercero excluido, el axioma del infinito y el axioma de elección, e induce un significado diferente para alguna terminología (por ejemplo, el término "o" tiene un significado más fuerte en las matemáticas constructivas que en las clásicas).
Algunas demostraciones no constructivas muestran que si cierta proposición es falsa, se produce una contradicción; en consecuencia, la proposición debe ser verdadera (prueba por contradicción). Sin embargo, el principio de explosión (ex falso quodlibet) ha sido aceptado en algunas variedades de matemáticas constructivas, incluido el intuicionismo.
Las pruebas constructivas pueden verse como una definición de los algoritmos matemáticos certificados: esta idea se explora en la interpretación de Brouwer-Heyting-Kolmogorov de la lógica intuicionista, la correspondencia de Curry-Howard entre pruebas y programas, y los sistemas lógicos como la teoría de tipos intuicionista de Per Martin-Löf y el cálculo de construcciones de Thierry Coquand y Gérard Huet.

## Un ejemplo histórico

Hasta finales del siglo XIX, todas las demostraciones matemáticas eran esencialmente constructivas. Las primeras demostraciones no constructivas aparecieron con la teoría de Georg Cantor de conjuntos infinitos y la definición formal de número real.
El primer uso de demostraciones no constructivas para resolver problemas previamente considerados parece ser el teorema de los ceros de Hilbert y el teorema de la base de Hilbert. Desde un punto de vista filosófico, el primero es especialmente interesante, ya que implica la existencia de un objeto bien especificado.
El Nullstellensatz (teorema cero) se puede establecer de la siguiente manera: si $f_{1},\ldots ,f_{k}$ son polinomios en n indeterminados con coeficientes complejos, que no tienen ceros complejos comunes, entonces hay polinomios $g_{1},\ldots ,g_{k}$ tales que
    $f_{1}g_{1}+\ldots +f_{k}g_{k}=1.$
Tal teorema de la existencia no constructiva sorprendió tanto a los matemáticos de la época que uno de ellos, Paul Gordan, escribió: "esto no es matemática, es teología".
Veinticinco años después, Grete Hermann proporcionó un algoritmo para calcular $g_{1},\ldots ,g_{k},$ que no es una prueba constructiva en sentido estricto, ya que utilizó el resultado de Hilbert. Demostró que, si existen $g_{1},\ldots ,g_{k}$, se pueden encontrar con grados menores a $2^{2^{n}}$.
Esto proporciona un algoritmo, ya que el problema se reduce a resolver un sistema de ecuaciones lineales, al considerar como incógnitas el número finito de coeficientes de $g_{i}.$.

## Ejemplos
### Pruebas no constructivas

Primero considérese el teorema de que hay una infinidad de números primos. La demostración dada por Euclides de su teorema es constructiva. Pero una forma común de simplificar la prueba de Euclides postula que, contrariamente a la afirmación del teorema, solo hay un número finito de primos, en cuyo caso hay uno más grande, denotado n. ¡Entonces considérese el número n! + 1 (1 + el producto de los primeros n números). Este número es primo o todos sus factores primos son mayores que n. Sin establecer un número primo específico, esto prueba que existe un primo mayor que n, contrariamente al postulado original.
Ahora, considérese el teorema "existen números irracionales $a$ y $b$ tales que $a^{b}$ es racional". Este teorema se puede probar usando tanto una prueba constructiva como una prueba no constructiva.
La siguiente prueba de 1953 de Dov Jarden se ha utilizado ampliamente como ejemplo de prueba no constructiva desde al menos 1970:
   CURIOSA 339. Una prueba simple de que una potencia de un número irracional elevado a un exponente irracional puede ser racional. ${\sqrt {2}}^{\sqrt {2}}$ es racional o irracional. Si es racional, nuestro enunciado está probado. Si es irracional, $({\sqrt {2}}^{\sqrt {2}})^{\sqrt {2}}=2$ prueba nuestra afirmación.
   Dov Jarden Jerusalén
Con un poco más de detalle:
* Debe recordarse que ${\sqrt {2}}$ es irracional, y que 2 es racional. Considérese el número $q={\sqrt {2}}^{\sqrt {2}}$. O es racional o es irracional.
* Si $q$ es racional, entonces el teorema es verdadero, con $a$ y $b$ siendo ambos ${\sqrt {2}}$.
* Si $q$ es irracional, entonces el teorema es verdadero, siendo $a$ ${\sqrt {2}}^{\sqrt {2}}$ y $b$ ${\sqrt {2}}$, ya que
    $\left({\sqrt {2}}^{\sqrt {2}}\right)^{\sqrt {2}}={\sqrt {2}}^{({\sqrt {2}}\cdot {\sqrt {2}})}={\sqrt {2}}^{2}=2.$
En esencia, esta prueba no es constructiva porque se basa en la declaración "O bien q es racional o bien es irracional", una instancia del principio del tercero excluido, que no es válida dentro de una prueba constructiva. La prueba no constructiva no construye un ejemplo de a y b; simplemente da una serie de posibilidades (en este caso, dos posibilidades mutuamente excluyentes) y muestra que una de ellas, pero no muestra "cuál", debe producir el ejemplo deseado.
Resulta que ${\sqrt {2}}^{\sqrt {2}}$ es irracional debido al teorema de Gelfond-Schneider, pero este hecho es irrelevante para la corrección de la prueba no constructiva.

### Pruebas constructivas

Una prueba "constructiva" del teorema anterior sobre las potencias irracionales de los irracionales daría un ejemplo real, como:
    $a={\sqrt {2}}\,,\quad b=\log _{2}9\,,\quad a^{b}=3\,.$
La raíz cuadrada de dos es irracional y el 3 es racional. $\log _{2}9$ también es irracional: si fuera igual a $m \over n$, entonces, por las propiedades del logaritmo, 9$^n$ sería igual a 2$^m$, pero el primero es impar, y el último es par.
Un ejemplo más sustancial es el teorema del menor de un grafo. Una consecuencia de este teorema es que se puede dibujar un grafo sobre un toro si, y solo si, ninguno de sus menores pertenece a un cierto conjunto finito de "caracterización de grafos prohibidos". Sin embargo, la prueba de la existencia de este conjunto finito no es constructiva y los menores prohibidos no están realmente especificados, y todavía se desconocen.

## Contraejemplos brouwerianos

En matemática constructivista, se puede refutar un enunciado dando un contraejemplo, como en las matemáticas clásicas. Sin embargo, también es posible dar un contraejemplo brouweriano para demostrar que el enunciado no es constructivo. Este tipo de contraejemplo muestra que el enunciado implica algún principio que se sabe que no es constructivo. Si puede demostrarse constructivamente que, si un enunciado implica algún principio que no es demostrable constructivamente, entonces el enunciado mismo no puede demostrarse constructivamente.
Por ejemplo, se puede demostrar que un enunciado en particular implica la ley del tercero excluido. Un ejemplo de un contraejemplo brouweriano de este tipo es el teorema de Diaconescu, que demuestra que el axioma de elección completo no es constructivo en sistemas de teoría de conjuntos constructiva, ya que el axioma de elección implica la ley del tercero excluido en tales sistemas. El campo de las matemáticas inversas constructivas desarrolla aún más esta idea al clasificar varios principios en términos de "cuán no constructivos" son, al mostrar que son equivalentes a varios fragmentos de la ley del tercero excluido.
Brouwer también proporcionó contraejemplos "débiles". Sin embargo, tales contraejemplos no refutan una declaración; solo muestran que, en la actualidad, no se conoce ninguna prueba constructiva de la declaración. Un contraejemplo débil comienza tomando algún problema matemático sin resolver, como la conjetura de Goldbach, que pregunta si todo número natural par mayor que 4 es la suma de dos números primos. Defínase una sucesión a(n) de números racionales como sigue:
    $a(n)={\begin{cases}(1/2)^{n}&{\mbox{ si todo número natural par en el intervalo }}[4,n]{\mbox{ es la suma de dos primos}},\\(1/2)^{k}&{\mbox{ si }}k{\mbox{ es el menor número par natural en el intervalo }}[4,n]{\mbox{ que no es la suma de dos primos}}\end{cases}}$
Para cada n, el valor de a(n) puede determinarse mediante una búsqueda exhaustiva, por lo que a es una secuencia bien definida, constructivamente. Además, como a es un sucesión de Cauchy con tasa de convergencia fija, a converge a algún número real α, según el tratamiento habitual de los números reales en las matemáticas constructivas.
Varios datos sobre el número real α pueden probarse constructivamente. Sin embargo, con base en el diferente significado de las palabras en las matemáticas constructivas, si hay una prueba constructiva de que "α = 0 o α ≠ 0", entonces esto significaría que hay una prueba constructiva de la conjetura de Goldbach (en el primer caso) o una prueba constructiva de que la conjetura de Goldbach es falsa (en el último caso). Debido a que no se conoce tal prueba, la declaración citada tampoco debe tener una prueba constructiva conocida. Sin embargo, es muy posible que la conjetura de Goldbach pueda tener una prueba constructiva (ya que no se sabe si la tiene), en cuyo caso la declaración citada también tendría una prueba constructiva, aunque se desconoce en la actualidad. El principal uso práctico de los contraejemplos débiles es identificar la "dureza" de un problema. Por ejemplo, el contraejemplo que se acaba de mostrar muestra que la declaración citada es "al menos tan difícil de probar" como la conjetura de Goldbach. Los contraejemplos débiles de este tipo a menudo se relacionan con el principio limitado de la omnisciencia.