Кёнигсберг, 7 сентября 1930

Неделя

С 5 по 7 сентября 1930 года в Кёнигсберге идёт вторая конференция по теории познания точных наук. Собрались, чтобы подвести черту под тридцатилетним спором о том, как чинить основания математики. Три школы, три программных доклада, 6 сентября:

• Рудольф Карнап — о логицизме: математика есть логика, надо лишь аккуратно её выписать;
• Аренд Гейтинг — об интуиционизме: Брауэр прав, законченных бесконечностей не бывает, доказательство обязано быть построением;
• Иоганн фон Нейман — о формализме: программа Гильберта, финитное доказательство непротиворечивости.

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

7 сентября, последний день, общая дискуссия. Ближе к концу Гёдель берёт слово и говорит несколько фраз. Смысл их такой: даже если непротиворечивость системы доказана, этого мало —

можно (при условии непротиворечивости классической математики) указать примеры утверждений, которые содержательно истинны, но в формальной системе классической математики недоказуемы.

Стенограмма дискуссии напечатана в журнале «Erkenntnis». По ней видно: разговор после реплики продолжился, будто ничего не произошло. Никто не переспросил.

Кроме одного человека. Фон Нейман после заседания отвёл Гёделя в сторону и попросил рассказать подробнее.

8 сентября, тот же город. Давид ГильбертДавид Гильбертнемецкий математик · 1862–1943Человек, сделавший Гёттинген столицей математики и задавший ей повестку на весь XX век — двадцатью тремя проблемами и одной программой, которую сам же и не смог спасти., шестидесяти восьми лет, выступает перед съездом Общества немецких естествоиспытателей и врачей. Повод — присвоение ему звания почётного гражданина Кёнигсберга, где он родился. Речь называется «Познание природы и логика», и заканчивается она так:

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

Четырёхминутный фрагмент передавали по радио, и запись сохранилась: это единственная запись голоса Гильберта.

Гильберт и Гёдель не встретились. О результате Гильберт узнал позже, и, по свидетельству Бернайса, сперва рассердился.

Как это устроено

Доказательство занимает три хода, и все три можно рассказать без формул.

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

Каждому знаку языка приписывается номер. Тогда формула — конечная последовательность знаков $a_1, a_2, \dots, a_k$ — получает номер

$$\ulcorner \varphi \urcorner = 2^{a_1}\cdot 3^{a_2}\cdot 5^{a_3}\cdots p_k^{a_k},$$

где $p_k$ — $k$-е простое. По основной теореме арифметики разложение единственно, значит по числу восстанавливается формула. Тем же способом номер получает доказательство — последовательность формул.

Это ровно тот приём, который Лейбниц придумал в 1679 году, чтобы исполнить свою мечту. Гёдель применил его, чтобы доказать, что мечта неисполнима.

Ход второй: синтаксис становится арифметикой.

Проверка «является ли последовательность с номером $p$ доказательством формулы с номером $f$» — чисто механическая работа: развернуть числа обратно в тексты и посмотреть, каждая ли строчка аксиома или следует из предыдущих по правилу. Механическая проверка — значит, её можно записать арифметической формулой. Гёдель строит такую формулу $\mathrm{Dok}(p, f)$ явно, и это самая трудоёмкая часть статьи: сорок шесть определений подряд.

Теперь «формула $f$ доказуема» записывается внутри арифметики: $\exists p\ \mathrm{Dok}(p, f)$. Арифметика заговорила о собственных доказательствах.

Ход третий: диагональ.

Осталось построить формулу, которая говорит о себе. Кажется, что для этого нужно слово «это», а его в языке арифметики нет. На самом деле не нужно.

Применим лемму к формуле «не существует доказательства для $x$». Получится предложение $G$, равносильное утверждению

$$G:\quad\text{«предложение с номером } \ulcorner G\urcorner \text{ недоказуемо»},$$

то есть попросту «я недоказуемо».

Дальше два шага.

• Если бы $G$ было доказуемо, то доказуемо было бы и то, что оно недоказуемо, — система доказывала бы и $G$, и его отрицание. Значит, при непротиворечивости $G$ недоказуемо.
• Но ведь $G$ ровно это и утверждает. Значит, $G$ — истинно.

Истинное недоказуемое утверждение предъявлено. $\blacksquare$

Для недоказуемости отрицания $G$ Гёделю понадобилось допущение посильнее непротиворечивости (так называемая $\omega$-непротиворечивость); в 1936 году Баркли Россер заменил конструкцию так, что хватает обычной непротиворечивости.

Вторая теорема и письмо фон Неймана

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

$$\mathrm{PA}\ \vdash\ \mathrm{Con}(\mathrm{PA}) \to G,$$

где $\mathrm{Con}(\mathrm{PA})$ — арифметическая запись утверждения «противоречие невыводимо». А раз $G$ недоказуемо, недоказуемо и $\mathrm{Con}(\mathrm{PA})$.

Никакая достаточно богатая непротиворечивая система не может доказать собственную непротиворечивость.

Это и есть вторая теорема, и это выстрел точно в программу Гильберта: она требовала удостоверить надёжность математики её же средствами.

20 ноября 1930 года фон Нейман пишет Гёделю: из вашей теоремы следует замечательное следствие — недоказуемость непротиворечивости. Ответ разминулся с письмом: статья Гёделя уже была в редакции (получена 17 ноября) и содержала оба результата. Фон Нейман признал приоритет немедленно и, по воспоминаниям современников, к основаниям больше не возвращался — ушёл в функциональный анализ, квантовую механику, теорию игр и вычислительные машины.

Статья вышла в 1931 году под названием «О формально неразрешимых предложениях „Principia Mathematica" и родственных систем I». Продолжения (номера II) не последовало: оно не понадобилось.

Чего теорема не говорит

Вокруг этих теорем накопилось столько вздора, что оговорки приходится делать отдельно.

«Есть вещи, которые нельзя доказать» — неточно. Теорема утверждает нечто гораздо более конкретное: для каждой конкретной системы (непротиворечивой, содержащей арифметику, с перечислимым списком аксиом) есть своё истинное утверждение, ей недоступное. Само это утверждение прекрасно доказывается в системе побогаче: ZFC доказывает непротиворечивость арифметики ПеаноДжузеппе Пеаноитальянский математик и логик · 1858–1932Аксиоматизировал натуральный ряд, векторное пространство и математическую запись — и построил кривую, которая проходит через каждую точку квадрата. без всякого труда. Не существует одной системы для всего — вот точное содержание.

Три условия существенны, и каждое можно нарушить.

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

«Математика оказалась ненадёжной» — нет. Ни одного противоречия в арифметике или в ZFC за сто лет не нашли. Теорема говорит не о том, что фундамент шаток, а о том, что проверить его прочность изнутри нельзя.

Про сознание, свободу воли и существование Бога теорема не говорит ничего. Она про формальные системы с перечислимым списком аксиом, содержащие арифметику. Всё остальное — метафоры, и метафоры чужие.

Что уцелело от программы Гильберта

Меньше, чем хотелось, но существенно больше, чем «ничего».

Непротиворечивость арифметики всё-таки доказана — Генценом в 1936 году, средствами, выходящими за пределы самой арифметики ровно на один точно измеренный шаг. Вторая теорема говорит, что выйти придётся; ГенценГерхард Генценнемецкий логик · 1909–1945Доказал непротиворечивость арифметики — после того, как Гёдель показал, что этого сделать нельзя. Оба утверждения верны: Генцен вышел за пределы самой арифметики, и его доказательство измеряет, насколько… показал, насколько именно.

Финитная часть работает. Гильберт хотел оправдать употребление бесконечности конечными средствами. В ослабленном виде это сделано: известно, какие куски анализа сводятся к каким слабым системам, — этим занимается обратная математика.

Появилась метаматематика. Побочный продукт оказался ценнее цели: рассуждения о доказательствах стали математикой, и из неё выросли теория доказательств, теория моделей и теория вычислимости. Программа Гильберта не достигла своей цели и создала три новые области.

Человек

Курт Гёдель (1906, Брно — 1978, Принстон) был человеком крайней осторожности и крайней последовательности. Он редко публиковал; каждая из его немногих работ меняла свою область.

С 1940 года — в Принстоне, в Институте перспективных исследований, где его ежедневным спутником стал ЭйнштейнАльберт Эйнштейннемецкий физик-теоретик · 1879–1955Единственный физик в этом справочнике по праву математика: чтобы записать тяготение, ему понадобилась геометрия Римана — и он потратил на её освоение семь лет.. Эйнштейн говорил под конец жизни, что ходит в институт главным образом ради привилегии возвращаться домой вместе с Гёделем.

При получении американского гражданства в 1947 году Гёдель сообщил сопровождавшим его Эйнштейну и Моргенштерну, что нашёл в конституции США логическую брешь, позволяющую законным путём превратить страну в диктатуру. Оба уговаривали его молчать на собеседовании. По рассказу Моргенштерна, судья всё-таки задал неудачный вопрос, Гёдель начал объяснять — и Эйнштейн увёл разговор в сторону.

Последние годы он страдал манией отравления и ел только то, что готовила жена. Когда она надолго попала в больницу, он перестал есть вовсе и умер от истощения 14 января 1978 года, весив тридцать килограммов.

Следующая точка: Варшава — где поставят точный диагноз: дело не в самоссылке, а в слове «истинно».