Estimación de las propiedades metamatemáticas de las conjeturas

Question

Dado un sistema matemático formalizado (un conjunto de axiomas y reglas de deducción), ¿es posible estimar las propiedades metamatemáticas de las conjeturas en este sistema, como el número de pasos de deducción a partir de los axiomas antes de intentar su demostración?

¿Puede un sistema matemático tener en sí mismo una estructura suficientemente analizable que permita esa heurística?

Parece que, a través de la correspondencia Curry-Howard, el problema general podría ser NP-completo, y demostrar la existencia de una prueba (dentro de unos límites) sería probablemente tan difícil como el problema de detención. Así que la heurística podría limitarse a sistemas formales muy simples.

Lo pregunto por dos razones:

• me pregunto si la intuición matemática puede ser formalizada
• no conozco tales mecanismos en los demostradores de teoremas automatizados

tldr:

Dado un conjunto de pruebas, ¿es posible estimar la distancia de deducción y otras propiedades de enunciados aún no probados, ahorrando recursos durante la búsqueda de pruebas?

Answer 1

La cuestión de si $p$ es un teorema de $T$ es equivalente al problema de detención en cuanto $T$ es (computablemente axiomatizable, consistente y) lo suficientemente fuerte como para implementar la "aritmética básica" - esto es básicamente inmediato a partir de parte de la prueba del teorema de incompletitud de Godel (la representabilidad de todas las funciones computables en $T$ ).

Y "implementar la "aritmética básica"" es una muy requisito débil - La aritmética de Robinson que ni siquiera puede demostrar que todo número es par o impar(!), ya es suficiente. Incluso para teorías decidibles "simples" como la geometría euclidiana o la aritmética con sólo la adición este problema es bastante difícil _(ver aquí y aquí respectivamente)_ .

Todo esto apunta a una respuesta general negativa a su pregunta. Sin embargo, la pregunta está formulada con demasiada amplitud como para tener una respuesta definitiva, por lo que todavía hay un elemento de subjetividad. Pero yo me arriesgaría:

Para todos los sistemas y propiedades, excepto los más simples, el problema de decir si una fórmula tiene esa propiedad con respecto a ese sistema es indecidible; e incluso para sistemas y propiedades muy simples, este problema es casi siempre inviable computacionalmente.

Obsérvese que la correspondencia Curry-Howard no desempeña realmente un papel en este caso: para obtener resultados de "límites inferiores" sólo tenemos que incrustar procesos computacionales en sistemas formales, y esto es bastante fácil en muchas situaciones.