First, the standard definition of semantic entailment is neither the “simple” one nor the “complicated” one, but the following: $T\models U$ iff for every $M$, if $M,A\models T$ for every $A$, then $M,A\models U$ for every $A$.
First-order Hilbert-style usually employ some form of a generalization rule: the simplest one is $$\phi\vdash\forall x\,\phi,$$ other common variants include $$\begin{align} \psi\to\phi\vdash\psi\to\forall x\,\phi,\\ \phi\to\psi\vdash\exists x\,\phi\to\psi, \end{align}$$ where $x$ must not occur free in $\psi$. (The choice of the rules depends on other axioms of the system, and of course on the logic, if you are dealing with non-classical systems.) Notice that these rules are not sound with respect to either your “simple” or “complicated” definition, but they are sound with respect to the semantics I gave above. (Note also that the system on the Wikipedia page, with no generalization rules, is quite unconventional.)
The way to simulate existential instantiation in Hilbert systems in is by means of a “meta-rule”, much like you’d use the deduction theorem to simulate the implication introduction rule. The most common formulation is:
Lemma 1: If $T\vdash\phi(c)$, where $c$ is a constant not appearing in $T$ or $\phi$, then $T\vdash\forall x\,\phi(x)$.
A version with explicit existential quantifiers may look like this:
Lemma 1’: If $T\vdash\psi(c)\to\phi$, where $c$ is a constant not appearing in $T$, $\phi$, or $\psi$, then $T\vdash\exists x\,\psi(x)\to\phi$.
Both lemmas follow easily by replacing the constant everywhere with a fresh variable, and applying an appropriate version of the generalization rule. In order to simulate the natural deduction existential elimination rule, you are in a situation where you have already derived (or assume) $\exists x\,\psi(x)$. You add $\psi(c)$ as an extra assumption, where $c$ is a fresh constant, and derive the desired result $\phi$. By deduction theorem (you have to make sure to satisfy its hypotheses, such as by not using generalization rules in the proof snippet, or by assuming $\psi(c)$ is a sentence), this implies the provability of $\psi(c)\to\phi$, and therefore of $\exists x\,\psi(x)\to\phi$ by Lemma 1’.
In particular, the construction of a Henkin completion of a theory basically needs that if $T+\exists x\,\psi(x)$ is consistent, where $\psi(x)$ has no other free variable, then $T+\psi(c)$ is consistent, where $c$ is a fresh constant. This follows from Lemma 1’ and the deduction theorem in the way I indicated.
