此词条暂由彩云小译翻译，翻译字数共11115，未经人工整理和审校，带来阅读不便，请见谅。

模板:Pp-pc1 Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of 模板:Not a typo in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

哥德尔的不完备性定理是数理逻辑中两个与形式公理理论的极限有关的定理。这些结果由库尔特 · 哥德尔于1931年发表，在数理逻辑和数学哲学中都很重要。这些定理被广泛而不是普遍地解释为表明希尔伯特为所有数学找到一个完整和一致的公理集的程序是不可能的。

The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency.

第一个不完备性定理指出，没有一个一致的公理系统，其定理可以通过一个有效的程序(即算法)列出，能够证明关于自然数算法的所有真理。对于任何这样一个一致的形式系统，总会有一些关于自然数的陈述是正确的，但是这些陈述在系统中是无法证明的。第二个不完备性定理是第一个不完备性定理的推广，它表明系统不能证明自身的一致性。

Employing a diagonal argument, Gödel's incompleteness theorems were the first of several closely related theorems on the limitations of formal systems. They were followed by Tarski's undefinability theorem on the formal undefinability of truth, Church's proof that Hilbert's Entscheidungsproblem is unsolvable, and Turing's theorem that there is no algorithm to solve the halting problem.

Employing a diagonal argument, Gödel's incompleteness theorems were the first of several closely related theorems on the limitations of formal systems. They were followed by Tarski's undefinability theorem on the formal undefinability of truth, Church's proof that Hilbert's Entscheidungsproblem is unsolvable, and Turing's theorem that there is no algorithm to solve the halting problem.

运用对角线论证，哥德尔的不完备性定理是关于形式系统局限性的几个密切相关的定理中的第一个。其次是 Tarski 关于形式上不可定义的真理的不可定义性定理，Church 关于 Hilbert 的可判定性不可解的证明，以及图灵关于停机问题没有算法的定理。

Formal systems: completeness, consistency, and effective axiomatization

The incompleteness theorems apply to formal systems that are of sufficient complexity to express the basic arithmetic of the natural numbers and which are consistent and effectively axiomatized. Particularly in the context of first-order logic, formal systems are also called formal theories. In general, a formal system is a deductive apparatus that consists of a particular set of axioms along with rules of symbolic manipulation (or rules of inference) that allow for the derivation of new theorems from the axioms. One example of such a system is first-order Peano arithmetic, a system in which all variables are intended to denote natural numbers. In other systems, such as set theory, only some sentences of the formal system express statements about the natural numbers. The incompleteness theorems are about formal provability within these systems, rather than about "provability" in an informal sense.

The incompleteness theorems apply to formal systems that are of sufficient complexity to express the basic arithmetic of the natural numbers and which are consistent and effectively axiomatized. Particularly in the context of first-order logic, formal systems are also called formal theories. In general, a formal system is a deductive apparatus that consists of a particular set of axioms along with rules of symbolic manipulation (or rules of inference) that allow for the derivation of new theorems from the axioms. One example of such a system is first-order Peano arithmetic, a system in which all variables are intended to denote natural numbers. In other systems, such as set theory, only some sentences of the formal system express statements about the natural numbers. The incompleteness theorems are about formal provability within these systems, rather than about "provability" in an informal sense.

= = 形式系统: 完备性、一致性和有效公理化 = = 不完备性定理适用于足够复杂的形式系统来表示自然数的基本算术，并且是一致的和有效公理化的。特别是在一阶逻辑的背景下，形式系统也被称为形式理论。一般来说，形式系统是一种演绎装置，它由一组特定的公理和符号操作规则(或推理规则)组成，这些规则允许从公理推导出新的定理。这样一个系统的一个例子是一阶 Peano 算术，其中所有变量的目的是表示自然数。在其他系统中，如集合论，只有形式系统中的一些句子表达关于自然数的陈述。不完备性定理是关于这些系统内部的形式可证明性，而不是非正式意义上的“可证明性”。

There are several properties that a formal system may have, including completeness, consistency, and the existence of an effective axiomatization. The incompleteness theorems show that systems which contain a sufficient amount of arithmetic cannot possess all three of these properties.

形式系统可能具有几个属性，包括完整性、一致性和有效公理化的存在。不完备性定理表明，具有足够数量算术的系统不可能具有所有这三个性质。

Effective axiomatization

= = 有效公理化 =

A formal system is said to be effectively axiomatized (also called effectively generated) if its set of theorems is a recursively enumerable set 模板:Harv.

A formal system is said to be effectively axiomatized (also called effectively generated) if its set of theorems is a recursively enumerable set .

如果一个形式系统的定理集是一个递归可枚举集合，那么它就是一个有效的公理化系统。

This means that there is a computer program that, in principle, could enumerate all the theorems of the system without listing any statements that are not theorems. Examples of effectively generated theories include Peano arithmetic and Zermelo–Fraenkel set theory (ZFC).

这意味着有一个计算机程序，原则上，可以列举系统的所有定理，而不列出任何不是定理的陈述。有效生成理论的例子包括 Peano 算法和 Zermelo-Fraenkel 集合理论(ZFC)。

The theory known as true arithmetic consists of all true statements about the standard integers in the language of Peano arithmetic. This theory is consistent and complete, and contains a sufficient amount of arithmetic. However it does not have a recursively enumerable set of axioms, and thus does not satisfy the hypotheses of the incompleteness theorems.

被称为真算术的理论包含了所有关于标准整数的真实陈述，这些陈述使用的是 Peano 算术语言。这个理论是一致的和完整的，并包含了足够的算术量。然而，它没有公理的递归可枚举集合，因此不满足不完备定理的假设。

Completeness

= 完整性 =

A set of axioms is (syntactically, or negation-) complete if, for any statement in the axioms' language, that statement or its negation is provable from the axioms 模板:Harv. This is the notion relevant for Gödel's first Incompleteness theorem. It is not to be confused with semantic completeness, which means that the set of axioms proves all the semantic tautologies of the given language. In his completeness theorem (not to be confused with the incompleteness theorems described here), Gödel proved that first order logic is semantically complete. But it is not syntactically complete, since there are sentences expressible in the language of first order logic that can be neither proved nor disproved from the axioms of logic alone.

A set of axioms is (syntactically, or negation-) complete if, for any statement in the axioms' language, that statement or its negation is provable from the axioms . This is the notion relevant for Gödel's first Incompleteness theorem. It is not to be confused with semantic completeness, which means that the set of axioms proves all the semantic tautologies of the given language. In his completeness theorem (not to be confused with the incompleteness theorems described here), Gödel proved that first order logic is semantically complete. But it is not syntactically complete, since there are sentences expressible in the language of first order logic that can be neither proved nor disproved from the axioms of logic alone.

如果对于公理语言中的任何语句，该语句或其否定可以从公理中证明，那么一组公理(语法上，或者说否定 -)是完整的。这个概念与哥德尔的第一个不完全性定理有关。不要把它与语义完全性混淆，这意味着公理集证明了给定语言的所有语义重言式。哥德尔在其完备性定理(不要与这里描述的不完备性定理相混淆)中证明了一阶逻辑是语义完备的。但是它在句法上是不完整的，因为有些句子可以用一阶逻辑的语言表达，仅仅从逻辑的公理中既不能证明也不能证伪。

In a mere system of logic it would be absurd to expect syntactic completeness.^{[citation needed]} But in a system of mathematics, thinkers such as Hilbert had believed that it is just a matter of time to find such an axiomatization that would allow one to either prove or disprove (by proving its negation) each and every mathematical formula.

In a mere system of logic it would be absurd to expect syntactic completeness. But in a system of mathematics, thinkers such as Hilbert had believed that it is just a matter of time to find such an axiomatization that would allow one to either prove or disprove (by proving its negation) each and every mathematical formula.

在一个纯粹的逻辑系统中，期望句法上的完整性是荒谬的。但在一个数学体系中，希尔伯特等思想家认为，找到这样一种公理化只是时间问题，它将允许人们证明或反驳(通过证明其否定)每一个数学公式。

A formal system might be syntactically incomplete by design, as logics generally are. Or it may be incomplete simply because not all the necessary axioms have been discovered or included. For example, Euclidean geometry without the parallel postulate is incomplete, because some statements in the language (such as the parallel postulate itself) can not be proved from the remaining axioms. Similarly, the theory of dense linear orders is not complete, but becomes complete with an extra axiom stating that there are no endpoints in the order. The continuum hypothesis is a statement in the language of ZFC that is not provable within ZFC, so ZFC is not complete. In this case, there is no obvious candidate for a new axiom that resolves the issue.

正式系统的语法设计可能不完整，正如逻辑学通常所做的那样。或者它可能是不完整的，仅仅因为并非所有必要的公理都被发现或包括在内。例如，欧几里得几何没有平行公设是不完整的，因为语言中的一些陈述(例如平行公设本身)不能从剩余的公理中得到证明。同样地，稠密线性序理论也不完整，但是在一个额外的公理声明序中没有终结点时就完整了。连续统假设是 ZFC 语言的一个声明，在 ZFC 中是不可证明的，所以 ZFC 是不完整的。在这种情况下，没有明显的新公理可以解决这个问题。

The theory of first order Peano arithmetic seems to be consistent. Assuming this is indeed the case, note that it has an infinite but recursively enumerable set of axioms, and can encode enough arithmetic for the hypotheses of the incompleteness theorem. Thus by the first incompleteness theorem, Peano Arithmetic is not complete. The theorem gives an explicit example of a statement of arithmetic that is neither provable nor disprovable in Peano's arithmetic. Moreover, this statement is true in the usual model. In addition, no effectively axiomatized, consistent extension of Peano arithmetic can be complete.

一阶 Peano 算术的理论似乎是一致的。假设情况确实如此，请注意，它有一个无限但递归可枚举集合的公理，并且可以为不完备定理的假设编码足够的算术。因此，根据第一不完备性定理，Peano 算术是不完备的。这个定理给出了一个明确的算术陈述的例子，在 Peano 的算术中既不能证明也不能推翻。此外，这种说法在通常的模型中是正确的。此外，没有有效的公理化，Peano 算术的一致扩展是完整的。

Consistency

A set of axioms is (simply) consistent if there is no statement such that both the statement and its negation are provable from the axioms, and inconsistent otherwise. That is to say, a consistent axiomatic system is one that is free from contradiction.

A set of axioms is (simply) consistent if there is no statement such that both the statement and its negation are provable from the axioms, and inconsistent otherwise. That is to say, a consistent axiomatic system is one that is free from contradiction.

= = = 一致性 = = = 一个公理集是(简单地)一致的，如果没有这样的语句，这样的语句和它的否定都可以从公理证明，否则不一致。也就是说，一致的公理系统是没有矛盾的。

Peano arithmetic is provably consistent from ZFC, but not from within itself. Similarly, ZFC is not provably consistent from within itself, but ZFC + "there exists an inaccessible cardinal" proves ZFC is consistent because if $κ$ is the least such cardinal, then $V κ$ sitting inside the von Neumann universe is a model of ZFC, and a theory is consistent if and only if it has a model.

Peano arithmetic is provably consistent from ZFC, but not from within itself. Similarly, ZFC is not provably consistent from within itself, but ZFC + "there exists an inaccessible cardinal" proves ZFC is consistent because if is the least such cardinal, then sitting inside the von Neumann universe is a model of ZFC, and a theory is consistent if and only if it has a model.

Peano 算法在 ZFC 中可以证明是一致的，但不是从内部来的。同样的，ZFC 本身也不能证明是一致的，但是 ZFC + “存在一个不可及基数”证明了 ZFC 是一致的，因为如果 ZFC 是最小的基数，那么坐在冯·诺伊曼全集里面就是 ZFC 的一个模型，一个理论是一致的当且仅当它有一个模型。

If one takes all statements in the language of Peano arithmetic as axioms, then this theory is complete, has a recursively enumerable set of axioms, and can describe addition and multiplication. However, it is not consistent.

如果一个人把所有用 Peano 算术语言写的陈述都当作公理，那么这个理论就是完整的，有一个递归可枚举集合的公理，并且能够描述加法和乘法。然而，这并不一致。

Additional examples of inconsistent theories arise from the paradoxes that result when the axiom schema of unrestricted comprehension is assumed in set theory.

集合论中假设无限制理解的公理图式所产生的悖论，也引出了不一致理论的其他例子。

Systems which contain arithmetic

= = 包含算术的系统 = =

The incompleteness theorems apply only to formal systems which are able to prove a sufficient collection of facts about the natural numbers. One sufficient collection is the set of theorems of Robinson arithmetic $Q$ . Some systems, such as Peano arithmetic, can directly express statements about natural numbers. Others, such as ZFC set theory, are able to interpret statements about natural numbers into their language. Either of these options is appropriate for the incompleteness theorems.

The incompleteness theorems apply only to formal systems which are able to prove a sufficient collection of facts about the natural numbers. One sufficient collection is the set of theorems of Robinson arithmetic . Some systems, such as Peano arithmetic, can directly express statements about natural numbers. Others, such as ZFC set theory, are able to interpret statements about natural numbers into their language. Either of these options is appropriate for the incompleteness theorems.

不完备性定理仅适用于能够证明关于自然数的充分事实集合的形式系统。一个充分的集合就是鲁宾逊算术定理的集合。有些系统，例如 Peano 算术，可以直接表达关于自然数的陈述。其他的，比如 ZFC 集合论，能够用他们的语言来解释关于自然数的陈述。这些选项中的任何一个都适用于不完备性定理。

The theory of algebraically closed fields of a given characteristic is complete, consistent, and has an infinite but recursively enumerable set of axioms. However it is not possible to encode the integers into this theory, and the theory cannot describe arithmetic of integers. A similar example is the theory of real closed fields, which is essentially equivalent to Tarski's axioms for Euclidean geometry. So Euclidean geometry itself (in Tarski's formulation) is an example of a complete, consistent, effectively axiomatized theory.

特征符号代数闭域的理论是完整的、一致的，并且有一个无限的公理递归可枚举集合。然而，对整数进行编码是不可能的，这种理论也不能描述整数的算术运算。一个类似的例子是实闭域理论，这在本质上等价于 Tarski 的欧几里得几何公理。因此，欧几里得几何本身就是一个完整的、一致的、有效的公理化理论的例子。

The system of Presburger arithmetic consists of a set of axioms for the natural numbers with just the addition operation (multiplication is omitted). Presburger arithmetic is complete, consistent, and recursively enumerable and can encode addition but not multiplication of natural numbers, showing that for Gödel's theorems one needs the theory to encode not just addition but also multiplication.

Presburger 算术系统由一组自然数的公理组成，只需要加法运算(省略乘法)。普雷斯伯格算术是完整的，一致的，递归的可数的，可以编码加法而不是自然数的乘法，这表明对于哥德尔定理，人们不仅需要编码加法，还需要编码乘法。

模板:Harvard citations has studied some weak families of arithmetic systems which allow enough arithmetic as relations to formalise Gödel numbering, but which are not strong enough to have multiplication as a function, and so fail to prove the second incompleteness theorem; that is to say, these systems are consistent and capable of proving their own consistency (see self-verifying theories).

has studied some weak families of arithmetic systems which allow enough arithmetic as relations to formalise Gödel numbering, but which are not strong enough to have multiplication as a function, and so fail to prove the second incompleteness theorem; that is to say, these systems are consistent and capable of proving their own consistency (see self-verifying theories).

已经研究了一些弱算术系统，这些算术系统允许足够的算术作为关系来形式化哥德尔编号，但是它们不够强大，不足以有乘法作为一个函数，因此不能证明第二个不完备定理，也就是说，这些系统是一致的，并能够证明自己的一致性(见自我验证理论)。

Conflicting goals

In choosing a set of axioms, one goal is to be able to prove as many correct results as possible, without proving any incorrect results. For example, we could imagine a set of true axioms which allow us to prove every true arithmetical claim about the natural numbers 模板:Harv. In the standard system of first-order logic, an inconsistent set of axioms will prove every statement in its language (this is sometimes called the principle of explosion), and is thus automatically complete. A set of axioms that is both complete and consistent, however, proves a maximal set of non-contradictory theorems 模板:Harv.

In choosing a set of axioms, one goal is to be able to prove as many correct results as possible, without proving any incorrect results. For example, we could imagine a set of true axioms which allow us to prove every true arithmetical claim about the natural numbers . In the standard system of first-order logic, an inconsistent set of axioms will prove every statement in its language (this is sometimes called the principle of explosion), and is thus automatically complete. A set of axioms that is both complete and consistent, however, proves a maximal set of non-contradictory theorems .

在选择一组公理时，一个目标是能够证明尽可能多的正确结果，而不是证明任何错误的结果。例如，我们可以想象一组真正的公理，它们允许我们证明关于自然数的每一个真正的算术断言。在一阶逻辑的标准体系中，一个不一致的公理集将用它的语言证明每个陈述(这有时被称为爆炸原理) ，因此是自动完成的。然而，一组既完备又一致的公理证明了一组极大的非矛盾定理。

The pattern illustrated in the previous sections with Peano arithmetic, ZFC, and ZFC + "there exists an inaccessible cardinal" cannot generally be broken. Here ZFC + "there exists an inaccessible cardinal" cannot from itself, be proved consistent. It is also not complete, as illustrated by the in ZFC + "there exists an inaccessible cardinal" theory unresolved continuum hypothesis.

前面几节用 Peano 算术、 ZFC 和 ZFC + “存在一个不可及基数”说明的模式一般不能被打破。这里 ZFC + “存在一个不可及基数”不能从本身出发，被证明是一致的。它也是不完整的，正如 ZFC + 中说明的那样，“存在一个不可及基数”理论没有解决连续统假设。

The first incompleteness theorem shows that, in formal systems that can express basic arithmetic, a complete and consistent finite list of axioms can never be created: each time an additional, consistent statement is added as an axiom, there are other true statements that still cannot be proved, even with the new axiom. If an axiom is ever added that makes the system complete, it does so at the cost of making the system inconsistent. It is not even possible for an infinite list of axioms to be complete, consistent, and effectively axiomatized.

第一个不完备性定理表明，在可以表达基本算术的形式系统中，一个完整的、一致的有限公理列表是永远不可能创建的: 每次一个额外的、一致的陈述作为一个公理被添加，还有其他一些真实的陈述仍然不能被证明，即使使用新的公理。如果添加了使系统完整的公理，那么这样做的代价是使系统不一致。一个公理的无限列表是完整的、一致的、有效的公理化是不可能的。

First incompleteness theorem

Gödel's first incompleteness theorem first appeared as "Theorem VI" in Gödel's 1931 paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I". The hypotheses of the theorem were improved shortly thereafter by 模板:Harvs using Rosser's trick. The resulting theorem (incorporating Rosser's improvement) may be paraphrased in English as follows, where "formal system" includes the assumption that the system is effectively generated.

Gödel's first incompleteness theorem first appeared as "Theorem VI" in Gödel's 1931 paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I". The hypotheses of the theorem were improved shortly thereafter by using Rosser's trick. The resulting theorem (incorporating Rosser's improvement) may be paraphrased in English as follows, where "formal system" includes the assumption that the system is effectively generated.

= = 第一个不完备性定理 = = 哥德尔的第一个不完备性定理作为“定理六”首次出现在哥德尔1931年的论文《论数学原理及相关系统 i 的形式不可判定命题》中。这个定理的假设很快就被罗塞尔的技巧改进了。结果定理(包括罗塞尔的改进)可以用英语解释如下，其中“形式系统”包括假设系统是有效生成的。

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)

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

第一个不完备性定理: “任何一个一致的形式系统，在这个系统中可以执行一定数量的四则运算，这是不完备的; 也就是说，有些语言的陈述既不能被证明也不能被否定。”(Raatikainen 2015)

