Этот небольшой спор показывает, как трудно использовать логику и рассуждения для защиты самой логики. В какой-то момент вы упираетесь в стенку, и вам ничего не остается, кроме как выкрикивать: "Я знаю, что я прав!" Мы снова столкнулись с вопросом, который Льюис Кэрролл так ярко проиллюстрировал в своем Диалоге: продолжать защищать схему собственного мышления до бесконечности невозможно. Рано или поздно наступает момент, когда приходится в нее просто поверить.
Систему рассуждений можно сравнить с яйцом. Его внутренность защищена скорлупой - но чтобы куда-то это яйцо послать, вы на нее не надеетесь. Вы упаковываете яйцо в контейнер, выбранный в соответствии с трудностью предстоящего путешествия. Если вы хотите действовать более осторожно, можете даже уложить яйцо в несколько вложенных одна в другую коробок. Однако сколько бы коробок вы не использовали, всегда можно вообразить себе, что происходит катастрофа и яйцо все же разбивается. Точно так же мы никогда не можем дать абсолютное, конечное доказательство того, что доказательства какой-либо системы истинны. Разумеется, мы можем представить доказательство доказательства, или доказательство доказательства доказательства - но нам всегда приходится принимать на веру состоятельность самой внешней из систем. Всегда возможно вообразить, что некая тонкость разрушит каждое из наших доказательств - и когда мы дойдем до "дна", то "доказанный" результат окажется вовсе не таким уж истинным. Это, однако, не означает, что математики и физики постоянно беспокоятся о том, что все здание математики может быть ложным. С другой стороны, когда люди сталкиваются с неординарными, или слишком длинными, или полученными на компьютере доказательствами, они начинают думать над тем, что же имеется в виду под этим почти святым понятием "доказательства"
Отличным упражнением для вас, читатель, было бы сейчас снова вернуться к Диалогу Кэрролла и попытаться закодировать весь спор с самого начала, используя нашу нотацию.

Ахилл: Если у вас имеется << A /\ B> Z > и < А /\ В >, то у вас наверняка есть Z.
Черепаха: Вы имеете в виду, что <<<< А /\ В > Z > < А /\ В >> Z >, не так ли?

(Подсказка: то, что Ахилл считает правилом вывода, Черепаха тут же превращает в простую строчку системы. Используя только буквы А, В и Z, вы получите непрерывно удлиняющуюся рекурсивную структуру.)

Кратчайший путь и выведенные правила

Выводя теоремы исчисления высказываний, мы обычно вскоре изобретаем различные сокращения пути, строго говоря, не являющиеся частью системы. Например, если бы в какой-то момент нам понадобилась бы строчка < Q \/ ~Q >, и при этом у нас уже имелась бы ранее выведенная строчка < P \/ ~P >, многие из нас действовали бы так, словно строчка < Q \/ ~Q > уже выведена, так как мы знаем, что ее вывод в точности соответствует выводу < P \/ ~P >. Выведенная теорема используется здесь как "схема теорем" - форма для их отливки. Этот прием вполне допустим, поскольку он помогает нам выводить новые теоремы, но сам по себе он не является правилом исчисления высказываний. Скорее это вторичное, выведенное правило, часть нашего знания о системе. Конечно, то, что это правило всегда оставляет нас в области теорем, еще надо доказать - но, тем не менее, это правило отличается от дериваций внутри системы. Оно является доказательством в ординарном, интуитивном значении этого слова - цепочка рассуждений, проведенная по способу I. Теория об исчислении высказываний является "мета-теорией", и ее результаты можно назвать "мета-теоремами" - Теоремами о теоремах. (Обратите внимание на заглавную букву в выражении "Теоремы о теоремах". Это - следствие нашего соглашения: метатеоремы являются Теоремами (доказанными результатами), касающимися теорем (выводимые строчки)).
В исчислении высказывании можно найти множество других мета-теорем, или вторичных правил вывода. Вот, например, вторичное правило Де Моргана:

<~ х \/ ~ у > и ~< x /\ y > взаимозаменяемы.

Если бы это было правилом системы, это значительно ускорило бы многие деривации. А что, если мы докажем, что оно верно - достаточно ли этого, чтобы использовать его в качестве еще одного правила вывода?
У нас нет причин сомневаться в истинности этого выведенного правила. Однако как только вы начинаете использовать выведенные правила в процедуре исчисления высказываний, формальность системы теряется, поскольку эти правила выведены неформально - вне системы. Формальные системы были предложены, как способ проследить за каждым шагом доказательства внутри единой строгой системы, чтобы каждый математик мог механически проверить работу своих коллег. Однако если вы готовы при малейшей возможности выскочить за рамки системы, то зачем ее вообще было создавать? Как видите, у подобных правил есть и отрицательная сторона.

Формализация высших уровней

