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?

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?

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?

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?