INTRODUCTION

[To Gödel's Theorem]

by

R. B. BRAITHWAITE

Every system of arithmetic contains arithmetical propositions, by which is meant propositions concerned solely with relations between whole numbers, which can neither be proved nor be disproved within the system. This epoch-making discovery by Kurt Gödel, a young Austrian mathematician, was announced by him to the Vienna Academy of Sciences in 1930 and was published, with a detailed proof, in a paper in the Monatshefte für Mathematik und Physik Volume 38 pp. 173-198 (Leipzig: 1931). This paper, entitled "Über formal unentseheidbare Sätze der Principia Mathematica und verwandter Systeme I" ("On formally undecidable propositions of Principia Mathematica and related systems I"), is translated in this book. Gödel intended to write a second part to the paper but this has never been published.

Gödel's Theorem, as a simple corollary of Proposition VI is frequently called, proves that there are arithmetical propositions which are undecidable (i.e. neither provable nor disprovable) within their arithmetical system, and the proof proceeds by actually specifying such a proposition, namely the proposition g expressed by the formula to which "17 Gen r" refers [188]. g is an arithmetical proposition; but the proposition that g is undecidable within the system is not an arithmetical proposition, since it is concerned with provability within an arithmetical system, and this is a metaarithmetical and not an arithmetical notion. Gödel's Theorem is thus a result which belongs not to mathematics but to metamathematics, the name given by Hilbert to the study of rigorous proof in mathematics and symbolic logic.

METAMATHEMATICS. Gödel's paper presupposes some knowledge of the state of metamathematics in 1930, which therefore I shall briefly explain. Following on the work of Frege and Peano, Whitehead and Russell's Principia Mathematica (1910-13) had exhibited the fundamental parts of mathematics, including arithmetic, as a deductive system starting from a limited number of axioms, in which each theorem is shown to follow logically from the axioms and theorems which precede it according to a limited number of rules of inference. And other mathematicians had constructed other deductive systems which included arithmetic (see note 3). In order to show that in a deductive system every theorem follows from the axioms according to the rules of inference it is necessary to consider the formulae which are used to express the axioms and theorems of the system, and to represent the rules of inference by rules (Gödel calls them "mechanical" rules, [173]) according to which from one or more formulae another formula may be obtained by a manipulation of symbols. Such a representation of a deductive system will consist of a sequence of formulae (a calculus) in which the initial formulae express the axioms of the deductive system and each of the other formulae, which express the theorems, are obtained from the initial formulae by a chain of symbolic manipulations. The chain of symbolic manipulations in the calculus corresponds to and represents the chain of deductions in the deductive system.

But this correspondence between calculus and deductive system may be viewed in reverse, and by looking at it the other way round Hilbert originated metamathematics. Here a calculus is constructed, independently of any interpretation of it, as a sequence of formulae which starts with a few initial formulae and in which every other formula is obtained from preceding formulae by symbolic manipulations. The calculus can then be interpreted as representing a deductive system if the initial formulae can be interpreted as expressing the axioms of the system and if the rules of symbolic manipulation can be interpreted as representing the logical rules of inference of the system. If this can be done, a proof that a formula (other than one of the initial formulae) occurs in the sequence of formulae of the calculus yields a proof that the proposition which is the interpretation of this formula is a theorem of the deductive system, i.e. can be deduced from the axioms of the system by the system's rules of inference. Metamathematicians in the 1920's established many important results about deductive systems by converting proofs of what formulae can be obtained by symbolic manipulations within a calculus into proofs of what theorems can be proved within a deductive system which could be represented by the calculus. Frequently consideration of symbolic manipulations provided a "decision procedure" by which whole classes of theorems could actually be proved. Thus Presburger in 1930 published a decision procedure applicable to every proposition of a mutilated system of arithmetic which uses the operation of addition but not that of multiplication; he proved that every one of its propositions is decidable, i.e. either provable or disprovable, within this system.

Gödel's paper established the opposite of this for an arithmetical system which uses multiplication as well as addition–"the theory of ordinary whole numbers" [173]. And this is the piece of mathematics which is oldest in the history of civilization and which is of such practical importance that we make all our children learn a great deal of it at an early age. Gödel was the first to prove any unprovability theorem for arithmetic, and his way of proof was subtler and deeper than the metamathematical methods previously employed. Either of these facts would have ranked this paper high in the development of metamathematics. But it was the fact that it was a proposition of whole-number arithmetic which he showed to be undecidable that created such a scandal.

GÖDEL's FORMAL SYSTEM P. In order rigorously to prove the undecidability of some arithmetical propositions it is necessary to be precise about the exact deductive system of arithmetic which is being considered. As is indicated in the title of his paper, Gödel takes for his arithmetical deductive system that part of the system of Principia Mathematica required to establish the theorems of whole-number arithmetic. Since his proof is metamathematical he is concerned with a calculus representing his arithmetical system: what he proves in Proposition VI is a result about the calculus and not about what the calculus represents, for what it directly establishes is that neither of two particular formulae–the first referred to by "17 Gen r", the second by "Neg (17 Gen r)" [189]–can be obtained from the initial formulae of the calculus by the rules of symbolic manipulation of the calculus. If the calculus is interpreted (as it can be interpreted) so that it represents the arithmetical part of the Principia Mathematica deductive system, with the second formula expressing the contradictory of the arithmetical proposition expressed by the first formula, then the theorem about the deductive system which corresponds to the calculus-theorem states that the proposition g to which "17 Gen r" refers is such that neither it nor its contradictory is provable within the system. Hence within the system g is neither provable nor disprovable. An unprovability theorem for the arithmetical deductive system which Gödel is considering is a simple corollary of Proposition VI about his calculus. Thus the paper is concerned with what formulae can (or, rather, cannot) be obtained within a particular calculus, although of course the calculus would have little general interest if it could not be interpreted as representing a deductive system of whole-number arithmetic.

Gödel's attention solely to his calculus will explain some features of his terminology which may puzzle philosophical logicians. He transfers many epithets which are applied more naturally to deductive systems than to calculi, using them to refer to features of his formal system (his term for what I have called his calculus). He employs formula in the way in which I have used it so that a formula is a "finite series of basic signs", but he goes on to say that "it is easy to state precisely just which series of basic signs are meaningful formulae and which are not" [174]. "Meaningful" is a misnomer, since it is the formal system that is being considered and not an interpretation of it. When he specifies on [177] precisely which series of basic signs are to be well-formed formulae (to use the modern term)–Gödel calls them formulae without a qualifying adjective–he makes no reference to meaning. A formula for him is a series of signs which either is an elementary formula (a concatenation of signs of specified sorts) or is built up out of elementary formulae together with some or all of three specified signs by the use, or repeated use, of three specified rules of construction. When Gödel speaks, in connexion with a formal system, of 'rules of inference', he is referring to the rules according to which one formula can be obtained from other formulae within the formal system. In his system he uses two 'rules of inference', which he specifies by giving one condition for a formula being an 'immediate consequence' of two formulae and one condition for its being an 'immediate consequence' of one formula [178]. A 'proof-schema', for him, is a series of formulae in which each formula (except the initial formulae, which he calls 'axioms') is an 'immediate consequence' of one or of two of the formulae preceding it in the series. A 'proof-schema' is a 'proof' of the last formula in it; and a formula is 'provable' if there is a 'proof' of it. Gödel gives his precise definition of the class of 'provable' formulae in language familiar to mathematicians as "the smallest class of formulae which contains the axioms and is closed with respect to the relation 'immediate consequence of'" [178], i.e. the smallest class which contains the axioms and which contains the 'immediate consequence' of every formula, and of every pair of formulae, contained in the class. For the benefit of philosophical logicians I shall continue the practice followed in this paragraph of putting single quotation marks round terms which without quotation marks refer to features of deductive systems, when I am using them, in Gödel's manner, with reference to a formal system, i.e. to a calculus.

Gödel gives an "exact description" of his formal system P by specifying (1) its basic signs, (2) its formulae (i.e. its well-formed formulae), (3) its 'axioms' (initial formulae), (4) the relation of being an 'immediate consequence' of. He says that P is "essentially the system obtained by superimposing on the Peano axioms [for whole-number arithmetic] the logic of PM [Principia Mathematica]" [176]. Since the Peano axioms are 'provable' (and indeed 'proved') in the calculus of PM, Gödel's system P is virtually that part of the calculus of PM required to lead up to whole-number arithmetic: as Gödel says, "the addition of the Peano axioms, like all the other changes made in the system PM, serves only to simplify the proof and can in principle be dispensed with" (note 16). Gödel states his rules of symbolic construction and manipulation more precisely than do Whitehead and Russell. His only noteworthy divergence from them is that, instead of employing a limited number of 'axioms', he follows the example of von Neumann in using, besides three of Peano's 'axioms', eight 'axiom-schemata' each covering an unlimited number of cases: by doing this he is able to manage with only two 'rules of inference' (see note 24). Gödel specifies the formal system P in the way he does in order to simplify his proof of the undecidability of some of the formulae of P. Since, as he explains, this undecidability is not due to "the special nature of the systems set up, but holds for a very extensive class of formal systems", the exact form he has chosen for P is of no intrinsic importance. What is essential is that P should be an appropriate subject for the exhibition of a method of metamathematical proof which Gödel invented, a method so powerful that it can establish an 'unprovability' result for every formal system capable of representing arithmetic.

THE METHOD OF "ARITHMETIZATION". Gödel's novel metamathematical method is that of attaching numbers to the signs, to the series of signs (formulae) and to the series of series of signs ('proof-schemata') which occur in his formal system. Just as Descartes invented co-ordinate geometry by assigning number-pairs to the points of plane Euclidean geometry, so Gödel invented what might be called co-ordinate metamathematics by assigning numbers to the basic signs, series of basic signs, series of series of basic signs (all of which I shall for convenience lump together under the generic term string) which form an essential part of the subject-matter of metamathematics. Descartes proved geometrical theorems about points by proving algebraic theorems about numbers; Gödel established metamathematical results about the strings of his formal system by considering numbers co-ordinated with the strings. The difference between the co-ordinate systems of co-ordinate geometry and of co-ordinate metamathematics is that the former uses number-pairs for two-dimensional geometry, number-triads for three-dimensional geometry, and so on, and the numbers used are not confined to integers, whereas co-ordinate metamathematics is one-dimensional, using only single numbers, and these (in Gödel's paper) are restricted to being "natural numbers", i.e. 0, 1, 2, 3, etc.

