@LSpice: please do. Thanks.

Where does it cut off mid-sentence?

Thanks. Will correct.

@FrancoisDorais: would "$\Sigma_{1}$-Separation implies the Union Principle" hold if the Union Principle was restricted to finite unions of finite sets?

@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.

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....

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.

Then is the 'Union Principle' exposited in the mathoverflow question I mentioned actually provable in $I$$\Sigma_n$ when restricted to finite sets?

What is the bigger research problem you are considering?

Thanks. Just checking....