Герхард Генцен

Программа Гильберта требовала доказать непротиворечивость арифметики средствами самой арифметики. Гёдель в 1930 году показал, что это невозможно. Через несколько лет Генцен непротиворечивость доказал. Противоречия тут нет — и разобраться, почему, полезнее, чем помнить оба факта по отдельности.

Натуральный вывод

Родился в 1909 году в Грайфсвальде, в семье адвоката. Учился в Гёттингене; научным руководителем был Герман Вейль, но фактически он работал в кругу Гильберта и Бернайса.

Диссертация 1933 года содержит две вещи, которыми пользуется всякий, кто занимается доказательствами формально.

Натуральный вывод — система правил, в которой рассуждение выглядит так, как рассуждает человек: у каждой связки есть правило введения («как доказать А и Б») и правило удаления («что следует из А и Б»). До Генцена логические исчисления состояли из аксиом и modus ponens и на человеческое рассуждение походили мало.

Секвенциальное исчисление и теорема об устранении сечения (Hauptsatz). Сечение — это использование вспомогательной леммы: доказали Б из А, доказали В из Б, заключили В из А. Генцен доказал, что всякий вывод можно переписать без сечений — то есть без лемм, напрямую.

Следствие огромно. В выводе без сечений все формулы — подформулы заключения; ничего постороннего изобретать не нужно. Отсюда разрешающие процедуры, автоматический поиск доказательств и — через соответствие Карри — Ховарда — вычисление как нормализация вывода: устранение сечения есть в точности исполнение программы.

Чем измеряется арифметика

В середине тридцатых Генцен доказал непротиворечивость арифметики Пеано. Средство, выводящее за её пределы, названо им явно: трансфинитная индукция до ординала $\varepsilon_0$.

Что такое $\varepsilon_0$: предел башни $\omega, \omega^{\omega}, \omega^{\omega^{\omega}},\ldots$ — наименьший ординал, для которого $\varepsilon_0 = \omega^{\varepsilon_0}$. Каждый отдельный шаг такой индукции арифметике доступен, вся индукция целиком — нет; ровно поэтому теорема Гёделя не нарушена.

Смысл результата — не «спасение» программы Гильберта, а измерение. Теперь у теории есть числовая характеристика: её теоретико-доказательственный ординал, то, докуда надо досчитать, чтобы обосновать её непротиворечивость. У арифметики Пеано это $\varepsilon_0$; у более сильных теорий — большие ординалы. Так родилась теория доказательств как наука о силе теорий.

Тот же ординал всплыл потом самостоятельно: недоказуемость теоремы Гудстейна и теоремы Кирби — Париса объясняется тем, что они требуют индукции до $\varepsilon_0$.

Прага

Тут кончается математика и начинается то, что о Генцене приходится сказать. В 1933 году он вступил в СА, в 1937-м — в НСДАП. В 1935-м участвовал в разборе «арийской» и «еврейской» математики; в 1943-м получил место в Немецком университете Праги и работал там, в том числе по заданиям, связанным с военными расчётами.

В мае 1945 года, после освобождения Праги, всех немецких преподавателей университета арестовали. Генцен умер в тюрьме 4 августа 1945 года от истощения, тридцати пяти лет.

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