Sabemos que hay enunciados que son indecidibles/independientes de ZFC. ¿Puede haber un enunciado S, tal que (ZFC $\not\vdash$ S y ZFC $\not\vdash$ ~S) es indecidible?
Por supuesto, todo esto suponiendo que ZFC sea realmente coherente... (-:
Sabemos que hay enunciados que son indecidibles/independientes de ZFC. ¿Puede haber un enunciado S, tal que (ZFC $\not\vdash$ S y ZFC $\not\vdash$ ~S) es indecidible?
Al menos una versión de esta pregunta tiene una respuesta casi trivial; si quieres saber si hay algún enunciado G tal que ZFC (o el sistema lógico compatible con PA que elijas) no demuestra G, ZFC no demuestra ~G, y no podemos demostrar que ZFC no demuestra G o no G, ¡entonces cualquier enunciado indecidible sirve!
En concreto, es imposible que ZFC demuestre que no puede demostrar algo, porque tal afirmación equivale a la consistencia de ZFC; si ZFC fuera inconsistente entonces podría demostrarlo todo, así que demostrar que hay algo que no se puede demostrar equivale a demostrar la consistencia de ZFC, y por supuesto esto está prohibido por el segundo teorema de incompletitud.
(Zhen: La independencia es con respecto a ZFC).
Dada cualquier sentencia S, o bien (1) ZFC prueba S, en cuyo caso es un teorema de ZFC que ZFC prueba S, o bien (2) ZFC no prueba S. En este caso, ZFC es consistente, y ZFC no sabe que no prueba S (o bien sabría que es consistente, y por tanto no lo sería, pero entonces probaría S). Así que, en este caso, ZFC no demuestra que no demuestra S, y no demuestra que demuestra S. Se deduce fácilmente que "ZFC demuestra S" es independiente de ZFC, para cualquier S para el que ZFC no demuestra S.
Preguntar si la afirmación "ZFC demuestra S" o una variante de ésta como (+): "ZFC no demuestra S y no demuestra no-S" es decidible, por otro lado, es una tontería, a no ser que se esté utilizando el término de forma extraña. Para cualquier S existe una máquina de Turing M sin entrada que da como resultado el valor de verdad del enunciado (+). No pides la decidibilidad de una sola afirmación, sino de una familia de afirmaciones, digamos con S como parámetro. Probablemente, debe aclarar lo que quiere decir.
La única forma sensata de entender lo que preguntas es tomar el conjunto cuyo único elemento es una frase que formaliza el enunciado (+), y preguntar si ese conjunto es decidible, pero por supuesto lo es como cualquier conjunto finito (de números naturales) es trivialmente decidible. Quizá sea más interesante saber si, llamando a la (formalización de la) afirmación entre comillas $(+)_S$ el conjunto $A=$ { $S\mid(+)_S$ } es decidible.
Ahora: Supongamos primero que ZFC es inconsistente. Entonces ZFC demuestra cualquier cosa, por lo que todas las afirmaciones $(+)_S$ son falsas. Por lo tanto, el conjunto $A$ es obviamente decidible. Supongamos ahora que ZFC es consistente. Sea S indecidible. Entonces si una máquina resuelve $A$ nos diría, al introducir S, que S es independiente. Como el conjunto de declaraciones independientes (de ZFC) es independiente, hemos terminado: $A$ es indecidible.
Quizás quieras saber si ZFC demuestra que A es decidible, o si demuestra que A es indecidible. Observe que si ZFC demuestra que A es indecidible, entonces el argumento anterior (formalizado dentro de ZFC) nos dice que ZFC sabe que ZFC es consistente. En este caso, ZFC es incoherente, y prueba cualquier cosa.
Supongamos, entonces, que ZFC demuestra que A es decidible. Esto es posible si ZFC es inconsistente. Entonces, supongamos que ZFC es consistente. Entonces el argumento anterior nos dice que ZFC demuestra que ZFC es inconsistente.
Esto no es de esperar, ya que nos dice que ZFC se equivoca con las declaraciones aritméticas. Si ZFC es una teoría "verdadera", es decir, si las consecuencias aritméticas de ZFC son verdaderas sobre los números naturales, entonces ZFC no puede demostrar que A es decidible, y "A es decidible" es independiente. Por supuesto, si ZFC no es una teoría verdadera, no creo que sea demasiado interesante que demuestre una cosa u otra sobre A.
Podemos complicar aún más las cosas considerando modelos de ZFC, y comprobando si el modelo piensa que ZFC demuestra que A es decidible, o no, o cualquiera de las posibles variantes sugeridas anteriormente. Podemos, de hecho, suponiendo unos requisitos de consistencia leves en ZFC, comprobar que hay modelos de ZFC que no están de acuerdo en si ZFC demuestra que A es decidible, demuestra que es indecidible, o no demuestra ninguna de las dos cosas.
Andres: estás hablando del concepto formal de "decidibilidad de la pertenencia a un conjunto", mientras que sospecho que el autor está utilizando un concepto informal de decidibilidad, es decir, "P es decidible" se está utilizando como un atajo para "los axiomas de mi teoría pueden demostrar P o demostrar ~P"...
Andrés, gran respuesta. Ahora me pregunto, si decimos que "ZFC demuestra que S" es independiente, ¿podemos forzarlo y así forzar S, o cuando forzamos S basta con forzar "ZFC demuestra que S"? ¿Qué pasa con S que es inconsistente con ZFC, si ZFC no puede probarlo, entonces "ZFC prueba que S" es independiente, podemos forzar esa afirmación?
@Steven: Sí, me lo imaginaba. Por eso trato primero el tema de la independencia de la teoría, para asegurarme de cubrir ambas opciones. (Al fin y al cabo, entender la "decidibilidad" en el sentido habitual de la teoría de la computabilidad nos da una pregunta más interesante, después de todo).
Esta respuesta es una respuesta a la respuesta de Simon. Es trivial demostrar que cualquier enunciado que es 2-indecidible es 3-indecidible. Por ejemplo, tome cualquier declaración S, entonces
(1)Supongamos que S es decidible, entonces su indecidibilidad es decidible.
(2)Supongamos que la indecidibilidad de S es indecidible, entonces desde (1), S es indecidible.
(3)Supongamos que la indecidibilidad de S es indecidible pero la indecidibilidad de su indecidibilidad es decidible, entonces se puede demostrar que la indecidibilidad de S es indecidible, y a partir de (2), esto significa que se puede demostrar que S es indecidible. Por lo tanto, la indecidibilidad de S es decidible, lo que contradice la suposición de que la indecidibilidad de S es indecidible.
Así, para cualquier enunciado S, si su indecidibilidad es indecidible, necesariamente la indecidibilidad de su indecidibilidad es indecidible.
También se puede demostrar que si S es 3-undecidible, entonces es 4-undecidible como sigue.
Sea T el enunciado S es indecidible. Supongamos ahora que S es 3 indecidible, entonces T es 2 indecidible por lo que T es 3 indecidible por lo que S es 4 indecidible.
He intentado exponer esta prueba con más detalle (y con un simbolismo que creo que es más fácil de entender que la prosa aquí expuesta) en esta respuesta .
Si todo enunciado fuera decidible, eso implicaría que todo enunciado podría demostrarse verdadero o falso, lo que contradice Primer teorema de incompletitud de Gödel .
Si la decidibilidad de todo enunciado fuera decidible, eso implicaría que todo enunciado podría demostrarse verdadero, falso o indecidible. Podríamos entonces definir un método para clasificar todos los enunciados como verdaderos o falsos: Enumerar todos los enunciados: Cuando se demuestre que uno es indecidible, añadir un axioma que diga que es falso. Esto se conoce como Programa Hilbert y de nuevo se demostró que era imposible por Primer teorema de incompletitud de Gödel .
Y así sucesivamente para $n$ -enunciados indecidibles.
Dejemos que $d(S)$ denotan "podemos demostrar que S es decidible".
Si probamos S, entonces sabemos que S es decidible. Si refutamos S, entonces sabemos que S es decidible. Es decir:
$$ S \implies d(S), \ \ \ \neg S \implies d(S) $$
De la misma manera: Si probamos $d(S)$ entonces sabemos que $d(S)$ es decidible. Si refutamos $d(S)$ entonces sabemos que $d(S)$ es decidible.
$$ \ \ \ d(S) \implies \ \ d(d(S)), \ \ \ \ \ \neg d(S) \implies \ \ \ d(d(S)) $$
La línea anterior implica (por modus tollens en cada uno) que:
$$ \neg d(S) \impliedby \neg d(d(S)), \ \ \neg\neg d(S) \impliedby \neg d(d(S)) $$
Así que concluimos que si la decidibilidad de S es en sí misma indecidible, entonces: no podemos demostrar que S es decidible y no podemos demostrar que S es indecidible.
"Podríamos entonces definir un nuevo axioma que afirme que todos los enunciados indecidibles son falsos". En realidad eso no funciona: un sistema así sería incoherente, ya que si $P$ es indecidible, entonces también lo es $\neg P$ . Hay que trabajar un poco más.
Sí. Esto es cierto para cualquier enunciado de primer orden por el teorema de Church, no sólo los enunciados con respecto a ZFC. La lógica de primer orden es semidecidible, en el sentido de que todo enunciado de primer orden que pueda demostrarse tiene un cálculo de prueba sólido y completo; los enunciados válidos siempre serán decidibles, y siempre podrán demostrarse, aunque esto puede llevar un poco de cálculo.
Sin embargo, la satisfacción es indecidible en general. Si un enunciado es satisfacible, a veces se puede demostrar que es satisfacible con modelos finitos, o forzados. Si el enunciado mismo y su negación son demostrables, entonces acabas de demostrar que el enunciado no es un enunciado universalmente válido. Sin embargo, uno de los resultados del teorema de Church demuestra que no hay ningún algoritmo en el que se pueda confiar para terminar de comprobar la satisfabilidad de un enunciado arbitrario de primer orden, porque de lo contrario se resolvería el Entscheidungsproblem.
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.
4 votos
¿Puede definir exactamente lo que quiere decir con " $\mathrm{ZFC} \vdash S$ es indecidible"? No tiene sentido decir que preguntar si " $\mathrm{ZFC} \vdash S$ " es independiente, porque no has preguntado de qué es independiente.
0 votos
Con(T) => (T $\not\vdash$ (Con(T) => T $\not\vdash$ S $\land$ T $\not\vdash$ ~S) $\land$ T $\not\vdash$ (Con(T) $\land$ (T $\vdash$ S $\lor$ T $\vdash$ ~S)) )
0 votos
T $\not\vdash$ (Con(T) $\land$ (T $\vdash$ S $\lor$ T $\vdash$ ~S)) es siempre verdadera porque T $\not\vdash$ Con(T).
0 votos
Versión 2: Con(T) => (Con(T + (Con(T) => (Con(T + S) $\land$ Con(T + ~S))) ) $\land$ Con(T + (Con(T) $\land$ (~Con(T + S) $\lor$ ~Con(T + ~S))) ))
0 votos
@ZhenLin: Me parece obvio que se refiere a la independencia de ZFC. Qué me estoy perdiendo aquí?