Lógica Computacional
Nota 07. Deducción natural para lógica de predicados

1 Deducción natural

Como en lógica proposicional, requerimos de un conjunto de reglas que nos permitan razonar y llegar a una conclusión a partir de ciertas premisas. A las reglas de deducción natural de la Nota 03, agregamos las siguientes reglas referentes a los cuantificadores que forman parte de la lógica de predicados.

Las reglas de introducción y eliminación de las fórmulas cuantificadas, $\forall x\phi$ y $\exists x\phi$, se muestran en la Figura 1.

Figura 1: Reglas de deducción natural para $\forall$ y $\exists$.

Reglas de derivación para el cuantificador universal

La regla de eliminación del $\forall$, que denotamos $E\forall x$, dice que si $\forall x\phi$ es verdadero, entonces podemos reemplazar la $x$ en $\phi$ por cualquier término $t$, asegurándonos que al efectuar la sustitución no se liguen variables libres, y concluir que $\phi [x:=t]$ es verdadero. Esta es en realidad una serie de reglas, una para cada término $t$, y debemos hacer una elección conveniente y consistente con las fórmulas involucradas en la demostración.

La regla de introducción del $\forall$, denotada $I\forall x$, es más complicada. La caja estipula el alcance de $x_0$. La regla dice que si comenzamos con una ‘variable nueva’ $x_0$ y demostramos $\phi [x:=x_0]$, entonces (porque $x_0$ es nueva) podemos concluir $\forall x\phi$. La variable $x_0$ no figura afuera de su caja; podemos pensar en ella como un término arbitrario. Como no supusimos nada acerca de $x_0$, cualquier otro objeto podría tomar su lugar con el mismo resultado; por lo tanto $\forall x\phi$.

Para comprender la idea detrás de $I\forall x$ pensemos en lo siguiente: si usted quiere demostrar que puede romper cualquier ladrillo con un golpe de karate, puede decir “Denme un ladrillo y lo romperé”. Le damos uno y lo hace. Pero, ¿cómo podremos asegurarnos que usted puede romper cualquier ladrillo con un golpe de karate? No le podemos dar todos los ladrillos. Suponemos que el que usted acaba de romper fue uno arbitrario, es decir, no tenía nada en especial; y eso basta para convencernos de que usted puede romper cualquier ladrillo. La regla dice que si podemos demostrar $\phi$ respecto a una $x_0$, que no tiene nada en especial, entonces podemos demostrar $\phi$ para cualquier $x$.

Aunque los paréntesis cuadrados representando la sustitución aparecen en las reglas $I\forall x$ y $E\forall x$, no aparecen en la práctica. La sustitución que se indica la llevamos a cabo de antemano. La expresión $\phi [x:=t]$ significa: “$\phi$, con las presencias libres de $x$ reemplazadas por $t$”.

Compare las reglas para $\wedge$ y $\forall$. Las reglas para $\forall$ son una generalización de aquellas para $\wedge$; mientras que $\wedge$ tiene dos elementos, $\forall$ se comporta como una conjunción de muchas fórmulas.

• La regla $I_{\wedge }$ tiene dos premisas; ahora bien, $I\forall x$ tiene una premisa $\phi [x:=x_0]$ por cada posible valor de $x_0$.

• La regla $E_{\wedge }$ nos permite deducir cualquiera $\phi$ y $\psi$ a partir de $\phi \wedge \psi$; en tanto que $E\forall x$ nos permite deducir $\phi [x:=t]$ para cualquier $t$ a partir de $\forall x\phi$.

Reglas de derivación para el cuantificador existencial

