5
$\begingroup$

Could anybody explain to me what's wrong with the following inference? Thanks.

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

2 Answers 2

9

When using the $\forall$ introduction rule backwards, you must use a fresh variable, a variable that doesn't have anything to do with what you've introduced so far. Since you already have $a$ for $x$, you can't use $a$ for $y$.

Look at the $\forall$ introduction rule says that from $\Gamma \vdash P(a)$, where $a$ does not appear in $\Gamma$, you can infer $\Gamma \vdash \forall a, P(a)$

If you have proved $P(a) \vdash P(a)$, you can't generalize $a$ since it appears also on the left. And also if you had proven $\vdash P(a) \supset P(a)$, and if you wanted to generalize $a$, you would get $\vdash \forall a, P(a) \supset P(a)$, and not $\vdash \forall x, P(a) \supset P(x)$.