Недоказуемые теоремы для диофантовых уравнений

Такое ``недоказуемое утверждение'' F может иметь, в действительности, очень простую логическую структуру. Существует недоказуемое утверждение, состоящее из атомарной формулы, перед которой стоит строка из кванторов существования:

$ v1 ··· vn (t1 = t2)

(9)

Это утверждение выражает факт существования решения диофантова уравнения.^* Недоказуемость (9) означает, что уравнение не имеет решений в натуральных числах, но имеет ``нестандартное решение'' в некоторой нестандартной модели арифметики первого порядка.

Существование недоказуемого утверждения вида (9) было установлено Юрием Матиясевичем в 1970 году.