In his answer to the following mathoverflow question, [The (un)decidability of Robinson Arithmetic without multiplication](https://mathoverflow.net/q/177047/1946), Emil Jerabek proved that the following fragment:


1. $\forall$x(Sx$\neq$0)
2. $\forall$x$\forall$y(Sx=Sy $\Rightarrow$ x=y)
3. $\forall$x(x$\neq$0 $\Rightarrow$ ($\exists$y)(x=Sy)
4. $\forall$x(x+0=x)
5. $\forall$x$\forall$y (x+Sy)=S(x+y)


"with '0' as the sole constant and 'S' [successor] and '+' as the built-in function signs...and whose deductive system is your favourite classical first-order logic with identity." (Quote from Peter Smith, the OP in question.)


is undecidable, and in fact hereditarily undecidable.


Question: What would be an example of a true but undecidable well-formed formula definable in the language of this fragment? 



A question regarding a fragment of Robinson Arithmetic
Just turning what SJR wrote to an answer: the true but undecidable sentence is:


$$ \forall x((\exists y(x=y+y))\lor(\exists y(x=S(y+y)))). $$


