On Formally Undecidable Propositions of Principia Mathematica and Related Systems
Encyclopedia
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I ("On Formally Undecidable Propositions of Principia Mathematica and Related Systems I") is a paper in mathematical logic
by Kurt Gödel
. Dated November 17, 1930, it was originally published in German in the 1931 volume of Monatshefte für Mathematik. Several English translations have appeared in print, and the paper has been included in two collections of classic mathematical logic papers. The paper is famous for the theorems it contains, which have many implications for consistency proof
s in mathematics, and for the techniques that Gödel invented to prove these theorems.
, which have had an enormous impact on the field of mathematical logic
. These appear as theorems VI and XI, respectively, in the paper.
In order to prove these results, Gödel introduced in this paper a method now known as Gödel numbering. In this method, each sentence and formal proof in first-order arithmetic is assigned a particular natural number. Gödel shows that many properties of these proofs can be defined within any theory of arithmetic that is strong enough to define the primitive recursive function
s. (The contemporary terminology for recursive function
s and primitive recursive function
s had not yet been established when the paper was published; Gödel used the word rekursiv ("recursive") for what are now known as primitive recursive functions.) The method of Gödel numbering has since become common in mathematical logic.
Because the method of Gödel numbering was novel, and to avoid any ambiguity, Gödel presented a list of 45 explicit formal definitions of primitive recursive functions and relations used to manipulate and test Gödel numbers. He used these to give an explicit definition of a formula Bew(x) that is true if and only if x is the Gödel number of a sentence φ and there exists a natural number that is the Gödel number of a proof of φ (The German word for proof is Beweis).
A second new technique invented by Gödel in this paper was the use of self-referential sentences. Gödel showed that the classical paradox
es of self-reference, such as "This statement is false
," can be recast as self-referential formal sentences of arithmetic. Informally,
the sentence employed to prove Gödel's first incompleteness theorem says "This statement is not provable." The fact that such self-reference can be expressed within arithmetic was not known until Gödel's paper appeared; independent work of Alfred Tarski
on his indefinability theorem
was conducted around the same time but not published until 1936.
In footnote 48a, Gödel stated that a planned second part of the paper would establish a link between consistency proofs and type theory, but Gödel did not publish a second part of the paper before his death. His 1958 paper in Dialectica did, however, show how type theory can be used to give a consistency proof for arithmetic.
(1966). According to Dawson's biography of Gödel (Dawson 1997:216),
The translation by Elliott Mendelson appears in the collection The Undecidable (Davis
1965:5ff). This translation also received a harsh review by Bauer-Medelburg (1965), who in addition to giving a detailed list of the typographical errors also described what he believed to be serious errors in the translation.
A translation by Jean van Heijenoort
appears in the collection From Frege to Gödel: A source book in Mathematical Logic (van Heijenoort 1967). A review by Alonzo Church
(1972) described this as "the most careful translation that has been made" but also gave some specific criticisms of it. Dawson (1997:216) notes:
This approval process was laborious. Gödel introduced changes to his text of 1931, and negotiations between the men were "protracted": "Privately van Heijenoort declared that Gödel was the most doggedly fastidious individual he had ever known." Between them they "exchanged a total of seventy letters and met twice in Gödel's office in order to resolve questions concerning subtleties in the meanings and usage of German and English words." (Dawson 1997:216-217).
Although not a translation of the original paper, a very useful 4th version exists that "cover[s] ground quite similar to that covered by Godel's original 1931 paper on undecidability" (Davis 1952:39), as well as Gödel's own extensions of and commentary on the topic. This appears as On Undecidable Propositions of Formal Mathematical Systems (Davis 1965:39ff) and represents the lectures as transcribed by Stephen Kleene and J. Barkley Rosser while Gödel delivered them at the Institute for Advanced Study in Princeton N.J. in 1934. Two pages of errata and additional corrections by Gödel were added by Davis to this version. This version is also notable because in it Gödel first describes the Herbrand suggestion that gave rise to the (general, i.e. Herbrand-Gödel) form of recursion
.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
by Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
. Dated November 17, 1930, it was originally published in German in the 1931 volume of Monatshefte für Mathematik. Several English translations have appeared in print, and the paper has been included in two collections of classic mathematical logic papers. The paper is famous for the theorems it contains, which have many implications for consistency proof
Consistency proof
In logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if and only if it has a model, i.e. there exists an interpretation under which all...
s in mathematics, and for the techniques that Gödel invented to prove these theorems.
Outline and key results
The main results established are Gödel's first and second incompleteness theoremsGödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
, which have had an enormous impact on the field of mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
. These appear as theorems VI and XI, respectively, in the paper.
In order to prove these results, Gödel introduced in this paper a method now known as Gödel numbering. In this method, each sentence and formal proof in first-order arithmetic is assigned a particular natural number. Gödel shows that many properties of these proofs can be defined within any theory of arithmetic that is strong enough to define the primitive recursive function
Primitive recursive function
The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
s. (The contemporary terminology for recursive function
Recursive function
Recursive function may refer to:*Recursion , a procedure or subroutine, implemented in a programming language, whose implementation references itself*A total computable function, a function which is defined for all possible inputs...
s and primitive recursive function
Primitive recursive function
The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
s had not yet been established when the paper was published; Gödel used the word rekursiv ("recursive") for what are now known as primitive recursive functions.) The method of Gödel numbering has since become common in mathematical logic.
Because the method of Gödel numbering was novel, and to avoid any ambiguity, Gödel presented a list of 45 explicit formal definitions of primitive recursive functions and relations used to manipulate and test Gödel numbers. He used these to give an explicit definition of a formula Bew(x) that is true if and only if x is the Gödel number of a sentence φ and there exists a natural number that is the Gödel number of a proof of φ (The German word for proof is Beweis).
A second new technique invented by Gödel in this paper was the use of self-referential sentences. Gödel showed that the classical paradox
Paradox
Similar to Circular reasoning, A paradox is a seemingly true statement or group of statements that lead to a contradiction or a situation which seems to defy logic or intuition...
es of self-reference, such as "This statement is false
Liar paradox
In philosophy and logic, the liar paradox or liar's paradox , is the statement "this sentence is false"...
," can be recast as self-referential formal sentences of arithmetic. Informally,
the sentence employed to prove Gödel's first incompleteness theorem says "This statement is not provable." The fact that such self-reference can be expressed within arithmetic was not known until Gödel's paper appeared; independent work of Alfred Tarski
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
on his indefinability theorem
Tarski's indefinability theorem
Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1936, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics...
was conducted around the same time but not published until 1936.
In footnote 48a, Gödel stated that a planned second part of the paper would establish a link between consistency proofs and type theory, but Gödel did not publish a second part of the paper before his death. His 1958 paper in Dialectica did, however, show how type theory can be used to give a consistency proof for arithmetic.
Published English translations
During his lifetime three English translations of Gödel's paper were printed, but the process was not without difficulty. The first English translation was by Bernard Meltzer; it was published in 1963 as a standalone work by Basic Books and has since been reprinted by Dover and reprinted by Hawking (God Created the Integers, Running Press, 2005:1097ff). The Meltzer version was adversely reviewed by Raymond SmullyanRaymond Smullyan
Raymond Merrill Smullyan is an American mathematician, concert pianist, logician, Taoist philosopher, and magician.Born in Far Rockaway, New York, his first career was stage magic. He then earned a BSc from the University of Chicago in 1955 and his Ph.D. from Princeton University in 1959...
(1966). According to Dawson's biography of Gödel (Dawson 1997:216),
"Fortunately, the Meltzer translation was soon supplanted by a better one prepared by Elliott Mendelson for Martin Davis's anthology The Undecidable; but it too was not brought to Gödel's attention until almost the last minute, and the new translation was still not wholly to his liking ... when informed that there was not time enough to consider substituting another text, he declared that Mendelson's translation was 'on the whole very good' and agreed to its publication.3 [3 Afterward he would regret his compliance, for the published volume was marred throughout by sloppy typography and numerous misprints.]
The translation by Elliott Mendelson appears in the collection The Undecidable (Davis
Martin Davis
Martin David Davis, is an American mathematician, known for his work on Hilbert's tenth problem . He received his Ph.D. from Princeton University in 1950, where his adviser was Alonzo Church . He is Professor Emeritus at New York University. He is the co-inventor of the Davis-Putnam and the DPLL...
1965:5ff). This translation also received a harsh review by Bauer-Medelburg (1965), who in addition to giving a detailed list of the typographical errors also described what he believed to be serious errors in the translation.
A translation by Jean van Heijenoort
Jean Van Heijenoort
Jean Louis Maxime van Heijenoort was a pioneer historian of mathematical logic. He was also a personal secretary to Leon Trotsky from 1932 to 1939, and from then until 1947, an American Trotskyist activist.-Life:Van Heijenoort was born in Creil, France...
appears in the collection From Frege to Gödel: A source book in Mathematical Logic (van Heijenoort 1967). A review by Alonzo Church
Alonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
(1972) described this as "the most careful translation that has been made" but also gave some specific criticisms of it. Dawson (1997:216) notes:
"The translation Gödel favored was that by Jean van Heijenoort ... In the preface to the volume van Heijenoort noted that Gödel was one of four authors who had personally read and approved the translations of his works."
This approval process was laborious. Gödel introduced changes to his text of 1931, and negotiations between the men were "protracted": "Privately van Heijenoort declared that Gödel was the most doggedly fastidious individual he had ever known." Between them they "exchanged a total of seventy letters and met twice in Gödel's office in order to resolve questions concerning subtleties in the meanings and usage of German and English words." (Dawson 1997:216-217).
Although not a translation of the original paper, a very useful 4th version exists that "cover[s] ground quite similar to that covered by Godel's original 1931 paper on undecidability" (Davis 1952:39), as well as Gödel's own extensions of and commentary on the topic. This appears as On Undecidable Propositions of Formal Mathematical Systems (Davis 1965:39ff) and represents the lectures as transcribed by Stephen Kleene and J. Barkley Rosser while Gödel delivered them at the Institute for Advanced Study in Princeton N.J. in 1934. Two pages of errata and additional corrections by Gödel were added by Davis to this version. This version is also notable because in it Gödel first describes the Herbrand suggestion that gave rise to the (general, i.e. Herbrand-Gödel) form of recursion
Recursion
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
.
External links
- On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Martin Hirzel, November 27, 2000.