Recursively enumerable sets of polynomials over a finite field

We prove that a relation over is recursively enumerable if and only if it is Diophantine over . We do this by first constructing a model of in , where n is represented by Zⁿ. In a second step, we show that it suffices to eliminate a bounded universal quantifier. Then finally, the hardest part of the proof is to show that we can eliminate this quantifier.