Герхард Генцен
Герхард Карл Эрих Генцен (нем. Gerhard Karl Erich Gentzen; * 24 ноября 1909, Грайфсвальд, Мекленбург — † 4 августа 1945, Прага) — немецкий математик и логик, внёсший большой вклад в исследование оснований математики и развитие теории доказательств, является создателем исчисления секвенций.
Биография[править | править код]
Родился в семье адвоката, имевшего практику в Бергене на острове Рюген. Учился в школе, затем в гимназии. Его отец погиб на фронте мировой войны и в 1920 Генцен с матерью переехали в Штральзунд.[1]
Окончив в 1928 годугимназию в Штральзунде с высшим знаком отличия, получил стипендию немецкого студенческого фонда, позволившую ему продолжить академическое образование. После двух семестров учебы в Грейфсвальдском университете, 22 апреля 1929 был принят в Геттингенский университет, в котором занимался два семестра, затем один семестр — в Мюнхене, один — в Берлине и снова вернулся в Геттинген, где работал под руководством Г.Вейля. Летом 1933 получил докторскую степень по математике. После недолгого перерыва в научной работе, связанного с ухудшением здоровья, Генцена снова приглашают в Геттинген в качестве ассистента Гильберта, там он работал и после ухода последнего на пенсию.[2]
В 1933 году вступил в СА.
Член НСДАП с 1937 года.
В 1937 году Генцен выступает на Конгрессе в Париже с докладом «Концепция бесконечности и последовательности математики». Его выдающаяся деятельность математика, прекращается с началом Второй мировой войны.
В апреле 1939 года, как новоизбранный академик, Генцен даёт присягу верности Адольфу Гитлеру.
В начале 2-й мировой войны был призван в армию, но через два года демобилизован по болезни. После выздоровления вернулся в Геттингенский университет, где в 1942 получил степень доктора философии. Осенью 1943 по приглашению директора Математического института Немецкого университета в Праге Генцен занял должность доцента этого университета и преподавал до 5 мая 1945, когда был арестован новыми властями.[2]
Участник разработок Фау-2.
Он умер в возрасте 35 лет в окружной тюрьме Карлсплатц от голода, так как на протяжении нескольких месяцев был лишён пищи.
Научные достижения[править | править код]
Генцен работал в основном в русле финитизма в математике. Его научные интересы относятся к области математической логики и оснований математики. Его труды, опубликованные в 1932‒34, посвящены анализу логических выводов, доказательству непротиворечивсти элементарной теории чисел и простой теории типов, а также анализу соотношения между интуиционистской и классической арифметикой, понятию бесконечности в математике и проблеме существования независимых аксиом для бесконечных систем предложений. Наибольший вклад Генцен внес в доказательств теорию. Самой известной его работой является «Исследование логических выводов» (1935, рус. пер. 1967), в которой представлены новые формы построения классической и интуиционистской логик в виде систем натурального вывода и исчислений секвенций, а также фундаментальный результат современной математической логики — доказана теорема об устранении сечения (элиминационная теорема).[3] Фактически, эта работа положила начало новому направлению в теории доказательств. Глубокие и методологически перспективные идеи Генцена, относящиеся к понятиям доказуемости и недоказуемости в математике и логике, к способам обоснования непротиворечивости формальных теорий, стимулировали множество новых исследований по основаниям математики и связанных с этим фундаментальных философских проблем. По свидетельству одного из его друзей, Генцен незадолго до своей смерти выражал полную уверенность в том, что может представить доказательство непротиворечивости математического анализа.[2]
Система натурального исчисления[править | править код]
В 1934 году разработал систему натурального исчисления. В соответствии с общепринятыми способами рассуждений, в натуральном исчислении допускается не только вывод истинных предложений из истинных посылок, но и вывод следствий из гипотез. В то время как теоремы аксиоматических систем логики высказываний и предикатов являются результатом последовательного применения правил вывода к некоторым исходным истинным формулам (аксиомам), в натуральном исчислении никакие формулы заранее не предполагаются истинными — в натуральном исчислении нет аксиом, а есть лишь правила вывода. Формальный аппарат натурального исчисления был близок к разработанному позже также Генценом исчислению секвенций.[4]
В 1935 году ввёл символ ∀ для квантора всеобщности.
Доказательство непротиворечивости[править | править код]
В 1900 году Гильберт сформулировал список т. н. задач столетия, вторая из которых звучит так: «доказать непротиворечивость арифметики». Вопрос статуса этой задачи очень забавен. Дело в том, что Курт Гёдель[5] в 1931 году доказал, что это невозможно, а Герхард Генцен в 1936 году доказал её непротиворечивость.[6] Для этого Генцену пришлось прибегнуть к оригинальному спорному методу, известному как бесконечная (бескванторная) индукция. Эта последняя не относилась к обычным методам доказательства и показалась учёному сообществу мало уместной.
Аналитическая дедукция[править | править код]
Естественная дедукция (англ. Natural deduction или Hilbert-style deduction)[7] является формальным отражением обычной практики ведения доказательств со времён Эвклида и Аристотеля в форме объясняющих текстов. Современная её формализация принадлежит перу Генцена, до этого её успешно (но менее элегантно) формализовали Гильберт и Фреге.
Для доказательства правоты своих методов Генцен создал систему Аналитической дедукции (англ. Analytic deduction), для которой:
- Разработал алгоритмы, превращающие Natural deduction в Analytic deduction и доказал их корректность.
- Доказал, что никакое арифметическое доказательство в форме аналитической дедукции не может выводить ложное утверждение.
- Доказал завершённость алгоритма Генцена.
Теоретико-доказательная семантика,[8] связывающая смысл утверждений с ролями, которые они играют в рассуждении, стала продолжением исчисления секвенций. Основателями её считаются Герхард Генцен, Дэг Превитц и Майкл Даммит.
Сочинения[править | править код]
- Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen. — «Mathematische Annalen», 107 (1932);
- Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik. Galley Proof. — Ibid. (1933), received on 15th March 1933;
- Untersuchungen über das logische Schliessen. — «Mathematische Zeitschrift», (1935);
- Die Widerspruchsfreiheit der reinen Zahlentheorie. — «Mathematische Annalen», 112 (1936);
- Appendix: Galley Proof. — Ibid. (1935), received on 1th August 1935;
- Die gegenwärtige Lage in der mathematischen Grundlagenforschung. — Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, New Series, N 4, Lp. (Hirzel), (1938);
- Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. — Ibid.;
- Collected Papers of Gerhard Gentzen, ed. by M. Ε. Szabo. Studies in Logic and the Foudations of Mathematics. Amst. — L., 1969;
- Исследования логических выводов. — В кн.: Математическая теория логического вывода. М., 1967;
- Непротиворечивость чистой теории чисел. — Там же;
- Новое изложение доказательства непротиворечивости для чистой теории чисел. — Там же.
Ссылки[править | править код]
- ↑ Герхард Генцен
- ↑ а б в Генцен. Новая философская энциклопедия: В 4 тт. М.: Мысль. Под редакцией В. С. Стёпина. 2001.
- ↑ en:Cut-elimination theorem
- ↑ Натуральное исчисление. Философская Энциклопедия. В 5-х т. — М.: Советская энциклопедия. Под редакцией Ф. В. Константинова. 1960—1970
- ↑ Биография Курта Гёделя
- ↑ Гёдель против Гентцена
- ↑ en:Natural deduction
- ↑ en:Proof-theoretic semantics