Shortest path property and monadic second order logic

Question

I know that induced paths and Hamiltonian cycles can be expressed with monadic second-order logic ($MS_2$).

Is it possible to express the shortest path in $MS_2$?

Answer 1

I'm assuming you want a formula $\varphi(s,t,X)$ in $MSO_2$ on graphs, stating that the set $X$ is the shortest path from $s$ to $t$. Under this meaning of "express the shortest path", no such formula exists.

We can prove this using the fact that there is no MSO formula that, given a word of the form $a^nb^m$, accepts it if $n\leq m$. This last fact is because MSO on words can only define regular languages.

For this, we can use a result of Courcelle and Engelfriet stating that if $\tau$ is a MSO interpretation $\mathcal C\to \mathcal D$ where $\mathcal C$ and $\mathcal D$ are classes of structures, and if $L\subseteq \mathcal D$ is MSO-definable, then $\tau^{-1}(L)\subseteq \mathcal C$ is MSO-definable as well. See the book of Courcelle and Engelfriet for details on MSO interpretations and the proof of this theorem here (there might be more recent and readable accounts).

Here, we can take for $\mathcal D$ the set of finite graphs where elements are nodes and edges (to capture $MSO_2$) with two distinguished points $s,t$ and a monadic predicate $X$, and for $\mathcal C$ the set of finite words.

The MSO interpretation $\tau$ will associate to each word a set of graphs (actually one graph or none) by defining the elements and relations as follows:

• if the word is not of the form $a^nb^m$ reject
• the nodes of the graph correspond to the positions of the word
• define $s$ to be the last $a$, and $t$ to be the last $b$
• edges are the same as in the word (two consecutive letters are linked), + an extra edge linking the beginning of the word to the end.
• the predicate $X$ marks $a$ positions + links between them and the extra edge.

We end up with a cycle, such that $X$ is the shortest path from $s$ to $t$ if and only $n\leq m$. This means that if there was a formula $\varphi(s,t,X)$ checking that $X$ is the shortest path from $s$ to $t$, we could obtain a MSO formula $\psi$ on words for $\tau^{-1}(L(\varphi))=\{a^nb^m\mid n\leq m\}$. So $\psi$ would be a MSO formula for a non-regular language, contradiction.