Математическая логика

Математическая логика – раздел математики, изучающий математические доказательства и вопросы оснований математики. Другими словами, это раздел, в котором законы логики изучаются математическими средствами. Традиционно принято разделять математическую логику на несколько областей исследований – теория моделей, теория доказательств, теория алгоритмов.

До XIX века логика изучалась лишь в рамках философии как «наука о правильном мышлении», «искусство рассуждать» и опиралась на описанные ещё Аристотелем силлогизмы – простейшие виды рассуждений, позволяющие из одних утверждений выводить другие. Математическая логика зародилась в середине 19 века в трудах Дж. Буля (1847) и О. де Моргана (1858) по алгебраизации аристотелевой логики. Позже Готтлоб Фреге (1879) и Чарльз Пирс (1885) в своих работах вводят в язык логики такие понятия, как предикаты, предметные переменные, кванторы, благодаря чему стало возможным применить язык логики к вопросам обоснования математики.

В конце XIX века постепенно возникло понимание того, что математика не имеет достаточно строгого обоснования. Особенно это стало явным после обнаружения парадоксов. Одним из известных является парадокс Рассела: если взять в качестве X множество всех таких множеств, которые не являются своими элементами, то утверждение «X является своим элементом» оказывается одновременно истинным и ложным. Этот парадокс показал, что наивная теория множеств, восходящая ещё к работам Дедекинда и Фреге, на которой базируется математика, содержит противоречия. Для устранения парадоксов Э. Цермело (1908) сформулировал аксиоматическую систему, позже расширенную А. Френкелем и получившую название теории множеств Цермело-Френкеля ZF.

Идея создания универсального языка для всей математики и формализации математических доказательств на базе такого языка выдвигалась ещё Г. Лейбницем в XVII веке. Глубокое развитие этой идеи произошло в конце XIX – начале XX веков, когда возникли аксиоматические системы для таких фундаментальных областей математики, как арифметика, анализ и геометрия. Дж. Пеано (1888) опубликовал свою систему аксиом для арифметики, то есть для теории натуральных чисел. Центральной аксиомой в этой системе является принцип математической индукции: если нам известно, что некоторое свойство верно для числа 0, то есть верно утверждение A(0), а также если мы можем для любого натурального числа n показать, что из A(n) следует A(n+1) , то отсюда следует, что утверждение A(n) верно для любого натурального числа n.

В 1900 году на международном конгрессе математиков Давид Гильберт сформулировал 23 проблемы, которые, как он считал, должны стать ключевыми в развитии математики XX века. Первая проблема состояла в доказательстве континуум-гипотезы (всякое подмножество вещественных чисел является либо конечным, либо счетным, т.е. равномощно множеству натуральных чисел, либо континуальным, т.е. равномощно множеству всех вещественных чисел). Вторая проблема связана с основаниями математики и заключается в доказательстве непротиворечивости системы аксиом арифметики Пеано. Гильберт позже сформулировал программу обоснования математики. Она заключается в том, чтобы создать точный язык для математических утверждений, сформулировать в этом языке систему аксиом, достаточную для получения математических теорем, и строгими математическими средствами доказать непротиворечивость этой системы.

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

Гильбертовская программа в полном её виде оказалась неосуществимой. Австрийский математик Курт Гёдель (1931) получил результаты, известные как теоремы о неполноте, из которых следует, что непротиворечивость аксиом арифметики Пеано невозможно доказать исходя из самих аксиом арифметики. Это же верно и для более сильных систем аксиом, в частности, для системы, описанной в труде Уайтхеда и Рассела, а также для теории множеств Цермело–Френкеля. Более точно, во всякой такой системе, если она непротиворечива, имеется утверждение, которое истинно, но не доказуемо в этой теории. Причем можно даже привести конкретный пример такого истинного недоказуемого утверждения – это утверждение, «означающее» непротиворечивость данной теории (Гёдель показал, что такое утверждение можно записать, причем для этого требуется лишь язык арифметики). Для формального доказательства непротиворечивости аксиом арифметики требуются средства, выходящие за ее рамки. Так, Г. Генцен (1936) доказал непротиворечивость арифметики, однако для этого ему пришлось прибегнуть к трансфинитной индукции.