The unprovable statement $G F$ referred to by the theorem is often referred to as "the Gödel sentence" for the system $F$ . The proof constructs a particular Gödel sentence for the system $F$ , but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence.

The unprovable statement referred to by the theorem is often referred to as "the Gödel sentence" for the system . The proof constructs a particular Gödel sentence for the system , but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence.

这个定理所引用的无法证明的陈述，通常被称为系统的“哥德尔句”。证明为系统构造了一个特定的哥德尔句子，但是在系统的语言中有无限多的语句具有相同的性质，例如哥德尔句子的连接词和任何逻辑上有效的句子。

Each effectively generated system has its own Gödel sentence. It is possible to define a larger system $F'$ that contains the whole of $F$ plus $G F$ as an additional axiom. This will not result in a complete system, because Gödel's theorem will also apply to $F'$ , and thus $F'$ also cannot be complete. In this case, $G F$ is indeed a theorem in $F'$ , because it is an axiom. Because $G F$ states only that it is not provable in $F$ , no contradiction is presented by its provability within $F'$ . However, because the incompleteness theorem applies to $F'$ , there will be a new Gödel statement $G F'$ for $F'$ , showing that $F'$ is also incomplete. $G F'$ will differ from $G F$ in that $G F'$ will refer to $F'$ , rather than $F$ .

Each effectively generated system has its own Gödel sentence. It is possible to define a larger system that contains the whole of plus as an additional axiom. This will not result in a complete system, because Gödel's theorem will also apply to , and thus also cannot be complete. In this case, is indeed a theorem in , because it is an axiom. Because states only that it is not provable in , no contradiction is presented by its provability within . However, because the incompleteness theorem applies to , there will be a new Gödel statement for , showing that is also incomplete. will differ from in that will refer to , rather than .

每个有效生成的系统都有自己的哥德尔句子。我们可以定义一个更大的系统，将整个 + 作为一个额外的公理。这不会导致一个完整的系统，因为哥德尔定理也适用于，因此也不能完整。在这种情况下，的确是一个定理，因为它是一个公理。因为它只是无法证明的状态，所以它的内在可证明性并不能表现出矛盾。然而，由于不完备性定理适用于年，将会有一个新的哥德尔陈述，表明这也是不完备的。不同之处在于，它指的是。

Syntactic form of the Gödel sentence

= = 哥德尔句子的句法形式 =

The Gödel sentence is designed to refer, indirectly, to itself. The sentence states that, when a particular sequence of steps is used to construct another sentence, that constructed sentence will not be provable in $F$ . However, the sequence of steps is such that the constructed sentence turns out to be $G F$ itself. In this way, the Gödel sentence $G F$ indirectly states its own unprovability within $F$ 模板:Harv.

The Gödel sentence is designed to refer, indirectly, to itself. The sentence states that, when a particular sequence of steps is used to construct another sentence, that constructed sentence will not be provable in . However, the sequence of steps is such that the constructed sentence turns out to be itself. In this way, the Gödel sentence indirectly states its own unprovability within .

哥德尔句子被设计成间接地指向自己。这个句子指出，当一个特定的步骤序列被用来构造另一个句子时，这个构造的句子将不能被证明。然而，步骤的顺序是这样的，构造出来的句子原来就是它自己。以这种方式，哥德尔句间接地陈述了它自己的内在无法证明。

To prove the first incompleteness theorem, Gödel demonstrated that the notion of provability within a system could be expressed purely in terms of arithmetical functions that operate on Gödel numbers of sentences of the system. Therefore, the system, which can prove certain facts about numbers, can also indirectly prove facts about its own statements, provided that it is effectively generated. Questions about the provability of statements within the system are represented as questions about the arithmetical properties of numbers themselves, which would be decidable by the system if it were complete.

为了证明第一个不完备性定理，哥德尔证明了系统内可证明性的概念可以纯粹地用运算系统句子的哥德尔数的算术函数来表示。因此，能够证明数字某些事实的系统，也可以间接证明自己陈述的事实，只要它是有效生成的。关于系统内语句的可证明性的问题被表示为关于数本身的算术性质的问题，如果它是完整的，系统将可判定。

Thus, although the Gödel sentence refers indirectly to sentences of the system $F$ , when read as an arithmetical statement the Gödel sentence directly refers only to natural numbers. It asserts that no natural number has a particular property, where that property is given by a primitive recursive relation 模板:Harv. As such, the Gödel sentence can be written in the language of arithmetic with a simple syntactic form. In particular, it can be expressed as a formula in the language of arithmetic consisting of a number of leading universal quantifiers followed by a quantifier-free body (these formulas are at level [math]\displaystyle{ \Pi^0_1 }[/math] of the arithmetical hierarchy). Via the MRDP theorem, the Gödel sentence can be re-written as a statement that a particular polynomial in many variables with integer coefficients never takes the value zero when integers are substituted for its variables 模板:Harv.

Thus, although the Gödel sentence refers indirectly to sentences of the system , when read as an arithmetical statement the Gödel sentence directly refers only to natural numbers. It asserts that no natural number has a particular property, where that property is given by a primitive recursive relation . As such, the Gödel sentence can be written in the language of arithmetic with a simple syntactic form. In particular, it can be expressed as a formula in the language of arithmetic consisting of a number of leading universal quantifiers followed by a quantifier-free body (these formulas are at level \Pi^0_1 of the arithmetical hierarchy). Via the MRDP theorem, the Gödel sentence can be re-written as a statement that a particular polynomial in many variables with integer coefficients never takes the value zero when integers are substituted for its variables .

因此，尽管哥德尔句子间接引用了系统中的句子，但当作为算术语句读时，哥德尔句子只直接引用了自然数。它断言任何自然数都不具有特定的性质，而这种性质是由原始递归关系给出的。因此，哥德尔句子可以用简单的句法形式用算术语言书写。特别是，它可以用算术语言表示为一个公式，该语言由一些前导的通用量词和一个无量词体组成(这些公式在算数阶层的 Pi ^ 0 _ 1级)。通过 MRDP 定理，可以将哥德尔语句重写为一个语句，即当整数被取代时，具有整数系数的多元特定多项式绝不取值为零。

Truth of the Gödel sentence

= = 哥德尔句子的真理 =

The first incompleteness theorem shows that the Gödel sentence $G F$ of an appropriate formal theory $F$ is unprovable in $F$ . Because, when interpreted as a statement about arithmetic, this unprovability is exactly what the sentence (indirectly) asserts, the Gödel sentence is, in fact, true (脚本错误：没有“Footnotes”这个模块。; also see 脚本错误：没有“Footnotes”这个模块。). For this reason, the sentence $G F$ is often said to be "true but unprovable." 模板:Harv. However, since the Gödel sentence cannot itself formally specify its intended interpretation, the truth of the sentence $G F$ may only be arrived at via a meta-analysis from outside the system. In general, this meta-analysis can be carried out within the weak formal system known as primitive recursive arithmetic, which proves the implication $Con (F)\to G F$ , where $Con (F)$ is a canonical sentence asserting the consistency of $F$ (脚本错误：没有“Footnotes”这个模块。, 脚本错误：没有“Footnotes”这个模块。).

The first incompleteness theorem shows that the Gödel sentence of an appropriate formal theory is unprovable in . Because, when interpreted as a statement about arithmetic, this unprovability is exactly what the sentence (indirectly) asserts, the Gödel sentence is, in fact, true (; also see ). For this reason, the sentence is often said to be "true but unprovable." . However, since the Gödel sentence cannot itself formally specify its intended interpretation, the truth of the sentence may only be arrived at via a meta-analysis from outside the system. In general, this meta-analysis can be carried out within the weak formal system known as primitive recursive arithmetic, which proves the implication , where is a canonical sentence asserting the consistency of (, ).

第一个不完备性定理表明，一个恰当的形式理论的哥德尔语句是不可证明的。因为，当解释为一个关于算术的陈述时，这种不可证性正是句子(间接地)所断言的，哥德尔句子事实上是真的(; 也见)。由于这个原因，这个句子通常被认为是“真实的，但是无法证明”.然而，由于哥德尔句子本身不能正式确定它的预期释义，这个句子的真实性只能通过系统外的元分析才能得到。一般来说，这种元分析可以在弱形式系统中进行，这种弱形式系统称为原始递归算法，它证明了蕴涵，其中一个规范句子断言(,)的一致性。

Although the Gödel sentence of a consistent theory is true as a statement about the intended interpretation of arithmetic, the Gödel sentence will be false in some nonstandard models of arithmetic, as a consequence of Gödel's completeness theorem 模板:Harv. That theorem shows that, when a sentence is independent of a theory, the theory will have models in which the sentence is true and models in which the sentence is false. As described earlier, the Gödel sentence of a system $F$ is an arithmetical statement which claims that no number exists with a particular property. The incompleteness theorem shows that this claim will be independent of the system $F$ , and the truth of the Gödel sentence follows from the fact that no standard natural number has the property in question. Any model in which the Gödel sentence is false must contain some element which satisfies the property within that model. Such a model must be "nonstandard" – it must contain elements that do not correspond to any standard natural number (脚本错误：没有“Footnotes”这个模块。, 脚本错误：没有“Footnotes”这个模块。).

Although the Gödel sentence of a consistent theory is true as a statement about the intended interpretation of arithmetic, the Gödel sentence will be false in some nonstandard models of arithmetic, as a consequence of Gödel's completeness theorem . That theorem shows that, when a sentence is independent of a theory, the theory will have models in which the sentence is true and models in which the sentence is false. As described earlier, the Gödel sentence of a system is an arithmetical statement which claims that no number exists with a particular property. The incompleteness theorem shows that this claim will be independent of the system , and the truth of the Gödel sentence follows from the fact that no standard natural number has the property in question. Any model in which the Gödel sentence is false must contain some element which satisfies the property within that model. Such a model must be "nonstandard" – it must contain elements that do not correspond to any standard natural number (, ).

虽然一致性理论中的哥德尔句子作为算术预期释义的陈述是真实的，但是由于哥德尔的完备性定理，哥德尔句子在一些非标准的算术模型中是错误的。这个定理表明，当一个句子独立于一个理论时，该理论将有句子为真的模型和句子为假的模型。如前所述，一个系统的哥德尔句是一个算术陈述，声称没有数字存在与一个特定的性质。不完备性定理表明，这一主张是独立于系统的，哥德尔句的真理来自于没有标准自然数具有所讨论的性质这一事实。任何 Gödel 句子为 false 的模型必须包含某个满足该模型中的性质的元素。这样的模型必须是“非标准的”——它必须包含不对应于任何标准自然数(,)的元素。

Relationship with the liar paradox

= 与说谎者悖论的关系 =

Gödel specifically cites Richard's paradox and the liar paradox as semantical analogues to his syntactical incompleteness result in the introductory section of "On Formally Undecidable Propositions in Principia Mathematica and Related Systems I". The liar paradox is the sentence "This sentence is false." An analysis of the liar sentence shows that it cannot be true (for then, as it asserts, it is false), nor can it be false (for then, it is true). A Gödel sentence $G$ for a system $F$ makes a similar assertion to the liar sentence, but with truth replaced by provability: $G$ says " $G$ is not provable in the system $F$ ." The analysis of the truth and provability of $G$ is a formalized version of the analysis of the truth of the liar sentence.

Gödel specifically cites Richard's paradox and the liar paradox as semantical analogues to his syntactical incompleteness result in the introductory section of "On Formally Undecidable Propositions in Principia Mathematica and Related Systems I". The liar paradox is the sentence "This sentence is false." An analysis of the liar sentence shows that it cannot be true (for then, as it asserts, it is false), nor can it be false (for then, it is true). A Gödel sentence for a system makes a similar assertion to the liar sentence, but with truth replaced by provability: says " is not provable in the system ." The analysis of the truth and provability of is a formalized version of the analysis of the truth of the liar sentence.

哥德尔特别引用了 Richard 的悖论和说谎者悖论作为语义类比，来对他的句法不完整性结果进行语义类比，这一结果出现在《论数学原理和相关系统 i 中的正式不可判定命题》的导言部分。说谎者悖论就是“这句话是假的”这句话对撒谎者句子的分析表明，它不可能是真的(因为它断言，它是假的) ，也不可能是假的(因为它是真的)。一个系统的哥德尔句子和说谎者句子做出了类似的断言，但真理被可证明性所取代: 说“在系统中是不可证明的”真理分析和可证明性分析是说谎者句子真理分析的形式化版本。

It is not possible to replace "not provable" with "false" in a Gödel sentence because the predicate " $Q$ is the Gödel number of a false formula" cannot be represented as a formula of arithmetic. This result, known as Tarski's undefinability theorem, was discovered independently both by Gödel, when he was working on the proof of the incompleteness theorem, and by the theorem's namesake, Alfred Tarski.

It is not possible to replace "not provable" with "false" in a Gödel sentence because the predicate " is the Gödel number of a false formula" cannot be represented as a formula of arithmetic. This result, known as Tarski's undefinability theorem, was discovered independently both by Gödel, when he was working on the proof of the incompleteness theorem, and by the theorem's namesake, Alfred Tarski.

在哥德尔句子中，不可能用“ false”代替“ not provedable”，因为谓词“ is the Gödel number of a false formula”不能表示为算术公式。这个结果，被称为塔尔斯基的不可定性定理，是由哥德尔和阿尔弗雷德 · 塔尔斯基独立发现的，当时他正在研究不完备性定理的证明。

Extensions of Gödel's original result

= = 哥德尔原始结果的扩展 = =

Compared to the theorems stated in Gödel's 1931 paper, many contemporary statements of the incompleteness theorems are more general in two ways. These generalized statements are phrased to apply to a broader class of systems, and they are phrased to incorporate weaker consistency assumptions.

与哥德尔在1931年的论文中提出的定理相比，许多当代的不完备性定理在两个方面更具普遍性。这些广义的陈述被用来适用于更广泛的系统类别，它们被用来包含较弱的一致性假设。

Gödel demonstrated the incompleteness of the system of Principia Mathematica, a particular system of arithmetic, but a parallel demonstration could be given for any effective system of a certain expressiveness. Gödel commented on this fact in the introduction to his paper, but restricted the proof to one system for concreteness. In modern statements of the theorem, it is common to state the effectiveness and expressiveness conditions as hypotheses for the incompleteness theorem, so that it is not limited to any particular formal system. The terminology used to state these conditions was not yet developed in 1931 when Gödel published his results.

Gödel demonstrated the incompleteness of the system of Principia Mathematica, a particular system of arithmetic, but a parallel demonstration could be given for any effective system of a certain expressiveness. Gödel commented on this fact in the introduction to his paper, but restricted the proof to one system for concreteness. In modern statements of the theorem, it is common to state the effectiveness and expressiveness conditions as hypotheses for the incompleteness theorem, so that it is not limited to any particular formal system. The terminology used to state these conditions was not yet developed in 1931 when Gödel published his results.

哥德尔论证了数学原理系统的不完备性，这是一个特殊的算术系统，但是对于任何具有一定表达能力的有效系统，可以给出一个并行的论证。哥德尔在他的论文的导言中对这一事实进行了评论，但是将证明限制在一个具体的体系中。在定理的现代表述中，通常将有效性和表达性条件作为不完备性定理的假设来表述，这样它就不局限于任何特定的形式系统。在1931年哥德尔发表他的研究结果时，用来描述这些情况的术语还没有发展起来。

Gödel's original statement and proof of the incompleteness theorem requires the assumption that the system is not just consistent but ω-consistent. A system is ω-consistent if it is not ω-inconsistent, and is ω-inconsistent if there is a predicate $P$ such that for every specific natural number $m$ the system proves $~ P (m)$ , and yet the system also proves that there exists a natural number $n$ such that $P$ ( $n$ ). That is, the system says that a number with property $P$ exists while denying that it has any specific value. The ω-consistency of a system implies its consistency, but consistency does not imply ω-consistency. 模板:Harvard citations strengthened the incompleteness theorem by finding a variation of the proof (Rosser's trick) that only requires the system to be consistent, rather than ω-consistent. This is mostly of technical interest, because all true formal theories of arithmetic (theories whose axioms are all true statements about natural numbers) are ω-consistent, and thus Gödel's theorem as originally stated applies to them. The stronger version of the incompleteness theorem that only assumes consistency, rather than ω-consistency, is now commonly known as Gödel's incompleteness theorem and as the Gödel–Rosser theorem.

Gödel's original statement and proof of the incompleteness theorem requires the assumption that the system is not just consistent but ω-consistent. A system is ω-consistent if it is not ω-inconsistent, and is ω-inconsistent if there is a predicate such that for every specific natural number the system proves , and yet the system also proves that there exists a natural number such that (). That is, the system says that a number with property exists while denying that it has any specific value. The ω-consistency of a system implies its consistency, but consistency does not imply ω-consistency. strengthened the incompleteness theorem by finding a variation of the proof (Rosser's trick) that only requires the system to be consistent, rather than ω-consistent. This is mostly of technical interest, because all true formal theories of arithmetic (theories whose axioms are all true statements about natural numbers) are ω-consistent, and thus Gödel's theorem as originally stated applies to them. The stronger version of the incompleteness theorem that only assumes consistency, rather than ω-consistency, is now commonly known as Gödel's incompleteness theorem and as the Gödel–Rosser theorem.

哥德尔对不完备性定理的原始陈述和证明需要假设系统不仅是一致的，而且是 ω- 一致的。一个系统如果不是 ω- 不相容的，则是 ω- 不相容的; 如果存在一个谓词使得系统对每一个特定的自然数都能证明，则系统是 ω- 不相容的，而且系统还证明了存在一个自然数使得()。也就是说，系统认为一个具有属性的数字存在，同时否认它具有任何特定的值。系统的 ω- 一致性意味着系统的 ω- 一致性，但是一致性并不意味着系统的 ω- 一致性。通过找到证明的一种变形(罗瑟的技巧) ，加强了不完备性定理，即只要求系统是一致的，而不是 ω- 一致的。这主要是技术上的兴趣，因为所有真正的算术形式理论(其公理都是关于自然数的真实陈述的理论)都是 ω- 一致的，因此哥德尔定理最初的陈述适用于它们。不完备性定理的更强版本只假设一致性，而不是 ω- 一致性，现在通常被称为哥德尔不完备性定理和哥德尔-罗塞尔定理。

Second incompleteness theorem

= 第二个不完备性定理 =

For each formal system $F$ containing basic arithmetic, it is possible to canonically define a formula Cons( $F$ ) expressing the consistency of $F$ . This formula expresses the property that "there does not exist a natural number coding a formal derivation within the system $F$ whose conclusion is a syntactic contradiction." The syntactic contradiction is often taken to be "0=1", in which case Cons( $F$ ) states "there is no natural number that codes a derivation of '0=1' from the axioms of $F$ ."

For each formal system containing basic arithmetic, it is possible to canonically define a formula Cons() expressing the consistency of . This formula expresses the property that "there does not exist a natural number coding a formal derivation within the system whose conclusion is a syntactic contradiction." The syntactic contradiction is often taken to be "0=1", in which case Cons() states "there is no natural number that codes a derivation of '0=1' from the axioms of ."

对于每个包含基本算术的形式系统，可以规范地定义一个公式 Cons ()来表示。这个公式表达了这样一个性质: “系统中不存在一个自然数来编码一个形式推导，其结论是句法矛盾的”句法上的矛盾通常被认为是“0 = 1”，在这种情况下 Cons ()表示“没有一个自然数可以从公理中推导出‘0 = 1’。”

Gödel's second incompleteness theorem shows that, under general assumptions, this canonical consistency statement Cons( $F$ ) will not be provable in $F$ . The theorem first appeared as "Theorem XI" in Gödel's 1931 paper "On Formally Undecidable Propositions in Principia Mathematica and Related Systems I". In the following statement, the term "formalized system" also includes an assumption that $F$ is effectively axiomatized.

