Sé que hay muchas conjeturas sin resolver, pero es posible que sean independientes de ZFC (ver ¿Podría ser que la conjetura de Goldbach sea indecidible? por ejemplo).
Me preguntaba si hay alguna conjetura para la cual hayamos demostrado que existe una prueba de ella o de su negación, pero simplemente no hemos encontrado esa prueba todavía.
¿Podría existir incluso una prueba de dependencia, o sería la única forma de demostrar que una afirmación es dependiente demostrándola/refutándola?
Hay un montón de problemas en matemáticas que pueden resolverse mediante una computación finita en principio, pero para los cuales la computación es demasiado grande para llevarse a cabo realmente y no conocemos ningún atajo que nos permita encontrar la respuesta sin calcularla por fuerza bruta. Por ejemplo, el valor del número de Ramsey $R(5,5)$ es desconocido, aunque se sabe que debe ser uno de los números $43,44,45,46,47$ o $48$. Sabemos que existe una demostración de cuál es realmente el número, ya que puedes encontrar la respuesta en principio mediante una búsqueda exhaustiva de un número finito (pero muy muy grande) de casos.
Otro ejemplo es resolver el juego de ajedrez. Sabemos que con un juego perfecto, una de las siguientes afirmaciones debe ser cierta en el ajedrez: Blanco puede forzar una victoria, Negro puede forzar una victoria, o ambos jugadores pueden forzar un empate. Debe existir una prueba de uno de los casos, ya que simplemente puedes examinar todas las secuencias posibles de movimientos (hay algunas cuestiones técnicas sobre posiciones repetidas pero al final no importan).
De hecho, cada ejemplo debe ser de esta forma, en el siguiente sentido. Supongamos que tienes una afirmación $P$ y sabes que existe una prueba de $P$ o una prueba de $\neg P$ (en un sistema formal fijo). Entonces hay un algoritmo que puedes llevar a cabo para determinar si $P$ o $\neg P$ es verdadero (asumiendo que tu sistema formal es coherente, lo que significa que solo puede probar afirmaciones verdaderas): uno por uno, enumera todas las posibles pruebas en tu sistema formal y verifica si son una prueba de $P$ o una prueba de $\neg P$. Eventualmente encontrarás una prueba de una de ellas, ya que una prueba de una de ellas existe. Así que esta es una computación que sabes que está garantizada de ser finita en longitud y que sabes que resolverá el problema.
¿No depende eso de cómo uno enumera sus pruebas formales? Por ejemplo, si aplicara repetidamente la misma regla inductiva a sí misma, cada vez obtendría una nueva prueba, y sin embargo hay ciertos teoremas que nunca tropezaré en este camino.
@gardenhead Es el mismo problema que, por ejemplo, tratar de enumerar todos los números racionales. Si comienzo a contar 1, 2, 3, ... nunca llegaré a 1/2.
La respuesta de Eric Wofsey es ciertamente más completa, pero pensé en proporcionar un ejemplo donde la garantía de que existe una prueba de $P$ o $\neg P$ que no es de la forma "hay un algoritmo sencillo, aunque tedioso, para verificar las cosas" como sucede en el caso de la Teoría de Ramsey o quién gana un juego como el Ajedrez.
La pregunta es acerca del "problema del número de besos" para la dimensión 5 (o cualquier dimensión más alta excepto 8 o 24). En 1D, dos intervalos de la misma longitud pueden tocarse sin superponerse. En 2D, 6 círculos de un radio dado pueden tocar un séptimo. No conocemos el número más alto de esferas de 5D de un radio fijo que pueden tocar todas la misma, pero la respuesta está entre 40 y 44, inclusive. Dado que estamos tratando con números reales, argumentaría que no hay un algoritmo obvio como con la Teoría de Ramsey: no podemos probar todos los posibles centros de las esferas.
Sin embargo, debido a que este tipo de pregunta se puede traducir en una afirmación simple sobre números reales (piensa en usar productos punto para lidiar con los ángulos, por ejemplo), solo depende de lo que sea cierto en cualquier "campo real cerrado" (un campo que actúa como los números reales para muchos propósitos algebraicos).
¡Lo interesante es que la teoría de campos reales cerrados es completa y decidible! Todo lo que se pueda expresar en el lenguaje de campos reales cerrados teóricamente se puede demostrar como verdadero o falso con un algoritmo, y son relativamente eficientes.
Este ejemplo no es mío, y se discute en varios lugares, incluyendo estas diapositivas sobre "Métodos formales en Análisis" por Jeremy Avigad.
¿Qué quieres decir con que 6 círculos pueden tocarse con un séptimo sin solaparse? ¿Tienen el mismo radio o algo así?
@NSZ, perdón por la confusión. Sí, todo debería tener el mismo radio. La página de Wikipedia que enlacé para el problema del número de besos tiene descripciones más precisas, así como algunas imágenes.
Tu respuesta y la otra de Eric Wofsey dan una frase que está parametrizada por un número natural, de manera que sabemos que es demostrable para algún parámetro de un conjunto finito, pero para el cual realmente no tenemos una prueba aún. Me gustaría saber si hay un ejemplo similar donde conozcamos la frase explícita. Por cierto, según esto, la eliminación de cuantificadores en RCF es doblemente exponencial, ¿es eso a lo que te refieres con "relativamente eficiente"? =)
¿Podría existir tal prueba de dependencia, o sería la única forma de probar que una afirmación es dependiente probándola/refutándola?
Me gustaría abordar esta pregunta específica. No es cierto en general que la existencia de una prueba de $P$ implique que $P$ en sí sea verdadero. Tampoco es cierto que la existencia de una prueba de demostrabilidad de $P$ implique la demostrabilidad de $P$. Según el teorema de Lob, cada uno de estos falla para alguna sentencia $P$, si tu sistema de fundamentos es lo suficientemente fuerte (la teoría de conjuntos ZFC es ciertamente más que suficiente). Para ser 100% precisos:
Toma cualquier sistema formal $S$ que cumpla con las condiciones de demostrabilidad de Hilbert-Bernays, donde $\def\box{\square}$"$\box_S P$" denota la sentencia aritmética uniforme que representa "$S$ demuestra $P$", y simplemente escribimos "$\box P$" si está en el contexto de "$S \vdash \cdots$". Entonces la forma externa del teorema de Lob (L* en el post vinculado) afirma que si $S \vdash \box P \to P$ entonces $S \vdash P$. Si $S$ es consistente, entonces $S \nvdash \bot$ y por lo tanto $S \nvdash \box \bot \to \bot$. Leído en inglés, esto muestra que $S$ no siempre prueba que la demostrabilidad implica verdad, incluso para frases individuales una por vez.
Se puede decir más al respecto. Si $S \vdash \box \box P \to \box P$ entonces nuevamente, por (L*), obtenemos $S \vdash \box P$. Si $S$ es $_1$-sólido entonces $S \nvdash \box \bot$, por lo que $S \nvdash \box \box P \to \box P$ no se cumple cuando $P = \bot. En inglés, S ni siquiera prueba que la existencia de una prueba de demostrabilidad implica demostrabilidad.
Curiosamente, incluso podría ser posible (pero ningún lógico lo cree) que ZFC sea consistente pero demuestre ¬Con(ZFC), lo que literalmente significa que ZFC demuestra la existencia de una prueba de contradicción sobre ZFC aunque no haya tal prueba...
Más específicamente, (en meta-sistemas muy débiles) podemos demostrar fácilmente que si ZFC es consistente entonces ZFC' = ZFC+¬Con(ZFC) también es consistente pero aún así ZFC' demuestra ¬Con(ZFC'). Por supuesto, cualquier persona que crea que ZFC es consistente debería rechazar ZFC' porque niega su propia consistencia. Pero el problema es que nunca podremos averiguar si ZFC en sí misma ya es como ZFC' en cuanto a ser consistente pero $_1$-insólido, a menos que encontremos realmente algo como una prueba concreta sobre ZFC de ¬Con(ZFC). Pero en realidad esperamos que ZFC sea $_1$-sólido, en cuyo caso nunca podemos establecerlo de manera no circular.
Ahora, para responder explícitamente la pregunta interpretada externamente, es posible que $S \vdash \box P \lor \box \neg P$ y aún así $S \nvdash P$ y $S \nvdash \neg P, ¡así que una 'prueba de dependencia' no es necesariamente un indicador confiable de dependencia real! Aquí hay una construcción explícita general:
Toma cualquier sistema formal $_1$-sólido $S$ que cumpla las condiciones de demostrabilidad de Hilbert-Bernays. Sea $S' = S + \box_S \box_S \bot. Entonces tenemos:
$S' \vdash \box_{S'} \box_S \bot \lor \box_{S'} \neg \box_S \bot$, ya que $S' \vdash \box_S P \to \box_{S'} P$ para cualquier sentencia $P$ sobre $S$.
$S' \nvdash \box_S \bot$, de lo contrario $S \vdash \box_S \box_S \bot \to \box_S \bot$, y por lo tanto $S \vdash \box_S \bot$ por (L*), contradiciendo la $_1$-solidez de $S$.
$S' \nvdash \neg \box_S \bot$, de lo contrario $S \vdash \box_S \box_S \bot \to \neg \box_S \bot$, pero $S \vdash \neg \box_S \box_S \bot \to \neg \box_S \bot$ por (D3), y por lo tanto $S \vdash \neg \box_S \bot$ contradiciendo el teorema de incompletitud de Gödel.
No estoy seguro de cómo estás aplicando el teorema de Löb en tu primera afirmación. Si tu afirmación formal es $\omega$-consistente (lo cual, como mencionas, es una afirmación más fuerte que simplemente consistente) entonces demostrar que existe una prueba implica que, de hecho, una prueba "realmente" existe, lo cual implica la verdad de la afirmación si tu sistema es sonido. El teorema de Löb dice que asumir la existencia de una prueba no ayuda mucho en el proceso de encontrar la prueba.
@cody: Resbalé un poco; aunque mi primera afirmación era correcta cuando se interpreta como "en general $S$ no prueba ( $\box \box P \to P$ )", y puede ser demostrada, no era lo que tenía en mente. También he expandido mi publicación para dar los detalles técnicos.
Tu primer párrafo parece usar "verdadero" de una manera confusa. Presumiblemente cada instancia de "verdadero" realmente significa "una consecuencia de S", y no verdad en algún modelo no especificado (o incluso en un sentido filosófico), ya que todas las siguientes declaraciones están calificadas $S \vdash$ o $S \nvdash$ o "$S$ no demuestra". ¿En el contexto de un modelo de $S$, si $S$ puede probar que existe una demostración de $P$, entonces es cierto que existe una demostración, lo que significa que $S$ puede probar $P$, y por lo tanto $P$ es verdadero.
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
¿No demostrar que existe una prueba constituiría una prueba?
17 votos
@Shaun: Sí, pero estoy hablando de una prueba de que existe una demostración de la conjetura o una prueba de que la conjetura es falsa (una prueba de que no es independiente).
0 votos
Ah, entiendo. Lo siento.
4 votos
Tarski ideó una axiomatización de la geometría euclidiana que es decidible. Por lo tanto, cualquier conjetura en geometría euclidiana es de este tipo, sujeta a la restricción de que sea expresable en el sistema de Tarski.
2 votos
El siguiente documento demuestra que si la conjetura de Dickson (una generalización de la conjetura de los primos gemelos) es cierta, entonces existe una extensión de la aritmética de Presburger que sigue siendo decidible pero es lo suficientemente fuerte como para expresar una variación de la conjetura de Goldbach (a saber, que todos los números pares pueden expresarse como la suma o diferencia de 2 primos): arxiv.org/pdf/1601.07099.pdf .