哥德尔的不完备性定理（On Formally Undecidable Propositions of Principia Mathematica and Related Systems I）与图灵的图灵机（On Computable Numbers, with an Application to the Entscheidungsproblem），都是源于解决希尔伯特提出的Entscheidungsproblem（判定问题）。

Brian Jack Copeland (1950-) 在“The EssentialTuring”书中收集了图灵的重要著作，同时作了相应的引读。以下是引读“Computable Numbers: A Guide”中关于Entscheidungsproblem（判定问题）的译文（p.45-53)。

一，译文

14，Entscheidungsproblem（判定问题）

在《论可计算数》第11章中，图灵转向了Entscheidungsproblem，或判定问题。Church给Entscheidungsproblem下了如下定义：

这里所说的符号逻辑系统的Entscheidungsproblem，是指找到一种有效的方法，通过这种方法，给定该系统符号中的任何表达式Q，可以确定Q在该系统中是否可以证明。（By the Entscheidungsproblem of a system of symbolic logic is here understood the problem to find an effective method by which, given any expression Q in the notation of the system, it can be determined whether or not Q is provable in the system.）

判定问题被德国数学家大卫-希尔伯特（David Hilbert）带到了数学的前沿（他在1900年巴黎的一次演讲中为20世纪的数学制定了议程）。1928年，希尔伯特将判定问题描述为“数理逻辑的主要问题”，说 “发现一般的判定程序是一个非常困难的问题，至今尚未解决”，而且“判定问题的解决具有根本的重要性”。

希尔伯特方案

希尔伯特和他的追随者认为，数学家应该寻求以完整的、一致的、可判定的形式系统来表达数学，这个系统以统一的方式表达“数学的全部思想内容”。 希尔伯特把这样一个系统比喻为“一个仲裁法庭，一个判定基本问题的最高法庭—在一个每个人都能同意的具体基础上，每一个陈述都能被控制”。正如希尔伯特在他的巴黎演讲中所宣称的： “在数学中没有无知”（没有我们不知道）。

重要的是，表达 "数学的全部思想内容 « 的系统必须是一致的。一个不一致的系统--包含矛盾的系统--是没有价值的，因为任何陈述，不管是真的还是假的，都可以通过简单的逻辑步骤从一个矛盾中得出，所以在一个不一致的系统中，诸如0=1和6⁄=6这样的荒谬是可以证明的。一个不一致的系统确实会包含所有真实的数学陈述--换句话说，会是完备的--但同时也会包含所有错误的数学陈述!

希尔伯特要求表达整个数学内容的系统是可判定的：必须有一种系统的方法来告诉每个数学陈述，在该系统中是否可以证明。如果这个系统要把无知完全从数学中驱逐出去，那么它必须是可解的。只有这样，我们才有信心始终能够知道任何给定的陈述是否可以证明。一个不可判定的系统有时可能会让我们处于无知状态。

以完备、一致、可解的形式系统来表达数学的项目被称为“证明理论”和 “希尔伯特方案”。1928年，希尔伯特在意大利博洛尼亚市的一次演讲中说：

- 在过去几年的一系列演讲中，我……开始采用一种处理基本问题的新方法。有了这种新的数学基础，人们可以方便地称之为证明理论，我相信数学中的基本问题最终会被消除，因为它使每一个数学陈述都成为可具体证明和严格推导的公式…。（In a series of presentations in the course of the last years I have . . . embarked upon a new way of dealing with fundamental questions. With this new foundation of mathematics, which one can conveniently call proof theory, I believe the fundamental questions in mathematics are finally eliminated, by making every mathematical statement a concretely demonstrable and strictly derivable formula . . .）

- 在数学中没有无知者，相反，我们总是能够回答有意义的问题；而且，正如亚里士多德也许预料到的那样，我们的理性不涉及任何形式的神秘艺术：相反，它是根据完全确定的可制定的规则进行的，而且也是其判断的绝对客观性的保证。（[I]n mathematics there is no ignorabimus, rather we are always able to answer meaningful questions; and it is established, as Aristotle perhaps anticipated, that our reason involves no mysterious arts of any kind: rather it proceeds according to formulable rules that are completely definite—and are as well the guarantee of the absolute objectivity of its judgement.）

然而，对希尔伯特计划来说，很快就会发现，大多数有趣的数学系统如果是一致的，则是不完备的和不可解的。

