Логики и программы – Часть 1. Что такое логики и какие логики бывают?

Непейвода Николай Николаевич - Доктор физико-математических наук, профессор Удмуртского государственного университета. Логик, математик, информатик, философ. Автор более 150 научных работ, в том числе книги "Логика и компьютер", "Прикладная логика", "Основания программирования", "Стили и методы программирования".

Оказывается, логики бывают разные. Впрочем, ничего удивительного – дети, женщины, программисты, ... – у всех есть своя специфическая логика. На уроках математики в школе учатклассической «Аристотелевой логике», которая является основой доказательных логических рассуждений. Но доказательное логическое рассуждение относится к обычному в некотором отношении так же, как стихи относятся к прозе. Речь пойдёт о возможных правилах построения логических рассуждений (правилах вывода). Программистам кроме классической логики на практике могут пригодиться конструктивные, релевантные, модальные идругие логики.

Содержание

Что такое логика?
Примеры исчислений и логик
Конструктивные логики
Отступление: Грязные теоремы существования³
Возможные миры
Невозможные миры
Сноски

Жили в грузинском селе три брата. Украл у них кто-то барана. 
Первый брат говорит: 
— Раз украл, значит рыжий. 
Второй продолжает рассуждение: 
— Раз рыжий, значит, кривой. 
Третий завершает: 
— Раз рыжий и кривой, значит, Гоги. 
Пошли они бить Гоги. Схватили их соседи и привели к судье. Тот спрашивает, почему они бесчинствуют? 
— Мы не бесчинствуем, а вора бьем. Гоги у нас барана украл. 
— А как вы это узнали? 
— Логически. 
Рассказали братья свои рассуждения. 
— Да где же здесь логика? Так вы что угодно доказать сможете! 
— Не что угодно, а лишь правду. 
— Ну ладно, я сейчас выйду в соседнюю комнату и что-то спрячу в ящичек, а вы логически установите, что я спрятал. 
Возвращается судья с ящичком. Первый брат говорит: 
— Раз спрятано, значит, круглое. 
Второй продолжает: 
— Раз круглое, значит, белое. 
Третий завершает: 
— Раз круглое и белое, значит, яйцо. 
Судья открывает ящичек, показывает всем яйцо и заявляет: 
— Гоги, сейчас же отдай барана и заплати штраф! 
Грузинско"=русский анекдот.

Что такое логика?

Логика определяется как «формальная наука о способах доказательного рассуждения». Обычно понятие доказательного рассуждения показывается на примерах (силлогизмах), подобным следующему:

                             Все люди смертны.
                             Сократ - человек
                             Следовательно, сократ смертен

На подобных рассуждениях иллюстрировал логику и её создатель Аристотель, и его последователи многие столетия (по традиционной хронологии 2000 лет, но нужно помнить, что измерения в истории подчиняются тем же законам, что и физические измерения, и точность дат из древней истории, вычисленная по законам, по которым обрабатываются физические измерения, 500 лет). Льюис Керролл ¹ заметил, что логика применима и к рассуждениям в возможных и невозможных мирах, подобным следующему:

                            Все змеи крылатые.
                            Автор статьи - змея.
                            Следовательно, у автора есть крылья

