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

(прим. символ «э» заменяет символ импликации «superset of»)

 Первое правило нашей системы таково:

ПРАВИЛО ОБЪЕДИНЕНИЯ: Если x и у — теоремы системы, то строчка <x y> — тоже теорема.

Это правило соединяет две теоремы в одну. Оно должно напомнить вам о предыдущем Диалоге.

Правильно сформированные строчки

У нас будет еще несколько правил вывода; вскоре я их объясню. Однако сначала необходимо определить некое подмножество всех строчек, а именно — правильно сформированные строчки. Они будут определены рекурсивным путем, начиная с атомов. АТОМЫ: P, Q, и R называются атомами. Новые атомы получаются путем добавления штрихов справа от старых атомов, таким образом, получаются R', Q'', R''' и т. д. Это дает нам бесконечные ресурсы атомов. Все атомы правильно сформированы.

Далее, у нас имеются четыре рекурсивных правила.

ПРАВИЛА ОБРАЗОВАНИЯ: Если x и у правильно сформированы, то следующие четыре строчки также правильно сформированы.

(1) ~x

(2) <x y>

(3) <x V y>

(4) <x э y>

Например, все следующие строчки правильны:

P атом

~P по правилу (1)

~~P по правилу (1)

Q' атом

~Q' по правилу (1)

<P ~Q'> по правилу (2)

~<P~Q'> по правилу (1)

<~~P э Q'> по правилу (4)

<~<P ~Q'>V<~~P э Q'>> по правилу (3)

Последняя строчка может показаться весьма сложной, но на самом деле, она построена всего лишь из двух компонентов — двух предыдущих строчек. Каждая из них, в свою очередь, построена из предыдущих строчек… и так далее. Происхождение любой правильно сформированной строчки может быть прослежено до ее элементарных составляющих — атомов. Для этого вы просто применяете правила в обратном порядке до тех пор, пока это возможно. Этот процесс рано или поздно должен кончиться, поскольку каждое правило вывода — удлиняющее правило; идя в обратном порядке, мы непременно дойдем до атомов.

Таким образом, метод разложения строчек служит проверкой их правильности. Это — нисходящая процедура разрешения для правильно-сформированности. Можете проверить, как вы поняли эту процедуру, найдя, какие из ниже приведенных строчек правильно сформированы:

(1) <P>

(2) <~P>

(3) <P Q R>

(4) <P Q>

(5) <<P Q><Q~  P>>

(6) <P ~P>

(7) <<P V<Q э R>><~P V ~R'>>

(8) <P Q><Q P>

(Ответ. Те строчки, номера которых являются числами Фибоначчи, сформированы неправильно; остальные — правильно.)

Еще правила вывода

Сейчас мы познакомимся с остальными правилами вывода, при помощи которых строятся теоремы системы. Во всех этих правилах символы «x» и «y» всегда относятся к правильно сформированным строчкам.

ПРАВИЛО РАЗДЕЛЕНИЯ: Если <x y> — теорема, то и x и у — также теоремы.

Вероятно, вы уже догадались, что значит символ «». (Подсказка: это то самое слово, что причинило столько проблем в Диалоге.) Из следующего правила вы сможете вывести значение тильды («~»):

ПРАВИЛО ДВОЙНОЙ ТИЛЬДЫ: Строчка «~~» может быть выброшена из любой теоремы. Она также может быть вставлена в любую теорему, если при этом получается правильно сформированная строчка.

Правило фантазии

Эта система отличается тем, что в ней нет аксиом — одни лишь правила. Вспомнив наши предыдущие формальные системы, вы можете спросить: как же здесь могут вообще существовать теоремы? Откуда они появляются? Ответом является правило, фабрикующее теоремы «из воздуха» — оно не требует ввода «старых теорем». (Остальные правила, наоборот, нуждаются во вводных данных.) Это правило называется «правилом фантазии.» Почему я его так окрестил? Ответ прост.

Чтобы использовать это правило, вы должны записать любую приглянувшуюся вам правильно сформированную строчку x, и затем спросить себя: что бы произошло, если строчка x действительно оказалась бы аксиомой или теоремой? После чего вы предлагаете системе ответить на этот вопрос; это значит, что вы начинаете вывод, используя x как первую строчку. Пусть у будет последней строчкой. От x до у включительно все является фантазией; x — посылка фантазии, а у — ее результат. Следующий шаг — выход из области фантазии; мы узнали, что

Если бы x являлось теоремой, то у также являлось бы теоремой.

Вы можете спросить: «Где же здесь настоящая теорема?» Это строчка:

<x э y>

Обратите внимание на то, как эта строчка напоминает предложение, напечатанное выше.

Чтобы отметить вход и выход в область фантазии, мы будем использовать квадратные скобки «[» и «]», соответственно. Таким образом, увидев левую квадратную скобку, вы будете знать, что вы «проталкиваетесь» в область фантазии, и следующая строчка будет посылкой. Увидев правую квадратную скобку, вы будете знать, что вы «выталкиваетесь» обратно из воображаемого мира, и что предыдущая строчка была результатом. Удобно (хотя и не необходимо) начинать те строчки вывода, что относятся к области фантазии, с нового абзаца.