1931年，哥德尔表明，即使在简单的算术情况下，希尔伯特的理想也不可能得到实现。他证明，怀特海和罗素在其开创性的《数学原理》中提出的形式算术系统，如果是一致的，则是不完备的。也就是说：如果该系统是一致的，那么有一些算术的真陈述在该系统中是无法证明的—形式系统未能抓住算术的“整个思想内容”。这被称为哥德尔的第一个不完全性定理。

哥德尔后来概括了这一结果，指出“由于A.M.图灵的工作，现在可以给形式系统的一般概念下一个精确和毫无疑问的充分定义”，其结果是不完备性，可以“为每一个包含一定数量的有限数论的一致形式系统严格地证明”。 图灵的工作所带来的定义是这样的（用哥德尔的话说）：“形式系统可以简单地定义为产生公式的任何机械程序，称为可证明公式（A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas.） ”

在他的不完备性定理中，哥德尔表明，无论数学家如何努力构建希尔伯特所设想的包罗万象的形式系统，他们的劳动成果如果是一致的，就不可避免地是不完备的。正如Hermann Weyl—希尔伯特最优秀的学生所言，这对希尔伯特计划来说无异于“一场灾难”。

可判定性

哥德尔定理留下了可解性的开放问题，正如纽曼（Newman ）所总结的那样：

在20世纪20年代和30年代，希尔伯特判定计划的目标是发现一个判定真假的一般过程......。哥德尔的不完全性定理（1931 年）对找到这块新的哲学家之石的前景进行了第一次打击，该定理清楚地表明，在任何有限的逻辑中，A的真假不能一劳永逸等同于A或非A的可证明性（truth or falsehood of A could not be equated to provability of A or not-A in any finitely based logic, chosen once for all）；但原则上仍有可能找到一个机械过程来判定A 或非A 或两者在特定系统中是否可以形式证明。

图灵和丘奇分别独立地从正面解决了可判定性的问题。

在《论可计算数》的第84页，图灵通过一个初步的方式指出了一个希尔伯特主义者似乎忽略了的事实：如果一个系统是完备的，那么它也是可解的。希尔伯特的亲密合作者伯纳斯曾说过：“人们注意到，对演绎完备性的要求并不像对可解性的要求那样远。”图灵在第84页的简单论证表明，伯纳斯所声称的区别在概念上是没有空间的。

尽管如此，关键问题仍未解决：鉴于事实上简单算术是（如果一致的话）不完备的，那么它是或不是可解的？图灵和丘奇都表明，没有一个一致的正式算术系统是可解的。他们通过证明连函数计算—任何形式化算术系统所预设的较弱的纯逻辑系统--都不是可解的。希尔伯特式的完全机械化数学的梦想现在完全破灭了。

一阶谓词系统简介

图灵所称的函数计算（functional calculus）（丘奇继希尔伯特之后，称之为engere Funktionenkalku¨l），今天被称为一阶谓词计算（FOPC）。FOPC是演绎逻辑推理的一种形式化。

有各种不同但等价的方法来表述FOPC，有一种提法将FOPC表述为由大约十几条正式的推理规则组成（这种表达比图灵在第84页提到的希尔伯特-阿克曼表达更容易理解，是由Gerhard Gentzen提出的）。

。。。

许多数学和科学都可以在FOPC的框架内形式化。例如，一个正式的算术系统可以通过在FOPC中加入一些算术公理来构建。这些公理由非常基本的算术语句组成，例如：

(x)(x + 0 = x) (x)

and

(y)(Sx = Sy → x = y) 

