¿Lo que ' s mal con esta inferencia deducción natural?

Question

¿Podría alguien explicarme cuál es incorrecto con la siguiente inferencia? Gracias.

$--- u$
$P(a)$
$---- {\forall}I^a$
$\forall x . P(x)$
$---- {\forall}E$
$P(b)$
$------ {\supset}I^u$
$P(a) \supset P(b)$
$-------- {\forall}I^b$
$\forall y . P(a) \supset P(b)$
$--------- {\forall}I^a$
$\forall x . \forall y . P(x) \supset P(y)$

Answer 1

Cuando se utiliza el $\forall$ introducción de la regla hacia atrás, usted debe utilizar un fresco de la variable, una variable que no tiene nada que ver con lo que usted ha presentado hasta el momento. Ya que usted ya tiene $a$$x$, no se puede usar $a$$y$.

Ver el $\forall$ introducción de la regla dice que de $\Gamma \vdash P(a)$ donde $a$ no aparece en $\Gamma$, se puede inferir $\Gamma \vdash \forall a, P(a)$

Si has demostrado ser $P(a) \vdash P(a)$, no se puede generalizar $a$, ya que aparece también en la izquierda. Y también si había probado a $\vdash P(a) \supset P(a)$, y si quería generalizar $a$, obtendría $\vdash \forall a, P(a) \supset P(a)$, y no $\vdash \forall x, P(a) \supset P(x)$.