# Is this first order version of the Collatz conjecture decidable in peano arithmetic?

Let $\phi(x)$ be a first order formula in the language of arithmetic with one free variable $x$. Consider the sentence $\psi_\phi$, defined as:

$$\phi(0)\wedge \phi(1) \wedge (\forall x \phi(x) \to \phi(2x)) \wedge (\forall x \quad 2\not |x \to (\phi(3x+1) \to \phi(x))) \to \forall x \phi(x)$$

A positive answer to the Collatz conjecture would imply that the above sentence is valid for all $\phi$.

However, I'm wondering whether this statement can be violated in nonstandard models of arithmetic.

If such a nonstandard model of arithmetic, I would like to see a proof that there is a $\phi$ with $\text{Con}(\text{PA}\cup\psi_\phi)$.

If you think that this first order version of the Collatz conjecture should still hold, I can't expect you to give me a prove for that, since this would probably be as hard as proving the Collatz conjecture. However, I would like to hear some reasons why, when one believes in the Collatz conjecture in $\Bbb N$, one should be able to prove the validity of all the $\psi_\phi$ only with methods from PA.

-
You do realize the actual Collatz conjecture is already expressible as a single first-order statement in the language of arithmetic, right? –  Chris Eagle Jun 23 '13 at 17:31
@ChrisEagle: How exactly? –  Dominik Jun 23 '13 at 17:32
If we let $f(m,n)$ denote the result of applying the Collatz iteration $m$ times starting at $n$, then $f$ is computable and hence expressible by a first-order arithmetic formula. The conjecture is then just $\forall n \exists m f(m,n)=1$. –  Chris Eagle Jun 23 '13 at 17:35