canon00-goedel

[ Pobierz całość w formacie PDF ]
0 About this document
Godel's famous proof [
2
,
1
] is highly interesting, but may be hard to understand. Some
of this diculty is due to the fact that the notation used by Godel has been largely
replaced by other notation. Some of this diculty is due to the fact that while Godel's
formulations are concise, they sometimes require the readers to make up their own
interpretations for formulae, or to keep denitions in mind that may not seem mnemonic
to them.
This document is a translation of a large part of Godel's proof. The translation
happens on three levels:
from German to English
from Godel's notation to more common mathematical symbols
from paper to hyper-text
Hyper-text and colors are used as follows: denitions take place in blue italics, like
this:
dened term
. Wherever the dened term is used, we have a red hyper-link to the
place in the text where the term was rst dened, like this:
dened term
. Furthermore,
each dened term appears in the clickable
index
at the end of this document. In the
margin of the document, there are page-numbers like this
[173]
, which refer to the
original document. Here are links for looking up something by page:
173 174 175 176
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 196
. Finally,
small text
snippets in magenta
are comments not present in the original text, but perhaps useful
for the reader.
This translation omits all foot-notes from the original, and only contains sections
1
and
2
(out of four).
The translation comes as-is, with no explicit or implied warranty. Use at your own
risk, the translator is not willing to take any responsibility for problems you might
have because of errors in the translation, or because of misunderstandings. You are
permitted to reproduce this document all you like, but only if you include this notice.
Boulder, November 27, 2000
Martin Hirzel
1
On formally undecidable propositions of Principia
Mathematica and related systems I
[173]
Kurt Godel
1931
1 Introduction
The development of mathematics towards greater exactness has, as is well-known, lead
to formalization of large areas of it such that you can carry out proofs by following a few
mechanical rules. The most comprehensive current formal systems are the system of
Principia Mathematica (PM)
on the one hand, the Zermelo-Fraenkelian axiom-system
of set theory on the other hand. These two systems are so far developed that you
can formalize in them all proof methods that are currently in use in mathematics, i.e.
you can reduce these proof methods to a few axioms and deduction rules. Therefore,
the conclusion seems plausible that these deduction rules are sucient to decide all
mathematical questions expressible in those systems. We will show that this is not true,
but that there are even relatively easy problem in the theory of ordinary whole numbers
that can not be decided from the axioms. This is not due to the nature of these systems,
[174]
but it is true for a very wide class of formal systems, which in particular includes all
those that you get by adding a nite number of axioms to the above mentioned systems,
provided the additional axioms don't make false theorems provable.
Let us rst sketch the main intuition for the proof, without going into detail and
of course without claiming to be exact. The formulae of a formal system (we will
restrict ourselves to the
PM
here) can be viewed syntactically as nite sequences of
the basic symbols (variables, logical constants, and parentheses or separators), and it is
easy to dene precisely which sequences of the basic symbols are syntactically correct
formulae and which are not. Similarly,
proofs
are formally nothing else than nite
sequences of formulae (with specic denable properties). Of course, it is irrelevant
for meta-mathematical observations what signs are taken for basic symbols, and so we
will chose natural numbers for them. Hence, a formula is a nite sequence of natural
numbers, and a proof schema is a nite sequence of nite sequences of natural numbers.
The meta-mathematical concepts (theorems) hereby become concepts (theorems) about
natural numbers, which makes them (at least partially) expressible in the symbols of the
system
PM
. In particular, one can show that the concepts \formula", \proof schema",
\provable formula" are all expressible within the system
PM
, i.e. one can, for example,
2
come up with a formula F(v) of
PM
that has one free variable v (whose type is sequence
of numbers) such that the semantic interpretation of F(v) is: v is a provable formula.
We will now construct an undecidable theorem of the system
PM
, i.e. a theorem A for
which neither A nor :A is provable, as follows:
[175]
We will call a formula of
PM
with exactly one free variable of type natural numbers a
class-sign
. We will assume the class-signs are somehow numbered, call the nth one R
n
,
and note that both the concept \class-sign" and the ordering relation R are denable
within the system
PM
. Let be an arbitrary class-sign; with (n) we denote the formula
that you get when you substitute n for the free variable of . Also, the ternary relation
x , y(z) is denable within
PM
. Now we will dene a class K of natural numbers as
follows:
K = fn 2 IN j:provable(R
n
(n))g (1)
(where provable(x) means x is a provable formula).
With other words, K is the set of
numbers n where the formula R
n
(n) that you get when you insert n into its own formula R
n
is improvable.
Since all the concepts used for this denition are themselves denable in
PM
, so is the compound concept K, i.e. there is a
class-sign
S such that the formula
S(n) states that n 2 K. As a
class-sign
, S is identical with a specic R
q
, i.e. we have
S , R
q
for a specic natural number q. We will now prove that the theorem R
q
(q) is
undecidable within
PM
.
We can understand this by simply plugging in the denitions:
R
q
(q) , S(q) , q 2 K ,:provable(R
q
(q)), in other words, R
q
(q) states \I am improvable."
Assuming the theorem R
q
(q) were provable, then it would also be true, i.e. because of
(
1
) :provable(R
q
(q)) would be true in contradiction to the assumption. If on the other
hand :R
q
(q) were provable, then we would have q 62 K, i.e. provable(R
q
(q)). That
means that both R
q
(q) and :R
q
(q) would be provable, which again is impossible.
The analogy of this conclusion with the Richard-antinomy leaps to the eye; there
is also a close kinship with the liar-antinomy, because our undecidable theorem R
q
(q)
states that q is in K, i.e. according to (
1
) that R
q
(q) is not provable. Hence, we have
in front of us a theorem that states its own unprovability. The proof method we just
applied is obviously applicable to any formal system that on the one hand is expressive
[176]
enough to allow the denition of the concepts used above (in particular the concept
\provable formula"), and in which on the other hand all provable formulae are also
true. The following exact implementation of the proof will among other things have
the goal to replace the second prerequisite by a purely formal and much weaker one.
From the remark that R
q
(q) states its own improvability it immediately follows that
R
q
(q) is correct, since R
q
(q) is in fact unprovable (because it is undecidable). The
theorem which is undecidable within the system
PM
has hence been decided by meta-
mathematical considerations. The exact analysis of this strange fact leads to surprising
results about consistency proofs for formal systems, which will be discussed in section
4
(theorem XI).
3
2 Main Result
We will now exactly implement the proof sketched above, and will rst give an exact
description of the formal system
P
, for which we want to show the existence of unde-
cidable theorems. By and large,
P
is the system that you get by building the logic of
PM
on top the Peano axioms (numbers as individuals, successor-relation as undened
basic concept).
2.1 Denitions
The
basic signs
of system
P
are the following:
I. Constant: \:" (not), \_" (or), \8" (for all), \0" (zero), \succ" (the successor of),
\(", \)" (parentheses).
Godel's original text uses a dierent notation, but the reader
may be more familiar with the notation adapted in this translation.
II.
Variable of type one
(for individuals, i.e. natural numbers including 0): \x
1
",
\y
1
", \z
1
", :::
Variables of type two
(for classes of individuals
, i.e. subsets of IN
): \x
2
", \y
2
", \z
2
",
:::
Variables of type three
(for classes of classes of individuals
, i.e. sets of subsets of
IN
): \x
3
", \y
3
", \z
3
", :::
And so on for every natural number as type.
Remark: Variables for binary or n-ary functions (relations) are superuous as
ba-
sic signs
, because one can dene relations as classes of ordered pairs and ordered pairs
as classes of classes, e.g. the ordered pair (a;b) by ffag;fa;bgg, where fx;yg and fxg
stand for the classes whose only elements are x;y and x, respectively.
[177]
By a
sign of type one
we understand a combination of signs of the form
a; succ(a); succ(succ(a)); succ(succ(succ(a))); ::: etc.;
where a is either 0 or a
variable of type one
. In the rst case we call such a sign a
number-sign
. For n > 1 we will understand by a
sign of type n
a
variable of type n
.
We call combinations of signs of the form a(b), where b is a sign of type n and a a sign
of type n + 1,
elementary formulae
. We dene the class of
formulae
as the smallest
set that contains all
elementary formulae
and that contains for a;b always also :(a),
(a) _ (b), 8x . (a) (where x is an arbitrary variable). We call (a) _ (b) the
disjunction
of a and b, :(a) the
negation
and 8x . (a) the
generalization
of a. A formula that
contains no free variables (where free variables is interpreted in the usual manner) is
called
proposition-formula
. We call a formula with exactly n free individual-variables
(and no other free variables) an
n-ary relation sign
, for n = 1 also
class-sign
.
By
subst
a
4
v
b
(where a is a
formula
, v is a
variable
, and b is a sign of the same type
as v) we understand the formula that you get by substituting b for every free occurrence
of v in a. We say that a formula a is a
type-lift
of another formula b if you can obtain
a from b by increasing the type of all variables occurring in a by the same number.
The following
formulae
(I through V) are called
axioms
(they are written with the
help of the abbreviations (dened in the usual manner) ^, ), ,, 9x, =, and using the
customary conventions for leaving out parentheses):
I.
The
Peano axioms
, which give fundamental properties for natural numbers.
1. :(succ(x
1
) = 0)
We start to count at 0.
2. succ(x
1
) = succ(y
1
) ) x
1
= y
1
If two natural numbers x
1;2
2 IN have the same
successor, they are equal.
3.
)8x
1
. x
2
(x
1
)
We can prove a predicate
x
2
on natural numbers by natural induction.
II. Every
formula
obtained by inserting arbitrary formulae for p;q;r in the following
schemata.
We call these
proposition axioms
.
[178]
1. p_p ) p
2. p ) p_q
3. p_q ) q_p
4. (p ) q) ) (r_p ) r_q)
III. Every formula obtained from the two schemata
1. (8v . a) )
subst
a
v
c
2. (8v . b_a) ) (b_8v . a)
by inserting the following things for a;v;b;c (and executing the operation denoted
by
subst
in 1.):
Insert an arbitrary
formula
for a, an arbitrary
variable
for v, any formula where v
does not occur free for b, and for c a sign of the same type as v with the additional
requirement that c does not contain a free variable that would be bound in a
position in a where v is free.
For lack of a better name, we will call these
quantor axioms
.
IV. Every formula obtained from the schema
1. 9u .8v . (u(v) , a)
by inserting for v and u any variables of type n and n + 1 respectively and for
a a formula that has no free occurrence of u. This axiom takes the place of the
reducibility axiom
(the
comprehension axiom
of set theory).
5
x
2
(0)^8x
1
. x
2
(x
1
) ) x
2
(succ(x
1
))
[ Pobierz całość w formacie PDF ]