What's wrong with this natural deduction proof?

Question

According to natural deduction $\forall$ $x$ $\exists$ y $P(x,y)$ $\models$ $\exists$ $x$ $\forall$ y $P(x,y)$ is incorrect. However I am able to prove the following using the rules of natural deduction. Consider this proof:

1. $\forall$ $x$ $\exists$ y $P(x,y)$ ------------- data
2. $\exists$ y $P(a,y)$ ----------------- $\forall$ elimination
3. $P(a,e)$ --------------------- $\exists$ elimination
4. $\forall$ x $P(x,e)$ ----------------- $\forall$ introduction
5. $\exists$ $y$ $\forall$ x $P(x,y)$ ------------ $\exists$ introduction

Clearly this proof must have something wrong with it but I cant seem to figure out where?

To clarify the inference rules I have used:

1. $\forall$ elimination says that for a formula $\forall x$F we may derive the conclusion F(x/a) where a is any element from the domain

2. $\forall$ introduction says that for any formula F(x/a) where a is an arbitrary element from the you can derive the $\forall x$F

3. $\exists$ elimination says that for a formula $\exists x$F we may derive the conclusion F(x/e) where e is a specific element of the domain

4. $\exists$ introduction says that for any formula F(x/e) where e is a specific element from the you can derive the $\exists x$F

Answer 1

You have misunderstood the use of $\exists$-Elimination in step 3: the rule is not Existential instantiation.

With $\exists\text{E}$ :

$$\dfrac{∃x \phi(x) \ \ \ \ \ \ \phi[t/x] \vdash \psi}{\psi}$$

we do not infer $\phi[t/x]$ from $∃x \phi(x)$ but - having $∃x \phi(x)$ in our derivation - we assume $\phi[t/x]$. In addition, $t$ must be a term and not an element of the domain.

This means that with $\phi[t/x]$ we start a sub-proof with it as open assumption.

Thus, we cannot apply $\forall\text{I}$ to it with $x$ as variable to be "generalized" [and again, we "generalize" a variable, and not an element of the domain], due to the proviso of the rule $\forall\text{I}$:

$$\dfrac{\phi(x) }{\forall x \ \phi(x)}$$

where the variable $x$ may not occur free in any hypothesis on which $\phi(x)$ depends.

---

In your purported derivation, if we replace $a$ with a free variable, we have :

2) $∃ y P(x,y)$ ----------------- $∀$ elimination

3) $P(x,e)$ --------------------- assumed for $∃$ elimination

4) $∀ x P(x,e)$ ----------------- $∀$ introduction : wrong, because $x$ is free in the assumption 3).

Answer 2

From 1. to 2., you "dropped" the $\forall x$, and try to restore it between 3. and 4. This can't be.