The answer is yesser than I thought. I mentioned this issue at http://eventos.cmm.uchile.cl/edynamicsxiii/, since the proximality lemma from my previous answer was discussed there. Someone pointed out that Hindman's original proof of his famous theorem is at least somewhat elementary in some technical sense, and implies a significant part of the proximality theorem, so the answer must be "yes" at least in some technical sense.

After a bit of searching I found the relevant paper [1]: in the sense of reverse mathematics, your theorem is provable in $\mathrm{ACA}_0^+$, a certain fragment of second-order arithmetic.

I quote the relevant theorem in the form stated in this paper. They call this the Auslander-Ellis theorem.

Theorem. Let $X$ be a compact metric space and let $T : X \to X$ be continuous. Regard $(X,T)$ as dynamical system. Given $x \in X$, there exists $y \in X$ such that $y$ is uniformly recurrent and proximal to $x$.

They show that this theorem is provable in $\mathrm{ACA}_0^+$. Let me recall how to conclude your result (this deduction seems very elementary, so I guess it needs much less than $\mathrm{ACA}_0^+$).

Corollary. Every distal system is invertible.

Proof. Injectivity is clear. Take $x \in X$, and apply the previous theorem, to get that $x$ is proximal to some uniformly recurrent $y$. Then $x = y$, so every point in $X$ is uniformly recurrent. Clearly this implies surjectivity, since if $U$ is a neighborhood of any $x \in X$, we have $T^n(x) \in U$ for some positive $n$, and then $T^{n-1}(x)$ maps to $U$ in $T$, so $TX$ is dense in $X$ and by compactness is equal to $X$. Square.

I am not an expert, but as far as I understand, second-order arithmetic in itself is weaker than Zermelo-Frankel set theory (without choice), and $\mathrm{ACA}_0^+$ is about medium strength as far as the most commonly studied fragments of second-order arithmetic go. Roughly, the logic $\mathrm{ACA}_0$ says that a set of natural numbers exists if you can define it by an arithmetical formula, and $\mathrm{ACA}_0^+$ adds the $\omega$th Turing jump of each set already definable.

Nevertheless, to quote [1], "It is well known that all existing proofs of HT are nonconstructive. One of the goals of this paper is to delimit the degree of nonconstructivity which is inherent in Hindman's Theorem."

To summarize the logical connections obtained: Write AET for the theorem about proximality, HT for Hindman's theorem, DT for OP's theorem about distal systems. We have
$$\mathrm{ACA_0^+} \implies \mathrm{AET} \implies \mathrm{HT} \implies \mathrm{ACA_0} \wedge \mathrm{DT}$$
Intuitively (and again I am not an expert), if you believe results of a certain flavor of infinite computation are well-defined, you can prove AET and therefore the theorem about distal systems. But in theory, the problem about distal systems could be much easier (I have a hard time imagining a proof not going through proximal pairs, but I've been wrong before). In the reverse math framework, one could ask if it is in $\mathrm{ACA}_0$, or $\mathrm{WKL}_0$, or $\mathrm{RCA}_0$, in decreasing order of strength.

Reference

[1]: *Blass, Andreas R.; Hirst, Jeffry L.; Simpson, Stephen G.*, Logical analysis of some theorems of combinatorics and topological dynamics, Logic and combinatorics, Proc. AMS-IMS-SIAM Conf., Arcata/Calif. 1985, Contemp. Math. 65, 125-156 (1987). ZBL0652.03040.

6more comments