Среди проблем Гильберта имеется 10-я проблема, которая состоит в нахождении универсального метода определения того, существует ли целочисленное решение у уравнения вида , где P – многочлен от нескольких переменных с целочисленными коэффициентами. То, что в формулировке этой проблемы названо «универсальным методом», позже было формализовано в виде понятия алгоритм. До того времени математикам обычно приходилось доказывать существование алгоритма путем его предъявления. Для этих целей не требуется точного определения, что такое алгоритм. Однако многочисленные попытки положительно решить 10-ю проблему Гильберта, то есть предъявить алгоритм, не приводили к успеху (были получены лишь частичные методы решения для очень узких классов уравнений). Это привело к гипотезе о том, что необходимо пытаться отрицательно решить эту проблему, то есть доказать, что алгоритма не существует. Чтобы иметь возможность доказывать отсутствие алгоритма строгими математическими средствами, необходимо точно определить само понятие алгоритма.

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

Уточнение представления о вычислимости на основе понятия машины Тьюринга (и других эквивалентных ей понятий) открыло возможности для строгого доказательства алгоритмической неразрешимости различных массовых проблем. Уже в течение первого десятилетия после формализации понятия алгоритма удалось установить неразрешимость множества проблем как в теории алгоритмов, так и в других разделах математической логики. Так, А. Тьюринг (1936) доказал, что неразрешима проблема остановки: по описанию алгоритма и его исходным данным определить, остановится ли за конечное время этот алгоритм на этих данных, или будет работать бесконечно долго. А. Чёрч (1936) и А. Тьюринг (1937) показали, что не существует алгоритма, проверяющего истинность утверждений арифметики Пеано, а также истинность формул логики предикатов. Последний результат означает, что неосуществима ещё одна часть Гильбертовской программы обоснования математики – предъявить алгоритм, который по описанию математической теории и предложению в языке этой теории отвечал бы на вопрос, является ли это предложение истинным в данной теории (то есть следует из теории).

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

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

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

Изначально теория моделей развивалась применительно к классической логике первого порядка, известной также как логика предикатов. Первым результатом, появившимся задолго до «официального» возникновения теории моделей, принято считать теорему Лёвенгейма–Сколема (1915): если множество предложений в счётном языке первого порядка имеет бесконечную модель, то оно имеет и счётную модель.

Одним из важнейших инструментов теории моделей является теорема компактности, доказанная К. Гёделем (1930) и А.И. Мальцевым (1936). Она утверждает, что множество формул первого порядка имеет модель тогда и только тогда, когда каждое его конечное подмножество имеет модель. Из этой теоремы вытекает, в частности, что если множество формул имеет сколь угодно большие конечные модели, то оно имеет и бесконечную модель. Как следствие, оказывается, что некоторые понятия не являются выразимыми в логике первого порядка. Например, понятия конечности или счётности модели не могут быть выражены никакими формулами первого порядка и даже никакими множествами формул.

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

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

Исчисления гильбертовского типа были построены для многих важнейших логик, таких как логика высказываний и логика первого порядка (она же логика предикатов). Известная теорема о полноте исчисления предикатов, доказанная Гёделем (1929), устанавливает связь между истинностью и доказуемостью: формула первого порядка истинна (во всех моделях) тогда и только тогда, когда она доказуема в гильбертовском исчислении предикатов.

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

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

Теория вычислимости изучает свойства вычислимых функций, а также вычислимую сводимость одних задач к другим. Классическим результатом в этой области является теорема Райса–Успенского: никакое нетривиальное свойство вычислимых функций невозможно распознать алгоритмически. Здесь нетривиальными называются такие свойства, что существуют функции, обладающие ими, и функции, не обладающие ими. Таким образом, по тексту программы невозможно распознать какое-либо свойство функции, которая этой программой вычисляется: например, является ли эта функция константной, или возрастающей функцией, определена ли она в точке 0, принимает ли она в точке 5 значение 7.

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

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