Gödel explains what is now called his "arithmetization" method on [179]. What he does is to provide a co-ordinating rule according to which a different number (which I shall call a Gödel number) is assigned to each string in his formal system. The rule also works in reverse: of every number 0, 1, 2, 3, etc. the rule determines whether the number is the Gödel number of a basic sign, or of a series of basic signs, or of a series of series of basic signs, or is not a Gödel number at all (i.e. there is no string of which it is the Gödel number); and if the number is a Gödel number, the rule specifies uniquely which string it is of which it is the Gödel number. In his account Gödel speaks of his rule as establishing a "one-to-one correspondence". Not all numbers are Gödel numbers: the one-to-one correspondence established by the rule is between the members of a specific sub-class of the class of natural numbers, namely those which are Gödel numbers, and the members of the class of strings, which class is the union (logical sum) of three exclusive classes–the class of basic signs, the class of series of these signs, the class of series of series of these signs. The Gödel number of a series of series of signs is not explicitly mentioned in Gödel's account of his method of arithmetization, but he uses the notion in the definitions (from 22 onwards) which form an essential preliminary to the proof of his Theorem. This Gödel number is the number constructed out of the Gödel numbers of the elements of the series of series of signs in exactly the same way as the Gödel number of a series of signs is constructed out of the Gödel numbers of the signs which are the elements of this series of signs [179]. Thus the Gödel number of a series of k elements, whether these elements are signs or are series of signs, is constructed out of the elements' Gödel numbers n1, n2, … nk as the number 2n1, 3n2pknk, a product whose prime factors are the first k prime numbers (1 not being counted as a prime number) with the 1st, 2nd, … k-th prime number occurring respectively n1, n2, … nk times in the product. The one-to-one correspondence between Gödel numbers defined in this way and the strings of which they are Gödel numbers is a consequence of the "fundamental theorem of arithmetic", namely that every natural number greater than 1 which is not itself a prime has a unique resolution into prime factors.

