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.
 A: The standard formulation of the Collatz conjecture is already first-order expressible. This is because we can code finite sequences of natural numbers as natural numbers, in a way simple enough that first-order arithmetic can "see." To write the Collatz conjecture in first-order logic, what we do is first define a "Collatz sequence" as a finite sequence $s$ of natural numbers such that for all $n$ with $n+1\in dom(s)$, if $s(n)$ is even then $2s(n+1)=s(n)$ and if $s(n)$ is odd then $s(n+1)=3s(n)+1$. Then the Collatz conjecture says that for any number $n$, there is a Collatz sequence $s$ and a number $k$ such that $s(0)=n$ and $s(k)=1$. 
Technical note: representing sequences is actually slightly tricky if we don't have a primitive symbol for exponentiation; see e.g. the first few pages of http://homepages.math.uic.edu/~marker/math502-03/meta9.pdf.
Once you see this, it should be clear that in fact your scheme is a consequence of the standard first-order version of the Collatz conjecture, and if the Collatz conjecture is false, then we can build a $\varphi$ such that $\psi_\varphi$ is false in the standard model. So your question is almost certainly as hard as the Collatz conjecture. 
