Математика и логика / Статьи — Математическая составляющая

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

Мы расскажем о том, как и почему возникла математическая логика, что она изучает, какие у неё есть достижения и современные применения.

От Аристотеля к Булю. Основы учения о правильных рассуждениях заложил Аристотель. Он заметил, что корректные умозаключения следуют определённым элементарным схемам, называемым силлогизмами, и перечислил ряд таких схем. (Классический пример силлогизма: «Все люди смертны. Сократ — человек. Следовательно, Сократ смертен».) Учение о силлогизмах в свою очередь опиралось на глубокий анализ понятий и их соединения в высказывания.

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

Возникновение математической логики полностью изменило представления учёных как о методах исследования логики, так и о том, что составляет сам предмет её изучения. В наше время заявления, что логика есть наука о правильных рассуждениях, кажутся настолько же справедливыми, насколько утверждение «математика — это наука о правильных вычислениях».

Аналогия между рассуждениями и вычислениями несколько глубже, чем кажется на первый взгляд. Возникновение логики как математической науки было связано с работами британских учёных Джорджа Буля и Августа де Моргана, которые обнаружили, что с логическими высказываниями можно оперировать как с алгебраическими выражениями. Например, если сложение читать как логическую связку «или», умножение как «и», а равенство как «равносильно», то для любых высказываний $a$, $b$ выполняются законы $$ a+b=b+a,\quad a\cdot(b+c)=a\cdot b+a\cdot c, $$

как и многие другие привычные нам законы арифметики. Но, помимо этого, в алгебре высказываний выполняется и кое-что непривычное, например всегда $$ a+a=a\quad \hbox{и}\quad a+(b\cdot c)=(a+b)\cdot (a+c). $$

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

Математизация логики и аксиоматизация математики. Движущей причиной процесса математизации логики был назревший в самой математике на рубеже XIX—XX веков кризис оснований. С одной стороны, во второй половине XIX века в математике получил распространение удобный язык теории множеств, созданной Георгом Кантором. Математики стали уверенно использовать в своих рассуждениях конструкции с бесконечными множествами. Математика, вооружённая теорией множеств, шла от успеха к успеху.

С другой стороны, в самой теории множеств Кантора обнаружились парадоксы, которые указывали на то, что с этой теорией не всё в порядке на самом базовом уровне. Простейший парадокс такого рода, в фольклорном варианте известный как парадокс брадобрея, был придуман Бертраном Расселом: рассмотрим множество $R$ всех тех множеств, которые не содержат сами себя в качестве элемента. Тогда $R\in R$ если и только если $R\notin R$, противоречие.

Такое положение дел заставило многих выдающихся математиков и философов той эпохи (Пеано, Фреге, Рассел, Гильберт, Пуанкаре, Брауэр, Вейль и др.) задуматься об основаниях математики. Их волновали такие фундаментальные вопросы как:

Что означает доказать математическую теорему? Какие средства при этом законно использовать?
Что значит выразить то или иное математическое понятие или утверждение на том или ином языке?
Когда мы говорим об истинности и о доказуемости какого-либо математического утверждения, имеется ли в виду одно и то же?

Параллельно в математике стали укореняться новые стандарты строгости. Основные области математики — анализ, алгебра, геометрия — были поставлены на аксиоматическую основу. Великий математик Давид Гильберт (1862—1943) был ярким сторонником и пропагандистом аксиоматического метода. Под его влиянием была построена и общепринятая в наше время система аксиом теории множеств, свободная от очевидных парадоксов. Эту аксиоматику предложил в 1908 году Э. Цермело и в дальнейшем дополнили Дж. фон Нейман и А. Френкель. Но где же настоящая гарантия, что полученная система не содержит противоречия? Каким образом это можно установить?

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

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

Математическая логика по предмету своему
есть логика, а по методу — математика.

(П. С. Порецкий, 1884 год, Казань.)

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

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

