0

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}$?]

Thomas Benjamin
  • 6,024
  • 2
    If memory serves, the usual proof of Szemeredi actually goes through in $\mathsf{RCA_0}$ alone (and Friedman conjectures that Szemeredi is equivalent to EFA over bounded arithmetic). Certainly since Szemeredi is about finite graphs, it has nothing to do with $\mathsf{ACA_0}$; it's already going to be provable in $\mathsf{I\Sigma_n}$ for some fixed $n$ (and I suspect $n=1$ is already enough). – Noah Schweber Jun 06 '22 at 06:09
  • Then is the 'Union Principle' exposited in the mathoverflow question I mentioned actually provable in $I$$\Sigma_n$ when restricted to finite sets? – Thomas Benjamin Jun 06 '22 at 06:28
  • Also, I didn't see that Prof. Friedman explicitly mentioned the Regularity Lemma in the FoM post you provided the link to though I am definitely aware of both of his Grand Conjectures. – Thomas Benjamin Jun 06 '22 at 06:34
  • If you could provide the proof that the Regularity Lemma is provable in $RCA_0$ or $I$$\Sigma_n$ in an answer I would, of course, accept it.... – Thomas Benjamin Jun 06 '22 at 06:39
  • @NoahSchweber: have you any reference that shows that "the usual proof of Szemeredi actually goes through in $RCA_{0}$ alone"? that would be very helpful to me to study. Thanks in advance for your help in this matter. It would be much appreciated. – Thomas Benjamin Jun 20 '22 at 23:34
  • 1
    Thanks. Will correct. – Thomas Benjamin Jul 03 '22 at 22:42
  • Where does it cut off mid-sentence? – Thomas Benjamin Jul 03 '22 at 22:55
  • 1
    @LSpice: please do. Thanks. – Thomas Benjamin Jul 03 '22 at 22:58
  • 1
    Done. – LSpice Jul 03 '22 at 23:04
  • 1
    @LSpice: Again, thanks. – Thomas Benjamin Jul 03 '22 at 23:28
  • @ThomasBenjamin I don't know a reference, I just skimmed a proof and didn't see a step that didn't go through in $\mathsf{RCA_0}$ alone. If I get a chance this coming weekend, I'll write a quick summary of a proof of Szemeredi and why each bit goes through in $\mathsf{RCA_0}$. – Noah Schweber Jul 05 '22 at 20:13
  • 3
    Szemerédi's lemma is a purely first-order arithmetical statement, and as such it cannot imply ACA_0 over RCA_0. Moreover, if it is provable in ACA_0, then it is provable in PA by arithmetical conservativity, and therefore (as Noah already mentioned) in $I\Sigma_n$ for some $n$. – Emil Jeřábek Jul 05 '22 at 20:28
  • @NoahSchweber: Thanks, I appreciate it. – Thomas Benjamin Jul 05 '22 at 21:47
  • @EmilJeřábek: for a Hamiltonian graph, would the property that makes that graph Hamiltonian also be able to be expressed as a first-order arithmetical statement? – Thomas Benjamin Jul 06 '22 at 02:10
  • For a finite graph, yes. In second-order arithmetic, all finite (i.e., bounded) sets can be represented by numbers. – Emil Jeřábek Jul 06 '22 at 06:28
  • @EmilJeřábek: Thanks. Very helpful. – Thomas Benjamin Jul 06 '22 at 09:10
  • @EmilJeřábek: Can you then characterize all finite hamiltonian graphs by this numbering? – Thomas Benjamin Jul 06 '22 at 09:20
  • I have no idea what you mean by "characterize" and "numbering", and what all this has to do with Szemerédi's lemma. – Emil Jeřábek Jul 06 '22 at 14:13
  • @EmilJeřábek: How ( for example) would you represent the simplest hamiltonian graph (a triangle--three vertices and three edges) by numbers? – Thomas Benjamin Jul 06 '22 at 21:16
  • In reverse mathematics? – Thomas Benjamin Jul 06 '22 at 21:22
  • @NoahSchweber Are you saying Szemeredi is provable in EFA? But according to Richard Borcherds, the tower type lower bound for the regularity lemma means it cannot be proven in EFA – Lxm Feb 19 '23 at 04:26
  • @Lxm I think I very clearly referred to $\mathsf{RCA_0}$, not $\mathsf{EFA}$ (which is much weaker); I only mentioned EFA at all in the context of a claim by Friedman. – Noah Schweber Feb 19 '23 at 04:40
  • @NoahSchweber I was talking about your first comment, which mentioned the conjecture by Friedman, which I understood to be false – Lxm Feb 19 '23 at 04:49
  • @Lxm Ah. Yes, that conjecture looks incorrect based on the bounds gotten. Certainly all I'll actively claim is that $\mathsf{RCA_0}$ suffices for the usual proof to go through. – Noah Schweber Feb 19 '23 at 05:49

0 Answers0