On the Mints Hierarchy in First-Order Intuitionistic LogicArticle
Authors: Aleksy Schubert ; Paweł Urzyczyn ; Konrad Zdanowski
0000-0002-9316-6098##NULL##0000-0002-8846-3733
Aleksy Schubert;Paweł Urzyczyn;Konrad Zdanowski
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.
Ken-etsu Fujita;Aleksy Schubert;Paweł Urzyczyn;Konrad Zdanowski, 2024, The existential fragment of second-order propositional intuitionistic logic is undecidable, Journal of Applied Non-Classical Logics, 34, 1, pp. 55-74, 10.1080/11663081.2024.2312774.
Makoto Fujiwara;Taishi Kurahashi, 2023, Prenex normalization and the hierarchical classification of formulas, Archive for Mathematical Logic, 63, 3-4, pp. 391-403, 10.1007/s00153-023-00899-x.