Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
It does not imply that Collatz is in $\Sigma_1$: as Noah says above, there is only a $\Sigma_1$ sentence implying Collatz, not one that is equivalent to it.
As far as we know, it is merely sufficient. This method is basically searching for proofs of a certain size that fit a template, and if the search does not succeed after some time we modify the constraints to allow larger proofs and keep searching. There exist rewriting systems that are terminating but do not admit a direct matrix interpretation proof. For a given rewriting system, I imagine it might be possible to prove that if it is terminating then there is a matrix interpretation proof of this fact. We know of no such result for the system at hand.
I was misquoted in the article—I actually said "If you can find them, this implies that the rewriting system is terminating." This is due to a method called "matrix interpretations" [1], widely used in proving termination of rewriting systems. Finding the matrices does settle the conjecture as true. We will put a preliminary writeup on arXiv soon. [1]: Endrullis, J., Waldmann, J. & Zantema, H. Matrix Interpretations for Proving Termination of Term Rewriting. J Autom Reasoning 40, 195–220 (2008). doi.org/10.1007/s10817-007-9087-9
