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 φ in time 𝑓 ⁡ ( | 𝜑 | , t w ⁡ ( 𝜋 ) ) ⋅ 𝑛 for some computable function f where 𝑛 = | 𝜋 | and t w ⁡ ( 𝜋 ) 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 𝒞 with mild assumptions on 𝒞 .