¿Es posible diseñar un algoritmo que pueda producir y probar continuamente nuevos teoremas y probar cosas con esos teoremas, dado un conjunto de axiomas? ¿Cómo sería este algoritmo?

Answer 1

Como enfoque básico del problema, proporcionaría las siguientes ideas. Puede elegir un lenguaje formal, un conjunto de axiomas y un conjunto de reglas de inferencia, y escribir algún algoritmo para generar algún teorema en ese lenguaje formal. Si tiene un conjunto finito de axiomas y un conjunto finito de reglas de inferencia, por supuesto, podrá generar todos los teoremas. Por lo general, puede tener un conjunto infinito de axiomas y un conjunto infinito de reglas de inferencia (básicamente porque cada axioma o regla de inferencia es un patrón que produce un conjunto infinito de oraciones o inferencias), pero puede enumerar esos axiomas y reglas de inferencia. puede generar de manera uniforme todos los teoremas. Pero surgen algunos problemas

– es posible que haya omitido un axioma importante o una regla de inferencia importante, esto le impedirá probar muchos teoremas importantes

– cómo separar los teoremas útiles de los no interesantes

– su enumeración nunca terminará, entonces, ¿cómo enumerar primero los interesantes?

– en el mejor de los casos, está enumerando todos los teoremas en un lenguaje formal específico, no todos los teoremas en todos los lenguajes formales posibles.

Por supuesto, hay una investigación masiva en matemáticas y ciencias de la computación sobre este tema, que pertenece al campo de la ‘demostración automática de teoremas’, y puede encontrar más información, por ejemplo, en esta página de Wikipedia

Prueba de teorema automatizada

Answer 2

Eso no es particularmente difícil. Gödel describió una forma de generar todos los teoremas demostrables a partir de una lista de axiomas. Simplemente usa cada una de las reglas de inferencia en todos los axiomas y teoremas probados previamente.

Lo difícil es crear teoremas significativos e interesantes. La fracción de esos entre todos los teoremas es extremadamente pequeña. Por ejemplo, en la teoría de números, verás todas las ecuaciones que involucran las operaciones aritméticas probadas en el camino, pero no es interesante que 14273 + 2743 – 2348/2 = 15842. Y el teorema que dice 14273 + 2743 – 2348/2 ≠ 15843 es aún menos interesante.

¿Cómo se separan los teoremas interesantes del resto?