Shortest path property and monadic second order logic

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$$?

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.

• Thanks for the answer. I don't understand the predicate X. Can you explain more about the predicate X?
– fva
Feb 27, 2023 at 10:38
• @fva a structure equipped with a predicate $X$ means that a subset of the elements are marked as belonging to $X$, and that we can use membership to $X$ in formulas. We can for instance write a formula $\forall y,\exists z, E(y,z)\wedge z\in X$, meaning that every node is connected to a node in $X$. If you have a formula $\varphi(s,t,X)$ with free variables $s,t,X$ that you want to evaluate to true or false, you need in a structure where elements $s,t$ and a set $X$ are part of the signature. $\mathcal D$ here will be these kind of structures. Feb 27, 2023 at 12:00