一，译文

1，哥德尔不完全性定理（第一不完全性定理）

哥德尔不完全性定理： 任何一致的形式系统F，在其中可以进行一定量的基本算术运算，都是不完备的；也就是说，F的语言存在着既不能证明也不能证伪的语句。(Raatikainen 2015)

2，哥德尔不完全性定理的证明草图

反证法有三个基本部分。首先，选择一个符合拟议标准的形式系统：

（1）该系统中的语句可以用自然数（称为哥德尔数）表示。其意义在于，语句的属性—如其真假—将等同于确定其哥德尔数是否具有某些属性，因此，语句的属性可以通过考察其哥德尔数来证明。这一部分的高潮是构建一个公式，表达“语句S在系统中是可以证明的”这一观点（可以应用于系统中的任何语句S）。

（2）在形式系统中，有可能构建一个数，其匹配的语句在被解释时是自指的，本质上说它（即语句本身）是不可证明的。这是用一种叫做“对角线化”的技术完成的（所谓的对角线化是因为它起源于康托尔的对角线论证）。

（3）在形式系统中，这个语句允许证明它在系统中既不能被证明也不能被证伪，因此系统事实上不可能是ω-一致的。因此，提议的系统符合标准的原始假设是错误的。

3，关于“可证明性”句子的构造

在指出原则上系统可以间接地做出关于可证明性的句子之后，通过分析代表句子的那些数字的属性，现在有可能指出如何构造一个实际上是这样的句子。

一个恰好包含一个自由变量x的公式F(x)被称为语句形式或类符号。只要x被一个特定的数字所取代，该语句形式就变成了一个真正的语句，然后它要么在系统中可被证明，要么不可被证明。对于某些公式，人们可以证明，对于每一个自然数n，F(n)是真的，当且仅当它可以被证明（原始证明中的精确要求更弱，但对于证明草图来说，这就足够了）。特别是，对于有限数量的自然数之间的每一个具体的算术运算，如2×3=6，这都是真的。

语句形式本身不是语句，因此不能被证明或证伪。但每个语句形式F(x)都可以被分配一个哥德尔数，用G(F)表示。F(x)形式中使用的自由变量的选择与哥德尔数G(F)的分配无关。

可证明性的概念本身也可以用哥德尔数来编码，方式如下：由于证明是遵守某些规则的语句的列表，因此可以定义证明的哥德尔数。现在，对于每个语句p，人们可以问一个数字x是否是其证明的哥德尔数。p的哥德尔数和x之间的关系，即其证明的潜在哥德尔数，是两个数字之间的算术关系。因此，有一个陈述形式Bew(y)使用这种算术关系来说明y的证明的哥德尔数存在：

Bew(y) = ∃ x（y是一个公式的哥德尔数，x是y所编码的公式的证明的哥德尔数）。

Bew这个名字是beweisbar的简称，是德语中 "可证明 "的意思；这个名字最初是由哥德尔用来表示刚才描述的可证明公式的。请注意，"Bew(y) "只是一个缩写，它代表了T的原始语言中的一个特殊的、很长的公式；字符串Bew本身并不声称是这个语言的一部分。

公式Bew(y)的一个重要特征是，如果一个语句p在系统中是可证明的，那么Bew(G(p))也是可证明的。这是因为任何对p的证明都会有一个相应的哥德尔数，它的存在导致Bew(G(p))被满足。

4，对角线化

证明的下一步是获得一个命题，该命题间接地断言了其自身的不可证明性。尽管哥德尔直接构造了这一命题，但至少有一个这样的命题存在于对角线引理中，即对于任何足够强的形式系统和任何命题形式F，都有一个声明p，使得系统证明了：

p ↔ F(G(p))

通过将F解释为Bew(x)的否定，我们得到定理：

p ↔¬Bew(G(p))

而由此定义的p大致说明它自己的哥德尔数是一个不可证的公式的哥德尔数。

