Герхард Генцен: доказательство, стоившее жизни

Герхард Генцен был одним из самых блестящих учеников Давида Гильберта. Он посвятил свою короткую жизнь попытке спасти программу своего учителя — доказать непротиворечивость арифметики.
Момент прорыва:
После того как Гёдель показал, что непротиворечивость арифметики нельзя доказать средствами самой арифметики, Генцен пошел на хитрость. В 1936 году он доказал непротиворечивость арифметики, используя трансфинитную индукцию вплоть до ординала ε₀. Это было за пределами формальной арифметики, но оставалось в области «конструктивного» разума. Гильберт был в восторге: программа была спасена, пусть и в измененном виде.
Драма:
Началась Вторая мировая война. Генцен был мобилизован. В 1945 году, в последние недели войны, он был арестован в Праге как «вражеский иностранец» (из-за своего интереса к трудам польских логиков) и брошен в тюрьму. Он умер от истощения в возрасте 36 лет, так и не увидев триумфа своих идей.
Наследие:
Система естественного вывода Генцена сегодня преподается на каждом курсе математической логики. Его доказательство непротиворечивости открыло целую область — ординальный анализ.
«Логика — это гигиена мысли, не позволяющая ей заражаться предрассудками и суевериями». Герхард Генцен следовал этому принципу до самого конца.