Логика предикатов. Разработчики первых формальных языков и систем, как правило, не думали о том, что эти системы могут быть реально использованы в вычислительных устройствах. (Исключением, видимо, можно считать великого учёного Готфрида Вильгельма Лейбница (1646—1716), который почти за два века до Буля предвосхитил многие идеи математической логики, включая идею формализации языка математики, и даже построил механический арифмометр.)

Первые формальные языки и системы возникли как результат выделения фрагмента естественного языка, достаточного для передачи формулировок математических утверждений и их анализа. Процесс выработки основных категорий этого языка был продолжительным и шёл параллельно с выработкой некоторых ставших в наше время стандартными математических обозначений. (Одним из важных понятий, введённых в это время, стало понятие квантора, сформировавшееся в работах Г. Фреге и Ч. Пирса. Кванторы существования $\exists$ и всеобщности $\forall$ заменяют языковые конструкции «для некоторого» и «для всех». Первое из этих обозначений введено Дж. Пеано в 1897 году, второе — по аналогии — Г. Генценом в 1935 году, однако общеупотребительными эти обозначения стали лишь под влиянием Бурбаки во второй половине XX века.) Этот процесс в основном завершился в 1920‐х годах, когда в качестве стандартного класса языков, предназначенных для формализации и анализа математических утверждений, стал рассматриваться язык логики предикатов (первого порядка).

Предикатом на множестве $M$ мы называем высказывание, зависящее от $n$ параметров из этого множества (например, «натуральное число $x$ чётно», «точки $x$, $y$ и $z$ плоскости лежат на одной прямой»). Как только фиксированы значения параметров, предикат принимает логическое значение ложь или истина. Таким образом, с формальной точки зрения предикат представляет собой функцию от $n$ аргументов из множества $M$ в $\{0,1\}$.

Не вдаваясь в технические подробности, можно приблизительно описать высказывания логики предикатов как такие, которые можно сформулировать (предполагая заранее заданными обозначения некоторых базовых предикатов) с помощью конструкций $\land$ «и», $\lor$ «или», $\neg$ «не», → «влечёт» и уже упомянутых кванторов. Например, текст $\forall{x} \exists{y} (y>x \land P(y))$ выражает неограниченность множества простых чисел, если договориться, что переменные пробегают множество натуральных чисел, «$>$» означает «больше», а $P(y)$ выражает простоту числа $y$. Эти договорённости составляют часть того, что мы назвали семантикой языка логики предикатов.

Удивительный факт, подтверждаемый всей существующей математической практикой, состоит в том, что выразительных средств языка логики предикатов — на первый взгляд очень скромных — достаточно для формулировки любых известных математических результатов. При этом может быть использовано всего лишь одно базовое понятие — предикат принадлежности $x\in y$ «множество $x$ есть элемент множества $y$». (В картине мира аксиоматической теории множеств все объекты, обозначаемые переменными, являются множествами.)

Доказуемость и вычислимость. Выразить в данном языке то или иное осмысленное утверждение — совсем не то же самое, что суметь его доказать. Следующий уровень языка логики предикатов состоит в описании таких текстов, которые следует признать корректными доказательствами. Традиционно этот уровень называется в математической логике исчислением предикатов. Формальное доказательство (в формате, который принято называть гильбертовским, но который существовал и до работ Давида Гильберта) представляет собой конечную цепочку высказываний логики предикатов, каждое из которых либо является аксиомой, либо получается из предшествующих высказываний по одному из постулируемых правил. Минимальный стандартный набор таких правил содержит лишь два: правило, позволяющее из высказываний $A$ и $A \to B$ вывести $B$, и правило, позволяющее из высказывания $A$ вывести $\forall x A$. (Если высказывание $A$ содержит параметр $x$, то формальное доказательство $A$ обосновывает его истинность при всех возможных значениях параметра.)

Таким образом, математическая доказуемость описывается двумя формальными языками — языком утверждений, описанным в предыдущем разделе, и языком доказательств — из которых второй является надстройкой над первым.

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

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

