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$?
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this communityI'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:
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.