| Autor(es) | David Hilbert (1862–1943); Paul Bernays (1888–1977); Wilhelm Ackermann (1896–1962) |
| Fecha / periodo | 1921–1939 · Siglo XX · Alemania (Gotinga) |
| Tipo | Formal |
| Deriva de | Lógica intuicionista · Teoría de tipos de Principia Mathematica · Lógica de primer orden clásica |
| Derivan de ella | Cálculo lambda · Semántica tarskiana · Sintaxis lógica y principio de tolerancia · Deducción natural y cálculo de secuentes · Lógica de la demostrabilidad |
| Tres leyes | Identidad: ✓ (axiomas de la igualdad en el cálculo formal) · No contradicción: ✓ (probar la consistencia es el objetivo del programa) · Tercio excluso: ✓ en la matemática «ideal»; en la finitaria solo para enunciados decidibles |
Tras las paradojas de la teoría de conjuntos y la crítica de Brouwer y Weyl, Hilbert quiso salvar la matemática clásica sin recortarla. Su gesto fue doble. Primero, formalizar por completo las teorías matemáticas, de modo que las demostraciones se conviertan en objetos finitos, sucesiones de fórmulas manipulables según reglas. Segundo, estudiar esos objetos con una matemática nueva, la metamatemática o teoría de la demostración, que solo usa razonamientos «finitarios», aceptables incluso para el intuicionista. Si con ellos se prueba que ninguna derivación termina en \(0 \neq 0\), el uso del infinito queda justificado como instrumento. Nadie, decía Hilbert en 1925, nos expulsará del paraíso que Cantor creó.
Distinciones básicas («Neubegründung der Mathematik», 1922; «Über das Unendliche», 1926).
El cálculo lógico. Hilbert y Ackermann (Grundzüge der theoretischen Logik, 1928) usan para la lógica proposicional los axiomas de Principia:
El libro plantea como problemas abiertos la completitud del cálculo de primer orden (resuelta por Gödel en 1929) y el Entscheidungsproblem: hallar un procedimiento que decida si una fórmula es universalmente válida.
El cálculo ε. Hilbert introduce un término \(\varepsilon x\, A(x)\), «un objeto que satisface \(A\), si lo hay», con el axioma crítico
Los cuantificadores se definen: \(\exists x\, A(x) :\leftrightarrow A(\varepsilon x\, A(x))\) y \(\forall x\, A(x) :\leftrightarrow A(\varepsilon x\, \neg A(x))\). El método de sustitución ε (Ackermann, 1924; corregido en 1940) busca eliminar los términos ε de una prueba asignándoles valores numéricos por ensayo y error, hasta obtener una prueba de un enunciado sin cuantificadores, verificable finitariamente. Los teoremas ε primero y segundo (Hilbert y Bernays, 1939) muestran que el cálculo ε es conservativo sobre la lógica de predicados.
Resultados. Ackermann (1924) y von Neumann (1927) probaron la consistencia de fragmentos de la aritmética. Gödel (1931) mostró que ningún sistema consistente y recursivamente axiomatizado que contenga la aritmética prueba su propia consistencia, lo que impide el programa en su forma original, pues los métodos finitarios son formalizables en la aritmética. En Grundlagen der Mathematik, vol. II (1939), Hilbert y Bernays dieron la primera prueba detallada del segundo teorema de incompletitud, con las «condiciones de derivabilidad» que debe cumplir el predicado de prueba. Gentzen (1936) probó la consistencia de la aritmética de Peano usando inducción transfinita hasta el ordinal \(\varepsilon_0\): un método no finitario en sentido estricto, pero más débil que la aritmética entera.
Qué se conserva. La lógica de los sistemas formalizados es la clásica completa. La restricción constructiva afecta solo al metanivel: el tercio excluso para cuantificadores infinitos no se usa en las pruebas de consistencia.
El programa es en parte reacción. Brouwer había rechazado el tercio excluso en dominios infinitos y Weyl, en 1921, se había pasado a su bando; Hilbert respondió que quitar al matemático el tercio excluso sería como prohibir al astrónomo el telescopio. Pero la metamatemática adopta, para sí, un punto de vista finitario próximo al constructivismo que combate. De Principia Mathematica toma el aparato formal, incluidos los axiomas proposicionales, sin su reducción logicista: para Hilbert la matemática no se reduce a la lógica, necesita objetos extralógicos, los signos. Su suelo son los cálculos lógicos que él y Bernays elaboran desde 1917, de donde nace la lógica de primer orden como sistema separado.
La descendencia es amplia. Church usó el cálculo λ para responder negativamente en 1936 al Entscheidungsproblem. Tarski toma el término y el programa de la metamatemática y lo extiende a conceptos semánticos como verdad y consecuencia. Carnap, en la Sintaxis lógica, generaliza la metamatemática a lenguajes cualesquiera. Gentzen trabaja dentro del programa: el cálculo de secuentes y la prueba de consistencia de 1936 son sus frutos. Las condiciones de derivabilidad de 1939, reformuladas por Löb (1955), están en el origen de la lógica de la demostrabilidad GL.
Es el polo opuesto al intuicionismo en la «crisis de fundamentos» de los años veinte, con episodios de hostilidad personal, como la expulsión de Brouwer del consejo de los Mathematische Annalen en 1928. Su fracaso parcial tras Gödel fue enormemente fecundo: creó la teoría de la demostración, la noción precisa de algoritmo y el estudio de la fuerza de los sistemas formales. Para la pregunta «¿una lógica o muchas?» ofrece una posición singular. Hay dos niveles con lógicas distintas: la clásica, como instrumento ideal, y una finitaria, casi constructiva, como garantía. La lógica clásica no se justifica por su verdad, sino por su consistencia probada desde otra lógica más segura.