I need to define a formula, which will be true for strings meeting this pattern (10)*1* (zero or more occurrences of 10, followed by zero of more occurrences of 1).
For the reference, syntax for WS1S (Weak monadic second order logic of one successor) is defined as followed: $$\phi \rightarrow X \subseteq X | succ(X) | ϕ ∨ ϕ | ¬ϕ | ∃X.ϕ$$ and is interpreted over finite subsets of $\mathbb{N}$.
I started solving this problem by defining conditions for this string one by one.
- Consider 2 sets $A$ and $B$. $A$ will represent positions of 1 in the pattern
(10)*and $B$ will represent positions of 1 in the pattern1*. - Sets must be distinct: $\neg(A \subseteq B)$ and $\neg(B \subseteq A)$
- In $A$ there can only by
10*pattern: $\neg(succ(A) \subseteq A)$ - In $B$ there can only by
1*pattern: $(succ(B)\subseteq B)$
Now I don't know how to connect this two sets, so $B$ can only be after $A$. I already tried defining this condition like this: $(succ(succ(A)) \subseteq B)$, but it doesn't ensure that $B$ can be only after the very last occurrence of 10 in $A$.