Godel's Theorem
Gödel's Theorem, established by mathematician Kurt Gödel, asserts that within any sufficiently complex formal mathematical system, there exist statements that cannot be proven true or false using the rules of that system. This groundbreaking result has profound implications for the foundations of mathematics, revealing inherent limitations in formal systems that aim to encompass all arithmetic truths. Specifically, Gödel's first theorem states that a consistent system cannot be complete; that is, there will always be true statements that remain unprovable within the system. His second theorem further states that the system's own consistency cannot be proven from within its own axioms.
The implications of Gödel's work extend beyond mathematical logic, influencing the fields of computer science and philosophy by highlighting the boundaries of what can be formally determined. The theorem challenges the notion that mathematical truth is synonymous with provability, suggesting a deeper understanding is necessary. Gödel's findings also prompted further discussion and investigation into the nature of computability, leading to significant developments in both mathematical theory and practical applications, such as the design of computers and algorithms. Overall, Gödel's Theorem is regarded as one of the most significant contributions to 20th-century mathematics, reshaping how mathematicians view the structure and limitations of formal systems.
Subject Terms
Godel's Theorem
Type of physical science: Mathematical methods
Field of study: General topics in mathematics
Godel's theorem states that no significant formal system can ever be powerful enough to prove or disprove every statement it can formulate. This result had a profound effect on mathematics, revealing its inherent limitations, and directly influenced subsequent work on understanding logic and computation.

