Gerhard Gentzen
Gerhard Karl Erich Gentzen (* November 24, 1909 in Greifswald, † August 4, 1945 in Prague ) was a German mathematician and logician.
Mathematical services
Gentzen is an important founders of modern mathematical proof theory. The enduring importance in his development of the methods, rules and structures seen today, especially in important areas of computer science, the verification of programs. This formal proofs themselves are interpreted as programs.
Gentzen was one of the leaders of the international working mathematical basic research and presented in 1936 and 1938 in the National Socialist German magazine mathematics respectively the state of basic research dar.
Based on the Hilbert- between program proving Gentzen for establishing the mathematics the consistency of number theory. He developed one of the first systems and natural deduction calculi sequences (also commonly Gentz type calculus ) for which he proved the so-called " law ". Thus, large parts of logic and mathematics provable as consistent.
Life
Gentzen was used in 1939 to 1941 in the war as a radio operator in Braunschweig, but fell ill and was subsequently exempted from military service. In 1940 he completed his habilitation in Göttingen. 1943 Gentzen was appointed by Hans Rohrbach to a lectureship at the German University in Prague. In addition to lecturing and research on the consistency of mathematics led Gentzen in Prague a group of high school students, the calculations conducted. Despite warnings Gentzen did not flee when the war ended in Germany. He died on 4 August 1945 in the county jail on Charles Square in Prague from malnutrition - three months after his arrest.
Quote
" It can also be expressed by saying that for number theory no one can specify for all adequate system of methods of inference, but rather that repeatedly sets can be found whose proofs require new methods of inference. "
" The predicate " awesome " is right here on the site. If you look at the work that produced the Hilbert school these days (to put it anachronistically to say, a "paradise of hackers" ) who is experienced Gentzen's method as a miracle of beauty. Outsiders think very quickly in logic ( and mathematics ) to a boring work for Trauerklösse, but you can believe me on my word that we are dealing here of a beauty of almost symphonic format. "
Works
- : On the existence of independent systems of axioms for infinite set systems. In: Mathematische Annalen. 107 (2 ), 1932, pp. 329-350.
- : Studies on logical reasoning. I. In: Mathematical Journal. 39 (2 ), 1934, pp. 176-210.
- : Studies on logical reasoning. II In: Mathematical Journal. 39 (3 ), 1935, pp. 405-431. Reprint in: Karel Berka, Lothar Kreiser: logic texts. Commenting selection on the history of modern logic, Berlin: Akademie 4th edition, 1986, page 206-261
Posthumous
- Summary of several full inductions into one. In: Archive for mathematical logic and basic research. 2 (1 ), 1954, pp. 81-93.
- The first consistency proof for classical number theory. In: Archive for mathematical logic and basic research. 16, 1974, p 97-118. - Posted by Paul Bernays.
- : On the relation between intuitionistic and classical arithmetic. In: Archive for mathematical logic and basic research. 16, 1974, p 119-132. - Posted by Paul Bernays.
English translation
- Gerhard Gentzen: Publisher ME Szabo (ed.): The Collected Papers of Gerhard Gentzen. North -Holland, Amsterdam, 1969, ISBN 0-7204 2254 - X.