<p>[This question has been asked on MathOverflow with no luck a month ago.]</p>
<p>Let me first clarify my definitions.  For a word <span class="math-container">$w \in \Sigma^*$</span>, with <span class="math-container">$\Sigma =\{a_1,
\ldots, a_n\}$</span>, I define two structures:</p>
<p><span class="math-container">$\mathbb{N}(w) = \langle \mathbb{N}, &lt;, Q_{a_1}, \ldots, Q_{a_n} \rangle$</span>,</p>
<p>and the more usual <i>word model</i>:</p>
<p><span class="math-container">$\mathbb{N}^r(w) = \langle \{0, \ldots, |w|-1\}, &lt;, Q_{a_1}, \ldots, Q_{a_n} \rangle$</span>,</p>
<p>where <span class="math-container">$Q_{a_i} = \{p \mid w_p = a_i\}$</span>.</p>
<p>Then WS1S is the set of second order formulas with models of the form
<span class="math-container">$\mathbb{N}(w)$</span>, with order, and for which second order quantification is
limited to finite subsets of the domain.  MSO is the set of monadic second order
formulas with models of the form <span class="math-container">$\mathbb{N}^r(w)$</span>, with order.</p>
<p>The usual proof that REG = WS1S proves at the same time that MSO = WS1S.  My
question is then, for which first or second order relations can we keep this
to be true?</p>
<p>For instance, if we add a unary predicate <span class="math-container">$E(X)$</span> which says that a
(monadic) second order variable contains an even number of objects, we add no
power, as <span class="math-container">$E(X)$</span> is expressible as &quot;there exists <span class="math-container">$X_1$</span> and
<span class="math-container">$X_2$</span> that partition <span class="math-container">$X$</span>, in such a way that if an element is in
<span class="math-container">$X_i$</span> the next one in <span class="math-container">$X$</span> is in <span class="math-container">$X_j$</span>, <span class="math-container">$i \neq j$</span>, and
the first element of <span class="math-container">$X$</span> is in <span class="math-container">$X_1$</span> and the last is in
<span class="math-container">$X_2$</span>.&quot;</p>
<p>Now, if we add a predicate <span class="math-container">$|X| &lt; |Y|$</span>, then WS1S becomes undecidable
(see Klaedtke &amp; Ruess, 10.1.1.7.3029), while MSO stays trivially decidable.</p>
<p>Thank you.</p>
<hr />
<p><b>Edit:</b> As a side question, ... is this question of interest?  I mean, I'm no expert in the field, so I'm not sure this question is relevant.</p>

CC BY-SA 3.0
2012-05-12T18:10:56.043Z
Your model $\mathbb{N}(w)$ is very unusual : what is the need of considering a finite word on an infinite underlying structure ? If you forget the letter predicates (which do not change the problem a lot), you are in fact comparing MSO on finite linear orders, and WS1S on the order $\omega$. This is strange, because it is more intuitive to compare different logic formalisms on the same structure.
Denis
CC BY-SA 2.5
2010-08-16T20:57:11.507Z
We *do* need Latex math support...
Jukka Suomela
CC BY-SA 2.5
2010-08-16T21:18:39.573Z
Ain't we just a click away from it?
Michaël Cadilhac
CC BY-SA 2.5
2010-08-17T07:36:47.030Z
also see the greasemonkey hack mentioned here: http://meta.cstheory.stackexchange.com/questions/3/latex-math-support
Suresh Venkat
CC BY-SA 2.5
2010-08-18T17:55:48.180Z
Was there no joy on MO because they couldn't figure it out, or because they found your question uninteresting? (I'm guessing the latter)
Robert Harvey
CC BY-SA 2.5
2010-08-18T18:14:11.137Z
What are your reasons to think this question is uninteresting?  From a practical point of view, it is useful to know when you can restrict yourself to finite models, isn't it?
For the record, I received no comment on MO.
Michaël Cadilhac
<lo.logic><automata-theory><descriptive-complexity>
To what extent MSO = WS1S, when adding relations?
Michaël Cadilhac
# To what extent MSO = WS1S, when adding relations?

(Asked by: username_0 on 2010-08-16)

[This question has been asked on MathOverflow with no luck a month ago.]

Let me first clarify my definitions. For a word $w \in \Sigma^\*$, with $\Sigma =\{a\_1,
\ldots, a\_n\}$, I define two structures:

$\mathbb{N}(w) = \langle \mathbb{N}, <, Q\_{a\_1}, \ldots, Q\_{a\_n} \rangle$,

and the more usual *word model*:

$\mathbb{N}^r(w) = \langle \{0, \ldots, |w|-1\}, <, Q\_{a\_1}, \ldots, Q\_{a\_n} \rangle$,

where $Q\_{a\_i} = \{p \mid w\_p = a\_i\}$.

Then WS1S is the set of second order formulas with models of the form
$\mathbb{N}(w)$, with order, and for which second order quantification is
limited to finite subsets of the domain. MSO is the set of monadic second order
formulas with models of the form $\mathbb{N}^r(w)$, with order.

The usual proof that REG = WS1S proves at the same time that MSO = WS1S. My
question is then, for which first or second order relations can we keep this
to be true?

For instance, if we add a unary predicate $E(X)$ which says that a
(monadic) second order variable contains an even number of objects, we add no
power, as $E(X)$ is expressible as "there exists $X\_1$ and
$X\_2$ that partition $X$, in such a way that if an element is in
$X\_i$ the next one in $X$ is in $X\_j$, $i \neq j$, and
the first element of $X$ is in $X\_1$ and the last is in
$X\_2$."

Now, if we add a predicate $|X| < |Y|$, then WS1S becomes undecidable
(see Klaedtke & Ruess, 10.1.1.7.3029), while MSO stays trivially decidable.

Thank you.

---

**Edit:** As a side question, ... is this question of interest? I mean, I'm no expert in the field, so I'm not sure this question is relevant.

**Tags:** lo.logic, automata-theory, descriptive-complexity
> **Comments:**
> **username_2**: We *do* need Latex math support...  
> **username_0**: Ain't we just a click away from it?  
> **username_3**: also see the greasemonkey hack mentioned here: http://meta.cstheory.stackexchange.com/questions/3/latex-math-support  
> **username_4**: Was there no joy on MO because they couldn't figure it out, or because they found your question uninteresting? (I'm guessing the latter)  
> **username_0**: What are your reasons to think this question is uninteresting?  From a practical point of view, it is useful to know when you can restrict yourself to finite models, isn't it? For the record, I received no comment on MO.  
> **username_1**: Your model $\mathbb{N}(w)$ is very unusual : what is the need of considering a finite word on an infinite underlying structure ? If you forget the letter predicates (which do not change the problem a lot), you are in fact comparing MSO on finite linear orders, and WS1S on the order $\omega$. This is strange, because it is more intuitive to compare different logic formalisms on the same structure.  

---

## 0 answers

