In his answer to the following mathoverflow question, "The (un)decidability of Robinson Arithmetic without multiplication", 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?