Одним из первых, кто это понял, был Алан Тьюринг, давший точное определение и наиболее убедительный анализ понятия вычислимой функции в 1936 году. Другими учёными, которые наряду с Тьюрингом пришли к тем же идеям приблизительно в то же время, были Алонзо Чёрч и Эмиль Пост. Этими и другими исследователями в 1930‐х годах были созданы начала теории алгоритмов, которая стала основой понимания работы и построения вычислительных устройств в 40‐е и 50‐е годы. В частности, идея универсальной машины Тьюринга была в дальнейшем технически реализована в компьютерной архитектуре «по фон Нейману», в соответствии с которой программа хранится в памяти устройства и может быть модифицирована в ходе его работы. На основе этой идеи построены все операционные системы.

Задачей, которую стремились решить пионеры теории алгоритмов, был вопрос, поставленный Гильбертом и названный им по‐немецки Entscheidungsproblem, «проблема решения». Вопрос состоял в том, чтобы найти алгоритм, который по данному утверждению, записанному на языке логики предикатов, давал бы ответ, существует ли формальное доказательство этого утверждения или нет. Если бы такой алгоритм существовал, то все математические проблемы в некотором смысле имели бы чисто механическое решение: как уже упоминалось, на языке логики предикатов можно сформулировать практически любое математическое утверждение, например знаменитую гипотезу о бесконечности числа пар простых чисел-близнецов. Тогда вопрос о том, выводима ли эта гипотеза из аксиом теории множеств, сводился бы к проверке доказуемости некоторого высказывания в исчислении предикатов. Неудивительно, что исследователи Entscheidungsproblem стремились показать, что требуемого алгоритма в принципе не может существовать.

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

Гёдель, хотя и был первым, кто фактически сформулировал универсальный язык программирования, не считал, что найденное им (и французским логиком Эрбраном) понятие является универсальным в смысле способности запрограммировать любой алгоритм. Первым, кто высказал тезис об универсальности своей вычислительной модели, был Алонзо Чёрч. Он также предъявил доказательство невозможности решения Entscheidungsproblem в рамках этой модели. Исчисление Чёрча было очень простым по форме, но больше напоминало формальное логическое исчисление, чем реальную вычислительную машину. Машины Тьюринга в этом смысле были ближе к будущей реальности, и поверить в тезис Тьюринга о том, что любая задача, имеющая алгоритмическое решение, может быть решена на машине Тьюринга, было намного легче, чем в аналогичный тезис Чёрча (известно, что именно работа Тьюринга смогла убедить Гёделя в справедливости этого тезиса). Тьюринг также показал, что его машины эквивалентны лямбда-исчислению в смысле вычислительных возможностей, что стало косвенным свидетельством справедливости тезиса Чёрча—Тьюринга, как его теперь принято называть.

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

Что касается лямбда-исчисления, то оно долгое время пребывало на обочине математической логики, будучи вытеснено из теории алгоритмов более удобными и интуитивными моделями. Однако во второй половине XX века лямбда-исчисление и системы на его основе нашли серьёзные практические применения. Лямбда-исчисление Чёрча стало прообразом так называемых функциональных языков программирования (таких как современный язык Haskell), которые имеют ряд преимуществ по сравнению с традиционными императивными языками и в настоящее время очень активно развиваются.

Алгоритмически неразрешимые проблемы в математике. Вслед за Entscheidungsproblem с точки зрения теории алгоритмов были проанализированы и многие другие математические проблемы, поставленные как вопросы о построении того или иного алгоритма. Некоторые из таких трудных проблем, остававшихся открытыми десятилетиями, оказались алгоритмически неразрешимыми задачами.

Среди такого рода вопросов наиболее известна 10‐я проблема Гильберта о распознавании разрешимости диофантовых уравнений. Диофантово уравнение — это уравнение вида $P(x_1,…,x_n)=0$, где $P$ — многочлен с целыми коэффициентами от переменных $x_1$, …, $x_n$. Требуется узнать по заданному многочлену $P$, существуют ли целые числа $x_1$, …, $x_n$, удовлетворяющие такому уравнению.

