teoría de la prueba
La teoría de la prueba es una rama principal [1] de la lógica matemática que representa las pruebas como objetos matemáticos formales , lo que facilita su análisis mediante técnicas matemáticas. Las pruebas suelen presentarse como estructuras de datos definidas inductivamente , como listas sencillas , listas en cajas o árboles , que se construyen de acuerdo con los axiomas y las reglas de inferencia del sistema lógico. En consecuencia, la teoría de la prueba es de naturaleza sintáctica , en contraste con la teoría de modelos , que es de naturaleza semántica .
Algunas de las principales áreas de la teoría de la prueba incluyen la teoría de la prueba estructural , el análisis ordinal , la lógica de demostrabilidad , las matemáticas inversas , la extracción de pruebas , la prueba automatizada de teoremas y la complejidad de la prueba . Gran parte de la investigación también se centra en aplicaciones en informática, lingüística y filosofía.
Aunque la formalización de la lógica avanzó mucho con el trabajo de figuras como Gottlob Frege , Giuseppe Peano , Bertrand Russell y Richard Dedekind , la historia de la teoría de la demostración moderna a menudo se considera establecida por David Hilbert , quien inició lo que se llama la teoría de Hilbert. programa en los Fundamentos de las Matemáticas . La idea central de este programa era que si pudiéramos dar finitarypruebas de consistencia para todas las teorías formales sofisticadas que necesitan los matemáticos, entonces podríamos fundamentar estas teorías por medio de un argumento metamatemático, que muestra que todas sus afirmaciones puramente universales (más técnicamente, sus oraciones demostrables ) son finitamente verdaderas; una vez así fundamentados, no nos importa el significado no finito de sus teoremas existenciales, considerándolos como estipulaciones pseudo-significativas de la existencia de entidades ideales.
El fracaso del programa fue inducido por los teoremas de incompletitud de Kurt Gödel , que mostraban que cualquier teoría ω-consistente que sea lo suficientemente fuerte para expresar ciertas verdades aritméticas simples, no puede probar su propia consistencia, que en la formulación de Gödel es una oración. Sin embargo, surgieron versiones modificadas del programa de Hilbert y se han realizado investigaciones sobre temas relacionados. Esto ha llevado, en particular, a:
Paralelamente al auge y la caída del programa de Hilbert, se estaban asentando los cimientos de la teoría de la prueba estructural . Jan Łukasiewicz sugirió en 1926 que se podrían mejorar los sistemas de Hilbert como base para la presentación axiomática de la lógica si se permitiera extraer conclusiones a partir de suposiciones en las reglas de inferencia de la lógica. En respuesta a esto, Stanisław Jaśkowski (1929) y Gerhard Gentzen (1934) proporcionaron de forma independiente tales sistemas, llamados cálculos de deducción natural , con el enfoque de Gentzen introduciendo la idea de simetría entre los motivos para afirmar proposiciones, expresados en reglas de introducción ., y las consecuencias de aceptar proposiciones en las reglas de eliminación , una idea que ha demostrado ser muy importante en la teoría de la demostración. [2] Gentzen (1934) introdujo además la idea del cálculo secuente , un cálculo avanzado con un espíritu similar que expresaba mejor la dualidad de los conectivos lógicos, [3] y siguió haciendo avances fundamentales en la formalización de la lógica intuicionista, y proporcionar la primera prueba combinatoria de la consistencia de la aritmética de Peano . Juntos, la presentación de la deducción natural y el cálculo secuencial introdujeron la idea fundamental de la teoría analítica de prueba a prueba.
La teoría de la prueba estructural es la subdisciplina de la teoría de la prueba que estudia los aspectos específicos de los cálculos de prueba . Los tres estilos más conocidos de cálculos de prueba son: