Часть VIII · Основания Глава 56 из 60
Гёдель, Тьюринг и пределы доказательства
Головоломка из четырёх правил, число, которое говорит о себе, и программа, которую невозможно написать. В 1931 году Гёдель доказал, что в арифметике есть истинные, но недоказуемые утверждения, а в 1936-м Тьюринг — что некоторые вопросы не решает никакой алгоритм.
Опирается на: 55 · Функциональный анализ
Вы научитесь
- отличать выводимость внутри формальной системы от истины о ней и доказывать невыводимость через инвариант
- объяснять гёделеву нумерацию и диагональную лемму и пересказывать, как из них получается утверждение, истинное, но недоказуемое
- доказывать неразрешимость проблемы остановки диагональным рассуждением и выводить из неё неполноту и невычислимость усердного бобра
7Может ли утверждение быть истинным, но недоказуемым?
Прошлая глава закончилась вопросом, который звучит почти как ересь. В «Шотландской книге» остались нерешённые задачи, и обычно это значит, что нужной идеи ещё не придумали. Но бывает ли утверждение о натуральных числах, которое истинно, а доказать его нельзя в принципе, какие бы гении за него ни брались? Прежде чем отвечать, сыграем в игру. Её придумал Дуглас Хофштадтер для книги «Гёдель, Эшер, Бах» (1979), и она содержит весь сюжет главы в миниатюре.
Есть строки из букв M, I и U. Начинаем со строки MI. Разрешены четыре хода, и больше ничего:
- если строка кончается на I, к ней можно приписать U: $x\mathrm{I} \to x\mathrm{IU}$;
- всё, что стоит после M, можно удвоить: $\mathrm{M}x \to \mathrm{M}xx$ (из MIU получается MIUIU);
- любые три I подряд можно заменить одной U: $\mathrm{III} \to \mathrm{U}$;
- любые две U подряд можно стереть: $\mathrm{UU} \to$ ничего.
Задача: получить строку MU. Попробуйте, прежде чем читать дальше.
Игра по правилам
Скорее всего, строки у вас быстро росли. Удвоение разгоняет их, тройки I превращаются в U, пары U исчезают, и кажется, что вот-вот останется одна U. Но MU не выходит. Перебор тоже не помогает: не больше чем за семь ходов из MI получается 1730 разных строк, и MU среди них нет. Только из того, что мы не нашли, ещё не следует, что искать нечего: вдруг MU появится на тысячном ходу?
У этой игры есть общее название.
Формальная система — это алфавит, набор исходных строк (аксиом) и правила, по которым из одних строк механически получаются другие. Строки, которые можно получить из аксиом конечным числом шагов, называют теоремами системы, а цепочку шагов — выводом.
Слово «механически» здесь главное. Чтобы проверить вывод, не нужно ничего понимать: достаточно сверять каждую строку с правилами. Это умеет и школьник, и компьютер. А вот чтобы ответить на вопрос «выводится ли MU», одних правил мало, и в этом вся интрига.
Мы должны знать
К началу XX века математики обнаружили, что интуиция подводит даже в основаниях. Наивная теория множеств привела к парадоксу Рассела (глава 51), и многие стали сомневаться, на чём вообще стоит здание математики. Давид Гильберт предложил в 1920-е годы программу спасения. Нужно записать всю математику как формальную систему — с аксиомами и механическими правилами вывода, как в игре MIU. Затем доказать, что эта система хорошая, и доказать строго, самыми простыми «финитными» средствами, в которых никто не усомнится. «Хорошая» означало две вещи.
Формальную систему, в которой можно записывать утверждения, называют непротиворечивой, если в ней нельзя вывести одновременно утверждение и его отрицание, и полной, если для каждого утверждения её языка выводится либо оно само, либо его отрицание.
Противоречивая система бесполезна: в ней выводится всё, ведь из лжи следует что угодно (глава 51). Полная система отвечает на любой вопрос. К этому Гильберт и Вильгельм Аккерман в 1928 году добавили третье требование: должен существовать алгоритм, который по любому утверждению решает, выводится ли оно. Это Entscheidungsproblem, «проблема разрешения».
Для арифметики кандидатом в такие системы была аксиоматика, которую опубликовал Джузеппе Пеано в 1889 году (годом раньше похожую систему описал Рихард Дедекинд). Язык у неё скупой: ноль $0$, функция «следующее число» $S$ (так что $S0$ — это один, $SS0$ — два), сложение, умножение, равенство, логические связки и кванторы по натуральным числам. Здесь натуральный ряд удобнее начинать с нуля, хотя в курсе мы обычно начинаем с единицы.
Ноль не следует ни за каким числом: $\forall x\;\neg(Sx = 0)$.
У разных чисел разные следующие: $\forall x\,\forall y\;(Sx = Sy \to x = y)$.
$x + 0 = x$, $\;x + Sy = S(x + y)$, $\;x \cdot 0 = 0$, $\;x \cdot Sy = x \cdot y + x$.
Для любой формулы $\varphi(x)$: если верно $\varphi(0)$ и для всех $x$ из $\varphi(x)$ следует $\varphi(Sx)$, то $\varphi(x)$ верно для всех $x$.
Вместе с правилами логики эти аксиомы называют арифметикой Пеано. Индукция — та самая, из главы о последовательностях, только теперь это не приём доказательства, а аксиома, одна для каждой формулы $\varphi$. Из этих аксиом выводятся все привычные свойства чисел, от $2 + 2 = 4$ до бесконечности простых. Казалось, дело за малым — доказать, что система непротиворечива и полна.
С 5 по 7 сентября 1930 года в Кёнигсберге шла конференция по основаниям математики. В последний день, на заключительной дискуссии, 24-летний Курт Гёдель из Вены коротко заметил, что в формальной системе арифметики есть утверждения, истинные, но недоказуемые в ней. Заметку почти никто не понял; сразу оценил её, по-видимому, только Джон фон Нейман. На следующий день, 8 сентября, в том же Кёнигсберге Гильберт выступил с речью, которую транслировало радио. Она кончалась словами «Wir müssen wissen. Wir werden wissen» — «Мы должны знать. Мы будем знать». Эти слова выбиты на его могиле в Гёттингене. Статья Гёделя вышла в 1931 году, и программа Гильберта в задуманном виде оказалась невыполнимой. Как Гёдель это доказал, мы увидим, но сначала решим головоломку.
Шаг из системы
Внутри игры MIU можно только делать ходы. Чтобы доказать, что MU не получится никогда, нужно посмотреть на игру снаружи и найти величину, которую ни один ход не меняет, — инвариант, как в задачах о графах или в пятнашках. Хофштадтер называл это «выпрыгнуть из системы».
В системе MIU ни одна выводимая строка не содержит число букв I, кратное трём. В частности, строка MU с нулём букв I не выводится.
Идея: следить не за всей строкой, а только за остатком от деления числа букв I на $3$. Правила двигают этот остаток по трём кружкам, и в кружок $0$ не ведёт ни одна стрелка.
Заметьте, где жило это доказательство. Не внутри MIU: в самой игре нет ни чисел, ни остатков, ни индукции. Мы рассуждали о системе на более богатом языке — языке арифметики. Инвариант даёт больше, чем отказ: он описывает все теоремы MIU целиком.
Строка вида $\mathrm{M}w$, где $w$ состоит из букв I и U, выводится из MI тогда и только тогда, когда число букв I в ней не делится на $3$.
В одну сторону это предыдущая теорема. Обратно, пусть в $w$ ровно $n$ букв I, $n$ не делится на $3$, и $u$ букв U. Строим вывод в четыре приёма. Положим $m = n + 3u$; это число тоже не делится на $3$ и даёт тот же остаток, что и $n$.
Разгон. Степени двойки дают остатки $1, 2, 1, 2, \dots$, поэтому найдётся $j$, при котором $2^j \ge m$ и $2^j$ даёт при делении на $3$ тот же остаток, что и $m$. Применив правило 2 ровно $j$ раз, получаем M и за ним $2^j$ букв I.
Лишние I. Разность $2^j - m = 3t$ делится на $3$. Если $t$ нечётно, сначала применим правило 1 и получим одну U в конце. Затем $t$ раз заменим последние три I одной U (правило 3). В конце строки стоит $t$ или $t + 1$ букв U — в любом случае чётное число, и правило 4 стирает их парами. Осталась строка M и $m$ букв I подряд.
Нарезка. Запишем $w = \mathrm{I}^{k_0}\,\mathrm{U}\,\mathrm{I}^{k_1}\,\mathrm{U}\cdots\mathrm{U}\,\mathrm{I}^{k_u}$, где $k_0 + \dots + k_u = n$. Строку из $m = n + 3u$ букв I можно разбить так же: $\mathrm{I}^{k_0}\,\mathrm{III}\,\mathrm{I}^{k_1}\,\mathrm{III}\cdots\mathrm{III}\,\mathrm{I}^{k_u}$. Каждую из $u$ отмеченных троек заменяем одной U по правилу 3 и получаем $\mathrm{M}w$.
Решатель в песочнице строит вывод именно так. Он не самый короткий, но он всегда существует.
Выводится ли в системе MIU строка MUIIU? Ответьте «да» или «нет».
Да. В ней две буквы I, а $2$ на $3$ не делится, и по теореме строка выводится. Один из выводов: $\mathrm{MI} \to \mathrm{MII} \to \mathrm{MIIII} \to \mathrm{MIIIIIIII}$ (восемь I) $\to \mathrm{MUIIIII} \to \mathrm{MUIIU}$ — сначала правило 2 трижды, потом правило 3 дважды: к первым трём I и к трём последним.
Для арифметики Гильберт надеялся на то же самое: всё, что можно узнать о числах, должно выводиться внутри системы. Гёдель заметил две вещи. Во-первых, язык арифметики настолько богат, что умеет говорить о формальных системах, в том числе о самой арифметике, — так же, как мы только что говорили о MIU на языке остатков. Во-вторых, из этого получается ловушка.
Формулы становятся числами
Чтобы арифметика могла рассуждать о формулах, формулы надо превратить в числа. Дадим каждому символу номер, например $0 \mapsto 1$, $S \mapsto 2$, $+ \mapsto 3$, $= \mapsto 5$, а строку символов закодируем произведением степеней простых чисел.
Гёделева нумерация — способ сопоставить каждой формуле натуральное число, её номер, так, чтобы по номеру формула восстанавливалась однозначно и механически. Номер формулы $\varphi$ обозначают $\ulcorner\varphi\urcorner$.
Однозначность обеспечивает основная теорема арифметики (глава 3): разложение на простые множители единственно, поэтому из номера показатели, а значит, и символы, читаются без двусмысленности. Не всякое число — номер: у $10 = 2 \cdot 5$ пропущена тройка, у $2^{20}$ показатель $20$ не код никакого символа. Проверьте на кодировщике.
Номера быстро растут: у формулы $\forall x\,\neg(Sx = 0)$ из девяти символов номер уже 55-значный. Но размер не важен, важна механичность. Доказательство — это последовательность формул, её тоже можно закодировать числом: например, $2^{\ulcorner\varphi_1\urcorner} \cdot 3^{\ulcorner\varphi_2\urcorner} \cdots$. И вот главное наблюдение Гёделя. Проверка «будет ли число $x$ номером доказательства формулы с номером $y$» — механическая процедура: разложить $x$, прочитать формулы, сверить каждую с аксиомами и правилами. А любую такую процедуру можно записать формулой арифметики. Получается формула $\mathrm{Prf}(x, y)$ — «$x$ — номер доказательства формулы с номером $y$», и формула $\mathrm{Prov}(y) = \exists x\,\mathrm{Prf}(x, y)$ — «формула с номером $y$ доказуема».
Хофштадтер показывает то же на MIU. Заменим M на $3$, I на $1$, U на $0$: строка MIIU превращается в число $3110$. Тогда правило 1 «к строке на I припиши U» — это «к числу, которое кончается единицей, припиши ноль справа», то есть умножь на $10$. Остальные правила тоже становятся действиями с десятичной записью, и фраза «MU — теорема MIU» превращается в утверждение о числах: «$30$ получается из $31$ этими действиями». Вопрос о символах стал вопросом арифметики.
По нашей таблице кодов ($0 \mapsto 1$, $S \mapsto 2$) какую строку символов кодирует число $180$?
$180 = 2^2 \cdot 3^2 \cdot 5^1$. Показатели по порядку: $2, 2, 1$, то есть символы $S, S, 0$. Это строка $SS0$ — запись числа два.
Фраза, которая говорит о себе
Древний парадокс лжеца: «Это утверждение ложно». Если оно истинно, то ложно, а если ложно, то истинно. Слово «это» здесь жульничает: в арифметике нет указательных местоимений, формула не может ткнуть пальцем в себя. Но самоотсылку можно построить честно, подстановкой. Вот фраза, придуманная по образцу философа Уиларда Куайна:
«даёт ложное утверждение, если приписать его к собственной цитате» даёт ложное утверждение, если приписать его к собственной цитате.
Проделайте то, о чём она говорит: возьмите кусок в кавычках и припишите его к его же цитате. Получится вся эта фраза целиком. Значит, фраза утверждает про себя, что ложна, — лжец без слова «это». Математическая версия приёма называется диагональной леммой. Её роль «приписать к собственной цитате» играет функция $\mathrm{diag}$: по номеру $n$ формулы $\varphi_n(x)$ с одной свободной переменной она выдаёт номер формулы $\varphi_n(\bar n)$, в которую вместо $x$ подставлено число $n$ (черта означает запись числа в языке: $\bar 2 = SS0$). Функция $\mathrm{diag}$ вычислима, и по лемме о выразимости арифметика умеет о ней говорить.
Для любой формулы $\varphi(y)$ арифметики с одной свободной переменной существует утверждение $G$, для которого в арифметике Пеано доказуемо $G \leftrightarrow \varphi(\ulcorner G\urcorner)$. Иначе говоря, $G$ утверждает про собственный номер, что он обладает свойством $\varphi$.
Идея — та же таблица, что в диагональном доказательстве Кантора (глава 52). Строки — формулы $\varphi_0(x), \varphi_1(x), \dots$ с одной переменной, выписанные по порядку номеров; столбцы — числа; в клетке $(n, k)$ стоит утверждение $\varphi_n(\bar k)$. Нас интересует диагональ.
Теперь возьмём в роли $\varphi(y)$ свойство «формула с номером $y$ недоказуема», то есть $\neg\mathrm{Prov}(y)$. Диагональная лемма выдаёт утверждение $G$, которое доказуемо равносильно $\neg\mathrm{Prov}(\ulcorner G\urcorner)$: «я недоказуемо». Это уже не парадокс, а ловушка. У лжеца нет хорошего значения истинности; у $G$ оно есть.
Пусть $T$ — непротиворечивая формальная система, содержащая арифметику Пеано, аксиомы которой можно распознавать механически. Тогда утверждение $G$ не доказуемо в $T$. Если вдобавок все теоремы $T$ истинны, то и $\neg G$ не доказуемо в $T$, а само $G$ истинно. Значит, $T$ неполна.
Хитрость в том, что доказательство $G$ само было бы опровержением $G$. Лемма о выразимости применяется к $\mathrm{Prf}$ для системы $T$: проверка доказательств в $T$ механическая, потому что механически распознаются её аксиомы.
Условие «все теоремы истинны» можно ослабить. Сам Гёдель обошёлся более слабым техническим условием, так называемой ω-непротиворечивостью, а Джон Россер в 1936 году построил другое утверждение, чуть хитрее $G$, для которого хватает одной непротиворечивости.
Главное в теореме — слово «любая». Добавьте $G$ к аксиомам: получится новая система $T'$, по-прежнему непротиворечивая и механическая, и для неё диагональная лемма построит своё $G'$. Никакой конечный или механически перечислимый список аксиом не исчерпывает арифметическую истину. Недоказуемость всегда относительна: $G$ недоказуемо в $T$, а в $T'$ доказуемо тривиально.
Что утверждает первая теорема Гёделя?
Неполнота — свойство каждой конкретной системы: для неё найдётся своё $G$. Добавив $G$ в аксиомы, мы получим систему, где $G$ доказуемо, но у неё будет своё недоказуемое утверждение.
Система не ручается за себя
Второй удар по программе Гильберта Гёдель нанёс в той же статье. Утверждение «$T$ непротиворечива» тоже записывается формулой арифметики: «не существует доказательства утверждения $0 = S0$», то есть $\mathrm{Con}(T) = \neg\mathrm{Prov}(\ulcorner 0 = S0\urcorner)$.
Если формальная система $T$ из первой теоремы непротиворечива, то утверждение $\mathrm{Con}(T)$ в ней не доказуемо.
Идея доказательства — перенести первую теорему внутрь самой системы. Рассуждение первой теоремы в части «если $T$ непротиворечива, то $G$ не доказуемо» состоит из шагов, каждый из которых арифметика может проделать сама, рассуждая о номерах формул. Если это проверить, получится, что $T$ доказывает импликацию $\mathrm{Con}(T) \to \neg\mathrm{Prov}(\ulcorner G\urcorner)$, а правая часть по диагональной лемме равносильна $G$. Значит, $T$ доказывает $\mathrm{Con}(T) \to G$. Если бы $T$ доказывала $\mathrm{Con}(T)$, она по правилу вывода доказала бы и $G$, а это невозможно по первой теореме. Полная проверка того, что рассуждение формализуется внутри $T$, — это три «условия выводимости» Гильберта — Бернайса — Лёба, и она занимает несколько десятков страниц. Идею мы изложили, а формальную часть можно найти, например, в книге Рэймонда Смаллиана «Gödel’s Incompleteness Theorems» (1992).
По воспоминаниям, фон Нейман в ноябре 1930 года сам вывел вторую теорему из первой и написал Гёделю, но тот уже нашёл её. Смысл жёсткий: доказать непротиворечивость арифметики средствами, которые слабее самой арифметики, нельзя. Программа Гильберта в первоначальном виде рухнула. Это не значит, что непротиворечивость арифметики под вопросом: в 1936 году Герхард Генцен доказал её, но опираясь на трансфинитную индукцию — принцип, которого нет в арифметике Пеано. Доверие к основаниям осталось, но оно стоит не на финитной проверке, а на убеждённости в более сильных принципах.
Что такое алгоритм
Оставался третий вопрос Гильберта, проблема разрешения: существует ли алгоритм, который по любому утверждению говорит, выводимо ли оно? Чтобы ответить «нет», нужно сначала точно сказать, что такое алгоритм. В 1936 году это независимо сделали Алонзо Чёрч в Принстоне и 23-летний Алан Тьюринг в Кембридже. Определение Тьюринга — воображаемый вычислитель, который делает самые простые действия, какие только можно представить.
Машина Тьюринга — это бесконечная в обе стороны лента из клеток, в каждой из которых записан символ (у нас $0$ или $1$), головка, которая стоит над одной клеткой, и конечная таблица правил. Машина находится в одном из конечного числа состояний; правило для пары «состояние, прочитанный символ» говорит, что записать в клетку, куда сдвинуться на одну клетку и в какое состояние перейти. Среди состояний есть «стоп».
Кажется, что так можно разве что прибавить единицу. Но Тьюринг показал, что такими таблицами выражается любое вычисление, которое можно описать как механическую процедуру. Более того, существует универсальная машина: она читает с ленты описание любой другой машины и её вход и делает то же, что сделала бы та. Это идея программы, хранящейся в памяти, больше чем за десять лет до первых таких компьютеров. Утверждение «всё, что вычисляется механической процедурой, вычисляется машиной Тьюринга» называют тезисом Чёрча — Тьюринга. Это не теорема: «механическая процедура» — понятие неформальное. Но за девяносто лет не нашлось ни одного вычисления, которое не укладывалось бы в машину Тьюринга, а все предложенные модели — λ-исчисление Чёрча, рекурсивные функции, любые языки программирования — оказались равносильны ей.
Проблема остановки
Каждая машина на пустой ленте либо когда-нибудь останавливается, либо работает вечно. Посмотреть на это можно, но что делать, если машина работает уже миллион шагов? Может, остановится на миллион первом. Хотелось бы программу-судью.
Проблема остановки — найти алгоритм, который по любой программе $P$ и входу $x$ за конечное время отвечает, остановится ли $P$, запущенная на $x$.
Алгоритма, решающего проблему остановки для всех программ и всех входов, не существует.
Хитрость — снова диагональ. Если бы судья существовал, из него можно было бы собрать программу, которая поступает наперекор судье на самой себе.
Проверьте рассуждение на живых «судьях». Ниже машина $D$ собирается из предсказателя, какой вы выберете, — включая вас самих.
Этим Тьюринг ответил и Гильберту. Если бы существовал алгоритм, решающий, выводимо ли утверждение, им можно было бы решать и проблему остановки: утверждение «машина $P$ на входе $x$ останавливается» записывается в арифметике на языке номеров, как доказуемость у Гёделя. Значит, проблема разрешения неразрешима. Сам термин «проблема остановки» появился позже, у последователей Тьюринга, но диагональное рассуждение — его.
Следует ли из теоремы, что нельзя узнать, остановится ли программа «пока истина: ничего не делай»?
Теорема запрещает универсального судью. Для многих конкретных программ ответ находится легко, а для некоторых — очень трудно; бывают и такие, про которые остановку нельзя ни доказать, ни опровергнуть в выбранной системе аксиом, об этом ниже.
Проблема остановки даёт второе доказательство неполноты, в котором нет ни одной технической леммы о выразимости, кроме самой простой: утверждение «$P$ на входе $x$ не останавливается» записывается формулой арифметики. Вычисление — конечная последовательность состояний ленты, её можно закодировать числом, и «$P$ останавливается» значит «существует число, кодирующее остановившееся вычисление».
Пусть $T$ — формальная система с механически распознаваемыми аксиомами, в которой записываются утверждения вида «$P$ на входе $x$ не останавливается», и все теоремы $T$ истинны. Тогда есть программа $P$ и вход $x$, такие что $P$ на $x$ не останавливается, но $T$ этого не доказывает.
Предположим противное: каждое истинное утверждение «$P$ на $x$ не останавливается» доказуемо в $T$. Опишем алгоритм, решающий проблему остановки. Получив $P$ и $x$, будем попеременно делать два дела: шаг работы $P$ на $x$ и проверку очередной строки символов — не доказательство ли она в $T$ утверждения «$P$ на $x$ не останавливается». Строки перебираем по порядку длины, а проверка доказательства механическая, потому что механически распознаются аксиомы. Если $P$ на $x$ останавливается, первое дело рано или поздно это покажет, и мы ответим «остановится». Если не останавливается, то утверждение истинно, по предположению у него есть доказательство, и второе дело рано или поздно его найдёт; тогда отвечаем «зациклится». Ошибиться алгоритм не может: $T$ доказывает только истинное, поэтому доказательство неостановки не найдётся для остановившейся программы. Так мы решили бы проблему остановки, а это невозможно. Значит, предположение неверно.
Неразрешимое по соседству
Можно подумать, что неразрешимость живёт только в искусственных вопросах о программах, которые спрашивают о себе. Во второй половине XX века выяснилось, что она прячется в самой обычной математике.
Задачу, для которой нет алгоритма, дающего верный ответ на каждый её частный случай, называют алгоритмически неразрешимой.
Десятая проблема Гильберта. В 1900 году Гильберт попросил найти способ, который по любому уравнению с целыми коэффициентами, вроде $x^3 + y^3 + z^3 = 42$, узнаёт, есть ли у него решение в целых числах. Для этого уравнения решение нашли только в 2019 году, и числа в нём семнадцатизначные. В 1970 году Юрий Матиясевич, завершив работу Мартина Дэвиса, Хилари Патнэма и Джулии Робинсон, доказал, что такого способа нет. Более того, для любой программы можно выписать многочлен, у которого целые корни есть тогда и только тогда, когда программа останавливается. Проблема остановки переодевается в уравнение.
Проблема слов. Группу можно задать образующими и соотношениями, как в главе о группах, и спросить, равно ли единице заданное произведение образующих. В 1955 году Пётр Новиков построил конечно заданную группу, для которой этот вопрос алгоритмически неразрешим; независимо это сделал Уильям Бун.
Плитки Ванга. Возьмите набор квадратных плиток с цветными сторонами; поворачивать их нельзя, соседние стороны должны совпадать по цвету. Можно ли замостить такими плитками всю плоскость? Хао Ван в 1961 году спросил, есть ли алгоритм, отвечающий на этот вопрос для любого набора. В 1966 году Роберт Бергер доказал, что нет. Попутно он построил набор из 20 426 плиток, которым можно замостить плоскость, но только непериодически; сейчас известен такой набор всего из 11 плиток.
Усердный бобёр
Вернёмся к машинам с пустой лентой. Возьмём все машины с $n$ состояниями и символами $0$ и $1$; их конечное число. Некоторые работают вечно, остальные останавливаются. Среди остановившихся найдём ту, что работала дольше всех.
Усердный бобёр $BB(n)$ — наибольшее число шагов, которое делает перед остановкой машина Тьюринга с $n$ состояниями и символами $0, 1$, запущенная на пустой ленте. Машину, на которой достигается максимум, тоже называют бобром.
Функцию придумал Тибор Радо в 1962 году. Её значения:
| $n$ | $BB(n)$ | кто доказал |
|---|---|---|
| 1 | 1 | — |
| 2 | 6 | Радо, 1962 |
| 3 | 21 | Шень Линь и Радо, 1965 |
| 4 | 107 | Аллен Брейди, 1983 |
| 5 | 47 176 870 | проект bbchallenge, 2024; доказательство проверено в Coq |
| 6 | неизвестно | больше башни из пятнадцати десяток $10^{10^{\cdot^{\cdot^{10}}}}$ (2022) |
Чемпиона с пятью состояниями нашли Хайнер Марксен и Юрген Бунтрок ещё в 1989 году, и он оставляет на ленте 4098 единиц. Трудность была не в том, чтобы его найти, а в том, чтобы доказать, что ни одна из остальных машин с пятью состояниями, которые останавливаются, не работает дольше. Для этого пришлось разобраться со всеми машинами, которые не останавливаются, и для каждой доказать, что она не остановится никогда. Десятки участников открытого проекта bbchallenge по всему миру делали это с 2022 по 2024 год, а итоговое доказательство проверил компьютер в системе формальной проверки Coq.
Бобёр с двумя состояниями: в состоянии $A$ на $0$ он пишет $1$, идёт вправо и переходит в $B$; на $1$ пишет $1$, идёт влево и переходит в $B$. В состоянии $B$ на $0$ пишет $1$, идёт влево и переходит в $A$; на $1$ пишет $1$, идёт вправо и останавливается. Сколько шагов он сделает на пустой ленте, считая последний?
Следим за лентой; скобки — головка. $A$: $[0] \to 1[0]$, $B$: $\to [1]1$, $A$: $\to [0]11$, $B$: $\to [0]111$, $A$: $\to 1[1]11$, $B$: пишет $1$, идёт вправо, стоп. Всего $6$ шагов, на ленте $4$ единицы. Проверьте в симуляторе выше.
Не существует алгоритма, который по числу $n$ выдаёт $BB(n)$.
Пусть такой алгоритм есть. Тогда решалась бы проблема остановки для машин на пустой ленте: чтобы узнать, остановится ли машина $M$ с $n$ состояниями, вычислим $BB(n)$ и запустим $M$ на $BB(n)$ шагов. Если за это время она не остановилась, то не остановится никогда: иначе она работала бы дольше чемпиона. Но и эта частная проблема неразрешима. По программе $P$ и входу $x$ механически строится машина $M_{P,x}$, которая сначала пишет $x$ на пустую ленту, а потом работает как $P$; она останавливается на пустой ленте тогда и только тогда, когда $P$ останавливается на $x$. Так мы решили бы общую проблему остановки, а это невозможно.
Так же доказывается, что $BB(n)$ в конце концов обгоняет любую вычислимую функцию: будь $BB(n) \le f(n)$ для вычислимой $f$, мы решали бы проблему остановки, запуская машины на $f(n)$ шагов. А с неполнотой бобёр связан совсем наглядно. Известны машины с несколькими сотнями состояний, которые останавливаются тогда и только тогда, когда в теории множеств ZFC обнаруживается противоречие. Если ZFC непротиворечива, такая машина работает вечно, но по второй теореме Гёделя доказать это в ZFC нельзя, а значит, нельзя в ней и вычислить соответствующее значение $BB$. Пять состояний оказались на пределе человеческих сил; для нескольких сотен предел поставлен уже теоремой.
Ответ на седьмой вопрос
Да. Для любой непротиворечивой системы аксиом, которую можно выписать механически и в которой есть арифметика, найдётся утверждение о натуральных числах, истинное, но в этой системе недоказуемое (Гёдель, 1931). Такие утверждения бывают и вполне «житейскими»: например, что определённая машина Тьюринга никогда не остановится. Недоказуемость всегда относительна системе аксиом, а абсолютной «истины без доказательства» теорема не утверждает.
Теорема часто пересказывается неверно, так что отметим, чего в ней нет. Она не говорит, что математика противоречива или что истина субъективна: в ней ровно наоборот, $G$ однозначно истинно. Она не говорит, что конкретные открытые проблемы недоказуемы: гипотеза Гольдбаха или гипотеза Римана вполне могут быть доказаны завтра. Она не утверждает, что человек сильнее машины: об этом спорят философы, и аргументы в таких спорах выходят за пределы математики. И она не отменяет доказательства: почти всё, чем занимаются математики, спокойно доказывается в ZFC.
А игра MIU теперь выглядит пророческой. Внутри неё нельзя было ни получить MU, ни понять, что это невозможно; ответ дал взгляд снаружи. С арифметикой так же, но с поправкой: выпрыгнув из системы в более сильную, мы снова оказываемся внутри системы, и у неё свои недоказуемые истины. Лестница не кончается.
Куда дальше
Строгость доведена до предела: доказательство стало цепочкой символов, которую проверяет машина, и мы увидели, где этот путь упирается в стену. Теперь можно позволить себе обратное — геометрию, в которой длины и углы не важны, а фигуры можно мять, как пластилин. Тополог, по известной шутке, не отличает кружку от бублика. Почему кружка и бублик — «одно и то же», а шарик и бублик — нет? И что вообще значит «одно и то же», если у фигур разные размеры и углы? Об этом глава о топологии.