Доказательство теоремы Гёделя о неполноте

[cscscs]

Пусть $G(F)$ - геделевский номер формулы $F$. Понятно как считать $G^{-1}(x)$ при конкретном значении $x$. Но что за формула арифметики Пеано соответствует $G^{-1}(x)$, когда там стоит не конкретное число вместо $x$, а просто переменная $x$ стоит? Например, пусть мы так занумеровали символы теории: $0$ -- $1$, $S$ -- $2$, $=$ -- $3$. Тогда $G^{-1}(525)=. Все чётко и ясно. Но чему равно $G^{-1}(x)$ -- не понятно. Её же нельзя выписать. Как мы можем тогда говорить вещи вроде: "давайте рассмотрим формулу арифметики $\exists x \; G^{-1}(x)$"? Ведь не понятно, что именно это за формула, из каких конкретно символов арифметики она состоит.

[Xaositect]

А какое изложение доказательства Вы имеете в виду? Я не припомню ни одной книги, где использовалась бы $G^{-1}$. И тем более $\exists x G^{-1}(x)$, это вообще очень сомнительное выражение.

[cscscs]

Xaositect в сообщении #824844 писал(а):

А какое изложение доказательства Вы имеете в виду?

http://www.math.ru/media/lecture/12
Там $G$ обозначается через $\gamma$ и определяются формула $\text{Dok}(y,x):=(y=\Gamma(\text{доказательство }\gamma^{-1}(x)))$, функция $s(z)=\gamma(\prod_x^z(\gamma^{-1}(z)))$.

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

[cscscs]

Нагель Э., Ньюмен Дз.Р.(Nagel, Newman) Теорема Геделя [2изд] УРСС 2010:

Цитата:

Мы будем записывать отношение между числами $x$ и $z$ посредством формулы "$\text{Dem}(x,y)$" напоминающей нам самим своим обликом о том метаматематическом утверждении, которому она соответствует (а именно, об утверждении "Последовательность формул, имеющая гёделевский номер $x$, является доказательством формулы, имеющей гёделевский номер $z$").

Читатель должен твердо уяснить себе, что хотя "$\text{Dem}(x,y)$" кодирует некоторое метаматематическое утверждение, сама эта запись является формулой арифметического исчисления. Формула эта в более привычных обозначения может быть записана в виде $f(x,y)=0$, где буква $f$ обозначает некоторый довольно-таки сложный комплекс арифметических операций над числами. Однако эта более привычная записаь не "подсказывает" сразу своей метаматематической интерпретации, почему мы и предпочли запись, приведенную в тексте.

Вот такое изложение никуда не годится. Не убедительно. Я хочу посмотреть на эту формулу арифметического исчисления. Или хотя бы чтобы мне показали как её строить. Не считать в некоторых значения, а построить для произвольных $x$ и $z$ формулу.

[nikvic]

cscscs в сообщении #824866 писал(а):

Вот такое изложение никуда не годится. Не убедительно. Я хочу посмотреть на эту формулу арифметического исчисления. Или хотя бы чтобы мне показали как её строить

Всё это "упрятано" в часть теории алгоритмов, где доказывается существование универсального алгоритма.
Даже если слово алгоритм не упоминается.

Как в анекдоте про коммивожёра, который представил хозяину (тот не хотел платить за шляпу) отчёт со словами ""Шляпа там есть, но Вы её не увидите.

В варианте

Цитата:

$f(x,y)=0$, где буква $f$ обозначает некоторый довольно-таки сложный комплекс арифметических операций над числами

приходится долго разбираться, когда речь идёт о функции, а когда - об одном из её "имён", т.е. алгоритмов.

[cscscs]

nikvic в сообщении #824899 писал(а):

Всё это "упрятано" в часть теории алгоритмов, где доказывается существование универсального алгоритма.
Даже если слово алгоритм не упоминается.

Я так и думал. Видимо через какие-нибудь рекурсивные функции построение дается.

[Xaositect]

cscscs в сообщении #824850 писал(а):

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

Посмотрите Мендельсон "Введение в математическую логику"