Вопрос Гильберта о построении общего алгоритма, работающего для всех диофантовых уравнений, с самого начала выглядел безнадёжным. С появлением теории алгоритмов исследователи стали предпринимать усилия в попытке доказать неразрешимость этой задачи. Промежуточные результаты в этом направлении получили американские логики Дж. Робинсон, М. Дэвис и Х. Патнэм, на их основе окончательное решение задачи было получено лишь в 1970 году ленинградским математиком Ю. В. Матиясевичем.

В наше время в математике алгоритмические вопросы занимают подобающее им важное место. Математическая логика научила нас тому, что далеко не всякий такой вопрос является разрешимым. Кроме того, даже если алгоритм решения той или иной задачи существует в принципе, не всегда можно говорить о его применимости на практике. Например, выполнение алгоритма может потребовать слишком много времени или памяти компьютера. Такого рода вопросами занимается отдельная область теории алгоритмов — теория сложности вычислений, о которой подробно рассказано в другой статье этого сборника (см. ⁠«Теория сложности»).

Теоремы Гёделя и недоказуемые утверждения. Ещё одним открытием, сделанным гениальным австрийским логиком Куртом Гёделем в 1931 году, было явление непополняемости аксиоматических систем. Знаменитые теоремы Гёделя о неполноте не только оказали большое влияние на развитие математической логики и дали толчок к созданию теории алгоритмов, но и стали общекультурным явлением, затронувшим даже творчество писателей и художников. Гёдель был назван в числе ста наиболее влиятельных личностей XX века по версии журнала Тайм. Однако известность теорем Гёделя приводит и к тому, что часто они интерпретируются в слишком расширительном, метафорическом смысле.

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

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

Целые числа создал Господь Бог,
всё остальное — дело рук человеческих.

(Леопольд Кронекер, 1886 год, Берлин.)

Во‐вторых, должен существовать алгоритм, распознающий, является ли данный текст аксиомой рассматриваемой теории или нет. (Если аксиомы теории нераспознаваемы, то неясно, как можно строить доказательства в такой системе.)

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

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

Теоремы Гёделя позволили построить первые примеры независимых утверждений для сильных систем аксиом, таких как арифметика или даже теория множеств. После работ Гёделя такие примеры были обнаружены среди открытых проблем в различных областях математики. Одной из самых знаменитых открытых проблем в математике была континуум-гипотеза Кантора, в соответствии с которой всякое бесконечное подмножество множества вещественных чисел либо счётно (равномощно множеству натуральных чисел), либо континуально (равномощно множеству вещественных чисел). В 1938 году Гёдель сумел доказать, что эту гипотезу невозможно опровергнуть в теории множеств, а в 1961 году американский математик Пол Коэн установил её недоказуемость.

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

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

Область математики, которая испытала на себе сильное влияние логических методов — это абстрактная алгебра. Соответствующее направление математической логики — теория моделей — возникло в 1940‐х годах в работах А. И. Мальцева в России и А. Тарского и А. Робинсона в США с прицелом на приложения в алгебре. Первые такие приложения были найдены в 1941 году А. И. Мальцевым, который осмыслил доказанную им (а ранее в более слабой форме Гёделем) теорему о компактности для логики предикатов как общий метод получения локальных теорем в алгебре. Оказалось, что методы универсальной алгебры и методы теории моделей весьма близки и понимание взаимосвязей обогатило обе дисциплины. Некоторые конструкции, впервые найденные в математической логике, стали стандартными в алгебре и анализе, например так называемая конструкция ультрапроизведения, придуманная польским логиком Е. Лосем.

