出版社: W. W. Norton & Company
副标题: The Proof and Paradox of Kurt Godel (Great Discoveries)
出版年: 200502
页数: 296
定价: USD 22.95
装帧: Hardcover
ISBN: 9780393051698
内容简介 · · · · · ·
A masterly introduction to the life and thought of the man who transformed our conception of math forever.
Kurt Gödel is considered the greatest logician since Aristotle. His monumental theorem of incompleteness demonstrated that in every formal system of arithmetic there are true statements that nevertheless cannot be proved. The result was an upheaval that spread far bey...
A masterly introduction to the life and thought of the man who transformed our conception of math forever.
Kurt Gödel is considered the greatest logician since Aristotle. His monumental theorem of incompleteness demonstrated that in every formal system of arithmetic there are true statements that nevertheless cannot be proved. The result was an upheaval that spread far beyond mathematics, challenging conceptions of the nature of the mind.
Rebecca Goldstein, a MacArthurwinning novelist and philosopher, explains the philosophical vision that inspired Gödel's mathematics, and reveals the ironic twist that led to radical misinterpretations of his theorems by the trendier intellectual fashions of the day, from positivism to postmodernism. Ironically, both he and his close friend Einstein felt themselves intellectual exiles, even as their work was cited as among the most important in twentiethcentury thought. For Gödel , the sense of isolation would have tragic consequences.
This lucid and accessible study makes Gödel's theorem and its mindbending implications comprehensible to the general reader, while bringing this eccentric, tortured genius and his world to life.
About the series:Great Discoveries brings together renowned writers from diverse backgrounds to tell the stories of crucial scientific breakthroughs—the great discoveries that have gone on to transform our view of the world.
世界上有一些人通过改变世界而改变人类，而另有一些人则通过改变人类的思想而改变世界，哥德尔应该算是后者。他被认为是继亚里士多德以后一位最伟大的逻辑学家，而他发现不完全性定理则是现代思想具有划时代意义的大事件。曾有评价说，不了解哥德尔就不了解人类已达到的智力水平与人类智力奋斗的历程。应该说，这个评价绝非言过其实。哥德尔和哥德尔的亲密朋友爱因斯坦都认为他们是智力的流放者，即使他们的工作被认为是20世纪最重要的思想。在此书中，曾获麦克阿瑟学会奖的哲学家Rebecca Goldstein揭示了对于哥德尔的数学具有启发意义的哲学理论，同时也对那些运用更时髦的哲学理论———这包括从实证主义到后现代理论等而对哥德尔的理论所作的诸般曲解加以分析。作者将哥德尔的理论以尽可能清晰明白的语言加以表述，并展示了这位天才人物看似古怪的生活世界。
Incompleteness的书评 · · · · · · (全部 0 条)
读书笔记 · · · · · ·
我来写笔记
The second incompleteness theorem states that the consistency of a formal system that contains arithmetic can't be formally proved within that system. It would seem to follow, pretty straightforwardly, from the first. Remember that the first incompleteness result has the form of a conditional statement: if the formal system of arithmetic is consistent, then G. /ĺ…Źĺź?ĺ†…...
20130909 05:57
($C \rightarrow G$)，($G$)不可证，所以($C$)不可证。The second incompleteness theorem states that the consistency of a formal system that contains arithmetic can't be formally proved within that system. It would seem to follow, pretty straightforwardly, from the first. Remember that the first incompleteness result has the form of a conditional statement: if the formal system of arithmetic is consistent, then G.
回应 20130909 05:57 
The first Godel's incompleteness theorem的证明的部分翻译： The First Incompleteness Theorem: The Overall Strategy The twentyodd pages of Godel's famous proof are densely compact. There are 46 preliminary definitions. There are also preliminary theorems that must be proved before the main event can take place: the construction of an arithmetical proposition that is both true and unprovable w...
20130908 22:55
The first Godel's incompleteness theorem的证明的部分翻译：The First Incompleteness Theorem: The Overall Strategy
The twentyodd pages of Godel's famous proof are densely compact. There are 46 preliminary definitions. There are also preliminary theorems that must be proved before the main event can take place: the construction of an arithmetical proposition that is both true and unprovable within the formal system under consideration. The lines of reasoning in the proof are highly compressed, composed of a hierarchy of interconnected levels of discourse, the blended voices of the symphony.
尽管细节很复杂，整体策略却非常简单。就像任何用到自我矛盾的证明，证明一个算术命题正确而又不可证明的策略简单而又奇怪。其中最神奇的部分是证明中与自引用矛盾的结合。证明中最有趣的部分类似于最古老的悖论，the liar's paradox。Though the details of the proof are difficult, the overall strategy is—happily!—almost simplicity itself. Simple but strange, as one would expect of a proof that draws so close to the edge of selfcontradiction, proving that there are true arithmetical propositions that are not provable. One of the strangest things of all about the proof is that it coopts the very structure of selfreferential paradoxes, those abominations to reason, and reshapes that structure to its own ends. The overall strategy of the proof—the delightfully accessible part of the proof—can be grasped in the context of the oldest known paradox of all, the liar's paradox. We can convey the gist of the proof in a breezy, easy way, which we will now proceed to do. Then in the next few sections we will concentrate on filling in a few more of the details, indicating how the hard work gets done.
By tradition, the liar's paradox is attributed to the Cretan Epimenides, who reputedly said something implying: All Cretans are liars. This sentence, in itself, isn't paradoxical, except insofar as it suggests that what Epimenides was saying was something like this:
($这个命题是假的。$)This very sentence is false.
问题在于上面的命题是真的只有在它为假的时候。而Godel的策略是使用一个类似的命题：Now that sentence, as we've already seen, is true if and only if it's false—not a good situation, logically speaking. Godel's strategy involves considering an analogue to that paradoxical sentence, viz. the proposition:
($这个命题在这个系统中不可证。$)This very statement is not provable within this system.
令它为($G$)。尽管像所有自引用命题一样奇怪，却不像之前的命题，($G$)不是一个悖论。Let's call this sentence G. G, unlike its analogue, isn't paradoxical, though it is, like all selfreferential propositions, somewhat strange. (Even the nonparadoxical selfreferential This very statement is true is mystifyingly strange. What's it saying? Where's its content?)
通过后面称为Godel计数的编码系统，($G$)可以转为算术符，所以它也可以看作是个算术命题，这个将在后面提到，是比较复杂的部分。Godel找到了一个算术和本身形式化相结合的方法，($G$)同时包含了两个方面，一是它本身算术上的声明，二同时断定了自己的不可证性。换句话说，除了直观的算术内容（尽管是非常奇怪的），($G$)同时意味着：Through the system of encoding we have come to call "Godel numbering" (of course selfeffacing Godel didn't name it so) G can be rendered in arithmetical notation, so that it also makes an arithmetical statement. Here is one of the places where the hard work comes in, and a bit later on in this chapter we'll dip a little deeper into this aspect of the proof. Godel found an ingenious way of making an arithmetical language speak of its own formalism. The upshot of the technique is that G is simultaneously making two different statements, asserting an arithmetical claim and also asserting its own unprovability. In other words, what G has to say, in addition to its straightforward arithmetical content (it's going to be a weird arithmetical proposition, what with all the fiddle faddling that gets us to it) is:
($G$)在系统中不可证。而($G$)的反是：($G$)在系统中可证。G is improvable in the system. The negation of G thus amounts to the proposition: G is provable in the system.
如果($G$)是可证的，它的反即为真，($G$)即为假。而如果($G$)可证，($G$)又是真的。所以，在假定系统一致的前提下（因为不一致的系统所有命题皆可证），G可证引出矛盾，所以在一致的系统中($G$)不可证，而这就是($G$)命题本身：即($G$)不可证，所以($G$)是真的。这样，($G$)即为真又不可证，而这就Godel的著名结论，在一致的系统中存在为真而不可证的命题。而因为($G$)同时有一个直观的对应的算术意义，Godel的证明显示了在一致的形式系统中存在一些算术真命题不可证（如($G$)），也就是说形式系统要么不一致要么不完备。If G were provable then its negation—which, after all, says that G is provable—would be true. But if the negation of a proposition is true, then the proposition itself is false. So if G is provable then it is false. But if G is provable, then it is also true. After all, what else does a proof show, assuming of course that the system is consistent (since in an inconsistent system all propositions are provable). So, assuming the consistency of the system, if G is provable then it is both true and false—a contradiction—which means that G is not provable. Thus if the system is consistent, then G is not provable in it. But that is exactly what G says: that it isn't provable. So G is true. Therefore, G is both unprovable and true, which is precisely the famous conclusion of Godel's proof, that there is a true but unprovable proposition expressible in the system if the system is consistent. And because G also has a straightforwardly arithmetical meaning which, of course, is true if G is true (because it is G) Godel's proof shows that there are arithmetical truths (for example, G!) that cannot be proved within the formal system, assuming the system to be consistent. The formal system is either inconsistent or incomplete.
更重要的是，证明同时显示了在我们将($G$)作为公理加入到形式系统之后，我们可以构造一个相应的新的($G$)，也就是说新的形式系统仍然是不完备的。结论是，在任何一致的包含基础算术的形式系统中，存在被证明的不可证却为真的命题。一个复杂到包含基本算术的系统不能同时一致和完备。后面是细节。What is more, the proof demonstrates that should we try to remedy the incompleteness by explicitly adding G on as an axiom, thus creating a new, expanded formal system, then a counterpart to G can be constructed within that expanded system that is true but unprovable in the expanded system. The conclusion: There are provably unprovable, but nevertheless true, propositions in any formal system that contains elementary arithmetic, assuming that system to be consistent. A system rich enough to contain arithmetic cannot be both consistent and complete. That's really the overall strategy. In some sense (once one assimilates the strange idea of a single proposition that can speak simultaneously of itself and of arithmetic), it is simple. Of course, the devil is all in the details; and it's to the diabolical details that we will now turn.
第一步：展开形式系统Step One: Lay Out a Formal System
Godel的形式系统包含了一个字符表，将这些符号结合成命题的规则，一组被称为公理的命题和一套推导系统。Godel begins his proof by laying out his formal system, which consists, as do all formal systems, of an alphabet of symbols, rules for combining these symbols into wffs, a special set of wffs called the "axioms," and a deductive apparatus for deriving (as "logical consequences") wffs from other wffs that must be either axioms or consequences of axioms.
大多形式逻辑系统有“且”、“或”、“意味”和“当且仅当”这样的逻辑表达式，同时一些系统还有像“所有”和“一些”这样的量词。而一些逻辑符号可以用其它的取代从而得到一个尽可能简单的系统。如“p意味着q”相当于“非p且q”。经过取代，我们通过含九个基本概念和相应符号的形式系统表达算术。In most systems of formal logic, it is convenient to have symbols for "and"(conjunction) and "or" (disjunction), as well as for the expressions "if... then ..." (material implication) and ". . . if and only if. ..". There are also symbols that express the quantificational notions of "all" and "some." However, it will be more convenient to have as few basic symbols as possible. We can eliminate conjunctions in favor of disjunctions since "p and q" means the same thing as "it's not the case that p is false or q is false." So I want to eat and I want to be thin is equivalent to It's not true that either I don't want to eat or don't want to he thin. Then we can take our elimination one step further since disjunction can be eliminated in favor of material implication because "if p, then q" means the same thing as "not p or q" We can also eliminate the notion of "some," by using the notion of "all" since "there are some x's that are F" is the same as "it is not the case that all x's are not i." So Some logicians are rational is equivalent to Not all logicians are irrational. After our eliminations, we're left with nine primitive concepts, and corresponding symbols, with which to express all of arithmetic in a formal system.
第二步：Godel计数Step Two: Godel Numbering
下一步是设计一种将不同的数字赋给系统中每一个命题的方法。通过这样的赋值，算术声明同时是元数学上的一个声明。The next step in the proof is to devise a mechanical method of assigning a unique number to every proposition of the system. It's by assigning these numbers that the blending of the voices is accomplished, with arithmetical statements also making metamathematical statements.
逻辑学家Simon Kochen通过Kafka（which Godel happened to admire）的工作向我解释了Godel的证明。在Kafka和Godel的世界里都有一个类似于AliceinWonderland的感觉，一种进入了一个奇怪的，所有东西，包括意义本身，都对应进入别的东西的世界里的感觉。这里是基本思想：The logician Simon Kochen beautifully described Godel's proof to me as bearing a marked similarity to Kafka's work (which Godel happened to admire). In both Kafka and Godel, there is a certain AliceinWonderland quality, a sense that one has entered a strange universe where things morph into others, including meanings themselves. Yet everything proceeds stepwise according to the most rigorous rulebound logic. (The rigorous logic of Kafka is underappreciated.) So much of the work in Godel's proof amounts, in Kochen's words, to "bookkeeping." This double aspect of the proof mirrors something, Kochen also said, essential about Godel's mind as well, the wild leaps of imagination coupled with a sort of legalistic ploddingness. Both of these aspects emerge in the Godel numbering. Here's the basic idea:
形式系统包含一系列的东西：字符表，结合字符表到命题和一串命题（即证明）。一切都是由基本字符组成：一个命题是一串符号，而一个证明是一串命题（结论是该串的最后一个命题）。The formal system, remember, involves a variety of types of objects: the symbols of the alphabet, the combinations of symbols into wffs, and special sequences of wffs (in other words, proofs). Everything is built out of the basic symbols of the alphabet: a wff is a sequence of these symbols, and a proof is a sequence of wffs (with the conclusion simply the last entry in the sequence).
因此，Godel计数首先给每一个基本符号分配了一个数字。之后依据组合的形式，继续给每一条命题分配数字。最后相应的给每个证明分配数字。The Godel numbering thus begins by assigning each primitive symbol of the alphabet a number. Once each of the primitive symbols has a number, one continues with a rule for assigning numbers to the wffs themselves, based on the corresponding numbers of their constituents. Then, once we have a Godel number for each wff, the Godel numbering is completed with a rule for assigning numbers to sequences of wffs, which, of course, are what proofs are.
此外，当每一个命题被赋值以后，我们可以仅仅通过数值上的算术关系分析命题间的结构关系，或相反。如当相应数字算术上有某种特定的关系时，其中的一条命题可以正好为另一条的结论。换句话说，形式系统中可表达的算术关系和元描述上通过命题表达的逻辑关系变得互相对应了，These metastatements are purely syntactic, as they are simply the consequences of the syntax of the formal system, that is, its rules.（而因为只是形式系统中语法规则的使用结果，其中的元描述又是纯语法上的？）Furthermore, once every wff has been assigned a corresponding number, we will be able to analyze the structural relationships between the propositions by merely analyzing the arithmetical relationships between their corresponding numbers. Or vice verse. For example, one wff will be a consequence of another one precisely in case the Godel numbers of the wffs are arithmetically related to each other in just the right way. In other words, two different sorts of descriptions will be collapsed into one another: arithmetical descriptions, setting forth relationships between numbers that are expressible within the formal system; and metadescriptions about the logical relationships holding between the wffs in the system. These metastatements are purely syntactic, as they are simply the consequences of the syntax of the formal system, that is, its rules.
Godel计数的思想本质上就是编码。The idea of Godel numbering is basically the idea of encoding, which allows you to move back and forth between the original propositions and the code. In elementary school, my friends and I had a similar code we'd use to pass notes in class, assigning each letter of the alphabet a number between 1 and 26, with "A" assigned 1, "B" assigned 2, etc. "Meet me" was rendered as: 13 5 5 20 13 5.
而Godel的编码系统要确保的是同一数字不会被赋给不同的东西，如赋给一个命题或一个证明。编码规则给了我们一个从命题或证明到唯一的数字的一个算法，当然也有一个逆算法。The Godel numbering must obey one further condition: the translation of syntactic descriptions of the logical relationships between wffs in the system into arithmetical propositions that it provides must be such that these arithmetical propositions are themselves expressible within the system.（Godel计数的另一个要求是翻译结果算术上必须可表述？）The encoding system Godel used had to ensure that the same Godel number wouldn't be assigned to different things, say to both some wff as well as to a sequence of wffs (a proof). The rules for encoding give us an algorithm (which is, remember, a set of rules which tell us, at each step, how to proceed, often based on the result we get from a previous application of rules in the set) for getting from any wff, or sequence of wffs, to a unique Godel number. There is also an algorithm for the reverse process: given any Godel number, we can effectively figure out what formal object in the system it stands for. The Godel numbering must obey one further condition: the translation of syntactic descriptions of the logical relationships between wffs in the system into arithmetical propositions that it provides must be such that these arithmetical propositions are themselves expressible within the system.
类比于日常的编码系统，Godel的系统使用的是质数的指数乘积并依赖于质因数分解理论。而这里例举的是简化的编码方式。The spirit of Godel numbering can be conveyed simply, though were we to be rigorous, as Godel of course was, there would be nothing simple about the encoding. The modern positional notation is so familiar to us that we forget it is itself a coding system, requiring proof in the formal system. So, for example, the usual digital symbol 365 is shorthand for 3 times 10 squared, plus six times 10, plus five. Godel's system of encoding used the exponential products of prime numbers and relied on the prime factorization theorem which states that every number can be uniquely factored into the product of primes. The prime factorization theorem ensured that there was an algorithm for getting from any wff or sequence of wffs to a Godel number and vice verse. The digit juxtaposition we use below would, if made rigorous, be every bit as complicated as the system that Godel used. But we won't be rigorous.
首先，我们任意的赋自然数给形式系统中的每个符号：First, we'll arbitrarily assign a natural number to each symbol of the alphabet of the formal system. We can do all we need to do in setting out a formal system of arithmetic if we restrict ourselves to just nine symbols, to each of which we'll assign a Godel number:
量词“所有”由括号和变量表示，如($(x)F(x)$)表示所有($x$)满足($F$)。角分符号用于新的变量：($x$)，($x'$)，($x''$)，($x'''$)等。另外因为($0$)符号和后继符号，我们有了所有的自然数。The quantificational notion of "all" is represented by using parentheses and variables. So, for example, (x)F(x) means: all x's are F. The prime allows us to generate additional variables: x, x', x'', x''' etc. Since we have a symbol for 0, and a way of indicating successors, we have a way of indicating all the natural numbers.
现在我们给出尽可能简单的赋值的规则，只是把Godel数字嵌入到到命题之中。We now specify a rule for assigning Godel numbers to wffs, which of course are just sequences of the symbols of the alphabet. We adopt the easiest rule possible, reminiscent of the encoding my friends and I used in elementary school. We simply plug in the Godel number for each symbol in the wff and that will be the Godel number for the wff.
考虑定理($P_1$)：($$(x)(x')((s(x) = s(x')) \rightarrow (x = x'))$$)So consider this wff:
假设我们讨论的是自然数，($p_1$)代表如果两个数字有相同的后继，那么他们相等。Assuming our universe of discourse (the objects to which the variables are interpreted to be referring) is the natural numbers, what P1 says is that if two numbers have the same successor, then they're the samenumber. Or, in other words, that one number can't be the successor of two different numbers. More literally: for all x and for all x', if the successor of x is identical to the successor of x, then x is identical to x.
现在依次将其中的符号替换为数值，开括号替换为7，($x$)为3，闭括号8，等等，我们得到了相应的Godel数。令($p$)的Godel数表示为($GN(p)$)，我们得到：($$GN(p_1) = 738739877673846739882734398$$)Now we're going to turn this wff into a number by just consecutively going along and replacing each symbol in the wff by its Godel number. Every symbol in the formula P1 has been assigned a number: the open parenthesis a 7, the x a 3, the close parenthesis an 8, the tilde a 1. Replacing each element of the formula with the corresponding Godel number yields a large number, which is the Godel number for the wff. Abbreviating "the Godel number of the proposition p" by GN(p),we obtain:
我们用0分割定理。In this way Godel numbers are assigned to wffs, which are sequences of symbols, and hence to propositions, which are just special wffs. In the same way, Godel numbers can be assigned to sequences of propositions, and in particular to potential proofs, which are, after all, just sequences of propositions, using the Godel numbers already assigned to propositions. Bookkeeping! In our simplified version, the Godel number of a sequence of propositions (a potential proof) is obtained basically by putting the Godel numbers of the sequenced propositions together; however, since it is important to be able to unambiguously extract from the number obtained the original sequence of propositions, we'll need some sort of signal that will indicate where one proposition ends and the next one begins—sort of like a carriage return on a typewriter. We'll let 0 function as our carriage return, indicating that we now go to a new line in the proof.
如在某个定理串中($p_1$)在($p_2$)后面，而($p_2$)定义为：($$s(0) = s(0)$$)So, let us say that in a particular sequence of propositions, p1 is followed by p2, where p2 is defined as:
Godel数为($$GN(p_1 p_2) = 7387398776738467398827343980675846758$$)The Godel number that will correspond to the sequence of P1 followed by p2 is
这样所有形式系统中逻辑关系变成了算术上可表达的。如，若($wff_1$)逻辑上导出($wff_2$)，($GN(wff_1)$)和($GN(wff_2)$)既有特定的纯算术上的关系。Through Godel's inspired contrivances, all of the logical relations that hold between propositions in the formal system become arithmetic relations expressible in the arithmetical language of the system itself. This is the essence of the heartstopping beauty of the whole thing. So if, for example, wff1 logically entails wff2, then GN(wff1) will bear some purely arithmetical relation to GN(wff2). Suppose, say, that it can be shown that if wff1 logically entails wff2, then GN(wff2) is a factor of GN(wff1). We would then have two ways of showing that wff1 logically entails wff2: we could use the rules of the formal system to deduce wff2 from wff1 or we could show that GN(wff1) can be obtained from GN(wff2) by multiplying by an integer. Suppose that GN(wff1) = 195589 and GN(wff2) = 317. 317 is a factor of 195589, since 317 multiplied by 617 = 195589. So that wff1 logically entails wff2 could be demonstrated either by using the formal rules of proof to arrive at wff2 from wff1 or, alternatively, by using the rules of arithmetic to arrive at GN(wff1) = 195589 by multiplying 617 by 317 = GN(wff2). The metasyntactic and the arithmetic collapse into one another.
一旦清楚了算术和逻辑之间的关系，逻辑证明在系统中就有了可表达的算术属性。而推导这些算术属性就相当于前段所讲的转换的结果。比如系统中合法证明得到的命题的Godel数就会有特定的算术属性，比如奇偶或者指数成方之类或更可能的远比此复杂的属性。换句话说，可证性变成了一种算术关系。这样，我们就得到了一种同时包含其自身在系统中可证性信息的在系统中可表达的算术定理。Once one has this sort of collapse between logical implication and arithmetical relationship, we can go on and demonstrate that certain sequences of wffs—precisely those that constitute proofs—have an arithmetical property expressible in the system. Proofs, of course, are built up out of logical entailments. So deriving this arithmetical property (of the Godel numbers of all and only the proofs in the system) is going to be a consequence of the sort of collapse discussed in the previous paragraph. The Godel number of those strings of wffs that are valid proofs within the system will have some sort of arithmetical property, say, they'll all be even or they'll all be odd or they'll be prime numbers or the squares of primes or, more likely, a property a good deal more complicated. In other words, the metasyntactic relationship of provability will become an arithmetical relationship; that a string of wffs is a proof will be some property of numbers. From this it becomes possible to show that all and only the provable wffs in the system, the theorems, have a certain arithmetical property. You can see where we're heading: toward arithmetical propositions expressible in the system that also speak to the issue of their own provability within the system. The Godel numbering allows some propositions to engage in an interesting sort of doublespeak, saying something arithmetical and also commenting on their own situation within the formal system, saying whether they're provable.
这就像戏剧中的角色和其扮演者日常生活中的角色相互影响的关系。The doublespeak of these propositions could be compared to the sort of thing that sometimes happens within a dramatic play, in particular when the play presents actors as characters, with their own "reallife" relationships, and then presents these characters as actors in a play within the play. Through careful contrivance, the lines that the actors speak, in the play within the play, can also be interpreted as having a reallife meaning in their relationships outside the play within the play (in the play proper). Godel's strategy asks us to grasp something analogous to what the country audience in Leoncavallo's opera Pagliacci grasp when they understand the actors to be delivering lines that, as well as making sense within the play, have a meaning in their offstage lives (in the opera). In Godel's inspired stage production, lines speak both to the formal relationships within the system, the play within the play, and also reveal reallife arithmetical relationships. The proposition that Godel's proof constructs, the one that will simultaneously announce both its own (provable) unprovability and a true (unprovable) arithmetical relationship, has the same sort of doubleentendre as Pagliacci's final tragic cry, "La Commedia è finita!"—the comedy is over.
第三部：构造一个因为描述了其不可证性而为真的命题Step Three: Create a Proposition That's True Because It Says That It's Unprovable
之后，Godel给出了一个神奇的算术属性，称为($Pr$)或者“可证明”。它是所有系统中可证命题的Godel数才拥有的纯算术属性。Having established his ingenious layers of meaning, Godel now conjures a rather amazing arithmetical property, which we'll designate as "Pr" for "provable." Because, although Pr is a purely arithmetical property, it's also that very property toward which all the contrivances have been heading. It's an arithmetical property that is true of all and only the Godel numbers of the provable propositions of the system. I choose the verb "conjures" deliberately because even though the collapse of the metasyntactic and arithmetical was heading toward "Pr", there is still a sense of magic about the entrance of Pr.
在继续之前，这里是一些小的技术细节：通过单变量的命题函数代表属性，形如($F(x)$)。当($x$)被定义域中任一值替换后，($F(x)$)才成为了一个或真或假的命题。Before getting to the property, one little technical point about the way in which properties are specified: by propositional functions of one variable. These can be thought of as of the form F(x). These are expressions in the formal system involving a single variable—the x which is a dummy standing for a whole range of possible values (the domain of individuals) that can be plugged in; if you plug in a value for the variable, you end up with a wff that is either true or false, in other words a proposition. F(x), just as it is, is neither true nor false. So say s(x) were to mean: x is the successor of 1. This is neither true nor false; it isn't a proposition, a definite statement, since what it says depends upon what x actually represents. Plugging in 2 for the variable x yields a true proposition, and plugging in anything else yields false propositions. That's how properties are designated in the system, by propositional functions of one variable.
回到($Pr(x)$)，一个比较复杂的算术属性。首先，所有命题都通过Godel计数被赋予了一个数值，即每个($wff_p$)，我们有($GN(p)$)。而定理是系统中所有命题的一个子集，即可证命题。所以，给一个自然数($n$)，它不一定对应于系统中的某个定理，即对($n = GN(p)$)，($p$)不一定可证。Now onward to Pr(x), which is a somewhat complicated property of numbers. Remember, first of all, that each of the wffs in the formal system have been assigned numbers through the wonders of Godel numbering. So for every wff p, we have some GN(p), some natural number or other. The theorems are a special subset of the wffs of the system, the provable propositions. Given any natural number n, then, it may or may not be the case that it corresponds to some theorem in the formal system, that is, it may or may not be the case that n = GN(p) for some proposition p which is a theorem of the formal system.
现在定义($Pr(x)$)。该命题函数的定义域为自然数，对任意自然数($n$)，若对定理($p$)，($n = GN(p)$)，我们称($n$)满足($Pr(x)$)，即($Pr(n) $)为真。Godel证明了该属性不管其复杂度，可通过形式系统中给出。另外通过这个属性，Godel可以同时描述命题是否为定理的属性，并将之转为算术陈述，即“($p$)是个定理”转为“Pr(GN(p))”，称($n$)满足($Pr(x)$)即表示($n$)相应的命题是定理。Now we are in position to define Pr(x). The possible values for this propositional function, the things we plug in for the dummy x, are (the expressions for) the natural numbers. For any natural number n, if n = GN(p) for a theorem p of the system then we say that n satisfies the property Pr(x), that is, that Pr(n) is true. Godel showed that this property is one that can in fact be expressed in the formal system, that is, that it's an example of an F(x). Pr(x) is a formally expressible arithmetical property, albeit one that is extremely complicated, not anything that we can explicitly give here. But by means of this property Godel is able to take metasentences about the system, stating which propositions are theorems of the system, and transform them into arithmetical sentences within the system: "p is a theorem" is transformed into "Pr(GN(p))". To say of some particular n that it has the property Pr(x) is to say that this number corresponds to a theorem in the formal system.
就如奇偶性一样，($n$)满足($Pr(x)$)确实是真的算术属性。Now perhaps you're thinking something like this: That a particular number n has the property Pr(x) isn't a real property of n. The number n, for example, may be even or it may be odd; if it's divisible by 2 then it's even. Let's say it is. Then its evenness is a real arithmetical property; n couldn't be the number it is if it weren't even. In contrast, looking at this property Pr(x) metasystematically, it doesn't seem at all a proper sort of numerical property. A number n has this property only arbitrarily, since the proposition with which n is associated is arbitrary, a consequence merely of the way in which the Godel numbering was set up, the inspired contrivances. True enough, but, arbitrary though it may be, Pr(x) is nonetheless a real arithmetical property, and a number n either will or won't have it. And n wouldn't be the number that it is unless it either did or didn't have it. Just because Pr(x) has a metameaning doesn't detract from its arithmetical character. This property Pr(x) is, in fact, stupendous, and it allows us to take the plunge into the heart of the proof.
接下来用到的是对角引理（diagonal lemma，证明未给出），它的一个特殊形式被用在了Godel的证明中，而这儿为简化证明，使用了它的通用形式。http://en.wikipedia.org/wiki/Diagonal_lemmaWhat we use next is something called the diagonal lemma. It's a general statement, a particular case of which is what we need to prove Godel's theorem. (Godel didn't actually use it, but rather derived the particular case.) Making use of this general lemma (which, of course, we're not going to prove) will simplify matters enormously.
对角引理指出Godel计数满足对任意单变量命题函数($F(x)$)，存在($n$)使($F(n)$)的Godel数等于($n$)本身（这大概暗示了Godel计数超常的一面）。即对任意($F(x)$)存在($n$)使得(0)($$n = GN(F(n))$$)The diagonal lemma states that the Godel numbering is such that for any propositional function F(x) of one variable, there exists a number n such that the Godel number of F(n), the proposition we get when we plug n into the function F(x), turns out to be n itself. (That there must exist such a number for each F(x) may suggest what superhuman efforts went into the Godel numbering.) In other words, the diagonal lemma asserts that for any F(x) there is an n such that
被称为对角引理是因为($n$)对应的点正好在($y = GN(F(x))$)的对角线上，即($y = x$)上。The number you get out is the same number you started with, and so the special n associated with a given F corresponds precisely to where the graph of y = GN(F(x)) intersects the diagonal, the graph of y = x, namely where x = n. Hence the name, the "diagonal lemma."
（注意：($n = GN(F(n))$)是元语言，它是一个“普通声明”，既不是形式上的声明（formal statement），在左侧的($n$)是自然数，而在右侧的是形式系统中给出($n$)，即出现了($n$)次($s$)的$s(s(s(...s(s(0)))))$。）(N.B. The statement n = GN(F(n)) is in the metalanguage. It's a "normal statement" (i.e., not a formal statement) and n on the left denotes a (normal)natural number. However, the n on the right represents the expression in the formal system that represents the number n, namely s(s(s( . . . s(s(0))))), with n occurrences of s.)
注意对角引理得到对应于命题函数($F(x)$)的($n$)本身满足属性($F$)。大致上相当于($这句话满足F$)，其中可以看到自引用的意思。Notice that the number n that the diagonal lemma associates with the propositional function F(x) is such that the proposition with Godel number n (namely F(n)) says that n itself has the property F. It is, roughly speaking, of the form; this very sentence is F. Soft whispers of selfreferentiality are hovering in the hushed air.
再回到($Pr$)。一个数满足($Pr$)当且仅当它对应的命题可证，即：Now let's go back to that stupendous property that Godel produced, Pr, which is true of all and only the Godel numbers of the theorems, the provable wffs, of the system. A number will have the arithmetical property Pr if and only if it corresponds to a provable proposition under the Godel numbering. In other words:
($$Pr(GN(p))当且仅当p可证$$)Pr(GN(p)) if and only if p is provable.
在其中的元语法（非算术）的意义上，对属性($$\text{~}Pr(x)$$)We have the metasyntactic sense of what Pr(x) means (though not what its arithmetical meaning is; you just have my assurance that it has an arithmetical meaning). Now let's look at the property:
这个属性为真当且仅当对应的命题不可证，即：This second property will be true of all and only the Godel numbers of non theorems; that is, it is true of the Godel numbers of objects that are not propositions provable in the system. In other words:
(1)($$\text{~}Pr(GN(p))当且仅当p不可证$$)~Pr(GN(p)) if and only if p is not provable (1)
(1)是一个元数学上的声明，既不是一个形式系统中的命题又不是算术表达式。单通过它我们可以将元数学上的声明转入到算术表达式中。What kind of sentence is (1)? It is a metamathematical sentence. It's not itself a sentence of the formal system, nor an arithmetical sentence. But by means of (1) we can transform some metamathematical sentences into arithmetical sentences.
现在将对角引理用于($F(x) = \text{~}Pr(x)$)中，我们得到一个($n$)满足($n = GN(F(n))$)，我们称这个($n$)为($g$)，即：(2)($$g = GN(\text{~}Pr(g))$$)Now the diagonal lemma concerns any prepositional function F(x), so let's apply it to F(x) = ~Pr(x). The diagonal lemma, remember, states that for any propositional function F(x) of one variable, there exists a number n that is the Godel number of the very proposition we get when we plug n itself into the function. We're now considering the propositional function ~Pr. According to the diagonal lemma there is some number, let's call it g, such that:
即($g$)不满足($Pr$)。We arrived at (2) by replacing F by ~Pr and n by g in (0). Equation (2) says that g is the Godel number of the proposition that states that the number g lacks the arithmetical property Pr (which belongs to all and only those numbers which are Godel numbers of provable propositions).
现在构造命题($G$)，令(3)($$G = \text{~}Pr(g)$$)Now we're ready to frame our proposition G. Let
($G$)表示数字($g$)不满足($Pr$)，通过(2)(3)有($$GN(G) = g$$)The proposition G states that the number g lacks the property Pr. Moreover, by (2) and (3), we have that:
回到(1)并作一些替换，有：Now we go back to (1) and make some substitutions. Here's (1) again:
($$\text{~}Pr(GN(p))当且仅当p不可证$$)~Pr(GN(p)) if and only if p is not provable
对(1)，令($p = G$)，又($GN(G) = g$)，有：Letting p = G in (1), and using the fact that GN(G) = g, we obtain:
(4)($$\text{~}Pr(g)当且仅当G不可证$$)~Pr(g) if and only if G is not provable (4)
因为(3)，我们得到($G当且仅当G不可证$)。That is, using again (3), G if and only if G is not provable. What (4) is saying is that G is true if and only if G is not provable!
($G$)是一个纯算术声明，同时又描述了它本身的不可证性。它为假时会引出矛盾，所以除非系统不一致，这样所有命题包括矛盾都可证，不然它只能为真。而系统一致是前提，所以($G$)即为真且不可证。我们没有通过推导证明它为真，而是在系统外证明了其不可证性而得到它为真。G is, of course, a purely arithmetical statement, but it's also simultaneously talking about itself, and what it's saying is that it's not provable. Is what it's saying true? Well, it could hardly be false since then it would have to be provable and hence true anyway. That is, unless, of course, the formal system of arithmetic is inconsistent, so that all its propositions would be provable, even contradictions. This is the point in the proof where that presumption of the consistency of the formal system is being called upon to stand up and deliver. And it does. G is both unprovable and, given that that's what it says, it's also true. We haven't shown that it's true by finding a proof for it within the formal system, using the purely mechanical rules of that system, that is, by deducing it. Rather, we've shown it's true by, ironically, going outside the system and showing that no proof for it can be produced within the formal system. We've shown that G is true by showing that it can't be proved, just as it says.
此外，Godel实际上给出了不只针对算术系统的而是所有含算术的形式系统的为真而不可证命题的构造方法。所以如果试图通过增加公理而绕开Godel不完备性定义，新的形式系统下仍然可构造出新的有问题的命题。也就是对任一包含基本算术的一致的形式系统都含为真而不可证的命题。Moreover, Godel in fact showed how to construct a true but unprovable proposition, not just for the formal system of arithmetic we have been discussing but for any formal system whatsoever containing arithmetic. So if we should try to weasel our way out of Godel's first incompleteness theorem by constructing a new formal system that has G appended as an axiom, a new problematic proposition can be constructed for that system. And so on, ad infinitum. There are provably unprovable but nonetheless true propositions in any formal system that contains elementary arithmetic, assuming that system to be consistent.
而这个就是Godel第一不完备性定理。And that is Godel's first incompleteness theorem.
回应 20130908 22:55 
The first of these problem revolving around Cantor's continuum hypothesis. What is Cantor's continuum hypothesis? The great nineteenthcentury mathematician Georg Cantor had proved that (roughly speaking) there are more real numbers than there are natural numbers, even though there are an infinite number of both. Cantor showed, by means of an elegant argument called the "diagonal argument&quo..;.
20130805 10:25
The first of these problem revolving around Cantor's continuum hypothesis. What is Cantor's continuum hypothesis? The great nineteenthcentury mathematician Georg Cantor had proved that (roughly speaking) there are more real numbers than there are natural numbers, even though there are an infinite number of both. Cantor showed, by means of an elegant argument called the "diagonal argument", that in the infinite pairing of one natural number with one real number, every natural number will be paired with a real number but some real number or other will forever be left out. The set of real numbers is thus of a higher ordinality (roughly speaking, there are more of them) than the set of natural numbers. Cantor hypothesized that there is no infinite set that intervenes between the set of natural numbers and the set of real numbers; that is, there is no set that has higher ordinality than the natural numbers and a lower ordinality than the real numbers. This is Cantor's continuum hypothesis and Hilbert's first problem was to prove Cantor's continuum hypothesis true. Gödel was to contribute to the solution to this problem, though not in a way that Hilbert welcomed. Gödel, together with Paul Cohen, proved that the continuum hypothesis can be proved neither true nor false within curren set theory. In other words the status of the continuum hypothesis is what Hilbert claimed there could not be: an ignoramibusa claim that can neither be confirmed nor discredited, a claim about which we remain ignorant.
回应 20130805 10:25 
More specifically, Einstein's and Gรถdel's meta convictions were addressed to the question of whether their respective fields are descriptions of an objective realityexisting independent of our thinking of itor, rather, are subjective human projection, socially shared intellectual constructs.
20130804 14:18
More specifically, Einstein's and Gödel's meta convictions were addressed to the question of whether their respective fields are descriptions of an objective realityexisting independent of our thinking of itor, rather, are subjective human projection, socially shared intellectual constructs.
回应 20130804 14:18

More specifically, Einstein's and Gรถdel's meta convictions were addressed to the question of whether their respective fields are descriptions of an objective realityexisting independent of our thinking of itor, rather, are subjective human projection, socially shared intellectual constructs.
20130804 14:18
More specifically, Einstein's and Gödel's meta convictions were addressed to the question of whether their respective fields are descriptions of an objective realityexisting independent of our thinking of itor, rather, are subjective human projection, socially shared intellectual constructs.
回应 20130804 14:18 
The first of these problem revolving around Cantor's continuum hypothesis. What is Cantor's continuum hypothesis? The great nineteenthcentury mathematician Georg Cantor had proved that (roughly speaking) there are more real numbers than there are natural numbers, even though there are an infinite number of both. Cantor showed, by means of an elegant argument called the "diagonal argument&quo..;.
20130805 10:25
The first of these problem revolving around Cantor's continuum hypothesis. What is Cantor's continuum hypothesis? The great nineteenthcentury mathematician Georg Cantor had proved that (roughly speaking) there are more real numbers than there are natural numbers, even though there are an infinite number of both. Cantor showed, by means of an elegant argument called the "diagonal argument", that in the infinite pairing of one natural number with one real number, every natural number will be paired with a real number but some real number or other will forever be left out. The set of real numbers is thus of a higher ordinality (roughly speaking, there are more of them) than the set of natural numbers. Cantor hypothesized that there is no infinite set that intervenes between the set of natural numbers and the set of real numbers; that is, there is no set that has higher ordinality than the natural numbers and a lower ordinality than the real numbers. This is Cantor's continuum hypothesis and Hilbert's first problem was to prove Cantor's continuum hypothesis true. Gödel was to contribute to the solution to this problem, though not in a way that Hilbert welcomed. Gödel, together with Paul Cohen, proved that the continuum hypothesis can be proved neither true nor false within curren set theory. In other words the status of the continuum hypothesis is what Hilbert claimed there could not be: an ignoramibusa claim that can neither be confirmed nor discredited, a claim about which we remain ignorant.
回应 20130805 10:25 
The first Godel's incompleteness theorem的证明的部分翻译： The First Incompleteness Theorem: The Overall Strategy The twentyodd pages of Godel's famous proof are densely compact. There are 46 preliminary definitions. There are also preliminary theorems that must be proved before the main event can take place: the construction of an arithmetical proposition that is both true and unprovable w...
20130908 22:55
The first Godel's incompleteness theorem的证明的部分翻译：The First Incompleteness Theorem: The Overall Strategy
The twentyodd pages of Godel's famous proof are densely compact. There are 46 preliminary definitions. There are also preliminary theorems that must be proved before the main event can take place: the construction of an arithmetical proposition that is both true and unprovable within the formal system under consideration. The lines of reasoning in the proof are highly compressed, composed of a hierarchy of interconnected levels of discourse, the blended voices of the symphony.
尽管细节很复杂，整体策略却非常简单。就像任何用到自我矛盾的证明，证明一个算术命题正确而又不可证明的策略简单而又奇怪。其中最神奇的部分是证明中与自引用矛盾的结合。证明中最有趣的部分类似于最古老的悖论，the liar's paradox。Though the details of the proof are difficult, the overall strategy is—happily!—almost simplicity itself. Simple but strange, as one would expect of a proof that draws so close to the edge of selfcontradiction, proving that there are true arithmetical propositions that are not provable. One of the strangest things of all about the proof is that it coopts the very structure of selfreferential paradoxes, those abominations to reason, and reshapes that structure to its own ends. The overall strategy of the proof—the delightfully accessible part of the proof—can be grasped in the context of the oldest known paradox of all, the liar's paradox. We can convey the gist of the proof in a breezy, easy way, which we will now proceed to do. Then in the next few sections we will concentrate on filling in a few more of the details, indicating how the hard work gets done.
By tradition, the liar's paradox is attributed to the Cretan Epimenides, who reputedly said something implying: All Cretans are liars. This sentence, in itself, isn't paradoxical, except insofar as it suggests that what Epimenides was saying was something like this:
($这个命题是假的。$)This very sentence is false.
问题在于上面的命题是真的只有在它为假的时候。而Godel的策略是使用一个类似的命题：Now that sentence, as we've already seen, is true if and only if it's false—not a good situation, logically speaking. Godel's strategy involves considering an analogue to that paradoxical sentence, viz. the proposition:
($这个命题在这个系统中不可证。$)This very statement is not provable within this system.
令它为($G$)。尽管像所有自引用命题一样奇怪，却不像之前的命题，($G$)不是一个悖论。Let's call this sentence G. G, unlike its analogue, isn't paradoxical, though it is, like all selfreferential propositions, somewhat strange. (Even the nonparadoxical selfreferential This very statement is true is mystifyingly strange. What's it saying? Where's its content?)
通过后面称为Godel计数的编码系统，($G$)可以转为算术符，所以它也可以看作是个算术命题，这个将在后面提到，是比较复杂的部分。Godel找到了一个算术和本身形式化相结合的方法，($G$)同时包含了两个方面，一是它本身算术上的声明，二同时断定了自己的不可证性。换句话说，除了直观的算术内容（尽管是非常奇怪的），($G$)同时意味着：Through the system of encoding we have come to call "Godel numbering" (of course selfeffacing Godel didn't name it so) G can be rendered in arithmetical notation, so that it also makes an arithmetical statement. Here is one of the places where the hard work comes in, and a bit later on in this chapter we'll dip a little deeper into this aspect of the proof. Godel found an ingenious way of making an arithmetical language speak of its own formalism. The upshot of the technique is that G is simultaneously making two different statements, asserting an arithmetical claim and also asserting its own unprovability. In other words, what G has to say, in addition to its straightforward arithmetical content (it's going to be a weird arithmetical proposition, what with all the fiddle faddling that gets us to it) is:
($G$)在系统中不可证。而($G$)的反是：($G$)在系统中可证。G is improvable in the system. The negation of G thus amounts to the proposition: G is provable in the system.
如果($G$)是可证的，它的反即为真，($G$)即为假。而如果($G$)可证，($G$)又是真的。所以，在假定系统一致的前提下（因为不一致的系统所有命题皆可证），G可证引出矛盾，所以在一致的系统中($G$)不可证，而这就是($G$)命题本身：即($G$)不可证，所以($G$)是真的。这样，($G$)即为真又不可证，而这就Godel的著名结论，在一致的系统中存在为真而不可证的命题。而因为($G$)同时有一个直观的对应的算术意义，Godel的证明显示了在一致的形式系统中存在一些算术真命题不可证（如($G$)），也就是说形式系统要么不一致要么不完备。If G were provable then its negation—which, after all, says that G is provable—would be true. But if the negation of a proposition is true, then the proposition itself is false. So if G is provable then it is false. But if G is provable, then it is also true. After all, what else does a proof show, assuming of course that the system is consistent (since in an inconsistent system all propositions are provable). So, assuming the consistency of the system, if G is provable then it is both true and false—a contradiction—which means that G is not provable. Thus if the system is consistent, then G is not provable in it. But that is exactly what G says: that it isn't provable. So G is true. Therefore, G is both unprovable and true, which is precisely the famous conclusion of Godel's proof, that there is a true but unprovable proposition expressible in the system if the system is consistent. And because G also has a straightforwardly arithmetical meaning which, of course, is true if G is true (because it is G) Godel's proof shows that there are arithmetical truths (for example, G!) that cannot be proved within the formal system, assuming the system to be consistent. The formal system is either inconsistent or incomplete.
更重要的是，证明同时显示了在我们将($G$)作为公理加入到形式系统之后，我们可以构造一个相应的新的($G$)，也就是说新的形式系统仍然是不完备的。结论是，在任何一致的包含基础算术的形式系统中，存在被证明的不可证却为真的命题。一个复杂到包含基本算术的系统不能同时一致和完备。后面是细节。What is more, the proof demonstrates that should we try to remedy the incompleteness by explicitly adding G on as an axiom, thus creating a new, expanded formal system, then a counterpart to G can be constructed within that expanded system that is true but unprovable in the expanded system. The conclusion: There are provably unprovable, but nevertheless true, propositions in any formal system that contains elementary arithmetic, assuming that system to be consistent. A system rich enough to contain arithmetic cannot be both consistent and complete. That's really the overall strategy. In some sense (once one assimilates the strange idea of a single proposition that can speak simultaneously of itself and of arithmetic), it is simple. Of course, the devil is all in the details; and it's to the diabolical details that we will now turn.
第一步：展开形式系统Step One: Lay Out a Formal System
Godel的形式系统包含了一个字符表，将这些符号结合成命题的规则，一组被称为公理的命题和一套推导系统。Godel begins his proof by laying out his formal system, which consists, as do all formal systems, of an alphabet of symbols, rules for combining these symbols into wffs, a special set of wffs called the "axioms," and a deductive apparatus for deriving (as "logical consequences") wffs from other wffs that must be either axioms or consequences of axioms.
大多形式逻辑系统有“且”、“或”、“意味”和“当且仅当”这样的逻辑表达式，同时一些系统还有像“所有”和“一些”这样的量词。而一些逻辑符号可以用其它的取代从而得到一个尽可能简单的系统。如“p意味着q”相当于“非p且q”。经过取代，我们通过含九个基本概念和相应符号的形式系统表达算术。In most systems of formal logic, it is convenient to have symbols for "and"(conjunction) and "or" (disjunction), as well as for the expressions "if... then ..." (material implication) and ". . . if and only if. ..". There are also symbols that express the quantificational notions of "all" and "some." However, it will be more convenient to have as few basic symbols as possible. We can eliminate conjunctions in favor of disjunctions since "p and q" means the same thing as "it's not the case that p is false or q is false." So I want to eat and I want to be thin is equivalent to It's not true that either I don't want to eat or don't want to he thin. Then we can take our elimination one step further since disjunction can be eliminated in favor of material implication because "if p, then q" means the same thing as "not p or q" We can also eliminate the notion of "some," by using the notion of "all" since "there are some x's that are F" is the same as "it is not the case that all x's are not i." So Some logicians are rational is equivalent to Not all logicians are irrational. After our eliminations, we're left with nine primitive concepts, and corresponding symbols, with which to express all of arithmetic in a formal system.
第二步：Godel计数Step Two: Godel Numbering
下一步是设计一种将不同的数字赋给系统中每一个命题的方法。通过这样的赋值，算术声明同时是元数学上的一个声明。The next step in the proof is to devise a mechanical method of assigning a unique number to every proposition of the system. It's by assigning these numbers that the blending of the voices is accomplished, with arithmetical statements also making metamathematical statements.
逻辑学家Simon Kochen通过Kafka（which Godel happened to admire）的工作向我解释了Godel的证明。在Kafka和Godel的世界里都有一个类似于AliceinWonderland的感觉，一种进入了一个奇怪的，所有东西，包括意义本身，都对应进入别的东西的世界里的感觉。这里是基本思想：The logician Simon Kochen beautifully described Godel's proof to me as bearing a marked similarity to Kafka's work (which Godel happened to admire). In both Kafka and Godel, there is a certain AliceinWonderland quality, a sense that one has entered a strange universe where things morph into others, including meanings themselves. Yet everything proceeds stepwise according to the most rigorous rulebound logic. (The rigorous logic of Kafka is underappreciated.) So much of the work in Godel's proof amounts, in Kochen's words, to "bookkeeping." This double aspect of the proof mirrors something, Kochen also said, essential about Godel's mind as well, the wild leaps of imagination coupled with a sort of legalistic ploddingness. Both of these aspects emerge in the Godel numbering. Here's the basic idea:
形式系统包含一系列的东西：字符表，结合字符表到命题和一串命题（即证明）。一切都是由基本字符组成：一个命题是一串符号，而一个证明是一串命题（结论是该串的最后一个命题）。The formal system, remember, involves a variety of types of objects: the symbols of the alphabet, the combinations of symbols into wffs, and special sequences of wffs (in other words, proofs). Everything is built out of the basic symbols of the alphabet: a wff is a sequence of these symbols, and a proof is a sequence of wffs (with the conclusion simply the last entry in the sequence).
因此，Godel计数首先给每一个基本符号分配了一个数字。之后依据组合的形式，继续给每一条命题分配数字。最后相应的给每个证明分配数字。The Godel numbering thus begins by assigning each primitive symbol of the alphabet a number. Once each of the primitive symbols has a number, one continues with a rule for assigning numbers to the wffs themselves, based on the corresponding numbers of their constituents. Then, once we have a Godel number for each wff, the Godel numbering is completed with a rule for assigning numbers to sequences of wffs, which, of course, are what proofs are.
此外，当每一个命题被赋值以后，我们可以仅仅通过数值上的算术关系分析命题间的结构关系，或相反。如当相应数字算术上有某种特定的关系时，其中的一条命题可以正好为另一条的结论。换句话说，形式系统中可表达的算术关系和元描述上通过命题表达的逻辑关系变得互相对应了，These metastatements are purely syntactic, as they are simply the consequences of the syntax of the formal system, that is, its rules.（而因为只是形式系统中语法规则的使用结果，其中的元描述又是纯语法上的？）Furthermore, once every wff has been assigned a corresponding number, we will be able to analyze the structural relationships between the propositions by merely analyzing the arithmetical relationships between their corresponding numbers. Or vice verse. For example, one wff will be a consequence of another one precisely in case the Godel numbers of the wffs are arithmetically related to each other in just the right way. In other words, two different sorts of descriptions will be collapsed into one another: arithmetical descriptions, setting forth relationships between numbers that are expressible within the formal system; and metadescriptions about the logical relationships holding between the wffs in the system. These metastatements are purely syntactic, as they are simply the consequences of the syntax of the formal system, that is, its rules.
Godel计数的思想本质上就是编码。The idea of Godel numbering is basically the idea of encoding, which allows you to move back and forth between the original propositions and the code. In elementary school, my friends and I had a similar code we'd use to pass notes in class, assigning each letter of the alphabet a number between 1 and 26, with "A" assigned 1, "B" assigned 2, etc. "Meet me" was rendered as: 13 5 5 20 13 5.
而Godel的编码系统要确保的是同一数字不会被赋给不同的东西，如赋给一个命题或一个证明。编码规则给了我们一个从命题或证明到唯一的数字的一个算法，当然也有一个逆算法。The Godel numbering must obey one further condition: the translation of syntactic descriptions of the logical relationships between wffs in the system into arithmetical propositions that it provides must be such that these arithmetical propositions are themselves expressible within the system.（Godel计数的另一个要求是翻译结果算术上必须可表述？）The encoding system Godel used had to ensure that the same Godel number wouldn't be assigned to different things, say to both some wff as well as to a sequence of wffs (a proof). The rules for encoding give us an algorithm (which is, remember, a set of rules which tell us, at each step, how to proceed, often based on the result we get from a previous application of rules in the set) for getting from any wff, or sequence of wffs, to a unique Godel number. There is also an algorithm for the reverse process: given any Godel number, we can effectively figure out what formal object in the system it stands for. The Godel numbering must obey one further condition: the translation of syntactic descriptions of the logical relationships between wffs in the system into arithmetical propositions that it provides must be such that these arithmetical propositions are themselves expressible within the system.
类比于日常的编码系统，Godel的系统使用的是质数的指数乘积并依赖于质因数分解理论。而这里例举的是简化的编码方式。The spirit of Godel numbering can be conveyed simply, though were we to be rigorous, as Godel of course was, there would be nothing simple about the encoding. The modern positional notation is so familiar to us that we forget it is itself a coding system, requiring proof in the formal system. So, for example, the usual digital symbol 365 is shorthand for 3 times 10 squared, plus six times 10, plus five. Godel's system of encoding used the exponential products of prime numbers and relied on the prime factorization theorem which states that every number can be uniquely factored into the product of primes. The prime factorization theorem ensured that there was an algorithm for getting from any wff or sequence of wffs to a Godel number and vice verse. The digit juxtaposition we use below would, if made rigorous, be every bit as complicated as the system that Godel used. But we won't be rigorous.
首先，我们任意的赋自然数给形式系统中的每个符号：First, we'll arbitrarily assign a natural number to each symbol of the alphabet of the formal system. We can do all we need to do in setting out a formal system of arithmetic if we restrict ourselves to just nine symbols, to each of which we'll assign a Godel number:
量词“所有”由括号和变量表示，如($(x)F(x)$)表示所有($x$)满足($F$)。角分符号用于新的变量：($x$)，($x'$)，($x''$)，($x'''$)等。另外因为($0$)符号和后继符号，我们有了所有的自然数。The quantificational notion of "all" is represented by using parentheses and variables. So, for example, (x)F(x) means: all x's are F. The prime allows us to generate additional variables: x, x', x'', x''' etc. Since we have a symbol for 0, and a way of indicating successors, we have a way of indicating all the natural numbers.
现在我们给出尽可能简单的赋值的规则，只是把Godel数字嵌入到到命题之中。We now specify a rule for assigning Godel numbers to wffs, which of course are just sequences of the symbols of the alphabet. We adopt the easiest rule possible, reminiscent of the encoding my friends and I used in elementary school. We simply plug in the Godel number for each symbol in the wff and that will be the Godel number for the wff.
考虑定理($P_1$)：($$(x)(x')((s(x) = s(x')) \rightarrow (x = x'))$$)So consider this wff:
假设我们讨论的是自然数，($p_1$)代表如果两个数字有相同的后继，那么他们相等。Assuming our universe of discourse (the objects to which the variables are interpreted to be referring) is the natural numbers, what P1 says is that if two numbers have the same successor, then they're the samenumber. Or, in other words, that one number can't be the successor of two different numbers. More literally: for all x and for all x', if the successor of x is identical to the successor of x, then x is identical to x.
现在依次将其中的符号替换为数值，开括号替换为7，($x$)为3，闭括号8，等等，我们得到了相应的Godel数。令($p$)的Godel数表示为($GN(p)$)，我们得到：($$GN(p_1) = 738739877673846739882734398$$)Now we're going to turn this wff into a number by just consecutively going along and replacing each symbol in the wff by its Godel number. Every symbol in the formula P1 has been assigned a number: the open parenthesis a 7, the x a 3, the close parenthesis an 8, the tilde a 1. Replacing each element of the formula with the corresponding Godel number yields a large number, which is the Godel number for the wff. Abbreviating "the Godel number of the proposition p" by GN(p),we obtain:
我们用0分割定理。In this way Godel numbers are assigned to wffs, which are sequences of symbols, and hence to propositions, which are just special wffs. In the same way, Godel numbers can be assigned to sequences of propositions, and in particular to potential proofs, which are, after all, just sequences of propositions, using the Godel numbers already assigned to propositions. Bookkeeping! In our simplified version, the Godel number of a sequence of propositions (a potential proof) is obtained basically by putting the Godel numbers of the sequenced propositions together; however, since it is important to be able to unambiguously extract from the number obtained the original sequence of propositions, we'll need some sort of signal that will indicate where one proposition ends and the next one begins—sort of like a carriage return on a typewriter. We'll let 0 function as our carriage return, indicating that we now go to a new line in the proof.
如在某个定理串中($p_1$)在($p_2$)后面，而($p_2$)定义为：($$s(0) = s(0)$$)So, let us say that in a particular sequence of propositions, p1 is followed by p2, where p2 is defined as:
Godel数为($$GN(p_1 p_2) = 7387398776738467398827343980675846758$$)The Godel number that will correspond to the sequence of P1 followed by p2 is
这样所有形式系统中逻辑关系变成了算术上可表达的。如，若($wff_1$)逻辑上导出($wff_2$)，($GN(wff_1)$)和($GN(wff_2)$)既有特定的纯算术上的关系。Through Godel's inspired contrivances, all of the logical relations that hold between propositions in the formal system become arithmetic relations expressible in the arithmetical language of the system itself. This is the essence of the heartstopping beauty of the whole thing. So if, for example, wff1 logically entails wff2, then GN(wff1) will bear some purely arithmetical relation to GN(wff2). Suppose, say, that it can be shown that if wff1 logically entails wff2, then GN(wff2) is a factor of GN(wff1). We would then have two ways of showing that wff1 logically entails wff2: we could use the rules of the formal system to deduce wff2 from wff1 or we could show that GN(wff1) can be obtained from GN(wff2) by multiplying by an integer. Suppose that GN(wff1) = 195589 and GN(wff2) = 317. 317 is a factor of 195589, since 317 multiplied by 617 = 195589. So that wff1 logically entails wff2 could be demonstrated either by using the formal rules of proof to arrive at wff2 from wff1 or, alternatively, by using the rules of arithmetic to arrive at GN(wff1) = 195589 by multiplying 617 by 317 = GN(wff2). The metasyntactic and the arithmetic collapse into one another.
一旦清楚了算术和逻辑之间的关系，逻辑证明在系统中就有了可表达的算术属性。而推导这些算术属性就相当于前段所讲的转换的结果。比如系统中合法证明得到的命题的Godel数就会有特定的算术属性，比如奇偶或者指数成方之类或更可能的远比此复杂的属性。换句话说，可证性变成了一种算术关系。这样，我们就得到了一种同时包含其自身在系统中可证性信息的在系统中可表达的算术定理。Once one has this sort of collapse between logical implication and arithmetical relationship, we can go on and demonstrate that certain sequences of wffs—precisely those that constitute proofs—have an arithmetical property expressible in the system. Proofs, of course, are built up out of logical entailments. So deriving this arithmetical property (of the Godel numbers of all and only the proofs in the system) is going to be a consequence of the sort of collapse discussed in the previous paragraph. The Godel number of those strings of wffs that are valid proofs within the system will have some sort of arithmetical property, say, they'll all be even or they'll all be odd or they'll be prime numbers or the squares of primes or, more likely, a property a good deal more complicated. In other words, the metasyntactic relationship of provability will become an arithmetical relationship; that a string of wffs is a proof will be some property of numbers. From this it becomes possible to show that all and only the provable wffs in the system, the theorems, have a certain arithmetical property. You can see where we're heading: toward arithmetical propositions expressible in the system that also speak to the issue of their own provability within the system. The Godel numbering allows some propositions to engage in an interesting sort of doublespeak, saying something arithmetical and also commenting on their own situation within the formal system, saying whether they're provable.
这就像戏剧中的角色和其扮演者日常生活中的角色相互影响的关系。The doublespeak of these propositions could be compared to the sort of thing that sometimes happens within a dramatic play, in particular when the play presents actors as characters, with their own "reallife" relationships, and then presents these characters as actors in a play within the play. Through careful contrivance, the lines that the actors speak, in the play within the play, can also be interpreted as having a reallife meaning in their relationships outside the play within the play (in the play proper). Godel's strategy asks us to grasp something analogous to what the country audience in Leoncavallo's opera Pagliacci grasp when they understand the actors to be delivering lines that, as well as making sense within the play, have a meaning in their offstage lives (in the opera). In Godel's inspired stage production, lines speak both to the formal relationships within the system, the play within the play, and also reveal reallife arithmetical relationships. The proposition that Godel's proof constructs, the one that will simultaneously announce both its own (provable) unprovability and a true (unprovable) arithmetical relationship, has the same sort of doubleentendre as Pagliacci's final tragic cry, "La Commedia è finita!"—the comedy is over.
第三部：构造一个因为描述了其不可证性而为真的命题Step Three: Create a Proposition That's True Because It Says That It's Unprovable
之后，Godel给出了一个神奇的算术属性，称为($Pr$)或者“可证明”。它是所有系统中可证命题的Godel数才拥有的纯算术属性。Having established his ingenious layers of meaning, Godel now conjures a rather amazing arithmetical property, which we'll designate as "Pr" for "provable." Because, although Pr is a purely arithmetical property, it's also that very property toward which all the contrivances have been heading. It's an arithmetical property that is true of all and only the Godel numbers of the provable propositions of the system. I choose the verb "conjures" deliberately because even though the collapse of the metasyntactic and arithmetical was heading toward "Pr", there is still a sense of magic about the entrance of Pr.
在继续之前，这里是一些小的技术细节：通过单变量的命题函数代表属性，形如($F(x)$)。当($x$)被定义域中任一值替换后，($F(x)$)才成为了一个或真或假的命题。Before getting to the property, one little technical point about the way in which properties are specified: by propositional functions of one variable. These can be thought of as of the form F(x). These are expressions in the formal system involving a single variable—the x which is a dummy standing for a whole range of possible values (the domain of individuals) that can be plugged in; if you plug in a value for the variable, you end up with a wff that is either true or false, in other words a proposition. F(x), just as it is, is neither true nor false. So say s(x) were to mean: x is the successor of 1. This is neither true nor false; it isn't a proposition, a definite statement, since what it says depends upon what x actually represents. Plugging in 2 for the variable x yields a true proposition, and plugging in anything else yields false propositions. That's how properties are designated in the system, by propositional functions of one variable.
回到($Pr(x)$)，一个比较复杂的算术属性。首先，所有命题都通过Godel计数被赋予了一个数值，即每个($wff_p$)，我们有($GN(p)$)。而定理是系统中所有命题的一个子集，即可证命题。所以，给一个自然数($n$)，它不一定对应于系统中的某个定理，即对($n = GN(p)$)，($p$)不一定可证。Now onward to Pr(x), which is a somewhat complicated property of numbers. Remember, first of all, that each of the wffs in the formal system have been assigned numbers through the wonders of Godel numbering. So for every wff p, we have some GN(p), some natural number or other. The theorems are a special subset of the wffs of the system, the provable propositions. Given any natural number n, then, it may or may not be the case that it corresponds to some theorem in the formal system, that is, it may or may not be the case that n = GN(p) for some proposition p which is a theorem of the formal system.
现在定义($Pr(x)$)。该命题函数的定义域为自然数，对任意自然数($n$)，若对定理($p$)，($n = GN(p)$)，我们称($n$)满足($Pr(x)$)，即($Pr(n) $)为真。Godel证明了该属性不管其复杂度，可通过形式系统中给出。另外通过这个属性，Godel可以同时描述命题是否为定理的属性，并将之转为算术陈述，即“($p$)是个定理”转为“Pr(GN(p))”，称($n$)满足($Pr(x)$)即表示($n$)相应的命题是定理。Now we are in position to define Pr(x). The possible values for this propositional function, the things we plug in for the dummy x, are (the expressions for) the natural numbers. For any natural number n, if n = GN(p) for a theorem p of the system then we say that n satisfies the property Pr(x), that is, that Pr(n) is true. Godel showed that this property is one that can in fact be expressed in the formal system, that is, that it's an example of an F(x). Pr(x) is a formally expressible arithmetical property, albeit one that is extremely complicated, not anything that we can explicitly give here. But by means of this property Godel is able to take metasentences about the system, stating which propositions are theorems of the system, and transform them into arithmetical sentences within the system: "p is a theorem" is transformed into "Pr(GN(p))". To say of some particular n that it has the property Pr(x) is to say that this number corresponds to a theorem in the formal system.
就如奇偶性一样，($n$)满足($Pr(x)$)确实是真的算术属性。Now perhaps you're thinking something like this: That a particular number n has the property Pr(x) isn't a real property of n. The number n, for example, may be even or it may be odd; if it's divisible by 2 then it's even. Let's say it is. Then its evenness is a real arithmetical property; n couldn't be the number it is if it weren't even. In contrast, looking at this property Pr(x) metasystematically, it doesn't seem at all a proper sort of numerical property. A number n has this property only arbitrarily, since the proposition with which n is associated is arbitrary, a consequence merely of the way in which the Godel numbering was set up, the inspired contrivances. True enough, but, arbitrary though it may be, Pr(x) is nonetheless a real arithmetical property, and a number n either will or won't have it. And n wouldn't be the number that it is unless it either did or didn't have it. Just because Pr(x) has a metameaning doesn't detract from its arithmetical character. This property Pr(x) is, in fact, stupendous, and it allows us to take the plunge into the heart of the proof.
接下来用到的是对角引理（diagonal lemma，证明未给出），它的一个特殊形式被用在了Godel的证明中，而这儿为简化证明，使用了它的通用形式。http://en.wikipedia.org/wiki/Diagonal_lemmaWhat we use next is something called the diagonal lemma. It's a general statement, a particular case of which is what we need to prove Godel's theorem. (Godel didn't actually use it, but rather derived the particular case.) Making use of this general lemma (which, of course, we're not going to prove) will simplify matters enormously.
对角引理指出Godel计数满足对任意单变量命题函数($F(x)$)，存在($n$)使($F(n)$)的Godel数等于($n$)本身（这大概暗示了Godel计数超常的一面）。即对任意($F(x)$)存在($n$)使得(0)($$n = GN(F(n))$$)The diagonal lemma states that the Godel numbering is such that for any propositional function F(x) of one variable, there exists a number n such that the Godel number of F(n), the proposition we get when we plug n into the function F(x), turns out to be n itself. (That there must exist such a number for each F(x) may suggest what superhuman efforts went into the Godel numbering.) In other words, the diagonal lemma asserts that for any F(x) there is an n such that
被称为对角引理是因为($n$)对应的点正好在($y = GN(F(x))$)的对角线上，即($y = x$)上。The number you get out is the same number you started with, and so the special n associated with a given F corresponds precisely to where the graph of y = GN(F(x)) intersects the diagonal, the graph of y = x, namely where x = n. Hence the name, the "diagonal lemma."
（注意：($n = GN(F(n))$)是元语言，它是一个“普通声明”，既不是形式上的声明（formal statement），在左侧的($n$)是自然数，而在右侧的是形式系统中给出($n$)，即出现了($n$)次($s$)的$s(s(s(...s(s(0)))))$。）(N.B. The statement n = GN(F(n)) is in the metalanguage. It's a "normal statement" (i.e., not a formal statement) and n on the left denotes a (normal)natural number. However, the n on the right represents the expression in the formal system that represents the number n, namely s(s(s( . . . s(s(0))))), with n occurrences of s.)
注意对角引理得到对应于命题函数($F(x)$)的($n$)本身满足属性($F$)。大致上相当于($这句话满足F$)，其中可以看到自引用的意思。Notice that the number n that the diagonal lemma associates with the propositional function F(x) is such that the proposition with Godel number n (namely F(n)) says that n itself has the property F. It is, roughly speaking, of the form; this very sentence is F. Soft whispers of selfreferentiality are hovering in the hushed air.
再回到($Pr$)。一个数满足($Pr$)当且仅当它对应的命题可证，即：Now let's go back to that stupendous property that Godel produced, Pr, which is true of all and only the Godel numbers of the theorems, the provable wffs, of the system. A number will have the arithmetical property Pr if and only if it corresponds to a provable proposition under the Godel numbering. In other words:
($$Pr(GN(p))当且仅当p可证$$)Pr(GN(p)) if and only if p is provable.
在其中的元语法（非算术）的意义上，对属性($$\text{~}Pr(x)$$)We have the metasyntactic sense of what Pr(x) means (though not what its arithmetical meaning is; you just have my assurance that it has an arithmetical meaning). Now let's look at the property:
这个属性为真当且仅当对应的命题不可证，即：This second property will be true of all and only the Godel numbers of non theorems; that is, it is true of the Godel numbers of objects that are not propositions provable in the system. In other words:
(1)($$\text{~}Pr(GN(p))当且仅当p不可证$$)~Pr(GN(p)) if and only if p is not provable (1)
(1)是一个元数学上的声明，既不是一个形式系统中的命题又不是算术表达式。单通过它我们可以将元数学上的声明转入到算术表达式中。What kind of sentence is (1)? It is a metamathematical sentence. It's not itself a sentence of the formal system, nor an arithmetical sentence. But by means of (1) we can transform some metamathematical sentences into arithmetical sentences.
现在将对角引理用于($F(x) = \text{~}Pr(x)$)中，我们得到一个($n$)满足($n = GN(F(n))$)，我们称这个($n$)为($g$)，即：(2)($$g = GN(\text{~}Pr(g))$$)Now the diagonal lemma concerns any prepositional function F(x), so let's apply it to F(x) = ~Pr(x). The diagonal lemma, remember, states that for any propositional function F(x) of one variable, there exists a number n that is the Godel number of the very proposition we get when we plug n itself into the function. We're now considering the propositional function ~Pr. According to the diagonal lemma there is some number, let's call it g, such that:
即($g$)不满足($Pr$)。We arrived at (2) by replacing F by ~Pr and n by g in (0). Equation (2) says that g is the Godel number of the proposition that states that the number g lacks the arithmetical property Pr (which belongs to all and only those numbers which are Godel numbers of provable propositions).
现在构造命题($G$)，令(3)($$G = \text{~}Pr(g)$$)Now we're ready to frame our proposition G. Let
($G$)表示数字($g$)不满足($Pr$)，通过(2)(3)有($$GN(G) = g$$)The proposition G states that the number g lacks the property Pr. Moreover, by (2) and (3), we have that:
回到(1)并作一些替换，有：Now we go back to (1) and make some substitutions. Here's (1) again:
($$\text{~}Pr(GN(p))当且仅当p不可证$$)~Pr(GN(p)) if and only if p is not provable
对(1)，令($p = G$)，又($GN(G) = g$)，有：Letting p = G in (1), and using the fact that GN(G) = g, we obtain:
(4)($$\text{~}Pr(g)当且仅当G不可证$$)~Pr(g) if and only if G is not provable (4)
因为(3)，我们得到($G当且仅当G不可证$)。That is, using again (3), G if and only if G is not provable. What (4) is saying is that G is true if and only if G is not provable!
($G$)是一个纯算术声明，同时又描述了它本身的不可证性。它为假时会引出矛盾，所以除非系统不一致，这样所有命题包括矛盾都可证，不然它只能为真。而系统一致是前提，所以($G$)即为真且不可证。我们没有通过推导证明它为真，而是在系统外证明了其不可证性而得到它为真。G is, of course, a purely arithmetical statement, but it's also simultaneously talking about itself, and what it's saying is that it's not provable. Is what it's saying true? Well, it could hardly be false since then it would have to be provable and hence true anyway. That is, unless, of course, the formal system of arithmetic is inconsistent, so that all its propositions would be provable, even contradictions. This is the point in the proof where that presumption of the consistency of the formal system is being called upon to stand up and deliver. And it does. G is both unprovable and, given that that's what it says, it's also true. We haven't shown that it's true by finding a proof for it within the formal system, using the purely mechanical rules of that system, that is, by deducing it. Rather, we've shown it's true by, ironically, going outside the system and showing that no proof for it can be produced within the formal system. We've shown that G is true by showing that it can't be proved, just as it says.
此外，Godel实际上给出了不只针对算术系统的而是所有含算术的形式系统的为真而不可证命题的构造方法。所以如果试图通过增加公理而绕开Godel不完备性定义，新的形式系统下仍然可构造出新的有问题的命题。也就是对任一包含基本算术的一致的形式系统都含为真而不可证的命题。Moreover, Godel in fact showed how to construct a true but unprovable proposition, not just for the formal system of arithmetic we have been discussing but for any formal system whatsoever containing arithmetic. So if we should try to weasel our way out of Godel's first incompleteness theorem by constructing a new formal system that has G appended as an axiom, a new problematic proposition can be constructed for that system. And so on, ad infinitum. There are provably unprovable but nonetheless true propositions in any formal system that contains elementary arithmetic, assuming that system to be consistent.
而这个就是Godel第一不完备性定理。And that is Godel's first incompleteness theorem.
回应 20130908 22:55 
The second incompleteness theorem states that the consistency of a formal system that contains arithmetic can't be formally proved within that system. It would seem to follow, pretty straightforwardly, from the first. Remember that the first incompleteness result has the form of a conditional statement: if the formal system of arithmetic is consistent, then G. /ĺ…Źĺź?ĺ†…...
20130909 05:57
($C \rightarrow G$)，($G$)不可证，所以($C$)不可证。The second incompleteness theorem states that the consistency of a formal system that contains arithmetic can't be formally proved within that system. It would seem to follow, pretty straightforwardly, from the first. Remember that the first incompleteness result has the form of a conditional statement: if the formal system of arithmetic is consistent, then G.
回应 20130909 05:57

The second incompleteness theorem states that the consistency of a formal system that contains arithmetic can't be formally proved within that system. It would seem to follow, pretty straightforwardly, from the first. Remember that the first incompleteness result has the form of a conditional statement: if the formal system of arithmetic is consistent, then G. /ĺ…Źĺź?ĺ†…...
20130909 05:57
($C \rightarrow G$)，($G$)不可证，所以($C$)不可证。The second incompleteness theorem states that the consistency of a formal system that contains arithmetic can't be formally proved within that system. It would seem to follow, pretty straightforwardly, from the first. Remember that the first incompleteness result has the form of a conditional statement: if the formal system of arithmetic is consistent, then G.
回应 20130909 05:57 
The first Godel's incompleteness theorem的证明的部分翻译： The First Incompleteness Theorem: The Overall Strategy The twentyodd pages of Godel's famous proof are densely compact. There are 46 preliminary definitions. There are also preliminary theorems that must be proved before the main event can take place: the construction of an arithmetical proposition that is both true and unprovable w...
20130908 22:55
The first Godel's incompleteness theorem的证明的部分翻译：The First Incompleteness Theorem: The Overall Strategy
The twentyodd pages of Godel's famous proof are densely compact. There are 46 preliminary definitions. There are also preliminary theorems that must be proved before the main event can take place: the construction of an arithmetical proposition that is both true and unprovable within the formal system under consideration. The lines of reasoning in the proof are highly compressed, composed of a hierarchy of interconnected levels of discourse, the blended voices of the symphony.
尽管细节很复杂，整体策略却非常简单。就像任何用到自我矛盾的证明，证明一个算术命题正确而又不可证明的策略简单而又奇怪。其中最神奇的部分是证明中与自引用矛盾的结合。证明中最有趣的部分类似于最古老的悖论，the liar's paradox。Though the details of the proof are difficult, the overall strategy is—happily!—almost simplicity itself. Simple but strange, as one would expect of a proof that draws so close to the edge of selfcontradiction, proving that there are true arithmetical propositions that are not provable. One of the strangest things of all about the proof is that it coopts the very structure of selfreferential paradoxes, those abominations to reason, and reshapes that structure to its own ends. The overall strategy of the proof—the delightfully accessible part of the proof—can be grasped in the context of the oldest known paradox of all, the liar's paradox. We can convey the gist of the proof in a breezy, easy way, which we will now proceed to do. Then in the next few sections we will concentrate on filling in a few more of the details, indicating how the hard work gets done.
By tradition, the liar's paradox is attributed to the Cretan Epimenides, who reputedly said something implying: All Cretans are liars. This sentence, in itself, isn't paradoxical, except insofar as it suggests that what Epimenides was saying was something like this:
($这个命题是假的。$)This very sentence is false.
问题在于上面的命题是真的只有在它为假的时候。而Godel的策略是使用一个类似的命题：Now that sentence, as we've already seen, is true if and only if it's false—not a good situation, logically speaking. Godel's strategy involves considering an analogue to that paradoxical sentence, viz. the proposition:
($这个命题在这个系统中不可证。$)This very statement is not provable within this system.
令它为($G$)。尽管像所有自引用命题一样奇怪，却不像之前的命题，($G$)不是一个悖论。Let's call this sentence G. G, unlike its analogue, isn't paradoxical, though it is, like all selfreferential propositions, somewhat strange. (Even the nonparadoxical selfreferential This very statement is true is mystifyingly strange. What's it saying? Where's its content?)
通过后面称为Godel计数的编码系统，($G$)可以转为算术符，所以它也可以看作是个算术命题，这个将在后面提到，是比较复杂的部分。Godel找到了一个算术和本身形式化相结合的方法，($G$)同时包含了两个方面，一是它本身算术上的声明，二同时断定了自己的不可证性。换句话说，除了直观的算术内容（尽管是非常奇怪的），($G$)同时意味着：Through the system of encoding we have come to call "Godel numbering" (of course selfeffacing Godel didn't name it so) G can be rendered in arithmetical notation, so that it also makes an arithmetical statement. Here is one of the places where the hard work comes in, and a bit later on in this chapter we'll dip a little deeper into this aspect of the proof. Godel found an ingenious way of making an arithmetical language speak of its own formalism. The upshot of the technique is that G is simultaneously making two different statements, asserting an arithmetical claim and also asserting its own unprovability. In other words, what G has to say, in addition to its straightforward arithmetical content (it's going to be a weird arithmetical proposition, what with all the fiddle faddling that gets us to it) is:
($G$)在系统中不可证。而($G$)的反是：($G$)在系统中可证。G is improvable in the system. The negation of G thus amounts to the proposition: G is provable in the system.
如果($G$)是可证的，它的反即为真，($G$)即为假。而如果($G$)可证，($G$)又是真的。所以，在假定系统一致的前提下（因为不一致的系统所有命题皆可证），G可证引出矛盾，所以在一致的系统中($G$)不可证，而这就是($G$)命题本身：即($G$)不可证，所以($G$)是真的。这样，($G$)即为真又不可证，而这就Godel的著名结论，在一致的系统中存在为真而不可证的命题。而因为($G$)同时有一个直观的对应的算术意义，Godel的证明显示了在一致的形式系统中存在一些算术真命题不可证（如($G$)），也就是说形式系统要么不一致要么不完备。If G were provable then its negation—which, after all, says that G is provable—would be true. But if the negation of a proposition is true, then the proposition itself is false. So if G is provable then it is false. But if G is provable, then it is also true. After all, what else does a proof show, assuming of course that the system is consistent (since in an inconsistent system all propositions are provable). So, assuming the consistency of the system, if G is provable then it is both true and false—a contradiction—which means that G is not provable. Thus if the system is consistent, then G is not provable in it. But that is exactly what G says: that it isn't provable. So G is true. Therefore, G is both unprovable and true, which is precisely the famous conclusion of Godel's proof, that there is a true but unprovable proposition expressible in the system if the system is consistent. And because G also has a straightforwardly arithmetical meaning which, of course, is true if G is true (because it is G) Godel's proof shows that there are arithmetical truths (for example, G!) that cannot be proved within the formal system, assuming the system to be consistent. The formal system is either inconsistent or incomplete.
更重要的是，证明同时显示了在我们将($G$)作为公理加入到形式系统之后，我们可以构造一个相应的新的($G$)，也就是说新的形式系统仍然是不完备的。结论是，在任何一致的包含基础算术的形式系统中，存在被证明的不可证却为真的命题。一个复杂到包含基本算术的系统不能同时一致和完备。后面是细节。What is more, the proof demonstrates that should we try to remedy the incompleteness by explicitly adding G on as an axiom, thus creating a new, expanded formal system, then a counterpart to G can be constructed within that expanded system that is true but unprovable in the expanded system. The conclusion: There are provably unprovable, but nevertheless true, propositions in any formal system that contains elementary arithmetic, assuming that system to be consistent. A system rich enough to contain arithmetic cannot be both consistent and complete. That's really the overall strategy. In some sense (once one assimilates the strange idea of a single proposition that can speak simultaneously of itself and of arithmetic), it is simple. Of course, the devil is all in the details; and it's to the diabolical details that we will now turn.
第一步：展开形式系统Step One: Lay Out a Formal System
Godel的形式系统包含了一个字符表，将这些符号结合成命题的规则，一组被称为公理的命题和一套推导系统。Godel begins his proof by laying out his formal system, which consists, as do all formal systems, of an alphabet of symbols, rules for combining these symbols into wffs, a special set of wffs called the "axioms," and a deductive apparatus for deriving (as "logical consequences") wffs from other wffs that must be either axioms or consequences of axioms.
大多形式逻辑系统有“且”、“或”、“意味”和“当且仅当”这样的逻辑表达式，同时一些系统还有像“所有”和“一些”这样的量词。而一些逻辑符号可以用其它的取代从而得到一个尽可能简单的系统。如“p意味着q”相当于“非p且q”。经过取代，我们通过含九个基本概念和相应符号的形式系统表达算术。In most systems of formal logic, it is convenient to have symbols for "and"(conjunction) and "or" (disjunction), as well as for the expressions "if... then ..." (material implication) and ". . . if and only if. ..". There are also symbols that express the quantificational notions of "all" and "some." However, it will be more convenient to have as few basic symbols as possible. We can eliminate conjunctions in favor of disjunctions since "p and q" means the same thing as "it's not the case that p is false or q is false." So I want to eat and I want to be thin is equivalent to It's not true that either I don't want to eat or don't want to he thin. Then we can take our elimination one step further since disjunction can be eliminated in favor of material implication because "if p, then q" means the same thing as "not p or q" We can also eliminate the notion of "some," by using the notion of "all" since "there are some x's that are F" is the same as "it is not the case that all x's are not i." So Some logicians are rational is equivalent to Not all logicians are irrational. After our eliminations, we're left with nine primitive concepts, and corresponding symbols, with which to express all of arithmetic in a formal system.
第二步：Godel计数Step Two: Godel Numbering
下一步是设计一种将不同的数字赋给系统中每一个命题的方法。通过这样的赋值，算术声明同时是元数学上的一个声明。The next step in the proof is to devise a mechanical method of assigning a unique number to every proposition of the system. It's by assigning these numbers that the blending of the voices is accomplished, with arithmetical statements also making metamathematical statements.
逻辑学家Simon Kochen通过Kafka（which Godel happened to admire）的工作向我解释了Godel的证明。在Kafka和Godel的世界里都有一个类似于AliceinWonderland的感觉，一种进入了一个奇怪的，所有东西，包括意义本身，都对应进入别的东西的世界里的感觉。这里是基本思想：The logician Simon Kochen beautifully described Godel's proof to me as bearing a marked similarity to Kafka's work (which Godel happened to admire). In both Kafka and Godel, there is a certain AliceinWonderland quality, a sense that one has entered a strange universe where things morph into others, including meanings themselves. Yet everything proceeds stepwise according to the most rigorous rulebound logic. (The rigorous logic of Kafka is underappreciated.) So much of the work in Godel's proof amounts, in Kochen's words, to "bookkeeping." This double aspect of the proof mirrors something, Kochen also said, essential about Godel's mind as well, the wild leaps of imagination coupled with a sort of legalistic ploddingness. Both of these aspects emerge in the Godel numbering. Here's the basic idea:
形式系统包含一系列的东西：字符表，结合字符表到命题和一串命题（即证明）。一切都是由基本字符组成：一个命题是一串符号，而一个证明是一串命题（结论是该串的最后一个命题）。The formal system, remember, involves a variety of types of objects: the symbols of the alphabet, the combinations of symbols into wffs, and special sequences of wffs (in other words, proofs). Everything is built out of the basic symbols of the alphabet: a wff is a sequence of these symbols, and a proof is a sequence of wffs (with the conclusion simply the last entry in the sequence).
因此，Godel计数首先给每一个基本符号分配了一个数字。之后依据组合的形式，继续给每一条命题分配数字。最后相应的给每个证明分配数字。The Godel numbering thus begins by assigning each primitive symbol of the alphabet a number. Once each of the primitive symbols has a number, one continues with a rule for assigning numbers to the wffs themselves, based on the corresponding numbers of their constituents. Then, once we have a Godel number for each wff, the Godel numbering is completed with a rule for assigning numbers to sequences of wffs, which, of course, are what proofs are.
此外，当每一个命题被赋值以后，我们可以仅仅通过数值上的算术关系分析命题间的结构关系，或相反。如当相应数字算术上有某种特定的关系时，其中的一条命题可以正好为另一条的结论。换句话说，形式系统中可表达的算术关系和元描述上通过命题表达的逻辑关系变得互相对应了，These metastatements are purely syntactic, as they are simply the consequences of the syntax of the formal system, that is, its rules.（而因为只是形式系统中语法规则的使用结果，其中的元描述又是纯语法上的？）Furthermore, once every wff has been assigned a corresponding number, we will be able to analyze the structural relationships between the propositions by merely analyzing the arithmetical relationships between their corresponding numbers. Or vice verse. For example, one wff will be a consequence of another one precisely in case the Godel numbers of the wffs are arithmetically related to each other in just the right way. In other words, two different sorts of descriptions will be collapsed into one another: arithmetical descriptions, setting forth relationships between numbers that are expressible within the formal system; and metadescriptions about the logical relationships holding between the wffs in the system. These metastatements are purely syntactic, as they are simply the consequences of the syntax of the formal system, that is, its rules.
Godel计数的思想本质上就是编码。The idea of Godel numbering is basically the idea of encoding, which allows you to move back and forth between the original propositions and the code. In elementary school, my friends and I had a similar code we'd use to pass notes in class, assigning each letter of the alphabet a number between 1 and 26, with "A" assigned 1, "B" assigned 2, etc. "Meet me" was rendered as: 13 5 5 20 13 5.
而Godel的编码系统要确保的是同一数字不会被赋给不同的东西，如赋给一个命题或一个证明。编码规则给了我们一个从命题或证明到唯一的数字的一个算法，当然也有一个逆算法。The Godel numbering must obey one further condition: the translation of syntactic descriptions of the logical relationships between wffs in the system into arithmetical propositions that it provides must be such that these arithmetical propositions are themselves expressible within the system.（Godel计数的另一个要求是翻译结果算术上必须可表述？）The encoding system Godel used had to ensure that the same Godel number wouldn't be assigned to different things, say to both some wff as well as to a sequence of wffs (a proof). The rules for encoding give us an algorithm (which is, remember, a set of rules which tell us, at each step, how to proceed, often based on the result we get from a previous application of rules in the set) for getting from any wff, or sequence of wffs, to a unique Godel number. There is also an algorithm for the reverse process: given any Godel number, we can effectively figure out what formal object in the system it stands for. The Godel numbering must obey one further condition: the translation of syntactic descriptions of the logical relationships between wffs in the system into arithmetical propositions that it provides must be such that these arithmetical propositions are themselves expressible within the system.
类比于日常的编码系统，Godel的系统使用的是质数的指数乘积并依赖于质因数分解理论。而这里例举的是简化的编码方式。The spirit of Godel numbering can be conveyed simply, though were we to be rigorous, as Godel of course was, there would be nothing simple about the encoding. The modern positional notation is so familiar to us that we forget it is itself a coding system, requiring proof in the formal system. So, for example, the usual digital symbol 365 is shorthand for 3 times 10 squared, plus six times 10, plus five. Godel's system of encoding used the exponential products of prime numbers and relied on the prime factorization theorem which states that every number can be uniquely factored into the product of primes. The prime factorization theorem ensured that there was an algorithm for getting from any wff or sequence of wffs to a Godel number and vice verse. The digit juxtaposition we use below would, if made rigorous, be every bit as complicated as the system that Godel used. But we won't be rigorous.
首先，我们任意的赋自然数给形式系统中的每个符号：First, we'll arbitrarily assign a natural number to each symbol of the alphabet of the formal system. We can do all we need to do in setting out a formal system of arithmetic if we restrict ourselves to just nine symbols, to each of which we'll assign a Godel number:
量词“所有”由括号和变量表示，如($(x)F(x)$)表示所有($x$)满足($F$)。角分符号用于新的变量：($x$)，($x'$)，($x''$)，($x'''$)等。另外因为($0$)符号和后继符号，我们有了所有的自然数。The quantificational notion of "all" is represented by using parentheses and variables. So, for example, (x)F(x) means: all x's are F. The prime allows us to generate additional variables: x, x', x'', x''' etc. Since we have a symbol for 0, and a way of indicating successors, we have a way of indicating all the natural numbers.
现在我们给出尽可能简单的赋值的规则，只是把Godel数字嵌入到到命题之中。We now specify a rule for assigning Godel numbers to wffs, which of course are just sequences of the symbols of the alphabet. We adopt the easiest rule possible, reminiscent of the encoding my friends and I used in elementary school. We simply plug in the Godel number for each symbol in the wff and that will be the Godel number for the wff.
考虑定理($P_1$)：($$(x)(x')((s(x) = s(x')) \rightarrow (x = x'))$$)So consider this wff:
假设我们讨论的是自然数，($p_1$)代表如果两个数字有相同的后继，那么他们相等。Assuming our universe of discourse (the objects to which the variables are interpreted to be referring) is the natural numbers, what P1 says is that if two numbers have the same successor, then they're the samenumber. Or, in other words, that one number can't be the successor of two different numbers. More literally: for all x and for all x', if the successor of x is identical to the successor of x, then x is identical to x.
现在依次将其中的符号替换为数值，开括号替换为7，($x$)为3，闭括号8，等等，我们得到了相应的Godel数。令($p$)的Godel数表示为($GN(p)$)，我们得到：($$GN(p_1) = 738739877673846739882734398$$)Now we're going to turn this wff into a number by just consecutively going along and replacing each symbol in the wff by its Godel number. Every symbol in the formula P1 has been assigned a number: the open parenthesis a 7, the x a 3, the close parenthesis an 8, the tilde a 1. Replacing each element of the formula with the corresponding Godel number yields a large number, which is the Godel number for the wff. Abbreviating "the Godel number of the proposition p" by GN(p),we obtain:
我们用0分割定理。In this way Godel numbers are assigned to wffs, which are sequences of symbols, and hence to propositions, which are just special wffs. In the same way, Godel numbers can be assigned to sequences of propositions, and in particular to potential proofs, which are, after all, just sequences of propositions, using the Godel numbers already assigned to propositions. Bookkeeping! In our simplified version, the Godel number of a sequence of propositions (a potential proof) is obtained basically by putting the Godel numbers of the sequenced propositions together; however, since it is important to be able to unambiguously extract from the number obtained the original sequence of propositions, we'll need some sort of signal that will indicate where one proposition ends and the next one begins—sort of like a carriage return on a typewriter. We'll let 0 function as our carriage return, indicating that we now go to a new line in the proof.
如在某个定理串中($p_1$)在($p_2$)后面，而($p_2$)定义为：($$s(0) = s(0)$$)So, let us say that in a particular sequence of propositions, p1 is followed by p2, where p2 is defined as:
Godel数为($$GN(p_1 p_2) = 7387398776738467398827343980675846758$$)The Godel number that will correspond to the sequence of P1 followed by p2 is
这样所有形式系统中逻辑关系变成了算术上可表达的。如，若($wff_1$)逻辑上导出($wff_2$)，($GN(wff_1)$)和($GN(wff_2)$)既有特定的纯算术上的关系。Through Godel's inspired contrivances, all of the logical relations that hold between propositions in the formal system become arithmetic relations expressible in the arithmetical language of the system itself. This is the essence of the heartstopping beauty of the whole thing. So if, for example, wff1 logically entails wff2, then GN(wff1) will bear some purely arithmetical relation to GN(wff2). Suppose, say, that it can be shown that if wff1 logically entails wff2, then GN(wff2) is a factor of GN(wff1). We would then have two ways of showing that wff1 logically entails wff2: we could use the rules of the formal system to deduce wff2 from wff1 or we could show that GN(wff1) can be obtained from GN(wff2) by multiplying by an integer. Suppose that GN(wff1) = 195589 and GN(wff2) = 317. 317 is a factor of 195589, since 317 multiplied by 617 = 195589. So that wff1 logically entails wff2 could be demonstrated either by using the formal rules of proof to arrive at wff2 from wff1 or, alternatively, by using the rules of arithmetic to arrive at GN(wff1) = 195589 by multiplying 617 by 317 = GN(wff2). The metasyntactic and the arithmetic collapse into one another.
一旦清楚了算术和逻辑之间的关系，逻辑证明在系统中就有了可表达的算术属性。而推导这些算术属性就相当于前段所讲的转换的结果。比如系统中合法证明得到的命题的Godel数就会有特定的算术属性，比如奇偶或者指数成方之类或更可能的远比此复杂的属性。换句话说，可证性变成了一种算术关系。这样，我们就得到了一种同时包含其自身在系统中可证性信息的在系统中可表达的算术定理。Once one has this sort of collapse between logical implication and arithmetical relationship, we can go on and demonstrate that certain sequences of wffs—precisely those that constitute proofs—have an arithmetical property expressible in the system. Proofs, of course, are built up out of logical entailments. So deriving this arithmetical property (of the Godel numbers of all and only the proofs in the system) is going to be a consequence of the sort of collapse discussed in the previous paragraph. The Godel number of those strings of wffs that are valid proofs within the system will have some sort of arithmetical property, say, they'll all be even or they'll all be odd or they'll be prime numbers or the squares of primes or, more likely, a property a good deal more complicated. In other words, the metasyntactic relationship of provability will become an arithmetical relationship; that a string of wffs is a proof will be some property of numbers. From this it becomes possible to show that all and only the provable wffs in the system, the theorems, have a certain arithmetical property. You can see where we're heading: toward arithmetical propositions expressible in the system that also speak to the issue of their own provability within the system. The Godel numbering allows some propositions to engage in an interesting sort of doublespeak, saying something arithmetical and also commenting on their own situation within the formal system, saying whether they're provable.
这就像戏剧中的角色和其扮演者日常生活中的角色相互影响的关系。The doublespeak of these propositions could be compared to the sort of thing that sometimes happens within a dramatic play, in particular when the play presents actors as characters, with their own "reallife" relationships, and then presents these characters as actors in a play within the play. Through careful contrivance, the lines that the actors speak, in the play within the play, can also be interpreted as having a reallife meaning in their relationships outside the play within the play (in the play proper). Godel's strategy asks us to grasp something analogous to what the country audience in Leoncavallo's opera Pagliacci grasp when they understand the actors to be delivering lines that, as well as making sense within the play, have a meaning in their offstage lives (in the opera). In Godel's inspired stage production, lines speak both to the formal relationships within the system, the play within the play, and also reveal reallife arithmetical relationships. The proposition that Godel's proof constructs, the one that will simultaneously announce both its own (provable) unprovability and a true (unprovable) arithmetical relationship, has the same sort of doubleentendre as Pagliacci's final tragic cry, "La Commedia è finita!"—the comedy is over.
第三部：构造一个因为描述了其不可证性而为真的命题Step Three: Create a Proposition That's True Because It Says That It's Unprovable
之后，Godel给出了一个神奇的算术属性，称为($Pr$)或者“可证明”。它是所有系统中可证命题的Godel数才拥有的纯算术属性。Having established his ingenious layers of meaning, Godel now conjures a rather amazing arithmetical property, which we'll designate as "Pr" for "provable." Because, although Pr is a purely arithmetical property, it's also that very property toward which all the contrivances have been heading. It's an arithmetical property that is true of all and only the Godel numbers of the provable propositions of the system. I choose the verb "conjures" deliberately because even though the collapse of the metasyntactic and arithmetical was heading toward "Pr", there is still a sense of magic about the entrance of Pr.
在继续之前，这里是一些小的技术细节：通过单变量的命题函数代表属性，形如($F(x)$)。当($x$)被定义域中任一值替换后，($F(x)$)才成为了一个或真或假的命题。Before getting to the property, one little technical point about the way in which properties are specified: by propositional functions of one variable. These can be thought of as of the form F(x). These are expressions in the formal system involving a single variable—the x which is a dummy standing for a whole range of possible values (the domain of individuals) that can be plugged in; if you plug in a value for the variable, you end up with a wff that is either true or false, in other words a proposition. F(x), just as it is, is neither true nor false. So say s(x) were to mean: x is the successor of 1. This is neither true nor false; it isn't a proposition, a definite statement, since what it says depends upon what x actually represents. Plugging in 2 for the variable x yields a true proposition, and plugging in anything else yields false propositions. That's how properties are designated in the system, by propositional functions of one variable.
回到($Pr(x)$)，一个比较复杂的算术属性。首先，所有命题都通过Godel计数被赋予了一个数值，即每个($wff_p$)，我们有($GN(p)$)。而定理是系统中所有命题的一个子集，即可证命题。所以，给一个自然数($n$)，它不一定对应于系统中的某个定理，即对($n = GN(p)$)，($p$)不一定可证。Now onward to Pr(x), which is a somewhat complicated property of numbers. Remember, first of all, that each of the wffs in the formal system have been assigned numbers through the wonders of Godel numbering. So for every wff p, we have some GN(p), some natural number or other. The theorems are a special subset of the wffs of the system, the provable propositions. Given any natural number n, then, it may or may not be the case that it corresponds to some theorem in the formal system, that is, it may or may not be the case that n = GN(p) for some proposition p which is a theorem of the formal system.
现在定义($Pr(x)$)。该命题函数的定义域为自然数，对任意自然数($n$)，若对定理($p$)，($n = GN(p)$)，我们称($n$)满足($Pr(x)$)，即($Pr(n) $)为真。Godel证明了该属性不管其复杂度，可通过形式系统中给出。另外通过这个属性，Godel可以同时描述命题是否为定理的属性，并将之转为算术陈述，即“($p$)是个定理”转为“Pr(GN(p))”，称($n$)满足($Pr(x)$)即表示($n$)相应的命题是定理。Now we are in position to define Pr(x). The possible values for this propositional function, the things we plug in for the dummy x, are (the expressions for) the natural numbers. For any natural number n, if n = GN(p) for a theorem p of the system then we say that n satisfies the property Pr(x), that is, that Pr(n) is true. Godel showed that this property is one that can in fact be expressed in the formal system, that is, that it's an example of an F(x). Pr(x) is a formally expressible arithmetical property, albeit one that is extremely complicated, not anything that we can explicitly give here. But by means of this property Godel is able to take metasentences about the system, stating which propositions are theorems of the system, and transform them into arithmetical sentences within the system: "p is a theorem" is transformed into "Pr(GN(p))". To say of some particular n that it has the property Pr(x) is to say that this number corresponds to a theorem in the formal system.
就如奇偶性一样，($n$)满足($Pr(x)$)确实是真的算术属性。Now perhaps you're thinking something like this: That a particular number n has the property Pr(x) isn't a real property of n. The number n, for example, may be even or it may be odd; if it's divisible by 2 then it's even. Let's say it is. Then its evenness is a real arithmetical property; n couldn't be the number it is if it weren't even. In contrast, looking at this property Pr(x) metasystematically, it doesn't seem at all a proper sort of numerical property. A number n has this property only arbitrarily, since the proposition with which n is associated is arbitrary, a consequence merely of the way in which the Godel numbering was set up, the inspired contrivances. True enough, but, arbitrary though it may be, Pr(x) is nonetheless a real arithmetical property, and a number n either will or won't have it. And n wouldn't be the number that it is unless it either did or didn't have it. Just because Pr(x) has a metameaning doesn't detract from its arithmetical character. This property Pr(x) is, in fact, stupendous, and it allows us to take the plunge into the heart of the proof.
接下来用到的是对角引理（diagonal lemma，证明未给出），它的一个特殊形式被用在了Godel的证明中，而这儿为简化证明，使用了它的通用形式。http://en.wikipedia.org/wiki/Diagonal_lemmaWhat we use next is something called the diagonal lemma. It's a general statement, a particular case of which is what we need to prove Godel's theorem. (Godel didn't actually use it, but rather derived the particular case.) Making use of this general lemma (which, of course, we're not going to prove) will simplify matters enormously.
对角引理指出Godel计数满足对任意单变量命题函数($F(x)$)，存在($n$)使($F(n)$)的Godel数等于($n$)本身（这大概暗示了Godel计数超常的一面）。即对任意($F(x)$)存在($n$)使得(0)($$n = GN(F(n))$$)The diagonal lemma states that the Godel numbering is such that for any propositional function F(x) of one variable, there exists a number n such that the Godel number of F(n), the proposition we get when we plug n into the function F(x), turns out to be n itself. (That there must exist such a number for each F(x) may suggest what superhuman efforts went into the Godel numbering.) In other words, the diagonal lemma asserts that for any F(x) there is an n such that
被称为对角引理是因为($n$)对应的点正好在($y = GN(F(x))$)的对角线上，即($y = x$)上。The number you get out is the same number you started with, and so the special n associated with a given F corresponds precisely to where the graph of y = GN(F(x)) intersects the diagonal, the graph of y = x, namely where x = n. Hence the name, the "diagonal lemma."
（注意：($n = GN(F(n))$)是元语言，它是一个“普通声明”，既不是形式上的声明（formal statement），在左侧的($n$)是自然数，而在右侧的是形式系统中给出($n$)，即出现了($n$)次($s$)的$s(s(s(...s(s(0)))))$。）(N.B. The statement n = GN(F(n)) is in the metalanguage. It's a "normal statement" (i.e., not a formal statement) and n on the left denotes a (normal)natural number. However, the n on the right represents the expression in the formal system that represents the number n, namely s(s(s( . . . s(s(0))))), with n occurrences of s.)
注意对角引理得到对应于命题函数($F(x)$)的($n$)本身满足属性($F$)。大致上相当于($这句话满足F$)，其中可以看到自引用的意思。Notice that the number n that the diagonal lemma associates with the propositional function F(x) is such that the proposition with Godel number n (namely F(n)) says that n itself has the property F. It is, roughly speaking, of the form; this very sentence is F. Soft whispers of selfreferentiality are hovering in the hushed air.
再回到($Pr$)。一个数满足($Pr$)当且仅当它对应的命题可证，即：Now let's go back to that stupendous property that Godel produced, Pr, which is true of all and only the Godel numbers of the theorems, the provable wffs, of the system. A number will have the arithmetical property Pr if and only if it corresponds to a provable proposition under the Godel numbering. In other words:
($$Pr(GN(p))当且仅当p可证$$)Pr(GN(p)) if and only if p is provable.
在其中的元语法（非算术）的意义上，对属性($$\text{~}Pr(x)$$)We have the metasyntactic sense of what Pr(x) means (though not what its arithmetical meaning is; you just have my assurance that it has an arithmetical meaning). Now let's look at the property:
这个属性为真当且仅当对应的命题不可证，即：This second property will be true of all and only the Godel numbers of non theorems; that is, it is true of the Godel numbers of objects that are not propositions provable in the system. In other words:
(1)($$\text{~}Pr(GN(p))当且仅当p不可证$$)~Pr(GN(p)) if and only if p is not provable (1)
(1)是一个元数学上的声明，既不是一个形式系统中的命题又不是算术表达式。单通过它我们可以将元数学上的声明转入到算术表达式中。What kind of sentence is (1)? It is a metamathematical sentence. It's not itself a sentence of the formal system, nor an arithmetical sentence. But by means of (1) we can transform some metamathematical sentences into arithmetical sentences.
现在将对角引理用于($F(x) = \text{~}Pr(x)$)中，我们得到一个($n$)满足($n = GN(F(n))$)，我们称这个($n$)为($g$)，即：(2)($$g = GN(\text{~}Pr(g))$$)Now the diagonal lemma concerns any prepositional function F(x), so let's apply it to F(x) = ~Pr(x). The diagonal lemma, remember, states that for any propositional function F(x) of one variable, there exists a number n that is the Godel number of the very proposition we get when we plug n itself into the function. We're now considering the propositional function ~Pr. According to the diagonal lemma there is some number, let's call it g, such that:
即($g$)不满足($Pr$)。We arrived at (2) by replacing F by ~Pr and n by g in (0). Equation (2) says that g is the Godel number of the proposition that states that the number g lacks the arithmetical property Pr (which belongs to all and only those numbers which are Godel numbers of provable propositions).
现在构造命题($G$)，令(3)($$G = \text{~}Pr(g)$$)Now we're ready to frame our proposition G. Let
($G$)表示数字($g$)不满足($Pr$)，通过(2)(3)有($$GN(G) = g$$)The proposition G states that the number g lacks the property Pr. Moreover, by (2) and (3), we have that:
回到(1)并作一些替换，有：Now we go back to (1) and make some substitutions. Here's (1) again:
($$\text{~}Pr(GN(p))当且仅当p不可证$$)~Pr(GN(p)) if and only if p is not provable
对(1)，令($p = G$)，又($GN(G) = g$)，有：Letting p = G in (1), and using the fact that GN(G) = g, we obtain:
(4)($$\text{~}Pr(g)当且仅当G不可证$$)~Pr(g) if and only if G is not provable (4)
因为(3)，我们得到($G当且仅当G不可证$)。That is, using again (3), G if and only if G is not provable. What (4) is saying is that G is true if and only if G is not provable!
($G$)是一个纯算术声明，同时又描述了它本身的不可证性。它为假时会引出矛盾，所以除非系统不一致，这样所有命题包括矛盾都可证，不然它只能为真。而系统一致是前提，所以($G$)即为真且不可证。我们没有通过推导证明它为真，而是在系统外证明了其不可证性而得到它为真。G is, of course, a purely arithmetical statement, but it's also simultaneously talking about itself, and what it's saying is that it's not provable. Is what it's saying true? Well, it could hardly be false since then it would have to be provable and hence true anyway. That is, unless, of course, the formal system of arithmetic is inconsistent, so that all its propositions would be provable, even contradictions. This is the point in the proof where that presumption of the consistency of the formal system is being called upon to stand up and deliver. And it does. G is both unprovable and, given that that's what it says, it's also true. We haven't shown that it's true by finding a proof for it within the formal system, using the purely mechanical rules of that system, that is, by deducing it. Rather, we've shown it's true by, ironically, going outside the system and showing that no proof for it can be produced within the formal system. We've shown that G is true by showing that it can't be proved, just as it says.
此外，Godel实际上给出了不只针对算术系统的而是所有含算术的形式系统的为真而不可证命题的构造方法。所以如果试图通过增加公理而绕开Godel不完备性定义，新的形式系统下仍然可构造出新的有问题的命题。也就是对任一包含基本算术的一致的形式系统都含为真而不可证的命题。Moreover, Godel in fact showed how to construct a true but unprovable proposition, not just for the formal system of arithmetic we have been discussing but for any formal system whatsoever containing arithmetic. So if we should try to weasel our way out of Godel's first incompleteness theorem by constructing a new formal system that has G appended as an axiom, a new problematic proposition can be constructed for that system. And so on, ad infinitum. There are provably unprovable but nonetheless true propositions in any formal system that contains elementary arithmetic, assuming that system to be consistent.
而这个就是Godel第一不完备性定理。And that is Godel's first incompleteness theorem.
回应 20130908 22:55 
The first of these problem revolving around Cantor's continuum hypothesis. What is Cantor's continuum hypothesis? The great nineteenthcentury mathematician Georg Cantor had proved that (roughly speaking) there are more real numbers than there are natural numbers, even though there are an infinite number of both. Cantor showed, by means of an elegant argument called the "diagonal argument&quo..;.
20130805 10:25
The first of these problem revolving around Cantor's continuum hypothesis. What is Cantor's continuum hypothesis? The great nineteenthcentury mathematician Georg Cantor had proved that (roughly speaking) there are more real numbers than there are natural numbers, even though there are an infinite number of both. Cantor showed, by means of an elegant argument called the "diagonal argument", that in the infinite pairing of one natural number with one real number, every natural number will be paired with a real number but some real number or other will forever be left out. The set of real numbers is thus of a higher ordinality (roughly speaking, there are more of them) than the set of natural numbers. Cantor hypothesized that there is no infinite set that intervenes between the set of natural numbers and the set of real numbers; that is, there is no set that has higher ordinality than the natural numbers and a lower ordinality than the real numbers. This is Cantor's continuum hypothesis and Hilbert's first problem was to prove Cantor's continuum hypothesis true. Gödel was to contribute to the solution to this problem, though not in a way that Hilbert welcomed. Gödel, together with Paul Cohen, proved that the continuum hypothesis can be proved neither true nor false within curren set theory. In other words the status of the continuum hypothesis is what Hilbert claimed there could not be: an ignoramibusa claim that can neither be confirmed nor discredited, a claim about which we remain ignorant.
回应 20130805 10:25 
More specifically, Einstein's and Gรถdel's meta convictions were addressed to the question of whether their respective fields are descriptions of an objective realityexisting independent of our thinking of itor, rather, are subjective human projection, socially shared intellectual constructs.
20130804 14:18
More specifically, Einstein's and Gödel's meta convictions were addressed to the question of whether their respective fields are descriptions of an objective realityexisting independent of our thinking of itor, rather, are subjective human projection, socially shared intellectual constructs.
回应 20130804 14:18
以下豆列推荐 · · · · · · ( 全部 )
 2005亚马逊科普类图书十佳 (pH7[..匪七..])
 科学模式 (spwood)
 Popular metatheories (Bearinger)
 数学家与统计学家 (金乌一点)
谁读这本书?
二手市场
 > 点这儿转让 有14人想读,手里有一本闲着?
订阅关于Incompleteness的评论:
feed: rss 2.0
1 有用 金乌一点 20120623
哭死我了。。。。。
1 有用 金乌一点 20120623
哭死我了。。。。。