Confusion of the decidability of $(N,s)$ In some context the PA has only the successor operator $'s'$, but in logic we always refer the structure of PA is $(\mathbb{N},0,1,s,+,\times)$. I believed the theory of the two sturctures are equivalent because I believed that $ '+'$and $  '\times'$ are definable in $(\mathbb{N},s)$. Then I concluded that the theory of $(\mathbb{N},s)$ is not decidable. 
But now I'm not quite sure about this, in addition, what is the decidability of the theory of $(\mathbb{N},+)$? Thanks for your help.
 A: The theory of the successor function, and the theory of addition, are both decidable. For details about the theory of addition, please see Presburger Arithmetic.
Multiplication is not definable in Presburger arithmetic. 
A: Let me address one way (using some powerful machinery, but well-known) to show that addition is not definable in $(\mathbb{N}, s)$. We will see that $(\mathbb{N}, s)$ and $(\mathbb{N}, +)$ have different decidability behaviour with respect the monadic second order language, this is enough.
As others have pointed out it is known that the first-order theory of  $(\mathbb{N}, s)$ is decidable, and the same is true for  $(\mathbb{N}, +)$. On the other hand, it is also a famous result of Buchi the fact that the monadic second order theory of $(\mathbb{N}, s)$ is also decidable (it is worth noticing here that Rabin generalized this result to the full binary tree). On the other hand, it is not difficult to check that multiplication $\cdot$ is definable in the monadic second order theory of $(\mathbb{N}, +)$; as a hint I suggest to first show that the binary divisibility relation "$a | b$" is definable. Thus, from the undecidability of the first-order theory of  $(\mathbb{N}, +, \cdot)$ it follows that it is also undecidable the monadic second order theory of $(\mathbb{N}, +)$.
A: Here's a straightforward way to show that $+$ is not definable relative to $\text{Th}(\mathbb{N},s)$.


*

*$0$ is definable in $\text{Th}(\mathbb{N},s)$, so $\text{Th}(\mathbb{N},s)$ and $\text{Th}(\mathbb{N},s,0)$ have the same definable sets (i.e. any formula in the language $\{s,0\}$ is equivalent to one in the language $\{s\}$ by replacing any occurrence of $0$ with its definition). In particular, it suffices to show that $+$ is not definable in $\text{Th}(\mathbb{N},s,0)$.

*$\text{Th}(\mathbb{N},s,0)$ has quantifier elimination. Showing this is not too hard.

*Now we want to examine all the formulas in three variables ($x$, $y$, $z$) and check that none of them picks out the graph of $+$ (i.e is the formula $x+y=z$). Well, any formula in three variables is equivalent to a boolean combination of atomic formulas. Since the only relation around is $=$, any atomic formula looks like $s^n(a) = s^m(b)$, where $a$ and $b$ are one of $x$, $y$, $z$, or $0$. So any such formula expresses that some variable has a particular value, or that some pair of variables differ in value by some fixed amount. It only takes a bit of thinking to convince yourself that no boolean combination of these can define $+$.
You said in a comment that you only know two ways of showing that something is not definable: decidability arguments and automorphism arguments. It's true that these are the main tricks, but there's a third, more basic way - actually characterizing all the definable sets. This is exactly what quantifier elimination helps us do.