Одним из ярких достижений теории моделей 1960‐х годов стало создание нестандартного анализа Абрахамом Робинсоном. Он описал логическую конструкцию, которая позволила непротиворечиво рассматривать пополнение множества вещественных чисел бесконечно малыми и бесконечно большими числами. С помощью этой конструкции стало возможным дать объяснение исходной интуиции лейбницевских «бесконечно малых» и дать технически простое и интуитивное построение основных результатов математического анализа. В дальнейшем эти методы были также использованы и для получения новых результатов.

Современное направление теории моделей, возникшее в работах 1980‐х годов и активно развивающееся в наши дни, установило новые связи между логическими и алгебро-геометрическими методами. Пожалуй, наиболее впечатляющим достижением этого направления было доказательство Э. Хрушовским в 1996 году гипотезы Морделла—Ленга для функциональных полей в любой характеристике, которое было впервые получено в полной общности лишь с использованием методов теории моделей. Не вдаваясь в объяснения этой теоремы, отметим, что речь идёт о сильном результате, связанным с доказанной Г. Фальтингсом в 1984 году гипотезой Морделла о конечности числа рациональных точек на алгебраической кривой (из которой, в частности, вытекает конечность числа возможных решений уравнения Ферма $x^n+y^n=z^n$ при $n>2$).

Методы теории доказательств — области математической логики, изучающей формальную доказуемость — также находят применения в «обычной» математике. Одним из успешных современных направлений является proof mining, извлечение конструктивных оценок из априори неконструктивных математических доказательств. Так называемые функциональные интерпретации, первоначально разработанные для анализа формальных систем, оказалось возможным применить и к конкретным содержательным математическим результатам (например, из области вещественного анализа, где интересен вопрос о скорости сходимости того или иного процесса к неподвижной точке и требуется явная оценка этой скорости). Результаты, полученные логическими методами, часто дают совершенно неочевидные усиления исходных теорем.

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

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

В 1960‐х годах американский учёный T. Кодд понял, что самый обычный язык логики предикатов очень удобен для обеих целей, поскольку позволяет эффективно осуществлять поиск по запросу. Эффективность обеспечивается с помощью аппарата реляционной алгебры — языка операций над отношениями, разработанного до этого в математической логике (в школе Альфреда Тарского) как алгебраический эквивалент языка логики предикатов. Идея Кодда о том, что запросы на языке реляционной алгебры допускают эффективный поиск, была первоначальным стимулом в разработке реляционных баз данных и общеупотребительных в настоящее время языков запросов, таких как SQL. С тех пор теория баз данных и логических языков успешно развиваются рука об руку.

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

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

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

Альтернативный подход, называемый theorem proving, состоит в том, чтобы сопоставить программе логическую формулу, выражающую её корректность, и искать формальное доказательство этой формулы — например, в исчислении предикатов. Этот подход на данный момент не так распространён на практике, как model checking, но продолжает развиваться. Успешность этого метода во многом зависит от эффективности работы пруверов — программ автоматического поиска формальных доказательств. Разработка такого рода систем активно ведётся в наши дни.

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

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

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

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

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

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

Формальные языки с типами (в отличие от бестиповых языков, в которых все переменные имеют один и тот же тип) впервые возникли в фундаментальном труде Б. Рассела и А. Уайтхеда «Основания математики», целью которого было построение математики на основе непротиворечивой системы аксиом теории множеств. В математике эта система, однако, не прижилась и была заменена более простой бестиповой теорией множеств Цермело—Френкеля с аксиомой выбора.

В 1950‐е годы в логике было обнаружено, что в достаточно развитых системах на базе лямбда-исчисления с типами последние ведут себя в точности как логические высказывания (языка интуиционистской логики), а функциональные программы — как формальные доказательства этих высказываний. Это явление, описанное здесь, разумеется, очень приблизительно, получило название соответствия Карри—Говарда. Через несколько десятков лет оно послужило основой для создания функциональных языков, в которых возможно написание программ с одновременной верификацией их кода. Наиболее известными языками такого рода являются Coq и Agda, созданные для формализации математических доказательств. В частности, именно на языке Coq удалось построить формальное доказательство гипотезы четырёх красок и ряда других трудных математических результатов. Эти же языки начинают применяться и для задач верификации программ, описанных в предыдущем пункте.