С другой стороны, возможен и иной выход. Почему бы нам не формализовать также и мета-теорию? Таким образом, выведенные правила (мета-теоремы) станут частью большей формальной системы и вывод новых, упрощающих деривацию теорем формализованной мета-теории станет законным. Эти теоремы затем могут быть использованы, чтобы облегчить вывод теорем исчисления высказываний. Это интересная идея, но как только мы начинаем ее обдумывать, то тут же сталкиваемся с мета-мета-теориями и так далее. Ясно, что сколько бы уровней мы не формализовали, всегда найдется кто-нибудь, кто захочет вывести упрощающие правила на высшем уровне.
Можно даже предположить, что теория логических рассуждений могла бы быть идентична своей мета-теории, если бы последняя была достаточно аккуратно разработана. Тогда, казалось бы, все уровни соединились бы в один единственный, и размышления о системе стали бы аналогичны работе внутри системы. Однако это не так просто. Даже если система и способна размышлять о самой себе, это еще не значит, что она выпрыгивает из себя. Вы, находясь вне системы, воспринимаете ее по-другому, чем она воспринимает себя сама. Таким образом, мета-теория - взгляд со стороны - все равно существует, даже если теория и может "обдумывать себя саму", не выходя за пределы системы. В дальнейшем мы увидим, что существуют теории, способные на самоанализ. Более того, вскоре мы познакомимся с системой, где это происходит совершенно случайно, без малейшего нашего желания, и увидим, что из этого получается. Однако в нашей работе с исчислением высказываний мы постараемся придерживаться простейших идей и избегать смешения уровней.
Ошибки получаются, когда нам не удается четко разграничить работу внутри системы (способ М) и размышления о системе (способ I). Например, может показаться вполне разумным предположить, что, поскольку < P \/ ~P > (частично интерпретируемое как Р или не Р) - теорема, то одна из двух - либо Р, либо не Р, должна также являться теоремой. Но это совершенно неверно: не один из членов этой пары не является теоремой. Опасно считать, что символы можно свободно передвигать между разными уровнями - как, например, язык формальной системы и ее метаязык (русский).

Размышления о сильных и слабых сторонах системы

Мы только что познакомились с системой, предназначенной отразить часть архитектуры логического мышления. Эта система имеет дело с небольшим количеством простых и точных понятий. Именно простота и точность исчисления высказываний делает его таким привлекательным для математиков. Для этого есть две причины. (1) Его свойства можно изучать сами по себе (так геометрия изучает простые и неподвижные формы). Исчисление высказываний можно варьировать путем изменения различных символов, правил вывода, аксиом или схем аксиом и так далее. (Кстати, представленный здесь вариант исчисления высказываний был изобретен Г. Гентценом в начале 1930-х годов. Существуют другие версии, в которых используется единственное правило вывода - обычно, отделение - и в которых есть несколько аксиом или схем аксиом.) Изучение методов логического мышления при помощи элегантных формальных систем - это весьма привлекательная ветвь чистой математики. (2) Исчисление высказываний может быть легко расширено до включения других фундаментальных аспектов мышления. Это будет частично показано в следующей главе, где исчисление высказываний целиком будет включено в намного большую и глубокую систему, способную на сложные рассуждения в области теории чисел.

Доказательства и деривации

Исчисление высказываний напоминает процесс мышления, но при этом мы не должны равнять его правила с правилами человеческой мысли. Доказательство - это нечто неформальное; иными словами - это продукт нормального мышления, записанный на человеческом языке и предназначенный для человеческого потребления. В доказательствах могут использоваться всевозможные сложные мыслительные приемы и, хотя интуитивно они могут казаться верными, можно усомниться в том, возможно ли доказать их логически. Именно поэтому мы и нуждаемся в формализации. Деривация, или вывод - это искусственное соответствие доказательства; ее назначение - достичь той же цели, на этот раз с помощью логической структуры, методы которой не только ясно выражены, но и очень просты.
Обычно формальная деривация бывает крайне длинна по сравнению с соответствующей "естественной" мыслью. Это, конечно, плохо - но это та цена, которую приходится платить за упрощение каждого шага. Часто бывает, что деривация и доказательство "просты" в дополнении друг к другу. Доказательство просто в том смысле, что каждый шаг "кажется правильным", даже если мы и не знаем точно, почему; деривация проста, потому что каждый из мириада ее шагов так прост, что к нему невозможно придраться и, поскольку вся деривация состоит из таких шагов, мы предполагаем, что она безошибочна. Каждый тип простоты, однако, привносит свои тип сложности. В случае доказательств, это сложность системы, на которую они опираются - а именно, человеческого языка; в случае деривации, это их астрономическая длина, делающая их почти невозможными для понимания.
Таким образом, мы считаем исчисление высказывании частью общего метода для составления искусственных структур, подобных доказательствам. Однако оно лишено гибкости или всеобщности, поскольку предназначено только для работы с математическими понятиями, которые, в свою очередь, жестко определенны. В качестве довольно интересного примера давайте рассмотрим деривацию, в которой посылкой фантазии является необычная строчка: < Р /\ ~Р >. По крайней мере, ее частичная интерпретация звучит странно. Исчисление высказываний, однако, не задумывается над интерпретациями - вместо этого, оно просто манипулирует типографскими символами, а в типографском смысле в этой строчке нет ничего необычного.
Вот фантазия с данной строчкой в качестве посылки.

