Posterior: Coherencia y completitud Arriba: Deducción natural en el Anterior: Camenes

Formas clausulares

En esta sección presentaremos una forma canónica equivalente de cada fórmula bien formada en el cálculo de predicados. Dada una fórmula, contaremos con un algoritmo que nos permita llevar los cuantificadores que aparezcan en la fórmula al mismo inicio de esa fórmula, de manera que al proceder así con todos los cuantificadores quede un bloque de cuantificadores actuando sobre una fórmula sin cuantificador alguno. Al escribir esta última fórmula en una forma conjuntiva equivalente (que por lo general podemos presuponer que será precisamente la forma normal conjuntiva) obtendremos la forma clausular de la fórmula dada. Las formas clausulares son de suma importancia porque además de proporcionar un medio canónico de representar a las fórmulas, entrañan también un procedimiento natural para verificar que la fórmula sea válida. Esta última propiedad da orien a su vez a la llamada PROGRAMACIÓN L´OGICA, la cual plantea al cálculo de predicados como un lenguaje de programación. Inicialmente, probemos la siguiente

Proposición 3.2   Sea $\phi\in\mbox{\rm Fbf}(L)$ una fórmula donde no aparezca libre la variable $x$ y sea $\psi(x)$ una segunda fórmula con apariciones libres de $x$. Entonces en cualquier teoría $T$ de primer orden:

$$T \vdash \phi \land \forall x\,\psi(x)\ \leftrightarrow\ \forall x\,\left(\phi \land \psi(x)\right)$$ (7)

$$T \vdash \phi \lor \exists x\,\psi(x)\ \leftrightarrow\ \exists x\,\left(\phi \lor \psi(x)\right)$$ (8)

$$T \vdash \phi \lor \forall x\,\psi(x)\ \leftrightarrow\ \forall x\,\left(\phi \lor \psi(x)\right)$$ (9)

$$T \vdash \phi \land \exists x\,\psi(x)\ \leftrightarrow\ \exists x\,\left(\phi \land \psi(x)\right)%%\\$$ (10)

En esta proposición es importante que $x$ no aparezca libre en $\phi$. Por ejemplo, en ${\mathbb{R}}$ para $x=-1$ la siguiente fórmula es válida:

$$(x+1)=0\ \land\ \forall x\, \left(\left(\exists y :\, x=y\cdot y\right)\rightarrow x\geq 0\right)$$

sin embargo es claramente falsa la fórmula

$$\forall x\, \left((x+1)=0\ \land\ \left(\left(\exists y :\, x=y\cdot y\right)\rightarrow x\geq 0\right)\right).$$

Demostración
Probemos primeramente la fórmula (7). La fórmula (8) se seguirá entonces por el principio de dualidad. Escribamos las componentes de la equivalencia lógica que aparece en (7) en términos de $\neg$ y $\rightarrow$ exclusivamente. Obtenemos:

$$\neg\left(\phi \rightarrow \neg\forall x\,\psi(x)\right)\ \... ...ow\ \forall x\,\neg\left(\phi \rightarrow \neg\psi(x)\right)$$ (11)

Pues bien, la implicación $\leftarrow$ en (11) se reduce a probar que

$$\forall x\,\neg\left(\phi \rightarrow \neg\psi(x)\right)\ \vdash\ \neg\left(\phi \rightarrow \neg\forall x\,\psi(x)\right),$$

lo cual se demuestra como sigue:

1.

$\forall x\,\neg\left(\phi \rightarrow \neg\psi(x)\right)\rightarrow \neg\left(\phi \rightarrow \neg\psi(x)\right)$ ( $\mbox{\rm Ax}_4$)

2.

$\forall x\,\left(\neg\left(\phi \rightarrow \neg\psi(x)\right)\right)$ ( $\mbox{\rm Hip}$)

3.

$\neg\left(\phi \rightarrow \neg\psi(x)\right)$ ( $\mbox{\rm MP}\ 1,2$)

4.

$\neg\left(\phi \rightarrow \neg\forall x\,\psi(x)\right)$ ( $\mbox{\rm Gen}\ 3$)

