En matemáticas , una prueba constructiva es un método de prueba que demuestra 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 sigue, tal prueba constructiva a veces se llama prueba efectiva .
Una prueba constructiva también puede referirse al concepto más fuerte de una prueba que es válida en las matemáticas constructivas .El constructivismo es una filosofía matemática que rechaza todos los métodos de prueba que implican la existencia de objetos que no están explícitamente construidos. Esto excluye, en particular, el uso de la ley 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 términos constructivos). matemáticas que en las clásicas). [1]
Algunas pruebas 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 la definición de algoritmos matemáticos certificados : esta idea se explora en la interpretación de la lógica constructiva de Brouwer-Heyting-Kolmogorov , la correspondencia de Curry-Howard entre pruebas y programas, y sistemas lógicos como el tipo intuicionista de Per Martin-Löf . y el cálculo de construcciones de Thierry Coquand y Gérard Huet .
Hasta finales del siglo XIX, todas las demostraciones matemáticas eran esencialmente constructivas. Las primeras construcciones no constructivas aparecieron con la teoría de los conjuntos infinitos de Georg Cantor y la definición formal de los números reales .
El primer uso de pruebas no constructivas para resolver problemas previamente considerados parece ser el Nullstellensatz 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.