Z is definable in Q by a universal first-order formula in the language of rings

You need to know: Set ${\mathbb Z}$ of integers, set ${\mathbb Q}$ of rational numbers, standard notations $\forall$ (for all) and $\exists$ (there exists), polynomials.

Background: Let ${\mathbb Z}[t, x_1, \dots, x_n]$ denote the set of polynomials in $n+1$ variable $t, x_1, \dots, x_n$ with integer coefficients.

The Theorem: On 15th October 2010, Jochen Koenigsmann submitted to arxiv a paper in which he proved the existence of positive integer n, and a polynomial $g \in {\mathbb Z}[t, x_1, \dots, x_n]$ such that, for any $t\in{\mathbb Q}$ , we have $t\in{\mathbb Z}$ if and only if $\forall x_1, \dots, \forall x_n \in {\mathbb Q}: g(t,x_1,\dots,x_n) \neq 0$ .

Short context: Hilbert’s 10th problem was to find a general algorithm for deciding, given any n and any polynomial $f \in {\mathbb Z}[x_1, \dots, x_n]$ , whether or not f has a zero in ${\mathbb Z}^n$ . In 1970, Matiyasevich proved that there can be no such algorithm. Hilbert’s 10th problem over ${\mathbb Q}$ remains open. If we could define ${\mathbb Z}$ in ${\mathbb Q}$ as in the Theorem but with existential quantifiers $\exists$ instead of universal ones $\forall$ , this together with Matiyasevich theorem would give a (negative) answer to this problem. The Theorem may be considered as a major step in this direction.