Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
add comment

1 Answer

up vote 7 down vote accepted

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

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.