El programa de Hilbert.

En matemáticas, el programa de Hilbert, formulado por el matemático alemán David Hilbert a principios de la década de 1920, fue una propuesta de solución a la crisis fundamental de las matemáticas, cuando los primeros intentos de aclarar los fundamentos de las matemáticas Se descubrió que las matemáticas adolecían de paradojas e inconsistencias. Como solución, Hilbert propuso basar todas las teorías existentes en un conjunto finito y completo de axiomas y proporcionar una prueba de que estos axiomas eran consistentes. Hilbert propuso que la coherencia de sistemas más complicados, como el análisis real, podría demostrarse en términos de sistemas más simples. En última instancia, la coherencia de todas las matemáticas podría reducirse a la aritmética básica.

Los teoremas de incompletitud de Gödel, publicados en 1931, demostraron que el programa de Hilbert era inalcanzable para áreas clave de las matemáticas. En su primer teorema, Gödel demostró que cualquier sistema consistente con un conjunto computable de axiomas que sea capaz de expresar la aritmética nunca puede ser completo: es posible construir un enunciado que pueda demostrarse que es verdadero, pero que no puede derivarse de la reglas formales del sistema. En su segundo teorema, demostró que tal sistema no podía probar su propia consistencia, por lo que ciertamente no puede usarse para probar con certeza la consistencia de algo más fuerte. Esto refutó la suposición de Hilbert de que un sistema finitista podría usarse para probar la consistencia de sí mismo y, por lo tanto, no podría probar todo lo demás.

Declaración del programa de Hilbert

El objetivo principal del programa de Hilbert era proporcionar bases seguras para todas las matemáticas. En particular, esto debería incluir:

• Una formulación de todas las matemáticas; en otras palabras todas las declaraciones matemáticas deben ser escritas en un lenguaje formal preciso, y manipuladas de acuerdo a reglas bien definidas.
• Completeness: una prueba de que todas las verdaderas declaraciones matemáticas pueden ser probadas en el formalismo.
• Consistencia: una prueba de que no se puede obtener contradicción en el formalismo de las matemáticas. Esta prueba de consistencia debe utilizar preferentemente sólo el razonamiento "finitístico" sobre objetos matemáticos finitos.
• Conservación: una prueba de que cualquier resultado sobre "objetos reales" obtenido utilizando el razonamiento sobre "objetos ideales" (como conjuntos incontables) puede ser probado sin usar objetos ideales.
• Decidibilidad: debe haber un algoritmo para decidir la verdad o falsedad de cualquier declaración matemática.

Teoremas de incompletitud de Gödel

Kurt Gödel demostró que la mayoría de los objetivos del programa de Hilbert eran imposibles de alcanzar, al menos si se interpretaban de la manera más obvia. El segundo teorema de incompletitud de Gödel muestra que cualquier teoría consistente lo suficientemente poderosa como para codificar la suma y multiplicación de números enteros no puede probar su propia consistencia. Esto presenta un desafío para el programa de Hilbert:

• No es posible formalizar Todos matemáticas verdaderas declaraciones dentro de un sistema formal, como cualquier intento de tal formalismo omitirá algunas verdaderas declaraciones matemáticas. No hay una extensión completa y consistente de hasta Peano aritmética basada en un conjunto repetidamente enumerable de axiomas.
• Una teoría como Peano aritmética no puede incluso demostrar su propia consistencia, por lo que un subconjunto "finitista" restringido de ella ciertamente no puede demostrar la consistencia de teorías más poderosas como la teoría de conjuntos.
• No hay algoritmo para decidir la verdad (o probabilidad) de las declaraciones en cualquier extensión consistente de Peano aritmética. Strictly speaking, this negative solution to the Entscheidungsproblem appeared a few years after Gödel's theorem, because at the time the notion of an algoritmo had not been accurate defined.

El programa de Hilbert después de Gödel

Muchas líneas actuales de investigación en lógica matemática, como la teoría de la prueba y las matemáticas inversas, pueden verse como continuaciones naturales del programa original de Hilbert. Gran parte se puede salvar cambiando ligeramente sus objetivos (Zach 2005), y con las siguientes modificaciones parte se completó con éxito:

• Aunque no es posible formalizar Todos matemáticas, es posible formalizar esencialmente todas las matemáticas que cualquiera utiliza. En particular Zermelo–Fraenkel set theory, combinado con la lógica de primer orden, da un formalismo satisfactorio y generalmente aceptado para casi todas las matemáticas actuales.
• Aunque no es posible probar la integridad de los sistemas que pueden expresar al menos el aritmético Peano (o, más generalmente, que tienen un conjunto computable de axiomas), es posible probar formas de integridad para muchos otros sistemas interesantes. Un ejemplo de una teoría no-trivial para la cual se ha probado la integridad es la teoría de campos algebraicamente cerrados de características dadas.
• La cuestión de si hay pruebas de consistencia finitarias de teorías fuertes es difícil de responder, principalmente porque no hay una definición generalmente aceptada de una "prueba definitiva". La mayoría de los matemáticos en la teoría de la prueba parecen considerar las matemáticas finitarias como contenidas en Peano aritmética, y en este caso no es posible dar pruebas finitarias de teorías razonablemente fuertes. Por otra parte, el propio Gödel sugirió la posibilidad de dar pruebas de consistencia finitarias utilizando métodos finitarios que no pueden formalizarse en la aritmética de Peano, por lo que parece haber tenido una visión más liberal de lo que podrían permitirse los métodos finitarios. Pocos años después, Gentzen dio una prueba de consistencia para Peano aritmética. La única parte de esta prueba que no era claramente finita fue una cierta inducción transfinita hasta el ε ordinal₀. Si esta inducción transfinita es aceptada como un método finitario, entonces se puede afirmar que hay una prueba finitaria de la consistencia de Peano aritmética. Los subconjuntos más poderosos de segunda orden aritmética han recibido pruebas de consistencia de Gaisi Takeuti y otros, y uno puede discutir de nuevo sobre exactamente lo finitario o constructivo que son estas pruebas. (Las teorías que han sido probadas consistentes por estos métodos son bastante fuertes, e incluyen la mayoría de las matemáticas "ordinarias".)
• Aunque no hay algoritmo para decidir la verdad de las declaraciones en Peano aritmética, hay muchas teorías interesantes y no-triviales para las que se han encontrado tales algoritmos. Por ejemplo, Tarski encontró un algoritmo que puede decidir la verdad de cualquier declaración en la geometría analítica (más precisamente, demostró que la teoría de los campos cerrados reales es decidable). Dado el axioma Cantor-Dedekind, este algoritmo se puede considerar como un algoritmo para decidir la verdad de cualquier declaración en la geometría euclidiana. Esto es sustancial ya que pocas personas considerarían la geometría euclidiana una teoría trivial.