Monadic Second-Order Logic of Permutations
Vít Jelínek, Michal Opler
排列可以视为线性序对的组合，或者更形式化地，作为由两个二元关系符号组成的签名上的模型。Albert、Bouvel和Féray采用了这种方法，他们研究了在此设置下一阶逻辑的表达能力。我们将注意力集中在一元二阶逻辑上。我们的结果朝着两个方向发展。首先，我们研究一元二阶逻辑的表达能力。我们展示了排列的自然性质，这些性质可以用一元二阶逻辑表达但不能用一阶逻辑表达。此外，我们证明了即使在一元二阶逻辑中，具有不动点的性质也是不可表达的。其次，我们关注一元二阶模型检验的复杂性。我们证明存在一种算法，可以在时间f(|φ|, tw(π)) · n内判定排列π是否满足给定的一元二阶句子φ，其中n = |π|且tw(π)是π的树宽，f是某个可计算函数。另一方面，我们证明即使将排列π限制在具有温和假设的固定遗传类𝒞中，该问题仍然保持困难。
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 mo...