Consider the monadic second order logic over the natural numbers with $<$ as a predicate, i.e. the second order logic over $(\mathbb N, 1, <)$, where we can quantify over sets and individual variables, denote it by $MSO[<]$.
Also consider the first order theory over the natural numbers with addition, i.e. $(\mathbb N, 1, +)$ where we can just quantify over individual elements (the so called Presburger arithmetic), call it $FO[+]$.
Of course in $FO[+]$ we can express $<$ by a formula, i.e. $x < y$ is equivalent to $$ \exists z ( x + z = y ). $$
But what is the relation of $MSO[<]$ to $FO[+]$? Both logics are decidable, but are their
- any formulaes in $FO[+]$ that could not be expressed in $MSO[<]$, and
- similar any formulas in $MSO[<]$ that could not be expressed in $FO[+]$?
I guess even such a simple formula as $\varphi(x,y,z) = (x + y = z)$ could not be described in monadic second order $MSO[<]$, but how to prove that? Also for some $MSO[<]$ formulas, like \begin{align*} \varphi(x_1) & = \exists X ( 1 \in X \land \forall u,v ( \neg \exists z ( u < z \land z < v ) \to ( u \in X \leftrightarrow v \notin X ) \land x_1 \in X ) \end{align*} we have the equivalent $FO[+]$ formula $$ \psi(x_1) = \exists x ( x + x + 1 = x_1 ) \lor x_1 = 1. $$
Addition is automatic. If $x$, $y$ and $z$ are three words of numerals of the same length over base $[b] = \{0,1,\dots,b-1\}$, then the predicate $x+y=z$, seen as a language of words over the triple alphabet $[b]^3$, is recognized by a finite automaton. Hence it is definable in $MSO[<]$ using this particular kind of interpretation, and so is all of Presburger arithmetic $FO[+]$. A 1994 paper by Bruy`ere, Hansel, Michaux and Villemaire studies this question fairly comprehensively.