It seems to me that for most of the twentieth century, axiomatic foundations for mathematical theories were constructed with the (mostly allied) goals of minimizing the number of primitive notions and minimizing the number of axioms. But one could equally well be guided by the goal of minimizing the logical depth of the axioms, i.e., minimizing the use of quantifiers.


Consider group theory, for instance. I have seen formalizations of group theory that say "There exists an element $h \in G$ such that for all $g \in G$, $gh=hg=g$" and then go on to prove that $h$ is unique and to name it $e$. But I have also seen formalizations that say "A group is a set $G$ equipped with an element $e$ such that..." which eliminates the need for a quantifier in an axiom. Likewise, if one includes the operation $g \mapsto g^{-1}$ as a primitive, one can avoid the axiom "For all $g$ there exists $h$ such that $gh=hg=e$" (or worse, "For all $g$ there exists $h$ such that for all $h'$, $ ghh'=hgh'=h'gh=h'hg"$, which I haven't seen, but which I can imagine a certain sorts of purist preferring!).


I know that in constructive mathematics, the status of existential quantifiers is suspect to begin with, so I imagine that there's already quite a bit of writing in foundations and philosophy of mathematics (and maybe computable mathematics as well) that addresses this issue. Some pointers to relevant literature would be appreciated.



getting rid of existential quantifiers
You're thinking of the process known as [Skolemization](http://en.wikipedia.org/wiki/Skolem_normal_form), which eliminates existential quantifiers at the cost of introducing new function or constant symbols in the language. The identity and inverse situation you describe are both examples of this.


The process is generally straightforward. To Skolemize the a formula like $$\forall x \exists y (P(x,y) \rightarrow \forall z Q(y,z)),$$ we introduce a new unary function symbol $f$ and we obtain the Skolem normal form $$\forall x (P(x,f(x)) \rightarrow \forall z Q(f(x),z)).$$ Note how the new function depends only on the variable $x$ since the $\exists y$ quantifier we are replacing is not within the scope of the $\forall z$ quantifier.


The Skolem normal form is always equisatisfiable with the original: if the first has a model then the second has a model and vice versa. In fact any model of the original sentence can be expanded to a model of the new sentence by interpreting the new symbols functions that pick appropriate witnesses for the statements involved. (This construction requires the Axiom of Choice to carry out in full generality.)


One drawback of Skolemization is that the new functions can be very complex and thus models become harder to describe. For example, it is often the case that the original sentence has a computable model but that the Skolem normal form does not. Another drawback is that function symbols are sometimes undesirable or unnatural. For example, the usual density axiom for linear orders $$\forall x \forall y(x \lt y \rightarrow \exists z(x \lt z \land z \lt y))$$ is rarely seen in its Skolemized form $$\forall x \forall y(x \lt y \rightarrow x \lt b(x,y) \land b(x,y) \lt y)$$ since one usually thinks of linear orders as strictly relational structures.