Recíprocamente, para probar la implicación opuesta, procedamos a demostrar:

$$\neg\left(\phi \rightarrow \neg\forall x\,\psi(x)\right)\ \vdash\ \forall x\,\neg\left(\phi \rightarrow \neg\psi(x)\right),$$

lo cual puede hacerse como sigue:

1.

$\neg\left(\phi \rightarrow \neg\forall x\,\psi(x)\right)\rightarrow \neg\left(\phi \rightarrow \neg\psi(x)\right)$ ( $\mbox{\rm Teo}$)

2.

$\neg\left(\phi \rightarrow \neg\forall x\,\psi(x)\right)$ ( $\mbox{\rm Hip}$)

3.

$\neg\left(\phi \rightarrow \neg\psi(x)\right)$ ( $\mbox{\rm MP}\ 1,2$)

4.

$\forall x\,\left(\neg\left(\phi \rightarrow \neg\psi(x)\right)\right)$ ( $\mbox{\rm Gen}\ 3$)

El teorema del que partimos en la prueba anterior, el que aparece en el paso 1. de la prueba, es una consecuencia del Teorema de Deducción. En efecto, se tiene las equivalencias siguientes:

$$\begin{eqnarray*} && \vdash\ \neg\left(\phi \rightarrow \neg\forall x\,\psi(x)... ...htarrow& \vdash\ \forall x\,\psi(x)\ \rightarrow\ \psi(y) %%\\ \end{eqnarray*}$$

pero esto último se cumple precisamente porque ésta es una instancia del tipo de axiomas $\mbox{\rm Ax}_4$.

Probemos ahora la fórmula (9). La fórmula (10) se seguirá entonces por el principio de dualidad. Escribamos las componentes de la equivalencia lógica que aparece en (9) en términos de $\neg$ y $\rightarrow$ exclusivamente. Obtenemos:

$$\left(\neg\phi \rightarrow \forall x\,\psi(x)\right)\ \left... ...tarrow\ \forall x\,\left(\neg\phi \rightarrow \psi(x)\right)$$ (12)

Pues bien, la implicación $\leftarrow$ en (12) es una instancia del tipo de axiomas $\mbox{\rm Ax}_5$ y por tanto es un teorema. La implicación recíproca se obtiene por ``Generalización'' observando que

$$\left\{\left(\neg\phi \rightarrow \forall x\,\psi(x)\right), \neg\phi\right\}\ \vdash\ \psi(y)$$

como una consecuencia directa de Modus Ponens. $\quad\Box$ Si ${\cal Q}$ es uno de los cuantificadores $\forall$ o $\exists$, sea ${\cal Q}'$ el otro cuantificador, es decir, el cuantificador tal que $\{{\cal Q},{\cal Q}'\} = \{\forall,\exists\}$.

Proposición 3.3   Sea $\phi\in\mbox{\rm Fbf}(L)$ una fórmula donde no aparezca libre la variable $x$ y sea $\psi(x)$ una segunda fórmula con apariciones libres de $x$. Entonces en cualquier teoría $T$ de primer orden:

$$T \vdash \left(\phi \rightarrow {\cal Q} x\,\psi(x)\right)\ \leftrightarrow\ {\cal Q} x\,\left(\phi \rightarrow \psi(x)\right)$$ (13)

$$T \vdash \left({\cal Q} x\,\psi(x) \rightarrow \phi\right)\ \leftrightarrow\ {\cal Q}' x\,\left(\psi(x) \rightarrow \phi\right)%%\\$$ (14)

Demostración
En efecto, teniendo en cuenta las equivalencias lógicas enunciadas en la proposición 3.3.2, para (13), se tiene:

$$\begin{eqnarray*} \phi \rightarrow {\cal Q} x\,\psi(x) &\leftrightarrow& \neg\p... ...tarrow& {\cal Q} x\,\left(\phi \rightarrow \psi(x)\right) %%\\ \end{eqnarray*}$$

Para (14), se tiene:

