Mixed quantifier prefixes over Diophantine equations with integer variables

TL;DR

This paper investigates the decidability of mixed quantifier prefixes over Diophantine equations with integer variables, establishing new undecidability results for specific quantifier structures and conjecturing further undecidability cases.

Contribution

It proves that certain mixed quantifier prefixes, such as  over , are undecidable, advancing understanding of the complexity of Diophantine problems with quantifier alternations.

Findings

 over  is undecidable.

Undecidability persists with bounded universal quantifiers.

Conjecture that  over  is also undecidable.

Abstract

In this paper we first review the history of Hilbert's Tenth Problem, and then study mixed quantifier prefixes over Diophantine equations with integer variables. For example, we prove that $\forall^2\exists^4$ over $\mathbb Z$ is undecidable, that is, there is no algorithm to determine for any $P(x_1,\ldots,x_6)\in\mathbb Z[x_1,\ldots,x_6]$ whether $$\forall x_1\forall x_2\exists x_3\exists x_4\exists x_5\exists x_6(P(x_1,\ldots,x_6)=0),$$ where $x_1,\ldots,x_6$ are integer variables. We also have some similar undecidable results with universal quantifies bounded, for example, $\exists^2\forall^2\exists^2$ over $\mathbb Z$ with $\forall$ bounded is undecidable. We conjecture that $\forall^2\exists^2$ over $\mathbb Z$ is undecidable.