Это сразу же привело к абсурду (точный логический термин!) — столько веков ошибочно приписывающуюся логике репутацию науки, занимающейся лишь тривиальностями. Формальная наука отличается тем, что она проверяет прежде всего форму и поэтому может рассуждать про глокую куздру из знаменитого предложения академика Щербы «Глокая куздра штеко быдланула бокра и кудрячит бокренка» столь же уверенно, как про сивую кобылу. Поскольку программист, в некотором смысле, творец возможных либо даже невозможных миров, в принципе он ограничен в своей деятельности лишь законами логики. Далее, в определении предмета логики мы избежали слова «изучение». Это связано с тем наблюдением, которое сделал ещё в XVIII веке великий кенигсбергский философ Иммануил Кант. Логика не изучает мышление, она упорядочивает и нормализует его. Она имеет дело не с процессом открытия, а с формой изложения полученного результата с тем, чтобы убедить других в его правильности, а себя в отсутствии самообмана (заметьте аналогию с отладкой программы!) Кант сказал ещё точнее и жестче: «Логика является цензурой мысли». Мы привыкли поклоняться идолу свободы и рассматривать само слово «цензура» как нечто почти нецензурное. Но посмотрите, как выродилась наша литература после получения абсолютной свободы. Противодействие порождает действие, наступление вызывается обороной (Клаузевиц), чтобы иметь опору, надо от чего-то отталкиваться, чтобы добиваться успехов, надо преодолевать трудности, и вот осталась нашей богеме лишь одна возможность измышлять нечто новое: наркотики, «дурь» — Это какой же дури надо было нанюхаться, чтобы придумать такое! Вот классно! «Творческая интеллигенция», из-за полного отсутствия представлений о платоновских идеальных мирах, которые приоткрывает настоящая наука (прежде всего, математика), не видит другого способа стимуляции воображения, кроме ‘дури’ ²! Для достижения большей выразительности поэт накладывает на себя самоограничение, переходя от прозы к стихам. Настоящие стихи (а не то, что в нынешнее время называется «верлибр») проверяются прежде всего по формальному признаку: наличию чёткого ритма, а затем по создаваемому ими впечатлению и заложенному в них смыслу. Доказательное логическое рассуждение относится к обычному в некотором отношении так же, как стихи относятся к прозе. Но стихи часто ценятся за неоднозначность, а доказательство — лишь за однозначность. Чтобы конструкция была доказательством, нужно, чтобы её синтаксическая правильность гарантировала семантическую. Чтобы конструкция была доказательством в конкретной системе (в этом случае её чаще всего называют выводом), нужно, чтобы она удовлетворяла однозначным, четким и алгоритмически разрешимым условиям, наложенным данной системой. Если система, в которой задано понятие вывода, работает с формулами математического формального языка, причём достаточно общепризнанным способом, её называют теорией, а в общем случае просто исчислением.

Примеры исчислений и логик

Начнем с простейшего примера исчисления, в котором выводятся правильно построенные скобочные конструкции и только они. Например, (()())() в нем выводится, а (())) — нет. Это исчисление задаётся тремя правилами вывода, которые позволяют выводить новые объекты из уже полученных ранее.

Первое из этих правил задаёт аксиому. Оно имеет посылок, и, соответственно, не требует для своего применения никаких ранее построенных объектов. Аксиомы часто пишутся просто как выражения, опуская конструкцию правила с посылок. Данная аксиома могла бы быть просто записана как . Второе правило позволяет соединить два ранее построенных скобочных выражения, поставив их одно за другим. Третье — поставить скобки вокруг ранее построенного выражения. Приведённое ниже дерево является выводом в данном исчислении.

Поскольку в структуре дерева для нас важно лишь то, что новые объекты могут быть построены лишь на базе уже построенных ранее, это дерево часто записывается как последовательность объектов: Программист при этом может заметить, что, перейдя от дерева к последовательности (что, как прокомментирует математик, никакой существенной роли не играет), мы коренным образом изменили структуру данных: теперь у нас имеется сеть, в которой один и тот же объект может использоваться несколько раз (в данном случае таким объектом была лишь наша аксиома). Вспомните, что писалось в статье «Чего не могут вычислительные машины?» Когда теоретик говорит, что это все безразлично, практик должен насторожиться. На этом примере показаны все характерные черты традиционных исчислений. Новые объекты получаются из уже выведённых по правилам вывода. С теоретической точки зрения вывод может быть записан как последовательность объектов либо как дерево. Только что приведённое исчисление выводило объекты, которые сами по себе особого смысла не имеют. Но ещё в 20-х гг. прошлого века Д. Гильберт и его ученики переформулировали аналогичным образом исчисление высказываний. В этом исчислении объектами являются формулы, построенные при помощи связок ("и", "или", "следовательно", "не"). Его фрагмент, содержащий лишь импликацию, задаётся тремя правилами с нулем посылок (схемами аксиом) и одним правилом с двумя посылками:

(1)

(2)

(3)

(4)

Это исчисление называется классической импликативной (импликация = следствие) логикой в форме Гильберта. Формулы имеют обычное истолкование, основанное на таблицах истинности. В этом исчислении выводятся те и только те импликативные формулы, которые тождественно обращаются в истину. Но установить это исключительно нетривиально.

В принципе (и даже в реальности) таблица истинности, в которой рассмотрены все наборы значений и получена тождественная истина, сама по себе является доказательством формулы исчисления высказываний. Но такое доказательство несколько туповато: в любом случае нужно рассматривать все значения, получается гарантированный полный перебор. А гильбертовское доказательство выглядит порою просто безумно. Например, вот как доказывается простейшая теорема :

(2)

(3)

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

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

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

