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. $$

  • $\begingroup$ What about expressing something like "$X$ is a finte" in $MSO[<]$? $\endgroup$ Jun 14, 2016 at 18:43
  • $\begingroup$ I mean, isn't such a formula generally expressible in SOL but not FOL? $\endgroup$ Jun 14, 2016 at 18:53
  • $\begingroup$ Yes, of course as we have no set variables in FOL, but if we restrict to individual variables, is every formula $\varphi(x_1, \ldots, x_k) \in MSO[<]$ also expressible as an equivalent formula $\psi(x_1, \ldots, x_k) \in FO[+]$ and vice versa with free variables $x_1, \ldots, x_k$? $\endgroup$
    – StefanH
    Jun 14, 2016 at 18:55
  • 2
    $\begingroup$ @QuinnCulver: "$X$ is finite" is easy to express in $MSO[<]$: $\exists n\forall m\cdot (X(m) \Rightarrow m < n)$. But I don't see how that helps with the OP's question (which I read as asking whether there are relative interpretations of $MSO[<]$ in $PA[+]$ and vice versa). $\endgroup$
    – Rob Arthan
    Jun 14, 2016 at 21:09
  • 1
    $\begingroup$ For one direction: Note that multiplication is definable in $MSO[<, +]$ since $ab = c$ iff $(a+b)^2 = a^2 + b^2 + 2c$, $a = b^2$ iff $a+b$ is the lcm of $b, b+1$ and $a$ is a multiple of $b$ iff $a$ belongs to every set that contains $a$ and is closed under addition by $a$. $\endgroup$
    – hot_queen
    Jun 16, 2016 at 4:39

1 Answer 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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .