Parte VII Teoria de la demostracion en logica de predicados

Observación.

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

Ejemplo.

D={personas}\displaystyle D=\{\text{personas}\}

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

“La madre de Antonio es rubia”.

R⁢(x):\displaystyle R(x)\colon x es rubio. R⁢(m⁢(a))\displaystyle R(m(a)).

∀x⁢(M⁢(x,a)→R⁢(x))\displaystyle\forall x(M(x,a)\rightarrow R(x))

“Todos los hermanos de Antonio son rubios” ⇒∀x⁢(H⁢(x,a)→R⁢(x))\displaystyle\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⁢∀\displaystyle E\forall I⁢∀\displaystyle I\forall
E⁢∃\displaystyle E\exists I⁢∃\displaystyle I\exists
Proposición 25.3.
  •  
    ​

    φ,ψ,…\displaystyle\varphi,\psi,\ldots representaran formulas cualesquiera de la logica de predicados.

  •  
    ​

    φ⁢(x)\displaystyle\varphi(x) denotara una formula donde la variable x\displaystyle x tiene apariciones libres. Si despues escribimos φ⁢(t)\displaystyle\varphi(t), donde t\displaystyle t puede ser un termino cualquiera, esto representara la formula φ\displaystyle\varphi donde todas las apariciones libres de x\displaystyle x se han sustituido por t\displaystyle t.

  •  
    ​

    Llamaremos variable fresca a una variable que no ha aparecido previamente en el razonamiento.

Definición 25.4 (Regla de eliminacion del universal, E⁢∀\displaystyle E\forall).

Sea t\displaystyle t un termino cualquiera

∀x⁢φ⁢(x)φ⁢(t)\displaystyle\begin{array}[]{c}\forall x\varphi(x)\\ \hline\cr\varphi(t)\end{array}
Definición 25.5 (Regla de introduccion del existencial, I⁢∃\displaystyle I\exists).

Sea t\displaystyle t un termino cualquiera

φ⁢(t)∃x⁢φ⁢(x)\displaystyle\begin{array}[]{c }\varphi(t)\\ \hline\cr\exists x\varphi(x)\end{array}
Ejemplo.

Demostrar la validez de {∀x⁢(P⁢(x)→Q⁢(x)),P⁢(a)}⊢Q⁢(a)\displaystyle\{\forall x(P(x)\to Q(x)),P(a)\}\vdash Q(a).

  1. 1.
    ​

    ∀x⁢(P⁢(x)→Q⁢(x))\displaystyle\forall x(P(x)\to Q(x)) Pr

  2. 2.
    ​

    P⁢(a)\displaystyle P(a) Pr

  3. 3.
    ​

    P⁢(a)→Q⁢(a)E⁢∀,1,x=a\displaystyle P(a)\to Q(a)\quad E\forall,1,x=a

  4. 4.
    ​

    Q⁢(a)E→,2,3\displaystyle Q(a)\quad E\rightarrow,2,3

Ejemplo.

Demostrar la validez de {P⁢(b),∃x⁢P⁢(x)→Q⁢(a)}⊢Q⁢(a)\displaystyle\{P(b),\exists xP(x)\to Q(a)\}\vdash Q(a).

  1. 1.
    ​

    P⁢(b)\displaystyle P(b) Pr

  2. 2.
    ​

    ∃x⁢P⁢(x)⁢t⁢o⁢Q⁢(a)\displaystyle\exists xP(x)toQ(a) Pr

  3. 3.
    ​

    ∃x⁢P⁢(x)I⁢∃,1\displaystyle\exists xP(x)\quad I\exists,1

  4. 4.
    ​

    Q⁢(a)E→,2,3\displaystyle Q(a)\quad E\rightarrow,2,3

Definición 25.6 (Regla de introduccion del universal, I⁢∀\displaystyle I\forall).
y Variable fresca ⋮ ⁢ φ ( y ) ∀x⁢φ⁢(x)\displaystyle\begin{array}[]{c}\noindent\framebox{\parbox{426.82pt}{ $\displaystyle y\qquad\qquad\quad\;\text{Variable fresca}$ \\ $\displaystyle\vdots$ \\ $\displaystyle\varphi(y)$}}\\ \hline\cr\forall x\varphi(x)\end{array}
Observación.

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.

