Deduce $ \forall x P(x) \vdash \exists xP(x) $ Well it's a little awkward but how can I show this in a natural deduction proof?
$ \forall x P(x) \vdash \exists xP(x) $
I think one has too proof that with a proof by contradiction rule but since I cannot eliminate the $ \exists $ quantifier I am stuck. I know this is a quite simple example. 
Any help would be appreciated!
 A: It is a consequence of the rule of Universal Specification in standard first-order logic (FOL). Implicit is the assumption that the domain of discourse is non-empty. 
In my own work,  I never make use of this assumption. I usually make the domain of discourse explicit, e.g $\forall x\in\mathbb{R}: P(x)$ We know that $\exists x\in\mathbb{R}$, so we can infer that $\exists x\in\mathbb{R}:P(x)$.
A: For a proof with natural Deduction, we refer to Dirk van Dalen, Logic and Structure (5th ed - 2013) for the rules :

$$\frac{∀x \varphi(x) }{\varphi(t)} \text {∀E ; we require $t$ to be free for $x$ in $\varphi$  [page 86] }$$
$$\frac{\varphi[t/x] }{∃x \varphi} \text {∃I, with $t$ free for $x$ in $\varphi$ [page 93]}$$


The proof is quite simple :
(i) $∀xP(x)$ --- assumed
(ii) $P(z)$ --- from (i) by $∀E$, where $z$ is a variable not used in $P(x)$
(iii) $∃xP(x)$ --- from (ii) by $∃I$


$∀xP(x) ⊢ ∃xP(x)$



The above proof is consistent with the previous comments; see van Dalen [page 54] :

Definition 3.2.1 A structure is an ordered sequence $\langle A, R_1,\ldots, R_n, F_1,\ldots, F_m, \{ c_i |i \in I \} \rangle$, where $A$ is a non-empty [emphasis added] set. $R_1,\ldots, R_n$ are relations on $A$, $F_1,\ldots, F_m$ are functions on $A$, and the $c_i (i \in I)$ are elements of $A$ (constants).


In order to admit also empty domains, the above rules regarding quantifiers must be modified; see Free Logic.