Gödel's rule of arithmetization ensures that to every class of strings there corresponds a unique class of Gödel numbers, and vice versa. And that to any relation R between strings there corresponds a unique relation R' between Gödel numbers, and vice versa: i.e. the n-adic relation R' holds between n Gödel numbers if and only if the n-adic relation R holds between the n strings. For example, the metamathematical statement that the series s of formulae is a 'proof' of the formula f is true if and only if a certain arithmetical relation holds between the Gödel numbers of s and of f which corresponds to the relation: being a 'proof' of. Gödel uses the same language to refer to the arithmetical properties of, and relation between, Gödel numbers as he uses to refer to the corresponding properties of, and relations between, strings (see note 9), printing the terms in italics when they refer to arithmetical concepts applicable to Gödel numbers [179]. In a sequence of definitions 6-46 he defines, step by step, a sequence of arithmetical concepts which correspond, according to his rule of arithmetization, to the metamathematical concepts expressed by the same words. [Definitions 1-5 define the ancillary arithmetical concepts (being the n-th prime number, etc.) used in his method of arithmetization.] As examples, definition 8 defines the arithmetical operation * upon two numbers x and y in such a way that the number x * y which is the result of performing this operation is the Gödel number of the string obtained by taking the string whose Gödel number is x and placing the string whose Gödel number is y immediately after it. And definition 45 defines the arithmetical relation B between x and y so that the proposition x B y is the same as the conjunction of the proposition that x is the Gödel number of a series of series of signs forming a 'proof-schema' with the proposition that the series of signs whose Gödel number is y is the last series of signs in this 'proof-schema', i.e. this 'proof-schema' is a 'proof' of the last formula in it. For the sake of clarity I shall not follow Gödel's abbreviating practice of using italicized words and phrases to refer to arithmetical concepts applicable to Gödel numbers, and shall use italics only in the ordinary way for emphasis. For example, while Gödel paraphrases the x B y of definition 45 as: x is a proof of the formula y, I paraphrase it as: x is the Gödel number of a 'proof' of the formula whose Gödel number is y.

The interpreted symbolism used in these definitions, as in all Gödel's metamathematical statements (see note 29), is that of Hilbert and Ackermann's Grundzüge der theoretischen Logik (1928: English translation, 1950). The only deviations from the symbolism of Principia Mathematica are: "~p" to stand for Not p, "p & q" for Both p and q, "p ® q" for Not both p and Not q (the "p É q" of PM), "p ~ q" for either both p and q or both Not p and Not q (the "p º q" of PM), and "(Ex)" as the existential quantifier in place of the "(\$x)" of PM. Gödel uses "º" as an abbreviation for "means the same as" in his definitions.

Except for these purely logical concepts, all the concepts involved in Gödel's definitions 1-46, and also those in (5), (6), (6.1), (8.1), are arithmetical concepts (properties, relations, operations) which apply to natural numbers, i.e. the substitution values for the variables "x", "y", "z", "n", etc. occurring in the definitions are "0", "1", "2", … And the logical concepts are restricted so that they apply to only a finite number of entities. Whenever a universal or existential quantifier occurs in any of the definitions 1-45, a clause is inserted within the quantification which ensures that the quantification is only over a finite number of values. For example, the first definition defines "x is divisible by y" as There is a z less than or equal to x which is such that x = y.z, the phrase which I have italicized being inserted so as to restrict the quantification to numbers not greater than x. This makes the definiens equivalent to: x = y.O or x = y.l or … or x = y.x, a truth-function of a finite number (x+1) of equalities. This restriction upon the quantifiers (except in definition 46) secures that all the arithmetical concepts employed (except Bew) are recursive in a sense of this word which Gödel defines and discusses in an excursus from his main argument.

RECURSIVENESS. The notion of recursiveness has played a central part in metamathematics since Gödel's work on it, but little more will be said about it here than is necessary for an understanding of Gödel's proof of his Theorem.

