ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда.

Алгоритм разрешения.

Работая над этой головоломкой, вы, вероятно, заметили, что она включает правила двух противоположных типов удлиняющие и укорачивающие. Два правила (I и II) позволяют нам удлинять строчки (естественно, лишь строго определенным образом), два других правила позволяют укорачивать строчки (опять же, следуя строгому закону). Кажется, что порядок применения этих правил можно бесконечно варьировать; таким образом, возникает надежда, что рано или поздно мы придем к искомой строчке MU. Возможно, нам придется создать для этого гигантскую строчку и затем сокращать ее, пока не останутся только два символа; или, того хуже, нам придется попеременно удлинять и сокращать, удлинять и сокращать, и так далее. При этом успех не гарантирован. На самом деле, мы уже заметили, что получить U вообще невозможно, даже если бы мы удлиняли и сокращали строчки до второго пришествия.

Тем не менее, кажется, что с MU ситуация иная, чем с U. Наше заключение о том, что U вывести невозможно, основывалось на очевидном свойстве этой строчки она не начинается с M, как все остальные теоремы. Иметь такой простой способ отличать не-теоремы весьма удобно. Однако кто может поручиться, что подобный способ укажет нам все не-теоремы? Вполне возможно, что существует множество начинающихся с M строчек, которые, тем не менее, невыводимы. Это означало бы, что проверка «по первой букве» указывает нам только на ограниченное количество не-теорем, оставляя «за бортом» все остальные. Однако существует возможность найти некий более сложный метод проверки, точно говорящий нам, какие строчки могут быть выведены с помощью данных правил, а какие — нет. Тут перед нами возникает вопрос: что мы подразумеваем под словом «проверка»? Читателю может быть не совсем понятно, какой смысл задаваться этим вопросом и почему он столь важен в данном контексте. Приведу пример такой «проверки», которая, как кажется, идет вразрез с самим смыслом этого слова.

Представьте себе джинна, в распоряжении которого имеется все время на свете. Джинн тратит это время на вывод теорем системы MIU. Делает он это весьма методично, скажем, следующим образом:

Шаг 1: Приложить все подходящие правила к аксиоме MI. Это дает две новые теоремы: MIU, MII.

Шаг 2: Приложить все подходящие правила к теоремам, полученным в шаге 1. Это дает три новые теоремы: MIIU, MIUIU, MIIII.

Шаг 3: Приложить все подходящие правила к теоремам, полученным в шаге 2. Это дает пять новых теорем: MUIIIIU, MIIUIIU, MIUIUIUIU, МIIIIIIII, MUI.

.

.

.

Следуя этому методу, рано или поздно мы выведем каждую теорему системы, так как правила применяются во всех мыслимых комбинациях. (См. рис. 11) Все удлиняющие и укорачивающие трансформации, упомянутые выше, со временем будут осуществлены.

Рис. 11. Систематически построенное «дерево» всех теорем системы MIU. N-ный уровень внизу содержит теоремы, для вывода которых понадобилось ровно N шагов. Номера в кружках говорят нам, с помощью какого правила была получена данная теорема. Растет ли на этом дереве MU?

Неясно, однако, как долго нам придется ждать появления той или иной строчки, поскольку теоремы расположены согласно длине их вывода. Это не очень-то полезное расположение, в особенности, если вы заинтересованы в какой-то определенной строчке (например, MU) и при этом не знаете не только того, какой длины ее вывод, но даже того, существует ли этот вывод вообще. Теперь давайте взглянем на обещанную «проверку теоремности»:

Ждите, пока данная строчка будет выведена; когда это случится, вы будете знать, что это — теорема. Если же этого не случится никогда, вы можете быть уверены, что данная строчка — не теорема.

Это звучит нелепо, так как здесь имеется в виду, что мы согласны ждать ответа до скончания веков. Таким образом, мы опять подошли к вопросу о том, что может считаться «проверкой». Прежде всего, нам необходима гарантия, что мы получим ответ за ограниченный промежуток времени. Такая проверка теоремности, которая завершается в конечный отрезок времени, называется алгоритмом разрешения для данной формальной системы.

Когда у вас имеется алгоритм разрешения, все теоремы системы приобретают конкретную характеристику. С первого взгляда может показаться, что правила и аксиомы формальной системы сами по себе характеризуют ее теоремы не менее полно, чем алгоритм разрешения; однако проблема здесь заключается в слове «характеризуют». Безусловно, как правила вывода, так и аксиомы системы MIU косвенно характеризуют строчки, являющиеся теоремами; еще более косвенно они характеризуют строчки, теоремами не являющиеся. Однако косвенная характеристика часто недостаточна. Если кто-нибудь утверждает, что он имеет в своем распоряжении характеристику всех теорем, но при этом тратит бесконечное время, чтобы установить, что данная строчка не является теоремой, вы, скорее всего, подумаете, что в его характеристике чего-то не хватает — она недостаточно конкретна. Именно поэтому так важно установить, есть ли в данной системе алгоритм разрешения. Положительный ответ будет означать, что вы всегда можете проверить, является ли данная строчка теоремой; при этом, какой бы длинной проверка ни была, она непременно придет к концу. В принципе, проверка — такой же простой, механический, конечный и верный процесс, как установление того, что первая буква строчки — M. Алгоритм разрешения — это «лакмусовая бумажка» для установления теоремности!

Кстати, одним из требований формальной системы является наличие алгоритма разрешения для аксиом: каждая формальная система должна иметь свою Лакмусовую бумажку для определения аксиомности. Таким образом, у нас не будет проблем по крайней мере в начале работы. Разница между множеством аксиом и множеством теорем в том, что первые всегда имеют алгоритм разрешения, в то время как последние могут его и не иметь.

Уверен, что вы согласитесь, что, когда вы начали работать с системой MIU, вам пришлось столкнуться именно с этой проблемой. Вам была известна единственная аксиома системы и простые правила вывода, косвенно характеризующие теоремы — и все же было неясно, каковы последствия этой характеристики. В частности, было совершенно непонятно, является ли MU теоремой.

Рис. 12. М. К. Эшер. «Воздушный замок» (гравюра на дереве), 1928.