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.