A formula in MSO Let $\Sigma$ be a signature: $\Sigma = \{e, P\}$. Let $\mathcal{A}$ be a class of undirected graphs of the form $\mathfrak{A} = (A, e, P) $ where $P$ is single-argument relation. Prove that for every connected component there exists a such $v \in A$ that $P(a)$ 
Write a Monadic Second Order formula which defines that property:
My approach:
$$\forall x \exists y (\forall X (\forall u \forall v ( u \in X \wedge e(u,v) \implies v \in X) \wedge x \in X ) \implies y \in X) \wedge P(y)$$
The second version:
$$ \forall X X\text{ is connected component } \implies \exists x x \in X \wedge P(x)$$ 
$$ X \text{ is connected component is defined: } \forall u,v (u \in X \wedge e(u,v)) \implies v \in X$$
Right?
 A: I'll use the convention that the scope of a quantifier is the parenthesized expression following the quantifier.  The first formula, slightly adjusted to conform to that convention, is:
$$\forall x \exists y \,((\forall X \,(\forall u \forall v \,( u \in X \wedge e(u,v) \rightarrow v \in X) \wedge x \in X ) \rightarrow y \in X) \wedge P(y)) \enspace. $$
It says that for every vertex $x$ there is a vertex $y$ such that $P(y)$ holds and, for every subset $X$ including $x$ with a certain property $C(X)$ to be discussed, $y$ is also in $X$.
$C(X)$ is not "$X$ is a connected component of the graph."  Rather, it is "$X$ is closed under the edge relation $e$."  However, every (maximal) connected component is closed under the edge relation, and every set of vertices that is closed under the edge relation consists of an integral number of connected components.  Hence $C(x)$ is adequate for the task at hand.
Bottom line: This sentence is OK.  
The second sentence is, with minor adjustments,
$$ \forall X \,(\text{ConnectedComponent}(X) \rightarrow \exists x \,(x\in X \wedge P(x))) \enspace. $$
It is obviously OK if we come up with a way to write a formula with one free variable $\text{ConnectedComponent}(X)$ that is true of a set of vertices $X$ if and only if $X$ is a connected component of the graph.  One solution is this:
$$  \forall Y \,((Y \neq \emptyset \wedge Y \subseteq X \wedge Y \neq X) \rightarrow \exists u \exists v \,(u \in Y \wedge v \in (X \setminus Y) \wedge e(u,v)))\enspace. $$
This formula says that no matter how you split $X$ into two nonempty subsets, there's an edge of the graph that joins the two subsets.
The subformulae like $Y \neq \emptyset$ and $Y \subseteq X$ are obviously abbreviations of formulae like $\forall v \,(\neg (v \in Y))$ and $\forall v \,(v \in Y \rightarrow v \in X)$.
