Таким образом, метод разложения строчек служит проверкой их правильности. Это — нисходящая процедура разрешения для правильно-сформированности. Можете проверить, как вы поняли эту процедуру, найдя, какие из ниже приведенных строчек правильно сформированы:
(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>
Обратите внимание на то, как эта строчка напоминает предложение, напечатанное выше.
Чтобы отметить вход и выход в область фантазии, мы будем использовать квадратные скобки «[» и «]», соответственно. Таким образом, увидев левую квадратную скобку, вы будете знать, что вы «проталкиваетесь» в область фантазии, и следующая строчка будет посылкой. Увидев правую квадратную скобку, вы будете знать, что вы «выталкиваетесь» обратно из воображаемого мира, и что предыдущая строчка была результатом. Удобно (хотя и не необходимо) начинать те строчки вывода, что относятся к области фантазии, с нового абзаца.
Ниже приводится иллюстрация правила фантазии в действии. Строчка P служит посылкой. (На самом деле, P не является теоремой, но для нас это не важно — мы просто задаем вопрос «а что, если бы она была теоремой?») Мы воображаем следующее:
[ проталкивание в область фантазии
P посылка
~~P результат (по правилу двойной тильды)
] выталкивание из области фантазии
Наша фантазия показывает, что:
если бы P было теоремой, ~~P также было бы теоремой.
Теперь мы постараемся «затолкать» это высказывание русского языка (метаязык) в рамки формальной нотации (предметный язык): <P э ~~P>. Таким образом, наша первая теорема исчисления высказываний должна подсказать вам интерпретацию символа «э».
Вот еще один пример вывода с помощью правила фантазии:
[ проталкивание в область фантазии
<P Λ Q> посылка
P отделение
Q отделение
<Q Λ P> соединение
] выталкивание из области фантазии
<<P Λ Q>э<Q Λ P>> правило фантазии
Необходимо помнить, что только последняя строчка здесь является настоящей теоремой; все остальное — чистая фантазия.
Рекурсия и правило фантазии
Как вы могли догадаться из рекурсивной терминологии («проталкивание» и «выталкивание»), правило фантазии может быть использовано рекурсивно — так что могут существовать фантазии внутри фантазий, фантазии, вложенные друг в друга три раза, и так далее. Это означает, что для этого правила существуют различные уровни реальности, так же как и во вставленных друг в друга рассказах или фильмах. Когда вы выталкиваетесь из фильма, вставленного внутрь другого фильма, на мгновение вам кажется, что вы достигли реального мира, хотя вас все еще отделяет от него один уровень. Точно так же, когда вы выталкиваетесь из фантазии внутри фантазии, вы находитесь в «более реальном», чем предыдущий, мире, хотя он и отстоит на один уровень от настоящего.
Предупреждение «НЕ КУРИТЬ», висящее в кинотеатре, не относится к актерам, играющим в фильме: реальный мир не проникает в фантастический мир фильмов. Однако в исчислении высказываний существует не только воздействие реального мира на фантазии, но и фантазий на вложенные в них более глубокие фантазии. Это свойство отражено в следующем правиле:
ПРАВИЛО ПЕРЕНОСА: В фантазию можно внести любую теорему из «реальности» одним уровнем выше и использовать ее там.
Это похоже на то, если бы табличка «НЕ КУРИТЬ» относилась не только к зрителям, но и ко всем актерам, и далее, к актерам «фильмов в фильме», если бы таковые имелись. (Внимание: переноса в обратном направлении не существует — теоремы из фантазии не приложимы к реальному миру! Иначе мы могли бы выдумать любую первую строчку фантазии и «вынести» ее в реальный мир в качестве теоремы.)
Чтобы показать, как действует правило переноса и как правило фантазии может быть применено рекурсивно, приведу следующий вывод:
[ проталкивание
P посылка внешней фантазии
[ снова проталкивание
Q посылка внутренней фантазии
P перенос P во внутреннюю фантазию
<P Λ Q> объединение
] выталкивание из внутренней фантазии во внешнюю
<Q э<P Λ Q>> правило фантазии
] выталкивание из внешней фантазии в реальный мир!
<P э<Q э<P Λ Q>>> правило фантазии
Обратите внимание на то, что для внешней фантазии я отступил на один абзац, в то время как для внутренней — на два; этим подчеркивается природа вставленных один в другой «уровней реальности». О правиле фантазии можно сказать, что оно вводит суждение, сделанное о системе, внутрь самой системы. Таким образом, можно сказать, что полученная нами теорема <x э y> — отображение внутри системы суждения о ней самой: «Если x — теорема, то у — также теорема». Более конкретно, <P э Q> интерпретируется как «если P, то Q» или, что одно и то же, «из P следует Q».
Перевернутое правило фантазии
В Диалоге Льюиса Кэрролла шла речь о высказываниях типа «если… то». В частности, Ахилл никак не мог убедить Черепаху принять за истинную вторую часть «если… то» высказывания, даже когда она приняла за истинные как все высказывание целиком, так и его первую часть. Следующее правило позволяет вам вывести вторую часть строчки «э», в том случае, если сама эта строчка и ее первая часть обе являются теоремами.
ПРАВИЛО ОТДЕЛЕНИЯ: Если x и <x э y> — теоремы, то у — также теорема.
Это правило часто зовется «Modus ponens», а правило фантазии — «Теоремой дедукции».
Интерпретация символов
Довольно загадок! Пора вытащить кота из мешка и открыть «значение» всех остальных символов нашей системы, если это вам еще не ясно. Итак, символ «Λ» действует в точности также, как обыкновенное «и». Символ «~» заменяет слово «не» в формальном отрицании. Уголки «<» и «>» являются группирующими скобками — их функция весьма напоминает функцию обычных скобок в алгебре. Основное различие в том, что в алгебре мы свободны вводить или не вводить скобки, согласно нашему вкусу и стилю, в то время как в формальной системе подобная анархия не допускается. Символ «V» заменяет слово «или» (по латыни «Vel»). Имеется в виду так называемое включающее «или»; это означает, что <x V y> читается как «x или у — или оба сразу».
