Tableros Semánticos en Lógica de Primer Orden

El mismo método que hemos presentado en la primera parte de este tema, el de Tableros Semánticos para LP, es extensible a LPO aunque, obviamente, para ello hemos de tener en cuenta las particularidades que presenta esta lógica.

Recordemos que LPO es una lógica que extiende LP permitiendo el uso de cuantificadores e introduciendo algunos elementos adicionales que lo convierten en una opción más flexible y expresiva, a costa de ser más compleja, claro:

Igual que LPO extiende LP, el método de Tableros Semánticos que veremos para LPO se obtendrá añadiendo métodos para manipular los nuevos operadores de construcción, pero el mecanismo general sigue siendo el mismo de clasificar fórmulas según su tipología y aplicar reglas de reducción según la clasificación.

Clasificación de fórmulas

Fórmulas $dN$, $\alpha$ y $\beta$

Corresponden exactamente a las tipologías presentadas en la parte anterior del tema, ya que hay plena coincidencia estructural entre las fórmulas de LP y LPO cuando no se atiende a los cuantificadores:

Fórmulas $\gamma$

Esta categoría engloba a todas la fórmulas que se comportan como universales. La representante más clara de este tipo de fórmulas es $F :\ \forall x \, G$. Debido al significado que tiene el cuantificador universal, $\forall$, la forma de reducir esta fórmula a otras fórmulas más sencillas pasa por considerar todas las posibles componentes que resultan de sustituir en $G$ la variable cuantificada universalmente (en el ejemplo, $x$) por cualquier término cerrado del lenguaje $(G\{x/t\})$, de forma que la satisfactibilidad de la fórmula original se reduce a la satisfactibilidad de todas estas posibles componentes. Son fórmulas de tipo $\gamma$:

Fórmulas $\delta$

Esta categoría engloba a todas aquellas fórmulas que se comportan como existenciales. La representante más clara es $F :\ \exists x \, G$. Debido al significado que tiene el cuantificador universal, $\exists$, la forma de reducir esta fórmula a otras fórmulas más sencillas pasa por considerar un objeto del mundo, representado por medio de una nueva constante, $a$, que verifica $G$, ($G\{x/a\}$), de forma que la satisfactibilidad de la fórmula original se reduce a la satisfactibilidad de esta componente usando una nueva constante. Son fórmulas de tipo $\delta$:

Reglas de Reducción en LPO

Reglas $dN$, $\alpha$ y $\beta$

Las reglas en estos casos son idénticas a las expuestas para LP:

1. Si $(F :\ \neg \neg G) \in U$, entonces $U$ es satisfactible si y sólo si lo es $(U - \{F\}) \cup \{G\}$.
2. Si $F \in U$ es de tipo $\alpha$, entonces $U$ es satisfactible si y sólo si lo es $(U - \{F\}) \cup \{\alpha_1, \alpha_2\}$.
3. Si $F \in U$ es de tipo $\beta$, entonces $U$ es satisfactible si y sólo si lo es $(U - \{F\}) \cup \{\beta_1\}$ o lo es $(U - \{F\}) \cup \{\beta_2\}$.

Regla $ \gamma$

Si $F \in U$ es de tipo $\gamma$, entonces $U$ es satisfactible si y sólo si lo es $U \cup \{\gamma_t : t \mbox{ término cerrado}\}$.

Observa que en este caso la fórmula $F$ no se elimina del conjunto, porque puede seguir siendo usada con otro término.

Regla $ \delta$