La regla de introducción del $\exists$, denotada $I\exists x$, dice que podemos deducir $\exists x\phi$ cuando tengamos $\phi [x:=t]$ para algún término $t$, asegurándonos que al efectuar la sustitución no se liguen variables libres. Observemos que la fórmula $\phi [x:=t]$ contiene más información que $\exists x\phi$. Esta última dice que $\phi$ se cumple para algún valor de $x$; mientras que $\phi [x:=t]$ exhibe el valor concreto $t$ de $x$ que cumple $\phi$. Al decir que Simon Biles es capaz de realizar un doble salto mortal hacia atrás con tres giros, estamos siendo más específicos que simplemente decir: “’hay alguien que es capaz de realizar un doble salto mortal hacia atrás con tres giros”. Podemos notar la analogía entre las reglas para $\vee$ y $\exists$; la regla $I_{\vee }$ dice que siendo cierto alguno de los elementos de la disyunción, entonces la disyunción es cierta; de manera similar, siendo cierto $\phi [x:=t]$ para algún $t$ podemos concluir que $\exists x\phi$ es cierto.

Continuando con la analogía entre $\vee$ y $\exists$, al contemplar $E_{\vee }$ podemos llegar a la formulación de la regla de eliminación del $\exists$, denotada $E\exists x$. El bosquejo del razonamiento para la regla $E\exists x$ es: sabemos que $\exists x\phi$ es verdadero, así que $\phi$ es verdadero para al menos un valor de $x$. Realizamos un análisis de casos sobre todos los posibles valores, escribiendo $x_0$ como un valor genérico representándolos a todos. Por ejemplo, para analizar “algún matemático ruso demostró la conjetura de Poincare” tenemos que analizar a los matemáticos rusos, que de forma genérica denotamos con $x_0$. Si $\phi [x:=x_0]$ nos permite demostrar $\chi$ la cual no menciona a $x_0$, entonces $\chi$ debe ser cierto sin importar qué $x_0$ hace verdadero a $\phi [x:=x_0]$. Por supuesto, $x_0$ no puede figurar afuera de su caja. La caja está controlando i) el alcance de $x_0$ y ii) el alcance de la hipótesis $\phi [x:=x_0]$. Del mismo modo que $E_{\vee }$ dice que para usar $\phi \vee \psi$ hay que estar preparados para usar ya sea $\phi$ o $\psi$, la regla $E\exists x$ dice que para usar $\exists x\phi$ hay que estar preparados para usar cualquier posible $\phi [x:=x_0]$. Otra forma de ver $E\exists x$ es: si sabemos $\exists x\phi$ y derivamos $\chi$ de $\phi [x:=x_0]$, es decir, derivamos $\chi$ al dar un nombre al objeto que sabemos existe, entonces podemos derivar $\chi$ sin ocupar el nombre que se le dio a dicho objeto.

Las reglas $I\forall x$ y $E\exists x$ tienen la condición de que la variable $x_0$ no puede aparecer afuera de su caja.

Es importante mencionar que el sistema de deducción natural para la lógica de predicados con las reglas recién definidas, junto con las que se tenían para la lógica proposicional, es correcto y completo de acuerdo a la semántica que se explicará en la siguiente nota.

Un sistema de deducción natural puede clasificarse como minimal, intuicionista o clásico, de acuerdo al manejo que se le da a la negación.

1.1 Lógica minimal

En un sistema minimal el operador de negación ocupa a la constante $\perp$ del siguiente modo:

$$\neg \phi \stackrel{def}{=}\phi \to \perp$$

Aquí estamos hablamos de la negación constructiva. De manera que en la lógica minimal, las reglas de inferencia que toman en cuenta a la negación y a $\perp$ son $I\neg$ y $E\neg$ únicamente. Excluimos a $E\perp$, $E\neg \neg$, $I\neg \neg$, $PPC$ y $LTE$.

1.2 Lógica intuicionista

La lógica intuicionista se obtiene al agregar a la lógica minimal la regla de eliminación del falso $E\perp$, conocida también como ex-falso-quodlibet. El carácter constructivo de la negación restringe a la lógica de una manera importante, en particular esta lógica no permite probar la ley del tercero excluido, $\phi \vee \neg \phi$, una tautología clásica. Debemos mencionar que la fórmula del tercero excluido surgió al describir ciertas situaciones finitas en las que se satisface, pero estudiosos de la lógica pusieron en duda su validez al contemplar su generalización al infinito. Por ejemplo, en el artículo titulado Intuitionistic Logic, Joan Moschovakis afirma que:

