How is this MSO- (Monadic second-order logic)-formula working? I have the following MSO-formula
\begin{array}{c} 
\varphi:=\exists X \exists Y \min \in X \wedge \max \in Y \wedge \forall x \neg(x \in X \wedge x \in Y) \wedge \\ 
\forall x(x<\max \rightarrow(x \in X \leftrightarrow x+1 \in Y)) 
\end{array}.
If I have the word $w=a,b,c,d$ with universe $\{1,2,3,4\}$ (positions of the letters) and the alphabet $\{a,b,c,d\}$.
Clearly $1\in X$ and $4\in Y$. If $1\in X$ -> $2\in Y$, but if $2\in Y$, how the formula works in this case?  $x$ would be $x = 2 < 4$ but $2$ can not be in $X$, because $X \cap Y = \emptyset$.
Hope someone can help me.:)
 A: As you observe, the first part of the formula tells us that if $X$ and $Y$ satisfy the relevant property (the part of the formula after the "$\exists X\exists Y$"), then $1\in X$, $4\in Y$, and $X\cap Y=\emptyset$.
Note that I'm conflating set variables with actual sets here. This is ultimately a bad habit, but will make things simpler at the moment.
This leaves the clause $\forall x<max(x\in X\leftrightarrow x+1\in Y)$. Each particular $x<max$ gives rise to an instance of this clause:

*

*$x=1$: we have $1\in X\leftrightarrow 2\in Y$.


*$x=2$: we have $2\in X\leftrightarrow 3\in Y$.


*$x=3$: we have $3\in X\leftrightarrow 4\in Y$.
So to recap, we have two "starting values" ($1\in X$ and $4\in Y$), three bi-implications (the bulletpoints above), and a disjointness fact. We can apply these to fully determine $X$ and $Y$ as follows:

*

*We already know $1\in X$, so our first bi-implication gives $2\in Y$ (as you observe). By disjointness, we also know $1\not\in Y$ and $2\not\in X$.


*Now our second bi-implication says $2\in X\leftrightarrow 3\in Y$. We know at this point that $2\not\in X$, so this tells us that $3\not\in Y$.


*Finally, since we know $4\in Y$, our third bi-implication tells us that $3\in X$ (go right-to-left). And by disjointness we know $4\not\in X$.

*

*Note that by disjointness, once we know $3\in X$ we also know $3\not\in Y$. So step $2$ was unnecessary. But it's still worth going through to build comfort with this sort of reasoning.



At this point we've determined that there is only one possible choice for $X$ and $Y$ to make that formula true, namely $$X=\{1,3\}, Y=\{2,4\}.$$ You should check that in fact this pair of sets does have the desired properties.
