The question is in the title. Szemerédi's Regularity Lemma is the following (according to the Wikipedia entry):
For every $\epsilon \gt 0$ and positive integer $m$ there exists an integer $M$ such that if $G$ is a graph with at least $M$ vertices, there exists an integer $k$ in the range $m \le k \le M$ and an $\epsilon$-regular partition of the vertex set of $G$ into $k$ sets where a partition of the vertex set $V$ of $G$ into $k$ sets $\mathcal P = \{V_1,\dotsc, V_k\}$ is called an $\epsilon$-regular partition if
$$\sum_{(V_i, V_j)} \lvert V_i\rvert\lvert V_j\rvert \le \lvert V(G)\rvert^2$$ where $(V_i, V_j)$ is not $\epsilon$-regular.
I conjecture that Szemerédi's Regularity Lemma is equivalent to $\mathit{ACA}_0$ over $\mathit{RCA}_0$ on the basis of the information contained in the MathOverflow question, "The Reverse Mathematics of writing a set as a union" (question 71420). This is because the Regularity Lemma is an instance of the Union Principle and the Union Principle is equivalent to $\mathit{ACA}_0$ over $\mathit{RCA}_0$.
Is this point of view correct, or am I missing something?
[Addendum. It should be noted that the Wikipedia entry, "Elementary Function Arithmetic", makes the the claim that that Szemerédi's Regularity Lemma is a "natural example" of an "arithmetical statement" that is "true but unprovable in EFA, $\ge$". Furthermore, the paper, "The Algorithmic Aspects of the Regularity Lemma" (by Alon, Duke, Lefmann, Rodl, and Yuster), claims that "we show how to obtain, for any input graph, a partition with the properties guaranteed by the lemma, efficiently [in polynomial time ($\Delta^{p}_1$)—my comment]" while claimimg that the problem of "deciding if the given partition[s] [of the partition given by the aforementioned algorithm—my comment] is $\epsilon$-regular" is "co-NP-complete"[$\Pi^{p}_1$]. Certainly, neither of the claims take the proof of Szemerédi's Regularity Lemma out of $\mathit{RCA}_{0}$ but are the two subsystems of $\mathit{RCA}_{0}$ mentioned in this addendum the same subsystem? Lastly, in the paper, "Reverse Mathematics and Recursive Graph Theory" [by Gasarch—my comment], it is claimed that the theorems regarding sequences of graphs in the paper are equivalent to $\mathit{ACA}_{0}$ or higher [Theorem 20 claims that the sequence of graphs mentioned in the theorem is equivalent to $\Pi^{1}_{1}$-$\mathit{CA}_{0}$. Isn't Szemerédi's Regularity Lemma a statement about the sequence of all finite graphs and as such possibly equivalent to $ACA_{0}$?]