Gödel's second incompleteness theorem shows that, under general assumptions, this canonical consistency statement Cons() will not be provable in . The theorem first appeared as "Theorem XI" in Gödel's 1931 paper "On Formally Undecidable Propositions in Principia Mathematica and Related Systems I". In the following statement, the term "formalized system" also includes an assumption that is effectively axiomatized.

哥德尔的第二个不完备性定理表明，在一般假设下，这个典范一致性陈述 Cons ()在年是不可证明的。这个定理最早以“定理 XI”的形式出现在哥德尔1931年的论文《论数学原理及相关系统 i 中的形式不可判定命题》中。在下面的陈述中，“形式化系统”这个术语还包括一个实际上已经公理化的假设。

Second Incompleteness Theorem: "Assume $F$ is a consistent formalized system which contains elementary arithmetic. Then [math]\displaystyle{ F \not \vdash \text{Cons}(F) }[/math]." 模板:Harv

Second Incompleteness Theorem: "Assume is a consistent formalized system which contains elementary arithmetic. Then F \not \vdash \text{Cons}(F)."

第二个不完备性定理: “假设是一个包含四则运算的一致形式化系统。然后 f not vdash text { Cons }(f)”

This theorem is stronger than the first incompleteness theorem because the statement constructed in the first incompleteness theorem does not directly express the consistency of the system. The proof of the second incompleteness theorem is obtained by formalizing the proof of the first incompleteness theorem within the system $F$ itself.

This theorem is stronger than the first incompleteness theorem because the statement constructed in the first incompleteness theorem does not directly express the consistency of the system. The proof of the second incompleteness theorem is obtained by formalizing the proof of the first incompleteness theorem within the system itself.

这个定理比第一个不完备性定理要强，因为第一个不完备性定理构造的陈述并不直接表示系统的一致性。第二个不完备性定理的证明是通过在系统内部形式化第一个不完备性定理的证明而得到的。

Expressing consistency

= = 表达一致性 =

There is a technical subtlety in the second incompleteness theorem regarding the method of expressing the consistency of $F$ as a formula in the language of $F$ . There are many ways to express the consistency of a system, and not all of them lead to the same result. The formula Cons( $F$ ) from the second incompleteness theorem is a particular expression of consistency.

There is a technical subtlety in the second incompleteness theorem regarding the method of expressing the consistency of as a formula in the language of . There are many ways to express the consistency of a system, and not all of them lead to the same result. The formula Cons() from the second incompleteness theorem is a particular expression of consistency.

在第二个不完备性定理中，有一个技术上的微妙之处，它涉及到用公式的语言来表示一致性的方法。表示系统一致性的方法有很多，但并不是所有的方法都能得到相同的结果。第二个不完备性定理中的公式 Cons ()是一个相容性的特殊表达式。

Other formalizations of the claim that $F$ is consistent may be inequivalent in $F$ , and some may even be provable. For example, first-order Peano arithmetic (PA) can prove that "the largest consistent subset of PA" is consistent. But, because PA is consistent, the largest consistent subset of PA is just PA, so in this sense PA "proves that it is consistent". What PA does not prove is that the largest consistent subset of PA is, in fact, the whole of PA. (The term "largest consistent subset of PA" is meant here to be the largest consistent initial segment of the axioms of PA under some particular effective enumeration.)

Other formalizations of the claim that is consistent may be inequivalent in , and some may even be provable. For example, first-order Peano arithmetic (PA) can prove that "the largest consistent subset of PA" is consistent. But, because PA is consistent, the largest consistent subset of PA is just PA, so in this sense PA "proves that it is consistent". What PA does not prove is that the largest consistent subset of PA is, in fact, the whole of PA. (The term "largest consistent subset of PA" is meant here to be the largest consistent initial segment of the axioms of PA under some particular effective enumeration.)

其他形式化的声称是一致的可能是不等价的，在年，有些甚至可以证明。例如，一阶 Peano 算法(PA)可以证明“ PA 的最大一致子集”是一致的。但是，因为 PA 是一致的，PA 的最大一致子集只是 PA，所以在这个意义上 PA“证明了它是一致的”。PA 没有证明的是 PA 的最大一致子集实际上是 PA 的整体(术语“ PA 的最大一致子集”在这里的意思是在某些特定的有效枚举下 PA 公理的最大一致初始段)

The Hilbert–Bernays conditions

= 希尔伯特-伯奈斯条件 =

The standard proof of the second incompleteness theorem assumes that the provability predicate $Prov A (P)$ satisfies the Hilbert–Bernays provability conditions. Letting $#(P)$ represent the Gödel number of a formula $P$ , the provability conditions say:

The standard proof of the second incompleteness theorem assumes that the provability predicate satisfies the Hilbert–Bernays provability conditions. Letting represent the Gödel number of a formula , the provability conditions say:

第二个不完备性定理的标准证明假定可证明谓词满足 Hilbert-Bernays 可证明条件。让我们来看一个公式的哥德尔数，可证条件是:

If $F$ proves $P$ , then $F$ proves $Prov A (#(P))$ .
$F$ proves 1.; that is, $F$ proves $Prov A (#(P)) \to Prov A (#(Prov A (#(P))))$ .
$F$ proves $Prov A (#(P \to Q)) \land Prov A (#(P)) \to Prov A (#(Q))$ (analogue of modus ponens).

If proves , then proves .
proves 1.; that is, proves .
proves (analogue of modus ponens).

如果证明，那么证明。证明1: 那就是证明。“证明”(与否定式类似)。

There are systems, such as Robinson arithmetic, which are strong enough to meet the assumptions of the first incompleteness theorem, but which do not prove the Hilbert–Bernays conditions. Peano arithmetic, however, is strong enough to verify these conditions, as are all theories stronger than Peano arithmetic.

有一些系统，比如鲁宾逊算术系统，它们强大到足以满足第一个不完备性定理的假设，但它们不能证明希尔伯特-伯奈斯条件。然而，Peano 算法足够强大，可以验证这些条件，所有的理论都比 Peano 算法强大。

Implications for consistency proofs

= = 影响一致性证明 = =

Gödel's second incompleteness theorem also implies that a system $F 1$ satisfying the technical conditions outlined above cannot prove the consistency of any system $F 2$ that proves the consistency of $F 1$ . This is because such a system $F 1$ can prove that if $F 2$ proves the consistency of $F 1$ , then $F 1$ is in fact consistent. For the claim that $F 1$ is consistent has form "for all numbers $n$ , $n$ has the decidable property of not being a code for a proof of contradiction in $F 1$ ". If $F 1$ were in fact inconsistent, then $F 2$ would prove for some $n$ that $n$ is the code of a contradiction in $F 1$ . But if $F 2$ also proved that $F 1$ is consistent (that is, that there is no such $n$ ), then it would itself be inconsistent. This reasoning can be formalized in $F 1$ to show that if $F 2$ is consistent, then $F 1$ is consistent. Since, by second incompleteness theorem, $F 1$ does not prove its consistency, it cannot prove the consistency of $F 2$ either.

Gödel's second incompleteness theorem also implies that a system satisfying the technical conditions outlined above cannot prove the consistency of any system that proves the consistency of . This is because such a system can prove that if proves the consistency of , then is in fact consistent. For the claim that is consistent has form "for all numbers , has the decidable property of not being a code for a proof of contradiction in ". If were in fact inconsistent, then would prove for some that is the code of a contradiction in . But if also proved that is consistent (that is, that there is no such ), then it would itself be inconsistent. This reasoning can be formalized in to show that if is consistent, then is consistent. Since, by second incompleteness theorem, does not prove its consistency, it cannot prove the consistency of either.

哥德尔的第二个不完备性定理也意味着，满足上述技术条件的系统不能证明任何系统的一致性。这是因为这样一个系统可以证明，如果证明了一致性，那么其实是一致的。对于一致性的权利要求具有“对所有数字，具有不是矛盾证明码的可判定性”。如果事实上是不一致的，那么就会证明对某些人来说那是一种矛盾的密码。但是，如果也证明了这是一致的(也就是说，没有这样的) ，那么它本身就是不一致的。这种推理可以形式化地表明，如果是一致的，那么就是一致的。由于第二不完备性定理不能证明它的一致性，因此也不能证明它们的一致性。

This corollary of the second incompleteness theorem shows that there is no hope of proving, for example, the consistency of Peano arithmetic using any finitistic means that can be formalized in a system the consistency of which is provable in Peano arithmetic (PA). For example, the system of primitive recursive arithmetic (PRA), which is widely accepted as an accurate formalization of finitistic mathematics, is provably consistent in PA. Thus PRA cannot prove the consistency of PA. This fact is generally seen to imply that Hilbert's program, which aimed to justify the use of "ideal" (infinitistic) mathematical principles in the proofs of "real" (finitistic) mathematical statements by giving a finitistic proof that the ideal principles are consistent, cannot be carried out 模板:Harv.

This corollary of the second incompleteness theorem shows that there is no hope of proving, for example, the consistency of Peano arithmetic using any finitistic means that can be formalized in a system the consistency of which is provable in Peano arithmetic (PA). For example, the system of primitive recursive arithmetic (PRA), which is widely accepted as an accurate formalization of finitistic mathematics, is provably consistent in PA. Thus PRA cannot prove the consistency of PA. This fact is generally seen to imply that Hilbert's program, which aimed to justify the use of "ideal" (infinitistic) mathematical principles in the proofs of "real" (finitistic) mathematical statements by giving a finitistic proof that the ideal principles are consistent, cannot be carried out .

第二个不完备性定理的这一推论表明，没有希望证明，例如，Peano 算法的一致性可以用任何有限手段在一个系统中形式化，而这个系统的一致性在 Peano 算法(PA)中是可以证明的。例如，被广泛认为是有限数学精确形式化的原始递归算法(PRA)系统在 pa 中是可证一致的。因此，PRA 不能证明 pa 的一致性。这一事实通常被认为意味着希尔伯特的程序，其目的是证明使用“理想”(无限)数学原则在“实”(有限)数学陈述的证明，通过给出一个有限的证明，理想原则是一致的，不能执行。

The corollary also indicates the epistemological relevance of the second incompleteness theorem. It would actually provide no interesting information if a system $F$ proved its consistency. This is because inconsistent theories prove everything, including their consistency. Thus a consistency proof of $F$ in $F$ would give us no clue as to whether $F$ really is consistent; no doubts about the consistency of $F$ would be resolved by such a consistency proof. The interest in consistency proofs lies in the possibility of proving the consistency of a system $F$ in some system $F'$ that is in some sense less doubtful than $F$ itself, for example weaker than $F$ . For many naturally occurring theories $F$ and $F'$ , such as $F$ = Zermelo–Fraenkel set theory and $F'$ = primitive recursive arithmetic, the consistency of $F'$ is provable in $F$ , and thus $F'$ cannot prove the consistency of $F$ by the above corollary of the second incompleteness theorem.

The corollary also indicates the epistemological relevance of the second incompleteness theorem. It would actually provide no interesting information if a system proved its consistency. This is because inconsistent theories prove everything, including their consistency. Thus a consistency proof of in would give us no clue as to whether really is consistent; no doubts about the consistency of would be resolved by such a consistency proof. The interest in consistency proofs lies in the possibility of proving the consistency of a system in some system that is in some sense less doubtful than itself, for example weaker than . For many naturally occurring theories and , such as = Zermelo–Fraenkel set theory and = primitive recursive arithmetic, the consistency of is provable in , and thus cannot prove the consistency of by the above corollary of the second incompleteness theorem.

这一推论也表明了第二个不完备性定理的认识论相关性。如果一个系统证明了它的一致性，那么它实际上不会提供任何有趣的信息。这是因为不一致的理论证明了一切，包括它们的一致性。因此，一个一致性的 in 不会给我们任何关于是否真的是一致的线索; 对于一致性的任何怀疑都不会被这样一个一致性解决。对一致性证明的兴趣在于证明某些系统的一致性的可能性，这些系统在某种意义上比它本身更不值得怀疑，例如比它更弱。对于许多自然发生的理论，如 = Zermelo-Fraenkel 集合论和 = 本原递归算法，其一致性是可以证明的，因而不能用第二不完备性定理的上述推论证明其一致性。

The second incompleteness theorem does not rule out altogether the possibility of proving the consistency of some theory $T$ , only doing so in a theory that $T$ itself can prove to be consistent. For example, Gerhard Gentzen proved the consistency of Peano arithmetic in a different system that includes an axiom asserting that the ordinal called $ε 0$ is wellfounded; see Gentzen's consistency proof. Gentzen's theorem spurred the development of ordinal analysis in proof theory.

The second incompleteness theorem does not rule out altogether the possibility of proving the consistency of some theory , only doing so in a theory that itself can prove to be consistent. For example, Gerhard Gentzen proved the consistency of Peano arithmetic in a different system that includes an axiom asserting that the ordinal called is wellfounded; see Gentzen's consistency proof. Gentzen's theorem spurred the development of ordinal analysis in proof theory.

第二个不完备性定理并不完全排除证明某一理论一致性的可能性，只有在一个理论本身可以证明一致性的情况下才能这样做。例如，Gerhard Gentzen 在一个不同的系统中证明了 Peano 算术的一致性，其中包括一个公理断言序数被称为是有根据的; 参见 Gentzen 的一致性。根岑定理促进了证明理论中序数分析的发展。

Examples of undecidable statements

There are two distinct senses of the word "undecidable" in mathematics and computer science. The first of these is the proof-theoretic sense used in relation to Gödel's theorems, that of a statement being neither provable nor refutable in a specified deductive system. The second sense, which will not be discussed here, is used in relation to computability theory and applies not to statements but to decision problems, which are countably infinite sets of questions each requiring a yes or no answer. Such a problem is said to be undecidable if there is no computable function that correctly answers every question in the problem set (see undecidable problem).

在数学和计算机科学中，“无法判定的”一词有两种截然不同的含义。第一个是与哥德尔定理相关的证明理论意义，即在一个特定的演绎系统中，一个陈述既不可证明也不可反驳。第二种意义，这里不会讨论，是用于可计算性理论，不是用于陈述，而是用于决策问题，这是可数的无限组问题，每个问题都需要一个是或否的答案。如果没有可计算函数能正确回答问题集中的每一个问题，那么这样的问题就是不可判定的(见不可解问题)。

Because of the two meanings of the word undecidable, the term independent is sometimes used instead of undecidable for the "neither provable nor refutable" sense.

由于“不可判定”一词有两种含义，所以“独立”一词有时被用来代替“既不可证明也不可反驳”的“不可判定”一词。

Undecidability of a statement in a particular deductive system does not, in and of itself, address the question of whether the truth value of the statement is well-defined, or whether it can be determined by other means. Undecidability only implies that the particular deductive system being considered does not prove the truth or falsity of the statement. Whether there exist so-called "absolutely undecidable" statements, whose truth value can never be known or is ill-specified, is a controversial point in the philosophy of mathematics.

在一个特定的演绎系统中，陈述的不可判定性本身并不能解决陈述的真值是否定义明确，或者是否可以通过其他方法来确定的问题。不可判定性仅仅意味着被考虑的特定演绎系统不能证明陈述的真或假。是否存在所谓的“绝对不可判定”的命题，其真值永远不可知或不可确定，一直是数学哲学界争论的焦点。

The combined work of Gödel and Paul Cohen has given two concrete examples of undecidable statements (in the first sense of the term): The continuum hypothesis can neither be proved nor refuted in ZFC (the standard axiomatization of set theory), and the axiom of choice can neither be proved nor refuted in ZF (which is all the ZFC axioms except the axiom of choice). These results do not require the incompleteness theorem. Gödel proved in 1940 that neither of these statements could be disproved in ZF or ZFC set theory. In the 1960s, Cohen proved that neither is provable from ZF, and the continuum hypothesis cannot be proved from ZFC.

The combined work of Gödel and Paul Cohen has given two concrete examples of undecidable statements (in the first sense of the term): The continuum hypothesis can neither be proved nor refuted in ZFC (the standard axiomatization of set theory), and the axiom of choice can neither be proved nor refuted in ZF (which is all the ZFC axioms except the axiom of choice). These results do not require the incompleteness theorem. Gödel proved in 1940 that neither of these statements could be disproved in ZF or ZFC set theory. In the 1960s, Cohen proved that neither is provable from ZF, and the continuum hypothesis cannot be proved from ZFC.

和 Paul Cohen 的联合著作给出了两个不可判定命题的具体例子(在第一种意义上) : 连续统假设在 ZFC (集合论的标准公理化)中既不能被证明也不能被反驳，选择公理在 ZF 中既不能被证明也不能被反驳(除了选择公理之外，ZFC 所有的公理都是 ZFC 的)。这些结果不需要不完备性定理。哥德尔在1940年证明，在 ZF 或 ZFC 集合论中，这两种说法都不能被推翻。在20世纪60年代，Cohen 证明了 ZF 不能证明任何一个，ZFC 也不能证明连续统假设。

In 1973, Saharon Shelah showed that the Whitehead problem in group theory is undecidable, in the first sense of the term, in standard set theory.^[1]

In 1973, Saharon Shelah showed that the Whitehead problem in group theory is undecidable, in the first sense of the term, in standard set theory.

1973年，Saharon Shelah 证明了群论中的怀特海问题在标准集合论中是不可判定的。

Gregory Chaitin produced undecidable statements in algorithmic information theory and proved another incompleteness theorem in that setting. Chaitin's incompleteness theorem states that for any system that can represent enough arithmetic, there is an upper bound $c$ such that no specific number can be proved in that system to have Kolmogorov complexity greater than $c$ . While Gödel's theorem is related to the liar paradox, Chaitin's result is related to Berry's paradox.

Gregory Chaitin produced undecidable statements in algorithmic information theory and proved another incompleteness theorem in that setting. Chaitin's incompleteness theorem states that for any system that can represent enough arithmetic, there is an upper bound such that no specific number can be proved in that system to have Kolmogorov complexity greater than . While Gödel's theorem is related to the liar paradox, Chaitin's result is related to Berry's paradox.

在《算法信息论产生了无法判定的命题，并在这个背景下证明了另一个不完备性定理。的不完备性定理指出，对于任何一个可以表示足够算术的系统，都存在一个上界，以至于在这个系统中没有一个特定的数可以被证明柯氏复杂性大于。虽然哥德尔定理与说谎者悖论有关，但柴丁的结论与贝瑞悖论有关。

Undecidable statements provable in larger systems

= = = 在大系统中可证明的无法判定的命题 = =

These are natural mathematical equivalents of the Gödel "true but undecidable" sentence. They can be proved in a larger system which is generally accepted as a valid form of reasoning, but are undecidable in a more limited system such as Peano Arithmetic.

这些都是哥德尔“真实但不可判定”句子的自然数学等价物。它们可以在一个更大的系统中得到证明，这个系统通常被认为是一种有效的推理形式，但是在一个更有限的系统中，例如 Peano 算术中，它们是不可判定的。

In 1977, Paris and Harrington proved that the Paris–Harrington principle, a version of the infinite Ramsey theorem, is undecidable in (first-order) Peano arithmetic, but can be proved in the stronger system of second-order arithmetic. Kirby and Paris later showed that Goodstein's theorem, a statement about sequences of natural numbers somewhat simpler than the Paris–Harrington principle, is also undecidable in Peano arithmetic.

1977年，Paris 和 Harrington 证明了无穷大 Ramsey 定理的一个版本 Paris-Harrington 原理在(一阶) Peano 算术中是不可判定的，但在更强的二阶算术系统中是可以证明的。柯比和帕里斯后来证明了古德斯坦定理在 Peano 算术中也是不可判定的。古德斯坦定理是一个关于自然数序列的陈述，比巴黎-哈林顿原理稍微简单一些。

Kruskal's tree theorem, which has applications in computer science, is also undecidable from Peano arithmetic but provable in set theory. In fact Kruskal's tree theorem (or its finite form) is undecidable in a much stronger system codifying the principles acceptable based on a philosophy of mathematics called predicativism. The related but more general graph minor theorem (2003) has consequences for computational complexity theory.

克鲁斯卡尔的树定理在计算机科学中有应用，它与 Peano 算术相比也是不可判定的，但在集合论中是可证明的。事实上，克鲁斯卡尔的树定理(或其有限形式)是不可判定的，在一个更强大的系统中，这个系统将可接受的原则编纂成法典，其基础是一种称为谓定论的数学哲学。2003年出现的相关但更为普遍的图形微分定理对计算复杂性理论有一定的影响。

Relationship with computability

The incompleteness theorem is closely related to several results about undecidable sets in recursion theory.

= = = 与可计算性的关系 = = 不完备性定理与可计算性理论中关于不可判定集的几个结果密切相关。

模板:Harvard citations presented a proof of Gödel's incompleteness theorem using basic results of computability theory. One such result shows that the halting problem is undecidable: there is no computer program that can correctly determine, given any program $P$ as input, whether $P$ eventually halts when run with a particular given input. Kleene showed that the existence of a complete effective system of arithmetic with certain consistency properties would force the halting problem to be decidable, a contradiction. This method of proof has also been presented by 脚本错误：没有“Footnotes”这个模块。; 脚本错误：没有“Footnotes”这个模块。; and 脚本错误：没有“Footnotes”这个模块。.

presented a proof of Gödel's incompleteness theorem using basic results of computability theory. One such result shows that the halting problem is undecidable: there is no computer program that can correctly determine, given any program  as input, whether  eventually halts when run with a particular given input. Kleene showed that the existence of a complete effective system of arithmetic with certain consistency properties would force the halting problem to be decidable, a contradiction. This method of proof has also been presented by ; ; and .

利用可计算性理论的基本结果证明了哥德尔的不完备性定理。一个这样的结果表明停机问题是不可判定的: 没有计算机程序能够正确地判断，给定任何程序作为输入，当运行一个特定的给定输入时是否最终停止。Kleene 证明了一个具有一致性的完备有效算术系统的存在将迫使停机问题成为可判定的矛盾。这种证明方法也由; 和。

脚本错误：没有“Footnotes”这个模块。 explains how Matiyasevich's solution to Hilbert's 10th problem can be used to obtain a proof to Gödel's first incompleteness theorem. Matiyasevich proved that there is no algorithm that, given a multivariate polynomial $p (x 1, x 2,..., x k)$ with integer coefficients, determines whether there is an integer solution to the equation $p$ = 0. Because polynomials with integer coefficients, and integers themselves, are directly expressible in the language of arithmetic, if a multivariate integer polynomial equation $p$ = 0 does have a solution in the integers then any sufficiently strong system of arithmetic $T$ will prove this. Moreover, if the system $T$ is ω-consistent, then it will never prove that a particular polynomial equation has a solution when in fact there is no solution in the integers. Thus, if $T$ were complete and ω-consistent, it would be possible to determine algorithmically whether a polynomial equation has a solution by merely enumerating proofs of $T$ until either " $p$ has a solution" or " $p$ has no solution" is found, in contradiction to Matiyasevich's theorem. Hence it follows that $T$ cannot be $w$ -consistent and complete. Moreover, for each consistent effectively generated system $T$ , it is possible to effectively generate a multivariate polynomial $p$ over the integers such that the equation $p$ = 0 has no solutions over the integers, but the lack of solutions cannot be proved in $T$ (脚本错误：没有“Footnotes”这个模块。; 脚本错误：没有“Footnotes”这个模块。).

explains how Matiyasevich's solution to Hilbert's 10th problem can be used to obtain a proof to Gödel's first incompleteness theorem. Matiyasevich proved that there is no algorithm that, given a multivariate polynomial  with integer coefficients, determines whether there is an integer solution to the equation  = 0. Because polynomials with integer coefficients, and integers themselves, are directly expressible in the language of arithmetic, if a multivariate integer polynomial equation  = 0 does have a solution in the integers then any sufficiently strong system of arithmetic  will prove this. Moreover, if the system  is ω-consistent, then it will never prove that a particular polynomial equation has a solution when in fact there is no solution in the integers. Thus, if  were complete and ω-consistent, it would be possible to determine algorithmically whether a polynomial equation has a solution by merely enumerating proofs of  until either " has a solution" or " has no solution" is found, in contradiction to Matiyasevich's theorem. Hence it follows that  cannot be -consistent and complete. Moreover, for each consistent effectively generated system , it is possible to effectively generate a multivariate polynomial  over the integers such that the equation  = 0 has no solutions over the integers, but the lack of solutions cannot be proved in  (; ).

解释了如何使用 Matiyasevich 对希尔伯特第10个问题的解决方案来获得哥德尔第一个不完备性定理的证明。证明了在给定一个整系数多元多项式时，没有一种算法能够确定方程 = 0。由于整系数多项式和整数本身都可以用算术语言直接表示，如果一个多元整数多项式方程 = 0在整数中有解，那么任何足够强的算术系统都可以证明这一点。此外，如果系统是 ω- 一致的，那么它将永远不会证明一个特定的多项式方程有一个解，而实际上在整数中没有解。因此，如果一个多项式方程是完全和 ω- 一致的，那么通过列举直到找到“有解”或“没有解”的证明，从算法上确定一个多项式方程是否有解是可能的，这与 Matiyasevich 的定理相矛盾。因此，它不可能是一致的和完整的。此外，对于每个一致的有效生成系统，可以有效地生成整数上的多元多项式，使得方程 = 0对整数没有解，但是缺少解不能在(;)中得到证明。

脚本错误：没有“Footnotes”这个模块。 shows how the existence of recursively inseparable sets can be used to prove the first incompleteness theorem. This proof is often extended to show that systems such as Peano arithmetic are essentially undecidable (see 脚本错误：没有“Footnotes”这个模块。).

shows how the existence of recursively inseparable sets can be used to prove the first incompleteness theorem. This proof is often extended to show that systems such as Peano arithmetic are essentially undecidable (see ).

展示了如何用递归不可分集的存在性来证明第一个不完备性定理。这个证明经常被扩展，以证明诸如 Peano 算术之类的系统本质上是不可判定的(见)。

Chaitin's incompleteness theorem gives a different method of producing independent sentences, based on Kolmogorov complexity. Like the proof presented by Kleene that was mentioned above, Chaitin's theorem only applies to theories with the additional property that all their axioms are true in the standard model of the natural numbers. Gödel's incompleteness theorem is distinguished by its applicability to consistent theories that nonetheless include statements that are false in the standard model; these theories are known as ω-inconsistent.

的不完备性定理提供了一种不同的方法来产生独立的句子，这种方法基于柯氏复杂性。就像上面提到的 Kleene 提出的证明一样，Chaitin 的定理只适用于具有额外性质的理论，即在自然数的标准模型中，所有的公理都是真实的。哥德尔的不完备性定理的特点在于它对一致性理论的适用性，尽管这些一致性理论包括标准模型中的错误陈述; 这些理论被称为 ω- 不一致性。

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:

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

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).
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).
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.

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 is provable in the system" (which can be applied to any statement "" in the system).
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).
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.

