Hfrhyu

It seems that outside of researchers in Mathematical Logic, mathematicians use almost exclusively bounded quantifiers instead of unbounded quantifiers. In fact, I haven't observed any other practice from the very first day on when I was a student.

For example, a logician would write

$forall a : ( a in mathbb R ) rightarrow ( a^2 geq 0 )$

whereas most working analysists and algebraists write

$forall a in mathbb R : a^2 geq 0$

On the other hand, most mathematicians I know accept the idea that all of mathematics can be built up from set-theoretical foundations alone (starting the natural numbers).

So there seems to be a set of assumptions, almost universally agreed upon, which most working mathematicians assume implicitly for their practice. These assumptions start with set theory but apparently exclude unbounded quantifiers. In fact, unless you attend a class in formal logic you might never encounter unbounded quantifiers.

It seems that most mathematicians use a subset of human language enhanced with a subset of mathematical language (avoiding universal quantifiers) as their working language.

Question: Have there been attempts at precisely identifying this mathematical sublanguage and the rules that it governs?

The most ambitious (and well-argued) attempt at formulating a set-theoretical foundation of the type you are proposing using bounded quantification has been suggested by non other than Saunders Mac Lane in the last chapter of his book Mathematics, Form and Function.

Mac Lane dubbed his system ZBQC, which can be described as a weakening of Zermelo set theory in which the scheme of separation is limited to formulae with bounded quantification. Curiously, at the level of consistency strength, ZBQC is the only known lower bound to the consistency strength of Quine's system NF; moreover, it is known that that the urelement-version, NFU, of NF (in which the axiom of infinity is included) is equiconsistent with ZBQC.

On the other hand, Adrian Mathias has critically-and-forcefully responded to Mac Lane's thesis to found mathematics on ZBQC; see here for an article of his addressed to philosophers and general mathematicians, together with a response from Mac Lane; and here for an article addressed to logicians.

Most mathematics can be done in logical systems which are far weaker than Zermelo-Fraenkel set theory. For example, something like structural set theory will suffice for a great deal of ordinary mathematics.

It's not exactly true that mathematicians never use unbounded quantification. For example, in category theory universal properties quantify over all objects of a category. When the category in question is large this amounts to unbounded quantification. In a sense, such quantification is "harmless" because it is "on the outside", i.e., it is of the form $forall X . phi(X)$ where $phi$ itself contains no further unbounded quantifiers. In many cases we can replace such a statement with a schema $phi(X)$ where $X$ is a schematic symbol (that is, instead of having a single formula $forall X . phi(X)$ we have many separate formulas $phi(X)$, one for each $X$).

Occasionally one sees mathematical statements which do contain inner unbounded quantifiers, but those are not common. One example I can think of is the following. The notion of epimorphism in a category requires quantification over all objects: a morphism $f : A to B$ is epi when for all all $C$ (unbounded quantifier!) and $g, h : B to C$, if $g circ f = h circ f$ then $g = h$. Often in concrete example we can characterize epis equivalently with some statement that only contains bounded quantifiers (e.g., in the category of sets a map is epi if, and only if it is surjective), but if we make general statements about epis in large categories, large quantification will be required.