В этой и следующей главах мы рассмотрим несколько новых формальных систем; это поможет нам лучше понять саму идею формальной системы. Когда вы дочитаете эти две главы до конца, у вас должно сложиться неплохое представление о мощности формальных систем и о том, почему они представляют интерес для математиков и логиков.
Система «pr»
В этой главе мы будем рассматривать систему pr. Ни математики, ни физики ею не заинтересуются; признаться, она — всего лишь мое собственное изобретение. Система pr интересна лишь постольку, поскольку она хорошо иллюстрирует многие идеи, играющие в этой книге важную роль. В этой системе три символа:
p r - — буквы p и r и тире.
Система pr имеет бесконечное множество аксиом. Поскольку мы не можем записать их все, мы должны придумать какой-нибудь метод их описания. На самом деле, нам нужно не просто описание этих аксиом; нам нужен способ, позволяющий узнать, является ли данная последовательность символов аксиомой. Простое описание аксиом охарактеризовало бы их полностью, но недостаточно сильно; именно в этом была проблема с описанием теорем системы MIU.
Мы не собираемся возиться в течении неопределенного — возможно, бесконечного — времени, чтобы определить, является ли некая строчка символов аксиомой. Нам необходимо такое определение аксиом, которое предоставит в наше распоряжение надежный алгоритм разрешения, устанавливающий аксиоматичность любой строчки, состоящей из символов p, r и тире.
ОПРЕДЕЛЕНИЕ: xp-rx- является аксиомой, когда x состоит только из тире.
Обратите внимание, что каждый из этих двух x-ов замещает одинаковое число тире. Например, --p-r--- является аксиомой. Само выражение xp-rx-, разумеется, не аксиома, так как x не принадлежит системе pr; оно, скорее, походит на форму, в которой отливаются все аксиомы данной системы. Такая «форма» называется схемой аксиом.
Система pr имеет только одно правило вывода:
ПРАВИЛО: Пусть x, у и z — строчки, состоящие только из тире. Пусть xpyrz является теоремой. Тогда xpy-rz- также будет теоремой.
Пусть, например, x будет «--», у — «---» и z — «-». Правило говорит нам:
Если --p---r- является теоремой, то --p----r-- также будет теоремой.
Это утверждение типично для правил вывода: оно устанавливает связь между двумя строчками, не сообщая нам ничего о том, является ли каждая из них по отдельности теоремой.
Очень полезное упражнение — попытаться найти разрешающий алгоритм для теорем системы pr. Это нетрудно — после нескольких попыток вы, скорее всего, найдете решение. Попробуйте!
Разрешающий алгоритм
Надеюсь, что вы уже попытались найти решение. Во-первых, хотя это и кажется очевидным, я хотел бы заметить, что каждая теорема системы pr имеет три отдельных группы тире, и что разделяющими элементами являются p и r, именно в таком порядке. (Это можно доказать, основываясь на аргументах «наследственности», так же, как мы смогли доказать, что теоремы системы MIU всегда должны начинаться с М.) Это означает, что уже сама форма такой строчки как --p--p--p--r-------- исключает ее из числа теорем.
Читатель может подумать, что, подчеркивая фразу «уже сама форма», автор поступает довольно глупо: что еще может быть в такой строчке, кроме формы? Что, кроме ее формы, может играть какую-либо роль в определении особенностей данной строчки? Совершенно ясно, что ничего больше! Однако имейте в виду, читатель, что по мере того, как мы будем углубляться в обсуждение формальных систем, понятие «формы» будет становиться все сложнее и абстрактнее и нам придется все чаще задумываться о значении самого этого слова. Во всяком случае, мы будем называть «правильно составленной строчкой» любую строчку следующей структуры: группа тире, одно p, вторая группа тире, одно r, завершающая группа тире.
Вернемся к алгоритму разрешения. Для того, чтобы данная строчка считалась теоремой, первые две группы тире в сумме должны давать третью группу тире. Так, например, --p--r---- является теоремой, так как 2 плюс 2 равняется 4, в то время как --p--r- теоремой не является, так как 2 плюс 2 не равняется 1. Чтобы понять, почему этот критерий верен, взгляните сначала на схему аксиом. Очевидно, она производит только такие аксиомы, которые удовлетворяют критерию сложения. Теперь обратитесь к правилу вывода. Если первая строчка удовлетворяет критерию сложения, то же условие необходимо будет выполняться и во второй строчке. И, наоборот, если первая строчка не удовлетворяет критерию сложения, не будет удовлетворять ему и вторая строчка. Это правило превращает критерий сложения в наследственное качество теорем; каждая теорема передает его своим «отпрыскам». Это показывает, почему критерий сложения верен.
Кстати, в системе pr есть некое свойство, позволяющее нам с уверенностью сказать, что данная система имеет разрешающий алгоритм, еще до того, как мы нашли критерий сложения. Это свойство заключается в том, что система pr не усложнена встречными укорачивающими и удлиняющими правилами; в ней имеются лишь удлиняющие правила. Любая формальная система, которая говорит нам, как получать более длинные теоремы из более коротких, но никогда не говорит нам обратного, должна иметь алгоритм разрешения для своих теорем. Представьте себе, что вам дана какая-либо строчка. Прежде всего, проверьте, является ли эта строчка аксиомой (я предполагаю, что у нас имеется алгоритм разрешения для аксиом, иначе наше предприятие было бы безнадежным). Если это аксиома, то, следовательно, по определению она является теоремой, и проверка на этом заканчивается. Предположим теперь, что наша строчка — не аксиома. В таком случае, чтобы быть теоремой, она должна была быть получена из более короткой строчки путем применения одного из правил. Перебирая правила одно за другим, вы всегда можете установить, какие из них были использованы для получения данной строчки, а также какие более короткие строчки предшествуют ей на «генеалогическом древе». Таким образом, проблема сводится к определению того, какие из новых, более коротких строчек являются теоремами. Каждая из них, в свою очередь, может быть подвергнута такой же проверке. В худшем случае, нам придется проверить огромное количество все более коротких строчек. Продолжая продвигаться таким образом назад, вы медленно, но верно приближаетесь к источнику всех теорем: схеме аксиом. Строчки не могут укорачиваться бесконечно; в один прекрасный момент вы либо установите, что одна из новых коротеньких строчек является аксиомой, либо застрянете на строчках, которые, не являясь аксиомами, тем не менее, не поддаются дальнейшему сокращению. Таким образом, системы, имеющие лишь удлиняющие правила, не особенно интересны; по-настоящему любопытны лишь системы, где взаимодействуют удлиняющие и укорачивающие правила.
Снизу вверх
vs. сверху вниз
Метод, описанный выше, можно назвать нисходящим алгоритмом разрешения; сравним его с восходящим алгоритмом, описание которого я сейчас приведу. Он весьма напоминает метод, используемый джинном для производства теорем в системе MIU; однако он несколько осложнен присутствием схемы аксиом. Мы возьмем что-то вроде корзины, куда будем бросать теоремы по мере их рождения.
(1а) Бросьте в корзину самую простую (-p-r--) из возможных теорем.
(1б) Приложите правило вывода к предмету в корзине и положите в корзину результат.
(2а) Положите в корзину следующую по простоте аксиому.
(2б) Приложите правило в каждому имеющемуся в корзине предмету и бросьте в корзину результаты.
(За) Положите третью по простоте аксиому в корзину.
(3б) Приложите правило к каждому имеющемуся в корзине предмету и бросьте в корзину результаты.
И т. д. и т. п.
Ясно, что, действуя таким образом, вы не можете пропустить не одной теоремы системы pr. С течением времени корзина будет наполняться все более длинными теоремами; это — следствие отсутствия сокращающих правил Таким образом, если вы желаете проверить, является ли данная строчка (например, --p---r-----) теоремой, вам придется следуя шаг за шагом, бросать в корзину все новые теоремы и сравнивать их с данной строчкой. Если таковая обнаружится, значит, это — теорема. Если же в какой-то момент вы заметите, что все, что попадает в корзину, длиннее искомой строчки, можете прекратить поиски — это не теорема. Такой разрешающий алгоритм называется восходящим, так как он исходит из основы, фундамента системы — аксиом. Предыдущий алгоритм разрешения, наоборот, спускался сверху, приближаясь к фундаменту системы.
