О формально неразрешимых предложениях

«О ФОРМАЛЬНО НЕРАЗРЕШИМЫХ ПРЕДЛОЖЕНИЯХ» — классическая работа К. Геделя (Godel К. Uber formal unentscheidbare Satze der Principia Mathemati-ca und verwandter Systeme, I // Monatshefte fur Mathematik und. Physik. 1931. Bd. 38. S. 173—198; (англ. пер.: Van Heijenoort J. (ed.) From Frege to Godel: A Sourcebook in Mathematical Logic, 1879—1931. Cambridge, MA: Harvard Univ. Press, 1967), центральным результатом которой является теорема о неполноте. Это одно из принципиальных достижений логики 20 в., явившихся интеллектуальным вызовом современной цивилизации. Содержание работы сводится не к единственной теореме. Гедель впервые в практике исследований последовательно провел в этой работе метод кодирования выражений логического языка натуральными числами, с тем чтобы в дальнейшем говорить о них внутри формальной теории, которая сама по себе не содержит обозначений для термов, формуЛит.п. как ее внутренних объектов. В этом смысле можно считать, что данная работа открыла тематику представления данных, которая приобрела актуальность в ходе развития информатики. Известно, что сейчас 70% успеха при решении сложной информационной задачи зависит от удачного представления данных.         Стоит разобрать подробнее способы представления данных у Геделя. Прежде всего, Гедель, не довольствуясь абстрактным результатом Кантора о том, что кортежи натуральных чисел можно занумеровать натуральными числами, построил их кодировку, исключительно просто выражающуюся в формальной арифметике. Это необходимо, поскольку при переводе на арифметический язык утверждений о доказательствах и формулах часто появляется необходимость говорить о произвольных конечных последовательностях чисел. Поскольку любое фиксированное конечное число кванторов не выводит за пределы арифметического языка, оказалось достаточно кодировать последовательности чисел не числами, а их парами. Далее, поскольку здесь важнее всего простота, Гедель смело отказался от однозначности кодировки.         Геделевская функция |3(c,d,i) = rm(c,S(d,i)), где rm — функция нахождения остатка, a 5(d,i) = l+(i+l)d, кодирует последовательности натуральных чисел парами чисел в следующем смысле. Для любой конечной последовательности натуральных чисел длины п найдутся такие ч и с л а e n d, что первые п значений ( 3 ( c, d, i ) дадут данную последовательность.         Для кодирования самих формул понадобилась менее элементарная, но значительно более строгая система кодов. Здесь необходимо, чтобы код формулы однозначно разлагался на коды составляющих и, наоборот, из кодов составляющих можно было получить код формулы. Идея геделевского кодирования следующая. Символы нумеруются ненулевыми числами. Код выражения, состоящего из символов аг..а, есть PjA а -...-р ла. Символ Л обозначает здесь возведение в степень, р. — соответствующее простое число.         Далее Гедель воспользовался диагональным методом Кантора и построил формулу, которая выражает собственную недоказуемость. При этом оказалось существенным различать выразимость в смысле истинности на модели и выразимость в смысле доказуемости формул. Предикат Р выразим в формальной системе, если для него можно записать формулу А, которая удовлетворяет двум условиям. Первое из них неформализуе-мое и требует, чтобы смысл записанной формулы в стандартной модели соответствовал смыслу представляемого ею предиката. Второе чисто формальное. А(п) должно быть доказуемо тогда и только тогда, когда истинно Р(п), ->А(п) должно быть доказуемо тогда и только тогда, когда ложно Р(п). В этом определении неявно содержится предположение о непротиворечивости формальной системы, и Гедель снял его, потребовав импликаций лишь в одну сторону: если предикат истинен, формула доказуема. Если он ложен, доказуемо ее отрицание.         Понятие того, что конструкция является доказательством формулы в формальной арифметике, оказалось выразимо в формальной системе арифметики. Тем самым (если провести аналогию, которую сам Гедель не проводил) понятие доказуемости оказывается рудиментом понятия истинности, по А. Тарскому; и, согласно теореме Тарского о невыразимости истины, не может быть полной формальной системы арифметики.         В дальнейшем Россер усилил методы Геделя, и стало ясно, что теорема неполноты относится к числу исключительно устойчивых математических результатов, которые никак не обойдешь.         Отношение к теореме Геделя о неполноте в значительной степени предопределило развитие эпистемологии, методологии математики и точных наук вообще. Те, кто исповедуют квазирелигию прогресса, долго пытались игнорировать ее, как касающуюся тех формул, которые не встречаются на практике, пока не было показано, что соответствующие эффекты возникают и для практических формул. Те, кто исповедуют квазирелигию мистицизма, использовали ее в качестве аргумента адвоката дьявола против рационального мышления. Положительных примеров ее использования маловато (пожалуй, лишь нестандартный анализ и теория неформализуемых понятий). Таким образом, теорема Геделя о неполноте ярко выявила симптомы тяжелой духовной болезни нынешнего общества: закрывание глаз на неприятные факты либо демагогическое их использование, если они касаются противников.         Но в работе Геделя есть еще одна классическая теорема (так называемая третья теорема Геделя). Ее доказательство явилось первым применением метода рефлексии. Гедель проследил, что его доказательство теоремы неполноты проводится в арифметике с добавленной аксиомой о непротиворечивости формальной арифметики. Таким образом, если бы удалось доказать непротиворечивость арифметики внутри самой арифметики, то была бы доказана и недоказуемая формула Геделя. Эта теорема показала, что конкретный способ реализации программы Д. Гильберта, предложенный самим Гильбертом, оказался несостоятельным. Она была ошибочно истолкована как провал самой программы (несмотря на возражения по этому поводу Л. Брауэра — самого принципиального критика Д. Гильберта).         Эта теорема интересна еще и тем, что она, в отличие от теоремы о неполноте, не так устойчива. Кодировка формул, при которой ее удается обойти, чуть-чуть ока-рикатуренно может быть описана следующим образом. Если формула А доказуема, закодируем ее конъюнкцией A&.-.&iA, где А повторена столько раз, какова длина ее доказательства. Если А не доказуема, закодируем ее самой А.         Таким образом, в своей классической работе К. Гедель заложил основы важнейших методов современной информатики, поставил исключительно важные методологические проблемы, которые не потеряли актуальности и до сих пор и очень далеки от разрешения.         Н.Н. Непейвода         Лит.: Клини С.К. Введение в метаматематику. М., 195 7.