Этими тремя темами мы ограничим избранный список областей информатики, в которых на деле применяются результаты математической логики. Многие не менее важные темы при этом оказались не затронутыми: теория сложности вычислений, теория автоматов и монадическая логика, SAT-solving, языки авторизации и контроля доступа к информации, логическое программирование и хорнова логика, онтологические базы данных и дескрипционная логика — перечисление можно очень долго продолжать.

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

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

Интуиционизм как философское течение возник в самом начале XX века в работах молодого нидерландского математика Л. Э. Я. Брауэра как реакция на кризис оснований математики и теории множеств. Характерной чертой философии Брауэра было желание избавить математику от неконструктивных теорем существования, т. е. утверждений о существовании тех или иных объектов, без возможности предъявить явно их конструкцию. Глубокий анализ привёл Брауэра к идее о том, что сама классическая логика, а именно закон исключённого третьего, является источником таких неконструктивных утверждений в математике. Это потребовало радикально пересмотреть традиционное понимание смысла математических утверждений, логических операций и кванторов.

Хотя сам Брауэр настаивал на неформальном характере своей философии математики — отсюда её название «интуиционизм» в противоположность гильбертовскому «формализму» — к началу 1930‐х годов возникла потребность в уточнении совокупности логических принципов, приемлемых с интуиционистской точки зрения. Решение этой задачи было дано учеником Брауэра А. Гейтингом, который сформулировал общепринятую в настоящее время интуиционистскую логику предикатов, опираясь на предшествовавшую работу А. Н. Колмогорова. Парадоксально, но в результате интуиционизм был также поставлен на прочную формальную основу.

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

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

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

Модальная логика. Другим классом логик, обогащающих классическую новыми выразительными возможностями, являются так называемые модальные логики. Язык модальной логики, наряду с обычными связками, содержит новую одноместную логическую связку $ □\, $. Высказывание $□\, A$ в разных контекстах может пониматься совершенно по‐разному, что приводит к разным постулируемым принципам, т. е. разным модальным логикам. Стандартные логические связки, такие как импликация или отрицание, как правило, сохраняют в модальной логике классическую интерпретацию. (Разумеется, могут рассматриваться модальные логики и над другими логиками, например над интуиционистской, однако такие системы в целом сложнее и потому менее распространены.)

Исторически первым, идущим ещё от Аристотеля, прочтением формулы $□\, A$ было высказывание «$A$ необходимо». (Здесь мы говорим о языковой конструкции, присутствующей в нашем естественном языке, а не о каком-либо математическом понимании того, что значит «необходимо».) Двойственное высказывание «не $A$ не является необходимым» обычно отождествляется с высказыванием «$A$ возможно» и обозначается $◇\, A$.

Перечислим некоторые известные интерпретации модальности, приводящие к интересным и полезным семействам логик.

Логика доказуемости: $□\, A$ означает «$A$ доказуемо» в данной аксиоматической теории, например в теории множеств. При этом высказывания понимаются как высказывания в языке теории множеств, каковым можно считать и само высказывание о доказуемости утверждения $A$. Эта логика интересна тем, что даёт точную математическую семантику модальности и применяется для исследования обычных классических аксиоматических теорий.

Временная логика, описывающая развитие некоторого процесса во времени: $□\, A$ означает «всегда в будущем будет верно $A$». Различные модели течения времени — непрерывное, дискретное или даже ветвящееся — приводят к разным временным логикам. Временные логики, применяемые на практике для верификации программ, используют и некоторые дополнительные связки, например двухместную связку, выражающую «$A$ имеет место до тех пор, пока $B$».

