Godel number of some relevant expression. Since we have shown in §10.
that all decidable properties can be defined in 3i > Inhere exists a relevant
expression A(x) which in the natural interpretation (i.e., the interpretation
in which 0 corresponds to zero, and so forth) holds for a natural number
if and only if this number is the Godel number of an expression in 3i •
Finite sequences of relevant expressions can be represented by numbers
in the same way as the expressions themselves, so that, in particular,
proofs can be expressed by numbers, since they are merely special
sequences of expressions. Since it is decidable whether a given rule of
inference has been correctly used, we can now find a relevant expression
C(p, q) which in the natural interpretation is true for/? and q if and only if/?
is the number of a relevant expression H and q is the number of a proof
of H in 3i.
We now proceed to construct a relevant expression E, containing no
free variables, which in the natural interpretation states that E (in other
words, the expression itself) is unprovable (cf. the Paradox of the Liar
in §11.3). If we assume that E is provable, we then have the following
situation: Every model of 3i, and consequently also the natural
interpretation, satisfies E and therefore states, in contradiction to our
assumption, that E is unprovable. On the other hand, if we assume that
—I £is provable, the natural model will satisfy —i E, and therefore falsify E;
that is, E is provable, a result which, taken together with the provability
of —I E, contradicts the consistency of 3i • Thus neither E nor —, £ is
provable.
This syntactical result, when reformulated in semantic language, states
that neither E nor —i £" is a consequence of 3i • In other words, 3i is
incomplete, as asserted.
The expression E, which asserts its own unprovability, is constructed as
follows: If n is the Godel number of an expression with exactly one free
variable x, let us denote this expression by /4„(.y) and call n an A number.
We construct the propositional form
A0.15) X is an A number and y is the Godel number of a proof of A^ix).
By means of the arithmetization, this propositional form can be
represented by an expression B{x,y) in 3i with the two free variables
X and y. Now let p be the Godel number of the expression A^ —, B{x, y).
We form the expression Aj,{p) obtained by replacing x with p in Aj,{x).
By A0.15) this expression states:/or every y, the number y is not the Godel
number of a proof of Aj,{p). Thus Aj,{p) is a proposition E of the desired
kind.
This theorem can obviously be extended to all axiomatic theories that
have constructive definitions for their expressions and rules of inference,
and that include a sufficiently large part of arithmetic.
78 PART A FOUNDATIONS OF MATHEMATICS
The incompleteness theorem has some remarkable consequences:
A) There exist arithmetical propositions (e.g., E) that are true for
the natural numbers but are not provable in 3i • It is conceivable, for
example, that the Fermat conjecture or the proposition A0.14) is true
but cannot be deduced by means of the familiar rules of inference in 3i •
B) From the incompleteness of 3i it follows by §4.6 that 3i '•s fiot
monomorphic. For example, the proposition E is true for the model of
the natural numbers but certainly untrue for some other model of 3i,
since E is not a consequence of 3i •
C) If we introduce into 3 certain natural rules of inference (it is to be
noted that the language in which 3 is formulated goes beyond the means
of expression available in the predicate logic), we can prove, just as for 3i,
that there exists in 3 a proposition E such that neither E nor —i £ is
deducible. Then we could proceed, again just as for 3i (see above), to
prove that 3 is incomplete, provided we were allowed, as is the case in 3i,
to replace the concept of provability by the concept of a consequence.
But we know that 3 is complete, as may be proved in exactly the same
way as for ^ in §10.2. Thus we have the important result that in 3> and
more generally in the logics of higher order as contrasted with the predicate
logic, the concept of a consequence cannot be reduced to an algorithm.
One might think that the incompleteness of 3i could be removed by
the introduction of further axioms that would leave the system consistent.
But so long as we are dealing with finitely many axioms (or more generally
with a decidable schema of axioms), the concept of provability remains
decidable, so that the above argument can be applied to the enlarged
system of axioms. Thus we are dealing here with an essential, nonremovable
incompleteness.
These results for 3i and 32 can also be obtained in the following way.
We can show that in any sufficiently expressive arithmetical language
there always exists, for any given recursively enumerable set (§5.3) M of
arithmetical theorems [i.e., arithmetical propositions that are valid in the
natural interpretation (§10.5)], an arithmetical proposition E which,
together with its negation, does not belong to M. Thus we have:
(a) Since the set of deductions in 3i is recursively enumerable (§6.2),
the system 3i is incomplete;
(b) The system 3? like ^, is monomorphic and therefore complete
(§10.2). Thus the set of deductions in 3 is not recursively enumerable,
and therefore certainly not decidable.
For a system of axioms S that includes arithmetic we can also construct,
by means of our arithmetization, a proposition W expressing the
syntactical consistency of S, Then the G5del theorem leads to the result