If the Collatz Conjecture is unsolvable is it true?

Recently Numberphile uploaded a video on Godel's Incompleteness Theorem, and the Professor in the video made the conclusion that

if you can prove a statement cannot be proven true or false by the axioms and if that statement happened to be false by some counterexample, there would be a contradiction,

and so the statement would be true.

Then if someone could prove the Collatz Conjecture was unsolvable would they have proven that it is true? Or is that overreaching from the conclusion in the video.

Also, has anyone attempted a rigorous proof that the Collatz Conjecture is unsolvable?

• I think that this answer by Tao, explains well what happens in situations like this: mathoverflow.net/questions/27755/… Jun 1 '17 at 16:24
• No. In Peano Arithmetic, or some other powerful enough axiomatic system, there are "false" (precisely what "false" is requires a bit more explanation) statements that are undecidable, that is, there are statements $S$ such that $S$ cannot be proven, and $\neg S$ cannot be proven either. Jun 1 '17 at 16:24

If you proved that Collatz was not disprovable in (say) PA, this would mean that there were no finite cycles not hitting $1$. However, it would leave open the possibility that there was some number $n$ which never hit $1$, and never entered a finite cycle (just "shot off to infinity"); so this wouldn't actually prove the Collatz conjecture.
Incidentally, the statements for which PA-unprovability implies truth are those which are equivalent in PA to a $\Pi^0_1$ sentence; it is not known whether the Collatz conjecture is equivalent over PA to a $\Pi^0_1$ sentence, so currently no way is known for turning a proof of the PA-undisprovability of Collatz into a proof of the Collatz conjecture.