# Decidability of $\forall\exists$ diophantine equations

By saying $$\forall\exists$$ diophantine equations I mean sentences of the form: $$\forall x\exists y\,[p(x,y) = 0]$$ where $$p$$ is a polynomial on $$x,y$$, and both $$x,y$$ range over natural numbers.

I want to know the decidability of these sentences. First of all, we can rewrite the sentence into $$\forall x\exists y\,[a_n(x)y^n+\cdots+a_1(x)y+a_0(x)]$$. If $$a_0(x)$$ is a constant, then all possible values of $$y$$ must be divisor of $$a_0(x)$$. Assume $$d_1,...,d_k$$ are non-negative divisors of $$a_0(x)$$ and we can rewrite the problem into $$\forall x\,[p(x,d_1)=0\lor \cdots\lor p(x,d_k) = 0]$$ = $$\forall x\,[(\Pi_{i=1}^k p(x,d_k)) = 0]$$, which is trivially decidable by examining whether all coefficients of $$x^n$$ are zeros or not.

So what if $$a_0(x)$$ contains $$x$$? A reasonable guess is to assign $$y$$ with all polynomial divisor of $$a_0(x)$$. Is that sufficient? And how can we guarantee that the divisor of $$a_0(x)$$ must be non-negative?