Are there "interesting" theorems in Peano arithmetic, that only use the addition operation? More precisely, are there "interesting" theorems of Presburger arithmetic, other than the following four well-known "interesting" ones?


*

*The commutativity of addition. 

*The theorem stating there are no two consecutive even numbers. 

*The theorem stating that every natural number, either is even or is followed by an even successor (along with analogous theorems about a sum of more than two identical natural numbers, e.g., the theorem stating that every natural number not being any sum of three identical natural numbers - is followed by a successor that either is such a sum or is followed by a successor which is such a sum).

*$\forall(a,c)\exists(b)[(a+b=c)\lor (c+b=a)]$
For our purposes, for an "additive" theorem to be "interesting" enough: 1) it must have an intuitive meaning [like that of the theorems I've mentioned as examples]; 2) its proof should need to rely on induction; 3) It should not be an intuitive generalization of any axiom [e.g. the axiom x+(y+1)=(x+y)+1, which can be viewed as a special case wherein z=1, intuitively generalized - for all z - as the theorem of associativity of addition: x+(y+z)=(x+y)+z].
 A: For fixed relatively prime integers $m$ and $n$, the fact that a number divisible by both of them is divisible by their product is expressible in Presburger arithmetic. The case $m=2$, $n=3$:
$$\forall x[(\exists y)(y+y=x)\land(\exists y)(y+y+y=x)\to(\exists y)(y+y+y+y+y+y=x)]$$
A: The associativity of addition is one candidate. Recall from the definition of addition that
\begin{align}
a+0 &=a & \text{A1} \\
a+S(b) &=S(a+b) & \text{A2}
\end{align}
Theorem: $(a+b)+c = a+(b+c)$
Proof: Let $\phi(c)$ denote the proposition that $(a+b)+c = a+(b+c)$. Proceed by induction on $c$.
Base case: Let $c=0$. Then
\begin{align}
(a+b)+c
&= (a+b)+0 && \text{A1} \\
&= a+b \\
&= a+(b+0) && \text{A1} \\
&= a+(b+c)
\end{align}
Therefore $\phi(0)$.
Inductive step: Suppose $(a+b)+c = a+(b+c)$. Then
\begin{align}
(a+b)+S(c)
&= S((a+b)+c) && \text{A2} \\
&= S(a+(b+c)) && \text{inductive hypothesis} \\
&= a+S(b+c) && \text{A2} \\
&= a+(b+S(c)) && \text{A2}
\end{align}
Therefore $\phi(c) \rightarrow \phi(c+1)$ for all $c \in \mathbb{N}$.
By the axiom schema of induction, $\phi(c)$ for all $c \in \mathbb{N}$. This proves that $(\mathbb{N}, +)$ is a semigroup. Together with the proof that 0 is a left identity (in addition to being a right identity as stated in A1), this proves that $(\mathbb{N}, +)$ is a monoid.
A: Presburger Arithmetic can express $x\equiv y\pmod n$ for fixed $n$, so we can state instances of the Chinese Remainder Theorem for fixed moduli, such as

For all $a$ and $b$ there is an $x$ such that $x\equiv a\pmod{7}$ and $x\equiv b\pmod{8}$.

Since this claim can be expressed and it's true in $\mathbb N$, Presburger Arithmetic, being complete, must be able to prove it.
