Gödel dice que hay declaraciones verdaderas que no se pueden probar, dado un sistema axiomático sólido. ¿Alguien dice algo sobre la demostrabilidad de la demostrabilidad de las declaraciones?
¿Sigue siendo una pregunta abierta que todo enunciado lógico que sea demostrable pueda probarse como demostrable? ¿O, de manera equivalente, que se puede demostrar que todo enunciado improbable es indemostrable?
O más específicamente, ¿sigue siendo una pregunta abierta si un subconjunto de los enunciados demostrables (por ejemplo, los verdaderos) siempre puede probarse como demostrable/no demostrable para que algún día podamos llegar a la conclusión de que todos los teoremas verdaderos demostrables pueden ser probado para ser demostrable?
Creo que mi pregunta puede estar un poco fuera de la caja. Intentaré ser más claro.
Gödel no especificó la clase de declaraciones que son indecidibles. ¿Qué pasa si, por ejemplo, todos los teoremas verdaderos que no se pueden demostrar tienen alguna propiedad P.
siendo P la propiedad 'inútil a todos los efectos prácticos'.
Entonces sabríamos que aunque hay teoremas verdaderos que no se pueden demostrar, son teoremas inútiles. Espera un minuto... ¿existe tal cosa como un teorema inútil?
Es una característica central de todos los principales sistemas formales que cuando un enunciado es demostrable, entonces es demostrablemente demostrable. De hecho, esta característica es una de las condiciones de derivabilidad que se usa comúnmente en la prueba del teorema de incompletitud, y es fundamental para la prueba de Goedel del segundo teorema de incompletitud.
Pero también, podría agregar, este principio es claramente algo que queremos tener en nuestros sistemas formales. Si puede probar un enunciado, significa que tiene una prueba finita, una secuencia de enunciados, cada uno de los cuales es un axioma o se sigue de los enunciados anteriores mediante una de las reglas de deducción, y que termina demostrando el enunciado. Comprobar que una prueba es realmente una prueba debe ser una tarea rutinaria. Por lo tanto, siempre que un enunciado sea demostrable, deberíamos esperar que podamos probar que es demostrable, ya que esto equivale simplemente a probar que la prueba es realmente una prueba, que es algo sobre lo que habrá poco desacuerdo.
Así que sí, de hecho, en cualquiera de los sistemas formales usuales, cada vez que un enunciado es demostrable, entonces también podemos probar que es demostrable.
Se puede introducir la modalidad de demostrabilidad, escribiendo Box φ para indicar que φ es demostrable (en algún sistema formal fijo en discusión). En esta terminología modal, el principio de que todo enunciado demostrable es demostrablemente demostrable es el axioma:
y este axioma se conoce como axioma 4 en la teoría modal S4 .
Existe una prueba de que cierta clase de declaraciones geométricas se pueden resolver mediante una máquina de Turing en un tiempo finito.
Este resultado fue un derivado del décimo problema de Hilbert, en el que preguntó si todas las ecuaciones aritméticas se pueden resolver mediante un algoritmo, que fue respondido negativamente en 1970.
Surgió una pregunta análoga sobre la posibilidad de un algoritmo que probaría cualquier afirmación verdadera en geometría elemental y refutaba cualquier afirmación falsa. Resulta que ese algoritmo sí existe, aunque es inútil a efectos prácticos porque es tan ineficiente que se necesitaría más tiempo que la existencia del Universo para resolver un problema usando dicho algoritmo.
Sin embargo, debido a que el algoritmo anterior existe en principio, puede tomar su existencia como prueba de que todas las declaraciones geométricas verdaderas son demostrables.
DBK
Miguel
DBK