Карта → событие
«Principia Mathematica»: три тома ради «1+1=2»
Починка вместо отказа
Обнаружив противоречие у Фреге, Рассел не стал хоронить логицизм. Он рассудил так: цель верна, ошибка в одном месте — надо найти общий источник всех известных парадоксов и запретить его.
Источник, по Расселу, — порочный круг: определение объекта через совокупность, к которой он сам принадлежит. Лжец говорит обо всех высказываниях, включая себя. Расселово множество определено через все множества, включая себя. Лекарство: устроить язык так, чтобы такие определения было невозможно записать.
Так появляется теория типов.
Предметы получают тип 0. Свойства предметов — тип 1. Свойства свойств — тип 2. И так далее. Запись $x \in y$ осмысленна только тогда, когда тип $y$ ровно на единицу выше типа $x$. Выражение $x \in x$ теперь не ложно — оно бессмысленно, как «зелёная идея спит»: грамматика языка его не порождает.
Парадокс исчезает. Но вместе с ним исчезает и много полезного, и приходится доплачивать.
Как типы разбирают лжеца — и почему одних типов не хватило
Возьмём лжеца в форме «всякое высказывание, которое я произношу, ложно». Если предметы имеют тип 0, а высказывания о предметах — тип 1, то это высказывание говорит обо всех высказываниях сразу, включая себя. По Расселу такая фраза не имеет типа и потому не является высказыванием вовсе.
Красиво. Беда в том, что тем же ножом отрезается и вполне законная математика.
Определение точной верхней грани звучит так: $\sup A$ — наименьшее из чисел, ограничивающих $A$ сверху. Здесь мы определяем число через совокупность всех ограничивающих чисел, среди которых находится и определяемое. Это тот самый порочный круг — определение называется непредикативным.
Рассел был последователен и запретил их тоже: в разветвлённой теории типов свойства делятся ещё и по «порядкам», и определение через совокупность свойств данного порядка даёт свойство порядком выше. Но тогда $\sup A$ живёт этажом выше, чем элементы $A$, и обычная теорема о верхней грани перестаёт формулироваться. Анализ рушится.
Чтобы поднять его обратно, вводится аксиома сводимости: всякому свойству любого порядка равносильно свойство самого низкого порядка. Она возвращает анализ на место — и одновременно сводит на нет весь смысл разделения на порядки. РамсейФрэнк Пламптон РамсейДоказал, что полный беспорядок невозможен: в любой достаточно большой структуре найдётся большой упорядоченный кусок. Теорема была у него вспомогательной леммой. Умер в двадцать шесть лет, успев основать три… и сам Рассел позднее признавали её чужеродной; во втором издании (1925–1927) Рассел пытался без неё обойтись и не смог.
Аксиома сводимости. В полной («разветвлённой») версии типы дробятся ещё и по порядкам, и в такой системе разваливается обычный анализ: определение точной верхней грани через все ограничивающие множества оказывается запрещённым. Чтобы этого не случилось, Рассел вводит аксиому, объявляющую, что всякому свойству высшего порядка равносильно свойство низшего. Аксиома спасает анализ, но выглядит как заплата, и сам Рассел этого не скрывал.
Аксиома бесконечности. Что предметов бесконечно много, из логики не следует — приходится потребовать.
Аксиома выбора. Она же, под именем «мультипликативной аксиомы».
Три допущения, ни одно из которых не является логическим законом. Уже поэтому программа «арифметика есть часть логики» в исходном виде не удалась: три раза пришлось выйти за пределы логики.
Десять лет и «1+1=2»
Работа шла с 1900 по 1910 год. Альфред Норт Уайтхед и его бывший ученик Рассел писали посменно, обмениваясь листами; Рассел вспоминал, что рукопись первого тома пришлось везти в типографию на извозчике — она весила больше, чем можно было унести.
В первом томе, на 379-й странице, стоит предложение $*54{.}43$ с примечанием: отсюда будет следовать, что $1+1=2$, — когда сложение будет определено. Само определение появляется позже, и сама теорема доказывается во втором томе, предложение $*110{.}643$. При ней стоит замечание авторов:
Приведённое предложение иногда бывает полезно.
Шутка вошла в фольклор, и над ней принято смеяться. Смеяться стоит осторожно: три тома доказывают не «$1+1=2$», а нечто иное — что арифметику можно развернуть из явно выписанного списка правил, ни разу не сославшись на очевидность. Триста семьдесят девять страниц — это цена честности, а не глупости.
Издание
Издательство Кембриджского университета оценило убыток от книги в 600 фунтов. Триста оно согласилось взять на себя, двести дало Королевское общество, оставшиеся сто внесли авторы — по пятьдесят каждый.
Расселу принадлежит подсчёт: за десять лет труда они заработали по минус пятьдесят фунтов на человека.
Четвёртый том, о геометрии, Уайтхед так и не закончил. Оба автора после «Principia» ушли из математической логики: Уайтхед — в философию природы, Рассел — в теорию познания, публицистику и политику. Рассел писал, что его ум так и не оправился от напряжения этих лет.
Что осталось
Обозначения. Значки Пеано, пропущенные через «Principia», стали общематематическими. Так же и слова: «пропозициональная функция», «область значений», сама привычка писать $\forall$ и $\exists$.
Теория типов. Заплата 1910 года оказалась долгоживущей идеей. Из неё выросли системы типов в языках программирования, а прямая наследница — теория типов Мартина-Лёфа — лежит в основе современных систем проверки доказательств и унивалентных оснований Воеводского. То, что Рассел придумал как ограничение, стало способом писать программы и доказательства на одном языке.
Образец формальной системы. Именно «Principia» стала тем конкретным предметом, на котором проверили, чего вообще можно достичь формализацией. Работа Гёделя 1931 года называется «О формально неразрешимых предложениях „Principia Mathematica" и родственных систем» — и доказывает, что в этой самой системе есть истинные утверждения, которые в ней не выводятся.
Три тома строили здание, о котором через восемнадцать лет было доказано, что достроить его до конца нельзя ни в каком варианте. Это не обесценило работу: чтобы доказать теорему о всех формальных системах, нужно было сперва увидеть хоть одну достаточно полную — и увидели её здесь.
Для класса
Теория типов запрещает запись $x \in x$. Проверьте, что она заодно запрещает и следующие две вещи, и решите, жалко ли их.
- Множество всех множеств.
- Тождественное отображение $\mathrm{id}(x) = x$, определённое сразу на всём.
(Ответ: 1 — запрещено: элементы этого множества имели бы все типы сразу, а у множества тип обязан быть один. Не жалко: именно оно и порождает парадокс. 2 — тоже запрещено, и вот это жалко: тождественное отображение приходится заводить отдельно на каждом типе, а значит, их бесконечно много и все они разные. Такая «размноженность» — обычная плата за типизацию; ровно с ней же имеют дело сегодняшние языки программирования, и лечат её тем, что называется полиморфизмом.)
Следующая точка: Кёнигсберг, сентябрь 1930 года.