требуют условие того, что формула должна содержать утверждение о своей собственной невыводимости
Это не условие. Это конкретная формула в теореме Геделя так строится. Т.е. если формула истинна, то в общем случае не факт, что она должна каким-то неведомым образом содержать утверждение о своей невыводимости, а в теореме Геделя именно так.
Блин, я Вам все-таки выпишу кусок из Мендельсона, в упрощенном виде... Только подождите...
Берется конкретная система аксиом для арифметики, напоминающая аксиомы Пеано. Далее, производится арифметизация теории: несложными приемами нумеруются все переменные, термы, выражения, формулы, выводы (т.е. у каждого объекта - свой номер - гёделев номер ГН, но не всякое число - ГН объекта). Для простых предикатов "

- ГН константы теории", "

- ГН функциональной буквы теории", "

- ГН предикатной буквы теории" строятся явно их арифметические формулы (например, "

- ГН переменной" выражается формулой

), причем они примитивно-рекурсивны. И поехало: мы, комбинируя простые отношения и выражающие их формулы, явно конструируем арифметические формулы для отношений "

- ГН терма", "

- ГН формулы теории", "

- ГН частного случая схемы аксиом такой-то", "

- ГН такого-то вывода (доказательства) в данной теории" и отношение

- "

- ГН формулы

со свободной переменной

, а

- ГН вывода

".
Берем отношение

- оно выразимо некоторой формулой

теории от

. Т.е. если

истинно, то

. Теперь берем формулу

, пусть

- ее ГН, и берем утверждение (без свободных переменных)

. Теорема Гёделя утверждает, что если теория (арифметика) непротиворечива, то сама формула

невыводима и ее отрицание

невыводимо.
Действительно, предположим, что теория непротиворечива, и формула

выводима.

- ГН этого вывода, то по смыслу

будет верно

, но так как

выражает

, то

. С другой стороны, если верна

, то она верна и для

- получается, что мы вывели

и

, что противоречит предположению, о непротиворечивости теории.
С другой стороны, если выводима

и теория непротиворечива, то

невыводима, поэтому

ложно для любого натурального

. А это значит, что

. Возьмем в качестве

формулу

- получим, что не

- а это противоречит

.
Мендельсон писал(а):
Весьма любопытна стандартная интерпретация неразрешимого пред-
предложения

:

. Так как

выражает в

отношение

, то, в соответствии со стандартной интерпретацией,

утверждает, что

ложно для каждого натурального числа

. Согласно (I) (т.е. определению

), это означает, что не существует вывода формулы

в

. Другими словами, формула

утверждает свою собственную невыводимость в

. По теореме же Гёделя, если только теория

непротиворечива, эта формула и в самом деле невыводима в

и потому истинна при
стандартной интерпретации. Итак, для натуральных чисел, соответствующих обычной интерпретации, формула

верна, но в

невыводима.
З.Ы. Вот я скачал из интернетов книгу Нагель Ньюман Теорема Геделя. Это научпоп, формул нет почти, но я сам не читал (и читал у какого-то E.G.A. в интернете и у Сингха ВТФ). Попробуйте ее прочесть.