History
Although the formalisation of logic was much advanced by the work of such figures as Gottlob Frege, Giuseppe Peano, Bertrand Russell, and Richard Dedekind, the story of modern proof theory is often seen as being established by David Hilbert, who initiated what is called Hilbert's program in the foundations of mathematics. Kurt Gödel's seminal work on proof theory first advanced, then refuted this program: his completeness theorem initially seemed to bode well for Hilbert's aim of reducing all mathematics to a finitist formal system; then his incompleteness theorems showed that this is unattainable. All of this work was carried out with the proof calculi called the Hilbert systems.
In parallel, the foundations of structural proof theory were being founded. Jan Łukasiewicz suggested in 1926 that one could improve on Hilbert systems as a basis for the axiomatic presentation of logic if one allowed the drawing of conclusions from assumptions in the inference rules of the logic. In response to this Stanisław Jaśkowski (1929) and Gerhard Gentzen (1934) independently provided such systems, called calculi of natural deduction, with Gentzen's approach introducing the idea of symmetry between the grounds for asserting propositions, expressed in introduction rules, and the consequences of accepting propositions in the elimination rules, an idea that has proved very important in proof theory. Gentzen (1934) further introduced the idea of the sequent calculus, a calculus advanced in a similar spirit that better expressed the duality of the logical connectives, and went on to make fundamental advances in the formalisation of intuitionistic logic, and provide the first combinatorial proof of the consistency of Peano arithmetic. Together, the presentation of natural deduction and the sequent calculus introduced the fundamental idea of analytic proof to proof theory,
Read more about this topic: Proof Theory
Famous quotes containing the word history:
“No one can understand Paris and its history who does not understand that its fierceness is the balance and justification of its frivolity. It is called a city of pleasure; but it may also very specially be called a city of pain. The crown of roses is also a crown of thorns. Its people are too prone to hurt others, but quite ready also to hurt themselves. They are martyrs for religion, they are martyrs for irreligion; they are even martyrs for immorality.”
—Gilbert Keith Chesterton (1874–1936)
“The history of progress is written in the blood of men and women who have dared to espouse an unpopular cause, as, for instance, the black man’s right to his body, or woman’s right to her soul.”
—Emma Goldman (1869–1940)
“It would be naive to think that peace and justice can be achieved easily. No set of rules or study of history will automatically resolve the problems.... However, with faith and perseverance,... complex problems in the past have been resolved in our search for justice and peace. They can be resolved in the future, provided, of course, that we can think of five new ways to measure the height of a tall building by using a barometer.”
—Jimmy Carter (James Earl Carter, Jr.)