In a course on real analysis one usually comes across the definition of the limit of a function:
Given a function $f:A\to \mathbb{R}$ where $A\subseteq\mathbb{R}$, then if $c\in A$ is an limit point of $A$, we say that
\begin{align} \lim_{x\to c}f(x) = L \end{align}
If
\begin{align} \forall_{\varepsilon>0}\exists_{\delta>0} 0<|x-c|<\delta \implies |f(x)-L|<\varepsilon \end{align}
When one uses this definition of a limit in a proof, it tends to get a bit messy, sometimes you have to do this "trick" where you restrict $\delta$ to always be less than a certain constant, to get some constant lower bounds in either of the inequalities. It also happens frequently that one starts with a $\delta$ and investigates what happens to $|f(x)-L|$, and then from that guess what a suitable relationship between $\varepsilon$ and $\delta$ should be. This approach seems to be a bit convoluted at times, so I propose an alternative definition which I believe is more rational
Given $f:A\to\mathbb{R}$ with $c\in A$ as before, then if there is a surjective function
\begin{align} g:(0,a)\to(0,b) \end{align}
That satisfies
\begin{align} 0<|x-c|<\delta \implies |f(x)-L|<g(\delta) \end{align}
Then \begin{align} \lim_{x\to c}=L \end{align}
This seems superficially more complicated, because now suddenly we have to check the surjectivity of a function, but what is interesting is that both quantifiers and a whole variable ($\varepsilon$) is now imbedded into a single statement about a function. The motivation behind the definition is that if one can find such a $g$, then given any $\varepsilon>0$, one can find $0<\varepsilon'<\varepsilon$ where $\varepsilon'\in(0,b)$, and since it is in the image of $g$ there is some $\delta$ such that $g(\delta)=\varepsilon'$ and from there you can prove that the limit holds in the traditional sense. Note that one can also prove surjectivity by proving that a function is bijective, and you can prove the latter by constructing the inverse, thereby entirely avoiding the use of quantifiers.
My questions then are: Does this alternative definition seem correct, and useful? Is there something analogous to this that is already used?
You asked: "Is there something analogous to this that is already used?"
There is indeed a way of defining limits with fewer quantifier alternations, as you suggested. This way can be viewed as a formalisation of the approach with functions that you sketched. Namely, one has $\lim_{x\to c} f(x) =L$ if and only if for all $x$ infinitely close to $c$ but different from $c$, one has $f(x)\approx L$ where $\approx$ is the relation of infinite proximity. Here $a\approx b$ iff $a-b$ is infinitesimal, and a number is infinitesimal if it is smaller in absolute value than every positive standard real number. A recent breakthrough showed that such a framework can be achieved conservatively over ZF (without the axiom of choice and without ultrafilters). See here for further details.