Demostraciones
- Profesor, ¿cuándo llegamos a la autorreferencia?
- Paciencia, ya falta poco.
En el capítulo anterior dijimos que el Programa de Hilbert proponía dar axiomas para la Aritmética y que estos axiomas (así como las reglas de inferencia, que son las que nos dicen qué conclusiones podemos obtener a partir de ciertas hipótesis) debían ser elegidos de modo tal que la corrección de cualquier demostración basada en ellos pudiera ser verificada (desde el nivel de la Metamatemática) mecánicamente en una cantidad finita de pasos (es decir, debía ser posible programar una computadora para que verificara si una demostración es válida o no).
En concreto, las demostraciones que contemplaba el Programa de Hilbert como válidas debían ser traducibles a una sucesión finita de enunciados tales que cada uno de estos, o bien era un axioma, o bien podía deducirse de enunciados previamente ubicados en la sucesión por aplicación de ciertas reglas de inferencia específicas. (1)
Esta idea impone tres características a la formalización de la Aritmética. La primera es que sus enunciados deben poder traducirse a un lenguaje con símbolos bien definidos (requisito necesario para que haya un algoritmo que trabaje sobre esos enunciados -a nivel metamatemático-).
A los efectos de esta serie de entradas, el lenguaje que usaremos constará de los símbolos "+" y ".", la constante 1, a los que agregaremos paréntesis y símbolos para las operaciones lógicas. El lenguaje tendrá también variables, x, y, z,... que sólo podrán representar números naturales (nunca expresarán funciones, conjuntos u otros objetos (2)).
Observemos que la Metamatemática trabaja solamente a nivel sintáctico, por lo que la expresión:
(1 + 1).(1 + 1) = 1 + 1 + 1 + 1
será, a nivel metamatemático, diferente de la expresión:
1 + 1 + 1 + 1 = (1 + 1).(1 + 1)
porque, aunque ambas tienen los mismos símbolos, estos están escritos en diferente orden.
Asumamos que, para su tratamiento metamatemático, todos los enunciados han sido traducidos a este lenguaje formal. Asumamos también que tenemos una secuencia de enunciados y que queremos escribir un programa que verifique si esa secuencia es, o no, una demostración válida. El programa "tomará" entonces un enunciado de la secuencia y deberá verificar si se trata, o no, de un axioma.
La segunda característica es, entonces, que exista un algoritmo que verifique en una cantidad finita de pasos si un enunciado es, o no, un axioma.
Continuando con el proceso que debería seguir ese programa, si un enunciado no es un axioma, el programa debe se capaz de verificar si el enunciado puede deducirse de enunciados anteriores en la sucesión. La tercera característica es, entonces, que la relación "Q se deduce de las hipótesis H1, H2, H3,..." debe ser verificable algorítmicamente.
En realidad, podemos reducirnos a tomar una única regla de inferencia: la llamada Regla del Modus Ponens, que dice que de P y de P ---> Q se deduce Q. (La regla debe ser entendida a nivel sintáctico, sin apelación a posible significados.)
Diremos que una propiedad es recursiva si es verificable algorítmicamente. Podemos decir entonces que el sistema de axiomas y sus reglas de inferencia deben ser ambos recursivos.
Continuará...
Notas:
(1) Éste es el proceso de verificación metamatemática de las demostraciopnes que proponía el Programa de Hilbert. Desde luego, no es el proceso por el que los matemáticos encuentran esas demostraciones.
(2) Toda teoría tiene dos tipos de axiomas: sus axiomas específicos y también los axiomas lógicos, que son generales y comunes a todas las teorías. Estos últimos son enunciados que valen cualquiera sea el universo del discurso considerado (como por ejemplo, "Para todo x, x = x"). Si respetamos las restricciones para el uso de variables entonces es posible dar un sistema de axiomas que respeta las condiciones de Hilbert y que permite deducir todas esas afirmaciones universalmente válidas (esto fue probado por Gödel en 1929). Si admitiéramos variables que representaran funciones, conjuntos, etc. entonces el Programa de Hilbert sería irrealizable al nivel mismo de esta lógica subyacente.
