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}$.

翻译：置换可视为线性序对，或更形式化地，作为由两个二元关系符号构成的签名上的模型。Albert、Bouvel和Féray采用此方法，研究了一阶逻辑在此设定下的表达能力。我们聚焦于一元二阶逻辑。我们的成果分为两个方向。首先，我们探究一元二阶逻辑的表达能力。我们展示了置换中可用一元二阶逻辑表达但无法用一阶逻辑表达的自然性质。此外，我们证明即使在一元二阶逻辑中，具有不动点的性质也是不可表达的。其次，我们关注一元二阶模型检验的复杂度。我们证明存在一种算法，可在时间$f(|\varphi|, \operatorname{tw}(π)) \cdot n$内判定置换$π$是否满足给定的一元二阶语句$\varphi$，其中$f$为可计算函数，$n = |π|$，$\operatorname{tw}(π)$为$π$的树宽。另一方面，我们证明即使将置换$π$限制在满足温和假设的固定遗传类$\mathcal{C}$中，该问题仍保持困难性。