Stratifying statements provable in classical first-order logic by the count of usages of LEM Statements provable in intuitionistic logic can be considered to be proved in classical logic without any usages of law of excluded middle. I'm curious about whether it's interesting to stratify statements provable in classical logic further by amount of LEM instantiations used in a formal proof.
As in, let's define $A_n$ to be the set of statements of classical first-order logic provable using no more than $n$ instances of LEM. (e.g. in this notation $A_0$ consists of statements provable in intuitionistic logic)
Obviously, $A_n \subseteq A_{n+1}$, but is it the case that the hierarchy collapses at some point, as in, for some $n$, $A_n = A_{n+1}$?
 A: tl;dr The hierarchy collapses at $n=1$, even in the first-order case. The argument showing this is in Part II of my answer.

I. The crucial observation is the well-known fact intuitionistic logic proves the implication $\neg (P \vee \neg P) \rightarrow (P \vee \neg P)$ for any formula $P$. Let me show this quickly.
Assume that $\neg (P \vee \neg P)$. I claim that under this assumption, $\neg P$ holds.
Assume for a contradiction that $P$ holds. Then by disjunction introduction $P \vee \neg P$ also holds, contradicting $\neg (P \vee \neg P)$. Our assumption of $P$ must be at fault, so by negation introduction we conclude $\neg P$.
But now we know that $\neg P$ holds, so by disjunction introduction $P \vee \neg P$ holds too.

II. I now show that your hierarchy collapses at $n=1$, i.e. every classical tautology has a proof that invokes the law of excluded middle at most once.
Assume for a contradiction that there is some first-order formula $\varphi$ such that every proof of $\varphi$ has to invoke LEM at least $n$ times for some $n > 1$.
Consider a proof of $\varphi$ that uses exactly $n$ instances of LEM, $A_1 \vee \neg A_1,  A_2 \vee \neg A_2, \dots  A_n \vee \neg A_n$.
Set $B := (A_1 \vee \neg A_1) \wedge (A_2 \vee \neg A_2)$. We will show in Part III that $B \vee \neg B$ implies both $A_1 \vee \neg A_1$ and $A_2 \vee \neg A_2$ using an argument in intuitionistic logic.
Consequently, we can find a proof of $\varphi$ which uses $n-1$ instances of LEM, $B \vee \neg B, A_3 \vee \neg A_3, \dots A_n \vee \neg A_n$. This is a contradiction.
Therefore, every classical tautology has a proof that invokes the law of excluded middle at most once.

III. How can we conclude $A_1 \vee \neg A_1$ and $A_2 \vee \neg A_2$ from the assumption $B \vee \neg B$? Well, our assumption is a disjunction, so we can use disjunction elimination. We have to consider two cases :
If the first disjunct, $B$ holds, then we have $(A_1 \vee \neg A_1) \wedge (A_2 \vee \neg A_2)$, so $A_1 \vee neg A_1$ follows by conjunction elimination, and similarly for $A_2 \vee \neg A_2$.
So from here on out, we can assume that the second disjunct of our assumption, $\neg B$ holds.
By currying, $\neg B$ is the same as $(A_1 \vee \neg A_1) \rightarrow (A_2 \vee \neg A_2) \rightarrow \bot$, in other words we have $(A_1 \vee \neg A_1) \rightarrow \neg (A_2 \vee \neg A_2)$.
But by the transitivity of implication and the result of Part I, this means that $(A_1 \vee \neg A_1) \rightarrow (A_2 \vee \neg A_2)$ and $(A_1 \vee \neg A_1) \rightarrow \neg (A_2 \vee \neg A_2)$ both hold. In other words $A_1 \vee \neg A_1$ implies a contradiction, so $\neg (A_1 \vee \neg A_1)$ holds. Repeating the argument of Part I, we conclude that $A_1 \vee \neg A_1$ follows as well.
Using the fact that conjuction is commutative, an identical argument gives $A_2 \vee \neg A_2$.
We considered two cases (the case of $B$ and of $\neg B$). In both cases, $A_1 \vee \neg A_1$ and $A_2 \vee \neg A_2$ held, so by disjuction elimination we have shown that $B \vee \neg B$ implies both $A_1 \vee \neg A_1$ and  $A_2 \vee \neg A_2$. This argument was purely intuitonistic: it used only the inference rules of intuitionistic Natural Deduction, and never relied on excluded middle, double-negation elimination, or any other principle that is invalid intuitionistically.

edit: As Mark Saving noted, I elide a fair bit of "quantifier maintenance" in Part III, in the sense that the instances of LEM are actually not just formulas $A \vee \neg A$, but universal closures of such formulas. However, this is not an issue in practice: if we have $\forall \overline{x}. A_1(\overline{x}) \vee \neg A_1(\overline{x})$ and $\forall \overline{y}. A_2(\overline{y}) \vee \neg A_2(\overline{y})$, then the argument of Part III gives us that if we set $B(\overline{x},\overline{y}) := (A_1(\overline{x}) \vee \neg A_1(\overline{x})) \wedge (A_2(\overline{y}) \vee \neg A_2(\overline{y}))$, then the implication $(\forall \overline{x}. \forall \overline{y}. B(\overline{x},\overline{y}) \vee \neg B(\overline{x},\overline{y})) \rightarrow \forall \overline{x}. \forall \overline{y}. A_2(\overline{y}) \vee \neg A_2(\overline{y})$ holds.
From that, using the universal elimination rule a couple of times allows us to conclude $\forall \overline{y}. A_2(\overline{y}) \vee \neg A_2(\overline{y})$ as desired -- simply substitute a fresh variable $t$ for each $x$ in $\overline{x}$. This is allowed in all formalizations of first-order intuitionistic logic (e.g. natural deduction NJ, sequent calculus LJ or the Hilbert system IPC). So one instance of LEM is sufficient.
But the same trick wouldn't work so simply in e.g. free logic, where we wouldn't be able to conclude $\forall \overline{y}. A_2(\overline{y}) \vee \neg A_2(\overline{y})$ from $\forall \overline{x}. \forall \overline{y}. A_2(\overline{y}) \vee \neg A_2(\overline{y})$. For free logic one would need to rule out the occurrence of such LEM instances in a minimal proof. This is likely to be a fairly hard exercise.
A similar issue technically affects logic-like systems where the quantifiers are bounded, such as type theories, although in such systems a single higher-order instance of LEM suffices to prove any classical first-order tautologies anyway.
