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.

@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}
}