# Write formula in MSO that forces on graph lack of cycle

We consider finite undirected graphs over structure with only one relation, namely relation of edges - $E$. The aim is writing formula in MSO of form $\phi = \forall_{X_1}...\forall_{X_k} \psi (X_1, ..., > X_k)$ where $\psi$ is sentence in first order logic. For each finite graph: $G\models\phi$ iff $G$ is undirected tree.

We know that we must find formula such that forces lack of cycles in graph $G$. In case of second order quantifiers we can only use $\forall$. So the natural idea is to express that graph contains cycle (exists) and negate it.

So lets try to express that in graph there exists some cycle.
I would like to express something like:
there exists subset of nodes such that there are two disjoint paths between them
Steps:
(0) (After edition) graph is finite
(1) there exists some subset of nodes
(2) chosen subgraph is connected (one component)
(3) each node in chosen subgraph has degree two
(4) (After edition): Graph must be one component (connected).

For (0) I can't deal with it. I can to it in SO, or even in MSO - but I must have $\exists$, here we have only $\forall$

For (4) we have (we should get negation of this): graph is not-connected $\theta(Y)=\exists_{X\subseteq Y}[ (\exists_x x\in X) \wedge (\exists_x x\notin X) \wedge [(\forall_x\forall_y x\in X \wedge y\notin X) \to (\neg E(x,y) \wedge \neg E(y,x))]]$

Is it ok plan ? Can someone help me realize it?
Thanks to @Noah hints we got final solution:
(3) Each node in $X$ has degree equals to $2$:
$\phi(X) = \forall_{x\in X} \exists_{x_1}\exists_{x_2} [x_1\neq x_2 \wedge E(x_1, x)\wedge E(x_2, x) \wedge (\forall_{y\in X} (E(x,y) \to y \in \{x_1, x_2\}) )]$
(4) $\neg \theta(X)$

Finally:
$$\exists_{X\subseteq V} [\neg \theta(X)\wedge \phi(X)]\wedge \neg\theta(V)$$
We know that each formula is form of $\forall_X ....$ :)

• Do you know a characterization of trees in terms of connectivity? No, i don't. I thought that: For each finite graph: $G⊨ϕ$ iff $G$ is undirected tree. guarantees that graph is not infinite. Moreover, at front of the content of the task we can see: We consider finite undirected graphs. (it was before infinite, but I edited my post and corrected this typo). I added also formula which guarantees connectivity. When our formula must be ready for rejecting infinite graphs, then I ask for your help – user343207 Feb 11 '17 at 9:11
• @HaskellFun There's no reason we shouldn't accept an infinite graph. The problem is to find a $\varphi$ such that for finite $G$, $G\models\varphi$ iff $G$ is a tree; but there's no restriction on what sorts of infinite $G$s should satisfy/not satisfy $\varphi$. – Noah Schweber Feb 11 '17 at 23:06