What is the formal definition of repeated limit using quantifiers? The basic question is what has been asked in the title. I looked for the definition here, here and here but no definition uses quantifiers. 
I tried to formulate the definition but succeeded only partially. For this I considered the following special case,

Let $f:D(\subseteq\mathbb{R}^2)\to\mathbb{R}$ and $(a,b)\in D$. Then we say $\displaystyle\lim_{x\to a}f(x,y)=L(y)$ if $$(\forall y)(\exists L_y\in\mathbb{R})\left[(\forall \varepsilon>0)(\exists \delta>0)\right[|x-a|<\delta\rightarrow |f(x,y)-L_y|<\varepsilon]]$$

 A: The definition for infinite limit is (almost) the following:
$$\exists b\forall \epsilon\exists k_0 \forall n:(n>k_0 \rightarrow|c_{n}-b|<\epsilon) \land \forall n \exists k_2 :(n>k_2) \rightarrow(\exists c_n  \forall \epsilon \exists k_1 \forall m: (m>k_1 \rightarrow|a_{n,m}-c_n|<\epsilon))$$
Here $b$ defines the outer limit and $c_n$ the inner limit which is required to exist after some point $k_2$. If the above is false, then the limit does not exist. We still need to define the domains, which should be obvious. The finite limit is defined replacing the conditions and switching to real or rational functions.
However, this may not be the best way to think about repeated limit as it requires proving what $c_n$ (the first limit) is independently. We can prove that the definition is equivalent to the intuitive definition of what a repeated limit should mean.
$$\exists b \forall \epsilon \exists k_0 \forall n \exists k_1(\epsilon,n)\forall m   : (n>k_0 \land m>k_1) \rightarrow|a_{n,m}-b|<\epsilon$$
Proof:
$\Rightarrow$
Suppose the first definition holds. Let now $\epsilon \in \mathbb R_+$ and $n,m \in \mathbb N$. Now by triangle inequality there are $k_0 (\epsilon),k_1 (n,\epsilon)\in \mathbb N$ such that
$$|a_{n,m}-b|=|a_{n,m}-c_n+c_n-b|\leq|a_{n,m}-c_n|+|c_n-b|<\frac{\epsilon}{2}+\frac{\epsilon}{2}=\epsilon,$$
when $k_0<n,k_1<m$. This is since, by the first condition we have a $k_0$ such that $|c_n-b|<\frac{\epsilon}{2}, k_0<n$, and by the second condition there is a $k_1(\epsilon,n)$ such that $|a_{n,m}-c_n|<\frac{\epsilon}{2}$, when $k_1<m$. This concludes the proof, we only switch the quantifier order to reflect the dependencies.
$\Leftarrow$
We have two statements to prove.
Proof of the second statement:
We can argue by contradiction, select $\epsilon=1$ and we get a contradiction as $c_n=b$ should satisfy the condition. Constructively, the condition should possibly be added to the second definition.
Proof of the first statement: Let $\epsilon \in \mathbb R_+$, we again use the triangle inequality. By the second statement and the assumption there is a $k_0,k_1$, such that
$$|c_n-b|=|a_{n,m}-c_n|+|a_{n,m}-b|< \frac{\epsilon}{2}+\frac{\epsilon}{2}=\epsilon,$$
when $k_0<n,k_1<m$. Hence the statement is proved.
