**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 **n**_{1}, **n**_{2},
… **n**_{k} as the number **2**^{n1}, **3**^{n2}
… **p**_{k}^{nk}, 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 **n**_{1}, **n**_{2}, … **n**_{k}
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 **x**_{1}, **x**_{2}, …
**x**_{n} 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(x**_{1},x_{2}, … x_{n}) is true,
**R(x**_{1},x_{2}, … x_{n}) can be proved in a *deductive system for
arithmetic* by constructing a finite sequence of propositions starting with the axioms
and ending with **R(x**_{1},x_{2}, … x_{n}); and if
**R(x**_{1},x_{2}, … x_{n}) is false, **Not R(x**_{1},x_{2}, … x_{n})
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(x**_{1},x_{2}, … x_{n})
or of **Not R(x**_{1},x_{2}, … x_{n})
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(x**_{1},x_{2}, … x_{n})
is true, there is a 'proof' of **f**, and **f** is a 'provable' formula
(definition 46); and if **R(x**_{1},x_{2}, … x_{n})
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
**B**_{c} is thus taken as equivalent to his relation **B**, and
**Bew**_{c} 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 p**–a
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 B_{c} and
Bew_{c} 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**,

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.]

Design © 1998 Siegfried. All rights reserved.