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
(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)$

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


EDIT: You've characterized "connectedness" correctly. And your comment is right - your characterization of trees works for finite graphs, and that's all you need. So with the addition of connectedness, you're good (and you don't need (0)).

  • $\begingroup$ 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 $\endgroup$ – user343207 Feb 11 '17 at 9:11
  • $\begingroup$ can you help me ? $\endgroup$ – user343207 Feb 11 '17 at 19:55
  • 1
    $\begingroup$ @HaskellFun See my edit; you were right. $\endgroup$ – Noah Schweber Feb 11 '17 at 20:03
  • $\begingroup$ thanks, I edited and show entire solution, for future generations. You are welcom in my thread about logic ! there are many without answer or partial answer $\endgroup$ – user343207 Feb 11 '17 at 22:24
  • 1
    $\begingroup$ @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$. $\endgroup$ – Noah Schweber Feb 11 '17 at 23:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy