Teoría de la Demostración
La teoría de la demostración estudia las pruebas formales como objetos matemáticos en sí mismos, analizando su estructura, transformaciones y la fuerza de las teorías que las producen.
Definition
La teoría de la demostración es la rama de la lógica matemática que trata las pruebas en sistemas formales como objetos combinatorios finitos, estudiando cómo pueden ser transformadas y normalizadas y qué revela su existencia sobre la consistencia y la fuerza de las teorías subyacentes.
Scope
Esta área abarca los cálculos formales como la deducción natural y el cálculo de secuentes, los teoremas de eliminación de cortes y de normalización, los teoremas de incompletitud de Goedel, la medición de la fuerza de las teorías mediante el análisis ordinal, y el contenido constructivo y computacional de las pruebas revelado por la correspondencia entre pruebas y programas.
Sub-topics
Core questions
- ¿Cómo se pueden representar y manipular las pruebas formales como objetos combinatorios?
- ¿Qué rodeos en las pruebas pueden eliminarse sistemáticamente y qué revela eso?
- ¿Cuáles son los límites inherentes a lo que una teoría formal puede probar sobre sí misma?
- ¿Cómo se puede medir con precisión la fuerza de una teoría?
Key theories
- Teorema de eliminación de cortes
- Gentzen demostró que cualquier prueba en el cálculo de secuentes puede transformarse en una sin la regla de corte, produciendo pruebas con la propiedad de la subfórmula y resultados de consistencia directos.
- Teoremas de incompletitud de Goedel
- Cualquier teoría formal consistente lo suficientemente fuerte como para expresar la aritmética contiene oraciones verdaderas que no puede probar y no puede probar su propia consistencia, estableciendo límites fundamentales a la formalización.
- Correspondencia de Curry-Howard
- Las pruebas en deducción natural corresponden a términos de un cálculo lambda tipado y la normalización de pruebas corresponde a la computación, vinculando la teoría de la demostración con la teoría de los lenguajes de programación.
Clinical relevance
La teoría de la demostración subyace al análisis de la consistencia y el contenido constructivo en matemáticas y proporciona la base teórica para la teoría de tipos, la programación funcional y los asistentes de prueba automatizados, donde las pruebas funcionan como programas verificables.
History
La teoría de la demostración fue fundada por Hilbert como parte de su programa para asegurar las matemáticas mediante pruebas de consistencia finitas. Los teoremas de incompletitud de Goedel de 1931 mostraron que el programa original no podía tener éxito por completo, y la eliminación de cortes de Gentzen y la prueba de consistencia para la aritmética mediante inducción transfinita redirigieron el campo hacia el análisis ordinal y, posteriormente, el paradigma de las pruebas como programas.
Key figures
- David Hilbert
- Gerhard Gentzen
- Kurt Goedel
- Jean-Yves Girard
Related topics
Seminal works
- troelstra2000
- takeuti1987
- girard1989
Frequently asked questions
- ¿En qué se diferencia la teoría de la demostración de la teoría de modelos?
- La teoría de modelos estudia las estructuras y la verdad de las oraciones en ellas, desde una perspectiva semántica, mientras que la teoría de la demostración estudia las derivaciones formales y sus transformaciones sintácticas. El teorema de completitud de Goedel vincula ambas, pero sus métodos y preguntas son distintos.
- ¿Qué es el programa de Hilbert?
- Fue la propuesta de probar la consistencia de todas las matemáticas utilizando solo razonamientos finitos e incontrovertibles. El segundo teorema de incompletitud de Goedel demostró que ninguna teoría suficientemente fuerte puede probar su propia consistencia, por lo que el programa no puede llevarse a cabo en su forma original, aunque las versiones modificadas siguen siendo influyentes.