系统中的语句可以用自然数表示(称为哥德尔数)。这一点的重要性在于，陈述的性质ーー例如它们的真实性和虚假性ーー将等同于确定它们的哥德尔数是否具有某些性质，因此，这些陈述的性质可以通过检查它们的哥德尔数来证明。这一部分最终构建了一个公式，表达了“语句在系统中是可证明的”(可以应用于系统中的“任何语句”)的思想。# 在形式系统中，可以构造一个数字，它的匹配语句在解释时是自参照的，本质上是说它(即。陈述本身)是无法证明的。这是通过一种叫做“对角化”(diagonalization)的技术来完成的(之所以这样称呼是因为它的起源是 Cantor 的对角线参数)。# 在正式系统中，这个陈述允许证明它在系统中既不可证明也不可推翻，因此系统实际上不可能是 ω- 一致的。因此，最初认为所提出的系统符合标准的假设是错误的。

Arithmetization of syntax

= = 语法的算术化 = =

The main problem in fleshing out the proof described above is that it seems at first that to construct a statement $p$ that is equivalent to " $p$ cannot be proved", $p$ would somehow have to contain a reference to $p$ , which could easily give rise to an infinite regress. Gödel's ingenious technique is to show that statements can be matched with numbers (often called the arithmetization of syntax) in such a way that "proving a statement" can be replaced with "testing whether a number has a given property". This allows a self-referential formula to be constructed in a way that avoids any infinite regress of definitions. The same technique was later used by Alan Turing in his work on the Entscheidungsproblem.

The main problem in fleshing out the proof described above is that it seems at first that to construct a statement that is equivalent to " cannot be proved", would somehow have to contain a reference to , which could easily give rise to an infinite regress. Gödel's ingenious technique is to show that statements can be matched with numbers (often called the arithmetization of syntax) in such a way that "proving a statement" can be replaced with "testing whether a number has a given property". This allows a self-referential formula to be constructed in a way that avoids any infinite regress of definitions. The same technique was later used by Alan Turing in his work on the Entscheidungsproblem.

充实上述证明的主要问题在于，首先似乎要构造一个等价于不能被证明的陈述，就必须以某种方式包含一个引用，这很容易引出一个无穷回归。哥德尔的独创性技巧在于证明语句可以与数字匹配(通常称为语法的算术化) ，这样“证明一个语句”就可以替换为“检验一个数字是否具有给定的性质”。这使得自参照公式的构造方式可以避免任何无穷回归的定义。同样的技术后来被 Alan Turing 应用到他在可判定性的工作中。

In simple terms, a method can be devised so that every formula or statement that can be formulated in the system gets a unique number, called its Gödel number, in such a way that it is possible to mechanically convert back and forth between formulas and Gödel numbers. The numbers involved might be very long indeed (in terms of number of digits), but this is not a barrier; all that matters is that such numbers can be constructed. A simple example is how English can be stored as a sequence of numbers for each letter and then combined into a single larger number:

The word hello is encoded as 104-101-108-108-111 in ASCII, which can be converted into the number 104101108108111.
The logical statement x=y => y=x is encoded as 120-061-121-032-061-062-032-121-061-120 in ASCII, which can be converted into the number 120061121032061062032121061120.

In simple terms, a method can be devised so that every formula or statement that can be formulated in the system gets a unique number, called its Gödel number, in such a way that it is possible to mechanically convert back and forth between formulas and Gödel numbers. The numbers involved might be very long indeed (in terms of number of digits), but this is not a barrier; all that matters is that such numbers can be constructed. A simple example is how English can be stored as a sequence of numbers for each letter and then combined into a single larger number:

The word hello is encoded as 104-101-108-108-111 in ASCII, which can be converted into the number 104101108108111.
The logical statement x=y => y=x is encoded as 120-061-121-032-061-062-032-121-061-120 in ASCII, which can be converted into the number 120061121032061062032121061120.

简单来说，可以设计一种方法，使得系统中的每个公式或语句得到一个唯一的数，称为哥德尔数，这样就可以机械地在公式和哥德尔数之间来回转换。所涉及的数字可能确实很长(按位数表示) ，但这不是障碍; 重要的是这些数字可以被构造。一个简单的例子是，如何将英语存储为每个字母的数字序列，然后组合成一个更大的数字:

hello 在 ASCII 中编码为104-101-108-108-111，可以转换为数字104101108108111。
逻辑语句 x = y = > y = x 在 ASCII 中编码为120-061-121-032-061-062-032-121-061-120，可以转换为数字120061121032061062032121061120。

In principle, proving a statement true or false can be shown to be equivalent to proving that the number matching the statement does or doesn't have a given property. Because the formal system is strong enough to support reasoning about numbers in general, it can support reasoning about numbers that represent formulae and statements as well. Crucially, because the system can support reasoning about properties of numbers, the results are equivalent to reasoning about provability of their equivalent statements.

In principle, proving a statement true or false can be shown to be equivalent to proving that the number matching the statement does or doesn't have a given property. Because the formal system is strong enough to support reasoning about numbers in general, it can support reasoning about numbers that represent formulae and statements as well. Crucially, because the system can support reasoning about properties of numbers, the results are equivalent to reasoning about provability of their equivalent statements.

原则上，证明一个语句为真或为假等同于证明与该语句匹配的数字有或没有给定的属性。由于形式系统足够强大，可以支持对一般数字的推理，因此也可以支持对表示公式和语句的数字的推理。至关重要的是，因为该系统可以支持关于数字性质的推理，所以其结果等价于关于等价语句的可证明性的推理。

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$ , 模板:Tmath 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模板:Resx3 = 6".

A formula that contains exactly one free variable is called a statement form or class-sign. As soon as 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 , 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 "23 = 6".

只包含一个自由变量的公式称为语句形式或类符号。一旦被一个特定的数字取代，语句形式就变成了善意的语句，然后在系统中可以证明，也可以不证明。对于某些公式，我们可以证明，对于每一个自然数，只有当且仅当它可以被证明时才为真(原始证明中的精确要求较弱，但对于证明草图，这就足够了)。特别是，对于有限数目的自然数之间的每一个特定算术运算，例如“23 = 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)$ .

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

陈述形式本身不是陈述，因此不能被证明或反驳。但是，每个语句表单都可以分配一个 Gödel 数，表示为。格式()中使用的自由变量的选择与 Gödel 数的赋值无关。

模板:AnchorThe 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) = \exists 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.

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 , one may ask whether a number is the Gödel number of its proof. The relation between the Gödel number of and , the potential Gödel number of its proof, is an arithmetical relation between two numbers. Therefore, there is a statement form that uses this arithmetical relation to state that a Gödel number of a proof of exists:

( is the Gödel number of a formula and is the Gödel number of a proof of the formula encoded by ).

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 "" is merely an abbreviation that represents a particular, very long, formula in the original language of ; the string "" itself is not claimed to be part of this language.

可证性的概念本身也可以用哥德尔数来编码，方式如下: 既然证明是遵循某些规则的陈述的列表，那么一个证明的哥德尔数可以被定义。现在，对于每一个陈述，人们可能会问一个数是否是它的证明的哥德尔数。的哥德尔数与其证明的潜在哥德尔数之间的关系，是两个数之间的算术关系。因此，有一种陈述形式，使用这种算术关系来说明存在的证明的哥德尔数: : (是公式的哥德尔数，是公式编码的证明的哥德尔数)。Bew 是 beweisbar 的缩写，在德语中是“可证明的”的意思; 这个名字最初是由哥德尔用来表示刚才描述的可证明的公式。请注意，“”只是一个缩写，用原语言表示一个特定的、非常长的公式; 字符串“”本身并不声称是这种语言的一部分。

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.

An important feature of the formula is that if a statement is provable in the system then is also provable. This is because any proof of would have a corresponding Gödel number, the existence of which causes 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 \leftrightarrow F (G (p))

.

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

p \leftrightarrow ~ 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 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 there is a statement such that the system proves

.

By letting be the negation of , we obtain the theorem

and the 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.

The statement is not literally equal to ; rather, 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 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.

Now, assume that the axiomatic system is ω-consistent, and let 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 were provable, then would be provable, as argued above. But asserts the negation of . Thus the system would be inconsistent, proving both a statement and its negation. This contradiction shows that 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.

If the negation of were provable, then would be provable (because was constructed to be equivalent to the negation of ). However, for each specific number , cannot be the Gödel number of the proof of , because 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 ), but on the other hand, for every specific number , we can prove that it does not have this property. This is impossible in an ω-consistent system. Thus the negation of is not provable.

如果否定是可证明的，那么就是可证明的(因为被构造为等价于否定)。但是，对于每个具体的数，不能对哥德尔数进行证明，因为不能证明(从前段)。因此，一方面系统证明了有一个具有某种性质的数(它是哥德尔数的证明) ，但另一方面，对于每一个特定的数，我们可以证明它不具有这种性质。这在 ω- 一致系统中是不可能的。因此，否定是无法证明的。

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

Thus the statement 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.

In fact, to show that 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 is not provable. Thus, if is constructed for a particular system:

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

事实上，要证明这是不可证明的，只需要假设系统是一致的。强 ω- 一致性假设是证明否定的不可证明的必要条件。因此，如果是为一个特定的系统构造的:

如果这个系统是 ω- 一致的，那么它既不能证明也不能证明它的否定，因此是不可判定的。
如果系统是一致的，它可能有相同的情况，或者它可能证明。在后一种情况下，我们有一个假的但是可证明的语句(“ not”) ，系统不是 ω- 一致的。

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.

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

如果一个人试图“添加缺失的公理”以避免系统的不完整性，那么他就必须添加或者或者“不”作为公理。但随后，“作为哥德尔数的一个证明”的定义发生了变化。也就是说分子式现在不同了。因此，当我们将对角引理应用于这个新的 Bew 时，我们得到了一个新的语句，它不同于以前的语句，如果它是 ω- 一致的，那么这个语句在新系统中是不可判定的。

Proof via Berry's paradox

模板:Harvard citations sketches an alternative proof of the first incompleteness theorem that uses Berry's paradox rather than the liar paradox to construct a true but unprovable formula. A similar proof method was independently discovered by Saul Kripke 模板:Harv. Boolos's proof proceeds by constructing, for any computably enumerable set $S$ of true sentences of arithmetic, another sentence which is true but not contained in $S$ . This gives the first incompleteness theorem as a corollary. According to Boolos, this proof is interesting because it provides a "different sort of reason" for the incompleteness of effective, consistent theories of arithmetic 模板:Harv.

sketches an alternative proof of the first incompleteness theorem that uses Berry's paradox rather than the liar paradox to construct a true but unprovable formula. A similar proof method was independently discovered by Saul Kripke .  Boolos's proof proceeds by constructing, for any computably enumerable set  of true sentences of arithmetic, another sentence which is true but not contained in . This gives the first incompleteness theorem as a corollary. According to Boolos, this proof is interesting because it provides a "different sort of reason" for the incompleteness of effective, consistent theories of arithmetic .

= = = 用贝瑞悖论证明 = = 第一个不完备性定理的另一种证明，用贝瑞悖论而不是说谎者悖论来构造一个真实但无法证明的公式。索尔 · 克里普克也独立发现了类似的证明方法。Boolos 的证明是通过构造一个可计算枚举的算术真句子集合来进行的，这个句子是真的，但不包含在。这就给出了第一个不完备性定理作为推论。布洛斯认为，这个证明很有意思，因为它为有效的、一致的算术理论的不完备性提供了一种“不同的理由”。

Computer verified proofs

The incompleteness theorems are among a relatively small number of nontrivial theorems that have been transformed into formalized theorems that can be completely verified by proof assistant software. Gödel's original proofs of the incompleteness theorems, like most mathematical proofs, were written in natural language intended for human readers.

这些不完备性定理是已经转化为形式化定理的相对较少的几个非平凡定理之一，可以通过证明辅助软件完全验证。哥德尔关于不完备性定理的最初证明，就像大多数数学证明一样，是用面向人类读者的自然语言写成的。

Computer-verified proofs of versions of the first incompleteness theorem were announced by Natarajan Shankar in 1986 using Nqthm 模板:Harv, by Russell O'Connor in 2003 using Coq 模板:Harv and by John Harrison in 2009 using HOL Light 模板:Harv. A computer-verified proof of both incompleteness theorems was announced by Lawrence Paulson in 2013 using Isabelle 模板:Harv.

Computer-verified proofs of versions of the first incompleteness theorem were announced by Natarajan Shankar in 1986 using Nqthm , by Russell O'Connor in 2003 using Coq and by John Harrison in 2009 using HOL Light . A computer-verified proof of both incompleteness theorems was announced by Lawrence Paulson in 2013 using Isabelle .

