43 votos

¿Cuáles son algunas pruebas del Teorema de Godel que son *esencialmente diferentes* de la prueba original?

Estoy buscando ejemplos de pruebas del (Primer) Teorema de Incompletitud de Godel que sean esencialmente diferente de (la mejora de Rosser de) la prueba original de Godel.

Esto se inspira en parte en las preguntas que se han formulado anteriormente:

( Pruebas del teorema de Gödel )

( Cuándo dos pruebas del mismo teorema son realmente pruebas diferentes )

Para dar un ejemplo de lo que quiero decir: La prueba de Godel/Rosser (ver http://www.jstor.org/pss/2269059 para una exposición) muestra que cualquier teoría axiomatizable consistente y suficientemente fuerte es incompleta. La prueba utiliza una cantidad sustancial de teoría de la recursión: la representabilidad de las funciones recursivas primitivas y el lema de la diagonal (más o menos lo mismo que el teorema de la recursión de Kleene) son ingredientes esenciales. El segundo teorema de incompletitud -que ninguna teoría axiomatizable suficientemente fuerte puede demostrar su propia consistencia- es esencialmente un corolario de esta demostración, y uno bastante natural. Por otra parte, en 2000 Hilary Putnam publicó ( https://doi.org/10.1305/ndjfl/1027953483 ) una prueba alternativa del primer teorema de incompletitud de Godel, debida a Saul Kripke hacia 1984. Esta prueba utiliza mucho menos la teoría de la recursión, basándose en cambio en alguna teoría elemental de modelos no estándar de la aritmética. El teorema demostrado es ligeramente más débil, ya que la prueba de Kripke requiere $\Sigma^0_2$ -sonoridad, que es más fuerte que la mera consistencia (aunque todavía más débil que la suposición original de Godel de $\omega$ -consistencia).

La prueba de Kripke es claramente lo suficientemente diferente de la prueba de Godel/Rosser como para merecer ser considerada un objeto genuinamente separado. Lo que hace que la diferencia parezca realmente impresionante, al menos para mí, es que la prueba de Kripke produce un corolario diferente al de Godel/Rosser. En un breve párrafo, Putnam muestra (y no sé si esta parte de su trabajo se debe a Kripke) que el argumento de Kripke demuestra que no hay ninguna extensión consistente finitamente axiomatizable de $PA$ . Este no es un resultado que yo sepa que se desprende de la prueba de Godel/Rosser; además, el Segundo Teorema de Incompletitud, que es un corolario de la prueba de Godel/Rosser, no parece fácilmente derivable de la prueba de Kripke.

Motivado por esto, digamos que dos demostraciones de (aproximadamente) el mismo teorema son esencialmente diferente si dan lugar a diferentes corolarios naturales. Es evidente que se trata de una noción totalmente subjetiva, pero creo que tiene suficiente significado compartido como para que valga la pena.

Mi pregunta principal, entonces, es:

  1. ¿Qué otras pruebas esencialmente diferentes de algo parecido al Primer Teorema de Incompletitud de Godel se conocen? En otras palabras, ¿hay alguna otra prueba de algo parecido a "toda extensión axiomatizable consistente de $PA$ es incompleto" que no da como corolario natural el Segundo Teorema de Incompletitud de Godel?

Me interesan especialmente las pruebas que no dan lugar a la inexistencia de extensiones consistentes finitamente axiomatizables de $PA$ y en las pruebas que sí dan algunos corolario natural. No me importa especialmente la versión precisa del Primer Teorema de Incompletitud demostrado: si se aplica a sistemas en el lenguaje de la aritmética de segundo orden, si asume $\omega$ -consistencia, o si sólo se aplica a sistemas más fuertes que $ATR_0$ digamos, que para mí es lo mismo. Sin embargo, yo hacer requieren que la versión del teorema de incompletitud demostrada se aplique a todos los sistemas suficientemente fuertes con cualquier propiedad de consistencia que se necesite; así, por ejemplo, no consideraría el trabajo de Paris y Harrington como un buen ejemplo de esto.

El único otro ejemplo potencial de una prueba esencialmente diferente que conozco es la(s) prueba(s) de Jech y Woodin (véase https://andrescaicedo.files.wordpress.com/2010/11/2ndincompleteness1.pdf ), pero no comprendo esa prueba a un nivel tal que me sienta cómodo diciendo que es de hecho una prueba esencialmente diferente. Me parece que es bastante similar a la prueba original. ¿Quizás alguien pueda aclararme?

Por supuesto, totalmente aparte de mi pregunta principal, mi caracterización de la diferencia entre las dos pruebas específicas del teorema de incompletitud mencionadas anteriormente puede ser incorrecta. Así que también me interesa la siguiente pregunta:

  1. ¿Es cierto que la prueba de Kripke no da lugar a la Segunda Incompletitud como corolario natural, y que la prueba de Godel/Rosser no da lugar fácilmente a la inexistencia de una extensión finitamente axiomatizable de PA como corolario natural?

38voto

mbanzon Puntos 175

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:

  1. 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)
  2. 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).
  3. 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:

  1. imprime su código en una variable R
  2. busca en S una prueba de 1. "R se imprime en la pantalla" o 2. "R no se imprime en la pantalla".
  3. 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:

  1. Imprimir su propio código en una variable R
  2. buscar en todas las deducciones de S de longitud hasta f(|R|) bytes una prueba de "R imprime bien"
  3. Si lo encuentra, deténgase sin imprimir
  4. 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:

  1. Imprime su código en R
  2. Deduce las consecuencias de S, buscando que "R se detenga implica A"
  3. 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:

  1. imprime el código de TWEEDLEDEE en ME, y el código de TWEEDLEDUM en HE
  2. busca 1. ME corre 2. ÉL corre
  3. si encuentra 1. se detiene, si encuentra 2. imprime "¡tweedle-dee-dee!" y entra en un bucle infinito.

