Parte VII Teoria de la demostracion en logica de predicados

Observación VII.1.

Los simbolos de funcion no son necesarios para la logica de predicados. Se pueden “simular” con predicados.

Ejemplo VII.1.

$D=\left\{\text{personas}\right\}$

$m(x)\colon$ la madre de $x\rightarrow M(x,y):$ x es la madre de $y$ .

“La madre de Antonio es rubia”.

$R(x)\colon$ x es rubio. $R(m(a))$ .

$\forall x(M(x,a)\rightarrow R(x))$

“Todos los hermanos de Antonio son rubios” $\Rightarrow\forall x(H(x,a)\rightarrow R(x))$ (que no la puedo hacer con funciones).

Vamos a ampliar el sistema de Gentzen para la logica proposicional, añadiendo a las 8 relgas que teniamos 4 nuevas reglas para los cuantificadores. El sistema de demostracion resultante es valido para la logica de predicados sin igualdad (definir un sistema que sea valido para la logica de predicados con igualdad que hemos introducido en los temas 5 y 6 requeriria reglas adicionales y tiene cierto grado de complejidad).

Los nombres de las 4 nuevas reglas de inferencia son:

$E\forall$	$I\forall$
$E\exists$	$I\exists$

Proposición VII.1.

$\varphi,\psi,\ldots$ representaran formulas cualesquiera de la logica de predicados.
$\varphi(x)$ denotara una formula donde la variable $x$ tiene apariciones libres. Si despues escribimos $\varphi(t)$ , donde $t$ puede ser un termino cualquiera, esto representara la formula $\varphi$ donde todas las apariciones libres de $x$ se han sustituido por $t$ .
Llamaremos variable fresca a una variable que no ha aparecido previamente en el razonamiento.