第一个不完备性定理的计算机验证证明由 Natarajan Shankar 在1986年用 Nqthm 公布，由 Russell o’connor 在2003年用 Coq 公布，由 John Harrison 在2009年用 HOL Light 公布。2013年，劳伦斯•保尔森(Lawrence Paulson)用伊莎贝尔(Isabelle)宣布了一个计算机验证的两个不完备性定理的证明。

Proof sketch for the second theorem

The main difficulty in proving the second incompleteness theorem is to show that various facts about provability used in the proof of the first incompleteness theorem can be formalized within a system $S$ using a formal predicate for provability. Once this is done, the second incompleteness theorem follows by formalizing the entire proof of the first incompleteness theorem within the system $S$ itself.

The main difficulty in proving the second incompleteness theorem is to show that various facts about provability used in the proof of the first incompleteness theorem can be formalized within a system using a formal predicate for provability. Once this is done, the second incompleteness theorem follows by formalizing the entire proof of the first incompleteness theorem within the system itself.

证明第二不完备性定理的主要困难在于，证明第一不完备性定理的可证明性的各种事实可以在一个系统中用形式谓词进行形式化证明。一旦做到这一点，第二个不完全性定理就会在系统内部形式化第一个不完全性定理的整个证明。

Let $p$ stand for the undecidable sentence constructed above, and assume for purposes of obtaining a contradiction that the consistency of the system $S$ can be proved from within the system $S$ itself. This is equivalent to proving the statement "System $S$ is consistent". Now consider the statement $c$ , where $c$ = "If the system $S$ is consistent, then $p$ is not provable". The proof of sentence $c$ can be formalized within the system $S$ , and therefore the statement $c$ , " $p$ is not provable", (or identically, "not $P (p)$ ") can be proved in the system $S$ .

Let stand for the undecidable sentence constructed above, and assume for purposes of obtaining a contradiction that the consistency of the system can be proved from within the system itself. This is equivalent to proving the statement "System is consistent". Now consider the statement , where = "If the system is consistent, then is not provable". The proof of sentence can be formalized within the system , and therefore the statement , " is not provable", (or identically, "not ") can be proved in the system .

代表上述构造的不可判定的句子，并假定系统的一致性可以从系统本身内部证明，以获得一个矛盾。这相当于证明“系统是一致的”这一陈述。现在考虑这个语句，where = “如果系统是一致的，那么就不能证明”。句子的证明可以在系统内形式化，因此系统可以证明“不可证明”(或者同样的“不可证明”)的陈述。

Observe then, that if we can prove that the system $S$ is consistent (ie. the statement in the hypothesis of $c$ ), then we have proved that $p$ is not provable. But this is a contradiction since by the 1st Incompleteness Theorem, this sentence (ie. what is implied in the sentence $c$ , "" $p$ " is not provable") is what we construct to be unprovable. Notice that this is why we require formalizing the first Incompleteness Theorem in $S$ : to prove the 2nd Incompleteness Theorem, we obtain a contradiction with the 1st Incompleteness Theorem which can do only by showing that the theorem holds in $S$ . So we cannot prove that the system $S$ is consistent. And the 2nd Incompleteness Theorem statement follows.

