In model theory one has to define functions and relations on a set for the function and relation symbols of the logical theory.
My questions are:
What kind of operations are allowed to define those functions and relations?
Must the definitions be constructible?
Can one use another logical theory as a model for a theory?
Are quantifiers allowed?
On
One can use any definition. However, when speaking about "informal mathematics", there is a distinction between "informal definition" and "something that is not a definition". Let's say you want to define a set. Starting with a simple example, you could say "the set of prime numbers". It's an informal definition, but it's still a definition, in the sense that if you have a number, you can determine if it's prime or not, so there's only one candidate. You could make the definition formal with a little effort, but if the set is defined by a very complex algorithm it may not be the case, yet it's still a definition as long as it defines unambiguously the mathematical object (although unambiguously is usually "up to isomorphism"...).
Trouble comes when you have "not a definition", for example the old notion of "arithmetic". The problem is not in itself that the notion was informal, it's that it was not a definition at all, so 'what an arithmetical statement is' was up to debate. The formalisation came to solve this issue, but then there's a step to acknowledge that the formal object does capture the notion "we had in mind" (in fact there's still discussion about it).
In general, you need to have 'arbitrary definitions'. The reason is that if you consider only the objects that have a 'short' or a 'simple' definition, it will only form a subclass of the objects. For example, the reals that can be defined with a short definition do not constitute all reals, by a simple diagonalization argument. It is often a question of great interest to characterize objects that have a nice definition, for various notions of nice.
When studying group theory, do you ask "What kind of operations are allowed to define the group operation? Are you allowed to use quantifiers to define the group operation?" A group is just any set together with any operation satisfying the group axioms. It's the same in model theory - a structure is any set together with any constants, functions, and relations on that set. Of course, what structures (and what groups!) you can prove exist may depend on your meta-theory, which could be informal mathematics or your favorite formal system.
In the comments, you ask about formal proofs of consistency. Here's an example: Let's say our meta-theory is ZFC. ZFC can prove the completeness theorem. So given a theory $T$, if ZFC can prove "there exists a model of $T$", then ZFC can prove "$T$ is consistent".