A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$
This is an excellent question, and is something which should be explicitly treated in basic logic texts (and in my experience, isn't). Disappointingly or satisfyingly depending on what you're looking for, first-order logic is already enough - at least, initially (see below the fold).
All the constructors you're talking about are definable in an appropriate sense, and so they can be implemented in standard first-order logic by just tweaking the syntax appropriately: basically, we'd add infinitely many new function symbols, each corresponding to an instance of the desired constructor, and axioms saying how they work. In all of the examples you've described, this can be done without difficulty.
For example, let's look at the Hilbert $\epsilon$-operator. Rather than have a single $\epsilon$, we'll have a separate $\epsilon_A$ for each formula $A$ with at least one free variable, and these will behave as follows:
The simplest case is for single-variable (so, parameter-free) $A$. In this case, $\epsilon_A$ is nullary - it's just a constant. And our corresponding axiom is $$\exists xA(x)\implies A(\epsilon_A).$$
Now let's look at the case where $A$ has two free variables, $x$ and $y$. We might now want to write something which for each $b$ picks some $a$ such that $A(a,b)$ holds (if such an $a$ exists). So our $\epsilon_A$ is now a unary function, and the corresponding axiom is $$\forall y(\exists xA(x,y)\implies A(\epsilon_A(y),y)).$$
More generally, an $(n+1)$-ary $A$ yields an $n$-ary $\epsilon_A$, with corresponding axiom $$\forall y_1,...,y_n(\exists xA(x,y_1,...,y_n)\implies A(\epsilon_A(y_1,...,y_n), y_1,...,y_n)).$$
Note the similarity between this kind of implementation and Skolem functions - it's exactly the same idea. Incidentally, it is at this point arguably better to adopt a version of first-order logic which allows for partial functions and empty structures, just for simplicity; the deductive apparatus of course gets more annoying, but very manageably so, and it might clean things up in certain respects. But that's not an essential point.
Of course, there's a more general question here which the above fails to address: what if we're looking for a general theory which allows for (essentially) arbitrary ways to build terms out of formulas?
In this case it seems that there is actually not too much literature out there. I asked an MO question about this a while back, since this is a topic I've already started working on and I wanted to avoid reinventing the wheel. Some basic model theory for the resulting logic is easy enough to whip up, but it seems not to have been done explicitly yet; the existing work seems to be on the computer science side, and not focused on those topics. (Incidentally, Andrej's answer to that question is a great example of how logicians should pay attention to computer science.)
If you're interested, I can tell you what I know about the resulting logic. But that gets a bit far afield for this answer, so I'll stop here for now.
(Incidentally, it looks like I forgot to mention the specific motivation at that question; briefly, I was - and am - playing around with abstract Godel numbering notions in the context of generalized recursion theory.)