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

от силлогизмов до машинной проверки доказательств

Сюжет в одном абзаце

Аристотель замечает, что правильность рассуждения зависит от его формы, а не от содержания, и выписывает все правильные формы списком; стоики строят рядом вторую логику — логику связок «если… то». Потом двадцать два века не происходит почти ничего, и Кант объявляет науку законченной. В ганноверском архиве лежат неопубликованные наброски Лейбница: он мечтает об исчислении, в котором спор разрешается вычислением, — их найдут через двести лет, когда всё уже переоткроют заново. В середине XIX века логика наконец становится математикой: Буль делает её алгеброй, Фреге строит исчисление с кванторами, Пеано выписывает аксиомы арифметики. И тут же выясняется, что фундамент дырявый: письмо Рассела от 16 июня 1902 года выводит противоречие прямо из аксиом Фреге. Математика раскалывается на три программы спасения, из которых самая амбициозная — гильбертовская: формализовать всё и доказать надёжность математики её же средствами. 7 сентября 1930 года в Кёнигсберге двадцатичетырёхлетний Гёдель в проходной реплике объявляет, что это невозможно, — а назавтра в том же городе Гильберт произносит «мы должны знать — мы будем знать». Из руин программы в 1936 году извлекают точное понятие вычисления — трижды и независимо, — и оно оказывается чертежом компьютера. Дальше неразрешимость расходится по всей математике: в алгебру, в теорию чисел, в саму арифметику. А вычисление, рождённое кризисом оснований, возвращается проверять математику: машина, придуманная в 1936 году, проверяет доказательства, которые человек проверить не в силах.

Что делает эту линию особенной

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

Второе: главные результаты здесь отрицательные — и это не поражение. Обычно «доказать, что нельзя» — утешительный приз. Здесь наоборот: неполнота, неопределимость истины, неразрешимость проблемы остановки, независимость континуум-гипотезы — вершины линии, и каждая ценнее того «можно», ради которого затевалась работа. Программа Гильберта не достигла ни одной из своих целей и создала при этом три новых раздела математики.

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

Четвёртое: здесь есть вопросы, у которых нет ответа — и это доказано. Не «пока не нашли», а «не существует». Гипотеза континуума не следует из аксиом и не опровергается ими; то же и с аксиомой выбора. Математика впервые столкнулась с тем, что вопрос может быть поставлен безупречно и всё-таки не иметь решения — не по нашей слабости, а по устройству дела.

Один сквозной сюжет: предмет, говорящий о себе

Если у линии есть главный герой, то это самоописание — и приём, которым его приручили.

Проследите, как он проходит насквозь.

Евбулид (IV в. до н. э.) произносит «это высказывание ложно» — и получает тупик, который два тысячелетия числится курьёзом.
Лейбниц (1679) додумывается кодировать понятия числами: «животное» — 2, «разумное» — 3, «человек» — 6, и вывод превращается в проверку делимости. Мечта — заставить рассуждение вычислять само себя.
Кантор (1891) строит диагональный аргумент: из любого списка последовательностей делается последовательность, в нём отсутствующая. Впервые самоприменение работает не как парадокс, а как инструмент.
Рассел (1902) применяет ту же диагональ к множествам — и обрушивает систему Фреге. Тупик Евбулида добрался до математики.
Гёдель (1931) заменяет в формуле лжеца «ложно» на «недоказуемо» — и парадокс становится теоремой. Приём Лейбница, приём Кантора и фраза Евбулида сходятся в одной конструкции.
Тарский (1933) объясняет, почему замена сработала: доказуемость выразима внутри языка, истина — нет.
Тьюринг (1936) той же диагональю доказывает неразрешимость проблемы остановки — и по дороге строит универсальную машину: устройство, для которого программа есть такие же данные, как всё прочее. Самоописание из беды окончательно превратилось в технологию.
Машинная проверка доказательств (2005) доводит дело до конца: доказательство — это программа, проверка доказательства — её исполнение. Мечта Лейбница исполнена буквально, а её неисполнимая половина честно доказана по дороге.

