¿Es posible probar que encontramos la prueba más corta?

Question

Consideraciones iniciales: mediante deducción natural como un sistema lógico, estamos limitados a la lógica proposicional, y tenemos un conjunto fijo de reglas básicas de inferencia. Supongamos que no podemos utilizar cualquier teoremas de la lógica de inmediato, y si queremos usar uno tenemos que insertar una prueba de ello en nuestro argumento.

Luego construimos una prueba de un arbitrario instrucción de esta manera. Mi pregunta es la siguiente, ¿hay una manera de averiguar si nuestra prueba es la más corta que puede ser construido en un sistema lógico. El menor significa el uno con el menor número de pasos, donde cada paso corresponde a una de las reglas básicas o premisa introducción.

Answer 1

Deje $N$ el número de pasos de la prueba de su declaración. Ahora mira en el conjunto de todas las pruebas de longitud de $< N$. Este es un conjunto finito de pruebas. Uno puede programar un ordenador para enumerar todas las pruebas de longitudes entre los $1$ e $N-1$, hacer una lista de las declaraciones que cada uno de ellos probar y, a continuación, para buscar a través de la lista para ver si su declaración se produce. Cualquiera que sea el resultado de esta búsqueda, se han determinado de una manera o de otra, si un menor prueba de su afirmación de que existe.