Definición VII.1 (Regla de eliminacion del universal,

E\forall

Sea $t$ un termino cualquiera

\begin{array}[]{c}\forall x\varphi(x)\\ \hline\cr\varphi(t)\end{array}

Definición VII.2 (Regla de introduccion del existencial,

I\exists

Sea $t$ un termino cualquiera

\begin{array}[]{c }\varphi(t)\\ \hline\cr\exists x\varphi(x)\end{array}

Ejemplo VII.2.

Demostrar la validez de $\left\{\forall x(P(x)\to Q(x)),P(a)\right\}\vdash Q(a)$ .

1.

$\forall x(P(x)\to Q(x))$ Pr
2.

$P(a)$ Pr
3.

$P(a)\to Q(a)\quad E\forall,1,x=a$
4.

$Q(a)\quad E\rightarrow,2,3$

Ejemplo VII.3.

Demostrar la validez de $\left\{P(b),\exists xP(x)\to Q(a)\right\}\vdash Q(a)$ .

1.

$P(b)$ Pr
2.

$\exists xP(x)toQ(a)$ Pr
3.

$\exists xP(x)\quad I\exists,1$
4.

$Q(a)\quad E\rightarrow,2,3$

Definición VII.3 (Regla de introduccion del universal,

I\forall

\begin{array}[]{c}\noindent\framebox{\parbox{426.82pt}{ $y\qquad\qquad\quad\;\text{Variable fresca}$ \par$\vdots$ \par$\varphi(y)$}}\vspace{0.2cm}\\ \hline\cr\forall x\varphi(x)\end{array}

Observación VII.2.

Este es el unico caso en el que usamos una demostracion auxiliar que no empieza con una premisa auxiliar, sino con una variable libre y que no sirve para introducir un implica sino un para todo.

Ejemplo VII.4.

Demostrar la validez de $\forall xP(x)\wedge\forall xQ(x)\vdash\forall x(P(x)\wedge Q(x))$

1.

$\forall xP(x)\wedge\forall xQ(x)$

[resume] 1. $y$ Variable fresca 2. $\forall xP(x)\quad E\wedge,1$ 3. $P(y)\quad E\forall,3,x=y$ 4. $\forall xQ(x)\quad E\wedge,1$ 5. $Q(y)\quad E\forall,5,x=y$ 6. $P(y)\wedge Q(y)$

8.

$\forall x(P(x)\wedge Q(x))\quad I\forall(2-7)$

Ejemplo VII.5.

Demostrar la validez de $\forall x(P(x)\wedge Q(x))\vdash\forall xP(x)\wedge\forall xQ(x)$ .

1.

$\forall x(P(x)\wedge Q(x))$ Pr

[resume] 1. $y$ Variable fresca 2. $P(y)\wedge Q(y)\quad E\forall,1,x=y$ 3. $P(y)\quad E\wedge,3$

5.

$\forall xP(x)\quad I\forall(2-3)$

6. $z$ Variable fresca 7. $P(z)\wedge Q(z)\quad E\forall,1,x=z$ 8. $Q(z)\quad E\wedge,7$

9.

$\forall xQ(x)\quad I\forall(6-8)$
10.

$\forall xP(x)\wedge\forall xQ(x)\quad I\wedge,5,9$

Definición VII.4 (Regla de eliminacion del existencial,

E\exists

Sea $y$ una variable fresca y que no aparece libre en $\psi$ .

\begin{array}[]{c}\exists x\varphi(x)\\ \varphi(v)\to\psi\\ \hline\cr\psi\end{array}

Observación VII.3.

Tipicamente la regla $E\exists$ se usa cuando se tiene una formula $\exists x\varphi(x)$ , iniciando una demostracion auxiliar que tiene como premisa auxiliar $\varphi(y)$ y llegando a una conclusion que no dependa de $y$ .

$\exists x\varphi(x)$

$\varphi(y)\qquad\quad\text{Premisa auxiliar}$ $\vdots$ $\psi$ $\begin{array}[]{lr}\varphi(y)\rightarrow\psi&I\rightarrow\\ \psi&E\exists\end{array}$

Ejemplo VII.6.

Demostrar la validez de $\left\{\forall x(P(x)\to Q(x)),\exists xP(x)\right\}\vdash\exists xQ(x)$ .

1.

$\exists xP(x)$ Pr
2.

$\forall x(P(x)\to Q(x))$ Pr

[resume] 1. $P(y)$ Pr aux (var fresca) 2. $P(y)\to Q(y)\quad E\forall,2,x=y$ 3. $Q(y)\quad E\to,3,4$ 4. $\exists xQ(x)\quad I\exists,5,x=y$

7.

$P(y)\to\exists xQ(x)\quad I\to(3-6)$
8.

$\exists xQ(x)\quad E\exists,1,7$

Ejemplo VII.7.

Demostrar la validez de $\left\{\exists xP(x),\exists xQ(x)\right\}\vdash\exists x\exists y(P(x)\wedge Q% (y))$ .

1.

$\exists xP(x)$ Pr
2.

$\exists xQ(x)$ Pr

[resume] 1. $P(z)$ Pr aux (z var fresca) 4. $Q(t)$ Pr aux (t var fresca) 5. $P(z)\wedge Q(t)\quad I\wedge,3,4$ 6. $\exists y(P(z)\wedge Q(y))\quad I\exists,5,y=t$ 7. $Q(t)\to\exists y(P(z)\wedge Q(y))\quad I\to(4-6)$ 8. $\exists y(P(z)\wedge Q(y))\quad E\exists,2,7$ 9. $\exists x\exists y(P(x)\wedge Q(y))\quad I\exists,8,x=z$

10.

$P(z)\to\exists x\exists y(P(x)\wedge Q(y))\quad I\to(3-9)$
11.

$\exists x\exists y(P(x)\wedge Q(y))\quad E\exists,1,10$

Ejemplo VII.8.

Demostrar la validez de $\exists y\forall xP(x,y)\vdash\forall x\exists yP(x,y)$ .

1.

$\exists y\forall xP(x,y)$ Pr

[resume] 1. $\forall xP(x,z)$ Pr aux (var fresca) 3. $t$ Var fresca 4. $P(t,z)\quad E\forall,2,x=t$ 5. $\exists yP(x,y)\quad I\exists,4,y=z$ 6. $\forall x\exists yP(x,y)\quad I\forall(3-5)$

7.

$\forall xP(x,z)\to\forall x\exists yP(x,y)\quad I\to(2-6)$
8.

$\forall x\exists yP(x,y)\quad E\exists,1,7$

Observación VII.4.

Se puede demostrar que el sistema de Gentzen que hemos introducido es correcto y completo para la logica de predicados. Sin embargo, esta logica no es decidible.