1. Собственно о парадоксе в теореме. Напомню, что (очень упрощённо) высказывания формального языка (для арифметики Пеано) однозначно кодируются, превращаясь таким образом в некоторые числа. Затем, уже с помощью метаязыка, получаем высказывание о высказываниях. Т.е. числом можно закодировать, что высказывание №NN истинно. Парадокс появляется на стадии, когда №NN - номер самого высказывания. Фактически имеем высказывание "Я - истинно".

Авторекурсия в таком высказывании не очевидна, однако, если его записать развёрнуто: "содержание данного высказывания истинно", то становится ясным, что содержанием данного высказывания является "содержание данного высказывания истинно". Иными словами: "содержание данного высказывания - <<"содержание данного высказывания истинно">> - истинно". И т.д. с бесконечной вложенностью.

Доказательство теоремы базируется на том факте, что высказывания, формируемые на базе аксиом PA, не описывают высказывания "Я - истинно", существующего, тем не менее в гёделевской нумерации.

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

Введем дополнительное (вполне формальное, впрочем) требование к языку: в высказывании всякое вложенное подвысказывание заключается в специально выбранные знаки (символы). Например - фигурные скобки (или что-то другое, не используемое в данном языке по иному назначению).

Теперь всякое высказывание мы можем разобрать на отдельные высказывания, заменяя подвысказывание некоторым специальным образом (например Р(x)).

Составим полный список из всех таких высказываний, нумеруя в каждом вложенные Р(x) - Р1(x), Р2(x) и т.д. Отсортируем их (например, по алфавиту), исключим из списка дублированные.

Аксиомы постулируют различные свойства некоторых объектов, однако две различные аксиомы, одинаковые тем не менее в содержательной части, могут постулировать различные свойства (например "X*Y -> Y*X" и "X*Y -> -Y*X"). Сгруппируем такие аксиомы и исключим из списка полных высказываний такие, что содержат подобные взаимоисключающие аксиомы. Теперь перестроим список аксиом на основании нового полного списка высказываний, группируя при этом аксиомы, встречающиеся в одном высказывании и не исключая дублирование. Мы получили некоторое количество различных групп аксиом, с помощью каждой из которых возможно синтаксически непротиворечиво сформировать различные же группы высказываний. Однако, некоторые группы аксиом могут состоять из одной единственной аксиомы и такой аксиоме будет соответствовать одно единственное высказывание. Из чего должно следовать, что для данного уровня финитности (т.е. длины выражения) существуют высказывания, которые не могут быть выведены на основании любой группы аксиом с числом аксиом в группе больше одной. Таким образом, существует аксиоматика, которая не в состоянии обеспечить построение всех возможных высказываний заданной длины на данном языке.

Назовём отношение двух различных высказываний тавтологией, если они оба могут быть сведены к третьему при помощи упрощающего высказывание алгоритма (соответственно, существует высказывание, которое не может быть алгоритмом упрощено, но оно вовсе не обязательно будет являться аксиомой). Равным образом, с помощью обратного алгоритма можно создавать тавтологии "от простого к сложному". Многократно применяя усложняющий алгоритм к неупрощаемому высказыванию можно создать дерево тавтологий (простейший пример: 4, 1+3, 2+2, 2+3-1 и т.п.). Обеспечение непротиворечивости преобразований упрощения и усложнения возлагается на соответствующие алгоритмы.

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

За полноту и непротиворечивость группы аксиом голову отдавать не стану, но вот вопрос: действительно эквивалентно ли существование невыводимого высказывания и неполноты группы аксиом... Возможно, в этом что-то есть.

Суть проблемы, собственно говоря, отсутствует. Наличествуют сопутствующие мысли, возникшие при прочтении книги, раскрывающей (популярно, но достаточно близко к источнику) суть доказательств Гёделя. В свою очередь из теорем Гёделя следует, что не существует аксиоматических систем аксиом, обладающих полнотой (поскольку существуют выражения, никак из этих аксиом не следующие). Горячие умы из этого делают вывод о глобальной несостоятельности аксиоматического подхода.

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

Кроме того (и в связи с пониманием автореферентности) возникли рассуждения по поводу соотношения между несуществованием автореферентных (т.е. фактически бесконечной длинны) высказываний при обеспечении финитности (общеупотребительный термин в данном вопросе) вычислений и между применением именно автореферентного высказывания применяемого при доказательстве теоремы. Научное сообщество проблемы в том не усматривает. Так тому и быть.

И, наконец, попытка небольшого исследования под лозунгом: а что если не пользоваться гёделевской нумерацией высказываний, а рассматривать некий абстрактный конечный полный список таких высказываний. За выводы стоять насмерть не берусь (сделано всё на коленке), но подход, возможно, представляет интерес.

Был.