<p>I'm assuming you want a formula <span class="math-container">$\varphi(s,t,X)$</span> in <span class="math-container">$MSO_2$</span> on graphs, stating that the set <span class="math-container">$X$</span> is the shortest path from <span class="math-container">$s$</span> to <span class="math-container">$t$</span>. Under this meaning of &quot;express the shortest path&quot;, no such formula exists.</p>
<p>We can prove this using the fact that there is no MSO formula that, given a word of the form <span class="math-container">$a^nb^m$</span>, accepts it if <span class="math-container">$n\leq m$</span>. This last fact is because MSO on words can only define regular languages.</p>
<p>For this, we can use a result of Courcelle and Engelfriet stating that if <span class="math-container">$\tau$</span> is a MSO interpretation <span class="math-container">$\mathcal C\to \mathcal D$</span> where <span class="math-container">$\mathcal C$</span> and <span class="math-container">$\mathcal D$</span> are classes of structures, and if <span class="math-container">$L\subseteq \mathcal D$</span> is MSO-definable, then <span class="math-container">$\tau^{-1}(L)\subseteq \mathcal C$</span> is MSO-definable as well. See the book of Courcelle and Engelfriet for details on MSO interpretations and the proof of this theorem <a href="https://www.labri.fr/perso/courcell/Book/TheBook.pdf" rel="noreferrer">here</a> (there might be more recent and readable accounts).</p>
<p>Here, we can take for <span class="math-container">$\mathcal D$</span> the set of finite graphs where elements are nodes and edges (to capture <span class="math-container">$MSO_2$</span>) with two distinguished points <span class="math-container">$s,t$</span> and a monadic predicate <span class="math-container">$X$</span>, and for <span class="math-container">$\mathcal C$</span> the set of finite words.</p>
<p>The MSO interpretation <span class="math-container">$\tau$</span> will associate to each word a set of graphs (actually one graph or none) by defining the elements and relations as follows:</p>
<ul>
<li>if the word is not of the form <span class="math-container">$a^nb^m$</span> reject</li>
<li>the nodes of the graph correspond to the positions of the word</li>
<li>define <span class="math-container">$s$</span> to be the last <span class="math-container">$a$</span>, and <span class="math-container">$t$</span> to be the last <span class="math-container">$b$</span></li>
<li>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.</li>
<li>the predicate <span class="math-container">$X$</span> marks <span class="math-container">$a$</span> positions + links between them and the extra edge.</li>
</ul>
<p>We end up with a cycle, such that <span class="math-container">$X$</span> is the shortest path from <span class="math-container">$s$</span> to <span class="math-container">$t$</span> if and only <span class="math-container">$n\leq m$</span>. This means that if there was a formula <span class="math-container">$\varphi(s,t,X)$</span> checking that <span class="math-container">$X$</span> is the shortest path from <span class="math-container">$s$</span> to <span class="math-container">$t$</span>, we could obtain a MSO formula <span class="math-container">$\psi$</span> on words for <span class="math-container">$\tau^{-1}(L(\varphi))=\{a^nb^m\mid n\leq m\}$</span>. So <span class="math-container">$\psi$</span> would be a MSO formula for a non-regular language, contradiction.</p>

CC BY-SA 4.0
2023-02-27T10:38:20.210Z
Thanks for the answer. I don't understand the predicate X. Can you explain more about the predicate X?
fva
CC BY-SA 4.0
2023-02-27T12:00:24.280Z
@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.
Denis
CC BY-SA 4.0
2023-02-24T15:57:46.457Z
2023-02-24T15:57:46.457Z
Denis
<p>I know that induced paths and Hamiltonian cycles can be expressed with monadic second-order logic (<span class="math-container">$MS_2$</span>).</p>
<p>Is it possible to express the shortest path in <span class="math-container">$MS_2$</span>?</p>

<lo.logic><shortest-path>
Shortest path property and monadic second order logic
fva
# Shortest path property and monadic second order logic

(Asked by: username_0 on 2023-02-21)

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

**Tags:** lo.logic, shortest-path


---

## 1 answers

### Answer by username_1 on 2023-02-24. Score: 5 | Accepted answer

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](https://www.labri.fr/perso/courcell/Book/TheBook.pdf) (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.

> **Comments:**
> **username_0**: Thanks for the answer. I don't understand the predicate X. Can you explain more about the predicate X?  
> **username_1**: @username_0 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.  

---

