一阶逻辑在单词上的 alternation 层次是可判定的

我们证明对于任意 $i > 0$，给定的正则语言是否可表达在一阶逻辑 FO[<] 的 $\Sigma_i[<]$ 片段中是可判定的。这解决了自 1971 年以来一直悬置的难题。我们的主要技术结果依赖于类语言 $\mathcal{V}$ 的多项式闭合概念，即形如 $L_0a_1L_1\cdots a_nL_n$ 的有限并集，其中每个 $a_i$ 为一个字符，每个 $L_i$ 为 $\mathcal{V}$ 中的语言。我们证明如果一个具有某些封闭性质（即正 Variety）的正则语言类 $\mathcal{V}$ 的可分离性问题是可判定的，那么它的多项式闭合 Pol($\mathcal{V}$) 也具有可判定性。对于 Pol($\mathcal{V}$) 的 resulting 算法时间复杂度为 $\mathcal{V}$ 的时间复杂度的指数级，我们提出一种自然的猜测，这将导致时间复杂度的多项式级增长。结果包含了半层次 dot-depth 层次和基于群的连接层次的可判定性。