Gerhard Gentzen
Encyclopedia
Gerhard Karl Erich Gentzen (November 24, 1909, Greifswald
, Germany
– August 4, 1945, Prague
, Czechoslovakia
) was a German
mathematician
and logician. He had his major contributions in the foundations of mathematics
, proof theory
, especially on natural deduction
and sequent calculus
. He died in 1945 after the Second World War, because he was deprived of food after being arrested in Prague
.
at the University of Göttingen. Bernays was fired as "non-Aryan
" in April 1933 and therefore Hermann Weyl
formally acted as his supervisor. At great risk to his career Gentzen kept in contact with Bernays until the beginning of the Second World War. In November 1933, he joined the Sturmabteilung
to pass the state exam for teachers. In 1935, he corresponded with Abraham Fraenkel from Jerusalem and was implicated by the Nazi teachers' union as one who "keeps contacts to the Chosen People
." In 1935 and 1936, Hermann Weyl, head of the Göttingen mathematics department in 1933 until his resignation under Nazi pressure, made strong efforts to bring him to the Institute for Advanced Study
in Princeton.
Between November 1935 and 1939 he was an assistant of David Hilbert
in Göttingen. To be able to take part in a congress in Paris in 1937, he had to join the NSDAP
. One of Gentzen's papers had a second publication in the ill-famed Deutsche Mathematik that was founded by Ludwig Bieberbach
who promoted "Aryan" mathematics.
From 1943 he was a teacher at the University of Prague
. After the war he starved to death in Prague
, after being arrested like all other Germans in Prague on May 7, 1945 and deprived of food.
Gentzen's main work was on the foundations of mathematics
, in proof theory
, specifically natural deduction
and the sequent calculus
. His cut-elimination theorem
is the cornerstone of proof-theoretic semantics
, and some philosophical remarks in his "Investigations into Logical Deduction", together with Ludwig Wittgenstein
's aphorism that "meaning is use", constitute the starting point for inferential role semantics
.
Gentzen proved the consistency
of the Peano axioms
in a paper published in 1936. In his Habilitation
sschrift, finished in 1939, he determined the proof-theoretical strength of Peano arithmetic. This was done by a direct proof of the unprovability of the principle of transfinite induction, used in his 1936 proof of consistency, within Peano arithmetic. The principle can, however, be expressed in arithmetic, so that a direct proof of Gödel's incompleteness theorem followed. Gödel used an artificial coding procedure to construct an unprovable formula of arithmetic. Gentzen's proof was published in 1943 and marked the beginning of ordinal proof theory
.
Greifswald
Greifswald , officially, the University and Hanseatic City of Greifswald is a town in northeastern Germany. It is situated in the state of Mecklenburg-Vorpommern, at an equal distance of about from Germany's two largest cities, Berlin and Hamburg. The town borders the Baltic Sea, and is crossed...
, Germany
Germany
Germany , officially the Federal Republic of Germany , is a federal parliamentary republic in Europe. The country consists of 16 states while the capital and largest city is Berlin. Germany covers an area of 357,021 km2 and has a largely temperate seasonal climate...
– August 4, 1945, Prague
Prague
Prague is the capital and largest city of the Czech Republic. Situated in the north-west of the country on the Vltava river, the city is home to about 1.3 million people, while its metropolitan area is estimated to have a population of over 2.3 million...
, Czechoslovakia
Czechoslovakia
Czechoslovakia or Czecho-Slovakia was a sovereign state in Central Europe which existed from October 1918, when it declared its independence from the Austro-Hungarian Empire, until 1992...
) was a German
Germany
Germany , officially the Federal Republic of Germany , is a federal parliamentary republic in Europe. The country consists of 16 states while the capital and largest city is Berlin. Germany covers an area of 357,021 km2 and has a largely temperate seasonal climate...
mathematician
Mathematician
A mathematician is a person whose primary area of study is the field of mathematics. Mathematicians are concerned with quantity, structure, space, and change....
and logician. He had his major contributions in the foundations of mathematics
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
, proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, especially on natural deduction
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
and sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
. He died in 1945 after the Second World War, because he was deprived of food after being arrested in Prague
Prague
Prague is the capital and largest city of the Czech Republic. Situated in the north-west of the country on the Vltava river, the city is home to about 1.3 million people, while its metropolitan area is estimated to have a population of over 2.3 million...
.
Life and career
Gentzen was a student of Paul BernaysPaul Bernays
Paul Isaac Bernays was a Swiss mathematician, who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant to, and close collaborator of, David Hilbert.-Biography:Bernays spent his childhood in Berlin. Bernays attended the...
at the University of Göttingen. Bernays was fired as "non-Aryan
Aryan
Aryan is an English language loanword derived from Sanskrit ārya and denoting variously*In scholarly usage:**Indo-Iranian languages *in dated usage:**the Indo-European languages more generally and their speakers...
" in April 1933 and therefore Hermann Weyl
Hermann Weyl
Hermann Klaus Hugo Weyl was a German mathematician and theoretical physicist. Although much of his working life was spent in Zürich, Switzerland and then Princeton, he is associated with the University of Göttingen tradition of mathematics, represented by David Hilbert and Hermann Minkowski.His...
formally acted as his supervisor. At great risk to his career Gentzen kept in contact with Bernays until the beginning of the Second World War. In November 1933, he joined the Sturmabteilung
Sturmabteilung
The Sturmabteilung functioned as a paramilitary organization of the National Socialist German Workers' Party . It played a key role in Adolf Hitler's rise to power in the 1920s and 1930s...
to pass the state exam for teachers. In 1935, he corresponded with Abraham Fraenkel from Jerusalem and was implicated by the Nazi teachers' union as one who "keeps contacts to the Chosen People
Chosen people
Throughout history and even today various groups of people have considered themselves as chosen by a deity for some purpose such as to act as the deity's agent on earth. In monotheistic faiths, like Abrahamic religions, references to God are used in constructs such as "God's Chosen People"...
." In 1935 and 1936, Hermann Weyl, head of the Göttingen mathematics department in 1933 until his resignation under Nazi pressure, made strong efforts to bring him to the Institute for Advanced Study
Institute for Advanced Study
The Institute for Advanced Study, located in Princeton, New Jersey, United States, is an independent postgraduate center for theoretical research and intellectual inquiry. It was founded in 1930 by Abraham Flexner...
in Princeton.
Between November 1935 and 1939 he was an assistant of David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
in Göttingen. To be able to take part in a congress in Paris in 1937, he had to join the NSDAP
National Socialist German Workers Party
The National Socialist German Workers' Party , commonly known in English as the Nazi Party, was a political party in Germany between 1920 and 1945. Its predecessor, the German Workers' Party , existed from 1919 to 1920...
. One of Gentzen's papers had a second publication in the ill-famed Deutsche Mathematik that was founded by Ludwig Bieberbach
Ludwig Bieberbach
Ludwig Georg Elias Moses Bieberbach was a German mathematician.-Biography:Born in Goddelau, near Darmstadt, he studied at Heidelberg and under Felix Klein at Göttingen, receiving his doctorate in 1910. His dissertation was titled On the theory of automorphic functions...
who promoted "Aryan" mathematics.
From 1943 he was a teacher at the University of Prague
Charles University in Prague
Charles University in Prague is the oldest and largest university in the Czech Republic. Founded in 1348, it was the first university in Central Europe and is also considered the earliest German university...
. After the war he starved to death in Prague
Prague
Prague is the capital and largest city of the Czech Republic. Situated in the north-west of the country on the Vltava river, the city is home to about 1.3 million people, while its metropolitan area is estimated to have a population of over 2.3 million...
, after being arrested like all other Germans in Prague on May 7, 1945 and deprived of food.
Gentzen's main work was on the foundations of mathematics
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, in proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, specifically natural deduction
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
and the sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
. His cut-elimination theorem
Cut-elimination theorem
The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively...
is the cornerstone of proof-theoretic semantics
Proof-theoretic semantics
Proof-theoretic semantics is an approach to the semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within the system...
, and some philosophical remarks in his "Investigations into Logical Deduction", together with Ludwig Wittgenstein
Ludwig Wittgenstein
Ludwig Josef Johann Wittgenstein was an Austrian philosopher who worked primarily in logic, the philosophy of mathematics, the philosophy of mind, and the philosophy of language. He was professor in philosophy at the University of Cambridge from 1939 until 1947...
's aphorism that "meaning is use", constitute the starting point for inferential role semantics
Inferential role semantics
Inferential role semantics is an approach to the theory of meaning that identifies the meaning of an expression with its relationship to other expressions, typically its inferential relations with other expressions. Proponents include Robert Brandom, Gilbert Harman, Paul Horwich, and Ned Block...
.
Gentzen proved the consistency
Gentzen's consistency proof
Gentzen's consistency proof is a result of proof theory in mathematical logic. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved , but to clarified logical principles.-Gentzen's theorem:In 1936 Gerhard Gentzen proved the consistency of...
of the Peano axioms
Peano axioms
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano...
in a paper published in 1936. In his Habilitation
Habilitation
Habilitation is the highest academic qualification a scholar can achieve by his or her own pursuit in several European and Asian countries. Earned after obtaining a research doctorate, such as a PhD, habilitation requires the candidate to write a professorial thesis based on independent...
sschrift, finished in 1939, he determined the proof-theoretical strength of Peano arithmetic. This was done by a direct proof of the unprovability of the principle of transfinite induction, used in his 1936 proof of consistency, within Peano arithmetic. The principle can, however, be expressed in arithmetic, so that a direct proof of Gödel's incompleteness theorem followed. Gödel used an artificial coding procedure to construct an unprovable formula of arithmetic. Gentzen's proof was published in 1943 and marked the beginning of ordinal proof theory
Ordinal analysis
In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. The field was formed when Gerhard Gentzen in 1934 used cut elimination to prove, in modern terms, that the proof theoretic ordinal of Peano arithmetic is ε0.-Definition:Ordinal...
.