existential elimination

174 Views Asked by At

In the rule of existential elimination

$$\underline{\Delta \vdash \ \exists a \phi (a) \hskip 0.5 cm \Delta, \phi(a) \vdash \psi} \\ \Delta \vdash \psi$$

it is typically said that the variable $a$ should not appear free in the lower sequent. I can certainly see why the variable $a$ appearing free in $\psi$ would cause problems -- then we could have

$$\underline{\exists a \phi (a) \vdash \ \exists a \phi (a) \hskip 0.5 cm \exists a \phi (a), \phi(a) \vdash \phi(a)} \\ \exists a \phi (a) \vdash \phi(a)$$

which is clearly problematic. What I can't quite see is what harm would come from $a$ appearing free in $\Delta$. Is there a problematic instance of this rule in which $a$ appears free in $\Delta$, but not $\psi$?

1

There are 1 best solutions below

1
On BEST ANSWER

$$\underline{ a=0 \vdash \exists a(a=1)\hskip 0.5 cm a=0, a=1\vdash 0=1} \\ a=0 \vdash 0=1$$