Карта → событие
Генцен: непротиворечивость арифметики, доказанная извне
Как люди на самом деле доказывают
Начал Генцен не с непротиворечивости, а с недовольства.
Формальные системы Фреге, Рассела и ГильбертаДавид ГильбертЧеловек, сделавший Гёттинген столицей математики и задавший ей повестку на весь XX век — двадцатью тремя проблемами и одной программой, которую сам же и не смог спасти. устроены одинаково: длинный список аксиом и одно-два правила вывода. Доказательство в такой системе — цепочка формул, и оно совершенно нечитаемо: чтобы доказать очевидное, приходится хитроумно подбирать подстановки в аксиомы.
Между тем живой математик рассуждает иначе. Он говорит: «предположим $A$… отсюда получаем $B$; значит, из $A$ следует $B$». Он вводит допущение, работает под ним и в конце его снимает.
В диссертации 1933 года и в статье «Исследования логического вывода» (1935) Генцен строит систему, где именно так и полагается: натуральный вывод. Аксиом нет вовсе. Вместо них — по два правила на каждую связку: как её ввести и как её устранить.
| Связка | Введение | Устранение |
|---|---|---|
| $\wedge$ | из $A$ и $B$ получить $A \wedge B$ | из $A \wedge B$ получить $A$ (или $B$) |
| $\to$ | предположив $A$, вывести $B$; снять допущение и получить $A \to B$ | из $A \to B$ и $A$ получить $B$ |
| $\forall$ | доказав $A(x)$ для произвольного $x$, получить $\forall x\, A(x)$ | из $\forall x\, A(x)$ получить $A(t)$ |
Всякий, кто вёл кружок или писал доказательство на доске, узнает здесь себя. Именно так изложены логика и её правила в сегодняшних учебниках — это Генцен.
Заодно обнаруживается вещь изящная: если у правил введения-устранения отбросить одно-единственное правило — вывод «из противоречия следует что угодно», — получится в точности интуиционистская логика Брауэра и Гейтинга. Классическая и интуиционистская логика оказываются одной системой, различающейся одной строчкой.
Главная теорема
Для технической работы Генцен строит второй вариант — исчисление секвенций, где записывается не отдельная формула, а утверждение вида «из посылок $\Gamma$ следует $\Delta$». В нём есть правило сечения: если из $\Gamma$ следует $A$, а из $A$ следует $\Delta$, то из $\Gamma$ следует $\Delta$. Это обычная лемма: доказал вспомогательное утверждение — пользуйся им дальше.
Hauptsatz, главная теорема Генцена (1935): всякое сечение можно устранить. Любое доказательство переписывается в такое, где лемм нет вовсе.
Следствие — свойство подформульности: в доказательстве без сечений встречаются только части того, что доказывается. Ничего постороннего вводить не приходится.
Отсюда мгновенно получается непротиворечивость чистой логики: чтобы вывести противоречие (пустую секвенцию), в доказательстве без сечений нечему взяться — подформул у пустоты нет. А ещё отсюда следует, что пространство поиска доказательства ограничено, и на этом стоит всё автоматическое доказательство теорем: и метод резолюций, и то, как ищут вывод современные ассистенты доказательств.
Цена устранения сечений — размер: доказательство без лемм может оказаться башней экспонент от исходного. Это, собственно, и есть математическое объяснение того, зачем математике нужны леммы.
1936: непротиворечивость арифметики
Теперь главное. Арифметика — это логика плюс индукция, и для неё сечения устраняются не всегда: индукция создаёт круг. Генцен обходит его так.
Каждому доказательству он приписывает ординал — трансфинитное число, измеряющее его сложность. Затем показывает: всякое доказательство противоречия можно переделать в другое доказательство противоречия со строго меньшим ординалом.
А теперь принцип, знакомый по натуральным числам: бесконечно убывающей последовательности не бывает. Значит, доказательства противоречия нет вовсе.
Все нужные ординалы оказываются меньше числа $\varepsilon_0$ — предела башни
$$\omega,\quad \omega^{\omega},\quad \omega^{\omega^{\omega}},\quad \dots \longrightarrow\ \varepsilon_0,$$
наименьшего ординала, для которого $\omega^{\varepsilon_0} = \varepsilon_0$. Он счётен: множество всех ординалов меньше $\varepsilon_0$ можно перенумеровать натуральными числами и работать с ним вполне конечными средствами. Требуется от него ровно одно свойство — трансфинитная индукция до $\varepsilon_0$: если бесконечного убывания нет, то принцип верен.
Как это уживается со второй теоремой ГёделяКурт ГёдельДоказал, что в любой достаточно богатой формальной системе есть истинные утверждения, которые она не может доказать, — и тем закрыл программу Гильберта в двадцать пять лет.
Вопрос законный: Гёдель доказал, что арифметика не может доказать собственную непротиворечивость. Генцен её доказал. Кто ошибся?
Никто. Доказательство Генцена использует средство, которого внутри арифметики нет: трансфинитную индукцию до $\varepsilon_0$. Сам Генцен в 1943 году показал это точно: арифметика ПеаноДжузеппе ПеаноАксиоматизировал натуральный ряд, векторное пространство и математическую запись — и построил кривую, которая проходит через каждую точку квадрата. доказывает трансфинитную индукцию до любого ординала, меньшего $\varepsilon_0$, — и не доказывает до самого $\varepsilon_0$.
Совпадение получилось идеально точным, и в этом вся ценность работы.
Ординал $\varepsilon_0$ — это мера того, чего именно не хватает арифметике, чтобы удостоверить собственную надёжность. Не «чего-то не хватает», а вот ровно столько.
Так родился ординальный анализ: каждой формальной системе приписывается ординал — её теоретико-доказательственная сила. Для арифметики Пеано это $\varepsilon_0$, для более слабых систем — меньше, для более сильных — больше (для систем уровня анализа ординалы получают такие имена, как «ординал Бахмана — Говарда»). Получилась линейка, которой сравнивают силу теорий; ею пользуются до сих пор.
Программа Гильберта в исходном виде требовала финитных средств. Трансфинитная индукция до $\varepsilon_0$ финитной не является. Но это и не произвольная сильная аксиома: она конструктивна, её содержание прозрачно, и почти все считают её надёжнее самой арифметики. В таком виде — не «доказать безусловно», а «свести к чему-то более очевидному и измерить разницу» — программа Гильберта работает по сей день.
Человек
Герхард Генцен (1909–1945) был учеником Пауля Бернайса, ближайшего сотрудника Гильберта; когда Бернайса в 1933 году уволили по расовым законам, руководителем диссертации формально стал Герман ВейльГерман ВейльСоединил теорию групп с квантовой механикой, придумал калибровочную симметрию и был, по общему мнению, самым широко образованным математиком своего поколения.. С 1935 года Генцен — ассистент уже отошедшего от дел Гильберта в Гёттингене, откуда к тому времени изгнали почти всех.
Он вступил в СА в 1934 году и в НСДАП в 1937-м. В 1939–1941 годах служил в связи, был комиссован по здоровью, а в 1943 году получил доцентуру в Немецком университете в Праге, где, помимо преподавания, руководил вычислительной группой из школьниц, работавшей на военные нужды.
5 мая 1945 года, в день Пражского восстания, весь состав Немецкого университета был арестован. Генцен провёл три месяца в заключении на Карловой площади и умер 4 августа 1945 года от истощения, тридцати пяти лет от роду.
Он успел напечатать восемь работ. Из них выросли теория доказательств как дисциплина, ординальный анализ, стандартный способ преподавания логики и техническая основа систем автоматического поиска доказательств.
Следующая точка: Иваново — где преподаватель пединститута докажет теорему, из которой вырастет теория моделей.