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 began 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.