Dada una declaración matemática, ¿por qué no hay Algoritmo que le diga si hay una prueba o una prueba de la declaración?

Por lo tanto, hay algunas herramientas para la generación de pruebas de algunas declaraciones matemáticas.

Sin embargo, dependiendo de la clase de lenguajes formales a la que pertenece la afirmación que uno intenta probar (o refutar), los teoremas de incompletitud de Godel limitan el poder de tales sistemas (al menos, para sistemas basados ​​en lógica de primer orden ). Es decir, siempre habrá [math] \ exist [/ math] una Statement [math] S [/ math] generada por Axioms [math] A [/ math] y Generation Rules [math] G [/ math], [math ] \ ni [/ math], la Proof(S) no converge .
En general, las declaraciones autorreferenciales sucumben al problema de detención , que es el equivalente teórico computacional del primer teorema de incompletitud de Godel .
La complejidad para probar / refutar declaraciones que pertenecen a diferentes idiomas formales también es diferente.

Aquí hay un pequeño documento que lo guiará en la generación de pruebas usando Kleene Algebra (básicamente, probando todas las declaraciones vinculadas en la clase de Idiomas regulares): http://www.diku.dk/hjemmesider/ansatte/henglein/papers/worthington2008.pdfH

(Tenga en cuenta que Proof-Generation(Kleene Algebra) [matemáticas] \ cong [/ matemáticas] Regular Languages [matemáticas] \ en [/ matemáticas] PSPACE )

Aquí hay un artículo general que habla sobre la madurez de diferentes sistemas de prueba de teoremas en diferentes lógicas de orden: Prueba de teorema automatizada

Si su pregunta quería saber si existe una máquina Oracle que pueda generar pruebas (o contradicciones) de TODOS los teoremas matemáticos establecidos, entonces la respuesta es NO . (Esto se deduce directamente del problema de detención )

La noción de expresividad de los sistemas lógicos es de suma importancia aquí. Podemos probar algunos, no podemos probar algunos.

Este es el problema Entscheidungs (alemán para “problema de decisión”) mencionado por primera vez por David Hilbert en 1928: ¿Existe un procedimiento mecánico general (es decir, un algoritmo) para determinar si una declaración matemática es un teorema o no?

No puede haber tal algoritmo. Este resultado fue mostrado por Alonzo Church e independientemente de él por Alan Turing en 1936. De hecho, fue precisamente el problema Entscheidungs ​​el que motivó el documento del seminario de Turing en el que las máquinas Turing se introdujeron por primera vez.

La prueba de Turing de la indecidibilidad del problema Entscheidungsproblem consiste en dar una representación en el lenguaje de la aritmética de primer orden de la afirmación de que una máquina de Turing eventualmente imprimirá el carácter [math] 0 [/ math] en alguna entrada. Esta propiedad es indecidible, y de esto obtenemos que el problema Entscheidungs ​​es indecidible.

Creo que la respuesta a su pregunta radica en los teoremas de incompletitud del godel . La esencia de los teoremas es que “no existe un algoritmo sólido y completo al mismo tiempo”, es decir, o el algoritmo dará un falso positivo (se infringe la solidez) o dará un falso negativo (se infringe la integridad).

Dices que entiendes la prueba de indisputabilidad del problema de detención. Eso hace que sea muy fácil explicar una razón por la cual no existe un algoritmo para determinar la validez de las declaraciones matemáticas. Las instancias del problema de detención son enunciados matemáticos.

Supongamos que existe una máquina Turing T que puede encontrar el valor de verdad de cualquier predicado.

Supongamos que le paso la entrada [P: P es falsa].

Si T dice que se puede probar (es decir, P = verdadero) => P = falso

de lo contrario, si T dice que puede ser refutado (es decir, P = falso) => P = verdadero

esto significa que T nunca puede probar o refutar P y, por lo tanto, se supone que T no existe.

Tal vez un ejemplo concreto como el problema del Castor ocupado te ayudaría a entender. Básicamente, pregunta que, dado un programa de computadora de tamaño n en una máquina Turing, ¿cuál es la mayor cantidad de 1 que se puede imprimir sin pasar por un bucle infinito? Suena fácil, ¿verdad? Todo lo que necesita hacer es ejecutar los programas que no van en un bucle infinito y ver cuánto tiempo tomó el más largo.

El único problema es que no sabemos cuáles continúan para siempre y cuáles se detienen. Solo sabemos la respuesta para n <5 porque estos programas son demasiado pequeños para hacer un bucle para siempre sin que lo sepamos. Sin embargo, una vez que obtienes una máquina Turing de 5 estados, hay programas que parecen que se repiten para siempre, pero no sabemos con certeza si lo hacen. Puede ser que de repente se detengan en el dígito [matemático] 10 ^ 10 ^ 10 [/ matemático] o tal vez nunca se detengan. No lo sabemos

Hay muchas declaraciones de matemáticas que son así. No sabemos si son verdaderas y no sabemos si son falsas. El problema es que existen preguntas que son más complejas que las máquinas que tenemos para resolverlas. Podríamos responder a estas preguntas si tuviéramos una computadora que tuviera memoria infinita y pudiera funcionar infinitamente rápido, pero nuestra red eléctrica no podría manejar los requisitos de energía de dicha computadora.

Hace unos años, he visto en clase que tal algoritmo no puede existir, al menos con una computadora convencional.

Según mis recuerdos, la Paradoja de Berry muestra que es imposible.

No pude encontrar información adicional y seguiré buscando.

Si alguien tiene más información, no dude en sugerir modificaciones 🙂