Кстати, в системе pr есть некое свойство, позволяющее нам с уверенностью сказать, что данная система имеет разрешающий алгоритм, еще до того, как мы нашли критерий сложения. Это свойство заключается в том, что система pr не усложнена встречными укорачивающими и удлиняющими правилами; в ней имеются лишь удлиняющие правила. Любая формальная система, которая говорит нам, как получать более длинные теоремы из более коротких, но никогда не говорит нам обратного, должна иметь алгоритм разрешения для своих теорем. Представьте себе, что вам дана какая-либо строчка. Прежде всего, проверьте, является ли эта строчка аксиомой (я предполагаю, что у нас имеется алгоритм разрешения для аксиом, иначе наше предприятие было бы безнадежным). Если это аксиома, то, следовательно, по определению она является теоремой, и проверка на этом заканчивается. Предположим теперь, что наша строчка — не аксиома. В таком случае, чтобы быть теоремой, она должна была быть получена из более короткой строчки путем применения одного из правил. Перебирая правила одно за другим, вы всегда можете установить, какие из них были использованы для получения данной строчки, а также какие более короткие строчки предшествуют ей на «генеалогическом древе». Таким образом, проблема сводится к определению того, какие из новых, более коротких строчек являются теоремами. Каждая из них, в свою очередь, может быть подвергнута такой же проверке. В худшем случае, нам придется проверить огромное количество все более коротких строчек. Продолжая продвигаться таким образом назад, вы медленно, но верно приближаетесь к источнику всех теорем: схеме аксиом. Строчки не могут укорачиваться бесконечно; в один прекрасный момент вы либо установите, что одна из новых коротеньких строчек является аксиомой, либо застрянете на строчках, которые, не являясь аксиомами, тем не менее, не поддаются дальнейшему сокращению. Таким образом, системы, имеющие лишь удлиняющие правила, не особенно интересны; по-настоящему любопытны лишь системы, где взаимодействуют удлиняющие и укорачивающие правила.
Снизу вверх vs. сверху вниз
Метод, описанный выше, можно назвать нисходящим алгоритмом разрешения; сравним его с восходящим алгоритмом, описание которого я сейчас приведу. Он весьма напоминает метод, используемый джинном для производства теорем в системе MIU; однако он несколько осложнен присутствием схемы аксиом. Мы возьмем что-то вроде корзины, куда будем бросать теоремы по мере их рождения.
(1а) Бросьте в корзину самую простую (-p-r--) из возможных теорем.
(1б) Приложите правило вывода к предмету в корзине и положите в корзину результат.
(2а) Положите в корзину следующую по простоте аксиому.
(2б) Приложите правило в каждому имеющемуся в корзине предмету и бросьте в корзину результаты.
(За) Положите третью по простоте аксиому в корзину.
(3б) Приложите правило к каждому имеющемуся в корзине предмету и бросьте в корзину результаты.
И т. д. и т. п.
Ясно, что, действуя таким образом, вы не можете пропустить не одной теоремы системы pr. С течением времени корзина будет наполняться все более длинными теоремами; это — следствие отсутствия сокращающих правил Таким образом, если вы желаете проверить, является ли данная строчка (например, --p---r-----) теоремой, вам придется следуя шаг за шагом, бросать в корзину все новые теоремы и сравнивать их с данной строчкой. Если таковая обнаружится, значит, это — теорема. Если же в какой-то момент вы заметите, что все, что попадает в корзину, длиннее искомой строчки, можете прекратить поиски — это не теорема. Такой разрешающий алгоритм называется восходящим, так как он исходит из основы, фундамента системы — аксиом. Предыдущий алгоритм разрешения, наоборот, спускался сверху, приближаясь к фундаменту системы.
Изоморфизмы порождают смысл
Теперь мы подошли к центральному вопросу данной главы — и книги в целом. Возможно, у вас уже мелькнула мысль, что теоремы pr напоминают сложение. Строчка --p--r---- является теоремой, потому что 2 плюс 3 равняется 5. Может быть, вы даже подумали, что теорема --p---r----- не что иное как записанное необычной нотацией утверждение, означающее, что 2 плюс 3 равняется 5. На самом деле я нарочно выбрал буквы p и r, чтобы напомнить вам о словах «плюс» и «равняется». Так что же, строчка --p---r----- на самом деле означает 2 плюс 3 равняется 5?
Что заставляет нас думать подобным образом? Мне кажется, что в этом виноват замеченный нами изоморфизм между системой pr и сложением. Во введении термин «изоморфизм» был определен как трансформация, сохраняющая информацию Теперь мы можем далее углубиться в это понятие и рассмотреть его в иной перспективе. Слово «изоморфизм» приложимо к тем случаям, когда две сложные структуры могут быть отображены одна в другой таким образом, что каждой части одной структуры соответствует какая-то часть другой структуры («соответствие» здесь означает, что эти части выполняют в своих структурах сходные функции). Такое использование слова «изоморфизм» восходит к более точному математическому понятию.
Обнаружить изоморфизм между двумя известными ему структурами — большая радость для математика. Часто это открытие изумительно и неожиданно, как гром с ясного неба. Осознание изоморфизма между двумя хорошо известными структурами — большой шаг вперед по дороге познания, и я считаю, что именно это порождает значения в человеческом мозгу. Для полноты картины заметим, что поскольку изоморфизмы бывают самых различных типов, иногда не совсем ясно, когда же мы в действительности имеем дело с изоморфизмом. Таким образом, слову «изоморфизм», как и вообще всем словам, присуща некая расплывчатость, что является одновременно и достоинством, и недостатком.
В данном случае, у нас имеется великолепный прототип для понятия «изоморфизм». Во первых, у нас есть «низший уровень» нашего изоморфизма — соответствие между частями двух структур:
p <==> плюс
r <==> равняется
- <==> один
-- <==> два
--- <==> три
и т. д.
Подобное соответствие между словами и символами называется интерпретацией.
Во-вторых, на более высоком уровне, у нас имеется соответствие между истинными утверждениями и теоремами. Заметим, однако, что это соответствие высшего уровня не может быть осознано, пока мы не выберем интерпретации для символов. Исходя из этого, правильнее будет говорить о соответствии между истинными суждениями и интерпретированными теоремами. В любом случае, мы установили соответствие между двумя порядками — нечто типичное для изоморфизма. Когда вы имеете дело с формальной системой, о которой ничего не знаете и в которой желаете найти скрытое значение, ваша задача — интерпретировать символы таким образом, чтобы установить соответствие между истинными высказываниями и теоремами. Возможно, что сначала вам придется искать наугад, прежде чем вы найдете набор слов, подходящий для ассоциации с символами системы. Эта процедура весьма напоминает попытки расшифровать секретный код или прочитать надпись на незнакомом языке, как, например, критский линейный В: единственный возможный путь состоит в использовании метода проб и ошибок, а также «разумных» догадок. Когда вы найдете правильный, «значащий» вариант, внезапно все приобретает смысл, и работа начинает идти во много раз быстрее. Очень скоро все встает на свои места. Счастливое волнение, испытываемое при этом исследователем, хорошо описано Джоном Чадвиком в его книге «Расшифровка линейного языка В» (John Chadwick, The Decipherment of Linear B).
Однако мало кому приходится расшифровывать формальные системы, найденные в раскопках древних цивилизаций. Больше всего с формальными системами имеют дело математики (а в последнее время также лингвисты, философы и некоторые другие ученые); они придерживаются определенной интерпретации в формальных системах, которые они изучают и используют. Эти специалисты пытаются создать такую формальную систему, теоремы которой изоморфно отражали бы какие-либо фрагменты действительности. В этом случае выбор символов так же важен, как выбор типографских правил вывода. Задумав систему pr, я очутился как раз в таком положении. Читателю, вероятно, уже понятно, почему я выбрал именно такие символы. Теоремы системы pr не случайно изоморфны сложению; это получилось потому, что я искал способ представить сложение типографским путем.