Одна и та же мысль — «предмет, применённый к самому себе» — сперва ломает логику, потом ломает теорию множеств, потом становится главным доказательным приёмом века, а под конец превращается в работающий инструмент.

Три оговорки, полезные при чтении

Первая: «логика» здесь не значит «умение рассуждать». Это не про риторику и не про то, как выигрывать споры. Математическая логика — раздел математики с определениями, теоремами и вычислениями, и предметом её служат формальные системы: язык, аксиомы, правила вывода. Всё, что тут доказано, доказано о них, а не о человеческом мышлении.

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

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

Открыть на карте

1

Афины ок. 350 г. до н. э.
Аристотель: форма важнее содержания
Первая в истории попытка описать не то, о чём рассуждают, а то, как рассуждают. Аристотель обнаруживает, что правильность вывода зависит только от его формы, и выписывает все правильные формы списком. Кант через двадцать два века объявит науку законченной — ровно за сто лет до того, как она начнётся заново.
2

Милет IV в. до н. э.
Парадокс лжеца
«Это высказывание ложно» — семь слов, из-за которых через двадцать три века рухнет программа Гильберта. Пока же это школьная шутка, которой мегарцы дразнят Аристотеля.
3

Афины ок. 280–206 гг. до н. э.
Хрисипп: логика связок
Вторая античная логика, о которой в школе не говорят: не «все люди смертны», а «если… то». Стоики строят исчисление высказываний с пятью правилами вывода — и всё это будет забыто на два тысячелетия и переоткрыто заново только в XIX веке.
4

Ганновер ок. 1679
«Calculemus!»: мечта Лейбница
Универсальный язык, в котором спор разрешается вычислением: «Подсчитаем!» Наброски остались в архиве и пролежали двести лет, пока всё не изобрели заново. Мечта сбудется наполовину — и доказательство несбыточности второй половины окажется ценнее самой мечты.
5

Корк Линкольн, 1847; Корк, 1854
Буль: законы мысли
Логика становится алгеброй

Сын сапожника, не учившийся в университете ни дня, превращает логику в алгебру, где $x^{2}=x$. Девяносто лет спустя Шеннон покажет: это в точности алгебра релейных схем.
6

Галле 1872–1884
Кантор: множества из рядов Фурье
Актуальная бесконечность: отсюда и парадоксы, и континуум-гипотеза

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

Йена 1879
«Begriffsschrift»: вся современная логика в 88 страницах
Малоизвестный доцент из Йены за одну книжку строит то, чего не было двадцать два века: язык с переменными, кванторами и правилами вывода, на котором записывается любое математическое рассуждение. Книжку почти не заметили — отчасти потому, что читать её было физически невозможно.
8

Турин 1889
Пеано: пять аксиом, из которых следует вся арифметика
Латинская книжка в три десятка страниц задаёт натуральный ряд списком аксиом, последняя из которых — школьный принцип математической индукции. Заодно там впервые появляются значки $\in$, $\supset$, $\cup$, $\cap$. Именно про эту систему через сорок два года будет доказано, что она неполна.
9

Гёттинген 1899
Гильберт: «Основания геометрии»
Аксиоматический метод: смысл слов не должен участвовать в доказательстве

Двадцать одна аксиома вместо пяти постулатов — и требование, чтобы смысл слов «точка» и «прямая» нигде в доказательстве не использовался. Заодно обнаруживается неожиданное: каждой геометрической аксиоме отвечает алгебраическое свойство координат, и теорема Паппа оказывается коммутативностью умножения, записанной фигурами.
10

Йена 16 июня 1902
Письмо Рассела: фундамент выбит
Три строчки в письме разрушают дело двадцати лет: из аксиом Фреге выводится противоречие. Второй том уже в типографии, и автор успевает вписать послесловие — вероятно, самое честное признание в истории науки.
11

Гёттинген теорема о вполне упорядочении — 1904, аксиоматика — 1908
Цермело: аксиома выбора и первая аксиоматика множеств
Доказательство на одну страницу вызывает самый громкий скандал в основаниях за век. Отбиваясь от критиков, Цермело выписывает теорию множеств списком аксиом — и получается фундамент, на котором математика стоит по сей день.
12