Si $F \in U$ es de tipo $\delta$, entonces $U$ es satisfactible si y sólo si lo es $((U - \{F\}) \cup \{\delta_a\}$ (donde $a$ es un nuevo símbolo de constante).

Algoritmo de Tableros en LPO (Tableros completos)

El algoritmo de construcción que vamos a ver es similar al del caso LP, añadiendo las consideraciones necesarias para las dos reglas nuevas ($\gamma$ y $\delta$). Sin embargo, como en el caso de LPO los conjuntos de fórmulas pueden crecer mucho más (sobre todo, debido a las fórmulas de tipo $\gamma$), usaremos una convención a la hora de escribirlos, y es que iremos añadiendo las nuevas fórmulas como nodos nuevos, de forma que en cada nodo el conjunto que se maneja es el que viene expresado en todos los nodos que hay desde él hasta la raíz.

Para diferenciar qué fórmulas se pueden aplicar y cuáles no (por ejemplo, las fórmulas $\alpha$, $\beta$ y $\delta$, aunque sigan apareciendo en los nodos, no se pueden usar más de una vez, pero las fórmulas $\gamma$ se pueden usar tantas veces como términos cerrados se puedan construir) se usará una marca adicional que indica si una fórmula es usable o no.

Un tablero para un conjunto de fórmulas $U = \{F_1, \ldots, F_n\}$ es un árbol $T$, con nodos etiquetados con fórmulas, construido siguiendo el siguiente esquema:

1. Se construye un árbol inicial y lineal, con nodos etiquetados por las fórmulas de U, de forma que se toma una como raíz (por ejemplo, la primera), y se añaden el resto, de manera sucesiva como hijos de la anterior.

$$F_1 - F_2 - \dots - F_n$$

2. Si quedan ramas en $T$ no marcadas (ni abiertas ni cerradas), se toma una de ellas, $T_{br}$.

3. Si $T_{br}$ contiene una contradicción, esto es, dos fórmulas donde una es la negación de la otra, o bien directamente una fórmula insatisfactible ($\perp$ o $\neg (t = t)$), entonces marcar la rama como cerrada ("╳").

4. Si no, si hay en $T_{br}$ una fórmula usable, $F$:

   • Si $F$ es de tipo $dN$, entonces extender $T_{br}$ con un nodo etiquetado por $dN(A)$. Marcar $F$ como no usable.
   • Si $F$ es de tipo $\alpha$, entonces extender $T_{br}$ con dos nodos sucesivos etiquetados con $\alpha_1(F)$ y $\alpha_2 (F)$. Marcar $F$ como no usable.
   • Si $F$ es de tipo $\beta$, entonces extender $T_{br}$ con dos nodos (ramificación) etiquetados $\beta_1(F)$ y $\beta_2(F)$. Marcar $F$ como no usable.
   • Si $F$ es de tipo $\delta$, entonces extender $T_{br}$ con un nodo etiquetado con $\delta_a(F)$, introduciendo una nueva constante $a$. Marcar $F$ como no usable.
   • Si $F$ es de tipo $\gamma$, entonces extender $T_{br}$ con un nodo etiquetado con $\gamma_t(F)$, donde $t$ es un término cerrado del lenguaje (considerando también las nuevas constantes introducidas por reglas $\delta$) que no ha sido usado hasta el momento en $\gamma_t(F)$. NO marcar $A$ como no usable (las fórmulas $\gamma$ se pueden usar indefinidamente).

5. En otro caso marcar la rama como abierta ("◯").

6. Repetir desde el paso 2 mientras haya ramas no marcadas.

Ha de tenerse presente que, pese a que las reglas siguen reduciendo la complejidad de las fórmulas que intervienen, ahora un tablero completo puede ser infinito (una rama puede crecer indefinidamente) debido a la aplicación sucesiva de una misma fórmula de tipo $\gamma$ (las demás dejan de ser usables en cuanto se aplican, y siempre reducen la complejidad de la fórmula resultante).

Nota: Como observación para la aplicación de las reglas $\gamma$, su uso puede acabar cuando no queden más términos cerrados en el lenguaje (es decir, no tiene porqué provocar un uso infinito). En el caso de que desde el principio sea la única regla aplicable y no haya términos cerrados en el lenguaje, se puede usar una primera vez haciendo uso de la introducción de una constante nueva que se añade al lenguaje. Pero esto solo se puede hacer una vez, y solo bajo estas condiciones.

Se llama tablero completo a un tablero construido siguiendo las pautas anteriores y que no admite extensión, esto es, todas sus ramas finitas están marcadas como abiertas/cerradas (pero puede tener ramas infinitas). Se dice que el tablero es cerrado si tiene todas sus ramas cerradas (por tanto, además, son finitas). Se dice abierto en caso contrario, es decir, basta que tenga una rama marcada como abierta, o una rama infinita.

Por ejemplo, un tablero completo para el conjunto $\{\exists x \, Q(x), \forall x \, (Q(x) \rightarrow R(x)), \forall x \, \neg R(x)\}$ podría ser:

Teorema de Corrección y Completitud

Dado un conjunto de fórmulas $U$ de fórmulas cerradas:

1. Corrección. Si $U$ admite un tablero completo y cerrado entonces $U$ es inconsistente.
2. Completitud. Si $U$ es inconsistente, entonces admite un tablero completo y cerrado.

Observa que, a pesar del teorema anterior, el algoritmo presentado no garantiza la parada del algoritmo, ya que en LPO los tableros pueden ser infinitos, algo que es consistente con la observación del primer tema en la que decíamos que el problema de satisfactibilidad en LPO no es decidible (es decir, no existe un algoritmo que para cualquier fórmula de LPO decida en tiempo finito si es satisfactible o no).

Búsqueda de modelos

Al igual que pasaba en LP, el Teorema de Corrección y Completitud concluye que un conjunto de fórmulas, $U$, admite un tablero completo abierto si y sólo si $U$ es consistente, de forma que cada una de las ramas abiertas (que son finitas y describen en las formulas usables conjuntos de literales no contradictorios) proporciona, al menos, un modelo (no necesariamente distinto) de $U$.

Estos modelos corresponden a $L$-estructuras en las que el universo (no necesariamente finito) contiene las interpretaciones de los términos cerrados que han aparecido en la rama, y las interpretaciones de los predicados es consistente con las secuencias de términos (según la aridad) que hacen uso del predicado en la rama.

Las ramas infinitas también proporcionan modelos, aunque más difíciles de determinar, pero que esencialmente siguen el mismo proceso.

Consecuencia lógica

Como el resultado en el que se basa el problema de consecuencia lógica sigue siendo válido para LPO ($U \models F \Leftrightarrow U \cup \{ \neg F\}$ es inconsistente), podemos usar los tableros semánticos de LPO para resolver este problema, ya que se puede reducir también a la obtención de un tablero cerrado de un conjunto de fórmulas. De esta forma, se tiene que dicha consecuencia será cierta ($U \models F$) si y sólo si un tablero (completo) asociado a $U \cup \{ \neg F\}$ es cerrado (realmente, si uno lo es, todos los serán).

Por supuesto, si el problema de satisfactibilidad no es decidible en LPO, el problema de la consecuencia tampoco lo será.

Ejemplos de aplicación

Los conceptos que hemos desarrollado previamente permiten trabajar con el Método de Tableros Semánticos para su aplicación a la satisfactibilidad de conjuntos en LPO. A continuación, se muestran algunos ejemplos (en forma de ejercicios resueltos) con el fin de afianzar los conceptos vistos durante esta segunda parte del tema:

Decide, utilizando tableros semánticos, cuáles de los siguientes conjuntos de fórmulas son consistentes ($P,Q$ y $R$ son predicados de la aridad correcta). Dar un modelo para cada uno de los conjuntos satisfactibles:

1. $\{\exists x \, Q(x), \forall x \, (Q(x) \rightarrow R(x)), \forall x \, \neg R(x)\}$
2. $\{\exists y \, \forall x \, P(x,y), \forall x \, \neg P(x,x)\}$
3. $\{\forall x \, \forall y \, (P(x,y) \rightarrow P(y,x)), \forall x \, P(x,x), \exists x \, \exists y \, P(x,y)\}$
4. $\{\forall x \, \exists y \, P(x,y), \forall x \neg P(x,x)\}$

Solución

1. Teniendo en cuenta el Teorema de Compacidad y Completitud, podemos reducir la satisfactibilidad del conjunto a la construcción del tablero completo que se muestra en la figura anterior. De forma que el tablero sale cerrado, y por tanto el conjunto es inconsistente.

2. De forma análoga al caso anterior:

   

De nuevo, el tablero nos sale cerrado, por tanto el conjunto es inconsistente.

3. Operando del mismo modo que en los casos anteriores:

   

   En este caso vemos que la rama derecha es abierta, puesto que no hay más términos cerrados sobre los que aplicar las fórmulas de tipo $\gamma$ y el resto de fórmulas son no usables. Vamos a intentar, entonces, dar un modelo a partir de la información que muestra esa rama y que pruebe que el conjunto sea satisfactible.

   Por ejemplo, a partir de las fórmulas atómicas (que son cerradas) que aparecen en la rama podemos construir una $L$-estructura que indica qué objetos hay y cómo funciona el predicado sobre ellos:

   $$\begin{array}{l} M = \{c1, c2\} \\ P = \{(c1,c1), (c1,c2), (c2, c1), (c2,c2)\} \end{array}$$

   Es fácil comprobar que, en efecto, es un modelo del conjunto original (observa que, realmente, basta cualquier mundo en el que $P$ se verifica siempre).

4. El tablero para el conjunto correspondería a:

   

   En este caso, el tablero no puede cerrar la única rama que tiene (observa que la presencia de la fórmula 1 es de tipo $\gamma$ y genera continuamente términos cerrados con los que poder seguir añadiendo nuevos nodos). Pero, a pesar de ello, no es difícil obtener un modelo infinito del conjunto de fórmulas. Por ejemplo, con la interpretación $M=\mathbb{N}$ y el predicado $P(x,y): x < y$, tenemos que, en efecto, para todo elemento existe uno que es mayor (primera fórmula) y ningún elemento es mayor que sí mismo (segunda fórmula). Por lo que el conjunto es consistente

   También podemos dar un modelo finito. Si tomamos $M=\{0,1\}$ y $P(x,y): x \neq y$, vemos que, en efecto, se verifica que para todo elemento existe uno que es distinto de él (primera fórmula) porque hay dos elementos en el mundo, y ningún elemento es distinto de sí mismo (segunda fórmula).

   En este ejemplo es importante destacar dos cosas:

   1. De las ramas infinitas pueden salir modelos finitos.
   2. Para encontrar el modelo de la rama infinita no hemos aplicado ningún proceso automático (aunque en este caso se podría haber hecho), sino que hemos "razonado" guiados por nuestra intuición y conocimiento previo, algo que es consistente con el hecho de que este problema en LPO es no decidible. Observa que esto significa que no hay un mecanismo general para todas las fórmulas LPO, pero tenemos uno que se comporta mecánicamente con muchas de esas fórmulas (en principio, solo para las que generan tableros finitos, pero se puede mejorar mecánicamente para abarcar incluso muchos casos en los que el tablero resultante sería infinito).

Razonamiento con Igualdad

Si el lenguaje LPO que estamos considerando tiene igualdad, recordemos que su interpretación viene prefijada por el uso habitual de la misma. En este caso, de forma implícita estamos introduciendo una serie de características en la interpretación de este predicado que han de ser explicitadas a la hora de tratar las fórmulas del conjunto por medio de tableros semánticos.

Una primera opción sería incluir los axiomas que describen las propiedades fundamentales de este predicado, que son:

1. Identidad: $\forall x\ (x=x)$.
2. Sustitución: Si $t_1,\dots,t_n$ son términos de $L$, y $F(x_1,\dots,x_n)$ es una fórmula atómica, entonces se tiene que: $$\forall x_1\dots \forall x_n\ (x_1=t_1\wedge\dots\wedge x_n=t_n\rightarrow F(x_1,\dots,x_n)=F(t_1,\dots,t_n))$$.

A partir de estos dos axiomas se pueden obtener otras propiedades habituales para este predicado, por ejemplo:

1. Simetría: $\forall x\forall y\ (x=y \rightarrow y=x)$.
2. Transitividad: $\forall x \forall y\forall z\ (x=y\wedge y=z\rightarrow x=z)$.

La existencia de estas propiedades se traduce en la introducción de dos nuevas reglas para tableros semánticos, conocidas como reglas de igualdad, que nos permiten introducir nuevos nodos a un tablero que consideran las relaciones de igualdad existentes entre los términos del lenguaje:

1. Regla $I_1$: Para cada término cerrado, $t$, se puede extender cualquier rama del tablero añadiendo a una de sus hojas un nuevo descendiente marcado con la fórmula: $$t = t$$.
2. Regla $I_2$: Si $t$ y $s$ son términos cerrados y en una rama del tablero aparecen un literal $P(t_1,\dots,t,\dots,t_n)$ y la fórmula $t = s$ (o la fórmula $s = t$), entonces podemos extender dicha rama añadiendo en su hoja un nuevo descendiente marcado con la fórmula: $P(t_1,\dots ,s,\dots,t_n)$.

El uso de estas dos reglas nos asegura que estemos considerando las identificaciones por igualdad en el tratamiento de los términos que aparecen en la construcción del tablero (y, en consecuencia, en las fórmulas que van apareciendo en sus nodos).

Veremos por medio de unos ejemplos cómo estas reglas afectan a la construcción de tableros en lenguajes con igualdad:

Ejemplo 1. Comprobar que $\forall x \forall y\ (x = y \rightarrow f (x) = f (y))$ es lógicamente válida.

La reducción del problema $TAUT$ a $SAT$ se hace por medio del siguiente resultado que vimos en temas anteriores: $F\in TAUT\Leftrightarrow \neg F \notin SAT$. Por tanto, basta ver que un tablero completo para la fórmula que nos dan es cerrado:

Ejemplo 2. Comprobar que $\forall x \forall y \forall z\ (x =y \wedge y = z \rightarrow x = z)$ es lógicamente válida.

Siguiendo un razonamiento similar al ejemplo anterior, basta comprobar que un tablero completo para la negación de a fórmula es cerrado:

Ejemplo 3. Comprobar que $\{\exists x\ (f (x,x) = a),\ \forall x\ (f (x,a) = b)\} \models \exists x\ (f (x,f (x,x)) = b)$.

En virtud del Teorema de la Consecuencia que vimos en el tema anterior, sabemos que este resultado es cierto si $\{\exists x\ (f (x,x) = a),\ \forall x\ (f (x,a) = b),\ \neg \exists x\ (f (x,f (x,x)) = b)\}$ es inconsistente, o lo que es lo mismo, si un tablero completo suyo es cerrado: