18
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ We do need Latex math support... $\endgroup$ – Jukka Suomela Aug 16 '10 at 20:57
  • $\begingroup$ Ain't we just a click away from it? $\endgroup$ – Michaël Cadilhac Aug 16 '10 at 21:18
  • $\begingroup$ also see the greasemonkey hack mentioned here: meta.cstheory.stackexchange.com/questions/3/latex-math-support $\endgroup$ – Suresh Venkat Aug 17 '10 at 7:36
  • $\begingroup$ 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) $\endgroup$ – Robert Harvey Aug 18 '10 at 17:55
  • 1
    $\begingroup$ 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. $\endgroup$ – Denis May 12 '12 at 18:10

Your Answer

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

Browse other questions tagged or ask your own question.