# Programa de Hilbert

En matemáticas, el Programa de Hilbert, formulado por el matemático alemán David Hilbert en la década de 1920, fue una solución propuesta ante la crisis fundacional de las matemáticas, en épocas en que en los primeros intentos por clarificar los fundamentos de la matemática contenían paradojas e inconsistencias. Como solución, Hilbert propuso basarse en todas las teorías existentes para formar un conjunto de axiomas finito y completo, y proveer prueba de que esos axiomas eran consistentes. El alemán propuso que la consistencia de sistemas más complicados, como el análisis real, podrían ser probados en términos de sistemas más simples. Últimamente, la consistencia de toda la matemática puede ser reducida a aritmética básica.
No obstante los teoremas de incompletitud de Gödel, formulados por el matemático austrohúngaro Kurt Gödel, demostraron en 1931 que el programa de Hilbert era inalcanzable. En su primer teorema mostró que cualquier sistema consistente con un conjunto computable de axiomas, capaz de expresar aritmética nunca puede ser completo: es posible construir una afirmación que puede ser demostrada como verdadera, pero no puede ser derivada de las reglas formales del sistema. En su segundo teorema, Gödel mostró que un sistema como aquel no podría probar su propia consistencia, de modo que tampoco puede ser usado para probar la consistencia de nada más fuerte. Esto contradijo la suposición de Hilbert de que un sistema finitista podía ser usado para probar la consistencia de una teoría más fuerte.

## Afirmación del programa de Hilbert

El principal objetivo del programa de Hilbert era dotar de fundamentos para todas las matemáticas. En particular esto debía incluir:
* Una formalización de todas las matemáticas. En otras palabras, todas las afirmaciones matemáticas deberían ser escritas en un lenguaje preciso y formal, y manipuladas de acuerdo a reglas bien definidas. (ver Formalismo matemático)
* Integridad: una prueba de que todas las afirmaciones matemáticas pueden ser probadas en el formalismo.
* Consistencia: una prueba de que ninguna contradicción puede ser obtenida en el formalismo de las matemáticas. Esta prueba de consistencia debería preferentemente usar solo razonamiento finitista acerca de los objetos matemáticos finitos.
* Conservación: una prueba de que ningún resultado acerca de "objetos reales" obtenida usando razonamiento sobre "objetos ideales" (como los conjuntos incontables) puede ser probado sin usar objetos ideales.
* Decidibilidad: debería haber un algoritmo para decidir la verdad o falsedad de cualquier afirmación matemática.

## Los teoremas de incompletitud de Gödel

Gödel demostró que la mayoría de los objetivos del programa de Hilbert eran imposibles de alcanzar, por lo menos si eran interpretados en la forma más obvia. Su segundo teorema de incompletitud afirmó que cualquier teoría lo suficientemente consistente como para cifrar la suma y multiplicación de enteros, no puede probar su propia consistencia. Esto acaba con la mayor parte del programa de Hilbert:
* No es posible formalizar toda la matemática, ya que cualquier intento dentro del formalismo omitirá ciertas afirmaciones matemáticas verdaderas.
* Una simple consecuencia del teorema de incompletitud de Gödel es que no hay una extensión completa consistente incluso de la aritmética de Peano con un conjunto recursivamente enumerable de axiomas, por lo tanto en particular la mayoría de las teorías matemáticas interesantes no están completas.
* Una teoría como la de axiomas de Peano no puede siquiera probar su propia consistencia, de modo que un subconjunto limitado finitista del mismo seguramente no puede probar la consistencia de teorías más poderosas, como la teoría de conjuntos.
* No existe algoritmo para decidir la veracidad (o probabilidad) de afirmaciones en ninguna extensión consistente del teorema de Peano. (Estrictamente hablando, este resultado apareció unos pocos años después de los teoremas de Gödel, ya que por esa época la definición de un algoritmo no era exacta.)

## El programa de Hilbert después de Gödel

Muchas de las líneas actuales de investigación sobre lógica matemática, teoría de la demostración y matemática inversa pueden ser vistas como continuaciones naturales del programa original de Hilbert. Gran parte de él puede ser salvado cambiando sus objetivos ligeramente, y con las siguientes modificaciones cierta parte pudo ser exitosamente completada:
* Si bien no es posible formalizar toda la matemática, sí es posible formalizar esencialmente toda matemática que cualquiera usa. En particular la teoría de conjuntos de Zermelo y Fraenkel, combinada con lógica de primer orden, resulta en un formalismo satisfactorio y generalmente aceptado para, esencialmente, toda matemática actual.
* Aunque no es posible probar la integridad en sistemas tan poderosos al menos como la aritmética de Peano (al menos, si tienen un conjunto computable de axiomas), es posible probar formas de integridad en muchos sistemas interesantes. El primer gran éxito fue del mismo Gödel (antes había probado los teoremas de incompletitud), quien probó el teorema de completitud para lógica de primer orden, demostrando que cualquier consecuencia lógica de una serie de axiomas es demostrable. Un ejemplo de una teoría no trivial para la cual la completitud ha sido probada es la teoría de los cuerpos algebraicamente cerrados de una característica dada.
* La pregunta de si hay pruebas de consistencia finitistas para teorías fuertes, es difícil de responder. Principalmente porque no hay, generalmente, una definición convenida para la "prueba finitista". La mayor parte de los matemáticos en la teoría de la demostración parecen considerar a las matemáticas finitistas como contenidas dentro de la aritmética de Peano, y en este caso no es posible dar pruebas finitistas de teorías razonablemente fuertes. Por otro lado, el mismo Gödel sugirió la posibilidad de dar pruebas de consistencia finitistas usando métodos del mismo estilo, que no pueden ser formalizados en la aritmética de Peano, por lo tanto él parece haber tenido una mirada más liberal acerca de qué métodos finitistas podrían ser permitidos. Pocos años después, Gentzen dio una prueba de consistencia para los axiomas de Peano, cuya única parte que no era claramente finitista era una cierta inducción transfinita hasta el ordinal ε$_0$. Si esta inducción transfinita es aceptada como método finitista, entonces se puede asegurar que existe prueba finitista de la consistencia de la aritmética de Peano.
* Aunque no hay algoritmo para decidir la veracidad de las afirmaciones de los postulados de Peano, hay muchas teorías interesantes y no triviales para las cuales dichos algoritmos sí han sido encontrados. Por ejemplo, el matemático polaco Alfred Tarski encontró un algoritmo que puede decidir la veracidad de cualquier afirmación dentro de la geometría analítica (más precisamente, Tarski probó que la teoría de cuerpos algebraicamente cerrados es decidible). Dado el axioma Cantor-Dedekind, este algoritmo puede ser visto como un algoritmo para decidir la veracidad de cualquier afirmación dentro de la geometría euclidiana. Esto es importante ya que pocas personas considerarían a la geometría euclidiana una teoría trivial.