Болонья 1905; Львов, 1924
Витали и Банах — Тарский: цена аксиомы выбора
Цена аксиомы выбора: множества, у которых нет объёма

Не всякое множество можно измерить. Витали строит первый пример, а Банах и Тарский доводят дело до предела: шар можно разрезать на пять частей и собрать из них два таких же шара. Обе конструкции опираются на аксиому выбора.
13

Амстердам 1910–1912
Брауэр: неподвижные точки и отречение
Интуиционизм: третья армия оснований

За три года — инвариантность размерности, теорема о неподвижной точке, степень отображения, теорема о причёсывании ежа. Топология получает рабочий арсенал. А затем автор объявляет собственные доказательства незаконными, потому что они неконструктивны, и уходит воевать с Гильбертом.
14

Кембридж т. I — 1910, т. II — 1912, т. III — 1913
«Principia Mathematica»: три тома ради «1+1=2»
Рассел и Уайтхед десять лет выводят арифметику из чистой логики. Теория типов запрещает парадокс — ценой такой громоздкости, что «1+1=2» доказывается в середине второго тома с пометкой «предложение иногда бывает полезно».
15

Кёнигсберг 7 сентября 1930
Кёнигсберг, 7 сентября 1930
На круглом столе двадцатичетырёхлетний Гёдель в проходной реплике объявляет, что во всякой достаточно богатой формальной системе есть истинные, но недоказуемые утверждения. Реплику замечает один человек в зале. Назавтра в том же городе Гильберт произносит «мы должны знать — мы будем знать».
16

Варшава 1933
Тарский: истина невыразима изнутри
Что значит «высказывание истинно»? Тарский даёт первое строгое определение — и тут же доказывает, что внутри самого языка такое определение невозможно. Родная сестра теоремы Гёделя, объясняющая, почему у неполноты нет обходного пути.
17

Принстон «An unsolvable problem…» — апрель 1936, «A note on the Entscheidungsproblem» — 1936
Чёрч: вычисление как подстановка
За семь месяцев до Тьюринга Алонзо Чёрч отвечает Гильберту «нет» — и делает это на языке, где нет ни чисел, ни машин, а есть только функции и подстановка. Из этого языка вырастут функциональное программирование и системы проверки доказательств.
18

Кембридж 1936
Тьюринг: что такое «вычислить»
Чтобы ответить «алгоритма не существует», надо сперва сказать, что такое алгоритм. В 1936 году это сделали трижды и независимо, и все три определения совпали. У Тьюринга определение оказалось не только точным, но и чертежом машины, которой ещё не было.
19

Гёттинген натуральный вывод и секвенции — 1934–1935, непротиворечивость арифметики — 1936
Генцен: непротиворечивость арифметики, доказанная извне
Вторая теорема Гёделя запрещает арифметике доказать собственную непротиворечивость. Генцен доказывает её, выйдя за пределы арифметики ровно на один шаг — и тем самым точно измеряет, насколько именно не хватает средств. Попутно он придумывает тот способ записи доказательств, которым логику преподают сегодня.
20

Иваново 1936
Мальцев: теорема компактности и рождение теории моделей
Теорема, без которой нет ни нестандартного анализа, ни современной теории моделей, доказана преподавателем Ивановского пединститута, куда его распределили после университета. Через пять лет он же покажет, как переводить ею теоремы логики в теоремы алгебры.
21

Стэнфорд Принстон, 1940; Стэнфорд, 1963
Гёдель и Коэн: вопрос без ответа
Вопрос без ответа: первая проблема Гильберта оказалась независимой от аксиом

Есть ли мощность между счётной и континуумом? Гёдель показывает, что «нет» опровергнуть нельзя, Коэн — что доказать тоже нельзя. Вопрос, которому Кантор посвятил жизнь, оказывается неразрешимым в принципе.
22

Москва 1955
П. С. Новиков: проблема тождества слов неразрешима
Неразрешимость приходит в алгебру: слова в группе

Алгоритмическая неразрешимость впервые приходит в обычную алгебру: нельзя написать программу, которая по группе, заданной образующими и соотношениями, скажет, равны ли два слова. Прямой мост от Тьюринга к Матиясевичу.
23