Заметим, что в предыдущем абзаце отсутствует слово «доказательство». Если бы мы ограничились задачей доказательства, классическая логика стала бы ещё более подходящей. Именно поэтому «практические» (что, как следует из многих уже сказанных вещей, да и из многого другого, означает: бесконечно далекие от практики) математики никакой другой логики не знают и знать не хотят. Но задача «доказать» включает в себя элемент жульничества. Для практики нужно проверять. Вы, наверно, уже слышали, что классическая логика не единственна. Но в большинстве популярных изданий и в «общественном мнении» проводится в корне неправильная точка зрения на неклассические логики: дескать. они многозначные, там могут быть другие значения формул, кроме двух стандартных: истина и ложь. Многозначные логические исчисления (даже если они могут претендовать на имя логики) являются скорее модификациями классической логики. Самые интересные и самые важные для приложений неклассические логики — те, где переходят к совершенно другой семантике формул.

Конструктивные логики

Еще в 1908 г. голландский аспирант (Э.Л.Я. Брауэр опубликовал на голландском языке диссертацию под наглым названием: «De onbetrouwbaarheid der logische principes», что означает «Недостоверность логических принципов». Брауэр аргументировал, что причина тех неприятностей, с которыми столкнулась математика в начале XX века (и которые не преодолены и до сих пор; к ним просто привыкли и стали игнорировать), не в каких-то частных принципах теории множеств, а в самой логике. Логика создавалась для конечных объектов, а перенесли её на бесконечные. В частности, для бесконечных объектов нельзя считать автоматически выполненным закон исключенного третьего « или не » (на символическом языке современной логики ), поскольку мы можем просто не уметь распознать эти два случая. Брауэр показал, что закон исключенного третьего в обычной логике эквивалентен ещё одному общепринятому закону: снятия двойного отрицания , который в курсе математики выступает в качестве доказательств от противного: «Нужно доказать A . Предположим, что не верно A … Получаем абсурд. Полученное противоречие доказывает теорему» Как всегда у первооткрывателей, гениальные прозрения у Брауэра сочетались с некорректными объяснениями. Если причина недоразумений в самой логике, почему же эллины, создавшие и отработавшие классическую логику на примере геометрии, в которой также рассматривается бесконечная совокупность объектов, ни с какими неприятностями, проистекающими от нее, не сталкивались? Да дело просто в том, что гениальная интуиция и потрясающее чувство гармонии эллинов воспрепятствовали им использовать в геометрии числа. Тем самым они избежали попадания в область неразрешимых проблем. А, как показал Гёдель, там, где появляются натуральные числа, возникают и неразрешимые проблемы. Но, конечно же, неразрешимые проблемы возникают лишь для бесконечных совокупностей объектов. А там, где возникают неразрешимые проблемы, закон исключенного третьего выглядит до глупости оптимистичным: как мы можем утверждать, что или не , когда мы в принципе не можем знать ни того, ни другого? Но самое важное у Брауэра было то, что он полностью видоизменил приоритеты математики. Если традиционная математика занимается поиском и доказательством теорем, то он начал её рассматривать как источник построений. Мало доказать теорему, нужно, чтобы обоснование дало нам построение объекта, существование которого утверждается в теореме. А использование доказательств в качестве источника построений — именно то, что нужно от математики информатику.

Отступление: Грязные теоремы существования³

Многие математические теоремы, утверждающие существование объекта, на самом деле никакого построения не то, что не дают, а в принципе дать не могут. В школьном курсе таких теорем стыдливо избегают, но классический курс высшей математики начинается с такой теоремы: любое ограниченное множество действительных чисел имеет верхнюю грань. Но она ещё не столь грязна, как другие теоремы, для которых не то, что построить, но и однозначно описать объект, существование которого доказывается, нельзя даже с привлечением самых мощных математических средств. Пример такой теоремы — знаменитая польская теорема о разрезании шара: Шар можно разбить на четыре подмножества таким образом, что, попарно совмещая их в пространстве, можно сложить два таких же шара.

Шар можно разбить на четыре подмножества таким образом, что, попарно совмещая их в пространстве, можно сложить два таких же шара. Рис Брауэр был, как и полагается гению, последователен и жесток. Мало высказать благие пожелания, нужно, чтобы они не стали благоглупостью, беспощадно провести их в жизнь . Если нам нужны построения, то логическое значение формулы отступает на второй план. Главное то, какую конструкцию несёт в себе её доказательство. Сами шаги доказательства в этом случае превращаются в шаги построения, а всё доказательство в программу. Как прекрасно для программистов! Но, конечно же, нужно помнить, что такой идеал достижим лишь в принципе. Таким образом, каждая формула в конструктивных логиках превращается в задачу, а сама концепция истинностных значений исчезает. В классической логике все теоремы имеют одно и то же значение — истина. В конструктивной логике они соответствуют разным задачам и разным построениям. Несмотря на то, что идеал остаётся сверкающей мечтой, конструктивные логики уже развились настолько, что могут служить средством анализа программ и помощью при их построении. Их связи с программами посвящена следующая статья.

Возможные миры

Это направление возникло гораздо более мирным и постепенным, не столь револющионным, путем. Еще Аристотель писал, что некоторые высказывания истинны с необходимостью, например, что , а другие лишь случайно, в нашем мире, например, что он сам родился в Стагире. Более того, наш мир развивается во времени, и, например, радикальные толки ислама рассматривают его как совокупность миров, которые каждое мгновение по своему благому умыслу творит Аллах, поскольку иначе пришлось бы задуматься над вопросом, подчиняется ли Бог законам логики, сама постановка которого кощунственна для мусульманина. Буддисты, джайны и манихеи вообще рассматривали наш мир как один из множества возможных миров. Эта концепция совокупности возможных миров была использована для представления в логике необходимости и возможности. Она же применяется для описания временных зависимостей. Заодно она оказалась полезна для описания и анализа программ: ведь программа — совокупность действий, каждое из которых изменяет внутренний мир вычислителя, исполняющего данную программу. Этому, в настоящий момент общепринятому, логическому средству будет посвящена одна из последующих статей.

Невозможные миры

Другое направление в логике заложил русский логик Л. Васильев примерно в те же годы, что и Брауэр, но оно было благополучно забыто до 50-х гг., когда его (действительно независимо!) переоткрыл бразильский логик Ньютон да Коста. В жизни всё время сталкиваемся с противоречивыми нормами. Например, давать списывать нельзя, но какой же русский школьник и студент не замешан в этом деле либо как активная, либо как пассивная (дающая) сторона? Паранепротиворечивые логики рассматривают, как рассуждать на базе противоречивых посылок и тем не менее получать разумные следствия. А их модельная основа — невозможные миры, где могут быть противоречия. С невозможными мирами связана и другая отрасль логик, появившаяся как попытка формализовать аргументы, часто используемые рецензентами работ: «Автор утверждает, что следует из . на самом деле верно, но из оно не следует. Оно опирается на другие аргументы.» Чисто формально, например, следующая импликация истинна в классической логике:

Дважды два — четыре. 
Значит, Москва — столица России.

Релевантные логики исследуют логические зависимости, связь по смыслу между высказываниями. В принципе, модальные и релевантные логики были бы великолепными инструментом программиста. Первые — для анализа противоречивых требований заказчиков или начальства. Вторые — для анализа собственных и чужих рассуждений, чтобы понять, где же кроется хитрая ошибка в программе. Но до такого уровня они ещё не доросли. Желающим подробнее ознакомиться с состоянием современной логики автор мог бы рекомендовать, скажем, свою книгу: Непейвода Н. Н. Прикладная логика. Издание второе. Новосибирск, НГУ, 2000 г.

Сноски

¹ Точнее, проф. Додсон, поскольку работы по логике он публиковал под своим настоящим именем, но в данном случае можно вспомнить русского поэта Фета, чья дворянская фамилия была Шеншин; когда царь пожаловал ему эту фамилию, признав его законным сыном русского дворянина, образованное общество иронизировало: «Как Фет, Вы имели имя, а теперь лишь фамилию»

² Будучи как-то раз на выставке картин акад. Фоменко, автор, наслаждаясь гениально выраженными идеальными сущностями, переданными в абстрактных и сюрреалистических образах, услышал за спиной разговорчик группки «интеллектуалов богемного вида»: — Это какой же дури надо было нанюхаться, чтобы придумать такое! Вот классно! «Творческая интеллигенция», из-за полного отсутствия представлений о платоновских идеальных мирах, которые приоткрывает настоящая наука (прежде всего, математика), не видит другого способа стимуляции воображения, кроме «дури».

³ По привычке математиков давать самым отвратительным вещам самые приятные названия, чтобы замаскировать скрытые уродства своей науки, они в обычной литературе называются «чистыми». После публикаций и докладов автора многие математики стали называть их грязными.

⁴ Но здесь поджидает другая опасность. Свобода, равенство и братство превращаются в гильотину, справедливость — в красный террор, забота о здоровье нации — в нацизм. Этой опасности Брауэр избежал в математике.