In some deduction systems there is a rule* that given $\exists x (\phi(x))$, we can infer $\phi(y)$, where $y$ is a fresh variable (i.e., one we haven't yet mentioned in this context). Call this rule "EI."

(Edit: in the opening sentence I originally said "in natural deduction systems there is typically a rule that..." Andrej Bauer has kindly informed me that natural deduction systems typically do not have this rule. In this post I am, I have learned, using a somewhat unusual set of conventions regarding the treatment of free variables.)

Let $M$ denote a model, $A,B$ variable assignments, and $T,U$ theories. Let $\text{fv}(T)$ denote the set of variables free in $T$. Let $A|_{\text{fv}(T)}$ denote $A$ restricted in its domain to $\text{fv}(T)$.

Call this the "simple definition" of semantic entailment: $T \models U$ iff, for all $M,A$, if $M,A \models T$ then $M,A \models U$. We can't use the simple definition in a system with EI, because $A$ might not contain an appropriate value in a fresh variable we instantiate into.

For contrast, call this the "complicated definition" of semantic entailment: $T \models U$ iff, for all $M,A$, if $M,A \models T$ then $M,B \models U$, for some $B \supseteq A|_{\text{fv}(T)}$. That is, we can change the values of unused variables across semantic entailments. This definition is compatible with EI.

My questions:

Does a typical Hilbert system (e.g., the one on Wiki) allow for anything like EI? Can we actually infer $\phi(y)$ (with $y$ fresh) from $\exists x (\phi(x))$? If not, how do we make up for the lack of this feature?

Can a typical Hilbert system be interpreted by the simple definition of semantic entailment?

The Henkin-style completeness proofs with which I am familiar (e.g., this one) make essential use of EI in the step of constructing a maximal, consistent superset with witnesses. If Hilbert systems don't have EI, how do we fulfill the function of this step? If Hilbert systems don't have EI, is it even possible to prove them complete using a Henkin-style proof, or do we need to use a completely different method?

I'm asking because I'm trying to write a completeness proof for a non-classical logic (a variant of LP), with a Hilbert-style deduction system.

Thank you for your help!