Definición: un sistema formal axiomático organiza una teoría deduciendo todos sus enunciados de unos axiomas mediante reglas, manipulando símbolos de forma mecánica.

Componentes: (1) alfabeto o símbolos primitivos; (2) reglas de formación (qué secuencias son fórmulas bien formadas); (3) axiomas (fbf admitidas sin demostración); (4) reglas de transformación/inferencia (p.ej. modus ponens). De ellos se derivan los teoremas; una demostración es una secuencia finita de fbf que termina en el teorema.

Sintaxis vs semántica: la sintaxis atiende solo a los símbolos y reglas (el cálculo puro, ⊢), como un juego de signos; la semántica da una interpretación y hace las fórmulas verdaderas o falsas (⊨). Una interpretación que hace verdaderos los axiomas es un modelo. Conclusión: la metalógica estudia la relación entre lo demostrable y lo válido.

Propiedades:

• Consistencia: no se puede derivar una fórmula y su negación (la más importante: de una contradicción se sigue todo).
• Completud: todo enunciado es demostrable o refutable / toda verdad válida es teorema.
• Decidibilidad: existe un algoritmo que decide en pasos finitos si una fórmula es teorema.
• Independencia: ningún axioma se deriva de los demás.

De Euclides a Hilbert: Euclides (Elementos) fue el primer modelo; los axiomas se veían como verdades evidentes. Las geometrías no euclídeas mostraron que son supuestos, no verdades evidentes. Hilbert (Fundamentos de la geometría, 1899) hizo el método plenamente formal: importan las relaciones, no el significado. Conclusión: el cálculo proposicional es consistente, completo y decidible; la lógica de predicados, consistente y completa pero no decidible.

Programa de Hilbert: formalizar toda la matemática y demostrar, con métodos finitistas, su consistencia y completud, para ponerla a salvo de las paradojas (crisis de fundamentos).

Teoremas de Gödel (1931), mediante la aritmetización (numeración de Gödel), que permite al sistema hablar de sí mismo:

• Primero: todo sistema formal consistente que contenga la aritmética es incompleto: hay enunciados verdaderos indemostrables en él.
• Segundo: tal sistema no puede demostrar su propia consistencia.

Consecuencias: el programa de Hilbert (en su forma original) es irrealizable; la verdad desborda la demostrabilidad formal; añadir el enunciado indemostrable como axioma solo da un sistema mayor que vuelve a ser incompleto. Matización: no prueban que «la razón sea impotente», sino que la demostrabilidad formal es más estrecha que la verdad. Debate mente/máquina (Lucas, Penrose).

Alfabeto (símbolos primitivos), reglas de formación (fórmulas bien formadas), axiomas y reglas de transformación o inferencia. De ellos se derivan los teoremas.

Consistente: no deriva una fórmula y su negación. Completo: toda verdad (o su negación) es demostrable. Decidible: hay un algoritmo que determina en pasos finitos si una fórmula es teorema.

Que todo sistema formal consistente y suficientemente potente para contener la aritmética es incompleto: contiene enunciados verdaderos que no pueden demostrarse dentro del sistema.