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$ – Quinn Culver Jun 14 '16 at 18:43
  • $\begingroup$ I mean, isn't such a formula generally expressible in SOL but not FOL? $\endgroup$ – Quinn Culver Jun 14 '16 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 '16 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 '16 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 '16 at 4:39

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.