Monadic Second-Order Logic of Permutations

Permutations can be viewed as pairs of linear orders, or more formally as models over a signature consisting of two binary relation symbols. This approach was adopted by Albert, Bouvel and Féray, who studied the expressibility of first-order logic in this setting. We focus our attention on monadic second-order logic. Our results go in two directions. First, we investigate the expressive power of monadic second-order logic. We exhibit natural properties of permutations that can be expressed in monadic second-order logic but not in first-order logic. Additionally, we show that the property of having a fixed point is inexpressible even in monadic second-order logic. Secondly, we focus on the complexity of monadic second-order model checking. We show that there is an algorithm deciding if a permutation $π$ satisfies a given monadic second-order sentence $\varphi$ in time $f(|\varphi|, \operatorname{tw}(π)) \cdot n$ for some computable function $f$ where $n = |π|$ and $\operatorname{tw}(π)$ is the tree-width of $π$. On the other hand, we prove that the problem remains hard even when we restrict the permutation $π$ to a fixed hereditary class $\mathcal{C}$ with mild assumptions on $\mathcal{C}$.