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?

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

3. 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).

4. $$\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].

• Please, give at least one (good) reference where we can get an idea of what Pressburger Arithmeticis about... – Jean Marie May 8 at 20:36
• @Jean Marie, I've just added a link to the article in Wikipedia about Presburger arithmetic. See above again. – Eli May 8 at 20:47
• "Interesting" is vague, but I'd expect the answer to your question to be negative. The reason is that Presburger arithmetic admits quantifier elimination on the basis of axioms that are essentially just like the facts you already quoted in the question. – Andreas Blass May 8 at 22:25
• @Andreas Blass, I know it's vague, and that's why I wrote "interesting" with quotation marks. That said, in my view, an "interesting" additive theorem must have an intuitive meaning (as in the example I have added to my question), and its proof must lean on induction. – Eli May 8 at 22:41
• Is it interesting that $\forall x.\exists y. x + Sx+ SSx = y+y+y$? (The sum of any three consecutive numbers is a multiple of 3.) How about $\forall x. \forall y. \exists z. x + (x + y) + (x + y + y) = z + z + z$? (The sum of any three consecutive terms of an arithmetic progression is a multiple of 3.) – MJD May 11 at 19:28

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)]$$

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.

• Thanks to your well known theorem, I have just added a third condition to my definition - of "interesting" theorems - that was given in the last section of my first post. – Eli May 12 at 4:06
• @Eli In Presburger and Peano arithmetic, associativity of addition is not an axiom but a theorem, so I'm not sure what you mean by that condition. – user76284 May 12 at 21:21
• Thanks to your new comment, I've just re-edited the last sentence in my post. – Eli May 12 at 21:46

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.

• Can't I tag two answers (i.e. yours and bof's) as "accepted"? – Eli May 12 at 4:20
• @Eli: No, only one answer can be accepted. But you can upvote as many answers as you want -- with the upwards-pointing triangle above each answer's vote count. – Henning Makholm May 12 at 11:12
• All right, I've just upvoted your answer! – Eli May 12 at 12:24