When are we allowed to use the $\exists$ elimination rule in first-order natural deduction?

Question

I don't really understand when we're allowed to use $\exists$-elimination when making first-order natural deduction proofs. I understand that the criteria are that the variable must be free in the conclusion, and in the "context" of the implication. When reading this, I feel like I understand, but when looking at examples, I get confused. For example,

$\exists x P(x)$ and $P(x) \implies \forall y P(y)$, we cannot use the elimination rule; why is this?

Another example would be $\exists x P(x)$ and $P(x) \implies P(x)$. Here I understand that, since x is free in $P(x)$, we cannot use the elimination. However, would it be possible if we instead had $\exists x P(x)$ and $P(x) \implies \forall xP(x)$?

If so, why? Wouldn't x still be free in the context?

Any help is appreciated. Thanks!

Adding picture:

$\begin{array}{lllll} 1&1&\text{Assume }\exists x\,P(x)\land(P(x)\to\forall y\,Q(y))&\qquad\\ 1&2&\exists x~P(x) &&\land E_1,1\\ 1 &3& P(x)\to\forall y~Q(y)&&\land E_2,1\\ \color{red}1&4&\forall y~Q(y)&&\exists E~2, 3~\color{red}{\text{ERROR}} \end{array}$

Answer 1

The $\exists$-elimination rule :

$$ \frac{\begin{array}{ccc} &&\phi[x_0/x]\\ &&\vdots\\ \exists x\phi&&\psi \end{array}}{\psi}\exists\text{-elim} $$

holds with the following proviso :

$x_0$ does not occur in $\psi$, $\phi$ or any undischarged assumption of the subderivation of $\psi$, except $\phi[x_0/x]$.

---

Here is an example showing the need for the proviso in the $\exists$-elim rule :

1) $\exists x(x=0)$ --- assumed

2) $(x=0)$ --- assumed for $\exists$-elim

3) $x=0$ --- from 2) and 1) by $\exists$-elim, discharging 2) : illegal ! $x=0$ is "the $\psi$" and we have the variable $x$ used in the $\exists$-elim application free in it

4) $\forall x(x=0)$ --- $\forall$-intro : correct ; there are no free occurrence of $x$ in the only assumption left, i.e. into 1)

5) $\exists x(x=0) \to \forall x(x=0)$ --- $\to$-intro.

The conclusion is clearly false in $\mathbb N$.

---

The intuition about the rule is this : we know that there is something that is $P$. Call it $x_0$ (a new term; this is required by the proviso asking for a term that does not occur in any undischarged assumption ).

Form $P(x_0)$ we derive a conclusion $\psi$ that does not "depend" on $x_0$ (and this is for sure satisfied if $x_0$ does not occur in $\psi$).

Thus, we can discard the temporary assumption $P(x_0)$ and the conclusion follows from the premise $\exists x P(x)$.

---

---

In your example, $\forall y Q(y)$ is the conclusion $\psi$ and $x$ is free into the hypothesis 1) that is an undischarged assumption of the subderivation of $\psi$.

Thus, the proviso has been violated.

Answer 2

Using my DC Proof 2.0

DC Proof will not allow the use of $x$ as both a bound and a free variable within a statement, saving much confusion. As you can see, you won't be able to apply Detachment (Modus Ponens) here.

Suggestion: Try to use the lowercase letters a-j for bound variables, the remaining lowercase letters for free variables. This also avoids some confusion.