Pruebas formales y teorema de deducción

Question

En esta pregunta explicaré una idea que tuve sobre las pruebas formales básicas y el uso del Teorema de la Deducción.

Considero que una fórmula es consecuencia lógica de un conjunto A de fórmulas si y sólo si es verdadera en todos los modelos del conjunto A de fórmulas ( estructuras que satisfacen el conjunto de fórmulas A ). Además, estoy considerando una prueba formal de una fórmula de un conjunto A de fórmulas, como una lista finita de fórmulas que son o bien fórmulas de A, fórmulas lógicamente válidas ( instancias de esquemas de axiomas ) o fórmulas obtenidas mediante la aplicación de reglas de inferncia ( esquemas de axiomas ) a dos o más fórmulas preeceding en la lista.

Al mismo tiempo, por solidez, decir que tenemos una demostración formal de a partir del conjunto A, sería decir que :
$ A $

Ahora tengo una serie de preguntas...

En primer lugar, ¿es cierto que para todas las proposiciones (teoremas, etc) que simplemente afirman que una fórmula es una consecuencia lógica de un conjunto de fórmulas, no importa lo difícil que sea su (de la proposición) prueba formal, siempre es posible que sea representado por una larga cadena de "consecuencias lógicas"? He oído decir a un profesor que éste sería el tipo de prueba formal más "formal", una prueba formal que consistiera sólo en una cadena de consecuencias lógicas. Por ejemplo, para cualquier A, , ¿es posible representar la prueba formal de de A como :

$ A \\ 1\\2\\...\\ $

Si la respuesta es afirmativa, entonces pensé inmediatamente que podríamos utilizar el teorema de la deducción para transformarlo en la siguiente fórmula lógicamente válida :

$A(1(2(....)))$

Entonces, pensé que significaría que en realidad cualquier prueba formal en este estado más formal ( sólo cadenas de consecuencias lógicas) podría ser vista como posiblemente traducida a una fórmula lógicamente válida de nuestra lógica formal ( de primer orden, de segundo orden ... ) que tiene la forma de una implicación, y que tiene toda la información requerida y utilizada para probar a partir de A. ¿ Es cierto ? Pondré un ejemplo :

http://postimg.org/image/fcg318fsn/

Extrapolación, ignorar si es completamente errónea

Como analogía pensé en la tupla (4,3,2) en R^n que lleva toda la información necesaria sobre el polinomio 4x² + 3x + 2 .

Entonces, analógicamente, ¿podríamos ver una especie de "isomorfismo informal" entre el conjunto de todas las pruebas formales en ese estado "supuestamente riguroso" de única cadena de consecuencias lógicas y las fórmulas lógicamente válidas de nuestro lenguaje formal en esa forma ( cadena de implicaciones ) ?

Entonces sería posible traducir de un lado a otro las pruebas formales sobre ese estado y las implicaciones lógicamente válidas de nuestro lenguaje formal.

Muchas gracias.

Answer 1

El teorema de la deducción dice que si { $\gamma$ , $\alpha$ } $\vdash$ $\beta$ entonces $\gamma$ $\vdash$ ( $\alpha$$ \flecha derecha $$\beta$ ). Ahora se puede representar una prueba de $\gamma$ de $\alpha$ por una secuencia

$\alpha$

$\vdash$ $\beta$ 1

$\vdash$ $\beta$ 2

.

.

.

$\vdash$ $\gamma$ .

En consecuencia por el teorema de la deducción podemos obtener ( $\alpha$$ \flecha derecha $$\alpha$ ), ( $\alpha$$ \flecha derecha $$\beta1$ ), ..., ( $\alpha$$ \flecha derecha $$\gamma$ ). Repito para enfatizar que tenemos ( $\alpha$$ \flecha derecha $$\gamma$ ) teniendo el teorema de la deducción. Ahora existe un teorema que dice:

((p $\rightarrow$ q) $\rightarrow$ (p $\rightarrow$ (r $\rightarrow$ q))).

Así, para obtener ( $\alpha$$ \flecha derecha $($ \beta $$\rightarrow$$ \gamma $)) we substitute p with $ \alfa $, q with $ \gamma $, and r with $ \beta $ in ((p$ \flecha derecha $q)$ \flecha derecha $(p$ \flecha derecha $(r$ \flecha derecha $q))), and from ($ \alfa $$\rightarrow$$ \gamma $) we detach ($ \alfa $$\rightarrow$ ( $\beta$$ \flecha derecha $$\gamma$ )).

Repetimos este proceso, sustituyendo p por $\alpha$ q con ( $\beta$$ \flecha derecha $$\gamma$ ), y r con $\delta$ y entonces podemos separar ( $\alpha$$ \flecha derecha $($ \delta $$\rightarrow$ ( $\beta$$ \flecha derecha $$\gamma$ ))).

La trampa aquí viene en que debemos obtener ( $\alpha$$ \flecha derecha $($ \beta $$_n$$ \flecha derecha $$\gamma$ )) primero, y después ( $\alpha$$ \flecha derecha $($ \beta $$_m$$ \flecha derecha $($ \beta $$_n$$ \flecha derecha $$\gamma$ )) a continuación [donde "m"=(n-1)], hasta obtener finalmente ( $\alpha$ →(β1→(β2→(....→γ)))).

Supongamos ahora que tenemos ( $\alpha$ →(β1→(β2→(....→γ)))), y $\alpha$ . Por desprendimiento podemos obtener (β1→(β2→(....→γ)). Por lo tanto, si tenemos ( $\alpha$$ \flecha derecha $$\beta$ 1) también, podemos obtener $\beta$ 1 y, por tanto, (β2→(....→γ)). Finalmente podemos obtener ( $\alpha$$ \flecha derecha $$\gamma$ ).

Por tanto, la respuesta a su pregunta, creo, es "sí".

Pero, fíjate que el propio teorema de la deducción no nos da directamente tal transformación como sugiere tu post original. Utilizamos

((p $\rightarrow$ q) $\rightarrow$ (p $\rightarrow$ (r $\rightarrow$ q))) para que esto funcione.

Dicho esto, si tenemos el teorema de la deducción, entonces ((p $\rightarrow$ q) $\rightarrow$ (p $\rightarrow$ (r $\rightarrow$ q))), como podemos ver a continuación:

hypothesis          1 | (p→q)
hypothesis          2 || p
hypothesis          3 ||| r
detachment 1, 2     4 ||| q
conditional-in 3-4  5 || (r→q)
conditional-in 2-5  6 | (p→(r→q))
conditional-in 1-6  7 ((p→q)→(p→(r→q)))

Si tenemos {(p→(q→p)), ((p→(q→r))→((p→q)→(p→r)))} como base utilizada para demostrar el teorema de la deducción (existen otras bases) también podríamos demostrar ((p→q)→(p→(r→q))) como sigue:

axiom               1 (p→(q→p))
axiom               2 ((p→(q→r))→((p→q)→(p→r)))
1 p/q, q/r          3 (q→(r→q))
1 p/(q→(r→q)), q/p  4 ((q→(r→q))→(p→(q→(r→q))))
detachment 4, 3     5 (p→(q→(r→q)))
2 r/(r→q)           6 ((p→(q→(r→q)))→((p→q)→(p→(r→q))))
detachment 6, 5     7 ((p→q)→(p→(r→q))))

Si ignoramos las sustituciones aquí, parece que en este caso una prueba axiomática puede resultar más corta que una derivación por deducción natural.