# 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

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$.
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.