Demostrar la validez de ∀x⁢P⁢(x)∧∀x⁢Q⁢(x)⊢∀x⁢(P⁢(x)∧Q⁢(x))\displaystyle\forall xP(x)\wedge\forall xQ(x)\vdash\forall x(P(x)\wedge Q(x))

  1. 1.
    ​

    ∀x⁢P⁢(x)∧∀x⁢Q⁢(x)\displaystyle\forall xP(x)\wedge\forall xQ(x)

2.​y\displaystyle y Variable fresca 3.​∀x⁢P⁢(x)E∧,1\displaystyle\forall xP(x)\quad E\wedge,1 4.​P⁢(y)E⁢∀,3,x=y\displaystyle P(y)\quad E\forall,3,x=y 5.​∀x⁢Q⁢(x)E∧,1\displaystyle\forall xQ(x)\quad E\wedge,1 6.​Q⁢(y)E⁢∀,5,x=y\displaystyle Q(y)\quad E\forall,5,x=y 7.​P⁢(y)∧Q⁢(y)\displaystyle P(y)\wedge Q(y)

  1. 8.
    ​

    ∀x⁢(P⁢(x)∧Q⁢(x))I⁢∀(2−7)\displaystyle\forall x(P(x)\wedge Q(x))\quad I\forall(2-7)

Ejemplo.

Demostrar la validez de ∀x⁢(P⁢(x)∧Q⁢(x))⊢∀x⁢P⁢(x)∧∀x⁢Q⁢(x)\displaystyle\forall x(P(x)\wedge Q(x))\vdash\forall xP(x)\wedge\forall xQ(x).

  1. 1.
    ​

    ∀x⁢(P⁢(x)∧Q⁢(x))\displaystyle\forall x(P(x)\wedge Q(x)) Pr

2.​y\displaystyle y Variable fresca 3.​P⁢(y)∧Q⁢(y)E⁢∀,1,x=y\displaystyle P(y)\wedge Q(y)\quad E\forall,1,x=y 4.​P⁢(y)E∧,3\displaystyle P(y)\quad E\wedge,3

  1. 5.
    ​

    ∀x⁢P⁢(x)I⁢∀(2−3)\displaystyle\forall xP(x)\quad I\forall(2-3)

6.​z\displaystyle z Variable fresca 7.​P⁢(z)∧Q⁢(z)E⁢∀,1,x=z\displaystyle P(z)\wedge Q(z)\quad E\forall,1,x=z 8.​Q⁢(z)E∧,7\displaystyle Q(z)\quad E\wedge,7

  1. 9.
    ​

    ∀x⁢Q⁢(x)I⁢∀(6−8)\displaystyle\forall xQ(x)\quad I\forall(6-8)

  2. 10.
    ​

    ∀x⁢P⁢(x)∧∀x⁢Q⁢(x)I∧,5,9\displaystyle\forall xP(x)\wedge\forall xQ(x)\quad I\wedge,5,9

Definición 25.7 (Regla de eliminacion del existencial, E⁢∃\displaystyle E\exists).

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

∃x⁢φ⁢(x)φ⁢(v)→ψψ\displaystyle\begin{array}[]{c}\exists x\varphi(x)\\ \varphi(v)\to\psi\\ \hline\cr\psi\end{array}
Observación.

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

∃x⁢φ⁢(x)\displaystyle\exists x\varphi(x) φ⁢(y)Premisa auxiliar\displaystyle\varphi(y)\qquad\quad\text{Premisa auxiliar} ⋮\displaystyle\vdots ψ\displaystyle\psi φ⁢(y)→ψI→ψE⁢∃\displaystyle\begin{array}[]{lr}\varphi(y)\rightarrow\psi&I\rightarrow\\ \psi&E\exists\end{array}
Ejemplo.

Demostrar la validez de {∀x⁢(P⁢(x)→Q⁢(x)),∃x⁢P⁢(x)}⊢∃x⁢Q⁢(x)\displaystyle\{\forall x(P(x)\to Q(x)),\exists xP(x)\}\vdash\exists xQ(x).

  1. 1.
    ​

    ∃x⁢P⁢(x)\displaystyle\exists xP(x) Pr

  2. 2.
    ​

    ∀x⁢(P⁢(x)→Q⁢(x))\displaystyle\forall x(P(x)\to Q(x)) Pr

