Is it possible to use order relation in Presburger arithmetic?

Question

The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely.

Is it possible to state and prove theorems in Presburger arithmetic that contain order relations (less than, <)?

$x + 1 = y → x < y$

Answer 1

In general, well-ordering is not definable in first-order arithmetic language. Nevertheless, such formulas as the mentioned $x<y\leftrightarrow\exists z(z+z\not=z\wedge x+z=y)$ or $\exists z(x + z = y - 1)$ express the notion (viz., implicitly, without an explicit order relation) by dint of the intended domain of quantification, which is $\mathbb{N}$ or $\mathbb{Z}$.

As a note for follow-up, I quote (with several additions and notational modifications) a relevant paragraph from Craig Smoryński's Logical Number Theory I: An Introduction (Springer, 1991, p. 308):

Presburger published his result the following year in the proceedings of a conference held in Warsaw [The First Congress of Mathematicians of the Slavic Countries, September 23–27, 1929]. In the published text, he only provided the details for the quantifier elimination for the structure $\langle\mathbb{Z}, +, 0, 1\rangle$, i.e., the addition of the integers. In an addendum, however, he announced that the proof could be extended to the case in which the order relation was added [as a primitive notion]. Since the non-negative integers are definable in $\langle\mathbb{Z}, <, +, 0, 1\rangle$, his decision procedure covered both structures, $\langle\mathbb{Z}, <, +, 0, > 1\rangle$ and $\langle\omega, <, +, 0, 1\rangle$. The full details were first published by Paul Bernays in Grundlagen der Mathematik I in 1934.