$$\begin{eqnarray*} {\cal Q} x\,\psi(x) \rightarrow \phi &\leftrightarrow& \neg\l... ...arrow& {\cal Q}' x\,\left(\psi(x) \rightarrow \phi\right) %%\\ \end{eqnarray*}$$

$\quad\Box$

Definición 3.5   Sea $\phi(x_1,\ldots,x_n)\in\mbox{\rm Fbf}(L)$ una fórmula libre de cuantificadores (es decir, no contiene cuantificador alguno). Como en el cálculo proposicional, se dice que $\phi(x_1,\ldots,x_n)$ es una literal si es un átomo o la negación de un átomo. Una conjunción de literales es una frase y una disyunción de literales es una cláusula. Una forma conjuntiva es una conjunción de cláusulas y una forma disyuntiva es una disyunción de frases.

Proposición 3.4   Si $\phi(\mbox{\bf x})\in\mbox{\rm Fbf}(L)$ es una fórmula libre de cuantificadores, donde $\mbox{\bf x}=[x_1,\ldots,x_n]$ es la lista de sus variables, entonces se puede encontrar algorítmicamente sendas fórmulas $\psi(\mbox{\bf x})=:\mbox{\rm FC}(\phi(\mbox{\bf x}))$ en forma conjuntiva y $\chi(\mbox{\bf x})=:\mbox{\rm FD}(\phi(\mbox{\bf x}))$ en forma disyuntiva equivalentes ambas a $\phi(\mbox{\bf x})$.

Demostración
En efecto, procedamos por inducción en el número $k$ de conectivos presentes en $\phi(\mbox{\bf x})$.

Caso base. ($k=0$) Si $\phi(\mbox{\bf x})$ es un átomo, hacemos

$$\mbox{\rm FC}(\phi(\mbox{\bf x}))=\phi(\mbox{\bf x})=\mbox{\rm FD}(\phi(\mbox{\bf x})).$$

Caso inductivo. ($k>0$) Sea $*$ el conectivo principal en $\phi(\mbox{\bf x})$.

Si $*=\neg$ es la negación, entonces $\phi(\mbox{\bf x})=\neg\phi_1(\mbox{\bf x})$, y, según las Leyes de De Morgan:

• $\mbox{\rm FC}(\phi(\mbox{\bf x}))$ se obtiene de $\mbox{\rm FD}(\phi_1(\mbox{\bf x}))$ al intercambiar cada conectivo $\land$ por $\lor$ y viceversa, negando cada literal.
• $\mbox{\rm FD}(\phi(\mbox{\bf x}))$ se obtiene de $\mbox{\rm FC}(\phi_1(\mbox{\bf x}))$ al intercambiar cada conectivo $\land$ por $\lor$ y viceversa, negando cada literal.

Si $*=\land$ es la conjunción, entonces $\phi(\mbox{\bf x})=\phi_1(\mbox{\bf x})\land\phi_2(\mbox{\bf x})$, y:

• $\mbox{\rm FC}(\phi(\mbox{\bf x}))$ se obtiene al concatenar $\mbox{\rm FC}(\phi_1(\mbox{\bf x}))$ y $\mbox{\rm FC}(\phi_2(\mbox{\bf x}))$, vistos ambos como ``listas'' de cláusulas.
• $\mbox{\rm FD}(\phi(\mbox{\bf x}))$ se obtiene como la lista de frases formadas al concatenar cada frase en $\mbox{\rm FD}(\phi_1(\mbox{\bf x}))$ con cada frase en $\mbox{\rm FD}(\phi_2(\mbox{\bf x}))$.

Si $*=\lor$ es la disyunción, entonces $\phi(\mbox{\bf x})=\phi_1(\mbox{\bf x})\lor\phi_2(\mbox{\bf x})$, y:

• $\mbox{\rm FC}(\phi(\mbox{\bf x}))$ se obtiene como la lista de cláusulas formadas al concatenar cada cláusula en $\mbox{\rm FCC}(\phi_1(\mbox{\bf x}))$ con cada cláusula en $\mbox{\rm FC}(\phi_2(\mbox{\bf x}))$.
• $\mbox{\rm FD}(\phi(\mbox{\bf x}))$ se obtiene al concatenar $\mbox{\rm FD}(\phi_1(\mbox{\bf x}))$ y $\mbox{\rm FD}(\phi_2(\mbox{\bf x}))$, vistos ambos como ``listas'' de frases.

