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?

predicative. $\endgroup$ – Pedro Sánchez Terraf Apr 8 at 9:47