Teorema de deducción

[alexpglez]

Hoy voy a tratar un teorema importantísimo en lógica y matemáticas conocido como el teorema de deducción.
Es recomendable haber leído la entrada anterior sobre el sistema deductivo formal $K_L$, que es lo que utilizaremos hoy.

En lógica, al menos lingüísticamente hablando, es bastante diferente deducir una proposición de otra ($\Gamma, \alpha \vdash \beta$), de deducir que esa proposición implique la siguiente $\Gamma \vdash \alpha \rightarrow \beta$. Sin embargo, cualquiera puede pensar que hay una relación entre ambas casi de equivalencia, y esto es cierto: es lo que queremos demostrar.

¿Cuál sería la ventaja de tener un teorema de éstas carácterísticas? Deducir $\Gamma, \alpha \vdash \beta$ suele ser extremadamente más simple que deducir $\Gamma \vdash \alpha \rightarrow \beta$, ahorrando muchos pasos y recurrir a los axiomas de $K_L$.
A modo de ilustración, intente el lector deducir el Modus Barbara $\alpha \rightarrow \beta, \beta \rightarrow \gamma \vdash \alpha \rightarrow \gamma$ utilizando el teorema deducción. Es decir, demuestre el lector que $\alpha \rightarrow \beta, \beta \rightarrow \gamma, \alpha \vdash \gamma$. Compare la demostración con la equivalente sin usar el teorema de deducción (que está en la entrada anterior).

Teorema de deducción: $\Gamma, \alpha \vdash \beta$ y existe una deducción de $\beta$ en la que no se generalice con respecto a las variables libres de $\alpha$. Entonces $\Gamma \vdash \alpha \rightarrow \beta$.
- Demostración del teorema:
Veamos por inducción sobre los casos posibles de demostración. Es decir, sabemos que existe una deducción en $K_L$, sólo debemos recorrer todos los casos posibles de demostración en K_L. Tenemos 3 casos, que $\beta$ sea un axioma o premisa, que se deduzca del Modus Ponens o de la Introducción del Generalizador.
Caso 1: $\beta$ es un axioma o premisa (está en $K_L$ o en el conjunto de fórmulas $\Gamma$).

$$\beta$$

$$\beta \rightarrow (\alpha \rightarrow \beta)$$

$$\alpha \rightarrow \beta$$

Caso 2: $\beta$ es consecuencia de aplicar el Modus Ponens a dos fórmulas $\gamma, \gamma \rightarrow \beta \vdash \beta$.
Por hipótesis ya hemos construido una deducción de las dos fórmulas anteriores, y por tanto hemos deducido que $\Gamma \vdash \alpha \rightarrow \gamma$ y $\Gamma \vdash \alpha \rightarrow (\gamma \rightarrow \beta)$. Deducción que por hipótesis llevamos a cabo siguiendo estos 3 casos.

$$\alpha \rightarrow \gamma$$

$$\alpha \rightarrow (\gamma \rightarrow \beta)$$

$$(\alpha \rightarrow (\gamma \rightarrow \beta))\rightarrow ((\alpha \rightarrow \gamma) \rightarrow (\alpha \rightarrow \beta))$$

$$(\alpha \rightarrow \gamma) \rightarrow (\alpha \rightarrow \beta)$$

$$\alpha \rightarrow \beta$$

Caso 3: $\beta$ es consecuencia de introducir el generalizador en otra fórmula, es decir $\beta \equiv \forall x \gamma$, y además x no está libre en $\alpha$.
Por hipótesis tenemos que $\alpha \rightarrow \gamma$:

$$\alpha \rightarrow \gamma$$

$$\forall x (\alpha \rightarrow \gamma)$$

Como $x$ no está libre en $\alpha$:

$$\forall x (\alpha \rightarrow \gamma) \rightarrow (\alpha \rightarrow \forall x \gamma)$$

$$\alpha \rightarrow \forall x \gamma$$

$$\alpha \rightarrow \beta$$

Luego si existe una deducción de $\beta$, siempre podremos deducir $\alpha \rightarrow \beta$, QED (quod erat dmostrandum, que proviene del latín y significa: lo que se quería demostrar). Es sencillo demostrar a su vez el recíproco, si $\Gamma \vdash \alpha \rightarrow \beta$, entonces $\Gamma, \alpha \vdash \beta$.


Este teorema en la práctica se usa para suponer $\alpha$, llegar a una consecuencia interesante $\beta$ y en la siguiente línea escribir $\alpha \rightarrow \beta$:

$$\alpha$$

$$...$$

$$\beta$$

$$\alpha \rightarrow \beta$$

Quiero a su vez recalcar que en la deducción no se puede generalizar respecto a variables libres de $\alpha$, lo que nos llevaría a fórmulas falsas. Por ejemplo supongamos a modo de ilustración que tratamos con variables numéricas:

$$x=y$$

$$\forall xy \; x=y$$

$$2=3$$

$$x=y \rightarrow 2=3$$

$$\forall xy \; x=y \rightarrow 2=3$$

$$0=0 \rightarrow 2=3$$

$$0=0$$

$$2=3$$

Luego $\vdash 2=3$, lo cuál es completamente falso.

- Ejemplos
1) A modo de ilustración veamos el siguiente ejemplo en la vida real, (advertimos que debido a la "equivalencia natural" mencionada anteriormente, el ejemplo no es muy simbólico). Sabemos según nuestra experiencia (o leyes físicas si se quieren, contenidas en ciertas fórmulas $\Gamma$), que cuando cae un rayo, podemos deducir que se escucha un trueno, representaremos a cada proposición $R$ y $T$ respectivamente. Es decir que $\Gamma, R \vdash T$, aplicando el teorema de deducción tenemos que $\Gamma \vdash R \rightarrow T$, es decir que hemos deducido que cuando cae un rayo se escucha un trueno.

2) Otro ejemplo más matemático pudiera ser el siguiente. Consideremos el lenguaje usual de la artimética, que en particular tiene un cierto funtor diádico $x \cdot y$ llamado multiplicación y que sigue la propiedad asociativa $\forall xyz \; ((x\cdot y)\cdot z= x \cdot(y \cdot z))$ y abreviamos $x \; | \; y \equiv \exists z\; y=x \cdot z$ expresión que se puede leer como "x divide a y". Entonces: $\vdash \forall xyz \; (x \; | \; y \wedge y \; | \; z \rightarrow x \; | \; z)$
Demostración:
Supongamos que $x \; | \; y \wedge y \; | \; z$. Luego $\exists u \; y=x \cdot u$ y $\exists w \; z=y \cdot w$ luego , utilizando la propiedad asociativa $z=(x \cdot u) \cdot w=x \cdot (u \cdot w)$. Es decir que existe otro $u'=(u \cdot w)$ tal que $z= x \cdot u'$, o expresado en lenguaje lógico: $\exists u \; z=x \cdot u \; \equiv \; x \; | \; z$.
Tenemos entonces que $x \; | \; y \wedge y \; | \; z \vdash x \; | \; z$. No hemos generalizado respecto a $x$ o $y$, luego podemos utilizar el teorema de deducción y entonces $\vdash x \; | \; y \wedge y \; | \; z \rightarrow x \; | \; z$. Ahora introducimos el generalizador para las 3 variables:

$$\vdash \forall xyz \; (x \; | \; y \wedge y \; | \; z \rightarrow x \; | \; z)$$

"Si $x$ divide a $y$ e $y$ divide a $z$, entonces $x$ divide a $z$", QED.


Referencia: Carlos Ivorra, Lógica Matemática cap. 2