Undecidability and algorithmic verification The following question has been asked few hours ago :
How can any statements be proven undecidable?
I'd like to ask a similar but more precise question.
Could we imagine that the Syracuse conjecture is undecidable w.r.t. ZF ?
Could we imagine that Riemann conjecture is undecidable ?
Or even simpler, let say we are in 1990, could we imagine that Fermat conjecture is undecidable ?
For all these questions, I would say no.
For the latter, here is a (buggy ?) sketch of proof.
Take x, y, z, n, positive integers, $n>2$. You can compute easily $x^n+y^n-z^n$. If you get zero, then you get a proof that Fermat's conjecture is false. So if the Fermat's conjecture were undecidable, then I could not get such a proof, so there would not exists a counter-example, so the Fermat's conjecture would be true, and not undecidable.
Is this reasoning flawed ?
This argument would apply to any statement which can by written in the following form :
$$ \forall n_i\in \mathbb N, \dotsc, \forall n_k\in \mathbb N, F(x_1,\dotsc,x_k) ,$$
where $F$ is an assertion we can check algorithmically.
I think the Riemann conjecture fits this form. But the Syracuse conjecture, does not (a priori) : you can check that a sequence reach 1, but not that this sequence does not reach 1.
 A: It was perfectly possible to imagine in $1990$ that the Fermat Last Theorem was neither provable nor refutable in ZF. That could only happen, as you point out, only if FLT is actually true in the natural numbers.  But truth in the natural numbers and provability in a specific formal theory are not the same thing.  
As a consequence of Matiyasevich's solution of Hilbert's Tenth Problem, one can in fact construct an explicit polynomial  $P(x_1,x_2,\dots, x_n)$ such that the equation $P(x_1,x_2,\dots, x_n)=0$ has no solution in the integers, but such that this fact is not provable in ZF (if ZF is consistent).  Actually, for exponential Diophantine equations (so we allow variable exponents, as in the Fermat equation), the result was known well before Matiyasevich's Theorem, as a consequence of work of Julia Robinson, Martin Davis, and Hilary Putnam. 
As for the Syracuse problem (Collatz Conjecture), Conway showed that there are relatively simple generalizations of the Collatz Conjecture that are (algorithmically) undecidable. As a consequence of the result, there are Collatz-like sentences that are neither provable nor refutable in ZF.  