Observe then, that if we can prove that the system is consistent (ie. the statement in the hypothesis of ), then we have proved that is not provable. But this is a contradiction since by the 1st Incompleteness Theorem, this sentence (ie. what is implied in the sentence , """ is not provable") is what we construct to be unprovable. Notice that this is why we require formalizing the first Incompleteness Theorem in : to prove the 2nd Incompleteness Theorem, we obtain a contradiction with the 1st Incompleteness Theorem which can do only by showing that the theorem holds in . So we cannot prove that the system is consistent. And the 2nd Incompleteness Theorem statement follows.

然后观察，如果我们能证明系统是一致的(即。假设中的陈述) ，那么我们已经证明了这是不可证明的。但这是一个矛盾，因为根据第一个不完备性定理，这个句子(即。在句子中隐含的，“”是不可证明的)是我们构造的是不可证明的。注意，这就是为什么我们需要将第一个不完全性定理形式化为: 为了证明第二个不完全性定理，我们得到了与第一个不完全性定理的矛盾，这个矛盾只能通过证明这个定理仍然有效。所以我们不能证明这个系统是一致的。第二个不完全性定理陈述如下。

Discussion and implications

The incompleteness results affect the philosophy of mathematics, particularly versions of formalism, which use a single system of formal logic to define their principles.

不完整的结果影响了数学哲学，特别是形式主义的各种版本，它们使用单一的形式逻辑系统来定义它们的原理。

Consequences for logicism and Hilbert's second problem

= = 对逻辑主义和希尔伯特的第二个问题的后果 =

The incompleteness theorem is sometimes thought to have severe consequences for the program of logicism proposed by Gottlob Frege and Bertrand Russell, which aimed to define the natural numbers in terms of logic 模板:Harv. Bob Hale and Crispin Wright argue that it is not a problem for logicism because the incompleteness theorems apply equally to first order logic as they do to arithmetic. They argue that only those who believe that the natural numbers are to be defined in terms of first order logic have this problem.

The incompleteness theorem is sometimes thought to have severe consequences for the program of logicism proposed by Gottlob Frege and Bertrand Russell, which aimed to define the natural numbers in terms of logic . Bob Hale and Crispin Wright argue that it is not a problem for logicism because the incompleteness theorems apply equally to first order logic as they do to arithmetic. They argue that only those who believe that the natural numbers are to be defined in terms of first order logic have this problem.

不完备性定理有时被认为会对 Gottlob Frege 和伯特兰·罗素提出的逻辑主义程序产生严重的后果，后者的目的是从逻辑的角度定义自然数。和 Crispin Wright 认为这不是逻辑主义的问题，因为不完备性定理同样适用于一阶逻辑和算术逻辑。他们认为，只有那些相信自然数是用一阶逻辑来定义的人才有这个问题。

Many logicians believe that Gödel's incompleteness theorems struck a fatal blow to David Hilbert's second problem, which asked for a finitary consistency proof for mathematics. The second incompleteness theorem, in particular, is often viewed as making the problem impossible. Not all mathematicians agree with this analysis, however, and the status of Hilbert's second problem is not yet decided (see "Modern viewpoints on the status of the problem").

许多逻辑学家认为，哥德尔的不完备性定理给 David Hilbert 的第二个问题带来了致命的打击，这个问题要求为数学设置一个一致性。特别是第二个不完备性定理，通常被认为使问题不可能解决。然而，并非所有的数学家都同意这种分析，希尔伯特的第二个问题的地位尚未确定(见“关于这个问题地位的现代观点”)。

Minds and machines

Authors including the philosopher J. R. Lucas and physicist Roger Penrose have debated what, if anything, Gödel's incompleteness theorems imply about human intelligence. Much of the debate centers on whether the human mind is equivalent to a Turing machine, or by the Church–Turing thesis, any finite machine at all. If it is, and if the machine is consistent, then Gödel's incompleteness theorems would apply to it.

包括哲学家 j · r · 卢卡斯和物理学家罗杰 · 彭罗斯在内的作者们争论过哥德尔的不完备性定理对人类智力的影响。争论的焦点主要集中在人类的大脑是否等同于图灵机，或者根据丘奇-图灵论点，是否等同于任何有限机器。如果是这样，如果机器是一致的，那么哥德尔的不完备性定理将适用于它。

模板:Harvard citations suggested that while Gödel's theorems cannot be applied to humans, since they make mistakes and are therefore inconsistent, it may be applied to the human faculty of science or mathematics in general. Assuming that it is consistent, either its consistency cannot be proved or it cannot be represented by a Turing machine.

suggested that while Gödel's theorems cannot be applied to humans, since they make mistakes and are therefore inconsistent, it may be applied to the human faculty of science or mathematics in general. Assuming that it is consistent, either its consistency cannot be proved or it cannot be represented by a Turing machine.

尽管哥德尔的定理不能应用于人类，因为他们犯错误，因此是不一致的，但它可以应用于人类的科学或数学的一般能力。假设它是一致的，要么它的一致性不能被证明，要么它不能被图灵机表示。

模板:Harvard citations has proposed that the concept of mathematical "knowability" should be based on computational complexity rather than logical decidability. He writes that "when knowability is interpreted by modern standards, namely via computational complexity, the Gödel phenomena are very much with us."

has proposed that the concept of mathematical "knowability" should be based on computational complexity rather than logical decidability.  He writes that "when knowability is interpreted by modern standards, namely via computational complexity, the Gödel phenomena are very much with us."

提出数学“可知性”的概念应该基于计算的复杂性而不是逻辑的可判定性。他写道，“当可知性被现代标准解释，即通过计算的复杂性，哥德尔现象是非常与我们。”

Douglas Hofstadter, in his books Gödel, Escher, Bach and I Am a Strange Loop, cites Gödel's theorems as an example of what he calls a strange loop, a hierarchical, self-referential structure existing within an axiomatic formal system. He argues that this is the same kind of structure which gives rise to consciousness, the sense of "I", in the human mind. While the self-reference in Gödel's theorem comes from the Gödel sentence asserting its own unprovability within the formal system of Principia Mathematica, the self-reference in the human mind comes from the way in which the brain abstracts and categorises stimuli into "symbols", or groups of neurons which respond to concepts, in what is effectively also a formal system, eventually giving rise to symbols modelling the concept of the very entity doing the perception. Hofstadter argues that a strange loop in a sufficiently complex formal system can give rise to a "downward" or "upside-down" causality, a situation in which the normal hierarchy of cause-and-effect is flipped upside-down. In the case of Gödel's theorem, this manifests, in short, as the following:

Douglas Hofstadter, in his books Gödel, Escher, Bach and I Am a Strange Loop, cites Gödel's theorems as an example of what he calls a strange loop, a hierarchical, self-referential structure existing within an axiomatic formal system. He argues that this is the same kind of structure which gives rise to consciousness, the sense of "I", in the human mind. While the self-reference in Gödel's theorem comes from the Gödel sentence asserting its own unprovability within the formal system of Principia Mathematica, the self-reference in the human mind comes from the way in which the brain abstracts and categorises stimuli into "symbols", or groups of neurons which respond to concepts, in what is effectively also a formal system, eventually giving rise to symbols modelling the concept of the very entity doing the perception. Hofstadter argues that a strange loop in a sufficiently complex formal system can give rise to a "downward" or "upside-down" causality, a situation in which the normal hierarchy of cause-and-effect is flipped upside-down. In the case of Gödel's theorem, this manifests, in short, as the following:

侯世达在他的著作《哥德尔，埃舍尔，巴赫和我是一个奇怪的循环》中，引用哥德尔的定理作为他所谓的奇怪循环的例子，一个存在于公理化形式系统中的层次化的、自我参照的结构。他认为，这是同样的结构，产生意识，“我”的意识，在人类的头脑。虽然哥德尔定理中的自我参照来自哥德尔句子，声称自己在数学原理的正式系统中是不可证明的，但人类大脑中的自我参照来自于大脑将刺激抽象和分类为“符号”，或者说是对概念作出反应的神经元群，在实际上也是一个正式系统中，最终导致符号模拟了正在进行感知的实体的概念。霍夫施塔特认为，在足够复杂的正式系统中，一个奇怪的循环可以产生一种“向下”或“上下颠倒”的因果关系，这种情况下，因果关系的正常层次结构是颠倒的。在哥德尔定理的情况下，简而言之，这表现为:

"Merely from knowing the formula's meaning, one can infer its truth or falsity without any effort to derive it in the old-fashioned way, which requires one to trudge methodically "upwards" from the axioms. This is not just peculiar; it is astonishing. Normally, one cannot merely look at what a mathematical conjecture says and simply appeal to the content of that statement on its own to deduce whether the statement is true or false." (I Am a Strange Loop.)^[2]

"Merely from knowing the formula's meaning, one can infer its truth or falsity without any effort to derive it in the old-fashioned way, which requires one to trudge methodically "upwards" from the axioms. This is not just peculiar; it is astonishing. Normally, one cannot merely look at what a mathematical conjecture says and simply appeal to the content of that statement on its own to deduce whether the statement is true or false." (I Am a Strange Loop.)

“仅仅通过知道公式的意义，就可以推断出公式的真实性或虚假性，而不需要用老式的方法来推导，这需要人们从公式中有条不紊地“向上”推导。这不仅仅是奇怪的，而是令人惊讶的。通常情况下，人们不能仅仅看一个猜想说了什么，然后仅仅依靠这个陈述的内容来推断这个陈述是对还是错。”(我是一个奇怪的循环。)

In the case of the mind, a far more complex formal system, this "downward causality" manifests, in Hofstadter's view, as the ineffable human instinct that the causality of our minds lies on the high level of desires, concepts, personalities, thoughts and ideas, rather than on the low level of interactions between neurons or even fundamental particles, even though according to physics the latter seems to possess the causal power.

在思维这个更为复杂的形式系统中，这种“向下的因果关系”在侯世达看来是人类不可言喻的本能，即我们思维的因果关系在于高层次的欲望、概念、人格、思想和想法，而不是在神经元之间甚至基本粒子之间低层次的相互作用，尽管根据物理学，后者似乎具有因果关系的力量。

"There is thus a curious upside-downness to our normal human way of perceiving the world: we are built to perceive “big stuff” rather than “small stuff”, even though the domain of the tiny seems to be where the actual motors driving reality reside." (I Am a Strange Loop.)^[2]

"There is thus a curious upside-downness to our normal human way of perceiving the world: we are built to perceive “big stuff” rather than “small stuff”, even though the domain of the tiny seems to be where the actual motors driving reality reside." (I Am a Strange Loop.)

“因此，我们人类对世界的正常感知方式存在着一种奇怪的上下颠倒: 我们生来就是要感知“大事物”，而不是“小事物”，尽管微小的领域似乎就是驱动现实的真正发动机所在的地方。”(我是一个奇怪的循环。)

Paraconsistent logic

= 次协调逻辑 =

Although Gödel's theorems are usually studied in the context of classical logic, they also have a role in the study of paraconsistent logic and of inherently contradictory statements (dialetheia). 模板:Harvard citations argues that replacing the notion of formal proof in Gödel's theorem with the usual notion of informal proof can be used to show that naive mathematics is inconsistent, and uses this as evidence for dialetheism. The cause of this inconsistency is the inclusion of a truth predicate for a system within the language of the system 模板:Harv. 模板:Harvard citations gives a more mixed appraisal of the applications of Gödel's theorems to dialetheism.

Although Gödel's theorems are usually studied in the context of classical logic, they also have a role in the study of paraconsistent logic and of inherently contradictory statements (dialetheia). argues that replacing the notion of formal proof in Gödel's theorem with the usual notion of informal proof can be used to show that naive mathematics is inconsistent, and uses this as evidence for dialetheism. The cause of this inconsistency is the inclusion of a truth predicate for a system within the language of the system . gives a more mixed appraisal of the applications of Gödel's theorems to dialetheism.

虽然哥德尔的定理通常是在经典逻辑的背景下研究，他们也有一个角色在研究次协调逻辑和内在矛盾的陈述(辩证法)。认为用通常的非正式证明概念取代哥德尔定理中的正式证明概念，可以用来表明朴素数学是不一致的，并将此作为辩证论的证据。这种不一致的原因是在系统的语言中包含了系统的真值谓词。对哥德尔定理在辩神论中的应用给出了更为混杂的评价。

Appeals to the incompleteness theorems in other fields

= = 引用其他领域的不完备性定理 = =

Appeals and analogies are sometimes made to the incompleteness theorems in support of arguments that go beyond mathematics and logic. Several authors have commented negatively on such extensions and interpretations, including Torkel Franzén (2005); Panu 脚本错误：没有“Footnotes”这个模块。; 模板:Harvard citations; and 模板:Harvard citations. 脚本错误：没有“Footnotes”这个模块。, for example, quote from Rebecca Goldstein's comments on the disparity between Gödel's avowed Platonism and the anti-realist uses to which his ideas are sometimes put. 脚本错误：没有“Footnotes”这个模块。 criticize Régis Debray's invocation of the theorem in the context of sociology; Debray has defended this use as metaphorical (ibid.).

Appeals and analogies are sometimes made to the incompleteness theorems in support of arguments that go beyond mathematics and logic. Several authors have commented negatively on such extensions and interpretations, including Torkel Franzén (2005); Panu ; ; and . , for example, quote from Rebecca Goldstein's comments on the disparity between Gödel's avowed Platonism and the anti-realist uses to which his ideas are sometimes put. criticize Régis Debray's invocation of the theorem in the context of sociology; Debray has defended this use as metaphorical (ibid.).

为了支持超越数学和逻辑的论证，人们有时会对不完整性定理进行上诉和类比。一些作者对这种延伸和解释持否定态度，包括 Torkel Franzén (2005) ; Panu; 和。例如，引用丽贝卡 · 戈尔茨坦对哥德尔公开承认的柏拉图主义和反现实主义运用之间的差异的评论。在社会学的背景下批评雷吉斯 · 德布雷引用这个定理; 德布雷为这个用法辩护说是比喻的(同上)。).

History

After Gödel published his proof of the completeness theorem as his doctoral thesis in 1929, he turned to a second problem for his habilitation. His original goal was to obtain a positive solution to Hilbert's second problem 模板:Harv. At the time, theories of the natural numbers and real numbers similar to second-order arithmetic were known as "analysis", while theories of the natural numbers alone were known as "arithmetic".

After Gödel published his proof of the completeness theorem as his doctoral thesis in 1929, he turned to a second problem for his habilitation. His original goal was to obtain a positive solution to Hilbert's second problem . At the time, theories of the natural numbers and real numbers similar to second-order arithmetic were known as "analysis", while theories of the natural numbers alone were known as "arithmetic".

在哥德尔于1929年在他的博士论文中发表了完备性定理的证明之后，他又转向了第二个问题来证明自己的能力。他最初的目标是为希尔伯特的第二个问题找到一个积极的解决方案。当时，类似于二阶算术的自然数和实数理论被称为“分析”，而自然数理论本身被称为“算术”。

Gödel was not the only person working on the consistency problem. Ackermann had published a flawed consistency proof for analysis in 1925, in which he attempted to use the method of ε-substitution originally developed by Hilbert. Later that year, von Neumann was able to correct the proof for a system of arithmetic without any axioms of induction. By 1928, Ackermann had communicated a modified proof to Bernays; this modified proof led Hilbert to announce his belief in 1929 that the consistency of arithmetic had been demonstrated and that a consistency proof of analysis would likely soon follow. After the publication of the incompleteness theorems showed that Ackermann's modified proof must be erroneous, von Neumann produced a concrete example showing that its main technique was unsound (脚本错误：没有“Footnotes”这个模块。; 脚本错误：没有“Footnotes”这个模块。).

Gödel was not the only person working on the consistency problem. Ackermann had published a flawed consistency proof for analysis in 1925, in which he attempted to use the method of ε-substitution originally developed by Hilbert. Later that year, von Neumann was able to correct the proof for a system of arithmetic without any axioms of induction. By 1928, Ackermann had communicated a modified proof to Bernays; this modified proof led Hilbert to announce his belief in 1929 that the consistency of arithmetic had been demonstrated and that a consistency proof of analysis would likely soon follow. After the publication of the incompleteness theorems showed that Ackermann's modified proof must be erroneous, von Neumann produced a concrete example showing that its main technique was unsound (; ).

哥德尔并不是唯一一个研究一致性问题的人。阿克曼在1925年发表了一份有缺陷的一致性分析报告，其中他试图使用希尔伯特最初发明的 ε- 替换方法。那年晚些时候，冯 · 诺依曼能够修正一个没有任何归纳公理的算术系统的证明。到1928年，Ackermann 已经将一个经过修改的证明传达给了伯奈斯; 这个经过修改的证明使得希尔伯特在1929年宣布了他的信念，即算术的一致性已经得到了证明，一个一致性的分析很可能很快就会接踵而至。在不完备性定理的发表表明阿克曼的修正证明一定是错误的之后，冯 · 诺依曼给出了一个具体的例子，说明其主要技术是不完备的(; ;)。

In the course of his research, Gödel discovered that although a sentence which asserts its own falsehood leads to paradox, a sentence that asserts its own non-provability does not. In particular, Gödel was aware of the result now called Tarski's indefinability theorem, although he never published it. Gödel announced his first incompleteness theorem to Carnap, Feigel and Waismann on August 26, 1930; all four would attend the Second Conference on the Epistemology of the Exact Sciences, a key conference in Königsberg the following week.

在他的研究过程中，哥德尔发现，尽管一个断言自己错误的句子会导致悖论，但一个断言自己无法证明的句子却不会。特别是，哥德尔知道这个现在被称为塔尔斯基不确定性定理的结果，尽管他从未发表过它。1930年8月26日，哥德尔向卡尔纳普、费格尔和 Waismann 宣布了他的第一个不完备性定理，四人都将参加第二届精确科学认识论会议，下周在柯尼斯堡举行的一个关键会议。

Announcement

The 1930 Königsberg conference was a joint meeting of three academic societies, with many of the key logicians of the time in attendance. Carnap, Heyting, and von Neumann delivered one-hour addresses on the mathematical philosophies of logicism, intuitionism, and formalism, respectively 模板:Harv. The conference also included Hilbert's retirement address, as he was leaving his position at the University of Göttingen. Hilbert used the speech to argue his belief that all mathematical problems can be solved. He ended his address by saying,

For the mathematician there is no Ignorabimus, and, in my opinion, not at all for natural science either. ... The true reason why [no one] has succeeded in finding an unsolvable problem is, in my opinion, that there is no unsolvable problem. In contrast to the foolish Ignorabimus, our credo avers: We must know. We shall know!

This speech quickly became known as a summary of Hilbert's beliefs on mathematics (its final six words, "Wir müssen wissen. Wir werden wissen!", were used as Hilbert's epitaph in 1943). Although Gödel was likely in attendance for Hilbert's address, the two never met face to face 模板:Harv.

The 1930 Königsberg conference was a joint meeting of three academic societies, with many of the key logicians of the time in attendance. Carnap, Heyting, and von Neumann delivered one-hour addresses on the mathematical philosophies of logicism, intuitionism, and formalism, respectively . The conference also included Hilbert's retirement address, as he was leaving his position at the University of Göttingen. Hilbert used the speech to argue his belief that all mathematical problems can be solved. He ended his address by saying,

This speech quickly became known as a summary of Hilbert's beliefs on mathematics (its final six words, "Wir müssen wissen. Wir werden wissen!", were used as Hilbert's epitaph in 1943). Although Gödel was likely in attendance for Hilbert's address, the two never met face to face .

1930年的哥尼斯堡会议是三个学术团体的联合会议，当时许多关键的逻辑学家出席了会议。卡尔纳普、海廷和冯 · 诺依曼分别就逻辑主义、直觉主义和形式主义的数学哲学发表了一个小时的演讲。会议还包括 Hilbert 的退休演说，当时他正准备离开他在哥廷根大学的职位。希尔伯特用这篇演讲来论证他的信念，即所有的数学问题都可以解决。他在演讲结束时说: “这篇演讲很快成为众所周知的希尔伯特数学信仰的总结(它的最后六个字，“ Wir müller wissen”)。Wir werden wissen!在1943年被用作希尔伯特的墓志铭)。虽然哥德尔很可能出席了希尔伯特的演讲，但他们从未见过面。

Gödel announced his first incompleteness theorem at a roundtable discussion session on the third day of the conference. The announcement drew little attention apart from that of von Neumann, who pulled Gödel aside for conversation. Later that year, working independently with knowledge of the first incompleteness theorem, von Neumann obtained a proof of the second incompleteness theorem, which he announced to Gödel in a letter dated November 20, 1930 模板:Harv. Gödel had independently obtained the second incompleteness theorem and included it in his submitted manuscript, which was received by Monatshefte für Mathematik on November 17, 1930.

Gödel announced his first incompleteness theorem at a roundtable discussion session on the third day of the conference. The announcement drew little attention apart from that of von Neumann, who pulled Gödel aside for conversation. Later that year, working independently with knowledge of the first incompleteness theorem, von Neumann obtained a proof of the second incompleteness theorem, which he announced to Gödel in a letter dated November 20, 1930 . Gödel had independently obtained the second incompleteness theorem and included it in his submitted manuscript, which was received by Monatshefte für Mathematik on November 17, 1930.

哥德尔在会议第三天的圆桌讨论会上宣布了他的第一个不完备性定理。除了冯 · 诺伊曼(von Neumann)把哥德尔拉到一边进行谈话之外，这份声明几乎没有引起人们的注意。1930年11月20日，冯 · 诺依曼在给哥德尔的一封信中宣布了第二个不完备性定理的证明。哥德尔独立地获得了第二个不完备性定理，并把它收入了他提交的手稿中，这份手稿于1930年11月17日被 Monatshefte für mathematica 收到。

Gödel's paper was published in the Monatshefte in 1931 under the title "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" ("On Formally Undecidable Propositions in Principia Mathematica and Related Systems I"). As the title implies, Gödel originally planned to publish a second part of the paper in the next volume of the Monatshefte; the prompt acceptance of the first paper was one reason he changed his plans 模板:Harv.

Gödel's paper was published in the Monatshefte in 1931 under the title "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" ("On Formally Undecidable Propositions in Principia Mathematica and Related Systems I"). As the title implies, Gödel originally planned to publish a second part of the paper in the next volume of the Monatshefte; the prompt acceptance of the first paper was one reason he changed his plans .

哥德尔的论文于1931年发表在《单子》杂志上，题目是“超越正式的不可判定的数学原理和可判定的系统 i”(论数学原理及相关系统 i 中的正式不可判定命题)。正如标题所暗示的，哥德尔最初计划在下一卷《莫纳特夫特》中发表论文的第二部分; 第一篇论文的迅速接受是他改变计划的原因之一。

Generalization and acceptance

= = 归纳和接受 = =

Gödel gave a series of lectures on his theorems at Princeton in 1933–1934 to an audience that included Church, Kleene, and Rosser. By this time, Gödel had grasped that the key property his theorems required is that the system must be effective (at the time, the term "general recursive" was used). Rosser proved in 1936 that the hypothesis of ω-consistency, which was an integral part of Gödel's original proof, could be replaced by simple consistency, if the Gödel sentence was changed in an appropriate way. These developments left the incompleteness theorems in essentially their modern form.

1933年至1934年间，哥德尔在普林斯顿大学(Princeton)就他的定理发表了一系列演讲，听众包括丘奇、克莱恩(Kleene)和罗瑟(Rosser)。此时，哥德尔已经掌握了他的定理所要求的关键性质，即系统必须是有效的(当时使用了“一般递归”这个术语)。罗塞尔在1936年证明了作为哥德尔原始证明不可分割的一部分的 ω- 一致性假设可以被简单的一致性假设所取代，只要哥德尔句子被适当地改变。这些发展使不完备性定理在本质上成为现代形式。

Gentzen published his consistency proof for first-order arithmetic in 1936. Hilbert accepted this proof as "finitary" although (as Gödel's theorem had already shown) it cannot be formalized within the system of arithmetic that is being proved consistent.

根岑在1936年出版了他的《一阶算术一致性》。希尔伯特认为这个证明是“有限的”(正如哥德尔定理已经证明的那样) ，尽管它不能在被证明是一致的算术体系内形式化。

The impact of the incompleteness theorems on Hilbert's program was quickly realized. Bernays included a full proof of the incompleteness theorems in the second volume of Grundlagen der Mathematik ([[#模板:Harvid|1939]]), along with additional results of Ackermann on the ε-substitution method and Gentzen's consistency proof of arithmetic. This was the first full published proof of the second incompleteness theorem.

The impact of the incompleteness theorems on Hilbert's program was quickly realized. Bernays included a full proof of the incompleteness theorems in the second volume of Grundlagen der Mathematik (1939), along with additional results of Ackermann on the ε-substitution method and Gentzen's consistency proof of arithmetic. This was the first full published proof of the second incompleteness theorem.

不完备性定理对希尔伯特程序的影响很快被认识到。伯奈斯包括了 Grundlagen 《数学》(1939)第二卷中关于不完备性定理的完整证明，以及阿克曼关于 ε- 替换方法和根岑的算术一致性的额外结果。这是第二个不完备性定理的第一个完整证明。

Criticisms

= = 批评 =

Finsler

模板:Harvard citations used a version of Richard's paradox to construct an expression that was false but unprovable in a particular, informal framework he had developed. Gödel was unaware of this paper when he proved the incompleteness theorems (Collected Works Vol. IV., p. 9). Finsler wrote to Gödel in 1931 to inform him about this paper, which Finsler felt had priority for an incompleteness theorem. Finsler's methods did not rely on formalized provability, and had only a superficial resemblance to Gödel's work 模板:Harv. Gödel read the paper but found it deeply flawed, and his response to Finsler laid out concerns about the lack of formalization (脚本错误：没有“Footnotes”这个模块。模板:Full citation needed). Finsler continued to argue for his philosophy of mathematics, which eschewed formalization, for the remainder of his career.

used a version of Richard's paradox to construct an expression that was false but unprovable in a particular, informal framework he had developed. Gödel was unaware of this paper when he proved the incompleteness theorems (Collected Works Vol. IV., p. 9). Finsler wrote to Gödel in 1931 to inform him about this paper, which Finsler felt had priority for an incompleteness theorem. Finsler's methods did not rely on formalized provability, and had only a superficial resemblance to Gödel's work . Gödel read the paper but found it deeply flawed, and his response to Finsler laid out concerns about the lack of formalization (). Finsler continued to argue for his philosophy of mathematics, which eschewed formalization, for the remainder of his career.

= = = 芬斯勒用理查德悖论的一个版本构造了一个表达式，这个表达式在他开发的一个特定的非正式框架中是错误的，但是无法证明。哥德尔在证明不完备性定理时并不知道这篇论文。IV., p. 9).芬斯勒在1931年写信给哥德尔，告诉他这篇论文，芬斯勒认为这篇论文优先于一个不完备性定理。芬斯勒的方法并不依赖于形式化的证明，而且与哥德尔的工作只有表面上的相似之处。哥德尔读了这篇论文，但发现它存在严重缺陷，他对芬斯勒的回应表达了对缺乏正规化的担忧。芬斯勒在余下的职业生涯中继续为他的数学哲学辩护，这种哲学避免了形式化。

Zermelo

In September 1931, Ernst Zermelo wrote to Gödel to announce what he described as an "essential gap" in Gödel's argument (脚本错误：没有“Footnotes”这个模块。模板:Full citation needed). In October, Gödel replied with a 10-page letter (脚本错误：没有“Footnotes”这个模块。模板:Full citation needed, 脚本错误：没有“Footnotes”这个模块。模板:Full citation needed), where he pointed out that Zermelo mistakenly assumed that the notion of truth in a system is definable in that system (which is not true in general by Tarski's undefinability theorem). But Zermelo did not relent and published his criticisms in print with "a rather scathing paragraph on his young competitor" (脚本错误：没有“Footnotes”这个模块。模板:Full citation needed). Gödel decided that to pursue the matter further was pointless, and Carnap agreed (脚本错误：没有“Footnotes”这个模块。模板:Full citation needed). Much of Zermelo's subsequent work was related to logics stronger than first-order logic, with which he hoped to show both the consistency and categoricity of mathematical theories.

In September 1931, Ernst Zermelo wrote to Gödel to announce what he described as an "essential gap" in Gödel's argument (). In October, Gödel replied with a 10-page letter (, ), where he pointed out that Zermelo mistakenly assumed that the notion of truth in a system is definable in that system (which is not true in general by Tarski's undefinability theorem). But Zermelo did not relent and published his criticisms in print with "a rather scathing paragraph on his young competitor" (). Gödel decided that to pursue the matter further was pointless, and Carnap agreed (). Much of Zermelo's subsequent work was related to logics stronger than first-order logic, with which he hoped to show both the consistency and categoricity of mathematical theories.

1931年9月，恩斯特 · 泽梅洛写信给哥德尔，宣布他所说的哥德尔论点中的“本质差距”。10月，哥德尔回复了一封长达10页的信(,) ，他在信中指出，泽梅洛错误地认为，一个系统中的真理概念在该系统中是可定义的(这在塔斯基的不可定义性定理中一般是不正确的)。但是策梅洛并没有松口，他用印刷版发表了他的批评，“对他年轻的竞争对手相当严厉的段落”()。哥德尔认为进一步研究这个问题是没有意义的，卡尔纳普对此表示同意()。后来的许多著作都与比一阶逻辑更强的逻辑学有关，他希望借此展示数学理论的一致性和分类性。

Wittgenstein

Ludwig Wittgenstein wrote several passages about the incompleteness theorems that were published posthumously in his 1953 Remarks on the Foundations of Mathematics, in particular one section sometimes called the "notorious paragraph" where he seems to confuse the notions of "true" and "provable" in Russell's system. Gödel was a member of the Vienna Circle during the period in which Wittgenstein's early ideal language philosophy and Tractatus Logico-Philosophicus dominated the circle's thinking. There has been some controversy about whether Wittgenstein misunderstood the incompleteness theorem or just expressed himself unclearly. Writings in Gödel's Nachlass express the belief that Wittgenstein misread his ideas.

Ludwig Wittgenstein wrote several passages about the incompleteness theorems that were published posthumously in his 1953 Remarks on the Foundations of Mathematics, in particular one section sometimes called the "notorious paragraph" where he seems to confuse the notions of "true" and "provable" in Russell's system. Gödel was a member of the Vienna Circle during the period in which Wittgenstein's early ideal language philosophy and Tractatus Logico-Philosophicus dominated the circle's thinking. There has been some controversy about whether Wittgenstein misunderstood the incompleteness theorem or just expressed himself unclearly. Writings in Gödel's Nachlass express the belief that Wittgenstein misread his ideas.

他在1953年发表在《路德维希·维特根斯坦数学基础上的评论》中，特别是其中一个有时被称为“臭名昭著的段落”的章节中，他似乎混淆了罗素系统中“真”和“可证明”的概念。在维特根斯坦早期理想语言哲学和逻辑哲学论主导维也纳学派思想的时期，哥德尔是维也纳学派的成员。关于维特根斯坦是否误解了不完全性定理，或者只是模糊地表达了自己的观点，一直存在争议。哥德尔《夜》中的文字表达了维特根斯坦误读了他的思想的信念。

Multiple commentators have read Wittgenstein as misunderstanding Gödel 模板:Harv, although Juliet Floyd and 模板:Harvard citations, as well as 模板:Harvard citations have provided textual readings arguing that most commentary misunderstands Wittgenstein. On their release, Bernays, Dummett, and Kreisel wrote separate reviews on Wittgenstein's remarks, all of which were extremely negative 模板:Harv. The unanimity of this criticism caused Wittgenstein's remarks on the incompleteness theorems to have little impact on the logic community. In 1972, Gödel stated: "Has Wittgenstein lost his mind? Does he mean it seriously? He intentionally utters trivially nonsensical statements" 模板:Harv, and wrote to Karl Menger that Wittgenstein's comments demonstrate a misunderstanding of the incompleteness theorems writing:

Multiple commentators have read Wittgenstein as misunderstanding Gödel , although Juliet Floyd and , as well as have provided textual readings arguing that most commentary misunderstands Wittgenstein. On their release, Bernays, Dummett, and Kreisel wrote separate reviews on Wittgenstein's remarks, all of which were extremely negative . The unanimity of this criticism caused Wittgenstein's remarks on the incompleteness theorems to have little impact on the logic community. In 1972, Gödel stated: "Has Wittgenstein lost his mind? Does he mean it seriously? He intentionally utters trivially nonsensical statements" , and wrote to Karl Menger that Wittgenstein's comments demonstrate a misunderstanding of the incompleteness theorems writing:

许多评论家认为维特根斯坦误解了哥德尔，尽管朱丽叶 · 弗洛伊德和，以及提供了文本解读，认为大多数评论误解了维特根斯坦。在他们发布的时候，伯奈斯、达米特和克瑞塞尔分别对维特根斯坦的言论写了评论，所有这些评论都是极端负面的。这种批评的一致性使得维特根斯坦关于不完备性定理的评论对逻辑学界影响甚微。1972年，哥德尔说: “维特根斯坦疯了吗？他是认真的吗？他故意发表了一些毫无意义的陈述”，并写信给卡尔•门格尔(Karl Menger)称，维特根斯坦的评论表明，他对不完整性定理存在误解。他写道:

It is clear from the passages you cite that Wittgenstein did not understand [the first incompleteness theorem] (or pretended not to understand it). He interpreted it as a kind of logical paradox, while in fact is just the opposite, namely a mathematical theorem within an absolutely uncontroversial part of mathematics (finitary number theory or combinatorics). 模板:Harv

Since the publication of Wittgenstein's Nachlass in 2000, a series of papers in philosophy have sought to evaluate whether the original criticism of Wittgenstein's remarks was justified. 脚本错误：没有“Footnotes”这个模块。 argue that Wittgenstein had a more complete understanding of the incompleteness theorem than was previously assumed. They are particularly concerned with the interpretation of a Gödel sentence for an ω-inconsistent system as actually saying "I am not provable", since the system has no models in which the provability predicate corresponds to actual provability. 脚本错误：没有“Footnotes”这个模块。 argues that their interpretation of Wittgenstein is not historically justified, while 脚本错误：没有“Footnotes”这个模块。 argues against Floyd and Putnam's philosophical analysis of the provability predicate. 脚本错误：没有“Footnotes”这个模块。 explores the relationship between Wittgenstein's writing and theories of paraconsistent logic.

Since the publication of Wittgenstein's Nachlass in 2000, a series of papers in philosophy have sought to evaluate whether the original criticism of Wittgenstein's remarks was justified. argue that Wittgenstein had a more complete understanding of the incompleteness theorem than was previously assumed. They are particularly concerned with the interpretation of a Gödel sentence for an ω-inconsistent system as actually saying "I am not provable", since the system has no models in which the provability predicate corresponds to actual provability. argues that their interpretation of Wittgenstein is not historically justified, while argues against Floyd and Putnam's philosophical analysis of the provability predicate. explores the relationship between Wittgenstein's writing and theories of paraconsistent logic.

自从2000年维特根斯坦的《纳克拉斯》出版以来，一系列哲学论文试图评估对维特根斯坦言论的最初批评是否合理。他们认为维特根斯坦对不完备性定理的理解比先前假设的更加完整。他们特别关注对于 ω- 不一致系统的哥德尔句子的解释，因为该系统没有可证明性谓词与实际可证明性相对应的模型。他们对维特根斯坦的解释是不具有历史正当性的，而反对弗洛伊德和普特南对可证明性谓词的哲学分析。探讨了维特根斯坦的写作与次协调逻辑理论之间的关系。

References

Citations

↑ Shelah, Saharon (1974). "Infinite Abelian groups, Whitehead problem and some constructions". Israel Journal of Mathematics. 18 (3): 243–256. doi:10.1007/BF02757281. MR 0357114.
↑ ^2.0 ^2.1 Hofstadter, Douglas R. (2007). "Chapter 12. On Downward Causality". I Am a Strange Loop. ISBN 978-0-465-03078-1. https://publicism.info/philosophy/strange/14.html.

Articles by Gödel

Kurt Gödel, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", Monatshefte für Mathematik und Physik, v. 38 n. 1, pp. 173–198. doi:10.1007/BF01700692

—, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", in Solomon Feferman, ed., 1986. Kurt Gödel Collected works, Vol. I. Oxford University Press, pp. 144–195.

. The original German with a facing English translation, preceded by an introductory note by Stephen Cole Kleene.

—, 1951, "Some basic theorems on the foundations of mathematics and their implications", in Solomon Feferman, ed., 1995. Kurt Gödel Collected works, Vol. III, Oxford University Press, pp. 304–323.

.

Kurt Gödel, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", Monatshefte für Mathematik und Physik, v. 38 n. 1, pp. 173–198.
—, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", in Solomon Feferman, ed., 1986. Kurt Gödel Collected works, Vol. I. Oxford University Press, pp. 144–195. . The original German with a facing English translation, preceded by an introductory note by Stephen Cole Kleene.
—, 1951, "Some basic theorems on the foundations of mathematics and their implications", in Solomon Feferman, ed., 1995. Kurt Gödel Collected works, Vol. III, Oxford University Press, pp. 304–323. .

Articles by Gödel

Kurt Gödel, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", Monatshefte für Mathematik und Physik, v. 38 n. 1, pp.173–198.
—, 1931, "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I", in Solomon Feferman, ed., 1986.库尔特 · 哥德尔作品集，第一卷。牛津大学出版社，页。144–195..德文原文，英文翻译，之前有斯蒂芬·科尔·克莱尼的介绍性说明。
ー，1951，“关于数学基础及其含义的一些基本定理”，Solomon Feferman，ed，1995。库尔特 · 哥德尔作品集，第卷。牛津大学出版社，第三版。304–323..

Translations, during his lifetime, of Gödel's paper into English

None of the following agree in all translated words and in typography. The typography is a serious matter, because Gödel expressly wished to emphasize "those metamathematical notions that had been defined in their usual sense before . . ." 模板:Harv. Three translations exist. Of the first John Dawson states that: "The Meltzer translation was seriously deficient and received a devastating review in the Journal of Symbolic Logic; "Gödel also complained about Braithwaite's commentary 模板:Harv. "Fortunately, the Meltzer translation was soon supplanted by a better one prepared by Elliott Mendelson for Martin Davis's anthology The Undecidable . . . he found the translation "not quite so good" as he had expected . . . [but because of time constraints he] agreed to its publication" (ibid). (In a footnote Dawson states that "he would regret his compliance, for the published volume was marred throughout by sloppy typography and numerous misprints" (ibid)). Dawson states that "The translation that Gödel favored was that by Jean van Heijenoort" (ibid). For the serious student another version exists as a set of lecture notes recorded by Stephen Kleene and J. B. Rosser "during lectures given by Gödel at to the Institute for Advanced Study during the spring of 1934" (cf commentary by 脚本错误：没有“Footnotes”这个模块。 and beginning on p. 41); this version is titled "On Undecidable Propositions of Formal Mathematical Systems". In their order of publication:

B. Meltzer (translation) and R. B. Braithwaite (Introduction), 1962. On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Dover Publications, New York (Dover edition 1992),

(pbk.) This contains a useful translation of Gödel's German abbreviations on pp. 33–34. As noted above, typography, translation and commentary is suspect. Unfortunately, this translation was reprinted with all its suspect content by

Stephen Hawking editor, 2005. God Created the Integers: The Mathematical Breakthroughs That Changed History, Running Press, Philadelphia,

. Gödel's paper appears starting on p. 1097, with Hawking's commentary starting on p. 1089.

Martin Davis editor, 1965. The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable problems and Computable Functions, Raven Press, New York, no ISBN. Gödel's paper begins on page 5, preceded by one page of commentary.

Jean van Heijenoort editor, 1967, 3rd edition 1967. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, Cambridge Mass.,

(pbk). van Heijenoort did the translation. He states that "Professor Gödel approved the translation, which in many places was accommodated to his wishes." (p. 595). Gödel's paper begins on p. 595; van Heijenoort's commentary begins on p. 592.

Martin Davis editor, 1965, ibid. "On Undecidable Propositions of Formal Mathematical Systems." A copy with Gödel's corrections of errata and Gödel's added notes begins on page 41, preceded by two pages of Davis's commentary. Until Davis included this in his volume this lecture existed only as mimeographed notes.

None of the following agree in all translated words and in typography. The typography is a serious matter, because Gödel expressly wished to emphasize "those metamathematical notions that had been defined in their usual sense before . . ." . Three translations exist. Of the first John Dawson states that: "The Meltzer translation was seriously deficient and received a devastating review in the Journal of Symbolic Logic; "Gödel also complained about Braithwaite's commentary . "Fortunately, the Meltzer translation was soon supplanted by a better one prepared by Elliott Mendelson for Martin Davis's anthology The Undecidable . . . he found the translation "not quite so good" as he had expected . . . [but because of time constraints he] agreed to its publication" (ibid). (In a footnote Dawson states that "he would regret his compliance, for the published volume was marred throughout by sloppy typography and numerous misprints" (ibid)). Dawson states that "The translation that Gödel favored was that by Jean van Heijenoort" (ibid). For the serious student another version exists as a set of lecture notes recorded by Stephen Kleene and J. B. Rosser "during lectures given by Gödel at to the Institute for Advanced Study during the spring of 1934" (cf commentary by and beginning on p. 41); this version is titled "On Undecidable Propositions of Formal Mathematical Systems". In their order of publication:

B. Meltzer (translation) and R. B. Braithwaite (Introduction), 1962. On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Dover Publications, New York (Dover edition 1992), (pbk.) This contains a useful translation of Gödel's German abbreviations on pp. 33–34. As noted above, typography, translation and commentary is suspect. Unfortunately, this translation was reprinted with all its suspect content by

Stephen Hawking editor, 2005. God Created the Integers: The Mathematical Breakthroughs That Changed History, Running Press, Philadelphia, . Gödel's paper appears starting on p. 1097, with Hawking's commentary starting on p. 1089.

Martin Davis editor, 1965. The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable problems and Computable Functions, Raven Press, New York, no ISBN. Gödel's paper begins on page 5, preceded by one page of commentary.
Jean van Heijenoort editor, 1967, 3rd edition 1967. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, Cambridge Mass., (pbk). van Heijenoort did the translation. He states that "Professor Gödel approved the translation, which in many places was accommodated to his wishes." (p. 595). Gödel's paper begins on p. 595; van Heijenoort's commentary begins on p. 592.
Martin Davis editor, 1965, ibid. "On Undecidable Propositions of Formal Mathematical Systems." A copy with Gödel's corrections of errata and Gödel's added notes begins on page 41, preceded by two pages of Davis's commentary. Until Davis included this in his volume this lecture existed only as mimeographed notes.

在哥德尔有生之年，他将他的论文翻译成英文。字体设计是一个严肃的问题，因为哥德尔明确地希望强调“那些元数学概念已经被定义在他们的通常意义之前。..".存在三种翻译。关于第一本《约翰 · 道森》，他说: “梅尔策的翻译严重不足，在《符号逻辑》杂志上受到了毁灭性的评论;”哥德尔还抱怨布雷斯韦特的评论。“幸运的是，梅尔策的译本很快被埃利奥特 · 门德尔松为马丁 · 戴维斯的选集《无法判定》所准备的更好的译本所取代。..他发现翻译不如他预期的那么好。..(但由于时间限制，他)同意出版这本书。”。(在一个脚注中，道森说: “他会后悔自己遵守了规定，因为出版的全部都被粗糙的排版和无数的印刷错误破坏了”(同上)。道森说，“哥德尔最喜欢的译本是让 · 范 · 海耶诺特的”(同上)。对于严肃的学生来说，另一个版本是由斯蒂芬 · 克莱恩和 j 记录的一套课堂笔记。B. Rosser”在哥德尔于1934年春天在高等研究所所作的讲座中”(见第41页的注释) ; 这个版本的题目是”关于形式数学系统的不可判定命题”。按出版顺序:

b. Meltzer (翻译)和 r. b. Braithwaite (引言) ，1962年。关于数学原理及相关系统的正式不可判定命题，多佛出版社，纽约(多佛版，1992) ，(pbk.)这里有一个很有用的翻译，是哥德尔在德语中 pp 的缩写。33–34.如上所述，字体、翻译和评论都值得怀疑。不幸的是，这个译本和它所有可疑的内容都被转载了:
斯蒂芬 · 霍金编辑，2005年。上帝创造了整数: 改变历史的数学突破》，Running Press，Philadelphia，。哥德尔的论文从第1097页开始，霍金的评论从第1089页开始。
马丁 · 戴维斯编辑，1965年。无法判定的: 关于无法判定命题、无法解决的问题和可计算函数的基本论文，瑞文出版社，纽约，无国际标准书号。哥德尔的论文从第5页开始，前面是一页的评论。
Jean van Heijenoort 编辑，1967，第三版1967。《从弗雷格到哥德尔: 数理逻辑的源书，1879-1931》，哈佛大学出版社，麻省剑桥出版社，(pbk)。范 · 海耶诺特做了翻译。他说，“哥德尔教授批准了这个译本，这在许多地方符合他的愿望。”(p. 595).哥德尔的论文开始于第595页; 范 · 海耶诺特的评论开始于第592页。
马丁 · 戴维斯编辑，1965，同上。关于形式数学系统的不可判定命题第41页开始是哥德尔对勘误和哥德尔附加注释的改正，前面是两页戴维斯的评论。直到戴维斯在他的卷中包括这个讲座只存在作为油印笔记。

Articles by others

George Boolos, 1989, "A New Proof of the Gödel Incompleteness Theorem", Notices of the American Mathematical Society, v, 36, pp. 388–390 and p. 676, reprinted in Boolos, 1998, Logic, Logic, and Logic, Harvard Univ. Press.

Bernd Buldt, 2014, "The Scope of Gödel's First Incompleteness Theorem", Logica Universalis, v. 8, pp. 499–552. doi:10.1007/s11787-014-0107-3
Arthur Charlesworth, 1980, "A Proof of Godel's Theorem in Terms of Computer Programs", Mathematics Magazine, v. 54 n. 3, pp. 109–121. 模板:JSTOR
Martin Davis, 2006, "The Incompleteness Theorem", Notices of the AMS, v. 53 n. 4, pp. 414.
Jean van Heijenoort, 1963, "Gödel's Theorem" in Edwards, Paul, ed., Encyclopedia of Philosophy, v. 3. Macmillan, pp. 348–57.
Geoffrey Hellman, 1981, "How to Gödel a Frege-Russell: Gödel's Incompleteness Theorems and Logicism", Noûs, v. 15 n. 4, Special Issue on Philosophy of Mathematics, pp. 451–468.
David Hilbert, 1900, "Mathematical Problems." English translation of a lecture delivered before the International Congress of Mathematicians at Paris, containing Hilbert's statement of his Second Problem.
Martin Hirzel, 2000, "On formally undecidable propositions of Principia Mathematica and related systems I.." An English translation of Gödel's paper. Archived from the original. Sept. 16, 2004.
Makoto Kikuchi and Kazayuki Tanaka, 1994, "On formalization of model-theoretic proofs of Gödel's theorems", Notre Dame Journal of Formal Logic, v. 5 n. 3, pp. 403–412. doi:10.1305/ndjfl/1040511346 模板:Mr
Stephen Cole Kleene, 1943, "Recursive predicates and quantifiers", reprinted from Transactions of the American Mathematical Society, v. 53 n. 1, pp. 41–73 in Martin Davis 1965, The Undecidable (loc. cit.) pp. 255–287.
Panu Raatikainen, 2015, "Gödel's Incompleteness Theorems", Stanford Encyclopedia of Philosophy. Accessed April 3, 2015.
Panu Raatikainen, 2005, "On the philosophical relevance of Gödel's incompleteness theorems", Revue Internationale de Philosophie 59 (4):513-534.
John Barkley Rosser, 1936, "Extensions of some theorems of Gödel and Church", reprinted from the Journal of Symbolic Logic, v. 1 (1936) pp. 87–91, in Martin Davis 1965, The Undecidable (loc. cit.) pp. 230–235.
—, 1939, "An Informal Exposition of proofs of Gödel's Theorem and Church's Theorem", Reprinted from the Journal of Symbolic Logic, v. 4 (1939) pp. 53–60, in Martin Davis 1965, The Undecidable (loc. cit.) pp. 223–230

C. Smoryński, 1982, "The incompleteness theorems", in Jon Barwise, ed., Handbook of Mathematical Logic, North-Holland, pp. 821–866.

Dan E. Willard, 2001, "Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles", Journal of Symbolic Logic, v. 66 n. 2, pp. 536–596. doi:10.2307/2695030 模板:JSTOR
Zach, Richard (2003). "The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program" (PDF). Synthese. Springer Science and Business Media LLC. 137 (1): 211–259. arXiv:math/0102189. doi:10.1023/a:1026247421383. ISSN 0039-7857. S2CID 16657040.
Zach, Richard (2005). "Kurt Gödel, paper on the incompleteness theorems (1931)". In Grattan-Guinness, Ivor. Landmark Writings in Western Mathematics 1640-1940. Elsevier. pp. 917–925. doi:10.1016/b978-044450871-3/50152-2. ISBN 9780444508713. https://philarchive.org/rec/ZACKGP.

George Boolos, 1989, "A New Proof of the Gödel Incompleteness Theorem", Notices of the American Mathematical Society, v, 36, pp. 388–390 and p. 676, reprinted in Boolos, 1998, Logic, Logic, and Logic, Harvard Univ. Press.
Bernd Buldt, 2014, "The Scope of Gödel's First Incompleteness Theorem", Logica Universalis, v. 8, pp. 499–552.
Arthur Charlesworth, 1980, "A Proof of Godel's Theorem in Terms of Computer Programs", Mathematics Magazine, v. 54 n. 3, pp. 109–121.
Martin Davis, 2006, "The Incompleteness Theorem", Notices of the AMS, v. 53 n. 4, pp. 414.
Jean van Heijenoort, 1963, "Gödel's Theorem" in Edwards, Paul, ed., Encyclopedia of Philosophy, v. 3. Macmillan, pp. 348–57.
Geoffrey Hellman, 1981, "How to Gödel a Frege-Russell: Gödel's Incompleteness Theorems and Logicism", Noûs, v. 15 n. 4, Special Issue on Philosophy of Mathematics, pp. 451–468.
David Hilbert, 1900, "Mathematical Problems." English translation of a lecture delivered before the International Congress of Mathematicians at Paris, containing Hilbert's statement of his Second Problem.
Martin Hirzel, 2000, "On formally undecidable propositions of Principia Mathematica and related systems I.." An English translation of Gödel's paper. Archived from the original. Sept. 16, 2004.
Makoto Kikuchi and Kazayuki Tanaka, 1994, "On formalization of model-theoretic proofs of Gödel's theorems", Notre Dame Journal of Formal Logic, v. 5 n. 3, pp. 403–412.
Stephen Cole Kleene, 1943, "Recursive predicates and quantifiers", reprinted from Transactions of the American Mathematical Society, v. 53 n. 1, pp. 41–73 in Martin Davis 1965, The Undecidable (loc. cit.) pp. 255–287.
Panu Raatikainen, 2015, "Gödel's Incompleteness Theorems", Stanford Encyclopedia of Philosophy. Accessed April 3, 2015.
Panu Raatikainen, 2005, "On the philosophical relevance of Gödel's incompleteness theorems", Revue Internationale de Philosophie 59 (4):513-534.
John Barkley Rosser, 1936, "Extensions of some theorems of Gödel and Church", reprinted from the Journal of Symbolic Logic, v. 1 (1936) pp. 87–91, in Martin Davis 1965, The Undecidable (loc. cit.) pp. 230–235.
—, 1939, "An Informal Exposition of proofs of Gödel's Theorem and Church's Theorem", Reprinted from the Journal of Symbolic Logic, v. 4 (1939) pp. 53–60, in Martin Davis 1965, The Undecidable (loc. cit.) pp. 223–230
C. Smoryński, 1982, "The incompleteness theorems", in Jon Barwise, ed., Handbook of Mathematical Logic, North-Holland, pp. 821–866.
Dan E. Willard, 2001, "Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles", Journal of Symbolic Logic, v. 66 n. 2, pp. 536–596.

= = 其他人撰写的文章 = =

George Boolos，1989，“哥德尔不完全性定理的新证明”，《美国数学学会通告》，第 v，36页。388-390 and p. 676，转载于 Boolos，1998，Logic，Logic，and Logic，Harvard univ。新闻稿。
Bernd Buldt，2014，“ The Scope of The Gödel’s First inteness Theorem”，Logica Universalis，v. 8，pp。499–552.
Arthur Charlesworth，1980，“ a Proof of Godel’s Theorem in Terms of Computer Programs”，Mathematics Magazine，v. 54 n. 3，pp。109–121.
Martin Davis，2006，“ The Incompleteness Theorem”，Notices of The AMS，v. 53 n. 4，pp。414.
Jean van Heijenoort，1963，“哥德尔定理”in Edwards，Paul，ed，Encyclopedia of Philosophy v. 3。Macmillan, pp.348–57.
Geoffrey Hellman，1981，“ How to Gödel a Frege-Russell: Gödel’s incompletion theores and Logicism”，Noûs，v. 15 n. 4，Special Issue on Philosophy of Mathematics，pp。451–468.
David Hilbert，1900，“ Mathematical Problems”在巴黎国际数学家大会大会上发表的演讲的英译本，其中包括希尔伯特关于他的第二个问题的声明。
Martin Hirzel，2000，“关于数学原理和相关系统 i 的正式不可判定命题。”哥德尔论文的英译本。从原件里存档的。2004年9月16日。
Makoto Kikuchi and Kazayuki Tanaka，1994，“ On formalization of model-------------------------------------------------- 关于哥德尔定理的模型论证明”，Notre Dame Journal of Formal Logic，v. 5 n. 3，pp。403–412.斯蒂芬·科尔·克莱尼，1943，“ Recursive predicates and quantifier”，reprint from Transactions of the American Mathematical Society，v. 53 n. 1，pp。41-73 in Martin Davis 1965，The undecutable (loc.Cit。)聚丙烯。255–287.
Panu Raatikainen，2015，“哥德尔的不完备性定理”，《斯坦福大学哲学百科全书。3,2015.
Panu Raatikainen，2005，“ On the philosophical relevance of Gödel’s incompletion theories”，Revue Internationale de hie 59(4) : 513-534。
John Barkley Rosser，1936，“ Gödel 和 Church 的一些定理的扩展”，转载自《符号逻辑杂志》，第1(1936)页。87-91，在马丁 · 戴维斯1965年，无法判定的。Cit。)聚丙烯。230–235.
ー，1939，“哥德尔定理和丘奇定理证明的非正式论述”，转载自《符号逻辑学杂志》，第4(1939)页。53-60，在马丁戴维斯1965年，无法判定的。Cit。)聚丙烯。223-230
c. smory ski，1982，“不完备性定理”，收录于 Jon Barwise，ed.Handbook of Mathematical Logic，North-Holland，pp。821–866.丹 · e · 威拉德，2001年，“自我验证公理系统，不完全性定理和相关的反映原则”，《符号逻辑杂志》，第66页，第2页。536–596.

Books about the theorems

Francesco Berto. There's Something about Gödel: The Complete Guide to the Incompleteness Theorem John Wiley and Sons. 2010.

Norbert Domeisen, 1990. Logik der Antinomien. Bern: Peter Lang. 142 S. 1990.

. 模板:Zbl.

Torkel Franzén, 2005. Gödel's Theorem: An Incomplete Guide to its Use and Abuse. A.K. Peters.

模板:MR

Douglas Hofstadter, 1979. Gödel, Escher, Bach: An Eternal Golden Braid. Vintage Books.

. 1999 reprint:

. 模板:MR

—, 2007. I Am a Strange Loop. Basic Books.

.

. 模板:MR

Stanley Jaki, OSB, 2005. The drama of the quantities. Real View Books.
Per Lindström, 1997. Aspects of Incompleteness, Lecture Notes in Logic v. 10.
J.R. Lucas, FBA, 1970. The Freedom of the Will. Clarendon Press, Oxford, 1970.

Ernest Nagel, James Roy Newman, Douglas Hofstadter, 2002 (1958). Gödel's Proof, revised ed.

. 模板:MR

Rudy Rucker, 1995 (1982). Infinity and the Mind: The Science and Philosophy of the Infinite. Princeton Univ. Press. 模板:MR
Peter Smith, 2007. An Introduction to Gödel's Theorems. Cambridge University Press. 模板:MR

N. Shankar, 1994. Metamathematics, Machines and Gödel's Proof, Volume 38 of Cambridge tracts in theoretical computer science.

Raymond Smullyan, 1987. Forever Undecided

- puzzles based on undecidability in formal systems

—, 1991. Godel's Incompleteness Theorems. Oxford Univ. Press.
—, 1994. Diagonalization and Self-Reference. Oxford Univ. Press. 模板:MR

—, 2013. The Godelian Puzzle Book: Puzzles, Paradoxes and Proofs. Courier Corporation.

.

Hao Wang, 1997. A Logical Journey: From Gödel to Philosophy. MIT Press.

模板:MR

Francesco Berto. There's Something about Gödel: The Complete Guide to the Incompleteness Theorem John Wiley and Sons. 2010.
Norbert Domeisen, 1990. Logik der Antinomien. Bern: Peter Lang. 142 S. 1990. . .
Torkel Franzén, 2005. Gödel's Theorem: An Incomplete Guide to its Use and Abuse. A.K. Peters.
Douglas Hofstadter, 1979. Gödel, Escher, Bach: An Eternal Golden Braid. Vintage Books. . 1999 reprint: .
—, 2007. I Am a Strange Loop. Basic Books. . .
Stanley Jaki, OSB, 2005. The drama of the quantities. Real View Books.
Per Lindström, 1997. Aspects of Incompleteness, Lecture Notes in Logic v. 10.
J.R. Lucas, FBA, 1970. The Freedom of the Will. Clarendon Press, Oxford, 1970.
Ernest Nagel, James Roy Newman, Douglas Hofstadter, 2002 (1958). Gödel's Proof, revised ed. .
Rudy Rucker, 1995 (1982). Infinity and the Mind: The Science and Philosophy of the Infinite. Princeton Univ. Press.
Peter Smith, 2007. An Introduction to Gödel's Theorems. Cambridge University Press.
N. Shankar, 1994. Metamathematics, Machines and Gödel's Proof, Volume 38 of Cambridge tracts in theoretical computer science.
Raymond Smullyan, 1987. Forever Undecided - puzzles based on undecidability in formal systems
—, 1991. Godel's Incompleteness Theorems. Oxford Univ. Press.
—, 1994. Diagonalization and Self-Reference. Oxford Univ. Press.
—, 2013. The Godelian Puzzle Book: Puzzles, Paradoxes and Proofs. Courier Corporation. .
Hao Wang, 1997. A Logical Journey: From Gödel to Philosophy. MIT Press.

= = = 关于定理的书籍 = =

弗朗西斯科 · 贝托。关于哥德尔的一些事: 约翰 · 威利和儿子们的不完全性定理完全指南。2010.
诺伯特 · 多梅森，1990。反律法学家。伯尔尼: 彼得 · 朗。142 s. 1990. ..
Torkel Franzén, 2005.哥德尔定理: 使用和滥用的不完整指南。A.k.彼得斯。
侯世达，1979年。哥德尔，埃舍尔，巴赫: 永恒的黄金编织。古董书籍。.1999年再版:。
—, 2007.我是一个奇怪的圈。基础书籍。..
Stanley Jaki，OSB，2005.数量的戏剧性。实景图书。
Per Lindström, 1997.不完整性的几个方面，逻辑 v. 10课堂讲稿。
j.r 卢卡斯，FBA，1970。意志的自由。克拉伦登出版社，牛津，1970年。
Ernest Nagel，James Roy Newman，侯世达，2002(1958)。哥德尔的证明，修订版。.
Rudy Rucker，1995(1982).无限与心灵: 无限的科学与哲学。普林斯顿大学。新闻稿。
彼得 · 史密斯，2007年。哥德尔定理导论。剑桥大学出版社。
n. Shankar，1994.元数学，机器和哥德尔的证明，卷38在理论计算机科学的剑桥大道。雷蒙·史慕扬，1987年。永远悬而未决——基于正式系统中不可判定性的难题
ー，1991。哥德尔的不完备性定理。牛津大学。新闻稿。
—, 1994.对角化与自我参照。牛津大学。新闻稿。
—, 2013.《哥德利之谜》 : 谜题、悖论与证明。深圳市信利达科技有限公司。.
郝望，1997。逻辑之旅: 从哥德尔到哲学。麻省理工学院出版社。

Miscellaneous references

Francesco Berto, 2009, "The Gödel Paradox and Wittgenstein's Reasons" Philosophia Mathematica (III) 17.
Dawson, John W., Jr. (1996). Logical dilemmas: The life and work of Kurt Gödel. Taylor & Francis. ISBN 978-1-56881-025-6.
Dawson, John W., Jr. (1997). Logical dilemmas: The life and work of Kurt Gödel. Wellesley, Massachusetts: A. K. Peters. ISBN 978-1-56881-256-4. OCLC 36104240.

Rebecca Goldstein, 2005, Incompleteness: the Proof and Paradox of Kurt Gödel, W. W. Norton & Company.

Floyd, Juliet; Putnam, Hilary (2000). "A Note on Wittgenstein's "Notorious Paragraph" about the Godel Theorem". The Journal of Philosophy. JSTOR. 97 (11): 624–632. doi:10.2307/2678455. ISSN 0022-362X. JSTOR 2678455.

John Harrison, 2009, "Handbook of Practical Logic and Automated Reasoning", Cambridge University Press,

David Hilbert and Paul Bernays, Grundlagen der Mathematik, Springer-Verlag.

John Hopcroft and Jeffrey Ullman 1979, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley,

James P. Jones, "Undecidable Diophantine Equations", Bulletin of the American Mathematical Society, v. 3 n. 2, 1980, pp. 859–862.

Stephen Cole Kleene, 1967, Mathematical Logic. Reprinted by Dover, 2002.

Russell O'Connor, 2005, "Essential Incompleteness of Arithmetic Verified by Coq", Lecture Notes in Computer Science v. 3603, pp. 245–260.
Lawrence Paulson, 2013, "A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets", Review of Symbolic Logic, v. 7 n. 3, 484–498.
Graham Priest, 1984, "Logic of Paradox Revisited", Journal of Philosophical Logic, v. 13,` n. 2, pp. 153–179.
—, 2004, Wittgenstein's Remarks on Gödel's Theorem in Max Kölbel, ed., Wittgenstein's lasting significance, Psychology Press, pp. 207–227.

—, 2006, In Contradiction: A Study of the Transconsistent, Oxford University Press,

Hilary Putnam, 1960, Minds and Machines in Sidney Hook, ed., Dimensions of Mind: A Symposium. New York University Press. Reprinted in Anderson, A. R., ed., 1964. Minds and Machines. Prentice-Hall: 77.

Wolfgang Rautenberg, 2010, A Concise Introduction to Mathematical Logic, 3rd. ed., Springer,

Victor Rodych, 2003, "Misunderstanding Gödel: New Arguments about Wittgenstein and New Remarks by Wittgenstein", Dialectica v. 57 n. 3, pp. 279–313. doi:10.1111/j.1746-8361.2003.tb00272.x
Stewart Shapiro, 2002, "Incompleteness and Inconsistency", Mind, v. 111, pp 817–32. doi:10.1093/mind/111.444.817

Alan Sokal and Jean Bricmont, 1999, Fashionable Nonsense: Postmodern Intellectuals' Abuse of Science, Picador.

Joseph R. Shoenfield (1967), Mathematical Logic. Reprinted by A.K. Peters for the Association for Symbolic Logic, 2001.

Jeremy Stangroom and Ophelia Benson, Why Truth Matters, Continuum.

George Tourlakis, Lectures in Logic and Set Theory, Volume 1, Mathematical Logic, Cambridge University Press, 2003.

Avi Wigderson, 2010, "The Gödel Phenomena in Mathematics: A Modern View", in Kurt Gödel and the Foundations of Mathematics: Horizons of Truth, Cambridge University Press.

Hao Wang, 1996, A Logical Journey: From Gödel to Philosophy, The MIT Press, Cambridge MA,

.

Zach, Richard (2007). "Hilbert's Program Then and Now". In Jacquette, Dale. Philosophy of logic. Handbook of the Philosophy of Science. 5. Amsterdam: Elsevier. pp. 411–447. arXiv:math/0508572. doi:10.1016/b978-044451541-4/50014-2. ISBN 978-0-444-51541-4. OCLC 162131413. https://arxiv.org/abs/math/0508572.

Francesco Berto, 2009, "The Gödel Paradox and Wittgenstein's Reasons" Philosophia Mathematica (III) 17.
Rebecca Goldstein, 2005, Incompleteness: the Proof and Paradox of Kurt Gödel, W. W. Norton & Company.
John Harrison, 2009, "Handbook of Practical Logic and Automated Reasoning", Cambridge University Press,
David Hilbert and Paul Bernays, Grundlagen der Mathematik, Springer-Verlag.
John Hopcroft and Jeffrey Ullman 1979, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley,
James P. Jones, "Undecidable Diophantine Equations", Bulletin of the American Mathematical Society, v. 3 n. 2, 1980, pp. 859–862.
Stephen Cole Kleene, 1967, Mathematical Logic. Reprinted by Dover, 2002.
Russell O'Connor, 2005, "Essential Incompleteness of Arithmetic Verified by Coq", Lecture Notes in Computer Science v. 3603, pp. 245–260.
Lawrence Paulson, 2013, "A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets", Review of Symbolic Logic, v. 7 n. 3, 484–498.
Graham Priest, 1984, "Logic of Paradox Revisited", Journal of Philosophical Logic, v. 13,` n. 2, pp. 153–179.
—, 2004, Wittgenstein's Remarks on Gödel's Theorem in Max Kölbel, ed., Wittgenstein's lasting significance, Psychology Press, pp. 207–227.
—, 2006, In Contradiction: A Study of the Transconsistent, Oxford University Press,
Hilary Putnam, 1960, Minds and Machines in Sidney Hook, ed., Dimensions of Mind: A Symposium. New York University Press. Reprinted in Anderson, A. R., ed., 1964. Minds and Machines. Prentice-Hall: 77.
Wolfgang Rautenberg, 2010, A Concise Introduction to Mathematical Logic, 3rd. ed., Springer,
Victor Rodych, 2003, "Misunderstanding Gödel: New Arguments about Wittgenstein and New Remarks by Wittgenstein", Dialectica v. 57 n. 3, pp. 279–313.
Stewart Shapiro, 2002, "Incompleteness and Inconsistency", Mind, v. 111, pp 817–32.
Alan Sokal and Jean Bricmont, 1999, Fashionable Nonsense: Postmodern Intellectuals' Abuse of Science, Picador.
Joseph R. Shoenfield (1967), Mathematical Logic. Reprinted by A.K. Peters for the Association for Symbolic Logic, 2001.
Jeremy Stangroom and Ophelia Benson, Why Truth Matters, Continuum.
George Tourlakis, Lectures in Logic and Set Theory, Volume 1, Mathematical Logic, Cambridge University Press, 2003.
Avi Wigderson, 2010, "The Gödel Phenomena in Mathematics: A Modern View", in Kurt Gödel and the Foundations of Mathematics: Horizons of Truth, Cambridge University Press.
Hao Wang, 1996, A Logical Journey: From Gödel to Philosophy, The MIT Press, Cambridge MA, .

= = 各种参考文献 = =

弗朗西斯科 · 贝托，2009，“哥德尔悖论与维特根斯坦的理由”，数学哲学(III)17。2005，Incompleteness: the Proof and Paradox of Kurt g ö del，威廉·沃德尔·诺顿公司。
John Harrison，2009，《实用逻辑与自动推理手册》，剑桥大学出版社，
David Hilbert and Paul Bernays，Grundlagen der mathematica，Springer-Verlag。
John hopccroft and Jeffrey Ullman 1979，Introduction to Automata Theory，Languages，and calculation，Addison-Wesley，
James p. Jones，“ undecutable Diophantine Equations”，Bulletin of the American Mathematical Society，v. 3 n. 2,1980，P.。859–862.斯蒂芬·科尔·克莱尼，1967，Mathematical Logic。2002年，多佛再版。
Russell o’connor，2005，“ Essential Incompleteness of Arithmetic Verified by Coq”，Lecture Notes in Computer Science v. 3603，pp。245–260.
Lawrence Paulson，2013，“ a machine-assisted proof of Gödel’s incompletion theories for the theory of cheritally finite sets”，Review of Symbolic Logic，v. 7 n. 3,484-498。1984，“ Logic of Paradox Revisited”，Journal of Philosophical Logic，v. 13，‘ n. 2，pp。153–179.
ー，2004，维特根斯坦对哥德尔定理的评论，Max Kölbel，ed.Wittgenstein’s lasting significance，Psychology Press，pp。207–227.
ー2006年，《矛盾: 横贯性研究》，牛津大学出版社，
希拉里 · 普特南，1960，《悉尼 · 胡克的思想与机器》，e.d. ，《思想的维度: 研讨会》。纽约大学出版社。再版于安德森，公元前年，1964年。思想与机器。普伦蒂斯-霍尔: 77。2010，a Concise Introduction to Mathematical Logic，rd.“误解哥德尔: 关于维特根斯坦和维特根斯坦的新评论的新论点”，《辩证法》，57 n. 3，pp。279–313.
Stewart Shapiro，2002，“ Incompleteness and inconsistence”，Mind，v. 111，pp 817-32。时髦的胡说：后现代知识分子对科学的糟蹋: 后现代知识分子对科学的滥用，Picador。
Joseph r. Shoenfield (1967) ，《数理逻辑》。转载: a.k。符号逻辑协会的 Peters，2001年。
杰里米·斯唐鲁姆和 Ophelia Benson，Why Truth Matters，Continuum。《逻辑与集合论讲座》，第一卷，数理逻辑，剑桥大学出版社，2003年。
Avi Wigderson，2010，《数学中的哥德尔现象: 一个现代的观点》，库尔特哥德尔和数学基础: 真理的视野，剑桥大学出版社。
王，1996，《逻辑之旅: 从哥德尔到哲学》，麻省理工学院出版社，麻省剑桥出版社，年。

External links

模板:In Our Time
模板:SEP.
模板:SEP.
Paraconsistent Logic § Arithmetic and Gödel's Theorem entry in the Stanford Encyclopedia of Philosophy.
MacTutor biographies:
- Kurt Gödel.
- Gerhard Gentzen.
What is Mathematics:Gödel's Theorem and Around by Karlis Podnieks. An online free book.
World's shortest explanation of Gödel's theorem using a printing machine as an example.
October 2011 RadioLab episode about/including Gödel's Incompleteness theorem
模板:Springer
How Gödel's Proof Works by Natalie Wolchover, Quanta Magazine, July 14, 2020.
[1] and [2] Gödel's incompleteness theorems formalised in Isabelle/HOL

` 模板:Metalogic 模板:Mathematical logic

.
.
Paraconsistent Logic § Arithmetic and Gödel's Theorem entry in the Stanford Encyclopedia of Philosophy.
MacTutor biographies:
- Kurt Gödel.
- Gerhard Gentzen.
What is Mathematics:Gödel's Theorem and Around by Karlis Podnieks. An online free book.
World's shortest explanation of Gödel's theorem using a printing machine as an example.
October 2011 RadioLab episode about/including Gödel's Incompleteness theorem
How Gödel's Proof Works by Natalie Wolchover, Quanta Magazine, July 14, 2020.
and Gödel's incompleteness theorems formalised in Isabelle/HOL

`

= = 外部链接 =

。
.
次协调逻辑算术和哥德尔定理入围斯坦福大学哲学百科全书。科特 · 哥德尔传记。
Gerhard Gentzen.
什么是数学: 哥德尔定理及其周围作者: Karlis Podnieks。一本在线免费书籍。
以印刷机为例，解释哥德尔定理的最短篇幅。
2011年10月 RadioLab 插曲: 关于/包括哥德尔的不完全性定理
哥德尔的证明是如何工作的 Natalie Wolchover，Quanta 杂志，2020年7月14日。
和哥德尔的不完备性定理在 Isabelle/HOL 中形式化

Category:Theorems in the foundations of mathematics Category:Mathematical logic Category:Model theory Category:Proof theory Category:Epistemology Category:Metatheorems Incompleteness theorems

范畴: 数学基础范畴中的定理: 数理逻辑范畴: 模型理论范畴: 证明理论范畴: 认识论范畴: 元定理不完备性定理

This page was moved from wikipedia:en:Gödel's incompleteness theorems. Its edit history can be viewed at 哥德尔不完备定理/edithistory

[1] Shelah, Saharon (1974). "Infinite Abelian groups, Whitehead problem and some constructions". Israel Journal of Mathematics. 18 (3): 243–256. doi:10.1007/BF02757281. MR 0357114.

[StrangeLoop-2] 2.0 ^2.1 Hofstadter, Douglas R. (2007). "Chapter 12. On Downward Causality". I Am a Strange Loop. ISBN 978-0-465-03078-1. https://publicism.info/philosophy/strange/14.html.

[1]

[2]

哥德尔不完备定理

Formal systems: completeness, consistency, and effective axiomatization

Effective axiomatization

Effective axiomatization

= = 有效公理化 =

Completeness

Completeness

= 完整性 =

Consistency

Systems which contain arithmetic

Systems which contain arithmetic

= = 包含算术的系统 = =

Conflicting goals

First incompleteness theorem

Syntactic form of the Gödel sentence

Syntactic form of the Gödel sentence

= = 哥德尔句子的句法形式 =

Truth of the Gödel sentence

Truth of the Gödel sentence

= = 哥德尔句子的真理 =

Relationship with the liar paradox

Relationship with the liar paradox

= 与说谎者悖论的关系 =

Extensions of Gödel's original result

Extensions of Gödel's original result

= = 哥德尔原始结果的扩展 = =

Second incompleteness theorem

Second incompleteness theorem

= 第二个不完备性定理 =

Expressing consistency

Expressing consistency

= = 表达一致性 =

The Hilbert–Bernays conditions

The Hilbert–Bernays conditions

= 希尔伯特-伯奈斯条件 =

Implications for consistency proofs

Implications for consistency proofs

= = 影响一致性证明 = =

Examples of undecidable statements

Undecidable statements provable in larger systems

Undecidable statements provable in larger systems

= = = 在大系统中可证明的无法判定的命题 = =

Relationship with computability

Proof sketch for the first theorem

Arithmetization of syntax

Arithmetization of syntax

= = 语法的算术化 = =

Construction of a statement about "provability"

Construction of a statement about "provability"

= = 构造一个关于“可证明性”的陈述 =

Diagonalization

Diagonalization

= 对角化 =

Proof via Berry's paradox

Computer verified proofs

Proof sketch for the second theorem

Discussion and implications

Consequences for logicism and Hilbert's second problem

Consequences for logicism and Hilbert's second problem

= = 对逻辑主义和希尔伯特的第二个问题的后果 =

Minds and machines

Paraconsistent logic

Paraconsistent logic

= 次协调逻辑 =

Appeals to the incompleteness theorems in other fields

Appeals to the incompleteness theorems in other fields

= = 引用其他领域的不完备性定理 = =

History

Announcement

Generalization and acceptance

Generalization and acceptance

= = 归纳和接受 = =

Criticisms

Criticisms

= = 批评 =

Finsler

Zermelo

Wittgenstein

See also

References