Part VII Teoria de la demostracion en logica de predicados

Remark 25.10.

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

Example 25.11.

$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$

Proposition 25.12.

•

$\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.

Definition 25.13 (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}

Definition 25.14 (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}

Example 25.15.

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$

Example 25.16.

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$

Definition 25.17 (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}

Remark 25.18.

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.

Example 25.19.

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)$

Example 25.20.

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$

Definition 25.21 (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}

Remark 25.22.

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}$

Example 25.23.

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$

Example 25.24.

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$

Example 25.25.

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$

Remark 25.26.

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.