en cualquier otro caso, se reescribe $*$ en su forma equivalente en términos de los conectivos booleanos $\neg$, $\land$ o $\lor$ y se calcula las formas conjuntiva y disyuntiva de la fórmula equivalente. $\quad\Box$

Definición 3.6   Una fórmula $\phi(x_1,\ldots,x_n)\in\mbox{\rm Fbf}(L)$ se dice estar en FORMA PRENEX si es de la forma

$$\phi(x_1,\ldots,x_n) \equiv {\cal Q}_1 y_1\, {\cal Q}_2 y_2\, \cdots {\cal Q}_m y_m\, \psi(x_1,\ldots,x_n,y_1,\ldots,y_m)$$

donde cada ${\cal Q}_i$ es un cuantificador $\forall$ o $\exists$, y $\psi$ es una fórmula libre de cuantificadores. Si además $\psi(x_1,\ldots,x_n,y_1,\ldots,y_m)$ es una forma conjuntiva, entonces se dice que $\phi(x_1,\ldots,x_n)$ está en FORMA NORMAL PRENEX.

Así en una forma prenex, los cuantificadores sólo aparecen al inicio de ella.

Proposición 3.5   Para toda fórmula $\phi(\mbox{\bf x})\in\mbox{\rm Fbf}(L)$, donde $\mbox{\bf x}=[x_1,\ldots,x_n]$ es la lista de sus variables libres, existe una fórmula $\psi(\mbox{\bf x})\in\mbox{\rm Fbf}(L)$ en forma normal prenex equivalente a $\phi$. Más aún, $\psi$ es algorítmicamente constructible a partir de $\phi$.

Demostración
Procederemos por inducción en cuanto al número $k$ de cuantificadores que aparezcan en $\phi(\mbox{\bf x})$.

Caso base. ($k=0$) Si $\phi(\mbox{\bf x})$ es una fórmula libre de cuantificadores, calculamos $\psi(\mbox{\bf x})= \mbox{\rm FC}(\phi(\mbox{\bf x}))$ según se vió en la demostración de la proposición 3.3.4.

Caso inductivo. ($k>0$) Distinguiremos casos diversos atendiendo a la forma de $\phi(\mbox{\bf x})$.

Si $\phi(\mbox{\bf x})={\cal Q}_1 y_1\,\phi_1(\mbox{\bf x},y_1)$ es la cuantificación de una fórmula, entonces se calcula la forma normal prenex $\psi_1(\mbox{\bf x},y_1)$ de $\phi_1(\mbox{\bf x},y_1)$. La forma normal buscada será $\psi(\mbox{\bf x})={\cal Q}_1 y_1\,\psi_1(\mbox{\bf x},y_1)$.

Si $\phi(\mbox{\bf x})=\neg\phi_1(\mbox{\bf x})$ es la negación de una fórmula, entonces se hace ``actuar $\neg$ al nivel de átomos''. Es decir, mediante las reglas de transformación:

$$\begin{array}{lcl} \neg\forall x\, \phi(x) &\leadsto& \ex... ...2\right) \lor \left(\phi_2\land\neg\phi_1\right) \end{array}$$ (15)

se transforma $\neg\phi_1(\mbox{\bf x})$ a una fórmula $\phi_2(\mbox{\bf x})$ equivalente cuyo conectivo principal ya no es $\neg$. La fórmula $\psi(\mbox{\bf x})$ buscada será la forma normal prenex de $\phi_2(\mbox{\bf x})$.

