Kenan-Safvet wrote:madner wrote:Nije sasvim precizno reci sadrzava ali je apsolutno ispravno koristiti teorem. Ovaj citat je implikacije teoreme, ne njena defincija.
Predlazem da pogledas izvorni tekst, pa se uvjeris da Godel korisitio teoreme za svoj dokaz a ne teorije.
A sad mi reci u cemu je razlika kada bi bila teorija a ne teorema?
Nije ovo implikacija teoreme, nego upravo njena tvrdnja, to mozes naci bilo gdje na netu. Originalnu formulaciju nisam uspio naci, ali nebitno, ti ovdje brkas dva potpuno razlicita pojma, teoreme i teorije. To su striktno definisani matematicki pojmovi, pa tu nema mjesta slobodnoj interpretaciji, tj. ne moze neko koristiti rijec teorem, a neko teorija za isti pojam. Razlika je u tome da jedna formulacija ima, a druga nema smisla, osim ako ti ne zelis uvesti novu konvenciju u matematici i redefinisati pojmove. Definiciju teoreme si ti vec dao, dok bi definicija teorije bila da je to
skup recenica (izjava) u logickom jeziku (ovdje se konkretno radi o logici prvog reda). Evo ti link sa wikipedie:
http://en.wikipedia.org/wiki/Theory_(ma ... cal_logic)
Dakle,
teoriju sacinjavaju aksiomi i njihove logicke implikacije, odnosno
teoreme. Govorimo o konzistentnosti i potpunosti teorije, a ne teoreme.
http://www.research.ibm.com/people/h/hi ... goedel.pdf
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 Rn,
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(Rn(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 Rn(n) that you get when you insert n into its own formula Rn
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 Rq, i.e. we have
S , Rq
for a specic natural number q. We will now prove that the theorem Rq(q) is
undecidable within PM. We can understand this by simply plugging in the denitions:
Rq(q) , S(q) , q 2 K , :provable(Rq(q)), in other words, Rq(q) states \I am improvable."
Assuming the theorem Rq(q) were provable, then it would also be true, i.e. because of
(1) :provable(Rq(q)) would be true in contradiction to the assumption. If on the other
hand :Rq(q) were provable, then we would have q 62 K, i.e. provable(Rq(q)). That
means that both Rq(q) and :Rq(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 Rq(q)
states that q is in K, i.e. according to (1) that Rq(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 Rq(q) states its own improvability it immediately follows that
Rq(q) is correct, since Rq(q) is in fact unprovable (because it is undecidable). The
theorem which is undecidable within the system PM has hence been decided by metamathematical
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).
iz
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
Pokusat cu jos jednom. Sa ovom definicijom teoreme koju si naveo se slazem. Medjutim, kao sto sam vec rekao, konkretan primjer gdje si pogresno upotrijebio tu rijec je ovdje : "...nego se odlucuje da li su tacne ili netacne i one time postaju aksiomi nove teoreme" . Nema smisla govoriti o aksiomima neke teoreme, jer je teorema, kao sto si i sam rekao, jedan iskaz, kao sto su i aksiomi. Govori se o aksiomima koji sacinjavaju teoriju. Evo ti formulacije Godelove teoreme sa wikipedie: 
90%kakao?' 
