哥德尔在1931年的著名文章《论数学原理和相关系统中形式上不可判定命题I》(On Formally Undecidable Propositions of Principia Mathematica and Related Systems I）[1][2]中声称证明了《数学原理》（Principia Mathematica，PM）中所报告的系统的不完备性（如皮亚诺算术，Peano Arithmetic，PA）。

哥德尔的这篇论文由三章组成：第1章概述了证明的主要思想，第2章和第3章将第1章的思想形式化。这里我将第1章译出。

一，译文

论《数学原理》及相关系统中形式上不可判定的命题(1931) - 第一章

库尔特-哥德尔

1.

众所周知，数学朝着更为精确的方向发展，导致了数学很大范围的形式化，因此，人们只需使用一些机械性规则就能证明任何定理。迄今为止建立的最全面的形式化系统，一个是《数学原理》（ Principia Mathematica，PM）的系统，另一个是集合论的策梅洛-弗兰克尔集合论（Zermelo-Fraenkel ）公理系统（由J.冯-诺依曼进一步发展）。这两个系统是如此全面，以至于今天数学中使用的所有证明方法都能够用这些系统来形式化，也就是说，被归约成几个公理和推理规则。因此，人们往往会认为，这些公理和推理规则足以判定任何用这些系统形式表达的数学问题。接下来的篇幅将表明事实并非如此，相反，在上述两个系统中存在着数论中相对简单的问题，这些问题不能根据公理来判定。这种情况决不是由于所建立的系统的特殊性质造成的，而是对一大类形式系统都适用；在这些系统中，尤其是由刚才提到的两个系统通过增加有限数量的公理而产生的所有系统，只要由于增加了公理，不会出现注4中规定的那种假命题变成可证明。

在讨论细节之前，我们将首先勾勒出证明的主要思路，当然不要求完全精确。一个形式化系统（我们在这里仅限于系统PM）的公式在外表上是原始符号（变量、逻辑常量和括号或标点符号）的有限序列，而且很容易完全精确地说明哪些原始符号序列是有意义的公式，哪些不是。同样，从形式化的角度来看，证明只不过是公式的有限序列（具有某些特定的属性）。当然，出于元数学的考虑，选择什么对象作为原始符号并不重要，我们将使用自然数。因此，元数学概念（命题）成为关于自然数或自然数序列的概念（命题）；它们就可以（至少部分地）由系统PM本身的符号来表达。特别是，“公式”、 “证明序列”和“可证公式”这些概念可以在系统PM中定义；也就是说，例如我们可以找到有一个自由变量v（数序列的一个类型）的PM公式F(v)，根据PM术语的含义解释F(v)：v是一个可证公式。我们现在构造PM系统的一个不可判定命题，也就是一个命题A，A和非A都不可证的，其方式如下：

只有一个自由变量的PM公式被称为“class sign（类符号）”，该自由变量是自然数的类型（类的类）。我们假设class sign已经以某种方式排列成一个序列，我们用R(n)表示第n个，我们注意到class sign这个概念以及排序关系R可以在PM系统中定义。让α是任何class sign，用[α；n]表示当自由变量被表示自然数n的符号取代时，由class sign α产生的公式。三元关系x= [y; z]，也被认为是可以在PM中定义的。我们现在以如下方式定义自然数的集合K：

K={n|～Bew[R(n); n]} (1)

其中Bew x的意思是：x是一个可证明的公式。由于在定义中出现的概念都可以在PM中定义，所以由它们形成的概念K也可以在PM中定义；也就是说，有一个class sign S，使公式[S；n]，根据PM术语的含义解释，说明自然数n属于K。由于S是一个class sign，它与某个R(q)是相同的，也就是说，我们有：S = R(q)，对某个自然数q。

我们现在证明命题[R(q); q]在PM中是不可判定的。因为我们假设命题[R(q); q]是可证明的；那么它也将是真的。但在这种情况下，根据上面给出的定义，q属于K，也就是说，根据（1），～Bew[R(q); q]将成立，这与假设相矛盾。另一方面，如果[R(q); q]的否定是可证明的，那么q不属于K，即Bew[R(q); q]将成立。但这样一来，[R(q); q]以及它的否定就可以被证明，这也是不可能的。

这个论证与“理查德悖论”的相似性跃然纸上，也与“说谎者悖论”密切相关；因为不可判定的命题[R(q); q]指出q属于K，也就是说，根据(1)，[R(q); q]是不可证明的。因此，我们面前有一个命题，它说它自己是不可证明的[在PM中]。刚刚解释的证明方法显然可以适用于任何形式系统，首先，当被解释为代表一个概念和命题系统时，它有足够的表达方式来定义上述论证中出现的概念（特别是“可证明公式”这一概念），其次，在所考虑的解释中，每个可证明公式是真的。在下文中完全精确地进行上述证明的目的是，除其他外，用一个纯形式的、弱得多的假设取代刚才提到的第二个假设。

从[R(q); q]说它自己是不可证明的这句话中，马上可以看出[R(q); q]是真的，因为[R(q); q]的确是不可证明的（是不可判定的）。因此，在系统PM中不可判定的命题仍然是由元数学的考虑决定的。对这种奇怪情况的精确分析导致了关于形式系统一致性证明的令人惊讶的结果，这些结果将在第四节（定理十一）中详细讨论。

二，原文

II On Formally Undecidable Propositions of Principia Mathematica and Related Systems I1 (1931)
Kurt Gödel 

1. 

The development of mathematics toward greater precision has led, as is well known, to the formalization of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules. The most comprehensive formal systems that have been set up hitherto are the system of Principia Mathematica (PM) on the one hand and the Zermelo-Fraenkel axiom system of set theory (further developed by J.von Neumann)3 on the other. These two systems are so comprehensive that in them all methods of proof today used in mathematics are formalized, that is, reduced to a few axioms and rules of inference. One might therefore conjecture that these axioms and rules of inference are sufficient to decide any mathematical question that can at all be formally expressed in these systems. It will be shown below that this is not the case, that on the contrary there are in the two systems mentioned relatively simple problems in the theory of integers4 that cannot be decided on the basis of the axioms. This situation is not in any way due to the special nature of the systems that have been set up but holds for a wide class of formal systems; among these, in particular, are all systems that result from the two just mentioned through the addition of a finite number of axioms, provided no false propositions of the kind specified in note 4 become provable owing to the added axioms. 

Before going into details, we shall first sketch the main idea of the proof, of course without any claim to complete precision. The formulas of a formal system (we restrict ourselves here to the system PM) in outward appearance are finite sequences of primitive signs (variables, logical constants, and parentheses or punctuation dots), and it is easy to state with complete precision which sequences of primitive signs are meaningful formulas and which are not. Similarly, proofs, from a formal point of view, are nothing but finite sequences of formulas (with certain specifiable properties). Of course, for metamathematical considerations it does not matter what objects are chosen as primitive signs, and we shall assign natural numbers to this use. Consequently, a formula will be a finite sequence of natural numbers, and a proof array a finite sequence of finite sequences of natural numbers. The metamathematical notions (propositions) thus become notions (propositions) about natural numbers or sequences of them; therefore they can (at least in part) be expressed by the symbols of the system PM itself. In particular, it can be shown that the notions ‘formula’, ‘proof array’, and ‘provable formula’ can be defined in the system PM; that is, we can, for example, find a formula F(v) of PM with one free variable v (of the type of a number sequence) such that F(v), interpreted according to the meaning of the terms of PM, says: v is a provable formula. We now construct an undecidable proposition of the system PM, that is, a proposition A for which neither A nor not-A is provable, in the following manner. 

A formula of PM with exactly one free variable, that variable being of the type of the natural numbers (class of classes), will be called a class sign. We assume that the class signs have been arranged in a sequence in some way, we denote the nth one by R(n), and we observe that the notion ‘class sign’, as well as the ordering relation R, can be defined in the system PM. Let α be any class sign; by [α; n] we denote the formula that results from the class sign α when the free variable is replaced by the sign denoting the natural number n. The ternary relation x= [y; z], too, is seen to be definable in PM. We now define a class K of natural numbers in the following way: 

K={n|～Bew[R(n); n]} (1)

(where Bew x means: x is a provable formula. Since the notions that occur in the definiens can all be defined in PM, so can the notion K formed from them; that is, there is a class sign S such that the formula [S; n], interpreted according to the meaning of the terms of PM, states that the natural number n belongs to K. Since S is a class sign, it is identical with some R(q); that is, we have 

S = R(q)

for a certain natural number q. 

We now show that the proposition [R(q); q] is undecidable in PM. For let us suppose that the proposition [R(q); q] were provable; then it would also be true. But in that case, according to the definitions given above, q would belong to K, that is, by (1),～Bew[R(q); q] would hold, which contradicts the assumption. If, on the other hand, the negation of [R(q); q] were provable, then ～n∈K, that is, Bew [R(q); q], would hold. But then [R(q); q], as well as its negation, would be provable, which again is impossible.

The analogy of this argument with the Richard antinomy leaps to the eye. It is closely related to the ‘Liar’ too;14 for the undecidable proposition [R(q); q] states that q belongs to K, that is, by (1), that [R(q); q] is not provable. We therefore have before us a proposition that says about itself that it is not provable [in PM].15 The method of proof just explained can clearly be applied to any formal system that, first, when interpreted as representing a system of notions and propositions, has at its disposal sufficient means of expression to define the notions occurring in the argument above (in particular, the notion ‘provable formula’) and in which, second, every provable formula is true in the interpretation considered. The purpose of carrying out the above proof with full precision in what follows is, among other things, to replace the second of the assumptions just mentioned by a purely formal and much weaker one.

From the remark that [R(q); q] says about itself that it is not provable it follows at once that [R(q); q] is true, for [R(q); q] is indeed unprovable (being undecidable). Thus, the proposition that is undecidable in the system PM still was decided by metamathematical considerations. The precise analysis of this curious situation leads to surprising results concerning consistency proofs for formal systems, results that will be discussed in more detail in Section 4 (Theorem XI).

参考文献：

[1] S.G. Shanker (ed.), Gödel’s Theorem in Focus, Croom Helm 1988, https://pdfslide.net/documents/godels-theorem-in-focus-philosophers-in-focus.html

[2] Translated by B. Meltzer, Introduction by R. B. Braithwaite, On Formally Undecidable Propositions of Principia Mathematica and Related Systems I1 (1931) Kurt Gödel, https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally_Undecidable_Propositions_of_Principia_Mathematica_and_Related_Systems_1992.pdf