The equivalence between MSO (Monadic Second Order Logic over finite words) and WS1S (Weak Monadic Second Order Logic over ℕ with finite subsets) holds for the standard case where both logics capture regular languages. When adding new relations, the equivalence is preserved if and only if the added relations are definable in both logics using their original vocabularies (i.e., order < and sym...

Short answer

• The Büchi–Elgot–Trakhtenbrot equivalence (MSO on finite words = WS1S on N with finite-set quantification) is robust under adding any relations that are already MSO-definable in the basic signature; in particular, all “regular” and modular-counting predicates preserve both equivalence and decidability.
• A much wider class also works: adding Presburger-style cardinality constraints o...

MSO vs WS1S: Equivalence Under Additional Relations

Your question is definitely of interest in theoretical computer science and logic! It explores the boundary conditions of two fundamental logical formalisms.

Understanding the Base Equivalence

The standard equivalence between MSO (over finite words) and WS1S occurs because:

1. Both logics exactly characterize the regular languages
2. For...

Let τ₀ = {<} ∪ {Qₐ | a ∈ Σ }.
For a finite word w the two structures you look at are

 N(w) = ⟨ ℕ , < , (Qₐ)ₐ ⟩ (WS1S – “weak”, finite–set quantification)
 Nᵣ(w) = ⟨ {0,…,|w|–1}, < , (Qₐ)ₐ ⟩ (MSO – ordinary monadic second–order logic)

Over the vocabulary τ₀ the Büchi/Elgot/Trakhtenbrot theorem gives

 REG = L(WS1S,τ₀) = L(MSO,τ₀).

Now fix an additiona...

Below is a sketch of why “whatever you can define already in MSO (or equivalently in WS1S) you may safely add as a primitive symbol, and you do not gain any extra power or lose decidability, but as soon as you add something not already MSO‐definable the two logics split (or you even lose decidability in the WS1S‐version).” In practice this means:

1. **Regular (or automatic) relations on po...

(Throughout we write

 WS1S(w) := ⟨ ℕ , < , Qₐ₁ , … , Qₐₖ ⟩ and MSO(w) := ⟨ {0,…,|w|–1} , < , Qₐ₁ , … , Qₐₖ ⟩ .
“WS1S-formulas” are interpreted in the first structure, but second–order quantifiers range only over finite sets; “MSO-formulas” are interpreted in the second structure and quantify over arbitrary subsets of the finite domain.)

Why do WS1S and MSO define the same languages in th...

Excellent question. It touches upon a fundamental topic in logic, automata theory, and descriptive complexity: the boundary of decidability and the expressive power of logical formalisms when augmented with new primitives.

Let's break down the problem to establish a clear answer.

Summary of the Answer

The equivalence between MSO on finite words and WS1S (for defining languages of finite wor...

This is indeed an interesting question that touches on fundamental issues in logic and automata theory. Let me provide a comprehensive answer.

The Core Issue

The question explores when the equivalence MSO = WS1S is preserved when extending these logics with additional predicates. This is important because:

1. MSO captures regular languages when interpreted on finite words
2. WS1S (we...