The core of the proof of the undecidability of the tenth problem is the proof that exponentiation is Diophantine. We reduced this to proving that certain sequences given by second-order recurrence equations are Diophantine. These are the Matiyasevich sequences: For ,
for all .
We begin the proof that they are Diophantine by analyzing some of the algebraic identities their terms satisfy.
Unsolvable problems, by M. Davis. In Handbook of mathematical logic, J. Barwise, ed., North-Holland (1977), 567-594.