Вступление

История этой книги

В последний год (2003) моего пребывания в академии я был преподавателем дискретной математики на факультете компьютерных наук в Стоуни-Брук. Программа курса требовала, чтобы студенты «изучали логику высказываний, функции, рекурсию и математическую индукцию, дополненные примерами из списков и деревьев для иллюстрации этих тем». Текст курса представлял собой массивный и монументально скучный фолиант.

Стоуни-Брук был моим первым знакомством с Очень Скучным Учебником, который господствует на курсах естественных наук в США. Знакомство состоялось так поздно в моей жизни, видимо, потому, что я избегал курсы, где требовалось читать такие скучные учебники. Как и во многих подобных книгах, главной проблемой было отсутствие повествования, связывающего темы. Дискретная математика, как сказал Тойнби об истории, часто преподается просто как одна чертова штука за другой.

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

После того, как я с большим удовлетворением написал письмо, выставляющее моих университетских гонителей как кучку отсталых тупиц, я сел и за месяц написал более 200 страниц материала с подробным описанием запланированного мной курса. Результатом стал учебник «Логика, доказательство и вычисления». Учебник никогда не публиковался, хотя Джим Тайлс из Гавайского университета прочитал его и отозвался положительно. Я просто отложил текст в сторону, посчитав его недостаточно оригинальным, чтобы заслуживать полноценной публикации, и выложил его в виде файла pdf в Интернете.

Десять лет спустя я вернулся к этой работе как основе для онлайн-курса. Без необходимости соответствовать требованиям учебной программы факультета компьютерных наук Стоуни-Брук я мог позволить книге формировать себя в соответствии с моими интересами и мировоззрением, и в результате получился текст, который, как я чувствовал, действительно мог что-то предложить и был написан для определенной аудитории. Я считал, что первоначальное название было хорошим, и поэтому переработанный текст стал вторым изданием «Логики, доказательств и вычислений».

В чем цель этой книги

Частично цель книги -- научить логике. Задача, которую часто с хорошими результатами выполняют такие авторы, как Ходжес и Леммон. Что же тогда может предложить еще один текст на ту же тему, чего не могут предложить эти выдающиеся книги? Ответ в заголовке -- логика находится на пересечении трех основных дисциплин: философия, информатика и математика. Частью задачи данной книги является обучение логике таким образом, чтобы привлечь внимание к пересечениям изучаемой дисциплины с каждой из этих областей.

Поскольку философия, математика и информатика представляют собой обширную область приложения человеческих усилий, невозможно за двадцать лекций охватить эти три области с большой глубиной. Мое намерение не в этом, а скорее в том, чтобы привести читателя к пониманию основ познания. «Логика, доказательство и вычисления» действительно задумана как своего рода отправная точка для студентов, чтобы после получения достаточного количества знаний о логике они могли сами решить, в каком направлении лежит их подлинный интерес.

Логика и математические рассуждения

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

Когда мы рассматриваем логику с такой точки зрения, мы обнаруживаем, что многие из классических подходов к логике не соответствуют этим требованиям. Аксиоматический, или гильбертовский, подход отлично подходит для доказательства метатеорем, но с его помощью трудно получить даже элементарные результаты. Табличные системы учат студентов рассматривать доказательство как довольно механический процесс разложения формул на подформулы, но это сильно затрудняет обучение, когда студенты в дальнейшем читают и сами выводят реальные математические доказательства. Неестественно трактовать каждую проблему как доказательство от противного, как принято в методе аналитических таблиц.

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

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

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

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

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

Логика и вычисления

Здесь нам на помощь приходит информатика, потому что для компьютера печать всех предположений является тривиальной задачей. Поэтому как только рассуждения с секвенциями переносятся с бумаги на компьютер, красота, ясность и сила подхода становятся очевидными. Доказательство с помощью компьютера очень популярно среди студентов! В группе из 240 студентов 220 проголосовали за доказательство с компьютером и только 8 за работу на бумаге. Так что данная книга построена на основе программы под названием provedit! для построения доказательств.

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

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

Вместо этого мы как можно более нежно знакомим читателя с применением программирования при построении доказательств. Средством обучения является язык программирования Shen, на котором написаны программы, используемые в этой книге. Используемые примеры просты и предназначены для понимания читателями без опыта программирования.

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

Логика и философия

Логика, конечно, богата на связи с философией. Наша книга развивает эти связи, показывая точки выбора в классической логике -- места, где мнения профессионалов расходятся относительно того, какие логические принципы следует признавать, а какие -- нет. Помимо минимальной логики, такие логики, как параконсистентная логика, интуиционистская логика и свободная логика, расходятся с ортодоксальной линией, и в нашей книге мы прослеживаем истоки этих разногласий и приводим классические доказательства, которые в таких системах считались бы недействительными.

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