# 哥德尔1931论文第一章的译文

1.

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

[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 nK, 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

https://wap.sciencenet.cn/blog-2322490-1334098.html

## 全部精选博文导读

GMT+8, 2022-8-9 07:04