jueves, 10 de enero de 2013

Teorema de la deducción y permutación de las hipótesis

El teorema de la deducción es el que afirma, por ejemplo, que de una demostración de p suponiendo q se puede concluir que q → p. Dicho teorema sirve para demostrar p → q →. p → q así: p → q, p ⊢ q luego p → q ⊢ p → q luego p → q →. p → q. Pero tal vez sea una forma más correcta de expresarse decir que lo que esto prueba es que existe la demostración de esta última fórmula, antes que ser la prueba de ella. De un modo bastante similar tenemos: p, p → q ⊢ q luego p ⊢ p → q → q luego p →. p → q → q. De nuevo, con esto probamos (en virtud de la prueba del teorema de la deducción) que tal prueba existe, pero no dijimos cual es en concreto (usando sólo el lenguaje objeto).

La prueba de Church proporciona en cierto sentido un modo de dar con una prueba. Veamos por ejemplo el primero de los dos ejemplos del post. El lector dirá probablemente que resulta más lógico probar primero p → p y luego sustituir p por p → q en dicho teorema. Eso se obtendría así:

ley de la reflexividad de la implicación material

1 [p →. p → p → p] →. [p →. p → p] →. p → p ; por sustitución en axioma 2.

2 p →. p → p → p ; sustitución en axioma 1

3 [p →. p → p] →. p → p ; modus ponens 1, 2

4 p →. p → p ;  sustitución en axioma 1

*5 p → p ; por modus ponens, 3, 4.
    

Luego, por sustitución en *5: p → q →. p → q

Pero a diferencia de p → q →. p → q, con p →. p  → q → q no podemos proceder así, apelando sencillamente a la reflexividad de →.

Primero tenemos que pasar de p, p → q ⊢ q a p  ⊢ p → q →. q. Aquí tenemos p → q en lugar de Aₙ y q de Bₘ (Cf. este post). Para cada B hay que probar Aₙ → B.


Como p es supuesto, sabemos como probar p ⊢ p → q → p. También sabemos probar p → q →. p → q. Tenemos que probar entonces p ⊢ p → q →. q. Y la parte derecha de dicha fórmula es nuestro Aₙ → Bₘ, con lo que usamos:

[Aₙ →. Bₖ → Bₘ] →. Aₙ → Bₖ →. Aₙ → Bₘ

 y sustiyendo:
[p → q →. Bₖ → q] →. [p → q] → Bₖ →. p → q. → q

y Bₖ es una las las líneas de la prueba de p, p → q ⊢ q. En este caso es una de las premisas: p. Así, nos queda

[p → q →. p → q] →. p → q → p →. p → q. → q

p → q →. p → q ya sabemos probarlo, obtenemos:

p → q → p →. p → q. → q 

Y como p es premisa, probamos también p ⊢ p → q → p. Una vez más modus ponens  y nos queda : 

p ⊢ p → q. → q

Ahora hacemos el paso que sigue. Sustituyendo en
[Aₙ →. Bₖ → Bₘ] →. Aₙ → Bₖ →. Aₙ → Bₘ

¿Cuál es Bₖ → Bₘ? Pues como vimos: 

** p → q → p →. p → q. → q

obtenemos pues:

[p →. [p → q → p] → [p → q. → q] ] →. p → [p → q → p] →. p → [p → q. → q] 

El antecedente se prueba por ** y lema 1. Obtenemos:

[p →. p → q → p] →. p →. p → q. → q

Y p →. p → q → p se obtiene en un paso del primer axioma, entonces:

p →. p → q. → q

Que es lo que queríamos probar.

Sin duda, ahora el lector querrá la prueba de algo un poco más general, a saber: [p →. q → r] → [q →. p → r], lo cual establece la posibilidad de permutación en general de las hipótesis en una deducción de modo que si de cualesquiera p y q se concluye r, se las puede suponer en cualquier orden, queda como ejercicio (o se lo encuentra acá).