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.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

$--- u$
$---- {\forall}I^a$
$\forall x . P(x)$
$---- {\forall}E$
$------ {\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|cite|improve this question
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|cite|improve this answer

Your Answer


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.