La cuestión gira en torno a la mejor respuesta a una pregunta anterior, ¿cuándo son iguales dos pruebas? Creo que la única respuesta satisfactoria a esta pregunta anterior es considerar la construcción implícita en la prueba. Dos pruebas son iguales cuando dan la misma construcción.
Para aislar una construcción, hay que distinguir cuidadosamente entre una prueba de enunciados de la forma "Existe..." y "Para todos...", y también hay que distinguir entre un enunciado y su doble negación. A efectos de distinguir las pruebas en la práctica, no es necesario ser tan pedante la mayoría de las veces. Por ejemplo, la "prueba topológica" de la infinidad de los primos es esencialmente la misma que la prueba de Euclides, porque dada una colección de primos, al desempacar su construcción, construye el mismo número.
Hay que señalar aquí que el problema de decidir cuándo dos programas producen las mismas respuestas es indecidible, más aún cuando los programas tienen acceso a oráculos, lo que es necesario a veces. Para complicar aún más las cosas, algunos programas sólo se diferencian superficialmente a la vista, pero son esencialmente iguales. No obstante, creo que se trata de una heurística útil, que tiene posibilidades de tener una contrapartida precisa.
La construcción del teorema de Godel suele quedar oculta por la pesada codificación que conlleva. Dado que hoy en día la codificación está estandarizada en la informática, prefiero exponer la construcción explícitamente como un programa de ordenador, en lugar de como una declaración codificada de lógica de primer orden. Dos pruebas son iguales cuando construyen el mismo programa de ordenador.
Hay exactamente tres tipos de pruebas sin empaquetar del teorema de Godel y resultados relacionados, hasta donde yo sé. Para ahorrar tecleo, un programa P "se ejecuta" si no se detiene.
TIPO I: enunciados autorreferenciales pi-0-1 (enunciados sobre la no-calidad de un determinado programa informático)
GODEL_1: Para demostrar el teorema de Godel a la manera de Godel (como lo aclararon Turing y Kleene), dado un sistema axiomático S cuyo sistema de deducción es computable, se construye el programa GODEL que hace lo siguiente:
- Imprime su propio código en una variable R. (Esto es posible ya que puedes escribir quines, y hacer que el quining sea una subrutina)
- Deduce todas las consecuencias de S, buscando una prueba en S del enunciado "R no se detiene" ("R se ejecuta"). (Este es un enunciado de aritmética de la forma "para todo n F^n(R) no se detiene", donde F es un conjunto de instrucciones recursivas primitivas para cualquier ordenador que se quiera codificar).
- Si encuentra esta declaración, se detiene.
El enunciado G--- "GODEL corre" es verdadero precisamente cuando S no lo demuestra. Por tanto, G afirma que "S no demuestra G". La autorreferencia es obvia en el primer paso del programa. Esto es equivalente a la construcción original de Godel.
A partir de la construcción, se pueden leer los requisitos del sistema de axiomas. Para estar seguro de que la interrupción de GODEL lleva a una contradicción, el sistema de axiomas tiene que ser capaz de demostrar cada declaración de la forma "el programa P lleva al estado de memoria M después del tiempo t" para todos los tiempos enteros t, y para todos los programas P. Cada una de estas declaraciones es un cálculo finito, una declaración sigma-0-1, por lo que el sistema de axiomas debe ser capaz de demostrar todas las declaraciones sigma-0-1 verdaderas (o incluso sólo un subconjunto de éstas lo suficientemente rico como para permitir que un ordenador se integre en el lenguaje).
GODEL_2: Obsérvese que si S es inconsistente, prueba todas las afirmaciones, incluida "GODEL se ejecuta", por lo que "S es inconsistente" implica "GODEL se detiene". "GODEL se detiene" también implica "S es consistente", si S puede demostrar que es sigma-0-1 completo. Por lo tanto, la incomprobabilidad de "GODEL se detiene" equivale a la incomprobabilidad de consis(S).
Pero S puede demostrar (falsamente) que "GODEL se detiene", sin ninguna contradicción, siempre que GODEL nunca se detenga realmente. Esto es decir que es posible que un sistema de axiomas demuestre su propia inconsistencia sin ser realmente inconsistente, simplemente diciendo mentiras sobre los programas de ordenador. La suposición de que S es omega consistente (o incluso sólo sigma-0-1 sonido), significa que no demuestra "P se detiene" a menos que P realmente se detenga. Así que la misma construcción de GODEL demuestra el segundo teorema de incompletitud tal y como lo afirma GODEL, un sistema omega-consistente (o un sistema sigma-0-1 sano) no puede demostrar su propia consistencia.
Todas las pruebas del teorema de Godel que pasan por el problema de la parada dan esta construcción.
ROSSER: El programa ROSSER no es más que una ligera modificación de GODEL. ROSSER hace esto:
- imprime su código en una variable R
- busca en S una prueba de 1. "R se imprime en la pantalla" o 2. "R no se imprime en la pantalla".
- Si encuentra 1. Se detiene sin imprimir, si 2, se detiene después de imprimir "hola".
Ahora note que un S consistente no puede probar 1 ni 2, porque de cualquier manera, hay un cálculo de parada que contradice la declaración. Así que un S consistente es incompleto. Si llamamos a la afirmación "ROSSER imprime en la pantalla" por el nombre R, y a su negación 2 por el nombre "notR", entonces "ROSSER no imprime" es if equivalente a "S demuestra R antes que notR", que es la glosa estándar para la construcción de ROSSER.
La afirmación de ROSSER es diferente a la de GODEL, porque la afirmación "ROSSER no imprime" no es equivalente a la afirmación "S es consistente". Pero como el enunciado "ROSSER no se detiene", ligeramente diferente, es en realidad equivalente a "S es consistente", la construcción de ROSSER incluye la construcción de GODEL de forma sencilla.
Aquí hay algunas modificaciones simples que también demuestran el teorema de Godel:
PROOF_LENGTH: Dado un enunciado demostrable de longitud L bytes en un sistema axiomático S, no existe una función computable de L, f(L), que limite la longitud de la prueba de L (teoremas relativamente cortos pueden tener pruebas enormemente largas).
construir PROOF_LENGTH para hacer lo siguiente:
- Imprimir su propio código en una variable R
- buscar en todas las deducciones de S de longitud hasta f(|R|) bytes una prueba de "R imprime bien"
- Si lo encuentra, deténgase sin imprimir
- Si no, imprime "ok" y se detiene.
En este caso, la construcción se aclara con una glosa: supongamos que f(L) existe, entonces se puede decidir el problema de detención recorriendo todas las pruebas de longitud f(|"P se detiene"|) en busca de una prueba de "P se detiene". Si no la encuentras, entonces P no se detiene.
Esto es también una prueba del teorema de Godel, ya que si S es completo, entonces decidirá todos los enunciados de la forma "P se detiene", y entonces se puede calcular la función f que es la longitud de la prueba del enunciado. Pero el programa construido es esencialmente el mismo que GODEL (en realidad ROSSER, en la versión que di aquí).
Pero la construcción explícita te da un corolario importante: si asumes que S es consistente, entonces sólo por la forma de PROOF_LENGTH, puedes ver que PROOF_LENGTH tiene que imprimir "ok" independientemente de la función f, ya que si no lo hace, esto significa que ha encontrado una prueba que no tenía. Así que la suposición de consis(S) colapsará esta prueba enormemente larga dependiente de f a una prueba corta independiente de f de la misma declaración.
Esta construcción no es más que una versión finita del programa GODEL original, y este teorema se denomina teorema de aceleración de GODEL. La suposición de consis(S) reduce la longitud de las pruebas de ciertos enunciados en una cantidad mayor que cualquier función computable de la longitud.
LOB: Dado un sistema axiomático S, considere el programa LOB que, dada la declaración A, hace lo siguiente:
- Imprime su código en R
- Deduce las consecuencias de S, buscando que "R se detenga implica A"
- si encuentra este teorema, se detiene.
"LOB se detiene" sólo si S demuestra que "LOB se detiene implica A", y entonces S también demuestra que "LOB se detiene", por lo que demuestra A por modus ponens, así que LOB se detiene si A. Pero "LOB se detiene" es equivalente a "(S demuestra que LOB se detiene) implica A", y por lo tanto a "(S demuestra (S demuestra A) implica A)". Por lo tanto, S demuestra "S demuestra ((S demuestra A) implica A) si (S demuestra A)". Este teorema se puede volver a empaquetar en una secuencia infinita de afirmaciones cada vez más oscuras, sustituyendo "LOB se detiene" por sus diferentes formas equivalentes (algunas de las cuales se contienen a sí mismas), y cerrando finalmente la recursión. El conjunto completo de enunciados Lob se genera mediante una simple gramática recursiva.
El teorema de LOB no demuestra el teorema de Godel, pero lo amplía. La prueba es del mismo tipo.
TWEEDLEDEE y TWEEDEDUM: considere dos programas como los siguientes:
TWEEDLEDEE:
- imprime el código de TWEEDLEDEE en ME, y el código de TWEEDLEDUM en HE
- busca 1. ME corre 2. ÉL corre
- si encuentra 1. se detiene, si encuentra 2. imprime "¡tweedle-dee-dee!" y entra en un bucle infinito.
TWEEDLEDUM:
- imprime el código de TWEEDLEDUM en ME, y el de TWEEDLEDEE en HE
- busca 1. ME corre 2. ÉL corre
- Si encuentra 1. se detiene, si encuentra 2. imprime "¡tweedle-dee-dum!" y entra en un bucle infinito.
Estos dan una especie de teorema de división para los sistemas axiomáticos que satisfacen las hipótesis del teorema de GODEL. Tanto "DEE corre" como "DUM corre" son indemostrables en S, ya que probar cualquiera de ellos lleva a una contradicción. "consis(S)" implica "DEE corre & DUM corre", y a la inversa "DEE corre & DUM corre" implica consis(S).
Por lo tanto, si S es inconsistente, entonces uno de TWEEDLEDEE o TWEEDLEDUM tiene que detenerse ¿Pero cuál? Esto no es decidible en S. Es decir, S+"DEE corre" es una teoría que es estrictamente más fuerte que S, ya que demuestra que "DEE corre", pero es más débil que S+"consis(S)" porque no puede demostrar que "DUM corre".
Para probar esto, observe que S prueba "DEE corre o DUM corre", es decir, "DEE se detiene implica DUM corre". Por lo tanto, si S también demostrara que "DEE se detiene implica que DUM se detiene", demostraría que "DUM se detiene", lo cual es imposible.
La razón de la declaración de impresión espuria es sólo para asegurarse de que los programas DEE y DUM, que son tan similares, no terminan siendo idénticos, lo que arruinaría la prueba (esta sutileza es difícil de ver si no se descompone la construcción en un programa explícito, pero también es fácil de evitar mediante el uso de diferentes nombres de variables, o espacios adicionales, o lo que sea).
Esta construcción es estrictamente más fuerte que la de GODEL. Demuestra que para cualquier sistema sólido S, la implicación "DEE corre implica DUM corre" es indemostrable. La construcción proporciona una prueba del teorema de Godel, aunque es similar a la de ROSSER (La afirmación DEE se detiene NO es la negación de "DUM se detiene", ese es el punto)
Me preguntaba si esta construcción estaba en la literatura desde hace mucho tiempo. Recientemente me encontré con ella en "The Realm of Ordinal Analysis" de Michael Rathjen (proposición 2.17 en la página 14). No pudo encontrarla en el resto de la literatura, pero los métodos son lo suficientemente conocidos (y lo suficientemente cercanos a los de Rosser) como para convertirla en folclore. Sin embargo, como subraya Rathjen, el resultado es significativamente más fuerte que los teoremas habituales.
TWEEDLE_N: Para adentrarnos aún más en un territorio inexplorado, consideremos la secuencia infinita de programas TWEEDLE_N (donde N es un número entero)
TWEEDLE_N:
- hace un bucle sobre M, imprimiendo el código de TWEEDLE_M en una variable R(M)
- Deduce consecuencias de S, buscando un teorema de la forma "TWEEDLE_M corre" para algún M
- Si encuentra este teorema, y M=N, se detiene. Si M != N, entra en un bucle infinito.
Es fácil ver que, o bien todos los TWEEDLE-N se ejecutan, o bien exactamente uno de ellos se detiene, algo que S puede probar, porque los pasos 1+2 (que deben ejecutarse simultáneamente en dos hilos) son los mismos para todos los programas. Pero S no puede demostrar que ninguno de ellos se ejecuta.
Para probar esto, observe que si hay una lista efectiva de programas A_N (como la de TWEEDLE), puede hacer un programa MERGE(A_N) que genera y ejecuta todos los programas en hilos paralelos y se detiene exactamente cuando lo hace cualquiera de ellos. Entonces S demuestra que o bien TWEEDLE_k se ejecuta o bien MERGE(A_r (r!=k)) se ejecuta. Es decir, TWEEDLE_k y MERGE(all the others) forman un par TWEEDLEDEE/TWEEDLEDUM. Esto significa que no se puede demostrar que una de las ejecuciones implica la otra.
El resultado es que para cualquier partición computable de los TEDELOS en dos subconjuntos disjuntos A y B, S no puede demostrar que el recorrido del TEDELO_A implica el recorrido del TEDELO_B, aunque consis(S) demuestra que todos los TEDELOS corren. Las teorías "S+toda la corrida del TEDEL_A" son teorías sólidas estrictamente entre S y S+consis(S) en términos de contenido Pi-0-1--- demuestran nuevos teoremas correctos sobre la no-calidad de los programas de ordenador, pero son más débiles que S+consis(S) (y más débiles entre sí de una manera descrita por el orden parcial de contención de conjuntos).
Me gusta este teorema, porque es una prueba que es muy ruidosa de traducir a un lenguaje lógico más tradicional. Creo que el lenguaje computacional es más natural para estos resultados.
Podría seguir haciendo pruebas autorreferenciales más complicadas (y creo que es algo interesante, todas demuestran cosas algo diferentes), pero me detendré aquí para considerar las pruebas no autorreferenciales, que funcionan en un nivel superior de la jerarquía aritmética.
TIPO II: demuestran que existen funciones totales que no son demostrables como totales. Las afirmaciones en este caso son pi-0-2, afirmaciones sobre la totalidad de alguna función computable.
FASTER_GROWTH: Dado el sistema axiomático S, considere todas las funciones computables f de los enteros a los enteros que se demuestre que son totales (es decir, que se detienen para todos los argumentos). Ahora construya el programa FASTER_GROWTH(n) que hace lo siguiente:
- Enumera las primeras n funciones que son demostrables como totales, y calcula su valor en la posición n.
- devuelve el mayor valor en n, más 1.
Si S es sólida para las declaraciones pi-0-2, entonces hay infinitas funciones probables totales, y FASTER_GROWTH se detiene en cada entrada. Además, FASTER_GROWTH es eventualmente mayor que cualquier función probablemente total en S. Así que "FASTER_GROWTH es total" es un teorema verdadero no demostrable.
La función FASTER_GROWTH se construye enteramente a partir de otras funciones que no son iguales a ella misma. El requisito de la teoría es que cuando demuestra que una función es total, está diciendo la verdad, de lo contrario FASTER_GROWTH se atascará en un bucle infinito en algún momento. Esto es la solidez pi-0-2. Las pruebas de solidez pi-0-2 generalmente construyen este tipo de cosas, cuando se desempacan.
La forma abreviada más común de este argumento es la siguiente: dado un sistema axiomático S, la diagonalización contra todas las funciones recursivas probables totales en la teoría da una función recursiva total que la teoría no puede probar que es total. Este argumento es folclórico.
Los teoremas de Godel de tipo II proporcionan una forma diferente de reforzar el sistema de axiomas, añadiendo la afirmación de la totalidad de FASTER_GROWTH. Esta afirmación implica la consistencia de S, pero es estrictamente más fuerte, ya que la consistencia no es suficiente para asegurar que FASTER_GROWTH es total (se necesita algo de solidez).
TIPO III: teorema no constructivo sobre una gran clase de enunciados, que no proporciona un enunciado indemostrable explícito, por lo que no puede utilizarse para ascender en la jerarquía de los sistemas.
BOOLOS: No hay ningún programa de ordenador que dé la respuesta verdadera a afirmaciones de la forma "El número entero N se puede nombrar utilizando k bytes o menos de símbolos de la Aritmética Peano"
escribir el programa BOOLOS: 1. hace un bucle sobre todos los enteros N, buscando el primer N que requiera más de M símbolos para nombrarlo, donde M es la longitud de los símbolos que describen la salida de BOOLOS, traducida a aritmética. 2. imprime N.
La contradicción significa que BOOLOS no funciona. Boolos no es tan grande, porque no se centra en un sistema particular, pero es la misma idea básica que...
CHAITIN: Que sustituye la noción de definibilidad por la complejidad de Kolmogorov, que es la definibilidad por un algoritmo. Escribe el programa CHAITIN para hacer lo siguiente:
- Enumerar todas las pruebas de S, buscando "la complejidad de Kolmogorov de la cadena Q es mayor que N" (donde N es la longitud de CHAITIN)
- Imprimir cadena Q
Ahora bien, si S demuestra alguna vez que la complejidad de Kolmogorov de cualquier cadena es mayor que la longitud de CHAITIN, entonces CHAITIN convertirá a S en un mentiroso sigma-0-1 (inconsistente). Esto demuestra que hay un límite completamente efectivo en la máxima complejidad de Kolmogorov demostrable de cualquier cadena. (esto se dio anteriormente como respuesta).
Hay una lista infinita de sentencias verdaderas de la forma "La complejidad de Kolmogorov de Q es N", ya que hay infinitas cadenas y sólo finitamente muchos programas de longitud inferior a N. Pero sólo un número finito de estos teoremas se deciden por cualquier sistema de axiomas S. Esta es una prueba menos explícita, porque no se puede estar seguro de qué cadenas son indemostrablemente complejas, por lo que no hay un axioma natural que añadir para fortalecer el sistema.
La afirmación "la complejidad de Kolmogorov de Q es N", traducida a la aritmética, es para todo P, existe N, ((F^N(P) es un estado detenido con salida Q) implica |P|>n), de modo que es Pi-0-2.
Ahora hay que identificar qué pruebas son de qué tipo:
- Pruebas de sentencias autorreferenciales--- tipo I (Godel, Rosser, Kleene, Post, Church, Turing, Smullyan, obras populares)
- Pruebas de inducción Epsilon-naught--- son del tipo II, pero específicas de la Aritmética de Peano. La versión general es la presentada anteriormente (la prueba de Kripke, y Paris-Harrington, Goodstein, Hydra). La versión que dan es que el ordinal límite de todos los ordinales demostrables recursivos es recursivo pero no demostrablemente recursivo, pero este es un argumento de tipo II.
- Prueba del modelo de la teoría de conjuntos de Jech/Woodin---a pesar de toda su elegancia y generalidad, la prueba es de tipo 1 cuando se formula computacionalmente. Lo explicaré a continuación
- Chaitin/Boolos--- tipo III. No conozco ningún otro tipo III.
Por cierto, estoy de acuerdo con Sergei en que la axiomaticidad finita (aunque Putnam la enfatiza por alguna razón) no es tan importante. Esa propiedad depende exactamente de cómo se elijan los axiomas. El teorema de completitud es lo suficientemente fuerte como para obtener un cálculo general a partir de sólo un número finito de axiomas. La prueba de la imposibilidad de la axiomatización finita (cuando se sostiene) es que la teoría es autorreflexiva, puede probar la consistencia de cualquier fragmento finito (esto es cierto en PA, porque PA prueba la consistencia de la inducción restringida al nivel N en la Jerarquía Aritmética), y la axiomatización es débil, en el sentido de que finitamente muchos axiomas están atascados en algún fragmento finito sin importar cuántas veces los uses. La autorreflexión es interesante, pero no es tan relevante para el teorema de incompletitud.
Para ver que la prueba de Jech/Woodin es realmente una prueba de tipo I disfrazada, es importante para el propósito de desempacar la construcción complementar la teoría de conjuntos con un procedimiento efectivo para dar significado computacional a los modelos. Esto no es más que lógica de primer orden y el teorema de completitud, como afirma Andreas Caicedo en la introducción. (Para continuar --- estoy demasiado cansado para evitar afirmaciones erróneas --- perdón por la excesiva longitud)