Teoría de la demostración

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"[1] 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:

${\displaystyle R:=\{x|x\notin x\}}$

sería una contradicción, ya que por construcción se tendría:

${\displaystyle R\in R\Leftrightarrow R\notin R}$

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"[2] 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.[3]

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 ${\displaystyle \scriptstyle T({\mathcal {A}})}$ es un tipo de teoría aritmética:

${\displaystyle (T({\mathcal {A}})\ {\mbox{recursiva}}\land T({\mathcal {A}})\ {\mbox{consistente}})\Rightarrow T({\mathcal {A}})\ {\mbox{incompleta}}}$

O equivalentemente:

${\displaystyle (T({\mathcal {A}})\ {\mbox{completa}}\land T({\mathcal {A}})\ {\mbox{consistente}})\Rightarrow \neg (T({\mathcal {A}})\ {\mbox{recursiva}})}$

En 1934 Gerhard Gentzen introdujo las nociones básicas que llevaron al desarrollo de la moderna teoría de la demostración.

• Pohlers, Wolfram (2009). Proof Theory: The first step into impredicatibility. Berlín: Springer-Verlag. pp. 17-42. ISBN 978-3-540-69319-2.