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

0

$--- 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(y)$
$--------- {\forall}I^a$
$\forall x . \forall y . P(x) \supset P(y)$

Universal Introduction is an assumption discharging rule of inference.

Those indices are to bookkeep the rise and discharge of assumptions, and the order in which you do so.   You must discharge assumptions in the reverse order that they were raised; and assumptions are no longer active after they are discharged.

Besides, that is an improper application of Universal Introduction.   You may only use it to deduce $\forall x~P(x)$ where you have derived $P(a)$ from no other assumptions about the term and are discharging the term.

Here's the fitch representation of your proof to clarify the error

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{}{\fitch{[a]}{\fitch{[b]}{\fitch{P(a)}{\forall x~P(x)\quad\gets\text{Invalid}\\P(b)}\\P(a)\to P(b)}\\\forall y~P(a)\to P(y)}\\\forall x\forall y~P(x)\to P(y)}$$