«Calculemus!»: мечта Лейбница

Придворный библиотекарь

С 1676 года и до смерти в 1716-м Готфрид Вильгельм Лейбниц служит в Ганновере библиотекарем и советником герцогов Брауншвейг-Люнебургских. Должность оставляет время: за эти сорок лет он изобретает знак интеграла, строит счётную машину со ступенчатым валиком, пишет о праве, теологии, китайской философии и генеалогии герцогского дома — и попутно затевает нечто, чему в его веке не находится ни названия, ни применения.

Замысел был такой. Нужен искусственный язык — characteristica universalis, «универсальная характеристика», — в котором каждое простое понятие обозначено своим знаком, а сложное собирается из простых по правилам. Такому языку положено «исчисление рассуждений», calculus ratiocinator: правила преобразования знаков, при которых из истинных посылок получаются только истинные следствия.

Что тогда будет? Знаменитый ответ — из работы «Об искусстве открытия» (1685):

…когда возникнут споры, двум философам не придётся спорить больше, чем двум счетоводам. Довольно будет взять перья, сесть за доски и сказать друг другу (позвав, если угодно, приятеля в свидетели): подсчитаем.

Calculemus. Подсчитаем.

Как он это делал: простые числа вместо понятий

Мечта — это одно, а Лейбниц ещё и считал. В апреле 1679 года он пробует конкретную конструкцию, и она поразительна.

Каждому простому понятию приписывается простое число. Составное понятие — произведение.

Пусть «животное» $= 2$, «разумное» $= 3$. Тогда «человек» $= 2\cdot 3 = 6$.

Теперь утверждение «всякий человек есть животное» превращается в арифметическую проверку: делится ли 6 на 2? Делится — значит, истинно. А «всякое животное есть человек» — делится ли 2 на 6? Не делится — ложно.

Силлогизм Barbara становится транзитивностью делимости: если $c$ делится на $b$, а $b$ делится на $a$, то $c$ делится на $a$.

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

С отрицательными и частными суждениями схема забуксовала, Лейбниц бросил её и пробовал другие: у него есть наброски, где логические операции ведут себя как сложение и умножение, где отмечено, что «$a$ и $a$ есть $a$» (сегодня это называется идемпотентностью и отличает алгебру Буля от обычной), и где выписаны законы, которые мы бы назвали дистрибутивностью.

Ящик стола

Ничего из этого он не напечатал.

Логические рукописи пролежали в ганноверской библиотеке двести с лишним лет. Отдельные куски публиковались в XIX веке, но систематически их разобрал только Луи Кутюра — книга «Логика Лейбница» (1901) и том неизданных фрагментов (1903).

К этому времени Буль уже пятьдесят лет как построил алгебру логики, Фреге двадцать лет как построил исчисление предикатов, а ПеаноДжузеппе Пеаноитальянский математик и логик · 1858–1932Аксиоматизировал натуральный ряд, векторное пространство и математическую запись — и построил кривую, которая проходит через каждую точку квадрата. ввёл значки, которыми мы пользуемся сегодня. Всё сделали заново, ничего не зная о предшественнике.

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

Что сбылось и что не сбылось

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

Сбылось: язык. Формальный язык, в котором каждое математическое утверждение записывается однозначно, построен — Фреге, Пеано, Расселом и Уайтхедом, Цермело. Сегодня всякий работающий математик уверен: любое его рассуждение при желании записывается формально. Это и есть characteristica universalis.

Сбылось: машина. «Взять перья и сесть за доски» — теперь это делает компьютер, и системы проверки доказательств действительно разрешают спор о правильности вывода вычислением, буквально по Лейбницу. Программа Coq не спорит: она считает.

Не сбылось: разрешение любого спора. Лейбниц полагал, что вычисление даст ответ на всякий вопрос — надо только достаточно долго считать. Именно это оказалось невозможным, и доказано это дважды: Гёделем в 1931-м (есть истинные утверждения, которые не выводятся) и Тьюрингом в 1936-м (нет процедуры, определяющей по утверждению, выводится оно или нет).

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

Следующая точка: Корк — где мечту начнут превращать в работающую алгебру, ничего не зная о ганноверском архиве.