[…]si $x$ y $y$ son números naturales y el predicado $B(x)$ quiere decir que existe un número $y>x$ tal que $y$ y $y+2$ son ambos números primos, entonces no tenemos método alguno para determinar si $B(x)$ es verdadero o falso para una $x$ arbitraria, así $\forall x(B(x)\vee \neg B(x))$ no se puede afirmar en el estado del conocimiento actual. Si $A$ representa el enunciado $\forall xB(x)$, entonces $(A\vee \neg A)$ no se puede afirmar porque ni $A$ ni $\neg A$ se han podido probar. De acuerdo a Brouwer la ley del tercero excluido era equivalente a una suposición a priori que afirma que todo problema en matemáticas tiene solución[…].

1.3 Lógica clásica

En la lógica clásica el tratamiento de la negación es el que hemos venido manejando desde un principio, en donde se valen todas las reglas referentes a la negación y a $\perp$ de la Nota 03.

2 Reglas de inferencia para la igualdad

Presentamos abajo algunas reglas de utilidad que involucran a la igualdad

$$\frac{}{t=t}(I=)\frac{t_1=t_2\phi [x:=t_1]}{\phi [x:=t_2]}(E=)$$

A partir de las reglas $I=$ y $E=$ podemos mostrar que la igualdad es reflexiva, transitiva y simétrica.

3 Equivalencia entre fórmulas con cuantificadores

A continuación presentamos algunas equivalencias entre cuantificadores. Escribimos ${\phi }_1⊣⊢{\phi }_2$ como una abreviatura para la validez de ${\phi }_1⊢{\phi }_2$ y ${\phi }_2⊢{\phi }_1$.

Teorema 3.1

Sean $\phi$ y $\psi$ dos fórmulas de la lógica de predicados. Se tienen las siguientes equivalencias:

1. 1. $\neg \forall x\phi ⊣⊢\exists x\neg \phi$

   2. $\neg \exists x\phi ⊣⊢\forall x\neg \phi$

2. Suponiendo que $x$ no es libre en $\psi$

   1. $\forall x\phi \wedge \psi ⊣⊢\forall x(\phi \wedge \psi )$

   2. $\forall x\phi \vee \psi ⊣⊢\forall x(\phi \vee \psi )$

   3. $\exists x\phi \wedge \psi ⊣⊢\exists x(\phi \wedge \psi )$

   4. $\exists x\phi \vee \psi ⊣⊢\exists x(\phi \vee \psi )$

   5. $\forall x(\psi \to \phi )⊣⊢\psi \to \forall x\phi$

   6. $\exists x(\phi \to \psi )⊣⊢\forall x\phi \to \psi$

   7. $\forall x(\phi \to \psi )⊣⊢\exists x\phi \to \psi$

   8. $\exists x(\psi \to \phi )⊣⊢\psi \to \exists x\phi$

3. 1. $\forall x\phi \wedge \forall x\psi ⊣⊢\forall x(\phi \wedge \psi )$

   2. $\exists x\phi \vee \exists x\psi ⊣⊢\exists x(\phi \vee \psi )$

4. 1. $\forall x\forall y\phi ⊣⊢\forall y\forall x\phi$

   2. $\exists x\exists y\phi ⊣⊢\exists y\exists x\phi$

4 Ejemplo de derivación

Abajo se encuentra una demostración en deducción natural para el secuente

$$\exists xQ(x),\forall x\left(Q(x)\wedge \exists yP(y)\to Q(f(x))\right),\forall z\left(Q(z)\to Q(g(z))\right)⊢P(b)\to \exists wQ\left(f(g(w))\right).$$