Falcão (falcao) wrote,
Falcão
falcao

"универсальная логическая машина" и теоремы Гёделя (продолжение)

Итак, вспомним, что нам говорит теорема Гёделя о неполноте в одной из возможных формулировок? Она гласит, что всякая формальная аксиоматическая теория неполна при условии, что она является непротиворечивой и "достаточно сильной" (то есть "содержит" формальную арифметику). Для начала прокомментируем формулировку.

Задание формальной аксиоматической теории (или "системы") предполагает, что мы работаем с формулами, то есть строго определёнными последовательностями знаков с использованием логических символов. Для каждой формулы имеется формула, являющаяся отрицанием предыдущей. Для формулы F мы обозначим отрицание последней через ~F. Далее, нам известны аксиомы и правила вывода этой теории. Аксиомы должны быть явно заданы (это обстоятельство очень важно), то есть их должно быть либо конечное число, либо, на худой конец, даже бесконечное, но аксиомы должны распознаваться среди других формул чисто механически (при помощи компьютерной программы, алгоритма). Полезно прямо сейчас представить себе, что означал бы отказ от этого условия. Фактически это значило бы, что мы допускаем существование Божественного Оракула, которому уже открылась Истина, и он может в силу этого объявить аксиомами просто все истинные положения. Ясно, что при такой "халяве" не будет никакой "неполноты", да и вообще никаких проблем. Оракул по определению знает всё.

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

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

Что такое доказуемое утверждение или теорема нашей теории? Это такое утверждение, которое можно вывести из аксиом по правилам вывода, то есть такое, для которого существует формальный вывод, последняя из формул которого совпадает с рассматриваемым утверждением. Заметим, что при таком подходе каждая из аксиом автоматически является теоремой -- доказательство состоит просто из её предъявления, выписывания. Это несколько противоречит обиходному представлению о том, что аксиомы -- это положения, которые принимаются без доказательства. На самом деле это вообще-то так и есть, потому что список аксиом мы "приняли" в самом начале, когда ещё никакого представления о доказательстве у нас не было. Но! Это обстоятельство не мешает нам впоследствии ДОКАЗАТЬ аксиому. Разумеется, это "доказательство" тривиально, и практического смысла в нём нет. Однако следует наотрез отказаться от глубоко укоренённого в сознании многих предрассудка, что доказывать можно только неочевидные вещи. Это, как мы видели, совершенно не так. Просто не надо здесь путать два значения слова "можно". В одном случае речь идёт о том, что "можно" -- это "разрешено правилами", и тут не может быть сомнений в том, что аксиомы МОЖНО доказывать. В обиходном же смысле слова, "можно" зачастую отождествляется с соответствием каким-то требованиям, в частности, практическим. (И при таком толковании "можно" переходит даже в свою "противоположность" -- "нужно".) Я бы не обращал на это обстоятельство внимания, если бы в такую "модальную ловушку" не попадались всё новые и новые жертвы...

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

У нас речь в формулировке идёт о неполноте теории, поэтому для большей ясности добавим, что теория неполна, если можно предъявить такую замкнутую формулу X, что не выводима ни она, ни её отрицание ~X. Если опять-таки погрузиться в сферу "истинности", то мы можем неполноту интерпретировать так: есть вопросы, на которые эта теория ответа не даёт. Истинно ли Х, ложно ли -- мы этого не можем заключить на основе данной теории. (Это вполне согласуется с обычным представлением о неполноте, например, наших знаний.)

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

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

Итак, формулировка теоремы Гёделя о неполноте теперь у нас имеется. Надо теперь показать, что теорема будет следовать из факта существования алгоритмически неразрешимых проблем. У нас есть пример алгоритмически неразрешимой проблемы -- это проблема остановки.

Выше уже шла речь о том, что утверждение, будто некая программа останавливается, можно перевести на язык арифметики и тем самым сделать формулой нашей теории. Эта формула будет замкнутой, так как мы имеем дело с неким вопросом, допускающим ответ "да" или "нет". Пусть это формула X. В нашей теории, если прелположить, что она полна, выводима в точности одна из формул X или ~X. Мы уже знаем, что можно выписывать все тексты один за другим, проверяя, является ли данный текст доказательством, и если да, то какого именно утверждения. Следовательно, при переборе текстов мы через конечное время обязательно столкнёмся либо с выводом формулы X, либо с выводом формулы ~X. В первом случае наша теория "говорит" о том, что тестируемая программа останавливается, во втором -- что не останавливается. Таким образом, мы имеем некую Программу, претендующую на то, чтобы решить проблему остановки алгоритмически.

