Что такое математическая логика и как она связана с языками программирования? Почему она находится на стыке математики и гуманитарного знания и какие прикладные возможности открывает? Об этом наш разговор с главным научным сотрудником математического института им. В.А. Стеклова РАН, руководителем отдела математической логики академиком Львом Дмитриевичем Беклемишевым.
— Лев Дмитриевич, всю свою сознательную научную жизнь вы занимаетесь математической логикой. Что это за наука, чем она отличается от других видов логики, в частности от женской?
― Наверное, некоторые читали заметки моего отца, профессора МФТИ Дмитрия Владимировича Беклемишева по поводу женской логики. Они были написаны очень давно, еще, наверное, в 1970-е гг., потом вышли в юмористическом сборнике Физтеха. По нынешним временам это апофеоз политнекорректности, но они пользовались популярностью. Так что по поводу женской логики читайте моего отца.
― Интересно, а женщина-математик может обладать женской логикой?
― Да, и примером тому моя мама, которая тоже была профессором МФТИ и замечательным преподавателем. Она отчасти и вдохновила отца на написание этих иронических заметок. Но, справедливости ради, уже там сказано, что даже и некоторые мужчины умело пользуются женской логикой. Хотя все это не имеет отношения к логике математической.
А я пришел в эту специальность, еще будучи студентом механико-математического факультета МГУ. Моими учителями были Сергей Иванович Адян, впоследствии ставший академиком, заведовавший отделом в нашем институте, и профессор Сергей Николаевич Артемов.
Чем интересна математическая логика и что это за наука? Если заглянуть в разные словари и энциклопедии, можно найти разные, иногда противоречащие друг другу определения того, что составляет предмет логики. Традиционно логика считается наукой о правильных рассуждениях. Думаю, в наше время лучше говорить о том, что математическая логика ― это наука о формальных языках. Точнее, это построение и исследование формальных языков математическими методами. Если в конце XIX в., когда закладывались основы математической логики, примеров развитых формальных языков практически не было, то в наши дни они встречаются повсюду, например в каждом мобильном телефоне. Это языки программирования, языки баз данных. Все это стало практическим применением тех идей и концепций, которые начали разрабатываться логиками в конце XIX — начале XX в.
― Насколько я знаю, первые формальные языки не были связаны с компьютерами?
― Совершенно верно, компьютеров еще не было. А связано это было с тем, что на рубеже XIX–XX вв. в математике возник так называемый кризис оснований. К концу XIX в. математика была поставлена на строгие рельсы теории множеств, созданной великим математиком Георгом Кантором. Математический анализ, теория вещественных чисел и функций получили строгое обоснование, люди уже не рассуждали о пределах в несколько туманных терминах бесконечно малых и бесконечно больших, и все, казалось, было очень хорошо, но в какой-то момент в теории множеств обнаружились противоречия.
― Речь идет о парадоксе Кантора?
― Да, Кантор доказал теорему о том, что нельзя установить взаимно однозначное соответствие между элементами любого множества и всеми его подмножествами. Парадокс Кантора состоит в том, что если мы возьмем множество всех множеств вообще, то оно содержит множество всех своих подмножеств, а значит, для него можно определить такое соответствие.
Потом были придуманы и более наглядные парадоксы, например парадокс Рассела, популярная версия которого ― парадокс брадобрея: брадобрей должен брить всех людей, которые сами себя не бреют, но должен ли он при этом брить сам себя? Оказалось, что причины парадоксов теории множеств довольно глубокие и существуют различные пути решения этих проблем. Чтобы разобраться во всем этом, математики заинтересовались основаниями своей науки, например следующими вопросами: в каком смысле существуют те или иные математические объекты, как построить непротиворечивую систему аксиом для математики, и вообще, что значит доказать математическую теорему?
― А что это значит?
― Вопрос этот не такой простой. Математические факты делятся на истинные и ложные. Но истинность и доказуемость ― это одно и то же? Всякое ли истинное утверждение можно доказать? В какой-то момент математики поняли, что эти вопросы выходят за рамки самой привычной математики. Математические утверждения, доказательства ― это объекты совсем другой природы, несвойственные математике XIX в. и более глубокого прошлого.
― Это что-то отчасти философское?
― Это абсолютно философская вещь. Математики обратились к этой науке ― логике, которая существовала еще со времен Аристотеля как часть философии. Она столь же древняя, как и математика. Математики начали анализировать логику своими математическими средствами, приспосабливать результаты из логики к своим собственным проблемам. Это привело к созданию первых формальных языков, описывающих те неформальные рассуждения, которыми пользуются математики. В результате математические рассуждения сами по себе стали точным математическим объектом, который можно так же анализировать средствами самой математики. Так родилась математическая логика.
А создание первых формальных языков привело к анализу таких понятий, как «алгоритм» и «вычисление». В частности, Алан Тьюринг, знаменитый логик, предложил одну из первых, как сейчас говорят, универсальных вычислительных моделей, появилось точное математическое определение вычислимой функции.
В те времена электронных компьютеров еще не было, компьютерами называли людей, как правило, женщин, коллективно выполнявших сложные математические расчеты для каких-нибудь целей вроде дешифровки. Так что компьютер ― это была профессия. После того как сама концепция вычислимости была понята и проанализирована, удалось, как мы знаем, создать реальные универсальные вычислительные устройства, компьютеры. Плоды этого мы все сейчас пожинаем. Таким образом, математическая логика стала источником того, что сейчас называется теоретической информатикой.
― Чем эта наука вам интересна?
― Она применяет математику к исследованию таких предметов, которые от нее весьма далеки. Это некоторое вторжение математики в гуманитарную область.
― Можно ли сказать, что математическая логика ― это тоже гуманитарная наука?
― Не совсем так. Это математическая наука, связанная с гуманитарной частью знания человечества. Это попытка математики применить свои методы к анализу чего-то, исходно относящегося к гуманитарному знанию. В этом отношении логика близка к такой науке, как лингвистика, которая изучает естественные человеческие языки, их структуру. Между формальными и естественными языками есть много общего. Конечно, естественные языки много сложнее, они не созданы искусственно, а развиваются по своим законам. Но грамматическая структура фразы русского языка довольно жесткая, и можно довольно четко отделить правильно построенные предложения от построенных неправильно. Мы говорим о синтаксисе ― это внешняя сторона языка.
Так же и у формальных языков есть четкие правила грамматики, там уже все строго фиксировано, и есть семантика ― то, какой смысл описывают правильно построенные высказывания. В лингвистике даже есть отдельная область ― семантика, изучающая смысл высказываний естественного языка.
― И в математической логике тоже есть семантика?
― Конечно, в математической логике есть семантика, изучающая структуры, описываемые формальными языками. Соответствующая область называется теорией моделей. А есть синтаксические области. Вот теория доказательств, например, изучает науку о формальных доказательствах ― то, как устроено правильно построенное доказательство и т.д. Сюда примыкает важный вопрос о том, какими средствами и можно ли в принципе доказать то или иное математическое утверждение.
Например, в знаменитом списке проблем Давида Гильберта первым номером шла так называемая проблема континуума Кантора. Это проблема о том, существует ли множество на прямой промежуточной мощности между счетными и континуальными. То есть всякое ли бесконечное подмножество прямой равномощно либо множеству натуральных чисел, либо множеству всех действительных чисел.
Долгое время математики бились над решением этой задачи, но не могли получить ее решение. В конце концов, в работах Геделя и Коэна было установлено, что это утверждение нельзя ни доказать, ни опровергнуть на основе общепринятых аксиом теории множеств. Такие примеры потом находились и в других областях математики. Оказалось, что наши математические методы, заложенные в системах аксиом, как правило, неполные. Об этом гласит знаменитая теорема Геделя о неполноте. И это пример результата из логики, который выходит далеко за рамки чисто логических или математических применений. Эта теорема имеет глубокие общефилософские и даже мировоззренческие следствия.
― Лев Дмитриевич, расскажите о том, чем вы сейчас заняты конкретно, какие вопросы в области математической логики решаете.
― Мои исследования относятся к теории доказательств и как раз ровно к вопросу о доказуемом и недоказуемом. Поскольку математические теории, с которыми имеют дело математики, оказались неполными, нет какой-то одной универсальной системы, пригодной для всех случаев жизни. И возникает задача сравнивать между собой разные системы аксиом. В одной из них можно больше доказать чего-то, в другой меньше, а если взять какие-то две разные теории, сформулированные в разных терминах, как их сравнить между собой?
Есть подходы, позволяющие это сделать. Такого рода вещи сейчас изучает часть математической логики, которая называется теорией доказательств. Меня интересовала область, в которую я внес некоторый вклад, ― это утверждения, элементарные по своей природе, касающиеся конечных объектов, например натуральных чисел или конечных последовательностей букв, которые можно доказать только с использованием аппарата теории бесконечных множеств. Такого рода утверждения можно объяснить школьнику, поскольку они очень простые, но вот доказать их он не сможет. Средствами системы аксиом арифметики, которая описывает конечные объекты, их в принципе доказать нельзя.
― А невозможность доказательства — не признак того, что это неверное утверждение?
― В данном случае нет. Его можно доказать, но с использованием более сильных средств.
― Что это значит?
― Более сильных ― значит, приняв больше абстрактных принципов. Ведь как устроена теория множеств? Это логический язык, на котором построено основное здание существующей математики. Она исходит из представления о том, что совокупность предметов любой природы, конечная или бесконечная, может рассматриваться как самостоятельный объект. Например, прямая в геометрии ― это множество всех ее точек. Можно рассматривать и множества, состоящие из множеств, и множества, состоящие из множеств множеств.
Теория множеств имеет такое свойство, что, с одной стороны, эти абстракции кажутся очевидными, но этот взгляд поверхностный, потому что исходит из нашей интуиции относительно конечных, обозримых совокупностей. А математики применяют эти представления более широко, к бесконечным множествам. И есть ли эти математические абстракции на самом деле? Можете ли вы себе представить, скажем, произвольное подмножество множества натуральных чисел? Ответ будет такой: некоторые можем, но не все, потому что всех, как известно, континуум, то есть их примерно столько же, сколько точек на прямой.
― То есть бесконечное количество, а этого наше сознание вместить не может.
― Они не очень укладываются в наше сознание. Так что здесь бывают подвохи.
― Я поймала себя на мысли, что машина, даже самая умная, никогда не сможет просчитать все эти вещи, поскольку здесь идет речь об абстракциях, о каких-то вещах неалгоритмических, которые в машину заложить нельзя.
― Совершенно верно. Мы говорим о некоторой, как сказал бы философ, абстракции, которая находится в платоновском мире идей. Это вещь, которой нет в материальном мире. Поэтому правомерно или нет их использование ― вопрос совершенно неочевидный. Есть взгляды на основания математики, которые противоречат такой точке зрения, они считают неправомерным использование произвольных подмножеств натурального ряда.
― А что будет, если принять эту точку зрения?
― Тогда наша математика преобразуется. Тогда мы чего-то лишаемся. И какие-то из принятых нами теорем оказываются недоказанными или даже неверными.
― Для чего все эти сложности, если они не имеют отношения к реальности и, возможно, их вовсе нет?
― Действительно, зачем мы подсчитываем чертей на кончике иглы? Говорить, что математические абстракции не имеют отношения к реальности, конечно же, неправильно. Они для того и были придуманы, что очень хорошо, иногда очень точно описывают окружающую нас физическую реальность. Но сами по себе они не принадлежат к этой реальности.
Ситуация на самом деле еще более удивительная. Как показал Курт Гедель, принятие абстрактных понятий и принципов позволяет нам доказать больше совершенно конкретных утверждений про конечные объекты, которые нельзя было бы доказать, исходя только из представления о том, что у нас все конечно. Такого рода следствия можно проверять на конкретных примерах и каждый раз убеждаться в том, что математика не ошиблась. Так что эти бесконечные абстракции не врут. Но они сформулированы в непроверяемых на практике терминах. Всякая проверка только частичная.
― Все это выглядит как абсолютно фундаментальная вещь, не могущая иметь никакого прикладного выхода. В то же время вы рассказали о том, что появление противоречий в математике в свое время привело к созданию формальных языков и, соответственно, появился интернет, без которого мы сейчас жить не можем. Видите ли вы какие-то новые возможности, к которым может привести ваша наука?
— У логики, конечно, больше применений в компьютерной науке, в теоретической информатике, чем в традиционной математике. Ведь математические утверждения, которые не доказуемы и не опровержимы, возникают довольно редко. А что касается информатики, то все ровно наоборот: в ней много реально возникающих на практике задач, связанных с математической логикой.
― Можете привести примеры?
― Как известно, в наше время компьютеры в основном обрабатывают информацию, которая содержится в тех или иных базах данных. Базы данных ― это какие-то сведения, организованные в большую таблицу. Потом пользователь задает этой базе данных какие-то вопросы, а она должна уметь дать на них быстрый ответ. На каком языке пользователь должен задавать эти вопросы? Эти языки очень близки к тем самым логическим языкам, которые были придуманы для описания математических теорий, ― так называемым языкам логики первого порядка. Теперь теория баз данных, по сути своей, основывается на этом.
Есть еще один хороший пример, показывающий связь между логикой, информатикой и практикой. Простейший логический язык, известный со времен Аристотеля, — это язык логики высказываний, когда у нас есть переменные, означающие высказывания, которые могут быть истинными или ложными, и есть логические связки «и», «или», «не». Формулы, которые мы можем построить с помощью этих связок из переменных, обозначают сложные высказывания. Такие формулы могут быть выполнимыми или невыполнимыми.
― Что это значит?
― Существуют тождественно истинные формулы, которые будут всегда иметь значение истины, при любых значениях переменных. Есть тождественно ложные формулы, которые всегда ложные. А есть формулы, которые не всегда истинные и не всегда ложные, их большинство. Распознание того, будет ли истинным данное высказывание при некоторых значениях переменных, и называется задачей выполнимости.
― Это опять какая-то абстракция?
― Вовсе нет. Все эти формулы заложены в наши компьютеры на уровне микросхем, и это уже давно не новость. Чуть менее известно вот что. Одна из наиболее известных математических проблем, за решение которой полагается премия в миллион долларов, называется проблемой P = NP. Простейшая формулировка этой задачи состоит в вопросе, существует ли алгоритм, который проверяет данную формулу на выполнимость за полиномиальное число шагов от числа ее переменных. Понятно, что переборный алгоритм решает эту задачу, но такой алгоритм неэффективен, он работает экспоненциальное число шагов от числа переменных в формуле. Это означает, что если формула очень большая, то нет никаких шансов таким способом ее вычислить за приемлемое время.
― Так какой же алгоритм эффективен?
― Как ни странно, математики до сих пор не знают, существует ли более эффективный алгоритм, чтобы решать эту задачу. Сделано очень много попыток, каждый год публикуются новые варианты, некоторые думают, что такой алгоритм построить можно, но бóльшая часть специалистов считают, что такого алгоритма в принципе не существует.
― А вы как считаете?
― Я человек сомневающийся. Когда я был студентом, эта задача была уже очень широко известна и общепринятая точка зрения состояла в том, что такого алгоритма, конечно же, нет, и нужно доказать, что его не существует. Понятно, что доказать, что алгоритма не существует, значительно сложнее, чем предъявить алгоритм, когда он есть. Но тогда считалось неприличным даже думать иначе.
Однако с тех пор много что произошло. Были некоторые другие задачи, выглядевшие похожими на эту. Например, существует ли полиномиальный алгоритм проверки данного натурального числа на простоту (то есть простое это число или нет). Там тоже надо перебирать все делители данного числа, но это неэффективно. И тоже все думали, что вряд ли что-то получится. Были вероятностные алгоритмы, которые эффективно решали эту задачу, но в то, что может существовать детерминированный алгоритм, никто особо не верил. А потом индийские математики придумали полиномиальный алгоритм. Он оказался не такой уж сложный, и он эту задачу решил. Это, конечно, была научная сенсация. Так что бывает и так: все верят во что-то одно, а в итоге оказывается по-другому. Это наука.
Но я хочу сказать о другом. Эта задача относится к дискретной математике, математической логике. Однако она интересна и с практической точки зрения. Оказывается (и это тоже известно уже довольно давно), многие возникающие на практике переборные задачи сводятся к этой; если мы научимся ее эффективно решать, то сможем решать и другие.
― Но при этом вы говорите, что математики не могут эффективно решить эту задачу…
― Неизвестен алгоритм, который эффективно решал бы эту задачу на любых исходных данных. Но все равно эти задачи нужно решать на практике, поэтому и родилась некоторая отдельная дисциплина, которая называется «решение задач выполнимости булевых формул» (SAT solving). В ней изучаются эвристические алгоритмы, решающие эту задачу. За последние десятилетия был достигнут очень большой прогресс именно в таком эвристическом решении, то есть в построении алгоритмов, работающих эффективно на практике, хотя и не во всех теоретически возможных случаях.
Эти SAT solvers ― очень большая работа, которую хорошо финансируют, потому что разработчики заинтересованы в решении этой задачи. В этой области достигнут значительный прогресс, и на практике такие алгоритмы сейчас работают очень эффективно. Эта деятельность показывает связь математики и инженерии.
― Лев Дмитриевич, занятия математической логикой каким-то образом помогают вам в повседневной жизни?
― Если говорить о конкретных результатах, то нет. Но вообще занятие наукой, я думаю, помогает в повседневной жизни. Ученые дольше живут, и не потому, что якобы умнее, а просто люди, которые работают головой, позже впадают в деменцию. Я думаю, что статистика это подтвердит. И про математиков это тоже можно сказать. Да и вообще, математика ― наука красивая, что бы о ней ни думали непосвященные. Настоящая серьезная наука открывает перед человеком разнообразные потрясающие вещи. В занятиях ею есть эстетическое удовольствие.
― Иван Ефремов называл красоту наивысшей целесообразностью.
― И красота ― это признак хорошей математики, можно так сказать. Если математика некрасива, значит что-то там не так.
― Вы стремитесь достигнуть этой гармонии?
― Да. Любой математик хочет достигнуть красоты, ясности, простоты, поскольку математика ― предмет довольно сложный. Главное, к чему мы стремимся как ученые, ― чтобы все было проще. Тогда эту красоту легче разглядеть.
