Шаг 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.
Двухголосная инвенция
или Что Черепаха сказала Ахиллу (записано Льюисом Кэрроллом)[8]
Ахилл перегнал Черепаху и с комфортом уселся отдыхать на ее широкой спине.
«Так вам все же удалось добежать до финиша?» — сказала Черепаха. «Несмотря на то, что дистанция состояла из бесконечного ряда отрезков? Я-то думала, какой-то умник доказал, что это невозможно сделать?»
«Это ВОЗМОЖНО сделать», — сказал Ахилл: «И я это СДЕЛАЛ! Solvitur ambulando. Видите ли, дистанции постоянно УМЕНЬШАЛИСЬ…»
«А если бы они постоянно УВЕЛИЧИВАЛИСЬ?» — перебила Черепаха, — «Что тогда?»
«Тогда бы меня здесь еще не было,» — скромно ответил Ахилл, — «А Вы уже успели бы обежать несколько раз вокруг света.»
«Вы весьма великодушны, Ахилл. Вы меня просто подавили… я хочу сказать, придавили, поскольку вы нешуточный тяжеловес. А теперь, не угодно ли вам послушать про такую беговую дорожку, о которой большинство людей воображают, что могут преодолеть ее в два-три шага, когда на самом деле она состоит из бесконечного числа расстояний, где каждое последующее больше предыдущего?»
«С превеликим удовольствием,» — ответствовал греческий воин, доставая из шлема (в те дни мало кто из греческих воинов мог похвастаться карманами) огромный блокнот с карандашом. «Приступайте к своему рассказу, да говорите, пожалуйста, помедленнее — ведь стенография еще не изобретена!»
«Этот прекрасный Первый Постулат Эвклида…» — пробормотала мечтательно Черепаха, — «вы восхищаетесь Эвклидом?»
«Страстно! Постольку, конечно, поскольку можно восхищаться трудом, который будет опубликован лишь через несколько столетий…»
«Давайте, в таком случае, рассмотрим первые два пункта его доводов, и выводы, которые из них следуют. Будьте так любезны, запишите их к себе в блокнот — для удобства обозначим их А, В и Z:
(A) Вещи, равные одному и тому же, равны между собой.
(B) Две стороны этого треугольника суть вещи, равные одному и тому же.
(Z) Две стороны этого треугольника равны между собой.
Читатели Эвклида согласятся, я думаю, что Z логически следует из А и В, так что тот, кто согласен с истинностью А и В, ДОЛЖЕН считать истинным и Z?»
«Несомненно! Уж с ЭТИМ-то легко согласится любой старшеклассник — как только старшие классы будут изобретены, каких-нибудь пару тысяч лет спустя.»
«И если какой-нибудь читатель не принимает А и В за истинные, он, тем не менее, должен согласиться с тем, что ВЗЯТАЯ ЦЕЛИКОМ, эта последовательность имеет смысл?»
«Без сомнения, такого читателя можно вообразить. Он мог бы сказать: „Я принимаю за истинное Гипотетическое Утверждение, что ЕСЛИ А и В истинны, то Z должно быть тоже истинно.“ Такой читатель поступил бы мудро, если бы он оставил Эвклида и занялся футболом».
«А что, если какой-нибудь другой читатель сказал бы: „Я принимаю за истинные А и В, но НЕ Гипотетическое Утверждение“?»
«Наверное, и такой читатель мог бы существовать. Ему, впрочем, тоже было бы лучше заняться футболом.»
«И никакой из этих читателей ПОКА не обязан соглашаться с тем, что логически Z должно быть истинно?»
«Совершенно верно,» — кивнул Ахилл.
«Теперь представьте на минуту, что я — тот второй читатель, и попробуйте логически заставить меня признать, что Z истинно.»
«Черепаха, играющая в футбол, была бы…» — начал Ахилл.
«… совершеннейшей аномалией, конечно,» — торопливо перебила Черепаха. «Не будем отвлекаться; сначала давайте разберемся с Z, а потом уж поговорим о футболе!»
«Я должен заставить вас принять Z, не так ли?» — задумчиво пробормотал Ахилл. «И вы утверждаете, что принимаете А и В, но тем не менее не принимаете Гипотетическое Утверждение…»
«Назовем его С», — вставила Черепаха.
«Но вы не принимаете
(С) Если А и В истинны, следовательно Z должно быть истинно.»
8
Lewis Carroll «What the Tortoise Said to Achilles» в журнале «Mind» n s 4 1895) стр. 255 6