 # The First Step to the Proof

Martin Davis had not much informal evidence in support of his conjecture. Slight support came from the following result announced in  and proved in [4-6].

Theorem (Martin Davis). For every listable set M there exists a polynomial Q with integer coefficients such that Representation of type (2.6) became known as Davis normal form. They can be considered as an improvement of Kurt Godel’s technique  of arithmetization. This technique allowed him to represent any listable set by an arithmetical formula containing, possibly, many universal quantifiers. If all of them are bounded than such an arithmetical formula defines a listable set, and this can be used as another definition of them (this is the content of Theorem 2.7 from Martin Davis dissertation ).

# A Milestone

In 1959 Martin Davis and Hilary Putnam  managed to eliminate the single universal quantifier from Davis normal form but this was not yet a proof of Davis conjecture for two reasons.

First, they were forced to consider a broader class of exponential Diophantine equations. They are equations of the form where EL and ER are exponential polynomials, that is expression constructed by traditional rules from the variables and particular positive integers by addition, multiplication and exponentiation.

Second, the proof given by Martin Davis and Hilary Putnam was conditional: they assumed that for every k there exist an arithmetical progression of length k consisting of different prime numbers. In 1959 this hypothesis was considered plausible but it was proved by Ben Green and Terence Green only in 2004 . Thus all what Davis and Putnam needed was to wait for 45 years!

Luckily, they had not to wait for so long. Julia Robinson  was able to modify the construction of Davis-Putnam and get an unconditional proof. In 1961 Martin Davis, Hilary Putnam, and Julia Robinson published a joint paper  with the following seminal result.

DPR-theorem. Every listable set M has an exponential Diophantine representation, i.e., a representation of the form where EL and ER are exponential polynomials.

The elimination of the universal quantifier from Davis normal form immediately gave the undecidability of the counterpart of Hilbert’s tenth problem for the broader class of exponential Diophantine equations.