I often see this informal inference rule being used in mathematics:
$$ \frac{\exists x\varphi}{\varphi\left[\frac ax\right]}, $$ where $a$ is the element of the model which satisfies $\varphi$. Since there exists some element such that $\varphi$ holds, we can do this, the reasoning goes. However, this approach has several problems:
This is mixing syntax with semantics, which is erroneous, as in the syntax of FOL, we do not have elements of the domain of models.
We can try to fix this issue by declaring that $a$ is a constant symbol. However, this fails again, because then $\exists x \varphi \vDash \varphi\left[\frac ax\right]$ does not hold, as this meta-theoretic statements ranges over all models, some of which satisfy the antecedent, but not the consequent, as they assign an "incorrect"/arbitrary value to $a$.
I am interested in how to formally ground this very useful intuitive inference. I would appreciate if the solution was extensible into multiple logical calculi (sequent calculus, natural deduction, Hilbert calculus and Fitch calculus come to mind) Thank you for your help. :)
Turning my comments into an answer:
There is indeed a subtlety here. Given that, I think it's best to start from a solid understanding of the semantic situation.
Suppose I have a language $\Sigma$, a set of $\Sigma$-sentences $\Gamma$, a $\Sigma$-formula $\varphi(x)$, and a $\Sigma$-sentence $\psi$. Then - fixing a new constant symbol $c\not\in\Sigma$ - we have the following "conservativity" fact:
The interesting part of this result is of course the $\Leftarrow$ direction, so let me prove that one in detail. I'll use the "language-monotonicity" of FOL, that whenever $\mathfrak{A}$ is a reduct of $\mathfrak{B}$ and $\theta$ is a sentence in the smaller language of $\mathfrak{A}$ then $\mathfrak{A}\models\theta\iff\mathfrak{B}\models\theta$; note that this is not a completely trivial property of logical systems (consider a logic with a quantifier for "Every definable element ...").
Assume that $$\Gamma\cup\{\varphi(c)\}\models\psi\quad\mbox{and}\quad \mathfrak{M}\models\Gamma\cup\{\exists x\varphi(x)\};$$ we want to show $\mathfrak{M}\models\psi$. Since $\mathfrak{M}\models\exists x\varphi(x)$, we can pick some $m\in\varphi^\mathfrak{M}$. Now consider the expansion of $\mathfrak{M}$ gotten by interpreting $c$ as $m$; call this $\mathfrak{M}'$. We have by choice of $m$ that $$\mathfrak{M}'\models\varphi(c),$$ and so by "language monotonicity" upwards from $\mathfrak{M}$ to $\mathfrak{M}'$ we get $$\mathfrak{M}'\models\Gamma$$ (since $\mathfrak{M}\models\Gamma$). By the first part of our assumption above (the RHS of the bi-implication we're trying to establish) we get $$\mathfrak{M}'\models\psi.$$ But now applying "language-monotonicity" downwards this time we get $$\mathfrak{M}\models\psi$$ as desired.
This sort of language-juggling can feel slippery at first. Here are a couple comments that might help:
First, note that the "language-monotonicity" fact mentioned above is not as trivial as it may first appear! There are perfectly meaningful logics which lack it. For instance, consider the version of FOL augmented by a quantifier for "Every definable set ..." This quantifier is very sensitive to changes of language (consider e.g. shifting from $\{+\}$ to $\{+,\times\}$ in the context of $\mathbb{N}$), and so we lose language-monotonicity in a rather dramatic way. So even though language-monotonicity is not hard to prove (or even hard not to prove) for FOL, it is actually substantive.
Second, there are more interesting examples of language-juggling that you'll see down the road. Compactness introduces some - there are lots of applications of compactness that require us to add a new constant, or even worse - and others appear in the context of results like Beth definability and Craig interpolation. Seeing more involved examples of a technique sometimes help demystify it.
Moving from semantics to syntax, the above intuitively tells us that we can safely introduce a new constant symbol in the course of a deduction to serve as a witness to an existential statement as long as we're careful about how that constant symbol appears/is used in the remaining steps of the deduction. Exactly how this caution is implemented will play out differently depending on the system used; personally I find sequent calculus the most intuitive (family of) approach(es), but one's mileage may vary.