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

Неосторожность: И, несмотря на это, вы все еще цепляетесь за мысль, что обе x и ~x могут быть теоремами? Почему бы вам заодно не предположить, что ежи — это жабы, или что 1 равняется 2, или что луна сделана из зеленого сыра? Я, со своей стороны, не хочу даже и думать, что основные ингредиенты моего мыслительного процесса могут быть ошибочными — иначе мне пришлось бы усомниться в собственном анализе всего этого вопроса, и я бы совершенно запуталась.

Осторожность: Ваши аргументы притянуты за уши. Все же мне хотелось бы увидеть ДОКАЗАТЕЛЬСТВО того, что все теоремы истинны, или того, что x и ~x не могут быть теоремами одновременно.

Неосторожность: Желаете доказательства? По-моему, вы более хотите убедиться в непротиворечивости исчисления высказываний, чем в вашем собственном душевном здоровье. Любое мыслимое доказательство включало бы более сложные операции, чем те, что возможны в самом исчислении высказываний. И что бы это доказало? С вашим желанием доказать непротиворечивость исчисления высказываний вы напоминаете мне человека, который захотел выучить русский и потребовал для этого словарь, определяющий все простые слова через более сложные…

Снова Кэрролловский Диалог

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

Систему рассуждений можно сравнить с яйцом. Его внутренность защищена скорлупой — но чтобы куда-то это яйцо послать, вы на нее не надеетесь. Вы упаковываете яйцо в контейнер, выбранный в соответствии с трудностью предстоящего путешествия. Если вы хотите действовать более осторожно, можете даже уложить яйцо в несколько вложенных одна в другую коробок. Однако сколько бы коробок вы не использовали, всегда можно вообразить себе, что происходит катастрофа и яйцо все же разбивается. Точно так же мы никогда не можем дать абсолютное, конечное доказательство того, что доказательства какой-либо системы истинны. Разумеется, мы можем представить доказательство доказательства, или доказательство доказательства доказательства — но нам всегда приходится принимать на веру состоятельность самой внешней из систем. Всегда возможно вообразить, что некая тонкость разрушит каждое из наших доказательств — и когда мы дойдем до «дна», то «доказанный» результат окажется вовсе не таким уж истинным. Это, однако, не означает, что математики и физики постоянно беспокоятся о том, что все здание математики может быть ложным. С другой стороны, когда люди сталкиваются с неординарными, или слишком длинными, или полученными на компьютере доказательствами, они начинают думать над тем, что же имеется в виду под этим почти святым понятием «доказательства».

Отличным упражнением для вас, читатель, было бы сейчас снова вернуться к Диалогу Кэрролла и попытаться закодировать весь спор с самого начала, используя нашу нотацию.

Ахилл: Если у вас имеется <<A Λ B>э Z> и <A Λ B>, то у вас наверняка есть Z.

Черепаха: Вы имеете в виду, что <<<<A Λ B> эZ>Λ<A Λ B>> эZ>, не так ли?

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

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

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