MathLabs

Worked solution: The MRDP theorem: Diophantine sets are exactly the recursively enumerable sets (1970)

Step 3 of 9: Davis's 1953 conjecture: r.e. sets are exactly the Diophantine sets
Previous stepNext step
In plain words

Building on Kurt Gödel's earlier work showing that computable notions can be arithmetized into statements about numbers, Martin Davis in 1953 took a first concrete step: he showed every listable set can be described using a formula with just one "for all" quantifier bounded by a limit, sitting in front of an otherwise purely algebraic statement (the "Davis normal form").

Davis conjectured that this bounded quantifier could eventually be eliminated entirely, leaving a pure polynomial equation — that is, that listable sets and Diophantine sets are exactly the same notion. If true, this would be the crucial bridge letting Turing's undecidable halting problem be encoded directly as a question about integer roots of a polynomial.

S recursively enumerable =? {a:∃x1,…,xn∈Z≥0, P(a,x1,…,xn)=0}S \text{ recursively enumerable} \ \overset{?}{=} \ \{a : \exists x_1, \ldots, x_n \in \mathbb{Z}_{\ge 0},\ P(a, x_1, \ldots, x_n) = 0\}
Detailed analysis

In 1953 Martin Davis conjectured that every recursively enumerable set S⊆Z≥0S \subseteq \mathbb{Z}_{\ge 0} equals a Diophantine set: there is a polynomial PP with integer coefficients such that a∈Sa \in S iff ∃x1,…,xn∈Z≥0\exists x_1, \ldots, x_n \in \mathbb{Z}_{\ge 0} with P(a,x1,…,xn)=0P(a, x_1, \ldots, x_n) = 0. This built on Davis's own "Davis normal form" result, itself refining Gödel's arithmetization of computable predicates, that every r.e. set already has a definition of the form ∃x ∀y≤x ∃z1,…,zk\exists x\, \forall y \le x\, \exists z_1, \ldots, z_k (polynomial equation), i.e. with just one bounded universal quantifier standing in the way of a pure existential (Diophantine) definition.

Eliminating that single bounded quantifier turned out to require nearly two decades of further work, because it demanded finding polynomial equations that could somehow simulate bounded search and exponential-sized computations — something ordinary polynomial growth (bounded by a fixed power of the input) seemed fundamentally too weak to do.

The path forward, developed through the 1950s, was to isolate exactly what extra ingredient was missing; the next step identifies it precisely as a single relation with exponential growth.

Terms in this step
Davis normal form
Davis's 1953 result that every recursively enumerable set can be defined by a formula with exactly one bounded universal quantifier in front of an otherwise purely existential polynomial statement — the precise gap Davis's conjecture proposed to close.
Knowledge used in this step
Recursive functions and Turing machines