Комментарий к приведённому доказательству Теоремы Гёделя.
Будем считать

,

, ... программами, которые, беря натуральное число на вводе, дают натуральные числа, на каждом шагу исполнения. Программы

,

, ... останавливаются, если на вводе их индекс, а все остальные программы зацикливаются.
Согласно терминологии теории алгоритмов, множество индексов {

,

, ... } - неразрешимо, т.е. нет алгоритма, позволяющего для любого натурального числа определить принадлежит оно этому множеству или нет.
С другой стороны, рассматриваемое множество индексов полуразрешимо, и перечислимо. Эти понятия определяются в теории алгоритмов, где доказывается, что полуразрешимость и перечислимость это эквивалентные понятия.
Заметим, что множество индексов {

,

, ...} перечислимо, но не в этом порядке (не в порядке возрастания), иначе оно было бы разрешимо.
В 1970 году, Юрий Матиясевич доказал, что любое перечислимое множество является диофантовым, т.е. элементы множества характеризуются тем, что они принадлежат решениям некоторого диофантового уравнения.
Значит утверждение о том, что "программа

останавливается, если на вводе индекс

" эквивалентно некоторому арифметическому утверждению относительно n. Cреди этих утверждений есть такие, которые невозможно ни доказать, ни опровергнуть. Понятия "доказать" и "опровергнуть" арифметическое утверждение зависят от выбора системы аксиом арифметики. Предположим мы написали программу вычисления

. Эта программа выполняет такие программы

относительно которых она найдёт "доказательство", что они останавливаются, если на вводе индекс

. Но если на самом деле они не останавливаются, то мы не сможем утверждать, что она вычисляет

, и не сможем придти к противоречию, доказывающему теорему Геделя. Это произойдёт, если выбрать противоречивую или нездравую систему аксиом.