TWEEDLEDUM:

  1. imprime el código de TWEEDLEDUM en ME, y el de TWEEDLEDEE en HE
  2. busca 1. ME corre 2. ÉL corre
  3. 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:

  1. hace un bucle sobre M, imprimiendo el código de TWEEDLE_M en una variable R(M)
  2. Deduce consecuencias de S, buscando un teorema de la forma "TWEEDLE_M corre" para algún M
  3. 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:

  1. Enumera las primeras n funciones que son demostrables como totales, y calcula su valor en la posición n.
  2. 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:

  1. 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)
  2. 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)

5voto

Brian Gillespie Puntos 1321

Hay un par de pruebas bien conocidas de incompletitud basadas en las propiedades de los grados PA. Los grados PA se han estudiado ampliamente en la teoría de la recursión.

Un grado de PA es un grado de Turing que puede calcular una extensión completa de PA. Obviamente, para demostrar el teorema de incompletitud, basta con mostrar que ningún grado de PA puede ser recursivo. (Si tuviéramos una teoría de e.r. consistente T que extendiera PA y que no fuera incompleta, entonces su terminación sería recursiva -- para decidir si $T \models \varphi$ o $T \models \neg \varphi$ simplemente busca una prueba de $\varphi$ o $\neg \varphi$ de $T$ y porque $T$ se supone que es completo, este proceso siempre termina y por lo tanto es recursivo).

Una forma de ver que no hay grados PA recursivos es observar que cualquier grado PA puede calcular un modelo no estándar de PA a través de la compacidad y una construcción de Henkin. Ahora aplique el teorema de Tennenbaum de que no hay modelos no estándar recursivos de PA.

Otra forma de ver que no hay grados PA recursivos es con $\Pi^0_1$ clases. Cada grado de PA puede calcular un camino a través de cada $\Pi^0_1$ clase (esta es una dirección del teorema de la base de Scott). Para terminar, hay que tener en cuenta que se puede construir $\Pi^0_1$ que no contienen elementos recursivos. Por ejemplo, hay $\Pi^0_1$ que contienen sólo elementos diagonales no recursivos.

5voto

lorenzo-s Puntos 237

Además de las pruebas ya enumeradas, un tratamiento esencialmente diferente que me viene a la mente es la prueba de consistencia de Gentzen de PA, que estableció que PA puede probar el buen orden de las notaciones ordinales menores que $\epsilon_0$ pero no pudo demostrar el buen orden de una notación para $\epsilon_0$ y que, a su vez, el buen orden de $\epsilon_0$ sería suficiente para demostrar la consistencia de la AP. La caracterización del ordinal teórico de la prueba de una teoría arroja resultados de incompletitud por una vía esencialmente diferente (y podría decirse que mucho más profunda / general) a la de Godel.

3voto

Venkata Koppaka Puntos 21

También hay un argumento de "definibilidad invariable". Lo esbozaré rápidamente a continuación, y luego daré un análisis para explicar por qué creo que es significativamente diferente. Lamentablemente, en este momento no puedo encontrar la fuente; recuerdo haberlo visto como una nota a pie de página en la obra de Kreisel Invariantes teóricos del modelo papel, pero no parece estar ahí. Varios autores han escrito sobre la definibilidad invariante (de la que esta respuesta es un anuncio no muy secreto) por lo que aún no he podido realizar una búsqueda exhaustiva de la referencia, pero cuando la encuentre actualizaré esto. Por cierto, este argumento fue referido al principio de otra respuesta mía .

A continuación, "definible" significa "definible sin parámetros". Para un lenguaje más agradable, llamaré a este argumento "argumento tarskiano".


Argumento

