一句话：证明一阶直觉主义逻辑 Mints 层级中 Δ2 不可判定、Σ1 为 Expspace-完全，并刻画元数受限 Σ1 的复杂度。
本文对一阶直觉主义逻辑中仅使用全称量词和蕴含的片段按量词正负出现交替进行分层，称为 Mints 层级，并系统研究各层的可判定性与复杂度。作者证明：即便位于较低交替层级的 Δ2 片段也是不可判定的；而 Σ1 片段是 Expspace-完全的。进一步，对于元数受限的 Σ1 片段，作者证明其复杂度为 co-Nexptime-完全。这些结果揭示了量词交替如何影响直觉主义一阶逻辑的可判定边界与计算难度，给出了精确的复杂度刻画。
We stratify intuitionistic first-order logic over $(\forall,\to)$ into fragments determined by the alternation of positive and negative occurrences of quantifiers (Mints hierarchy). We study the decidability and complexity of these fragments. We prove that even the $\Delta_2$ level is undecidable and that $\Sigma_1$ is Expspace-complete. We also prove that the arity-bounded fragment of $\Sigma_1$ is complete for co-Nexptime.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{SchubertUZ15,
title = {On the Mints Hierarchy in First-Order Intuitionistic Logic},
author = {Aleksy Schubert and Paweł Urzyczyn and Konrad Zdanowski},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 4},
year = {2017},
doi = {10.2168/lmcs-12(4:11)2016}
}