Son todas las pruebas "lo suficientemente corto como" ser calculada?

Question

El Completura Teorema de la Lógica Proposicional dice que una afirmación tautológica tiene una derivación.

¿Esta existencia implica que esta derivación se compone de un número finito de formación de la secuencia?

No sé si hay una conclusión, que requeriría de infinitos pasos, aunque (salvo cuando hay una inducción de la regla), es decir, en este sentido un unexecutable prueba. Pero no sé por qué sería excluido. Si no, ¿dónde está este obstáculo?

Y hay pruebas, que pueden ser "encontrado", pero no se puede hacer? En el sentido de que su idea puede ser visto de forma explícita, pero ellos no pueden ser ejecutadas en tiempo finito $-$, incluso en regla general.

Answer 1

Pruebas/derivaciones son, por definición, finito. Así que sí, cada tautología tiene un finito derivaciones.

Permitiendo que las pruebas a ser infinito llevaría a absurdos tales como esta la prueba de $1=0$ en un sistema donde la $\mathscr P\to\mathscr P$ es un axioma lógico:

$$\begin{array}{rll} 1.&1=0\to 1=0 & \text{Ax}\\ 2.&1=0\to 1=0 & \text{Ax}\\ 3.&1=0\to 1=0 & \text{Ax}\\ 4.&1=0\to 1=0 & \text{Ax}\\ \vdots&\vdots\\ (\infty-3).&1=0 & \text{MP}, 1, (\infty-4) \\ (\infty-2).&1=0 & \text{MP}, 1, (\infty-3) \\ (\infty-1).&1=0 & \text{MP}, 1, (\infty-2) \\ \infty.&1=0 & \text{MP}, 1, (\infty-1) \\ \end{array}$$ Se puede comprobar que cada línea de la siguiente manera por una aplicación válida de la indicada en la regla de líneas antes de la derivación.

Con el fin de demostrar que el sistema formal con infinitas derivaciones es el sonido, uno tendría que requiere, al menos, que el orden de las líneas en una derivación es un bien de orden - y si ese es el caso y cada regla de inferencia tiene un número finito de premisas, entonces se puede demostrar que todo lo que tiene una derivación también tiene un finito derivación. Así que no hay ningún punto en el considerando incluso este tipo de infinitas derivaciones.

---

Sin embargo, dependiendo de los detalles de cómo configurar su sistema formal, es muy posible que no son de corto plazo(ish) comprobable declaraciones de cuyas derivaciones (aunque finita) debe ser demasiado larga para ser escrito en cualquier lugar dentro del universo observable. A veces, esto puede ser ayudado por el uso de más potente (por ejemplo, teniendo en cuenta el Teorema de la Deducción de una primitiva regla de inferencia en lugar de un meta-resultado de la ayuda enormemente en muchas pruebas de tamaño); a veces no se puede.

Answer 2

Sí, cada prueba en la lógica proposicional se compone de un número finito de formación de la secuencia.

Sí, las "pruebas" puede llegar a encontrar que no puede hacerse en términos del mundo real de la potencia de computación/mano-escritura. En definitiva, tenemos una cantidad finita de la potencia de computación antes de que todos nuestros equipos de dejar de existir, y nosotros, como especie, también. Una prueba consiste de una secuencia finita de fórmulas (wffs), que termina con un teorema, donde cada fórmula consigue inferir válidamente por medio de una regla de inferencia o califica como un axioma. Nada dice de las pruebas no puede estúpidamente secuencias de repetición que ir a ninguna parte que la prueba no ha ido ya. Por ejemplo, he aquí una prueba (en notación polaca y en un sistema de deducción natural) de la ley débiles de la identidad:

1 | p assumption
2 | App 1 disjunction introduction
3 | KpApp 1, 2 conjunction introduction
4 | p 3 conjunction elimination
5 | App 4 disjunction introduction
6 | KpApp 4, 5 conjunction introduction
7 | p 6 conjunction elimination
8 Cpp 1-7 conditional introduction

Ahora, por supuesto, existe un pequeño punto en los pasos 5 a 7 en condiciones de probar el teorema (e incluso los pasos 2 a 4, pero estoy divagando). Pero, las pruebas de "existir" (en principio), que se repite a la larga de las fórmulas de los pasos 2-4 una y otra vez, aparentemente sin fin inmediato de partida, después del paso 4, y al final Cpp después de la última larga. Así, dicen que todos los de la potencia de cálculo en el multiverso/universo podría escribir sólo el 10$^{1,000,000}$ de las subsecuencias en cualquier secuencia de fórmulas. Así, una secuencia de fórmulas con el 10$^{2,000,000}$ de las subsecuencias, y, a continuación, Cpp después de que el pasado subsequence todavía califica como una prueba, aun cuando por hipótesis de los recursos materiales para escribir tal prueba no existe (por no hablar de cualquier tipo de ser que nunca iba a leer!).

Así que, sí, existen pruebas que pueden llegar a "encontrar", pero no se hace.