On the Mints Hierarchy in First-Order Intuitionistic Logic

We stratify intuitionistic first-order logic over (∀,→) 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 Δ2 level is undecidable and that Σ1 is Expspace-complete. We also prove that the arity-bounded fragment of Σ1 is complete for co-Nexptime.