Cuatro técnicas de deducción

Las herramientas de partida

En la clase sobre sistemas deductivos formales se fijó el sistema de Łukasiewicz. Su lenguaje es la lengua de círculos y discos, escrita con las abreviaturas oficiales de la clase sobre el lenguaje de la lógica proposicional; sus axiomas son todas las instancias de los tres esquemas siguientes, donde $\varphi$, $\psi$ y $\chi$ son fórmulas cualesquiera, y su única regla es el modus ponens.

• A1: $(\varphi \rightarrow (\psi \rightarrow \varphi))$.
• A2: $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$.
• A3: $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$.
• MP: de $\varphi$ y $(\varphi \rightarrow \psi)$ se deduce $\psi$.

Una deducción de $\varphi$ desde un conjunto $\Gamma$ de fórmulas es una sucesión finita de fórmulas que termina en $\varphi$ y en la que cada fórmula es un axioma, un elemento de $\Gamma$ o el resultado de aplicar el modus ponens a dos fórmulas anteriores; si existe, se escribe $\Gamma \vdash \varphi$, y si $\Gamma$ es vacío, $\vdash \varphi$, y se dice que $\varphi$ es un teorema. En esa misma clase se demostraron los metateoremas que usaremos aquí: la presunción (Pre: si $\varphi \in \Gamma$, entonces $\Gamma \vdash \varphi$), la monotonía (Mon: si $\Gamma \subseteq \Delta$ y $\Gamma \vdash \varphi$, entonces $\Delta \vdash \varphi$), el modus ponens derivado (si $\Gamma \vdash \varphi$ y $\Gamma \vdash (\varphi \rightarrow \psi)$, entonces $\Gamma \vdash \psi$), el corte (Corte: si $\Gamma \vdash \varphi_{i}$ para cada $i$ de $1$ a $n$ y $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, entonces $\Gamma \vdash \psi$), el carácter finito (si $\Gamma \vdash \varphi$, algún subconjunto finito de $\Gamma$ basta), el teorema de deducción (TD: si $\Gamma \cup \{\varphi\} \vdash \psi$, entonces $\Gamma \vdash (\varphi \rightarrow \psi)$) y su recíproco (RTD), y el teorema $\vdash (\varphi \rightarrow \varphi)$, que en las justificaciones abreviaremos Id. Por último, $\varphi \dashv\vdash \psi$ (equivalencia probada) significa que $\{\varphi\} \vdash \psi$ y $\{\psi\} \vdash \varphi$.

Conviene recordar que $\neg$ y $\rightarrow$ no son signos de la lengua base, sino abreviaturas: $\neg\varphi$ es la cadena $(\varphi \downarrow \varphi)$, y $(\varphi \rightarrow \psi)$ es $(\neg\varphi \vee \psi)$, es decir, $\neg(\neg\varphi \downarrow \psi)$. Los tres axiomas hablan solo de negaciones y de implicaciones, y la misma clase mostró, con una marca de $0$ y $1$ que ellos y el modus ponens conservan, el límite que de ello se sigue: en el sistema de Łukasiewicz, desde $(v_{1} \downarrow v_{2})$ no se deduce $(\neg\neg v_{1} \downarrow v_{2})$, y la negación conjunta queda en parte fuera de su alcance. Esta clase procede, por tanto, en dos tiempos. Hasta la doble negación inclusive, $\vdash$ se refiere al sistema de Łukasiewicz, y nada de lo que se demuestra depende de desplegar las abreviaturas. Demostrada la doble negación, se añade al sistema una segunda regla primitiva, el reemplazo de la doble negación, que actúa sobre la cadena desplegada; desde ese punto, $\vdash$ se refiere al sistema del curso, el de Łukasiewicz más esa regla. Como toda deducción del primero es también deducción del segundo, nada de lo demostrado antes se pierde.

Dos estilos de deducción

Hay dos maneras de escribir una deducción, y ambas se usarán. La primera es la deducción propiamente dicha, una sucesión de fórmulas en la que cada línea es un axioma, una premisa o el resultado del modus ponens; cada línea se justifica con A1, A2, A3, Premisa o MP$(i, j)$, donde la línea $i$ es el antecedente y la línea $j$ es la implicación cuyo antecedente es exactamente la línea $i$ (y, desde que se introduzca la regla nueva, RDN$(i)$). La segunda es la deducción sobre deducciones, cuyas líneas no son fórmulas, sino afirmaciones de la forma $\Gamma \vdash \varphi$; cada una se justifica con un metateorema ya demostrado, y la sucesión entera es un razonamiento del metalenguaje que garantiza que existe una deducción del primer estilo, aunque no la escriba. Las justificaciones de este segundo estilo se leen como sigue.

• Pre: la fórmula de la derecha pertenece al conjunto de la izquierda.
• A1, A2, A3: la fórmula de la derecha es una instancia del esquema; una instancia de un axioma se deduce desde cualquier $\Gamma$ con una deducción de una sola línea.
• MP$(i, j)$: el modus ponens derivado, aplicado a la línea $i$, $\Gamma \vdash \varphi$, y a la línea $j$, $\Gamma \vdash (\varphi \rightarrow \psi)$, con el mismo $\Gamma$.
• TD$(i)$ y RTD$(i)$: el teorema de deducción o su recíproco, aplicado a la línea $i$.
• El nombre de un teorema ya demostrado, como Id o DN: la fórmula de la derecha es una instancia de ese teorema, y se deduce desde cualquier $\Gamma$ por monotonía, porque el conjunto vacío está contenido en $\Gamma$.
• Premisa, en una deducción sobre deducciones: la línea es una de las hipótesis de la regla que se está demostrando.

Todo resultado de esta clase se enuncia con metavariables y vale, por tanto, para fórmulas cualesquiera: su demostración es un esquema, y al reemplazar en ella cada metavariable por una fórmula se obtiene otra demostración correcta, porque las instancias de un esquema de axioma siguen siéndolo y cada modus ponens sigue siéndolo (lo mismo valdrá para cada aplicación de la regla nueva). Así, de $\vdash (\varphi \rightarrow \varphi)$ se sigue $\vdash (\neg\psi \rightarrow \neg\psi)$, con $\neg\psi$ en lugar de $\varphi$. Este recurso, aplicar un resultado a una fórmula más compleja que la del enunciado, es el que más rinde en lo que sigue.

Del resultado a la regla

Las técnicas de esta clase se demuestran desde premisas fijas, como $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$; pero se usan en medio de deducciones con otras premisas, donde $(\varphi \rightarrow \psi)$ y $(\psi \rightarrow \chi)$ no son premisas, sino fórmulas ya deducidas. El lema siguiente, consecuencia directa de la monotonía y del corte, autoriza ese uso de una vez para siempre.

De ello se sigue que cada técnica demostrada desde premisas tiene tres presentaciones: el resultado mismo, el teorema que se obtiene descargando sus premisas y la regla que se aplica bajo cualquier $\Gamma$. En una deducción sobre deducciones, la regla se invoca con el nombre de la técnica y los números de las líneas a las que se aplica, como SH$(3, 4)$, y el lema garantiza que el paso es legítimo.