Teoría de la prueba
La teoría de la demostración o teoría de la prueba es una rama de la lógica matemática que trata a las demostraciones como objetos matemáticos, facilitando su análisis mediante técnicas matemáticas. Las demostraciones suelen presentarse como estructuras de datos inductivamente definidas que se construyen de acuerdo con los axiomas y reglas de inferencia de los sistemas lógicos. En este sentido, la teoría de la demostración se ocupa de la sintaxis, en contraste con la teoría de modelos, que trata con la semántica. Junto con la teoría de modelos, la teoría de conjuntos axiomática y la teoría de la computabilidad, la teoría de la demostración es uno de los «cuatro pilares» de los fundamentos de las matemáticas.[cita requerida]
Dentro de la teoría de la demostración es muy importante distinguir entre las demostraciones «informales» encontradas en la práctica cotidiana de los matemáticos y en los libros comunes sobre matemáticas, de las demostraciones puramente «formales» de la teoría de la demostración formal. Las primeras tienen el objetivo de mostrar rigurosamente un resultado matemático de manera clara, pero al mismo tiempo intuitiva e inteligible, las segundas de estas demostraciones son como una especie de esquemas de alto-nivel escritos en lenguaje formal, que en principio, pueden permitir a un experto o un lógico construir una demostración puramente formal del mismo resultado, dado el suficiente tiempo y paciencia. Para la mayoría de los matemáticos, escribir una demostración completamente formal es un gasto de tiempo innecesario como para ser práctica común.
Las demostraciones formales pueden ser construidas con ayuda de ordenadores mediante métodos de demostración de teoremas interactivos u otras técnicas. Es significativo, que estas demostraciones puramente formales basadas en la manipulación de signos pueden ser verificadas automáticamente, también por ordenador. Verificar una demostración puramente formal es simple, mientras que encontrar demostraciones es generalmente mucho más difícil. Una demostración informal en un artículo matemático, por el contrario, requiere semanas de revisión por pares para ser verificada, y frecuentemente puede contener errores que pasen inadvertidos incluso para matemáticos profesionales en temas de investigación suficientemente complejos.
La teoría de la demostración formal se ocupa de las propiedades de los sistemas deductivos, su complejidad, el poder expresivo de dichos sistemas y está íntimamente conectada a la lógica matemática, la teoría de modelos y la fundamentación de las matemáticas. Por el contrario el desarrollo de demostraciones informales es un terreno altamente creativo y si bien existen familias enteras de esquemas de demostración en diferentes áreas, son un ejercicio básicamente humano en el que no existen algoritmos generales para construir demostraciones.
La teoría de la demostración formal comenzó con la crisis sobre los fundamentos de las matemáticas de las primeras décadas del siglo XX. A principios de ese siglo, y como reacción a la explosión del conocimiento matemático, comenzaron esfuerzos para proporcionar al creciente cuerpo de conocimientos un fundamento formal firme. Si bien en las aplicaciones de las matemáticas esta fundamentación no era importante, en otras áreas de la matemática, como la filosofía de la matemática se estaba haciendo necesaria una clarificación de los conceptos fundamentales, ya que estaban apareciendo problemas lógicos como los identificados por B. Russell y A. N. Whitehead en el trabajo de Gottlob Frege y otras personas que habían tratado de fundamentar sólidamente las matemáticas.
Entre los problemas de fundamentación por ejemplo estaba el uso de los "infinitesimales" que vagamente relacionados con algo "infinitamente pequeño" (lo cual era una noción demasiado imprecisa). La eliminiación de los infinitesimales mediante el uso de límites significó un gran progreso para establecer las matemáticas existentes sobre un fundamento más firme y claro. Otro problema sin fudamentar era lo "infinitamente grande". Las investigaciones sobre unicidad de representación de Georg Cantor forzaron a este matemático a desarrollar una nueva teoría de lo infinitamente grande. Uno de los puntos centrales de la teoría de Cantor era la posibilidad de considerar incluso una colección no finita de objetos y formar un "objeto matemático" con esta colección. Estos "objetos" fueron denominados por Cantor en alemán como Mengen y el término se tradujo como 'conjunto' en español. Debido a eso Cantor denominó a su teoría Mengenlehre que es el origen de la teoría de conjuntos. La posibilidad de formar conjuntos sin restricciones, producía ciertas contradicciones o antinomias. Un ejemplo notable de estas antinomias es la paradoja de Russell sobre el conjunto de conjuntos que no son miembros de sí mismos. Así si se pudiera definir el conjunto:
sería una contradicción, ya que por construcción se tendría:
Estas paradojas y probablemente también el hecho aparentemente paradójico de que el axioma de elección ofrecía la posibilidad de que cualquier conjunto pudiera ser un conjunto bien ordenado, crearon la sensación de incertidumbre entre la comunidad matemática. Hermann Weyl en su artículo "Über die neue Grundlagenkrise der Mathematik" apuntó que la circularidad de las definiciones causaban paradojas y antinomias también en la teoría de conjuntos que se usaba en análisis matemático. Este matemático introdujo el término "nueva crisis de fundamentos" en la discusión de la época. En su libro Das Kontinuum ya había propuesto desarrollar matemáticas libres de definiciones circulares.
Las diversas paradojas surgidas en la teoría de conjuntos y los problemas de fundamentación del concepto de infinito, llevaron a la llamada crisis fundacional de las matemáticas a principios del siglo XX. Frente a este debate entre los matemáticos, David Hilbert y algunos de sus colaboradores consideraron elaborar un programa de formalización completo, para demostrar la consistencia de numerosas ramas de la matemática. Esta propuesta de formalización se conoció como programa de Hilbert.
Este enfoque formalista pretendía axiomatizar de manera explícita los supuestos usados en diversas ramas de las matemáticas mediante un conjunto de axiomas expresables en un lenguaje formal bien definido y de manera que se pudiera probar la consistencia de las matemáticas así formalizadas. Hilbert y muchos otros matemáticos tenían confianza en que este programa tendría éxito para cualquier área de las matemáticas y siempre sería posible construir un conjunto de reglas que permitieran demostrar en un número finito de pasos si una proposición era una proposición válida (Entscheidungsproblem). Sin embargo, K. Gödel pudo demostrar en 1931 que este enfoque tenía limitaciones esenciales, incluso en un sistema tan central para las matemáticas como era la aritmética de los números naturales.
El teorema de incompletitud de Gödel establece que ninguna teoría consistente, con un número finito de axiomas recursivamente enumerable (en un lenguaje por lo menos tan potente como la aritmética), puede incluir todos las proposiciones verdaderas. Sin embargo, la aritmética es una teoría completable añadiendo un conjunto de axiomas infinito y no recursivo. En otras palabras el teorema de Gödel solo establece que si es un tipo de teoría aritmética:
O equivalentemente:
En 1934 Gerhard Gentzen introdujo las nociones básicas que llevaron al desarrollo de la moderna teoría de la demostración.