Введение

Германский математик Герхард Карл Эрих Гентцен (24 ноября 1909 – 4 августа 1945) был немецким математиком и логиком. Он внес значительный вклад в основания математики и теорию доказательств, особенно в области естественной дедукции и исчисления секвенций. Он умер от голода в чешском лагере для интернированных в Праге в 1945 году, будучи интернированным как гражданин Германии после Второй мировой войны.

Жизнь и карьера

Гентцен был студентом Пола Бернейса в Геттингенском университете. Бернейс был уволен как "неарийский" в апреле 1933 года, и поэтому Герман Вейль формально стал его научным руководителем. Гентцен вступил в штурмовые отряды (Sturmabteilung) в ноябре 1933 года, хотя к этому его ни в коем случае не принуждали. Тем не менее, он поддерживал связь с Бернейсом до начала Второй мировой войны. В 1935 году он переписывался с Абрахамом Френкелем в Иерусалиме и был обвинён нацистским профсоюзом учителей в поддержании контактов с "избранным народом". В 1935 и 1936 годах Герман Вейль, возглавлявший математический факультет Геттингенского университета в 1933 году до своей отставки под нацистским давлением, приложил значительные усилия, чтобы пригласить его в Институт перспективных исследований в Принстоне. С ноября 1935 по 1939 год он был ассистентом Давида Гильберта в Геттингене. Гентцен вступил в нацистскую партию в 1937 году. В апреле 1939 года Гентцен принёс присягу на верность Адольфу Гитлеру в связи со своей академической должностью. С 1943 года он преподавал в немецком университете Карла Фердинанда в Праге. По контракту с СС, Гентцен работал над проектом V-2. Гентцен был арестован во время Пражского восстания против оккупационных немецких войск 5 мая 1945 года. Он вместе с остальными сотрудниками немецкого университета в Праге был заключён в советский лагерь, где умер от голода 4 августа 1945 года.

Работа

Основная работа Гентцена была посвящена основам математики, в теории доказательств, в частности, естественной дедукции и исчислению секвенций. Его теорема об устранении обрезаний является краеугольным камнем теоретической семантики доказательств, а некоторые философские замечания в его «Исследованиях логической дедукции» вместе с поздними работами Людвига Витгенштейна составляют отправную точку для семантики инференциальных ролей. Одна из работ Гентцена была вторично опубликована в идеологическом журнале Deutsche Mathematik, основанном Людвигом Бибербахом, который продвигал «арийскую» математику. Гентцен доказал непротиворечивость аксиом Пеано в статье, опубликованной в 1936 году. В своей работе Habilitationsschrift, завершенной в 1939 году, он определил доказательную силу арифметики Пеано. Это было сделано путем прямого доказательства недоказуемости принципа трансфинитной индукции, использованного в его доказательстве непротиворечивости 1936 года, средствами арифметики Пеано. Однако этот принцип может быть выражен в арифметике, что привело к прямому доказательству теоремы о неполноте Гёделя. Гёдель использовал процедуру кодирования для построения недоказуемой формулы арифметики. Доказательство Гентцена было опубликовано в 1943 году и ознаменовало начало ординальной теории доказательств.

Посмертно

(Английский перевод). – Издано Полом Бернейсом. – Издано Полом Бернейсом. – Издано Яном фон Плато.