其中’S’意味着“后继者”—1的后继者是2，以此类推。(在这些公理中，变量'x'和'y'的范围被限制为数字）。通过FOPC的规则，可以从这些公理推导出其他算术语句。例如，规则（v）告诉我们，语句：

1+0 = 1

可以从上述第一条公理中得出结论。

如果FOPC是不可判定的，那么就可以得出算术是不可判定的。事实上，如果

FOPC是不可解的，那么许多重要的数学系统也是不可解的。为了找到可解的逻辑，我们必须在那些在某种意义上比FOPC弱的系统中寻找。可解逻辑的一个例子是，如果所有的量词规则—如(iv)和(v)的规则—都从FOPC中删除，就会产生一个系统，这个系统被称为命题演算。

FOPC不可判定性的证明

图灵和丘奇表明，没有一种系统的方法，在给定FOPC符号中的任何公式Q时，可以确定Q在系统中是否可以证明（即是否'Q'）。换句话说，丘奇和图灵表明，在FOPC的情况下，Entscheidungsproblem是不可解的。

丘奇对不可解性的证明是通过他的λ计算和他的理论进行的，即每个有效的方法都有一个λ-definable函数。人们普遍认为图灵的观点是正确的，如上文所述（第45页），他自己证明不可解性的方法比丘奇的方法“更有说服力”。

图灵的方法利用了他关于没有计算机可以解决打印问题的证明。他表明，如果一个图灵机可以告诉任何给定的语句，该语句在FOPC中是否可被证明，那么一个图灵机可以告诉任何给定的图灵机，它是否曾经打印出'0'。正如他已经确定的那样，没有图灵机可以做后者，因此，没有图灵机可以做前者。论证的最后一步是应用图灵的论点：如果没有图灵机可以解决所说的任务，那么就没有系统的方法来解决它。

详细来说，图灵的证明包含以下步骤：

1. 图灵证明了如何为任何计算机m构造一个复杂的FOPC语句，即“在某一点上，机器m打印出0”。他称这个公式为’Un(m)'。(字母'Un'可能来自'undecidable'或德语中的'unentscheidbare')。

2. 图灵证明了以下情况：

1. 如果Un(m)在FOPC中是可证明的，那么在某一点上，m会打印0。

2. 如果在某一点上m打印为0，那么Un(m)在FOPC中是可证明的。

3. 想象一个计算机器，当给定FOPC符号中的任何语句Q时，它能够（在某些有限的步骤中）确定Q是否可以在FOPC中被证明。我们把这种机器称为希尔伯特之梦。2(a)和2(b)告诉我们，希尔伯特之梦会解决打印问题。因为如果机器表明Un(m)是可证明的，那么，鉴于2(a)，它实际上是表明m确实打印了0；而如果机器表明Un(m)这个陈述是不可证明的，那么，鉴于2(b)，它实际上是表明m没有打印0。没有任何一台计算机能够在某些有限的步骤中确定每个语句Q是否可以在FOPC中被证明。

4. 如果有一种系统的方法，在给定任何语句Q的情况下，可以确定Q是否可以在FOPC中被证明，那么，根据图灵的论述，就会得出这样一种计算机器，即希尔伯特的梦。因此不存在这样的系统方法。

不可解性的意义

尽管对希尔伯特学派来说， Entscheidungsproblem的不可解性是个坏消息，但在其他方面却是个非常受欢迎的消息，原因是希尔伯特的杰出学生冯-诺伊曼在1927年就提出了一个理由：

如果不判定性失败了，那么今天意义上的数学将不复存在；它的位置将被一个完全机械的规则所取代，借助于这个规则，任何一个人都能够判定任何给定的陈述，该陈述是否可以被证明。

正如剑桥大学数学家G.H.Hardy在1928年的一次演讲中所说，。。。如果有一套解决所有数学问题的机械规则。。。我们作为数学家的活动就会结束。

参考资料：

The Essential Turing: Seminal Writings in Computing, Logic, Philosophy, Artificial Intelligence, and Artificial Life:

Plus The Secrets of Enigma, B. Jack Copeland, Editor （p.45-53)

http://www.cse.chalmers.se/~aikmitr/papers/Turing.pdf

二，原文

14. The Entscheidungsproblem

In Section 11 of ‘On Computable Numbers’, Turing turns to the Entscheidungsproblem, or decision problem. Church gave the following definition of the Entscheidungsproblem:

By the Entscheidungsproblem of a system of symbolic logic is here understood the problem to find an effective method by which, given any expression Q in the notation of the system, it can be determined whether or not Q is provable in the system.

The decision problem was brought to the fore of mathematics by the German mathematician David Hilbert (who in a lecture given in Paris in 1900 set the agenda for much of twentieth-century mathematics). In 1928 Hilbert described the decision problem as ‘the main problem of mathematical logic’, saying that ‘the discovery of a general decision procedure is a very difficult problem which is as yet unsolved’, and that the ‘solution of the decision problem is of fundamental importance’.

The Hilbert programme

Hilbert and his followers held that mathematicians should seek to express mathematics in the form of a complete, consistent, decidable formal system—a system expressing ‘the whole thought content of mathematics in a uniform way’. Hilbert drew an analogy between such a system and ‘a court of arbitration, a supreme tribunal to decide fundamental questions—on a concrete basis on which everyone can agree and where every statement can be controlled’.81 Such a system would banish ignorance from mathematics: given any mathematical statement, one would be able to tell whether the statement is true or false by determining whether or not it is provable in the system. As Hilbert famously declared in his Paris lecture: ‘in mathematics there is no ignorabimus’ (there is no we shall not know)