Si $\phi(\mbox{\bf x})=\phi_1(\mbox{\bf x})*\phi_2(\mbox{\bf x})$ es una composición booleana de dos fórmulas, donde $*=\land$ o $*=\lor$, entonces se puede suponer que $\phi_2(\mbox{\bf x})$ posee un cuantificador (si fuera necesario podría intercambiarse a $\phi_2(\mbox{\bf x})$ con $\phi_1(\mbox{\bf x})$), digamos $\phi_2(\mbox{\bf x})={\cal Q}_2y_2\, \phi_{21}(\mbox{\bf x},y_2)$. Ya que $y_2$ no aparece en la lista de variables libres $\mbox{\bf x}$, si acaso $y_2$ aparece también en $\phi_1(\mbox{\bf x})$ entonces aparecería ahí como una variable ligada. En este caso renombramos a $y_2$, en su alcance en $\phi_1(\mbox{\bf x})$, como una nueva variable $y_2'$ de manera que $y_2$, en suma, no aparezca más en $\phi_1(\mbox{\bf x})$. De acuerdo con la proposición 3.3.2, $\phi(\mbox{\bf x})$ es entonces equivalente a ${\cal Q}_2y_2\, \left(\phi_1(\mbox{\bf x})*\phi_{21}(\mbox{\bf x},y_2)\right)$ y la fórmula $\phi_1(\mbox{\bf x})*\phi_{21}(\mbox{\bf x},y_2)$ posee un cuantificador menos. Sea pues $\psi_1(\mbox{\bf x},y_2)$ su forma normal prenex. Entonces la forma normal prenex de $\phi(\mbox{\bf x})$ será $\psi(\mbox{\bf x})={\cal Q}_2y_2\, \psi_{1}(\mbox{\bf x},y_2)$.

Si $\phi(\mbox{\bf x})=\phi_1(\mbox{\bf x})\rightarrow\phi_2(\mbox{\bf x})$ es una implicación de dos fórmulas, entonces una de las dos (o incluso ambas) $\phi_1(\mbox{\bf x})$ o $\phi_2(\mbox{\bf x})$ posee un cuantificador. Si acaso $\phi_2(\mbox{\bf x})={\cal Q}_2y_2\, \phi_{21}(\mbox{\bf x},y_2)$ podemos suponer (acaso mediante un renombramiento de variables) que $y_2$ no aparece en $\phi_1(\mbox{\bf x})$. De acuerdo con la relación (13) en la proposición 3.3.3, $\phi(\mbox{\bf x})$ es entonces equivalente a ${\cal Q}_2y_2\, \left(\phi_1(\mbox{\bf x})\rightarrow \phi_{21}(\mbox{\bf x},y_2)\right)$ y la fórmula $\left(\phi_1(\mbox{\bf x})\rightarrow \phi_{21}(\mbox{\bf x},y_2)\right)$ posee un cuanificador menos. Sea pues $\psi_2(\mbox{\bf x},y_1)$ su forma normal prenex. Entonces la forma normal prenex de $\phi(\mbox{\bf x})$ será $\psi(\mbox{\bf x})={\cal Q}_2y_2\, \psi_{2}(\mbox{\bf x},y_2)$. Si acaso $\phi_1(\mbox{\bf x})={\cal Q}_1y_1\, \phi_{11}(\mbox{\bf x},y_1)$ podemos suponer (acaso mediante un renombramiento de variables) que $y_1$ no aparece en $\phi_2(\mbox{\bf x})$. De acuerdo con la relación (14) en la proposición 3.3.3, $\phi(\mbox{\bf x})$ es entonces equivalente a ${\cal Q}'_1y_1\, \left(\phi_{11}(\mbox{\bf x},y_1)\rightarrow \phi_{2}(\mbox{\bf x})\right)$ y la fórmula $\left(\phi_{11}(\mbox{\bf x},y_1)\rightarrow \phi_{2}(\mbox{\bf x})\right)$ posee un cuanificador menos. Sea pues $\psi_1(\mbox{\bf x},y_1)$ su forma normal prenex. Entonces la forma normal prenex de $\phi(\mbox{\bf x})$ será $\psi(\mbox{\bf x})={\cal Q}'_1y_1\, \psi_{1}(\mbox{\bf x},y_1)$. $\quad\Box$
Posterior: Coherencia y completitud Arriba: Deducción natural en el Anterior: Camenes