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.