The method of recursive definition is an extension of the method of definition by "mathematical induction" by which the natural numbers are, step by step, defined. Starting with 0, 1 is defined as the immediate successor of 0, 2 as the immediate successor of 1, and so on. A recursive definition (a "primitive recursive definition", as it is now called) is the specification of each number in a sequence of numbers by means of a specification of the first number and of a rule which specifies the (k+1)-th number in terms of the k-th number and of k itself. [This is a paraphrase of Gödel's definition of a recursively defined arithmetical function, where this function is of only one numerical variable: see eq. (2).] An arithmetical function is recursive if it is the last term in a finite sequence of functions in which each function is recursively defined by a rule involving two functions preceding it in the sequence (or is the successor function or a constant or obtained by substitution from a preceding function); and the recursiveness of other arithmetical concepts is defined by means of the notion of recursive function. The essential feature of a recursive concept–a dyadic relation R, for example–is that whether or not R holds between m and n, i.e. whether R(m,n) is true or false, can be decided by a step-by-step procedure working upwards from R(0,0) with the use of a limited number of recursive definitions.

The importance of recursiveness for metamathematics in general lies in the fact that recursive definition enables every number in a recursively defined infinite sequence to be constructed according to a rule, so that a remark about the infinite sequence can be construed as a remark about the rule of construction and not as a remark about a given infinite totality. For this reason the use of only such mathematical concepts as are recursive is favoured by mathematical thinkers of both the finitist and intuitionist schools of metamathematics, and is accepted (although with extensions made by Gödel and others to the notion of recursiveness in this paper) by present-day constructivists who decline to talk about any mathematical entities that cannot be recursively constructed.

For the proof of Gödel's 'Unprovability' Theorem the importance of recursiveness lies in the fact (Proposition V) that every statement of a recursive relationship holding between given numbers x1, x2, … xn is expressible by a formula f of the formal system P which is 'provable' within P if the statement is true and 'disprovable' within P (i.e. the 'negation' of f, written as Neg f, is 'provable' within P) if the statement is false. Gödel only outlines a proof of this proposition, since it "offers no difficulties of principle and is somewhat involved" [186]; so I will expand what he says in his footnote (note 39). Since the relation R in question is recursive, then if R(x1,x2, … xn) is true, R(x1,x2, … xn) can be proved in a deductive system for arithmetic by constructing a finite sequence of propositions starting with the axioms and ending with R(x1,x2, … xn); and if R(x1,x2, … xn) is false, Not R(x1,x2, … xn) can similarly be proved. The calculus or formal system P was designed by Gödel to represent this deductive system; so the finite sequence of propositions which constitutes a proof of R(x1,x2, … xn) or of Not R(x1,x2, … xn) will be expressed in P by a finite series of formulae ending in a formula f in the one case and in the formula Neg f in the other. To express in P the step-by-step definitional procedure by which the truth or falsity of the recursive relationship is established is to construct either a 'proof' of f or a 'proof' of Neg f: f or Neg f will only appear in the formal system accompanied by a 'proof-schema' of which it is the last formula. So if R(x1,x2, … xn) is true, there is a 'proof' of f, and f is a 'provable' formula (definition 46); and if R(x1,x2, … xn) is false, Neg f is a 'provable' formula within the system P.

Define a class-sign as a series of signs which is a formula and which contains exactly one free variable (which may occur at several places in the formula) [177]. [In Gödel's system P there is no distinction between a class-sign and a property-sign, since 'axiom-schema' V may be regarded as expressing the axioms that two properties (of the same type) which always go together are identical–"axioms of extensionality".] A class-sign is recursive if it can be interpreted as expressing a recursive arithmetical class, in which case the formula resulting from the substitution for its variable of a number-sign will be 'provable' or 'disprovable' according as the number represented by the number-sign in the interpretation of the system is or is not a member of this recursive class. A recursive relation-sign is defined similarly ([177]: see also note 28). Note that neither a class-sign nor a relation-sign is a basic sign, since the former contains one and the latter several free variables.

THE UNPROVABILITY THEOREM FOR P. "We now come", as Gödel says, "to the object of our exercises"–the proof of the 'Unprovability' Theorem. To prove this he establishes Proposition VI which is more general than is necessary for proving that there are undecidable formulae in the formal system P, since it is concerned not only with 'proofs' within P but also with 'deductions' within P from formulae not included among the 'axioms' of P, i.e. with 'proofs' within a formal system P' obtained from P by adding these formulae as additional 'axioms'. Gödel requires this subtlety later on in his paper; but it complicates the proof of Proposition VI, which I shall discuss in the simplified form in which the class c of added formulae is the null class (i.e. no formulae are added to the axioms), so that a 'c-provable' formula within P [189] is the same as a 'provable' formula within P, and the argument is concerned solely with 'proofs' within P. Gödel's Bc is thus taken as equivalent to his relation B, and Bewc as equivalent to his property Bew.

Proposition VI simplified in this way may be stated as follows: If the formal system P satisfies a certain condition of 'consistency', then there is at least one recursive class-sign r in P such that neither v Gen r nor Neg (v Gen r) is 'provable' within P, where v Gen r is the generalization of r with respect to its free variable v.

The undecidability of v Gen r within P depends upon P's satisfying a certain 'consistency' condition. Since this condition is only relevant to the last stage of the proof, and itself raises important questions, consideration of 'consistency' will be deferred until the main part of the proof has been discussed.

This main part is given from (8.1) to (16). Gödel states his argument in terms of Gödel numbers and of relations between Gödel numbers; and when the expressions relation-sign, free variable, class-sign, provable are used they are italicized to show that they refer to arithmetical concepts applicable to Gödel numbers. Because of the correspondence between these concepts as applied to Gödel numbers and metamathematical concepts as applied to the strings which have these Gödel numbers, Gödel's whole argument applies equally well if his symbols are interpreted as strings and the terms relation-sign, free variable, etc. are taken in their usual sense. Since Gödel's argument, though couched in terms of numbers, is a metamathematical argument, it may be convenient for philosophical logicians if I give it wholly in metamathematical terms. This will have the additional advantage that interpretations of the formulae can be inserted parenthetically at appropriate places, on the assumption that the calculus (Gödel's formal system P) is to be interpreted as representing a deductive system which includes propositional and first-order predicate logic–though, strictly speaking, any actual interpretation is irrelevant to the argument.

However, a recasting of Gödel's argument in metamathematical terms makes one unimportant modification necessary. For the part of his argument which establishes the 'unprovability' of Neg (v Gen r) requires at one point considering a statement about all numbers, whether or not they are Gödel numbers; and this statement cannot be construed without change as a statement about all strings, since a number which is not a Gödel number does not correspond to any string. But it is easy to close the gap in the recasting by considering the numbers which are Gödel numbers as arranged in a sequence of increasing magnitude, and then using, instead of a Gödel number itself, the number which gives the place of this Gödel number in the sequence. To be precise, if n is the (m+1)-th Gödel number in increasing order, call m the G-number of the string of which n is the Gödel number, and use the G-number m wherever Godel in his argument uses the Gödel number n. Then every natural number 0, 1, 2, etc. will be the G-number of some string; and there will be a recursive one-to-one correspondence between natural numbers and strings. So arithmetical statements about all numbers can be construed as metamathematical statements about all strings. Of course Gödel's sequence of definitions 6-46 defines arithmetical concepts which correspond to metamathematical concepts according to the Gödel-number method of arithmetization. But the purpose of his definitions is to establish that all the arithmetical concepts concerned (except Bew) are recursive and so are also all the corresponding metamathematical concepts. Consequently any proposition about them is expressible in P by a formula which is 'provable' or 'disprovable' according as the proposition is true or false. Having proved this (by Proposition V) Gödel makes no further use in his argument for the 'Unprovability' Theorem of his particular method of arithmetization. All that is necessary is that there should be a unique number assigned to every string. So no harm will result from continuing the argument using G-numbers instead of the corresponding Gödel numbers; and this use of G-numbers I shall call the "modified arithmetization".

To facilitate comparison with Gödel's text, I shall use Gödel's symbols, except that, as well as single small italic letters denoting numbers, I shall in future use the same letters in bold type to stand for the strings of which these numbers are G-numbers. Thus x will be the string whose G-number is x. Gödel writes Z(x) for the Gödel number of the number-sign for the number x in his formal system P (see definition 17). This number-sign is "0" preceded by x "¦" s; e.g. the number-sign for 3 is "¦¦¦0" (see [177]). I shall call these number-signs numerals; and shall write Gx (or, if x is a complex expression, G[x]) for the numeral for the G-number of x and call Gx the G-numeral of x. Since every number is a G-number, every numeral is a G-numeral; and there is a recursive one-to-one correspondence between the members of the class of numerals "0", "¦0", "¦¦0", etc. and the members of the class of strings (which, of course, includes the class of numerals as a sub-class).

A class-sign will be written in the form a(v) and a dyadic relation-sign in the form b(v,w) with v or v, w, the free variables (of first type) concerned, mentioned explicitly. [But the G-numerals of a(v) and of b(v,w) will be abbreviated to Ga and to Gb.] Since we are concerned with the formal system P whose "individuals" are natural numbers [176] the substitution values for v and w will always be numerals, and thus always G-numerals. The result of substituting Gx for v and Gy for w in b(v,w) will be written as b(Gx,Gy). [Gödel uses a typographically less convenient notation for substitution. In comparing my version with his text it should be remembered that 17 is the Gödel number of v and 19 that of w.]

The simplified Proposition VI may now be restated as: If the formal system P satisfies a certain condition of 'consistency', then there is at least one recursive class-sign r(v) in P such that neither v Gen r(v) nor Neg [v Gen r(v)] is 'provable' within P.

We can now follow the principal steps in the argument from (8.1) onwards.

Define Q'(x,y(u)) as Not [x B y(Gy)], i.e. x is not a 'proof' of the formula obtained by substituting for the variable in the class-sign y(u) the G-numeral Gy for the class-sign itself.

Let Q(x,y) be the relationship between the G-numbers of x and of y which is equivalent to Q'(x, y(u)) by the modified arithmetization. Q(x,y) is recursive; and so it follows from Proposition V that there is a recursive relation-sign q(v,w) which is such that

Q(x,y) ® [q(Gx,Gy)] is 'provable';
Not Q(x,y) ® [Neg q(Gx,Gy)] is 'provable'.

But Q'(x,y(u)) is equivalent to Q(x,y); and thus

Q'(x,y(u)) ® [q(Gx,Gy)] is 'provable';
Not Q'(x,y(u)) ® [Neg q(Gx,Gy)] is 'provable'.

The relation-sign q(v,w) may therefore be regarded as a formula expressing the relation which x has to y(u) when x is not a 'proof' of y(Gy).

Consider the 'generalization' of the relation-sign q(v,w) with respect to the free variable v, yielding the formula v Gen q(v,w). This has one free variable, namely w, and so is a class-sign. Call it p(w). It may be regarded as denoting the class of which a class-sign y(u) is a member if and only if everything is not a 'proof' of y(Gy), i.e. if and only if y(Gy) is 'unprovable'.

Next consider the substitution in the same relation-sign q(v,w) of Gp for the free variable w, yielding the formula q(v,Gp). This also has one free variable, v, and so is also a class-sign. Call it r(v). It may be regarded as denoting the class of strings which are not 'proofs' of p(Gp). Since it may also be regarded, according to the modified arithmetization, as denoting the class of the G-numbers of these strings, which is a recursive arithmetical class, r(v) is a recursive class-sign.

Now consider the 'generalization' of this class-sign r(v) i.e. of q(v,Gp), with respect to its free variable v, which yields the formula v Gen r(v). This has no free variable, and may be regarded as expressing the proposition that everything is not a 'proof' of p(Gp), i.e. that p(Gp) is 'unprovable'.

But, and here is the crux of the argument, v Gen r(v) is the same as p(Gp). For we arrived at the former by first substituting Gp for w in q(v,w), which yielded r(v), and then 'generalizing' with respect to v, which yielded v Gen r(v). But, since the substitution and the 'generalization' had reference to different free variables, the two operations yield the same final result if performed in the reverse order, i.e. by first 'generalizing' q(v,w) with respect to v, which yields p(w), and then substituting Gp for w in p(w), which yields p(Gp). If either of the formulae v Gen r(v) or p(Gp) be expanded to get rid of the abbreviations r and p, we get one and the same formula

v Gen q(v,G[v Gen q(v,w)]).

This formula, and of course each of the abbreviations of it, may be regarded as expressing the proposition that the formula itself is 'unprovable', i.e. the formula expresses its own 'unprovability'.

The formula of Gödel's which I have sometimes quoted, namely "17 Gen r", is the modified arithmetization of my metamathematical "v Gen r(v)", but with 17, the Godel number of my variable v, used instead of the G-number of v. Since it is immaterial in which way the metamathematical formula is written, I shall in the next few pages use the shortest form, namely p(Gp).

Now for the last stages of the proof. We go back to Q'(x,y(u)), defined as Not [x B y(Gy)], i.e. as expressing the metamathematical proposition that x is not a 'proof' of y(Gy). If we take the class-sign y(u) to be p(u), which is the same as p(w), since u and w are variables, we get for the consequences of the truth or falsity of Q'(x, p(u)), i.e. of the truth or falsity of Not [x B p(Gp)]:

Not [x B p(Gp)] ® [q(Gx,Gp)] is 'provable';
x B p(Gp) ® [Neg q (Gx, Gp)] is 'provable'.

q(Gx,Gp) is the same as r(Gx) (which corresponds to Gödel's expression in square brackets on the right-hand side of (15)).

Suppose now that p(Gp) were to be 'provable'. Then there would be a 'proof-schema' n such that n B p(Gp), and hence such that Neg q(Gn,Gp) i.e. Neg r(Gn) would be 'provable'. But if p(Gp), i.e. v Gen r(v), were 'provable', so also would be r(Gn). So from the supposition that p(Gp) is 'provable', there follows that both r(Gn) and Neg r(Gn) are 'provable'. Call a formal system (a calculus) 'consistent' if it contains no pair of 'provable' formulae of the forms f, Neg f. Then, if p(Gp) is 'provable', the formal system P is 'inconsistent'; so, if P is 'consistent', p(Gp) is 'unprovable' within P.

Suppose that P is 'consistent' and that Neg p(Gp) were to be 'provable'. Since p(Gp) is 'unprovable', Not [n B p(Gp)] holds for every string n. Thus q(Gn,Gp), i.e. r(Gn), is 'provable' for every string n; and hence r(m) is 'provable' for every numeral m. But Neg p(Gp) is the same as Neg [v Gen r(v)]; and, if this were to be 'provable', the curious situation would arise of every substitution-instance r(m) of the class-sign r(v) being 'provable' while the 'generalization' of r(v) with respect to v was 'disprovable'. This situation is, however, compatible with the 'consistency' of P: in order to prohibit its occurrence a stronger form of consistency, called by Gödel 'w-consistency', must be assumed to hold of P. [A formal system is 'w-consistent' if it contains no class-sign a(u) which is such both that a(m) is 'provable' within the system for every numeral m and that Neg [u Gen a(u)] is 'provable' within the system [187].] Since the 'consistency' (sometimes called 'simple consistency') of P is a consequence of its 'w-consistency', the conjunction of 'w-consistency' with the 'provability' of Neg p(Gp) yields a contradiction; so, if the formal system P is 'w-consistent', Neg p(Gp) is 'unprovable' within P.

Combining these two results tells us that, if P is 'w-consistent', neither p(Gp) nor Neg p(Gp) is 'provable' within P, i.e. p(Gp) is undecidable within P.

In order to compare this with my simplified restatement of Gödel's Proposition VI we must remember that p(Gp) is the same as v Gen r(v). r(v) is a recursive class-sign; so there is a recursive class-sign r(v) in P such that neither v Gen r(v) nor Neg [v Gen r(v)] is 'provable' within P, if P is 'w-consistent'.

'CONSISTENCY'. If a formal system (a calculus) is 'inconsistent', it will contain both a 'provable' formula f and a 'provable' formula Neg f. If its 'axioms' and 'rules of inference' are such that the 'inconsistent' calculus can be interpreted, with Neg interpreted as meaning Not and a 'provable' formula interpreted as standing for a provable proposition, so that the deductive system which it represents includes a deductive sub-system of propositional logic (as is the case with Gödel's calculus P), then this deductive system will have as theorems both a proposition p (namely, the proposition represented by f) and its contradictory Not p (the proposition represented by Neg f), and hence the conjunction p & Not pa self-contradiction. The deductive system will thus be inconsistent in the usual sense of the term, which, of course, is why Gödel uses the same word to apply to a calculus and I use the same word within single quotation marks.

Since p É (p Ú q), which is equivalent to (p & Not p) É q, is either an axiom or a theorem in propositional logic (the formula representing it in Gödel's P falls under 'axiom-schema' II.2), and since modus ponens (q is an immediate consequence of p and p É q) is a rule of inference in propositional logic (Gödel's P uses the corresponding 'rule': see [178]), every proposition is a consequence of a self-contradiction. An inconsistent deductive system which includes a sub-system of propositional logic will therefore contain every proposition whatever as a theorem of the system. So if a calculus can be interpreted as representing a deductive system with the very small number of features required for it to include propositional logic, and if the calculus is 'inconsistent', every (well-formed) formula in the calculus will be 'provable' within the calculus. Such a calculus will be of no interest, since there will be no division of its formulae into those which are 'provable' and those which are not. This is the principal reason why metamathematicians attach such importance to a calculus being 'consistent', altogether apart from whether or not the calculus is in fact interpreted to represent a deductive system.

If the calculus P were 'inconsistent', all its formulae would be 'provable' and so the condition for 'w-consistency' could not be satisfied. So if P is 'w-consistent', it is also 'consistent'. The notion of 'w-consistency' is intimately connected with finitist methods of proof. It will not be further considered here, since it is not a necessary condition in an 'Unprovability' Theorem for Gödel's formal system P. In 1936 Rosser, by an argument involving a recursive class-sign more complicated than Gödel's r(v), established an 'Unprovability' Theorem for P (and for systems of similar character) which required as a condition only that P is 'consistent'.

A principal aim of Hilbert and his school had been to establish the 'consistency' of a calculus capable of being interpreted as expressing arithmetic, and thus to prove the consistency of a deductive system of arithmetic. To them the second great theorem contained in this paper was even more of a shock than the 'Unprovability' Theorem. For this second theorem proves the undecidability within P of a formula expressing the 'consistency' of P, thus showing that the 'consistency' of P, if P is 'consistent', cannot be established by a 'proof' within P, i.e. a 'proof' starting with only the 'axioms' of P and using only P's 'rules of inference'. [If P is 'inconsistent', of course both P's 'consistency' and P's 'inconsistency' can be 'proved' within P.]

THE 'UNPROVABILITY'-OF-'CONSISTENCY' THEOREM FOR P. Gödel proves this theorem (his Proposition XI) in a general form, corresponding to that of his Proposition VI, which is concerned with 'deductions' as well as 'proofs' within P. As with Proposition VI I shall discuss Proposition XI in a simplified form in which it is concerned solely with 'proofs' within P. The simplified form is obtained by taking the class c to be the null class, and consequently Bc and Bewc as equivalent to B and to Bew respectively.

Proposition XI simplified in this way may be stated as follows: If the formal system P is 'consistent', its 'consistency' is 'unprovable' within P.

In order to prove this theorem Gödel uses the result established towards the end of the proof of his 'Unprovability' Theorem, namely that, if P is 'consistent', the formula p(Gp) is 'unprovable'. Since, as we have seen, this formula may be regarded as expressing its own 'unprovability', the metamathematical proposition

P is 'consistent' ® p(Gp) is 'unprovable'

may be expressed within P by the formula, 'provable' within P,

w Imp p(Gp),

where w (this symbol no longer being used as a variable) is a recursive formula expressing in P the 'consistency' of P, and u Imp v expresses in P the propositional schema Not a or b (see definition 32). Then it follows from the definition of 'immediate consequence' (definition 43) that, if w were to be 'provable', p(Gp) would also be 'provable'. But if P is 'consistent', p(Gp) is 'unprovable', and so also is w. Thus a formula w expressing the 'consistency' of P is 'unprovable' within P–on the assumption, of course, that P is 'consistent'.

In this paper Gödel only professed to "sketch in outline" the proof of his Proposition XI, and the sequel in which he intended to present it "in detail" he never published. Indeed the part of the detailed proof which establishes that w Imp p(Gp) is 'provable' within P requires exhibiting a 'proof' within P of w Imp p(Gp), and this is a lengthy and complicated business. However there is prima facie a gap in Godel's "sketch" of the proof, namely how a recursive formula w which expresses the 'consistency' of P can be constructed in P; but this gap can easily be closed by an argument which I owe to Rosser. Let t be a particular formula which is 'provable' in P; e.g. one of the 'axioms' of P. If Neg t is also 'provable', P is 'inconsistent'. But, if P is 'inconsistent', every (well-formed) formula is 'provable' in P, and so Neg t is 'provable'. Thus the 'inconsistency' of P is logically equivalent to the 'provability' of Neg t, and the 'consistency' of P to the 'unprovability' of Neg t. So all that is required is a recursive formula in P expressing the 'unprovability' of Neg t, which is easy to provide. x B y (x is a 'proof' of the formula y) is a recursive relation-sign (definition 45) with x and y as its free variables; hence Neg (x B Neg t) is a recursive class-sign, with x as its free variable, and x Gen [Neg (x B Neg t)] is a recursive formula which expresses in P the 'unprovability' of Neg t, which is equivalent to the 'consistency' of P. So the w of the proof in the last paragraph may be taken to be x Gen [Neg (x B Neg t)], in which case the proof (when given in detail) will fully satisfy the requirements of finitists and constructivists.

Gödel says at the end of his paper that his 'Unprovability'-of-'Consistency' Theorem represents "no contradiction of the formalistic standpoint of Hilbert. For this standpoint presupposes only the existence of a consistency proof effected which cannot be stated in P" (see [197]). This was a pious hope of Gödel's, made reasonable when he uttered it by the lack of precision in Hilbert's notion of a proof "effected by finite means". Clarification of this notion, to which this paper and later work of Gödel notably contributed, have explicated it in terms of the concept of recursiveness and of extensions of this concept; and it is now certain that, within any formal system using only such concepts and capable of expressing arithmetic, it is impossible to establish its own 'consistency' (if it is 'consistent'). In 1936 Gentzen was able to prove the 'consistency' of such a formal system, but only by using non-constructive methods of proof ("transfinite induction") which fall outside the constructive 'rules of inference' of the system. Gödel, in this paper which established his two great theorems by methods which are constructive in a precise sense, on the one hand showed the essential limitations imposed upon constructivist formal systems (which include all systems basing a calculus for arithmetic upon "mathematical induction"), and on the other hand displayed the power of constructivist methods for establishing metamathematical truths. To a philosophical logician it appears an even more remarkable feat to have been able to establish the internal undecidability of some arithmetical formulae than to provide (as Hilbert's school would have wished) a decision procedure for the whole of arithmetic.

THE SYNTACTICAL CHARACTER OF GÖDEL'S THEOREMS. In concluding this Introduction I wish to elaborate a point I have made several times in passing, namely that Gödel's two great theorems are metamathematical theorems about a calculus (his formal system P) and are not, in themselves, metamathematical theorems about a deductive system which is an interpretation of the calculus. However, theorems about deductive systems are immediate corollaries. The statement that there are arithmetical propositions which are neither provable nor disprovable within their arithmetical system (which at the beginning of this Introduction I called Gödel's Theorem tout court) is, for the deductive system for arithmetic represented by the calculus P, a corollary of the 'Unprovability' Theorem for P.

To appreciate this, consider the formula v Gen r(v) whose undecidability (subject, of course, to P being 'w-consistent') was established by the proof of the 'Unprovability' Theorem. Interpret the class-sign r(v) as denoting the class of G-numbers of the strings which are not 'proofs' of p(Gp)–the second interpretation of r(v) mentioned. This class of numbers, specified thus metamathematically, may also be specified arithmetically by modifying the arithmetization of series of formulae, formula, proof provided by definitions 1-45. So if 'generalizing' r(v) with respect to v is interpreted as stating that the class of numbers denoted by r(v) is the universal class, the formula v Gen r(v) will be interpreted as expressing the proposition that every number is a member of a certain arithmetically specified class–a straight arithmetical proposition (call it g). If the calculus P (assumed to be 'w-consistent') is interpreted as representing a deductive system S for arithmetic (and it was devised so that it could represent that part of the Principia Mathematica deductive system required for arithmetic), with the 'axioms' and 'rules of inference' of P representing the axioms and rules of inference of S (and such an interpretation permits the interpretation of v Gen r(v) as expressing the arithmetical proposition g), then g will be neither provable nor disprovable by the methods of proof available in S, i.e. neither g nor Not g will be a theorem of S. [In Section 3 of this paper Gödel uses arithmetical in a more restricted sense than I have used it, and establishes that, even in this restricted sense, there will be arithmetical propositions undecidable in S.] The undecidability (the 'unprovability' and 'undisprovability') of v Gen r(v) within P is transferred to the deductive system S represented by P to yield the undecidability (the unprovability and undisprovability) of g within S. Similarly the 'unprovability' within P of the 'consistency' of P (assumed to be 'consistent') transfers to S to yield the unprovability within S of the consistency of S.

The undecidability of some arithmetical propositions within the deductive system S may be classed among the syntactical metamathematical characteristics of the system S (represented by the calculus P), for the reason that this undecidability derives from the undecidability of some formulae within the calculus P which represents S. Deductive systems, unlike calculi, have also semantical metamathematical characteristics; in particular their propositions have or lack the semantical property of being true–what Gödel in his introductory Section I calls being "correct as regards content" (inhaltlich richtig). Connecting the syntactical property of being provable with the semantical property of being true by taking every proposition provable within S (i.e. every axiom and theorem of S) to be true (see [176]) gives an additional kick to the undecidability in S of g–by adding that g is true. For the correlation of arithmetical and metamathematical propositions effected by the modified arithmetization ensures that g will be true if and only if v Gen v(r) is 'unprovable' within P, i.e. if and only if g is unprovable within S. Hence if g were not true, g would be provable within S and so true–a contradiction. Consequently if the axioms and theorems of the deductive-system-for-arithmetic S are true (and this implies the consistency of S, for otherwise two propositions p and Not p, which cannot both be true, would both be theorems of S), then there is an arithmetical proposition, namely g, which is not provable within S (a syntactical characteristic) but which nevertheless is true (a semantical characteristic). This metamathematical argument which, combines semantical with syntactical considerations, establishes the truth of an arithmetical proposition which cannot be proved within S.

In his introductory Section 1 Gödel intermingles semantical with syntactical considerations in sketching a proof of the undecidability of g (which is the reason why I have seldom referred to this section in this Introduction). The distinction between what is syntactical and what semantical was not made explicitly until a year or two later (by Tarski, whose work included rigorously establishing unprovability theorems that were semantical); but it is implicit in Gödel's remark towards the end of Section I that "the exact statement of the proof [of the undecidability of g], which now follows, will have among others the task of substituting for the second of these assumptions [that every provable formula is also correct as regards content] a purely formal and much weaker one" [176]. Gödel's proof in Section 2 is a purely syntactical proof about a calculus (the formal system P) whose interpretation as a deductive system for arithmetic is, strictly speaking, irrelevant to his argument. It is true that Gödel explains arithmetization as a way of co-ordinating strings in his calculus with natural numbers, and he discusses recursive functions in terms of natural numbers (and I have followed him in speaking of numbers in both these contexts). But whenever he talks about numbers, and thus makes a remark which is prima facie about a deductive system rather than about a calculus, the remark is always a syntactical remark about the deductive system, and is therefore in essence a remark about the calculus which represents the system. For example, when Gödel says at the beginning of Section 2 that his formal system P has "numbers as individuals", and speaks of "variables of first type (for individuals, i.e. natural numbers including 0)" [176], all that is relevant to his argument is that numerals are the only substitution values (not containing variables) permitted for his variables of first type. This is shown most clearly when Gödel specifies the substitution operation in connexion with his 'axiom-schema' III.1, which requires the substitution for a variable of first type of a sign of first type, which he has previously explained as being "a combination of signs of the form: a, ¦a, ¦¦a, ¦¦¦a, etc., where a is either "0" [in which case the sign is a number-sign] or a variable of first type" ([176]; in Gödel's text 0 occurs instead of "0", but this would seem to be a misprint).

Gödel's 'arithmetization' of metamathematical concepts (as also my 'modified arithmetization') is in fact effected by correlating to each string x another string which is a numeral: there is no need to pass from a string x to this numeral by the indirect route of first moving to the Gödel number (or G-number) of x and then passing from this number to the numeral which expresses it in the calculus P. In the argument the equivalence, for example, between the metamathematical proposition about P stating that the string (the series of formulae) n is a 'proof' of the string (the formula) y and an arithmetical relationship between the G-numbers n and y of these strings may equally well be construed as an equivalence between the metamathematical proposition and the occurrence as a 'theorem' of P (i.e. as a 'provable' formula within P) of an appropriate 'recursive' 'arithmetical' formula f containing the strings (the numerals) Gn and Gy. [The requirement that f should be 'recursive' ensures that, if f is not a 'theorem' of P, Neg f is.] The peculiarity of the 'recursive' class-sign r(v) of the 'Unprovability' Theorem is that, if there were to be a string n which was a 'proof' of v Gen r(v), the 'recursive' 'arithmetical' formula Neg r(Gn) would occur as a 'theorem' of P, whereas r(Gn) would also appear as a 'theorem' of P as an 'immediate consequence' of a formula falling under 'axiom-schema' III.I and of v Gen r(v). In other words, if v Gen r(v) were to be a 'theorem' (derived by a 'proof' n), r(Gn) would be a 'theorem' for a reason internal to the calculus, and Neg r(Gn) would be a 'theorem' for the reason that it was the 'recursive' formula whose occurrence as a 'theorem' was equivalent, according to the 'modified arithmetization', to n being a 'proof' of v Gen r(v).

In the last paragraph, where part of the proof of Gödel's 'Unprovability' Theorem has been restated in terms which either are used within the calculus P or are syntactical terms used to describe features of P, I have put single quotation marks round 'recursive', 'arithmetical', 'arithmetization', 'modified arithmetization'to indicate that these words are being used (like 'theorem', 'proof', 'provable', etc.) as calculus terms and not as deductive-system terms. The whole of Gödel's formal argument in this paper is syntactical: that he arithmetizes metamathematics instead of only 'arithmetizing' it is purely a matter of expository convenience. For his arithmetization is in terms of recursive arithmetical concepts, and by his Proposition V the question as to whether or not a recursive arithmetical relationship holds between numbers is equivalent to the syntactical question as to which of two 'recursive' formulae containing numerals, of the forms f, Neg f respectively, is a 'theorem' of the calculus P. [In my sketch of Gödel's proof of the 'Unprovability' Theorem I have declined to follow him in using such terms as formula, proof, class-sign with an arithmetical interpretation; and I have, so far as was conveniently possible, employed G-numerals instead of G-numbers.]

Thus Gödel's two great theorems are theorems about his calculus P: they assert the 'unprovability' within P of certain well-formed formulae of P (on the assumption that P is 'w-consistent' or 'consistent' respectively). Of course the interest to the learned world of the calculus P is that it can be regarded as representing a deductive system for arithmetic in which, therefore, there are undecidable arithmetical propositions. Though Gödel's formal proofs apply only to P, he indicates how similar proofs would apply to any calculus satisfying two very general conditions [190], conditions so general that any calculus capable of expressing arithmetic can hardly fail to satisfy them. So this paper of Gödel's proclaimed the thesis, which has been clarified and confirmed by the work of subsequent metamathematicians, that no calculus can be devised in such a way that every arithmetical proposition is represented in it by a formula which is either 'provable' or 'disprovable' within the calculus, and therefore that any deductive system whatever for arithmetic will have the general syntactical characteristic of not containing either a proof or a disproof of every arithmetical proposition.

This syntactical fact about arithmetic is sometimes described by saying that arithmetic, in its very nature, is incomplete. Gödel's discovery of this incompleteness, presented in this paper, is one of the greatest and most surprising of the intellectual achievements of this century.

[I am much indebted to Dr T. J. Smiley for criticizing most helpfully the penultimate draft of this Introduction.

R. B. B.]