Выше было показано, что, располагая Программой, мы можем создать тест T, который Программа не проходит. То есть T это некая программа без параметров, про которую мы можем сказать одно из двух. Либо T останавливается на самом деле, но Программа говорит нам противоположное. Либо T не останавливается, но Программа нам говорит о грядущей остановке T. Мы хотим показать, что отсюда следует наличие противоречия в самой теории. Если мы сможем это сделать, то теорему Гёделя о неполноте можно считать установленной.

Рассмотрим первый случай. Пусть T останавливается. Тогда мы можем её запустить и дождаться остановки. Работе программы соответствует, грубо говоря, некое арифметическое "вычисление", то есть за фактом остановки стоит определённое арифметическое утверждение. Это утверждение доказуемо в арифметике -- доказательство извлекается из хода работы программы. Таким образом, в нашей теории можно доказать утверждение X об остановке программы, коль скоро последняя "на самом деле" останавливается. Но мы сейчас анализируем случай, когда Программа говорит нам о том, что T не останавливается, что выражено в виде доказуемости утверждения ~X. Таким образом, в нашей теории доказуемо и X, и ~X -- теория оказалась противоречивой.

Второй случай чуть посложнее. Здесь Программа говорит нам о том, что программа T останавливается, в то время как "на самом деле" она не останавливается. Как же нам здесь явно "изобличить" Программу? В первом случае это было сделать легко: если программа T останавливается на самом деле, то факт её остановки можно наблюдать в реальности, что является однозначным свидетельством в пользу факта остановки. Но сейчас наша программа T не останавливается. Как же в этом убедиться? Всякому ясно, что мы способны наблюдать факт остановки, но как можно наблюдать факт "безостановочности"? Выход, однако, состоит в следующем. Вспомним, как устроена программа T. С учётом того, что она не останавливается, мы знаем, что в ходе работы программы сначала было выяснено, что Программа вынесла иной вердикт, а затем T вошла в бесконечный цикл. С учётом того, что ход работы программы "транслируется" в арифметическое утвеждение, мы можем из доказуемости в нашей теории утверждения X вывести, что T обязана войти в бесконечный цикл, и тем самым она не остановится. Это приводит к выводу утверждения ~X в нашей теории, что снова даёт противоречие.

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

Итак, мы выяснили связь между теоремой Гёделя и алгоритмически неразрешимыми проблемами. Чтобы завершить тему, добавим к сказанному, что иногда неполноту теории подают в виде существования "истинных", но не доказуемых (в рамках теории) утверждений. При любом разумном подходе к "истинности", если таковой применим, все доказываемые утверждения считаются "истинными". Поскольку из двух утверждений X и ~X ровно одно "истинно", то условие невыводимости обоих утверждений говорит о том, что одно из них будет "истинно", но не доказуемо. Каков конкретный пример? В математике их известно довольно много, и мы не будем излагать эту сторону дела. Ограничимся двумя примерами. В рамках нашего подхода мы обнаружим программу T, которая не останавливается, но соответствующий факт не может быть установлен в рамках теории. Более распространённый пример даёт так называемая вторая теорема Гёделя о неполноте. При тех условиях на формальную теорию, что и выше, оказывается возможным выразить на языке арифметики утверждение о непротиворечивости нашей теории. Это утверждение оказывается "истинным", но оно недоказуемо в рамках теории. В общем виде вторая теорема Гёделя о неполноте утверждает, что если формальная теория непротиворечива и "достаточно сильна", то в рамках этой теории невозможно установить её собственную непротиворечивость.

Естественной может показаться попытка расширения аксиоматики при столкновении с "истинным", но не доказуемым в теории утверждением. Можно рассуждать так. Пусть имеется теория T_1. Она неполна. Мы видим, что утверждение X_1 "истинно", но в теории T_1 не доказуемо. Мы говорим: прекрасно, а кто нам мешает принять X_1 за аксиому, раз это истинное утверждение? Идя по такому пути, мы расширяем список аксиом теории T_1 за счёт новой аксиомы X_1 и получаем теорию T_2. Но трудности никуда не исчезли: новая теория по-прежнему непротиворечива и "сильна". То есть это приводит к необходимости принятия новой аксиомы X_2 и так далее. В конце процесса мы примем все новые аксиомы X_1, X_2, ..., получая какую-то очередную теорию. Но и она оказывается неполной по всё тем же причинам! Из этой "дурной бесконечности" выхода нет.

Я сейчас не буду анализировать разного рода философские аспекты этой проблематики, хотя такое обсуждение в комментах считаю вполне уместным.
Tags: математика
Subscribe
Comments for this post were disabled by the author