Недоказуемые теоремы для диофантовых уравнений
Такое ``недоказуемое утверждение'' F может иметь, в действительности,
очень простую логическую структуру.
Существует недоказуемое утверждение, состоящее из
атомарной формулы, перед которой стоит строка из кванторов существования:
$ v1 ··· vn (t1 = t2)
| (9) |
Это утверждение выражает факт существования решения
диофантова уравнения.* Недоказуемость (9) означает,
что уравнение не имеет решений в натуральных числах, но имеет ``нестандартное
решение'' в некоторой нестандартной модели арифметики первого порядка.
Существование недоказуемого утверждения вида (9) было
установлено Юрием Матиясевичем в 1970 году.
Назад