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.

quantifier elimination: en.wikipedia.org/wiki/Quantifier_elimination – Gerald Edgar Mar 6 '12 at 1:37