Cualquier sistema formal consistente F dentro del cual pueda llevarse a cabo cierta cantidad de aritmética elemental es incompleto; es decir, hay enunciados del lenguaje de F que no se pueden probar ni refutar en F.
Entonces, ¿por qué no puede tener una cantidad finita de sistemas formales F2...FN que prueben todas las afirmaciones (o, de lo contrario, una cantidad considerable) que no pueden probarse dentro de sí mismos?
Si no, ¿no prueba esto que algunas afirmaciones no pueden probarse en absoluto bajo ningún sistema formal?
Inicialmente, pensé que esto podría deberse a que F2 y F suponiendo que la coherencia podría tratarse como un sistema y, por lo tanto, están incompletos de la misma manera.
Razoné que, por otro lado, esto implicaría que existe un sistema formal perfecto que prueba tanto como es factible.
Sin embargo, esto me hizo pensar en la posibilidad de hacer esto con un sistema formal más débil y un sistema formal más fuerte (W1 y F), probando o simplificando las declaraciones que F no puede probar por sí sola. ¿Por qué esto no es factible? Para ser precisos, me preguntaba por qué no se pueden combinar sistemas formales sin usarlos como un nuevo sistema formal en este contexto. Por ejemplo, usar W1 o F2 para probar declaraciones en F (que F no puede probar) sin referirse directamente a F.
Version corta:
Primero, tenga en cuenta que no ha establecido el teorema de Gödel correctamente; más bien, es:
Toda teoría consistente computablemente axiomatizable que "contenga suficiente aritmética" es incompleta.
"Computablemente axiomatizable" aquí básicamente significa que la teoría no es tan complicada como para ser imposible de describir; por ejemplo, tomando una postura platónica por la simplicidad, el conjunto de todas las oraciones verdaderas sobre los números naturales es consistente, completo y, trivialmente, "contiene suficiente aritmética".
Esto no será relevante hasta el final de mi respuesta, pero es importante señalarlo.
Toda proposición puede decidirse en alguna teoría. Como un ejemplo tonto, si p no es lógicamente inválido, entonces es refutado por el conjunto vacío de axiomas, y si p no es lógicamente inválido, entonces { p } es un conjunto consistente de axiomas que prueba p . Menos estúpidamente, asumiendo (digamos) que ZFC es consistente, entonces uno de ZFC+ p y ZFC+~ p es consistente, o ambos , y cualquiera que sea consistente claramente decide p .
(Tenga en cuenta que es el caso en negrita el que es crucial aquí: si solo uno de ZFC + p y ZFC + ~ p es consistente, entonces ZFC solo decide p ya).
Entonces eso responde a una de sus preguntas: "Si no, ¿no prueba esto que algunas declaraciones no pueden probarse en absoluto bajo ningún sistema formal?"
Ahora veamos qué sucede cuando tratamos de usar múltiples teorías para eludir la incompletitud.
Si tenemos teorías T1 , ..., Tn que no discrepan en nada , entonces su unión T es también una teoría a la que es aplicable el teorema de Gödel; el enunciado de Gödel resultante g(T) es a fortiori indecidible en cada uno de T1 ,..., Tn .
(En realidad, como punto técnico aquí, deberíamos usar la oración de Rosser en su lugar, pero meh).
¿Qué pasa si permitimos el desacuerdo? Bueno, para empezar, esto arroja toda la idea al caos: si hay desacuerdo entre los Ti (digamos, T1 prueba p pero T2 refuta p ), entonces es difícil decir cómo la colección de teorías T1,...,Tn podría Se puede decir que decide cualquier cosa , pero resulta que incluso permitir el desacuerdo no ayuda:
Si T1 , ..., Tn son cada una de las teorías a las que se aplica el teorema de incompletitud de Gödel (= consistentes, computablemente axiomatizables y que contienen suficiente aritmética) , entonces hay alguna oración indecidible en cada una de T1 ,..., Tn .
(He puesto esto en una fuente gigante porque creo que es realmente el resultado más importante mencionado en esta respuesta).
Esto es sorprendentemente difícil de probar; un par de respuestas mías antiguas ( 1 , 2 ) manejan el caso de dos teorías (la segunda prescinde de una suposición innecesaria utilizada en la primera), y el caso general es más complicado pero fundamentalmente el mismo. Específicamente, el punto es que no podemos tener un "bucle de consistencia" donde una teoría prueba la consistencia de otra teoría que prueba la consistencia de otra teoría que... que prueba la consistencia de la teoría original, pero si cada oración es decidible en una de nuestras teorías, entonces tal "bucle de consistencia" es imposible de evitar.
Finalmente, su declaración
Razoné que, por otro lado, esto implicaría que existe un sistema formal perfecto que prueba tanto como es factible
entra en conflicto con el requisito de axiomatizabilidad computable en el teorema de Gödel. Incluso ignorando el problema de encontrar un mecanismo para elegir la teoría "correcta" que decida una oración dada que no hemos decidido hasta ahora, no podemos evitar el problema de que la unión de un número infinito de teorías axiomatizables no necesita serlo. .
Es en este punto que la teoría de la computabilidad se vuelve muy relevante: resulta que podemos cuantificar cuán complicada debe ser una teoría completa consistente que contenga suficiente aritmética. La respuesta es técnica , pero el punto es que esto es algo que podemos atacar rigurosamente y desarrollar una buena comprensión.
JD
Conifold