Godel's
Theorem. The
proof, published by Kurt Godel in 1931, of the existence of formally undecidable
propositions in any formal system of arithmetic. More precisely, his first
incompleteness theorem… states that in any formal system S of arithmetic,
there will be a sentence P of the language of S such that if S
is consistent, neither P nor its negation can be proved in S.
…This makes it possible to show that there must be a sentence P of S
which can be interpreted (very roughly) as saying 'I am not provable'. It is
shown that if S is consistent, this sentence is not provable, and hence,
it is sometimes argued, P must be true. It is this last step which had
led people to claim that Godel's theorem demonstrates the superiority of men
over machines - men can prove propositions which no machine (programmed with
the axioms and rules of
a formal system) can prove. But this is to overlook the point that the proof
of the theorem only allows one to conclude that if S is consistent,
neither P nor its negation is provable in S. One cannot go on
to conclude that P is not provable in S, and hence must be true,
without having proved the consistency of S. Indeed, because Godel's proof
is formalizable in S, it could be said that one machine T could
prove of another machine T' that if T' is consistent, there is
a proposition that T' cannot prove. But T' could prove the same
thing about T.
…The fact that the first
incompleteness proof can be formalized in S allows one to derive Godel's
second incompleteness theorem as a corollary. This theorem states that the
consistency of a formal system of arithmetic cannot be proved by means formalizable
within that system. This result was damaging to the prospects of completing
Hilbert's programme for the foundations of mathematics, for Hilbert had hoped
to justify the use, in calculus for example, of the notion of infinity by
showing that a formal system governing its use could be shown to be consistent
using only finitistic methods. This would have demonstrated that the notion
could be regarded merely as a calculating device whose use was legitimate,
in that it would never lead one astray, and justified in terms of economy
of labour. But the finitistic methods envisaged are formalizable with a formal
system of arithmetic and were thus shown to be inadequate to Hilbert's task.