Overview
Any formal mathematical system that is sophisticated enough to contain descriptions of elementary arithmetical propositions and is consistent must contain assertions that can be neither proved nor disproved. This is Godel's first theorem. As a corollary, which is sometimes known as "Godel's second theorem," it can be shown that the statement of the consistency of the system itself, suitably put into arithmetical form, cannot be proved within the system.
A "formal mathematical system" can be regarded as a system of symbols together with a set of rules for their use. For example, the set of arabic numerals, 0, 1, 2, 3,… , together with +, =, and the other symbols, and the rules for obtaining a numeral from combinations of the others, constitute such a system. It is possible to use binary notation, formed from 0 and 1, or any set of individual symbols. A "formula" is any finite sequence or string of symbols, such as "2 + 2 = 4."
A "meaningful formula" is any such string that is "syntactically correct." This essentially means grammatically correct; that is, to be meaningful, a formula must satisfy the notational rules of the formalism, such as "to every left-hand parenthesis there must correspond a right-hand parenthesis." Certain of these meaningful formulas are called "axioms," which can be regarded as a set of statements whose truth is obvious or "self-evident," given the meaning of the symbols from which the statements are formed. So, for example, two of the axioms of arithmetic, expressed informally, are that there is a number 1 and that every number has a successor.
From the axioms, it is possible to obtain other meaningful formulas using the "rules of inference." These can be thought of as (self-evident) instructions that tell how to derive new formulas from those already established. They are similar to the rules of chess, which determine which moves are allowable. Starting from the axioms and using these rules, it is possible to obtain a long list of formulas. Any axiom can be used again in the derivation, as can any formula already obtained. Proceeding in this way enables one to continue to lengthen the list of derived formulas; formulas obtained in this way are called "theorems." In order to "prove" a particular formula, it is necessary to find a list of formulas, constructed using the rules of inference, which terminates with that particular formula. In other words, a proof of a particular formula is a finite sequence of formulas in which each formula in the sequence is either an axiom of the system or a formula obtained from the axioms or preceding formulas using the rules of inference, and the final formula in the sequence is the one to be proved. A formula is said to be "provable" if such a proof of it exists. Thus, the steps of a proof can be thought of as similar to the allowable moves in a game of chess, with the axioms corresponding to the starting position of the game.
According to the "formalist" approach to mathematics, such formulas can be regarded as nothing more than strings of symbols, and a proof involves merely the mechanical manipulation of these symbols according to certain rules. Within this approach, mathematics is treated as merely a matter of form, or a game, like chess. A formula is said to be "true" if it is provable within the system. If the negation of the formula is provable, then the formula itself is false. A system is said to be "consistent" if there is no string of symbols for which both a formula and its negation are provable within the system; otherwise, the formula would be both true and false. Finally, a system is said to be "complete" if it is possible, in principle, to prove any formula or its negation; or, if it is possible to determine the truth or falsity of any formula that can be expressed within the system.
There are, then, two questions that can be asked about mathematics when it is regarded as a formal system: Is it complete? Is it consistent? It is important to realize that these are questions about the system and that their answers will express statements about the system; such statements are referred to as "metamathematical" statements. Again, using the chess example, if "doing mathematics" is like "playing chess," then metamathematical statements are analogous to statements about chess, such as "two knights cannot force a checkmate."
Godel's theorem states that, when asked of arithmetic, the answer to the first question is no. His "second theorem" tackles the second question and asserts that arithmetic cannot be proved to be consistent within the system itself. Furthermore, the argument underlying these results applies to any mathematical system that is rich enough to include arithmetic, which covers most systems of interest. The steps in the demonstration are necessarily detailed and complicated. The central idea, however, not only is beautiful and profound but also is intelligible to the general reader.
The first step is to show that the axioms and rules of inference of a formal system such as arithmetic can themselves be encoded into arithmetical operations. This is done by assigning a unique number to each elementary symbol, each formula (or finite string of symbols), and each proof (or finite sequence of formulas). Such a number serves as a distinct tag or label and is called the "Godel number" of the symbol, formula, or proof. Given any statement within the system, the Godel number that uniquely corresponds to it can be calculated, and, moving in the opposite direction, given any Godel number, the unique statement corresponding to it can be retrieved. In essence, then, this gives a method for "arithmetizing" the system.
The next step is to show that all metamathematical statements about the system can be similarly arithmetized. Since every formula in the system is associated with a Godel number, a metamathematical statement about these formulas and their relations to one another can be regarded as a statement about the corresponding Godel numbers and their arithmetical relations to one another. An analogous example from everyday life is that of the busy post office in which customers are asked to take a ticket with a number on it when they enter. The order of the number determines the order in which the customers will be served, and from a simple inspection of the numbers, it can be seen how many customers have been served, who will be served before whom, and so forth.
Using this method, it is possible to construct an arithmetical formula G that represents the metamathematical statement: "The formula G is not provable in the system," where the formal system considered embraces arithmetic. Notice that G says of itself that it is not provable. This is an adaption of the famous "liar paradox," in which a statement ("This statement is false") asserts its own falsity. In the case of G, "not provable" is substituted for "false," thereby allowing the statement to be expressed in the system.
If G were provable within the system, then according to G itself, it would be false. Only true formulas, however, are provable within the system. Hence, if G is false, it must be unprovable, but if it is unprovable, then G must be true, since this is precisely what is asserts. Therefore, G must be a true formula which has no proof within the system.
If G is true, however, then the negation of G must be false. Since the system is assumed to be consistent, the negation of G is not provable within the system either. Thus, neither G nor its negation is provable. Since G represents a formula that is true but not provable within the system, the system must be incomplete. Furthermore, it is essentially incomplete, since if G were added to the axioms to give a new system, another true but undecidable arithmetical formula could be constructed within the new system. This is the essence of Godel's theorem.
The above argument assumes that the system is consistent. Hence, the conclusion that has been obtained should be read as: "If the system is consistent, then it is incomplete." This statement can itself be encoded in terms of a Godel number and represented by a provable formula within formalized arithmetic. Letting A stand for the formula representing the metamathematical statement "The system is consistent," the above conditional statement can be read as "If A, then G," since if the system is incomplete, there exists a formula that is true but unprovable, which is precisely what G asserts. If A were provable, however, then, since "If A, then G" is provable, G would be provable, too.
Yet, G is not provable, and therefore A cannot be provable either. Therefore, if the system is consistent, then the formula representing the metamathematical statement "The system is consistent" is not provable within the system. In other words, if the system is consistent, then its consistency cannot be established by reasoning that can be represented within the system.
This is Godel's "second theorem."
Applications
Godel's theorem shows, first of all, that the concept of mathematical "truth" must mean something other than the formalists' notion of "provable" within a system, because there exist statements that are known to be true but are not provable. Furthermore, it follows that the notion of a mathematical "proof" cannot be captured in terms of a formalized method based on a fixed set of axioms and rules of inference. The inventiveness of mathematicians in devising new rules cannot be subject to formal limitation or constraint, as the arguments employed in obtaining the theorem themselves demonstrate.
Second, Godel's result shows that the consistency of a system, such as arithmetic, cannot be demonstrated by any metamathematical reasoning that can be represented in terms of the formal system itself. This does not exclude the possibility, however, that a demonstration might be given in other terms. Indeed, proofs of the consistency of arithmetic can be given that involve novel principles of metamathematical reasoning and that extend the class of rules of inference (such proofs cannot be represented arithmetically themselves).
It would therefore be a mistake to view Godel's theorem as wholly negative in character. By showing precisely what could and could not be done within the confines of a formal mathematical system, it provided the impetus needed for mathematicians and logicians to break out of these confines and establish new methods for obtaining their results. In particular, Kurt Godel's work represented an important advance in mathematicians' understanding of what is meant by "computable," a concept that was given a sound mathematical footing for the first time by Alan Mathison Turing.
A third question that can be asked of a formal system is whether it is "decidable," in the sense that there exists a definite method that could, in principle, be applied to any formula to determine whether it is provable or not. Godel's results left open the possibility that there might be some mechanical way of distinguishing the provable formulas from the unprovable ones (such as G). Turing demonstrated that this possibility was also closed; the answer to this third question is "no" as well. To arrive at this result, Turing conceived an ideal machine that simply calculates numbers according to some set of definite rules. Such numbers are said to be "computable." By using Godel's idea of encoding the rules themselves as numbers, Turing was able to show that there will always be some number that is inherently uncomputable. Since such a number effectively represents an unsolvable problem, Turing's result showed that there is no mechanical way of identifying such problems. Perhaps more important, in practical terms, this work not only supplied the first clear and precise definition of "computable" but also, through a consideration of what an ideal calculating machine must be like, set down in abstract terms what it means for a machine to be a "computer." All modern computers are instances of the "universal Turing machine."
By building on this work and generalizing the notion of a computation, a number of important results have been established concerning the relationship between logic and computer programs. Yet another question arises in this context: How complex must a program be to produce a given result? The answer to this question led to the development, by Gregory Chaitin and A. N. Kolmogorov, of the mathematical theory of random strings of symbols. Any string of symbols that is the output of some program can be assigned a number representing its complexity, or information content, where this number is measured by the length of the input plus the length of the program, suitably coded. By extending Godel's theorem, Chaitin showed that, given a consistent set of rules of proof for statements of the form "The complexity of a given output is greater than some number n," there is a number k such that no such statement is provable using these rules for any n greater than k. What this means is that there exists some definite number k such that it is in principle impossible, by the usual methods of mathematics, to prove that any string of symbols has a complexity greater than k. If the "input" is taken to be the axioms of some formal system, then this result, known as the Godel-Chaitin theorem, shows that it is impossible to verify, within the system itself, the complexity of strings of symbols whose complexity exceeds that of the axioms. As Chaitin himself put it: "You can't prove a twenty-pound theorem with a ten-pound theory." Once again, Godel's work has led to the realization that there is a startling and profound limitation on the power of mathematics.
Context
Godel's theorem is generally regarded as the most important single piece of work in the foundations of mathematics in the twentieth century. It arose in the context of a program, set down by the great mathematician David Hilbert and articulated in terms of the formalist approach, which posed the fundamental question of the limitations, in principle, of any formal mathematical system. This question assumed a profound importance with the growing realization, at the beginning of the twentieth century, that pure mathematics was not in the business of developing systems that were true, but was concerned merely with the formal derivation of theorems from certain axioms, whether these were actually true or not.
This realization developed with the study of geometry. During the nineteenth century, geometrical systems other than Euclid's were developed and questions arose, not only regarding which system described the real world, but also regarding the completeness and consistency of the Euclidean system itself. By the end of the nineteenth century, Hilbert managed to find a set of axioms from which all the theorems of the Euclidean system could be produced, without having to appeal to the nature of the physical world. His proof, however, assumed that arithmetic was consistent, and thus a further problem was created--that of demonstrating the consistency of arithmetic.
One approach to this problem had already been developed by Friedrich Ludwig Gottlob Frege, who tried to derive arithmetic from the logical relationships between things in the physical world. This line of attack was continued in more abstract terms by Bertrand Russell, who, with Alfred North Whitehead, published the monumental PRINCIPIA MATHEMATICA (1910), which set out their derivation of mathematics from the axioms of logic. In order to avoid certain paradoxes which lead to inconsistency, however, the theory presented in this work was much more complicated and difficult than the system of arithmetic that it was supposed to justify.
Nevertheless, by introducing a system of notation capable of codifying all the formulas of mathematics and by making explicit the rules of inference used in mathematical proofs, Principia Mathematica came to be regarded as the ideal instrument for investigating the system of arithmetic, which was considered, in formalist terms, as nothing more than a system of symbols, strings of these symbols, and sequences of these strings, manipulated in accordance with the stated rules.
It was with respect to systems such as that of Principia Mathematica that Hilbert posed the three questions of completeness, consistency, and decidability. It was in terms of this system that Godel demonstrated his profound and important results.
Did Godel's work demolish Hilbert's program or did it simply shake it to its foundations? Certainly, it dealt a serious blow to Hilbert's hope that it could be shown that in mathematics there is no such thing as an inherently unsolvable problem. It also revealed the inadequacy of the formalists' identification of mathematical truth with provability, and subsequent work, which shows that reasonably simple Godel-like propositions can be obtained, drives this point home. Nevertheless, the program was continued, albeit in altered form, through the extension of the notion of "proof" to include novel principles and rules not originally envisaged within its framework. These principles have shown themselves to be immensely fruitful in developing a number of significant results, particularly in analysis and set theory.
Thus, Godel's theorem had the effect of both opening up the range of significant problems in mathematics and providing a broader perspective on the problem of determining the limitations of given methods of proof in general.
Principal terms
AXIOMS: statements regarded as basic or "given"
FORMAL MATHEMATICAL SYSTEM: a set of axioms, together with certain rules of inference for deriving formulas from the axioms
FORMULA: a string of formal symbols
MEANINGFUL FORMULA: a string of symbols arranged according to the syntax or grammar of the system; meaningful formulas correspond to statements such as "2 + 2 = 4" or "every integer is the sum of four squares"
PROOF: a list of meaningful formulas in which each one is derived from others in the list by using the rules of inference; the last formula in the list is the one that is "proved"
RULES OF INFERENCE: specific rules that represent the procedure for obtaining one meaningful formula from another
Bibliography
Davis, M. "What Is a Computation?" In MATHEMATICS TODAY: TWELVE INFORMAL ESSAYS, edited by Lynn A. Steen. New York: Vintage Books, 1980. Aimed at the nonspecialist reader, this essay gives a detailed analysis of the notion of a computation. Set in the framework of Turing's work, it explores a number of mathematical investigations concerning unsolvable problems, including the ideas leading to the Godel-Chaitin theorem.
DeLong, Howard. "Unsolved Problems in Arithmetic." SCIENTIFIC AMERICAN 224 (March, 1971): 50-60. In the form of a general survey of inherently unsolvable problems, this article gives an introduction to logic and the notion of a formal mathematical system before presenting Godel's results and certain other unsolvable problems in mathematics.
Hofstadter, Douglas. GODEL, ESCHER, BACH: AN ETERNAL GOLDEN BRAID. New York: Basic Books, 1979. Looping around the fundamental theme of self-reference, this remarkable book takes the reader on an exhilarating trip through the implications of Godel's results for the understanding of the mental processes and the possibility of artificial intelligence in general. The proof of Godel's theorem is explained carefully and wittily, as is the work of Turing and others.
Hopcraft, John E. "Turing Machines." SCIENTIFIC AMERICAN 250 (May, 1984): 86-98. An outline of Turing's work is given in this introductory piece, and the importance for modern computer science is emphasized. Hopcraft also includes a brief discussion of Hilbert's program and modern complexity theory.
Nagel, Ernest, and James R. Newman. GODEL'S PROOF. New York: New York University Press, 1958. An excellent introduction to Godel's theorem and its proof that assumes very little knowledge of mathematics and logic on the part of the reader. The discussion of the nature and importance of consistency proofs is particularly good.
Rucker, Rudy. MIND TOOLS. Boston: Houghton Mifflin, 1987. This is an accessible introduction to mathematics in terms of the concept of "information." Godel's theorem is presented from a number of standpoints, including Chaitin's, and there is a general discussion of Turing machines.
Smullyan, Raymond. FOREVER UNDECIDED: A PUZZLE GUIDE TO GODEL. New York: Alfred A. Knopf, 1987. This volume will appeal to those readers who delight in tackling logical puzzles about liars and truthtellers. Smullyan writes with considerable wit and charm and leads the reader through the intricacies of symbolic logic to the heart of Godel's theorem and beyond, to questions of provability, necessity, and possible worlds.