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

• Название: ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда
• Автор: Даглас Хофштадтер
• Издательство: Издательский Дом «Бахрах-М», 2001.
• Жанр: Математика
• Год: 2001
• ISBN: ISBN 5-94648-001-4

Не часто приходится держать в руках книгу, которая открывает новые миры, в которой сочетаются глубина мысли и блестящая языковая игра; книгу, которой удалось совместить ничем на первый взгляд не связанные сложные области знания.

Выдающийся американский ученый изобретает остроумные диалоги, обращается к знаменитым парадоксам пространства и времени, находит параллели между картинами Эшера, музыкой Баха и такими разными дисциплинами, как физика, математика, логика, биология, нейрофизиология, психология и дзен-буддизм.

Автор размышляет над одной из величайших тайн современной науки: каким образом человеческое мышление пытается постичь самое себя. Хофштадтер приглашает в мир человеческого духа и «думающих» машин. Это путешествие тесно связано с классическими парадоксами, с революционными открытиями математика Курта Геделя, а также с возможностями языка, математических систем, компьютерных программ и предметного мира говорить о самих себе с помощью бесконечных отражений.

Начав читать эту книгу,вы попадете в волшебные миры, отправитесь в путешествие, изобилующее увлекательными приключениями, путешествие, после которого вы по-иному взглянете на мир и на самого себя.

Переведенная на 17 языков, книга потрясла мировое интеллектуальное сообщество и сразу стала бестселлером. Теперь и русский читатель получил доступ к одной из культовых книг XX века.

---

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

Ахилл: Если у вас имеется <<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. Теория об исчислении высказываний является «мета-теорией», и ее результаты можно назвать «мета-теоремами» — Теоремами о теоремах. (Обратите внимание на заглавную букву в выражении «Теоремы о теоремах». Это — следствие нашего соглашения: мета-теоремы являются Теоремами (доказанными результатами), касающимися теорем (выводимые строчки).)

В исчислении высказываний можно найти множество других мета-теорем, или вторичных правил вывода. Вот, например, вторичное правило Де Моргана:

<~ x V ~ y> и ~<x Λ у> взаимозаменяемы.

Если бы это было правилом системы, это значительно ускорило бы многие деривации. А что, если мы докажем, что оно верно — достаточно ли этого, чтобы использовать его в качестве еще одного правила вывода?

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

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

С другой стороны, возможен и иной выход. Почему бы нам не формализовать также и мета-теорию? Таким образом, выведенные правила (мета-теоремы) станут частью большей формальной системы и вывод новых, упрощающих деривацию теорем формализованной мета-теории станет законным. Эти теоремы затем могут быть использованы, чтобы облегчить вывод теорем исчисления высказываний. Это интересная идея, но как только мы начинаем ее обдумывать, то тут же сталкиваемся с мета-мета-теориями и так далее. Ясно, что сколько бы уровней мы не формализовали, всегда найдется кто-нибудь, кто захочет вывести упрощающие правила на высшем уровне.

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

Ошибки получаются, когда нам не удается четко разграничить работу внутри системы (способ M) и размышления о системе (способ I). Например, может показаться вполне разумным предположить, что, поскольку <P V ~ P> (частично интерпретируемое как P или не P) — теорема, то одна из двух — либо P, либо не P, должна также являться теоремой. Но это совершенно неверно; не один из членов этой пары не является теоремой. Опасно считать, что символы можно свободно передвигать между разными уровнями — как, например, язык формальной системы и ее метаязык (русский).

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

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

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

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

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

Таким образом, мы считаем исчисление высказываний частью общего метода для составления искусственных структур, подобных доказательствам. Однако оно лишено гибкости или всеобщности, поскольку предназначено только для работы с математическими понятиями, которые, в свою очередь, жестко определенны. В качестве довольно интересного примера давайте рассмотрим деривацию, в которой посылкой фантазии является необычная строчка: <Р Λ ~ Р>. По крайней мере, ее частичная интерпретация звучит странно. Исчисление высказываний, однако, не задумывается над интерпретациями — вместо этого, оно просто манипулирует типографскими символами, а в типографском смысле в этой строчке нет ничего необычного.