(1)	[              проталкивание
(2)	   <Р/\~Р>     посылка
(3)	    Р          разделение
(4)	    ~Р         разделение
(5)	    [          проталкивание
(6)	      ~Q       посылка
(7)	      Р        переход, строка 3
(8)	      ~~Р      двойная тильда
(9)	    ]          выталкивание
(10)	    <~О~~Р>  фантазия
(11)	    <~PQ>    контрапозиция
(12)	    Q          отделение (строчки 4, 11)
(13)	 ]             выталкивание
(14)	 <<P/\~P>Q>  фантазия

Эта теорема имеет очень странную частичную интерпретацию:

Из Р и не Р вместе взятых следует Q

Поскольку Q можно интерпретировать любым предложением, мы можем считать, что эта теорема утверждает, что "из противоречия следует что угодно"! Поэтому системы, основанные на исчислении высказываний, не могут содержать противоречий - противоречия мгновенно заражают всю систему, подобно глобальному раку.


Подход к разрешению противоречий

Это не похоже на человеческую мысль. Если вы обнаружите в своих рассуждениях противоречие, вряд ли это разрушит все здание вашего мышления. Вместо этого вы, скорее всего, попытаетесь найти те идеи или методы рассуждения, которые явились причиной противоречия. Иными словами, вы попытаетесь, насколько это возможно, выйти из ваших внутренних систем, приведших к противоречию, и попробуете их исправить. Маловероятно, что вы поднимете руки вверх и воскликнете: "Это показывает, что теперь я верю во все, что угодно!" - разве что в шутку.
В действительности, противоречия - это важный источник прогресса во всех областях жизни, и математика не является исключением. В прошлом, когда в математике обнаруживалось противоречие, математики тут же пытались найти виновную в этом систему, выйти из таковой, проанализировать ее и, если возможно, залатать прореху. Вместо того, чтобы делать математику слабее, нахождение и "починка" противоречивых систем только усиливали ее. Этот путь был долог и усеян ошибками, но в конце концов, он приносил плоды. Например, в средневековье предметом горячих споров была бесконечная последовательность

1 - 1 + 1 - 1 + 1 - ...

Существовали "доказательства", что эта серия равняется 0, 1, 1/2 - а может быть, и другим числам. Из подобных противоречивых результатов выросла более полная и глубокая теория бесконечных рядов.
Более актуальный пример - противоречие, с которым мы сталкиваемся в данный момент; это противоречие между тем, как мы действительно думаем, и тем, как исчисление высказываний имитирует наше мышление. Это продолжает быть источником дискомфорта для многих логиков; множество творческих усилий было приложено к тому, чтобы улучшить исчисление высказываний, чтобы оно не было таким жестким. Одна из попыток, изложенная в книге А. Р. Андерсона и Н. Белнапа "Следствие" (A.R. Anderson & N.Belnap, "Entailment")³, включает "уместный подтекст", с тем, чтобы придать символу "если - то" действительную причинность или, по крайней мере, некоторую связь со смыслом. Взгляните на следующие теоремы исчисления высказываний:

<P<QP>>
<P<Q\/~Q>>
<<Р/\~Р>Q>
<<PQ>\/<QP>>

Эти и другие подобные теоремы показывают, что первая и вторая части суждений типа "если...то" вовсе не должны иметь никакой связи для того, чтобы быть доказанными в исчислении высказываний. С другой стороны, "уместный подтекст" ставит некоторые ограничения на контекст, в котором может действовать правило вывода. Опираясь на интуицию, он говорит нам, что "что-то может быть выведено из чего-то только в том случае, если эти части как-то соотносятся между собой". Например, строка 10 в деривации выше была бы невозможна в данной системе - и это, в свою очередь, заблокировало бы вывод строчки << Р/\~Р >Q >.
Более радикальные попытки полностью отказываются от поисков непротиворечивости и полноты, пытаясь взамен симулировать человеческое мышление со всеми его противоречиями. Подобные исследования уже не ставят своей целью дать математике прочный фундамент; они занимаются изучением процесса человеческой мысли.
Несмотря на некоторые странности, исчисление высказываний обладает многими положительными чертами. Если рассматривать его как часть большей системы (что мы и сделаем в следующей главе), и знать наверняка, что сама эта система свободна от противоречий (мы будем в этом уверены), то исчисление высказываний выполняет все, чего мы можем от него ожидать: оно производит все возможные правильные умозаключения. Даже если противоречие все-таки будет обнаружено, мы можем быть уверены, что виновница этого - сама большая система, а не ее подсистема - исчисление высказываний.

Вопросы? Предложения? Претензии?
Обсудить материал в моем ЖЖ