语句p并不等同于¬Bew(G(p))；相反，p指出，如果进行某种计算，所产生的哥德尔数将是一个不可证明的语句。但当这个计算被执行时，结果的哥德尔数变成了p本身的哥德尔数。这类似于英语中的以下句子：“, when preceded by itself in quotes, is unprovable.”，前面有引号的时候，是无法证明的。

这个句子没有直接提到它自己，但是当进行所述的转换时，原句作为结果得到了，因此这个句子间接地断言了它自己的不可证性。对角线法则的证明也采用了类似的方法。

现在，假设公理系统是ω一致的，让p是上一节中得到的语句。

如果p是可证的，那么Bew(G(p))将是可证的，正如上面所论证的。但是p断言了Bew(G(p))的否定。因此，这个系统将是不一致的，既证明了一个陈述，又证明了它的否定。这个矛盾表明，p是不可证明的。

如果p的否定是可证明的，那么Bew(G(p))将是可证明的（因为p被构造为等同于Bew(G(p))的否定）。然而，对于每个具体的数字x，x不可能是p的证明的哥德尔数，因为p是不可证明的（来自上一段）。因此，一方面系统证明了有一个数字具有某种属性（即它是p的证明的哥德尔数），但另一方面，对于每个具体的数字x，我们可以证明它不具有这种属性，这在一个ω一致的系统中是不可能的。因此，p的否定是不可证明的。

因此，在我们的公理系统中，语句p是不可判定的：它在系统中既不能被证明也不能被证伪。

事实上，要证明p是不可证明的，只需要假设系统是一致的。要证明p的否定是不可证明的，则需要更强的ω一致性的假设。因此，如果p是为一个特定系统构造的。

如果该系统是ω一致性的，它既不能证明p也不能证明其否定，因此p是不可判定的。

如果系统是一致的，它可能有同样的情况，或者它可能证明p的否定。在后一种情况下，我们有一个陈述（“不是p”），它是假的，但可以证明，而且系统不是ω一致的。

如果人们试图“增加缺失的公理”以避免系统的不完全性，那么就必须增加p或“非p”作为公理。但这样一来，语句的“作为证明的哥德尔数”的定义就会改变。这意味着公式Bew(x)现在是不同的。因此，当我们将对角线法应用于这个新的Bew时，我们会得到一个新的声明p，与之前的声明不同，如果它是ω一致的，那么在新的系统中是不可判定的。

二，原文

First incompleteness theorem

First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F." (Raatikainen 2015)

Proof sketch for the first theorem

The proof by contradiction has three essential parts. To begin, choose a formal system that meets the proposed criteria:

1，Statements in the system can be represented by natural numbers (known as Gödel numbers). The significance of this is that properties of statements—such as their truth and falsehood—will be equivalent to determining whether their Gödel numbers have certain properties, and that properties of the statements can therefore be demonstrated by examining their Gödel numbers. This part culminates in the construction of a formula expressing the idea that "statement S is provable in the system" (which can be applied to any statement "S" in the system).

