# Is hypergraph reachability definable in MSO?

Let $$(A,E)$$ be a directed 2-uniform hypergraph and $$E$$ the corresponding binary relation such that $$(X,Y) \in E$$ iff there is a hyperedge from $$X$$ to $$Y$$. We say that there is a path from $$X_1$$ to $$X_k$$ iff there is a sequence $$(X_1,...,X_k)$$ such $$(X_1,X_2) \in E \wedge (X_2,X_3) \in E \wedge ... \wedge (X_{k-1},X_k)\in E$$.

Is there a MSO-sentence reach such $$(A,E) \models \text{reach}(U,V)$$ iff $$V$$ is reachable from $$U$$?

Reachability for graphs in general is definable by reach$$(u,v)$$ $$\exists X \forall Y ((u \in Y \wedge \forall x \forall y (x \in Y \wedge y \in X \wedge E(x,y))\rightarrow y \in Y) \rightarrow v \in Y)\text{.}$$ However, I am not successful with replacing the first order variables by second order ones (and the corresponding $$\in$$ by $$\subseteq$$).

• Sorry, I do not understand the question. What is the difference between a "directed 2-uniform hypergraph" and simply a directed graph? What are the elements of the set $A$ in your notion of a directed 2-uniform hypergraph? Are they something else than vertices of a graph? In fact, I wonder if there isn't some underlying confusion in your question: MSO formulas can use quantification over sets, but the domain of the structure on which they are evaluated consists of elements just like in first-order logic.
– a3nm
Jan 24 at 18:43