It is important that the system expressing the ‘whole thought content of mathematics’ be consistent. An inconsistent system—a system containing contradictions—is worthless, since any statement whatsoever, true or false, can be derived from a contradiction by simple logical steps. So in an inconsistent system, absurdities such as 0 = 1 and 6 ⁄= 6 are provable. An inconsistent system would indeed contain all true mathematical statements—would be complete, in other words—but would in addition also contain all false mathematical statements!

Hilbert’s requirement that the system expressing the whole content of mathematics be decidable amounts to this: there must be a systematic method for telling, of each mathematical statement, whether or not the statement is provable in the system. If the system is to banish ignorance totally from mathematics then it must be decidable. Only then could we be confident of always being able to tell whether or not any given statement is provable. An undecidable system might sometimes leave us in ignorance.

The project of expressing mathematics in the form of a complete, consistent, decidable formal system became known as ‘proof theory’ and as the ‘Hilbert programme’. In 1928, in a lecture delivered in the Italian city of Bologna, Hilbert said:

In a series of presentations in the course of the last years I have . . . embarked upon a new way of dealing with fundamental questions. With this new foundation of mathematics, which one can conveniently call proof theory, I believe the fundamental questions in mathematics are finally eliminated, by making every mathematical statement a concretely demonstrable and strictly derivable formula . . .

[I]n mathematics there is no ignorabimus, rather we are always able to answer meaningful questions; and it is established, as Aristotle perhaps anticipated, that our reason involves no mysterious arts of any kind: rather it proceeds according to formulable rules that are completely definite—and are as well the guarantee of the absolute objectivity of its judgement.

Unfortunately for the Hilbert programme, however, it was soon to become clear that most interesting mathematical systems are, if consistent, incomplete and undecidable.

In 1931, Go¨del showed that Hilbert’s ideal is impossible to satisfy, even in the case of simple arithmetic. He proved that the formal system of arithmetic set out by Whitehead and Russell in their seminal Principia Mathematica is, if consistent, incomplete. That is to say: if the system is consistent, there are true statements of arithmetic that are not provable in the system—the formal system fails to capture the ‘whole thought content’ of arithmetic. This is known as Go¨del’s first incompleteness theorem.

Go¨del later generalized this result, pointing out that ‘due to A. M. Turing’s work, a precise and unquestionably adequate definition of the general concept of formal system can now be given’, with the consequence that incompleteness can ‘be proved rigorously for every consistent formal system containing a certain amount of finitary number theory’.87 The definition made possible by Turing’s work is this (in Go¨del’s words): ‘A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas.’

In his incompleteness theorem, Go¨del had shown that no matter how hard mathematicians might try to construct the all-encompassing formal system envisaged by Hilbert, the product of their labours would, if consistent, inevitably be incomplete. As Hermann Weyl—one of Hilbert’s greatest pupils— observed, this was nothing less than ‘a catastrophe’ for the Hilbert programme.

Decidability

Go¨del’s theorem left the question of decidability open. As Newman summarized matters:

The Hilbert decision-programme of the 1920’s and 30’s had for its objective the discovery of a general process . . . for deciding . . . truth or falsehood . . . A first blow was dealt at the prospects of finding this new philosopher’s stone by Go¨del’s incompleteness theorem (1931), which made it clear that truth or falsehood of A could not be equated to provability of A or not-A in any finitely based logic, chosen once for all; but there still remained in principle the possibility of finding a mechanical process for deciding whether A, or not-A, or neither, was formally provable in a given system.

The question of decidability was tackled head on by Turing and, independently, by Church.

On p. 84 of ‘On Computable Numbers’ Turing pointed out—by way of a preliminary—a fact that Hilbertians appear to have overlooked: if a system is complete then it follows that it is also decidable. Bernays, Hilbert’s close collaborator, had said: ‘One observes that [the] requirement of deductive completeness does not go as far as the requirement of decidability.’91 Turing’s simple argument on p. 84 shows that there is no conceptual room for the distinction that Bernays is claiming.

Nevertheless, the crucial question was still open: given that in fact simple arithmetic is (if consistent) incomplete, is it or is it not decidable? Turing and Church both showed that no consistent formal system of arithmetic is decidable. They showed this by proving that not even the functional calculus—the weaker, purely logical system presupposed by any formal system of arithmetic—is decidable. The Hilbertian dream of a completely mechanized mathematics now lay in total ruin.

A tutorial on first-order predicate calculus

What Turing called the functional calculus (and Church, following Hilbert, the engere Funktionenkalku¨l) is today known as frist-order predicate calculus (FOPC). FOPC is a formalization of deductive logical reasoning.