2，In the formal system it is possible to construct a number whose matching statement, when interpreted, is self-referential and essentially says that it (i.e. the statement itself) is unprovable. This is done using a technique called "diagonalization" (so-called because of its origins as Cantor's diagonal argument).

3，Within the formal system this statement permits a demonstration that it is neither provable nor disprovable in the system, and therefore the system cannot in fact be ω-consistent. Hence the original assumption that the proposed system met the criteria is false.

Construction of a statement about “provability”

Having shown that in principle the system can indirectly make statements about provability, by analyzing properties of those numbers representing statements it is now possible to show how to create a statement that actually does this.

A formula F(x) that contains exactly one free variable x is called a statement form or class-sign. As soon as x is replaced by a specific number, the statement form turns into a bona fide statement, and it is then either provable in the system, or not. For certain formulas one can show that for every natural number n, {\displaystyle F(n)}F(n) is true if and only if it can be proved (the precise requirement in the original proof is weaker, but for the proof sketch this will suffice). In particular, this is true for every specific arithmetic operation between a finite number of natural numbers, such as "2 × 3 = 6 ».

Statement forms themselves are not statements and therefore cannot be proved or disproved. But every statement form F(x) can be assigned a Gödel number denoted by G(F). The choice of the free variable used in the form F(x) is not relevant to the assignment of the Gödel number G(F).

The notion of provability itself can also be encoded by Gödel numbers, in the following way: since a proof is a list of statements which obey certain rules, the Gödel number of a proof can be defined. Now, for every statement p, one may ask whether a number x is the Gödel number of its proof. The relation between the Gödel number of p and x, the potential Gödel number of its proof, is an arithmetical relation between two numbers. Therefore, there is a statement form Bew(y) that uses this arithmetical relation to state that a Gödel number of a proof of y exists:

Bew(y) = ∃ x (y is the Gödel number of a formula and x is the Gödel number of a proof of the formula encoded by y).

The name Bew is short for beweisbar, the German word for "provable"; this name was originally used by Gödel to denote the provability formula just described. Note that "Bew(y)" is merely an abbreviation that represents a particular, very long, formula in the original language of T; the string "Bew" itself is not claimed to be part of this language.

An important feature of the formula Bew(y) is that if a statement p is provable in the system then Bew(G(p)) is also provable. This is because any proof of p would have a corresponding Gödel number, the existence of which causes Bew(G(p)) to be satisfied.

Diagonalization

The next step in the proof is to obtain a statement which, indirectly, asserts its own unprovability. Although Gödel constructed this statement directly, the existence of at least one such statement follows from the diagonal lemma, which says that for any sufficiently strong formal system and any statement form F there is a statement p such that the system proves

p ↔ F(G(p)).

By letting F be the negation of Bew(x), we obtain the theorem：

p ↔ ~Bew(G(p))

and the p defined by this roughly states that its own Gödel number is the Gödel number of an unprovable formula.

The statement p is not literally equal to ~Bew(G(p)); rather, p states that if a certain calculation is performed, the resulting Gödel number will be that of an unprovable statement. But when this calculation is performed, the resulting Gödel number turns out to be the Gödel number of p itself. This is similar to the following sentence in English:

", when preceded by itself in quotes, is unprovable.", when preceded by itself in quotes, is unprovable.

This sentence does not directly refer to itself, but when the stated transformation is made the original sentence is obtained as a result, and thus this sentence indirectly asserts its own unprovability. The proof of the diagonal lemma employs a similar method.

Now, assume that the axiomatic system is ω-consistent, and let p be the statement obtained in the previous section.

If p were provable, then Bew(G(p)) would be provable, as argued above. But p asserts the negation of Bew(G(p)). Thus the system would be inconsistent, proving both a statement and its negation. This contradiction shows that p cannot be provable.

If the negation of p were provable, then Bew(G(p)) would be provable (because p was constructed to be equivalent to the negation of Bew(G(p))). However, for each specific number x, x cannot be the Gödel number of the proof of p, because p is not provable (from the previous paragraph). Thus on one hand the system proves there is a number with a certain property (that it is the Gödel number of the proof of p), but on the other hand, for every specific number x, we can prove that it does not have this property. This is impossible in an ω-consistent system. Thus the negation of p is not provable.

Thus the statement p is undecidable in our axiomatic system: it can neither be proved nor disproved within the system.

In fact, to show that p is not provable only requires the assumption that the system is consistent. The stronger assumption of ω-consistency is required to show that the negation of p is not provable. Thus, if p is constructed for a particular system:

If the system is ω-consistent, it can prove neither p nor its negation, and so p is undecidable.

If the system is consistent, it may have the same situation, or it may prove the negation of p. In the later case, we have a statement ("not p") which is false but provable, and the system is not ω-consistent.

If one tries to "add the missing axioms" to avoid the incompleteness of the system, then one has to add either p or "not p" as axioms. But then the definition of "being a Gödel number of a proof" of a statement changes. which means that the formula Bew(x) is now different. Thus when we apply the diagonal lemma to this new Bew, we obtain a new statement p, different from the previous one, which will be undecidable in the new system if it is ω-consistent.

参考文献：

https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#First_incompleteness_theorem