Dejemos que $T$ ser una teoría "apropiada" de la aritmética (digamos, $T\supseteq R$ ). Modificamos el teorema de indefinibilidad de Tarski muy ligeramente como sigue. Para $X\subseteq\mathbb{N}$ y $M\models T$ , digamos que $X$ es pseudodefinible en $M$ si $X=D\cap \mathbb{N}$ para algún tipo de $D\subseteq M$ . Entonces tenemos:

$(*)\quad$ Supongamos que $M\models T$ . Entonces $Th(M)$ no es pseudodefinible en $M$ .

La prueba estándar sigue funcionando: suponiendo al contrario que $\theta$ pseudodefinido $Th(M)$ en $M$ , dejemos que $m$ sea el número de Godel de la fórmula $\eta(x)\equiv$ " $\theta$ falla en el número de la frase que se obtiene al enchufar $x$ en la fórmula con el número $x$ " - debidamente formalizado - y considere la frase $\eta(\underline{m})$ (aplicando adecuadamente la representabilidad).

Con esto en la mano, argumentamos lo siguiente. Supongamos que $S\supseteq T$ es computable y satisfacible. Entonces por representabilidad tenemos que $S$ es pseudodefinible en $M$ por cada $M\models T$ . Tomando $M\models S$ tenemos por $(*)$ que $S\not=Th(M)$ Así que $S$ no está completa.


Análisis

Ahora permítanme argumentar a favor de que el argumento Tarskiano es un genuino variación.

En primer lugar, es fácil negativo observación: se aplica a las teorías autoverificadas de Willard y, por tanto, no puede dar lugar al segundo teorema de incompletitud como corolario directo. Desde un punto de vista más subjetivo, el argumento es bastante no constructivo, y no produce (por lo que veo) rápidamente una sentencia específica indecidible.

Por supuesto, esta es también una característica de los muchos argumentos teóricos de computabilidad estándar. Creo que todavía hay una diferencia aquí - esta vez un positivo uno - debido a la forma en que el argumento tarskiano interactúa con la noción de definibilidad invariable . Hay un par de maneras de enmarcar esto - ver por ejemplo el principio del artículo Computabilidad abstracta y definibilidad invariante de Moschovakis para discutirlo - y usaré lo siguiente:

Definición:

  • Un contexto aritmético es un conjunto $\mathfrak{C}$ de modelos de la aritmética de Robinson $R$ .

  • Para un contexto aritmético $\mathfrak{C}$ , un conjunto $A\subseteq \mathbb{N}$ es $\mathfrak{C}$ -invariablemente definible si existe alguna fórmula $\varphi$ con $\varphi^M\cap\mathbb{N}=A$ para todos $M\in\mathfrak{C}$ .

(Aquí me permito la habitual confusión abusiva de $\underline{k}^M$ y $k$ .)

  • Para una teoría $E$ y un contexto aritmético $\mathfrak{C}$ , digamos que $E$ es $\mathfrak{C}$ -satisfiable si algún miembro de $\mathfrak{C}$ satisface $E$ .

Entonces el argumento Tarskiano de hecho da:

Propuesta: Supongamos que $\mathfrak{C}$ es un contexto aritmético. Entonces no $\mathfrak{C}$ -La teoría satisfactoria es $\mathfrak{C}$ -invariablemente definible.

(Dado que los conjuntos computables son invariablemente definibles en todo contexto aritmético y en toda teoría que extienda $R$ y se produce en un contexto aritmético, se trata de una generalización de la indecidibilidad esencial).

La cuestión es que, en general, el $\mathfrak{C}$ -conjuntos definibles de forma invariable no tienen por qué soportar una buena teoría de la computabilidad en ningún sentido: mediante una elección juiciosamente terrible de $\mathfrak{C}$ podemos hacer que el conjunto de $\mathfrak{C}$ -los conjuntos definibles de forma invariable no tienen básicamente ninguna propiedad estructural aparte de formar un álgebra booleana. Así que, por ejemplo, no veo cómo se puede hacer un análogo del argumento de los "conjuntos inseparables c.e." para contextos aritméticos arbitrarios.

Por supuesto, los contextos aritméticos patológicos no son interesantes por lo que es difícil argumentar que este aspecto es realmente valioso de cualquier manera. Pero es - por lo que puedo decir - una característica no trivial.

2voto

Michael Hardy Puntos 4554

Creo recordar que en los sistemas razonables de aritmética (tiene que haber un algoritmo para decidir si un enunciado es un axioma, y tiene que haber un algoritmo de comprobación de pruebas, y una cierta cantidad de aritmética tiene que ser demostrable) sólo hay un número finito de secuencias que se puede demostrar que son aleatorias en el sentido de Kolmogorov--Chaitin, aunque debe haber infinitas secuencias que son aleatorias en ese sentido.

i-Ciencias.com

I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.

Powered by:

X