Discoveries about formal mathematical systems
The two central questions of metalogic are those of the completeness and consistency of a formal system based on axioms. In 1931 Gödel made fundamental discoveries in these areas for the most interesting formal systems. In particular, he discovered that, if such a system is ω-consistent—i.e., devoid of contradiction in a sense to be explained below—then it is not complete and that, if a system is consistent, then the statement of its consistency, easily expressible in the system, is not provable in it.
Soon afterward, in 1934, Gödel modified a suggestion that had been offered by Jacques Herbrand, a French mathematician, and introduced a general concept of recursive functions—i.e., of functions mechanically computable by a finite series of purely combinatorial steps. In 1936 Alonzo Church, a mathematical logician, Alan Mathison Turing, originator of a theory of computability, and Emil L. Post, a specialist in recursive unsolvability, all argued for this concept (and certain equivalent notions), thereby arriving at stable and exact conceptions of “mechanical,” “computable,” “recursive,” and “formal” that explicate the intuitive concept of what a mechanical computing procedure is. As a result of the development of recursion theory, it is now possible to prove not only that certain classes of problems are mechanically solvable (which could be done without the theory) but also that certain others are mechanically unsolvable (or absolutely unsolvable). The most notable example of such unsolvability is the discovery, made in 1970, that there is no algorithm, or rule of repetitive procedure, for determining which Diophantine equations (i.e., polynomial equations of which the coefficients are whole numbers) have integer solutions. This solution gives a negative solution to the 10th problem in the famous list presented by Hilbert at the International Mathematical Congress in 1900.
In this way, logicians have finally arrived at a sharp concept of a formal axiomatic system, because it is no longer necessary to leave “mechanical” as a vague nonmathematical concept. In this way, too, they have arrived at sharp concepts of decidability. In one sense, decidability is a property of sets (of sentences): that of being subject (or not) to mechanical methods by which to decide in a finite number of steps, for any closed sentence of a given formal system (e.g., of N), whether it is true or not or—as a different question—whether it is a theorem or not. In another sense, decidability can refer to a single closed sentence: the sentence is called undecidable in a formal system if neither it nor its negation is a theorem. Using this concept, Gödel’s incompleteness theorem is sometimes stated thus: “Every interesting (or significant) formal system has some undecidable sentences.”
Given these developments, it was easy to extend Gödel’s findings, as Church did in 1936, to show that interesting formal systems such as N are undecidable (both with regard to theorems and with regard to true sentences).
The two incompleteness theorems
The first and most central finding in this field is that systems such as N are incomplete and incompletable because Gödel’s theorem applies to any reasonable and moderately rich system. The proof of this incompleteness may be viewed as a modification of the liar paradox, which shows that truth cannot be defined in the language itself. Since provability in a formal system can often be expressed in the system itself, one is led to the conclusion of incompleteness.
Let us consider the sentence
(2) This sentence is not provable in the system.
In particular, N may be thought of as the system being studied. Representing expressions by numbers and using an ingenious substitution function, Gödel was able to find in the system a sentence p that could be viewed as expressing (2).
Once such a sentence is obtained, some strong conclusions result. If the system is complete, then either the sentence p or its negation is a theorem of the system. If p is a theorem, then intuitively p or (2) is false, and there is in some sense a false theorem in the system. Similarly, if ∼p is a theorem, then it says that ∼(2) or that p is provable in the system. Since ∼p is a theorem, it should be true, and there seem then to be two conflicting sentences that are both true—namely, p is provable in the system and ∼p is provable in it. This can be the case only if the system is inconsistent.
A careful examination of this inexact line of reasoning leads to Gödel’s exact theorem, which says that, if a system is reasonably rich and ω-consistent, then p is undecidable in it. The notion of ω-consistency is stronger than consistency, but it is a very reasonable requirement, since it demands merely that one cannot prove in a system both that some number does not have the property A and yet for each number that it does have the property A—i.e., that (∃ x)∼A(x) and also all of A(0), A(1), . . . are theorems. The American mathematician J. Barkley Rosser, who also contributed to number theory and applied mathematics, weakened the hypothesis to mere consistency in 1936, at the expense of complicating somewhat the initial sentence (2).
More exactly, Gödel showed that, if the system is consistent, then p is not provable; if it is ω-consistent, then ∼p is not provable. The first half leads to Gödel’s theorem on consistency proofs, which says that if a system is consistent, then the arithmetic sentence expressing the consistency of the system cannot be proved in the system. This is usually stated briefly thus: that no interesting system can prove its own consistency or that there exists no consistency proof of a system that can be formalized in the system itself.
The proof of this theorem consists essentially of a formalization in arithmetic of the arithmetized version of the proof of the statement, “If a system is consistent, then p is not provable”; i.e., it consists of a derivation within number theory of p itself from the arithmetic sentence that says that the system is consistent. Hence, if the arithmetic sentence were provable, p would also be provable—contradicting the previous result. This proof, which was only briefly outlined by Gödel, has been carried out in detail by Paul Bernays in his joint work with Hilbert. Moreover, the undecidable sentence p is always of a relatively simple form—namely, the form (∀x)A(x), “For every x, x is A,” in which A is a recursive, in fact a primitive recursive, predicate.