**LITI** Formas Prenex, de Skolem y Teorema de Herbrand Al igual que vimos cómo extender los Tableros Semánticos de LP a LPO, en este capítulo vamos a ver los fundamentos necesarios para extender las Formas Normales y Formas Clausales vistas en LP a un formato igualmente útil en LPO. El objetivo no solo es disponer de fórmulas equivalentes, sino ver hasta qué punto podemos trasladar los algoritmos que se desarrollan para LP al contexto de Primer Orden. En este caso, no solo tendremos que tratar la aparición de cuantificadores para poder manipular las fórmulas de la manera adecuada, sino que también tendremos que ver de qué forma se puede extender el lenguaje (si es necesario) para poder tratar las fórmulas como si fueran abiertas y cerradas (para que se parezcan a fórmulas proposicionales, sin cuantificadores, y sin variables libres). Para ello, introduciremos dos nuevos tipos de Formas Normales: **las Formas Prenex y de Skolem**, que servirán como modo de preprocesado de las fórmulas LPO para poder aplicar entonces las Formas Normales FNC y FND similares a las vistas en el caso proposicional, y veremos cómo los trabajos del matemático Jaques Herbrand nos permitirán en gran medida reducir la complejidad de las interpretaciones LPO a modelos finitos parecidos a los que se tratan en LP. En el tema anterior estudiamos el concepto de equivalencia entre fórmulas proposicionales: _dos fórmulas proposicionales son equivalentes si tienen los mismos modelos_. Esta definición no se puede traducir directamente a LPO debido a la posibilidad de que las fórmulas puedan no ser cerradas, pero daremos una definición que, cuando así sean, será similar a la anterior: !!!Def:Equivalencia Dos fórmulas $F$ y $G$ de un lenguaje de primer orden son equivalentes si y sólo si la fórmula $F \leftrightarrow G$ es lógicamente válida (es decir, $F\equiv G\ \Leftrightarrow \ \models F\leftrightarrow G$). Nótese que si ambas fórmulas son cerradas entonces se tiene la misma definición que en el caso LP, esto es, $F$ y $G$ son equivalentes si y sólo si poseen, exactamente, los mismos modelos. Para las fórmulas no cerradas la equivalencia queda como: $F \equiv G \ \Leftrightarrow \ \models \forall\vec{x}\ (F(\vec{x}) \leftrightarrow G(\vec{x}))$. Al igual que en la Lógica Proposicional, el uso de preprocesamientos que mantengan la equivalencia es indispensable para poder aplicar técnicas que nos lleven a los algoritmos que estamos buscando. # Formas Prenex El primer paso es manipular los cuantificadores que aparecen en las fórmulas para obtener expresiones equivalentes que sean más _cercanas_ a fórmulas proposicionales sobre las que podemos calcular la FNC. !!!def:Forma Prenex Una fórmula, $F$, de un lenguaje LPO está expresada en _Forma Prenex_ si todos los cuantificadores se encuentran en la cabeza de la fórmula. Esto es, $F$ es de la forma: $$ Q_1x_1 \, Q_2x_2 \, \ldots Q_nx_n G(x_1, x_2, \ldots, x_n)$$ donde $Q_i \in \{\exists, \forall\}$ y $G(x_1, \ldots, x_n)$ es abierta. Se dice que una fórmula, $H$, es una _forma normal prenexa_ de $F$ si se tiene que $F\equiv H$ y $H$ está en forma prenex. La siguiente tabla proporciona un conjunto de operaciones atómicas (llamadas **operaciones prenex**) que permiten manipular los cuantificadores de fórmulas de primer orden obteniendo fórmulas equivalentes (es fácil probar que realmente es así), pero en las que los cuantificadores se van agrupando para aproximarse a una forma normal prenexa:  Este resultado se puede formalizar bajo el siguiente Lema: !!!note: Lema Si $F'$ se obtiene de $F$ por aplicación de una operación prenex, entonces $F \equiv F'$. Y se completa con el siguiente Teorema, que nos indica no solo que siempre es posible obtener una forma prenexa equivalente, sino que indica cómo hacerlo: !!!note:Teorema Para toda fórmula, $F$, existe otra, $G$, en forma prenex, que es equivalente a $F$. De hecho, basta seguir los pasos siguientes para el cálculo de una forma prenex: 1. Sustitución de las expresiones de la forma $F \leftrightarrow G$ por $(F\rightarrow G) \wedge (G\rightarrow F)$. 2. Renombrado (por medio de P1) de las variables para que no se produzcan interferencias en las cuantificaciones. 3. Interiorización de las negaciones (por medio de P2). 4. Extracción de los cuantificadores (por medio de P3-P6). !!!note Evidentemente, la forma prenex no es única, ya que cuando aparece más de un cuantificador al mismo nivel de profundidad en el árbol de formación de la fórmula se puede elegir el orden que se desee para la extracción, por lo que puede haber variaciones en el orden de aparición de los cuantificadores en la cabeza de la fórmula resultante. Por razones que se entenderán más adelante (en la Forma de Skolem), normalmente tomaremos como opción más deseable aquella en la que los cuantificadores existenciales quedan en posiciones más externas (es decir, están más altos en el árbol de formación). Veamos un par de ejemplos de aplicación del método anterior: !!!Tip:Ejemplo 1 Calcular una forma prenex de: $$F(z,y) \equiv \forall x \, \exists y \, (x + z = y) \rightarrow \exists z \, \forall x (x·y = 0 + z)$$ 1. No es necesaria la sustitución de $\leftrightarrow$. 2. Renombrado de variables: $$\forall x_1 \, \exists y_1 \, (x_1 + z = y_1) \rightarrow \exists z_1 \, \forall x_2 (x_2·y = 0 + z_1)$$ 3. No es necesario interiorizar negaciones. 4. Extracción de cuantificadores del antecedente (intercambiados) y del consecuente priorizando los existenciales en la cabeza: $$\begin{array}{c} \exists x_1 \, \left(\exists y_1 \, (x_1 + z = y_1) \rightarrow \exists z_1 \, \forall x_2 (x_2·y = 0 + z_1) \right) \\ \exists x_1 \exists z_1 \, \left(\exists y_1 \, (x_1 + z = y_1) \rightarrow \forall x_2 (x_2·y = 0 + z_1) \right) \\ \exists x_1 \exists z_1 \forall y_1 \, \left((x_1 + z = y_1) \rightarrow \forall x_2 (x_2·y = 0 + z_1) \right) \\ \exists x_1 \exists z_1 \forall y_1 \forall x_2 \,\left((x_1 + z = y_1) \rightarrow (x_2·y = 0 + z_1) \right)\\ \end{array}$$ !!!Tip:Ejemplo 2 Calcular una forma prenex de: $$G(x) \equiv \exists x \, P(x,a) \rightarrow \left( \forall z \, P(x,z) \rightarrow \forall x \, P(x,a) \right)$$ 1. No es necesaria la sustitución de $\leftrightarrow$. 2. Renombrado de variables: $$\exists x_1 \, P(x_1,a) \rightarrow \left( \forall z_1 \, P(x,z_1) \rightarrow \forall x_2 \, P(x_2,a) \right)$$ 3. No es necesario interiorizar negaciones. 4. Extracción de cuantificadores del antecedente (intercambiados) y del consecuente priorizando los existenciales en la cabeza: $$\begin{array}{c} \exists x_1 \, P(x_1,a) \rightarrow \exists z_1 \forall x_2 \, (P(x,z_1) \rightarrow P(x_2, a))\\ \exists z_1 \forall x_1 \forall x_2 \, P(x_1,a) \rightarrow (P(x,z_1) \rightarrow P(x_2, a))\\ \end{array}$$ # Formas de Skolem En este apartado vamos a tratar de reducir un problema en LPO a un problema LP, prácticamente, equivalente. Para ello, tras haber obtenido la Forma Prenex, y haciendo uso de la llamada _Forma de Skolem_, vamos a transformar las fórmulas LPO a otras, también en LPO (aunque quizás en un lenguaje ligeramente distinto), pero mucho más sencillas, tanto, que pudieran parecer casi proposicionales. La Forma de _Skolem_ trata de restringir la complejidad de las fórmulas en LPO sin perder la expresividad de las mismas. Su aplicación necesita trabajar sobre fórmulas cerradas y que se encuentren en Forma _Prenex_ (si no fuera así bastaría calcular la forma Prenex de la clausura universal de la fórmula), y devolverá una fórmula en forma Prenex pero que no hace uso de cuantificadores existenciales. !!!note Recordemos que en Primer Orden una fórmula con variables libres se manipula por medio de su cierre universal, por lo que una fórmula en forma Prenex que solo tiene cuantificadores universales se identifica con una fórmula abierta: $$\forall x'_1 \ldots \forall x'_m \, H(x'_1, \ldots, x'_m) \equiv H(x'_1, \ldots, x'_m)$$ Se debe tener en cuenta que la nueva fórmula obtenida mediante la aplicación del método de Skolem no será, en general, equivalente a la fórmula original, pero sí se mantiene la consistencia, es decir, si la original era consistente, entonces la nueva también lo es, y viceversa. Es todo lo que necesitamos para poder responder a problemas como el de la consecuencia lógica (y veremos también que, en caso de serlo, es fácil transformar un modelo de una fórmula en un modelo de la otra). Veremos que la forma en que lo hace recuerda, en cierta forma, a las reglas $\delta$ y $\gamma$ que se usaban en los Tableros Semánticos de Primer Orden. !!!Def:Funciones y Constantes de Skolem Para eliminar los cuantificadores existenciales de una fórmula en Forma Prenex se aplican las siguientes reglas: * Por cada bloque del tipo $$\exists x\ F(x)$$ se añade una **nueva** **constante**, $c$, y se reescribe como $$F(c)$$ Se dice que $F(c)$ se obtiene a partir de la original introduciendo una **constante de Skolem**. * Por cada bloque $$\forall x_1 \dots \forall x_n \exists y\ F(x_1,\dots,x_n,y)$$ se introduce un **nuevo símbolo de función**, $g$, de aridad $n$, y se reescribe como $$\forall x_1 \dots \forall x_n \exists y \ F(x_1,\dots,x_n,g(x_1,\dots, x_n))$$ Se dice que la segunda fórmula se obtiene a partir de la original introduciendo una **función de Skolem**. Repitiendo este proceso tantas veces como cuantificadores existenciales haya en la forma Prenex obtendremos finalmente una nueva fórmula en forma Prenex que solo tendrá cuantificadores universales. !!!note Ahora podemos entender por qué es más deseable tener los cuantificadores existenciales más exteriores en la forma de Skolem resultante (cuando sea posible), ya que cuantos menos cuantificadores universales precedan a los existenciales, más sencillas son las funciones (pudiendo llegar a ser constantes) de Skolem que se introducen, simplificando la expresión de la forma de Skolem final. !!!Tip:Ejemplo Por ejemplo, si $F=\exists x\ A(x) \wedge \forall y\ B(y)$, encontramos dos posibles formas Prenex: 1. $\exists x \forall y\ (A(x)\wedge B(y))$. 2. $\forall y\exists x\ (A(x)\wedge B(y))$. Que dan lugar a dos fórmulas bastante diferentes (al menos, desde el punto de vista de la complejidad de los símbolos que se introducen): 1. $\forall y\ (A(a)\wedge B(y))$ (se ha introduce una constante de Skolem, $a$). 2. $\forall y\ (A(f(y))\wedge B(y))$ (se ha introducido una función de Skolem, $f$). Sea cual sea el orden en que se haga, los siguientes resultados nos confirman que su utilidad está asegurada para los fines que perseguimos. El siguiente resultado confirma la _equiconsistencia_ que buscábamos: !!!note:Teorema (de equiconsistencia) La introducción de funciones de Skolem conserva la consistencia. Es decir, dada una fórmula $F$ en LPO, si $F'$ se obtiene por medio de la aplicación del método de Skolem, entonces se tiene que: $$F \textit{ posee un modelo } \Leftrightarrow F' \textit{ posee un modelo } $$ Aunque en ningún momento se asegura que los modelos de ambas fórmulas coincidan. Debe observarse que $F$ y $F'$ no tienen porqué estar expresadas en los mismo lenguajes (normalmente, $F'$ usará símbolos de un lenguaje más amplio que el de $F$, ya que se han introducido nuevos símbolos para ello). Pero, además, tenemos un resultado más potente que nos indica que, esencialmente, hemos introducido símbolos para relaciones y objetos que ya estaban ahí, aunque sin nombre propio: !!!note:Teorema (de Skolem) La introducción de funciones de Skolem no aumenta el conocimiento deducible del lenguaje original. Es decir, dada una fórmula cerrada, $F$, de un lenguaje de primer orden, $L$, si $F'$ se obtiene por medio de la aplicación del método de Skolem, entonces se tiene que para toda fórmula $H$ del lenguaje de $L$ se tiene: $$ F \models H \Leftrightarrow F' \models H $$ Los conceptos y resultados anteriores permiten dar una definición formal de lo que se conoce como _Forma de Skolem_ y su aplicabilidad sobre conjuntos de fórmulas LPO. De forma que se tiene: !!!def:Forma de Skolem) Sea $L$ un lenguaje de primer orden y $F$ una fórmula cerrada de $L$. Una **forma de Skolem** de $F$ es una fórmula universal, $G$, que se obtiene a partir de una forma prenexa de $F$ mediante la introducción sucesiva de funciones de Skolem. Y, además, podemos extender estas definiciones y resultados para conjuntos de fórmulas (que es lo que necesitamos para tratar el _problema de la consecuencia_, por ejemplo): !!!note:Teorema Dado un conjunto, $\Sigma=\{F_1, \ldots, F_n\}$, de fórmulas cerradas de un lenguaje de primer orden, $L$, y un conjunto, $\Sigma'$, formado por las formas de Skolem de las fórmulas de $\Sigma$, entonces: * $\Sigma$ posee un modelo si y sólo si $\Sigma'$ posee un modelo (es decir, son equiconsistentes). * Para toda fórmula, $H$, del lenguaje $L$, se cumple: $$ \Sigma \models H \Leftrightarrow \Sigma' \models H $$ Veamos, algunos ejemplos de cálculo de _Formas de Skolem_: !!!Tip:Ejemplo 3 Calcular la forma de Skolem de: $$F \equiv \forall x \exists y \exists z \, (P(y,x) \wedge P(z,y))$$ $F$ ya se encuentra en forma _Prenex_ y es cerrada, por lo que basta aplicar el método de _Skolem_: 1. El primer existencial que encontramos se encuentra en un bloque del tipo $\forall x\exists y$, por lo que introducimos una función de Skolem, $f_1$, dependiente de la variable $x$, sustituimos la variable $y$ y eliminamos el cuantificador $\exists y$: $$\forall x \exists z \, (P(f_1(x),x) \wedge P(z,f_1(x)))$$ 2. Tras el paso 1 estamos en la misma situación, pero con la variable $z$, por lo que introducimos una función de Skolem, $f_2$, dependiente de la variable $x$ que sustituye a la variable $z$ y eliminamos el cuantificador $\exists z$: $$\forall x \, (P(f_1(x),x) \wedge P(f_2(x),f_1(x)))$$ !!!Tip:Ejemplo 4 Calcular la forma de Skolem de: $$F \equiv \exists x_1 \forall y_1 \exists z_2 \forall x_2 \exists y_2 \, ((x_1 + b = y_1) \rightarrow (x_2 · y_2 = 0 + z_2)) $$ $F$ ya se encuentra en forma _Prenex_ y es cerrada, por lo que basta aplicar el método de _Skolem_: 1. Introducimos una constante de Skolem, $c$, que sustituye a $x_1$ y eliminamos el cuantificador $\exists x_1$: $$ \forall y_1 \exists z_2 \forall x_2 \exists y_2 \, ((c + b = y_1) \rightarrow (x_2 · y_2 = 0 + z_2)) $$ 2. Introducimos una función de Skolem, $f_1$, dependiente de la variable $y_1$ sustituyendo a la variable $z_2$ y eliminamos el cuantificador $\exists z_2$: $$ \forall y_1 \forall x_2 \exists y_2 \, ((c + b = y_1) \rightarrow (x_2 · y_2 = 0 + f_1(y_1))) $$ 3. Introducimos una función de Skolem, $f_2$, dependiente de las variables $y_1$ y $x_2$ sustituyendo a la variable $y_2$ y eliminamos el cuantificador $\exists y_2$: $$ \forall y_1 \forall x_2 \, ((c + b = y_1) \rightarrow (x_2 · f_2(y_1,x_2) = 0 + f_1(y_1))) $$ # FNC, FND y Forma Clausal De igual manera que definíamos las _Forma Normales Conjuntiva y Disyuntiva_ para fórmulas LP podemos definirlas para fórmulas de LPO: !!!Def: Formas Normales * Una fórmula, $F$, de un LPO se dice **Literal** si es una fórmula atómica o la negación de una fórmula atómica. * Una fórmula abierta está en **Forma Normal Conjuntiva** si está expresada como conjunción de disyunciones de literales: $$F = \bigwedge \limits_{i=1}^{n}\left(\bigvee \limits_{j=1}^{m_i} L_{i,j}\right)$$ * Una fórmula abierta está en **Forma Normal Disyuntiva** si está expresada como disyunción de conjunciones de literales: $$F = \bigvee \limits_{i=1}^{n}\left(\bigwedge \limits_{j=1}^{m_i} L_{i,j}\right)$$ * Una **cláusula** corresponde a una disyunción de literales, por tanto es una fórmula abierta. Al igual que en el caso proposicional identificaremos una cláusula con el conjunto de literales que aparecen en ella, y denotaremos la cláusula vacía con el símbolo □. * Dada una fórmula, $F$ de $L$, una **Forma Clausal** de $F$ corresponde a un conjunto de cláusulas $S$ (ahora no es necesario que sean del lenguaje $L$, ya que en la forma de Skolem hemos podido introducir nuevos símbolos) que es equiconsistente con $F$ (es decir, que $F$ tiene un modelo si y solo si $S$ tiene un modelo). !!!note Uniendo todas las formas vistas anteriormente, la obtención de una forma clausal se reduce a la aplicación del siguiente procedimiento: * Obtener el cierre universal de $F$ (si $F$ no es cerrada): $G$. * Obtener una Forma de Skolem para $G$: $G_{sk}$, y expresarla en su forma abierta (obviando los cuantificadores universales). * Obtener una FNC para $G_{sk}$, siguiendo el procedimiento visto en el caso LP, de forma que cada una de las disyunciones corresponde a una cláusula y la conjunción de las disyunciones corresponde a la unión de las cláusulas: $\bigwedge \limits_{i=1}^{n} C_i$. * Una Forma Clausal para $F$ será: $\{C_i\}_{i=1, \ldots, n}$. De forma análoga, una Forma Clausal para un conjunto de fórmulas, $\Gamma$, corresponde a un conjunto de fórmulas equiconsistente, $S$, que se puede obtener como la unión de las formas clausales de cada una de las fórmulas de $\Gamma$. !!!Tip:Ejemplo 5 Calcular una Forma Clausal de: $$F \equiv \forall x \, \left( \forall y \, H(x,y) \rightarrow \exists z \forall u \, (u \neq z \rightarrow P(z,u))\right)$$ Teniendo en cuenta que $F$ es una fórmula cerrada, y siguiendo el procedimiento descrito: 1. Obtenemos una forma _Prenex_ $F$: $$ \forall x \exists y \exists z \forall u \, \left( H(x,y) \rightarrow (u \neq z \rightarrow P(z,u))\right) $$ 2. Obtenemos una forma de _Skolem_ a partir de ella y la expresamos como fórmula abierta: $$ \begin{array}{c} \forall x \forall u \, \left(H(x, f_1(x)) \rightarrow (u \neq f_2(x) \rightarrow P(f_2(x),u)) \right) \\ \Downarrow \\ H(x, f_1(x)) \rightarrow (u \neq f_2(x) \rightarrow P(f_2(x),u)) \\ \end{array}$$ 3. Obtenemos una FNC de esta nueva fórmula: $$ \neg H(x, f_1(x)) \ \vee \ u = f_2(x) \ \vee\ P(f_2(x), u)$$ 4. Obtenemos una Forma Clausal directamente de la expresión anterior: $$ \left\lbrace \{ \neg H(x, f_1(x)) ,\ u = f_2(x) ,\ P(f_2(x), u) \} \right\rbrace$$ # De LPO a LP: Teorema de Herdbrand En este apartado vamos a exponer cómo podemos reducir la consistencia de un conjunto de fórmulas en un lenguaje de primer orden a la de un conjunto de fórmulas proposicionales usando los trabajos que, en esta dirección, realizó el matemático Jaques Herdbrand. Para ello, si $\Gamma$ es un conjunto de fórmulas de un lenguaje $L$ debemos tener en cuenta que: * Hemos visto que el cálculo de formas de Skolem reduce la consistencia de $\Gamma$ a la consistencia de un conjunto, $\Sigma$, de fórmulas abiertas (de hecho, cláusulas) en un nuevo lenguaje $L'$ (que extiende a $L$ con nuevos símbolos). * Daremos un paso más y reduciremos la consistencia de $\Gamma$ a la consistencia de un conjunto de fórmulas que son abiertas y cerradas a la vez. * Una fórmula abierta y cerrada puede identificarse con su esqueleto proposicional y, por tanto, considerarse una fórmula proposicional (pero escrita con símbolos de un lenguaje LPO). Para ello, Herbrand define un conjunto de fórmulas que se puede formar cerrando de la forma más amplia posible las variables libres en nuestros conjuntos de fórmulas: !!!def:Extensión de Herbrand Sea $\Sigma$ un conjunto de fórmulas abiertas. La **extensión de Herbrand** de $\Sigma$, es el conjunto, $EH(\Sigma)$, formado por todas las fórmulas cerradas que pueden obtenerse sustituyendo, de todas las formas posibles, las variables de las fórmulas de $\Sigma$ por términos cerrados del lenguaje. Esencialmente, los términos cerrados del lenguaje representan todos aquellos objetos del mundo que el lenguaje es capaz de nombrar directamente, usando los símbolos del lenguaje. Debe recordarse que muy fácilmente el conjunto de términos cerrados de un lenguaje puede ser infinito (basta que haya, por ejemplo, un símbolo de constante y un símbolo de función). Lo interesante es que, realmente, la consistencia o inconsistencia de un conjunto de fórmulas depende únicamente de expresiones que usan términos cerrados, porque si hay una inconsistencia, ésta debe ser expresada haciendo uso de esos términos. Esto es lo que dice el conocido como Teorema de Herbrand: !!!note:Teorema (de Herdbrand) Sea $\Sigma$ un conjunto de fórmulas abiertas (o, equivalentemente, cláusulas), son equivalentes: 1. $\Sigma$ tiene un modelo (es consistente, en el sentido LPO, por medio de un universo y sus interpretaciones asociadas). 2. $EH(\Sigma)$ tiene un modelo (es consistente, en el sentido LPO, por medio de un universo y sus interpretaciones asociadas). 3. $EH(\Sigma)$ es satisfactible proposicionalmente. Es decir, si identificamos cada fórmula $EH(\Sigma)$ con su esqueleto proposicional, entonces el conjunto de fórmulas proposicionales es satisfactible (es consistente, en el sentido LP, con una valoración que las hace simultáneamente ciertas). Gracias a este resultado: !!!note Se reduce la consistencia de un conjunto de fórmulas LPO (o de una Forma de Skolem de dicho conjunto) a la consistencia de un conjunto de fórmulas proposicionales. Como hemos comentado, $EH(\Sigma)$ puede ser infinito, y parece que este hecho podría dar lugar a inconsistencias en las que podrían intervenir infinitas fórmulas, pero el siguiente Teorema nos indica que, de hecho, no es así. !!!note:Teorema (de Compacidad) Si $EH(\Sigma)$ es inconsistente, entonces existe un subconjunto finito de $EH(\Sigma)$ que es inconsistente. De forma que bajo el uso conjunto de la _Forma de Skolem_ y la _Extensión de Herdbrand_ podemos lograr el objetivo marcado al inicio del tema. !!!Tip:Ejemplo 6 Demostrar que el siguiente conjunto de fórmulas es inconsistente haciendo uso del Teorema de Herbrand: $$\Sigma \equiv \{F_1(x): P(x) \rightarrow P(f(f(x))),\ F_2(x): \neg P(f(f(f(x)))),\ F_3: P(f(a))\}$$ Teniendo en cuenta que si $\Sigma$ es inconsistente entonces existe un subconjunto finito de $EH(\Sigma)$ también inconsistente, basta ir comprobando, de manera incremental, si las distintas sustituciones de términos cerrados en $\Sigma$ van generando conjuntos de fórmulas abiertas y cerradas inconsistentes. La extensión de Herbrand, $EH(\Sigma)$, contiene, entre otras, las fórmulas (ni siquiera es necesario pasarlo a Forma Clausal, se puede usar cualquier método de consistencia proposicional): 1. $F_3=p(f(a))$ 2. $F_1(a)=p(a)\rightarrow p(f(f(a)))$ 3. $F_2(a)=\lnot p(f(f(f(a))))$ 4. $F_1(f(a))=p(f(a))\rightarrow p(f(f(f(a))))$ 5. $F_2(f(a))=\lnot p(f(f(f(f(a)))))$ 6. $F_1(f(f(a)))=p(f(f(a)))\rightarrow p(f(f(f(f(a)))))$ 7. $F_2(f(f(a)))=\lnot p(f(f(f(f(f(a))))))$ 8. $\quad \quad \vdots$ El subconjunto de $EH(\Sigma)$ formado por las fórmulas 1, 3 y 4 es claramente inconsistente.