Authors: 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.

• 03B20 - Subsystems of classical logic (including intuitionistic logic)
• 03B25 - Decidability of theories and sets of sentences
• 03D15 - Complexity of computation (including implicit computational complexity)
• 03D35 - Undecidability and degrees of sets of sentences