Deducción natural para lógica de predicados

Demostrar usando deducción natural el secuente:

$$\forall y\, Q(b,y), \forall x \forall y \big(Q(x,y) \rightarrow Q(s(x),s(y))\big) \vdash \exists z \big(Q(b,z) \wedge Q\big(z,s(s(b))\big)\big)$$

Podemos interpretar el secuente anterior como una declaración sobre números naturales, donde:

• $b^{(0)}$: es la constante 0
• $s^{(1)}$: es la función sucesor
• $Q(x,y): x\leq y$

Demostrar usando deducción natural el secuente:

$$\forall y\, Q(b,y), \forall x \forall y \big(Q(x,y) \rightarrow Q(s(x),s(y))\big) \vdash \exists z \big(Q(b,z) \wedge Q\big(z,s(s(b))\big)\big)$$

La parte de la derecha dice que hay un natural ($z$) mayor o igual que $b$ y menor o igual que $s(s(b))$.

• En clase demostramos el secuente considerando $z=s(b)$.
• También se puede tener $z=b$ y $z=s(s(b))$, como se verá a continuación.