On the Mints Hierarchy in First-Order Intuitionistic Logic

TL;DR

This paper investigates the Mints hierarchy in first-order intuitionistic logic, revealing undecidability at certain levels and complexity classifications for others, advancing understanding of logical fragment decidability.

Contribution

It provides new results on the decidability and complexity of Mints hierarchy fragments, including undecidability of the  level and complexity of  levels.

Findings

 level is undecidable

 level is Expspace-complete

Arity-bounded  fragment is co-Nexptime-complete

Abstract

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.