Si un humano puede demostrar algo, ¿puede un ordenador demostrarlo?

Question

Me metí en una discusión bastante intensa con un amigo sobre hasta qué punto podemos esperar una interpretación completamente formalista de las matemáticas. Hay que reconocer que no sé mucho sobre las (muchas) teorías de los fundamentos de las matemáticas y, viniendo de la geometría, la idea de que todo lo que tenemos actualmente (con pruebas procedentes de una gran cantidad de lugares, conexiones con la física, EDP, etc.) podría demostrarse con algún tipo de algoritmo finito es algo que no puedo interiorizar.

Tomemos algo en lo que, por ejemplo, la prueba sea construir algún tipo de ejemplo patológico, digamos la función de Weierstrass o algo así. Ahora hay una prueba de "existe una función continua en todas partes y diferenciable en casi todas partes" simplemente escribiendo esta función. Pero dado que dicha función se construyó utilizando la "intuición" y la "motivación" matemáticas, no estoy seguro de qué esperanza, si es que hay alguna, existe para formalizar dichas pruebas.

¿Se espera que cualquier prueba dada por una persona pueda ser encontrada por un proceso algorítmico finito que comience con, digamos, ZFC y cualquier otra cosa extra que a veces se agrega a esto? ¿Se espera que todas las pruebas actuales en geometría puedan darse en algún tipo de sistema axiomático razonable?

Answer 1

Se cree que (efectivamente) todos los teoremas matemáticos clásicos y sus pruebas pueden ser mapeados a teoremas y pruebas en ZFC. Estas pruebas podrían ser verificadas por un ordenador, pero no necesitaríamos que el ordenador diera los pasos del argumento por sí mismo para que la prueba fuera formalizada, sino que los verificara.

Esto no quiere decir que no haya ningún interés o progreso en hacer que los ordenadores intenten generar automáticamente una prueba por sí mismos... este es un campo activo. Y en un sentido estricto, un ordenador siempre puede hacerlo. Puede simplemente enumerar todas las pruebas posibles. Si el teorema tiene una prueba, eventualmente la escupirá.

Obviamente, esto no es factible en la vida real. Y también sólo funciona si sabemos que hay una prueba. De lo contrario, el ordenador seguirá enumerando las pruebas y no podremos saber si la prueba del enunciado en cuestión no existe o simplemente no es una que hayamos enumerado todavía. Podríamos hacernos los listos y buscar paralelamente las pruebas de su negación, pero según el teorema de Godel hay enunciados que ni ellos ni su negación son demostrables.