Formal proof involving existential quantifier It is common sense that to derive a formula with existential quantifier is only necessary to prove that a formula is valid for any term , ie:
$\Gamma$ , $\phi$ [t/x] $\vdash$ $\exists$x$\phi$.
By definition t could be any term since it is free for x in $\phi$. So my question is, If I want to prove $\exists$x$\phi$ then I can prove that $\phi$ is true for a constant or weird function in a particular universe ?
For example:
Let $\phi$ = Even(x). I wish to prove that 2 is even, denoted by Even(2), in a Universe = $\mathbb{Z}.$
2 = 2 * 1.
Then by definition $\exists$x(2 = 2x). Even(2).
Therefore $\exists$x($\phi$[2/x]).
Is this correct, can i prove any existential quantifier for any function that involves x, variable or constant?
 A: In Natural Deduction, we have the $\exists$-introduction rule [following Trismegistos correction]:
if a derivation $D$ of $\phi(t/x)$ exists, then we can infer $\exists x \phi(x)$, and its undischarched assumptions are those of $D$ (provided that $t$ is free for $x$ in $\phi$).
So, if $\Gamma$ is the set of closure of FO Peano Axioms, and you will provide a proof of "$2$ is even" (i.e. $\phi(2)$) from them (i.e. a derivation $D$ of $\phi(2)$ from $\Gamma$) youn can "add" to $D$ a new step using $\exists$-intro and obtain a proof of "there are even numbers" (i.e. $\exists x\phi(x)$).
The First-Order logical calculus is sound : if $\Gamma \vdash \phi$ then $\Gamma ⊨ \phi$. This means that, if $\Gamma$ is as above, all theorems you can prove from FO Peano Axioms are logical consequences of them, i.e. are true in all models of the Axioms.
A: As far as I understood, $\Gamma$ was a set of sentences. In that case, proving $\Gamma \vdash \exists x\phi$ is the same as proving that sentence in every model of $\Gamma$. That is, if $\mathcal M \models \Gamma$, then $\mathcal M \models \exists x\phi$. In your example, you checked for only one model.
Because you don't know for which model you should get the realization of the formula, you cannot specify a constant, if the constant is not included in your language. You should really find a term realizing the formula. And in the case, when there are constants in your language realizing the formula, those constants are particular cases of terms too.