3.​P⁢(y)\displaystyle P(y) Pr aux (var fresca) 4.​P⁢(y)→Q⁢(y)E⁢∀,2,x=y\displaystyle P(y)\to Q(y)\quad E\forall,2,x=y 5.​Q⁢(y)E→,3,4\displaystyle Q(y)\quad E\to,3,4 6.​∃x⁢Q⁢(x)I⁢∃,5,x=y\displaystyle\exists xQ(x)\quad I\exists,5,x=y

  1. 7.
    ​

    P⁢(y)→∃x⁢Q⁢(x)I→(3−6)\displaystyle P(y)\to\exists xQ(x)\quad I\to(3-6)

  2. 8.
    ​

    ∃x⁢Q⁢(x)E⁢∃,1,7\displaystyle\exists xQ(x)\quad E\exists,1,7

Ejemplo.

Demostrar la validez de {∃x⁢P⁢(x),∃x⁢Q⁢(x)}⊢∃x⁢∃y⁢(P⁢(x)∧Q⁢(y))\displaystyle\{\exists xP(x),\exists xQ(x)\}\vdash\exists x\exists y(P(x)% \wedge Q(y)).

  1. 1.
    ​

    ∃x⁢P⁢(x)\displaystyle\exists xP(x) Pr

  2. 2.
    ​

    ∃x⁢Q⁢(x)\displaystyle\exists xQ(x) Pr

3.​P⁢(z)\displaystyle P(z) Pr aux (z var fresca) 4.​Q⁢(t)\displaystyle Q(t) Pr aux (t var fresca) 5.​P⁢(z)∧Q⁢(t)I∧,3,4\displaystyle P(z)\wedge Q(t)\quad I\wedge,3,4 6.​∃y⁢(P⁢(z)∧Q⁢(y))I⁢∃,5,y=t\displaystyle\exists y(P(z)\wedge Q(y))\quad I\exists,5,y=t 7.​Q⁢(t)→∃y⁢(P⁢(z)∧Q⁢(y))I→(4−6)\displaystyle Q(t)\to\exists y(P(z)\wedge Q(y))\quad I\to(4-6) 8.​∃y⁢(P⁢(z)∧Q⁢(y))E⁢∃,2,7\displaystyle\exists y(P(z)\wedge Q(y))\quad E\exists,2,7 9.​∃x⁢∃y⁢(P⁢(x)∧Q⁢(y))I⁢∃,8,x=z\displaystyle\exists x\exists y(P(x)\wedge Q(y))\quad I\exists,8,x=z

  1. 10.
    ​

    P⁢(z)→∃x⁢∃y⁢(P⁢(x)∧Q⁢(y))I→(3−9)\displaystyle P(z)\to\exists x\exists y(P(x)\wedge Q(y))\quad I\to(3-9)

  2. 11.
    ​

    ∃x⁢∃y⁢(P⁢(x)∧Q⁢(y))E⁢∃,1,10\displaystyle\exists x\exists y(P(x)\wedge Q(y))\quad E\exists,1,10

Ejemplo.

Demostrar la validez de ∃y⁢∀x⁢P⁢(x,y)⊢∀x⁢∃y⁢P⁢(x,y)\displaystyle\exists y\forall xP(x,y)\vdash\forall x\exists yP(x,y).

  1. 1.
    ​

    ∃y⁢∀x⁢P⁢(x,y)\displaystyle\exists y\forall xP(x,y) Pr

2.​∀x⁢P⁢(x,z)\displaystyle\forall xP(x,z) Pr aux (var fresca) 3.​t\displaystyle t Var fresca 4.​P⁢(t,z)E⁢∀,2,x=t\displaystyle P(t,z)\quad E\forall,2,x=t 5.​∃y⁢P⁢(x,y)I⁢∃,4,y=z\displaystyle\exists yP(x,y)\quad I\exists,4,y=z 6.​∀x⁢∃y⁢P⁢(x,y)I⁢∀(3−5)\displaystyle\forall x\exists yP(x,y)\quad I\forall(3-5)

  1. 7.
    ​

    ∀x⁢P⁢(x,z)→∀x⁢∃y⁢P⁢(x,y)I→(2−6)\displaystyle\forall xP(x,z)\to\forall x\exists yP(x,y)\quad I\to(2-6)

  2. 8.
    ​

    ∀x⁢∃y⁢P⁢(x,y)E⁢∃,1,7\displaystyle\forall x\exists yP(x,y)\quad E\exists,1,7

Observación.

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.