In mathematics we casually use expresions with variable number of quantifiers, like $$\forall a \in A\ \exists n \in \mathbb{N}\ \exists b_1,\ldots,b_n \in B\ \ \ a = b_1 + \cdots + b_n.$$ I'm wondering what is the formal status of such expressions. Is this just a convenient notation for second-order formulas? Because I guess $\exists n \in \mathbb{N}\ \exists b_1,\ldots,b_n \in B$ could be switched to $\exists S \subseteq B, |S|<\infty$.
I'd like to know what is the logical basis for these expressions.
If you see $b_1, \dots, b_n$ as a function from an index set $\{1, 2, \dots, n\}$ to $B$, then it's an abbreviation for $$\forall a \in A \;\exists n \in {\mathbb N} \;\exists b \colon \{1, 2, \dots, n\} \to B \;\; [a = \textstyle\sum_{i=1}^n b(i)].$$ (And this is not equivalent to $$\forall a \in A \; \exists S \subseteq B \;\;[ |S| < \infty \land a = \textstyle\sum S],$$ because in the first formulation the $b_i$ can be repeated).