There are various different but equivalent ways of formulating FOPC. One formulation presents FOPC as consisting of about a dozen formal rules of inference. (This formulation, which is more accessible than the Hilbert–Ackermann formulation mentioned by Turing on p. 84, is due to Gerhard Gentzen.)

。。。

Much of mathematics and science can be formulated within the framework of FOPC. For example, a formal system of arithmetic can be constructed by adding a number of arithmetical axioms to FOPC. The axioms consist of very basic arithmetical statements, such as:

(x)(x + 0 = x) (x)

and

(y)(Sx = Sy → x = y) 

where ‘S’ means ‘the successor of’—the successor of 1 is 2, and so on. (In these axioms the range of the variables ‘x’ and ‘y’ is restricted to numbers.) Other arithmetical statements can be derived from these axioms by means of the rules of FOPC. For example, rule (v) tells us that the statement

1+0 = 1

can be concluded from the first of the above axioms.

If FOPC is undecidable then it follows that arithmetic is undecidable. Indeed, if FOPC is undecidable, then so are very many important mathematical systems. To find decidable logics one must search among systems that are in a certain sense weaker than FOPC. One example of a decidable logic is the system that results if all the quantifier rules—rules such as (iv) and (v)—are elided from FOPC. This system is known as the propositional calculus.

The proof of the undecidability of FOPC

Turing and Church showed that there is no systematic method by which, given any formula Q in the notation of FOPC, it can be determined whether or not Q is provable in the system (i.e. whether or not ‘ Q). To put this another way, Church and Turing showed that the Entscheidungsproblem is unsolvable in the case of FOPC.

Both published this result in 1936. Church’s demonstration of undecidability proceeded via his lambda calculus and his thesis that to each effective method there corresponds a lambda-definable function. There is general agreement that Turing was correct in his view, mentioned above (p. 45), that his own way of showing undecidability is ‘more convincing’ than Church’s.

Turing’s method makes use of his proof that no computing machine can solve the printing problem. He showed that if a Turing machine could tell, of any given statement, whether or not the statement is provable in FOPC, then a Turing machine could tell, of any given Turing machine, whether or not it ever prints ‘0’. Since, as he had already established, no Turing machine can do the latter, it follows that no Turing machine can do the former. The final step of the argument is to apply Turing’s thesis: if no Turing machine can perform the task in question, then there is no systematic method for performing it.

In detail, Turing’s demonstration contains the following steps.

1. Turing shows how to construct, for any computing machine m, a complicated statement of FOPC that says ‘at some point, machine m prints 0’. He calls this formula ‘Un(m)’. (The letters ‘Un’ probably come from ‘undecidable’ or the German equivalent ‘unentscheidbare’.)

2. Turing proves the following ：

1. If Un(m) is provable in FOPC, then at some point m prints 0. (b) If at some point m prints 0, then Un(m) is provable in FOPC.

2. If at some point m prints 0, then Un(m) is provable in FOPC.

3. Imagine a computing machine which, when given any statement Q in the notation of FOPC, is able to determine (in some finite number of steps) whether or not Q is provable in FOPC. Let’s call this machine hilbert’s dream. 2(a) and 2(b) tell us that hilbert’s dream would solve the printing problem. Because if the machine were to indicate that Un(m) is provable then, in view of 2(a), it would in effect be indicating that m does print 0; and if the machine were to indicate that the statement Un(m) is not provable then, in view of 2(b), it would in effect be indicating that m does not print 0. Since no computing machine can solve the printing problem, it follows that hilbert’s dream is a figment. No computing machine is able to determine in some finite number of steps, of each statement Q, whether or not Q is provable in FOPC.

4. If there were a systematic method by which, given any statement Q, it can be determined whether or not Q is provable in FOPC, then it would follow, by Turing’s thesis, that there is such a computing machine as hilbert’s dream. Therefore there is no such systematic method.

The significance of undecidability

Poor news though the unsolvability of the Entscheidungsproblem was for the Hilbert school, it was very welcome news in other quarters, for a reason that Hilbert’s illustrious pupil von Neumann had given in 1927:

If undecidability were to fail then mathematics, in today’s sense, would cease to exist; its place would be taken by a completely mechanical rule, with the aid of which any man would be able to decide, of any given statement, whether the statement can be proven or not.

As the Cambridge mathematician G. H. Hardy said in a lecture in 1928: ‘if there were...a mechanical set of rules for the solution of all mathematical problems . . . our activities as mathematicians would come to an end.’