Finding polynomials with a specific property I am stuck with the following problem.

Show that there exist a $n \in \mathbb{N}$ and polynomials $p,q \in \mathbb{N}[x_1,\ldots,x_n]$ such that neither the formula $$ \phi(n,p,q) = \forall x_1  \cdots \forall x_n : \neg ( p(x_1,\ldots,x_n) = q(x_1,\ldots,x_n))$$ nor $\neg \phi$ are not theorems of formal arithmetic.

How can one construct such polynomials?
 A: This is a consequence of the result of Matiyasevich that every recursively enumerable predicate is Diophantine.
Let $R(y)$ be a recursively enumerable predicate which is not recursive. Then by the result of Matiyasevich, there exists an $n$, and a polynomial $A(y)$ with integer coefficients, such that for any natural number $y$, $R(y)$ iff $\exists x_1\exists x_2\dots \exists x_n(A(y,x_1,\dots,x_n)=0$) is true in $\mathbb{N}$. 
By separating the positive and negative coefficients, we can rewrite $A=0$ as $P=Q$, where $P$ and $Q$ have coefficients in $\mathbb{N}$.
If we use recursively axiomatized arithmetic $T$ all of whose axioms are true in $\mathbb{N}$, such as (first-order) Peano Arithmetic, and for every $k$ the sentence obtained by replacing $y$ by $k$ is provable or refutable in $T$, then $R(y)$ is recursive. 
Remark: In principle, for any theory $T$ described above, one can use the proof of Matiyasevich's Theorem, and diagonalization, to construct an explicit pair of polynomials $p$ and $q$. But these  would be extremely complicated.   