Принстон 1960–61; Лос-Анджелес, 1962–66
Нестандартный анализ: призраки реабилитированы
Теорема компактности в работе: бесконечно малые возвращаются законно

Абрахам Робинсон средствами математической логики строит поле гипердействительных чисел: бесконечно малые существуют законно. Лейбниц был прав — через 230 лет после насмешек Беркли.
24

Кембридж (Массачусетс) гипотеза Ван Хао — 1961, диссертация Бергера — 1964, мемуар — 1966
Ван Хао и Бергер: задача домино неразрешима
Ван Хао свёл кусок логики к задаче о плитках и предположил: если набор замощает плоскость, то замощает и периодически. Его аспирант доказал обратное — построил набор из 20 426 плиток, замощающий плоскость и никогда не повторяющийся, и вывел отсюда, что алгоритма для распознавания замощаемости не существует. Апериодические паркеты родились как побочный продукт теоремы о неразрешимости.
25

Москва 1963 и 1965
Колмогоров: случайно — значит несжимаемо
Через тридцать два года после своих аксиом Колмогоров возвращается к вопросу, который они обошли: что такое случайный объект? Ответ: сложность слова — это длина самой короткой программы, которая его печатает. Миллион нулей печатается коротким циклом; у случайного слова короткой программы нет, его придётся выписать целиком. Случайность перестаёт быть свойством мира и становится свойством описания — и её теперь можно мерить в битах. Годом раньше к тому же понятию независимо пришёл Рэй Соломонов, искавший формализацию индукции.
26

Стокгольм статья — 1966; работа у Колмогорова в Москве — 1964–1965
Мартин-Лёф: случайно — значит проходит все проверки
Швед, приехавший учиться к Колмогорову, доводит определение до конца с другой стороны. Всякая проверка на случайность указывает множество меры нуль — последовательности, подозрительные по какому-то признаку. Проверок бесконечно много, но эффективных, тех, что выполнит машина, — счётное число, и их можно свести в одну, самую сильную. Случайно то, что эту проверку проходит. Позже выяснилось, что получается ровно тот же класс, что и через сложность, — если сложность считать в самоограниченном виде.
27

Йорктаун-Хайтс теорема о неполноте — 1974, число Ω — 1975
Чейтин: число, которое нельзя вычислить
Чейтин строит число Ω — вероятность того, что наугад набранная программа когда-нибудь остановится. Его двоичная запись случайна в самом сильном смысле: ни один кусок не ужимается. Отсюда следствие, стоящее рядом с гёделевым: у всякой формальной системы есть собственный предел сложности, и утверждение «сложность этого слова больше такой-то» она доказать не может. Почти всякое слово случайно — и почти ни про одно этого нельзя доказать.
28

Санкт-Петербург 1970
Десятая проблема Гильберта: ответ — «нет»
Неразрешимость приходит в теорию чисел

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

Манчестер Парис — Харрингтон — 1977, Кирби — Парис — 1982
Кирби и Парис: неполнота приходит в обычную арифметику
Полвека гёделевские недоказуемые утверждения оставались самоссылающимися курьёзами: «я недоказуемо» — не то, что придёт в голову обычному математику. Манчестерские логики предъявляют утверждения о натуральных числах, которые придумал бы кто угодно, — и доказывают, что арифметика Пеано с ними не справляется.
30

Принстон мотивные когомологии — 1996–2000; унивалентные основания — 2006–2013
Воеводский: гомотопии в алгебре и логике
Новые основания: типы как пространства, равенства как пути

Сначала методы теории гомотопий переносятся в алгебраическую геометрию и решают гипотезу Милнора. Потом обнаруживается, что топологически устроена сама логика: типы ведут себя как пространства, а равенства — как пути. Топология, начинавшаяся как раздел геометрии, оказывается кандидатом в основания всей математики.
31

Кембридж доказательство закончено в декабре 2004, объявлено в апреле 2005
Машина проверяет математику
Мечта Лейбница буквально: машина проверяет доказательство, которое человек проверить не мог

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