Эпистемическая логика, описывающая знания и обмен информации между несколькими агентами: $□\,_x A$ означает «агенту $x$ известно $A$» (в этой логике, как правило, описываются знания нескольких агентов $x$, $y$, … и каждому из них соответствует своя модальность $□\,_x$, $□\,_y$, …). Эпистемическая логика является частью (формальной) эпистемологии — обширного и важного раздела философии, занимающегося исследованием таких понятий, как знание и вера, того как знание возникает, как оно связано с понятием доказательства (обоснования). Формализм эпистемической логики позволяет построить модели различных аспектов этих явлений и использовать их для анализа тех или иных теоретических положений.

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

Деонтическая логика формализует модальности типа долженствования, например $□\, A$ можно понимать как «$A$ требуется» или «$A$ обязательно» (двойственную модальность можно понимать как «$A$ разрешено»). Такие логики впервые стали рассматриваться в философии и теории права для формализации и анализа различных аспектов правовых систем.

Многозначная логика и нечёткая логика. Многозначные логики возникают, если допускаются другие истинностные значения, помимо классических истины 1 и лжи 0. Например, можно рассматривать промежуточное значение 1/2 и интерпретировать его как «неизвестно». Следующий шаг требует определения того, каким образом вычисляются значения логических связок, и конкретное решение по этому поводу может привести к различным логикам.

Если пойти дальше по пути многозначности, то естественно возникает идея о том, что истинностным значением высказывания может быть любое вещественное число в интервале $[0,1]$ (например, это число может выражать степень нашей уверенности в справедливости высказывания). Такие логики часто называют «нечёткими» (fuzzy), поскольку предикаты в такой системе могут выглядеть как размытые, не имеющие чётких границ. Например, высказывание о том, что видимый цвет является красным, не является чётким в силу неопределённости самого понятия «красный».

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

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

Аргументы и доказательства, приводимые в суде, могут быть оспорены или опровергнуты противной стороной. Процесс выстраивания аргументов, таким образом, на практике выглядит совершенно непохоже на привычные нам дедуктивные математические доказательства. Эти аспекты изучает теория аргументации — весьма развитая область исследований, связанная с философией, лингвистикой, теорией права и искусственным интеллектом. Формальные модели аргументации во многих случаях базируются на немонотонных логиках.

Паранепротиворечивая логика. Как известно, в классической логике действует закон ex contradictio quodlibet, т. е. из противоречия следует всё что угодно. Поэтому противоречивые классические системы все эквивалентны между собой и, по существу, бесполезны. На практике людям приходится рассуждать в не столь стерильных условиях: не всегда бывает известно, есть ли противоречие в имеющейся информации, на основании которой приходится делать выводы. Логики, приспособленные для рассуждений в условиях возможно противоречивых предположений, называются паранепротиворечивыми. В таких системах возникновение противоречия не приводит к доказуемости всех вообще утверждений.

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

Грамматики Хомского и семантика Монтегю. Одной из теорий, соединивших в себе сразу несколько аспектов неклассических логик — кванторы, предикаты, модальности, модели Крипке и лямбда-абстракцию — является семантика Монтегю. Эта теория, предложенная американским логиком Р. Монтегю в начале 1970‐х годов, представляет собой попытку применить идеи математической логики к трудной задаче описания семантики естественного языка. Она, по существу, положила начало целому направлению в математической лингвистике — формальной семантике. Ранее работы Н. Хомского, создавшего теорию формальных грамматик, произвели революцию в понимании синтаксиса естественных языков. Применения математической логики в лингвистике, из которых мы вскользь упомянули лишь два важных направления, безусловно заслуживают отдельного разговора.

Неужели это всё математика? — недоумённо воскликнет читатель. И да, и нет. Исследователи, применяющие методы математической логики в той или иной области знания, должны прежде всего быть компетентными специалистами именно в этой области и разбираться в постановках специфических для неё задач. Напомним, что многие создатели математической логики — Гёдель, Тьюринг, фон Нейман и др. — не были только лишь «чистыми» математиками.

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

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