今天这段依然出自艾伦·图灵（Alan Turing）1936年发表的经典论文《论可计算数及其在判定问题上的应用》（Alan Turing, On Computable Numbers, with an Application to the Entscheidungsproblem, 1936），具体是文章的第十一章。

原文

11. Application to the Entscheidungsproblem

The results of §8 have some important applications. In particular, they can be used to show that the Hilbert Entscheidungsproblem can have no solution. For the present I shall confine myself to proving this particular theorem. For the formulation of this problem I must refer the reader to Hilbert and Ackermann's Grundzüge der Theoretischen Logik (Berlin, 1931), chapter 3.

I propose, therefore, to show that there can be no general process for determining whether a given formula $\mathfrak{U}$ of the functional calculus $\mathbf{K}$ is provable, i.e. that there can be no machine which, supplied with any one $\mathfrak{U}$ of these formulae, will eventually say whether $\mathfrak{U}$ is provable.

It should perhaps be remarked that what I shall prove is quite different from the well-known results of Gödel. Gödel has shown that (in the formalism of Principia Mathematica) there are propositions $\mathfrak{U}$ such that neither $\mathfrak{U}$ nor $-\mathfrak{U}$ is provable. As a consequence of this, it is shown that no proof of consistency of Principia Mathematica (or of $\mathbf{K}$) can be given within that formalism. On the other hand, I shall show that there is no general method which tells whether a given formula $\mathfrak{U}$ is provable in $\mathbf{K}$, or, what comes to the same, whether the system consisting of $\mathbf{K}$ with $-\mathfrak{U}$ adjoined as an extra axiom is consistent.

If the negation of what Gödel has shown had been proved, i.e. if, for each $\mathfrak{U}$, either $\mathfrak{U}$ or $-\mathfrak{U}$ is provable, then we should have an immediate solution of the Entscheidungsproblem. For we can invent a machine $\mathcal{K}$ which will prove consecutively all provable formulae. Sooner or later $\mathcal{K}$ will reach either $\mathfrak{U}$ or $-\mathfrak{U}$. If it reaches $\mathfrak{U}$, then we know that $\mathfrak{U}$ is provable. If it reaches $-\mathfrak{U}$, then, since $\mathbf{K}$ is consistent (Hilbert and Ackermann, p. 65), we know that $\mathfrak{U}$ is not provable.

Owing to the absence of integers in $\mathbf{K}$ the proofs appear somewhat lengthy. The underlying ideas are quite straightforward. Corresponding to each computing machine $\mathcal{M}$ we construct a formula Un($\mathcal{M}$) and we show that, if there is a general method for determining whether Un($\mathcal{M}$) is provable, then there is a general method for determining whether $\mathcal{M}$ ever prints 0.

The interpretations of the propositional functions involved are as follows: $R_{S_l}(x, y)$ is to be interpreted as "in the complete configuration $x$ (of $\mathcal{M}$) the symbol on the square $y$ is $S_l$". $I(x, y)$ is to be interpreted as "in the complete configuration $x$ the square $y$ is scanned". $K_{q_m}(x)$ is to be interpreted as "in the complete configuration $x$ the m-configuration is $q_m$". $F(x, y)$ is to be interpreted as "$y$ is the immediate successor of $x$".

$Inst { q_i S_j S_k L q_l }$ is to be an abbreviation for $(x, y, x', y') { ( R_{S_j}(x, y) \& I(x, y) \& K_{q_i}(x) \& F(x, x') \& F(y', y) ) \rightarrow ( I(x', y') \& R_{S_k}(x', y) \& K_{q_l}(x') \& (z) [ F(y', z) \vee (R_{S_j}(x, z) \rightarrow R_{S_k}(x', z)) ] ) }$

$Inst { q_i S_j S_k R q_l }$ and $Inst { q_i S_j S_k N q_l }$ are to be abbreviations for other similarly constructed expressions.

Let us put the description of $\mathcal{M}$ into the first standard form of §6. This description consists of a number of expressions such as "$q_i S_j S_k L q_l$" (or with $R$ or $N$ substituted for $L$). Let us form all the corresponding expressions such as $Inst { q_i S_j S_k L q_l }$ and take their logical sum. This we call Des($\mathcal{M}$).

The formula Un($\mathcal{M}$) is to be $(Es)[ N(s) \& (x)( N(x) \rightarrow (Es') F(x, s') ) \& (y, z)( F(y, z) \rightarrow N(y) \& N(z) ) \& (y) R_{S_0}(s, y) \& I(s, u) \& K_{q_1}(s) \& \text{Des}(\mathcal{M}) ] \rightarrow (Es)(Et)[ N(s) \& N(t) \& R_{S_1}(s, t) ]$

$[N(x) \& \dots \& \text{Des}(\mathcal{M})]$ may be abbreviated to $A(\mathcal{M})$.

[When we substitute the meanings suggested on p. 259–60 we find that Un($\mathcal{M}$) has the interpretation "in some complete configuration of $\mathcal{M}$, $S_1$ appears on the tape". Corresponding to this I prove that

(i) If $S_1$ appears on the tape in some complete configuration of $\mathcal{M}$, then Un($\mathcal{M}$) is provable.

(ii) If Un($\mathcal{M}$) is provable, then $S_1$ appears on the tape in some complete configuration of $\mathcal{M}$.

When this has been done, the remainder of the theorem is trivial.]

Lemma 1. If $S_1$ appears on the tape in some complete configuration of $\mathcal{M}$, then Un($\mathcal{M}$) is provable.

We have to show how to prove Un($\mathcal{M}$). Let us suppose that in the n-th complete configuration the sequence of symbols on the tape is $S_{r_0}, S_{r_1}, ...., S_{r_n}$, followed by blanks, and that the scanned symbol is the $l$-th, and that the m-configuration is $q_k$. Then we may form the proposition $$R_{S_{r_0}}(u^{(0)}, u) \& R_{S_{r_1}}(u^{(0)}, u') \& ... \& R_{S_{r_n}}(u^{(0)}, u^{(n)})$$ $$\& I(u^{(0)}, u^{(l)}) \& K_{q_k}(u^{(0)}) \& (y) [ F(y, u) \lor F(y, u') \lor ... \lor F(y, u^{(n)}) \lor R_{S_0}(u^{(0)}, y) ]$$ which we may abbreviate to $CC_n$.

As before, $F(u, y) \& F(y, u') \& ... \& F(u^{(n-1)}, u^{(n)})$ is abbreviated to $F^{(n)}$.

I shall show that all formulae of the form $A(\mathcal{M}) \& F^{(n)} \to CC_n$ (abbreviated to $CF_n$) are provable. The meaning of $CF_n$ is "The n-th complete configuration of $\mathcal{M}$ is so and so", where "so and so" stands for the actual n-th complete configuration of $\mathcal{M}$. That $CF_n$ should be provable is therefore to be expected.

$CF_0$ is certainly provable, for in the complete configuration the symbols are all blanks, the m-configuration is $q_1$, and the scanned square is $u$, i.e. $CC_0$ is $$R_{S_0}(u^{(0)}, u) \& I(u^{(0)}, u) \& K_{q_1}(u^{(0)}) \& (y) R_{S_0}(u^{(0)}, y)$$

$A(\mathcal{M}) \to CC_0$ is then trivial.

We next show that $CF_n \to CF_{n+1}$ is provable for each $n$. There are three cases to consider, according as in the move from the n-th to the $(n+1)$-th configuration the machine moves to left or to right or remains stationary. We suppose that the first case applies, i.e. the machine moves to the left. A similar argument applies in the other cases.

If $r(l, n) = i$, $r(l+1, n) = a$, $k(n) = m$, and $\delta(m, i) = q_k S_k L q_l$, then Des($\mathcal{M}$) must include $Inst{q_m S_i S_k L q_l}$ as one of its terms, i.e. $$\text{Des}(\mathcal{M}) \to Inst{q_m S_i S_k L q_l}$$

Hence $$A(\mathcal{M}) \& F^{(n+1)} \to Inst{q_m S_i S_k L q_l} \& F(u^{(l)}, u^{(l+1)}) \& CC_n$$

and $$(A(\mathcal{M}) \& F^{(n+1)} \& CC_n) \to CC_{n+1}$$

i.e. $$CF_n \to CF_{n+1}$$

$CF_n$ is provable for each $n$. Now it is the assumption of this lemma that $S_1$ appears somewhere, in some complete configuration, in the sequence of symbols printed by $\mathcal{M}$; that is, for some integers $N, K$, $CC_N$ has $R_{S_1}(u^{(N)}, u^{(K)})$ as one of its terms, and therefore $CC_N \to R_{S_1}(u^{(N)}, u^{(K)})$ is provable. We have then $$A(\mathcal{M}) \& F^{(N+K)} \to CC_N$$ and $$A(\mathcal{M}) \& F^{(N+K)} \to R_{S_1}(u^{(N)}, u^{(K)})$$ and $$(\exists u) A(\mathcal{M}) \to (\exists u)(\exists u') ... (\exists u^{(N+K)}) (A(\mathcal{M}) \& F^{(N+K)})$$ where $N' = \max(N, K)$. And so $$(\exists u) A(\mathcal{M}) \to (\exists u)(\exists u') ... (\exists u^{(N')}) R_{S_1}(u^{(N)}, u^{(K)})$$ i.e. Un($\mathcal{M}$) is provable.

Lemma 2. If Un($\mathcal{M}$) is provable, then $S_1$ appears on the tape in some complete configuration of $\mathcal{M}$.

If we substitute any propositional functions for function variables in a provable formula, we obtain a true formula. In particular, if we substitute the meanings tabulated above in Un($\mathcal{M}$), we obtain a true proposition with the meaning "$S_1$ appears on the tape in some complete configuration of $\mathcal{M}$".

We are now in a position to show that the Entscheidungsproblem cannot be solved. Let us suppose the contrary. Then there is a general (mechanical) process for determining whether Un($\mathcal{M}$) is provable. By Lemmas 1 and 2, this implies that there is a process for determining whether $\mathcal{M}$ ever prints 0, and this is impossible, by §8. Hence the Entscheidungsproblem cannot be solved.

In view of the large number of particular cases of solutions of the Entscheidungsproblem for formulae with restricted systems of quantors, it is interesting to express Un($\mathcal{M}$) in a form in which all quantors are at the beginning. Un($\mathcal{M}$) is, in fact, expressible in the form

$$ (u)(\exists x)(w)(\exists u_1)\ldots(\exists u_n)\mathfrak{B}, \tag{I} $$

where $\mathfrak{B}$ contains no quantors, and $n = 6$. By unimportant modifications we can obtain a formula, with all essential properties of Un($\mathcal{M}$), which is of form (I) with $n = 5$.

翻译

11. 判定问题的应用

第8节的结果有一些重要应用。尤其是，它们可以用来证明希尔伯特判定问题（Entscheidungsproblem）不可能有解。目前我只限于证明这个特定定理。关于该问题的表述，请读者参阅希尔伯特和阿克曼的《理论逻辑基础》（Grundzüge der Theoretischen Logik，柏林，1931年）第3章。

因此，本文要证明的是：不存在通用过程来判定谓词演算 $\mathbf{K}$ 中任意给定公式 $\mathfrak{U}$ 是否可证——换个说法就是，不存在一台机器，给它任意公式 $\mathfrak{U}$，它最终能判定 $\mathfrak{U}$ 是否可证。

需要特别指出的是，我将证明的结果与哥德尔的著名结论截然不同。哥德尔在《数学原理 Principia Mathematica》所构建的形式逻辑体系下证明了，存在命题 $\mathfrak{U}$，使得 $\mathfrak{U}$ 和 $-\mathfrak{U}$ 都不可证。由此可以推出，无法在该形式体系内给出《数学原理》（或 $\mathbf{K}$）的一致性证明。而我要证明的是：不存在通用方法，判定给定公式 $\mathfrak{U}$ 在 $\mathbf{K}$ 中是否可证——这个判定问题等价于判定由 $\mathbf{K}$ 加上 $-\mathfrak{U}$ 作为额外公理所构成的系统是否一致。

如果哥德尔所证结论的反面成立——即对每个 $\mathfrak{U}$，$\mathfrak{U}$ 或 $-\mathfrak{U}$ ，两者至少有一个可证——那么判定问题立即有解。因为我们可以设计一台机器 $\mathcal{K}$，按顺序证明所有可证公式。迟早 $\mathcal{K}$ 会得到 $\mathfrak{U}$ 或 $-\mathfrak{U}$。如果得到 $\mathfrak{U}$，则 $\mathfrak{U}$ 可证；如果得到 $-\mathfrak{U}$，由于 $\mathbf{K}$ 是一致的（见希尔伯特和阿克曼，第65页），则 $\mathfrak{U}$ 不可证。

由于 $\mathbf{K}$ 中没有整数，证明显得有些冗长，但基本思想非常直接。对应于每台计算机器 $\mathcal{M}$，我们构造一个公式 Un($\mathcal{M}$)，并证明：如果存在通用方法判定 Un($\mathcal{M}$) 是否可证，那么就存在通用方法判定 $\mathcal{M}$ 是否会打印0。

相关命题函数的解释如下： $R_{S_l}(x, y)$ 意为“在 $\mathcal{M}$ 的完整构型 $x$ 中，方格 $y$ 上的符号是 $S_l$”。 $I(x, y)$ 意为“在完整构型 $x$ 中，方格 $y$ 正被扫描”。 $K_{q_m}(x)$ 意为“在完整构型 $x$ 中，m-构型是 $q_m$”。 $F(x, y)$ 意为“$y$ 是 $x$ 的直接后继”。

$Inst { q_i S_j S_k L q_l }$ 是以下表达式的缩写： $(x, y, x', y') { ( R_{S_j}(x, y) \& I(x, y) \& K_{q_i}(x) \& F(x, x') \& F(y', y) ) \rightarrow ( I(x', y') \& R_{S_k}(x', y) \& K_{q_l}(x') \& (z) [ F(y', z) \vee (R_{S_j}(x, z) \rightarrow R_{S_k}(x', z)) ] ) }$

$Inst { q_i S_j S_k R q_l }$ 和 $Inst { q_i S_j S_k N q_l }$ 是类似构造的表达式的缩写。

将 $\mathcal{M}$ 的描述写成第6节的第一种标准形式。该描述由若干形如“$q_i S_j S_k L q_l$”（或将 $L$ 换成 $R$ 或 $N$）的表达式组成。构造所有对应的表达式如 $Inst { q_i S_j S_k L q_l }$，取它们的逻辑和，称为 Des($\mathcal{M}$)。

公式 Un($\mathcal{M}$) 定义为： $(Es)[ N(s) \& (x)( N(x) \rightarrow (Es') F(x, s') ) \& (y, z)( F(y, z) \rightarrow N(y) \& N(z) ) \& (y) R_{S_0}(s, y) \& I(s, u) \& K_{q_1}(s) \& \text{Des}(\mathcal{M}) ] \rightarrow (Es)(Et)[ N(s) \& N(t) \& R_{S_1}(s, t) ]$

$[N(x) \& \dots \& \text{Des}(\mathcal{M})]$ 可缩写为 $A(\mathcal{M})$。

代入前文建议的含义，我们发现 Un($\mathcal{M}$) 的解释是“在 $\mathcal{M}$ 的某个完整构型中，$S_1$ 出现在纸带上”。相应地，可以证明

(i) 若 $S_1$ 出现在 $\mathcal{M}$ 的某个完整构型的纸带上，则 Un($\mathcal{M}$) 可证。

(ii) 若 Un($\mathcal{M}$) 可证，则 $S_1$ 出现在 $\mathcal{M}$ 的某个完整构型的纸带上。

上面这部分等到证明后，定理其余部分即显然。

引理 1. 若 $S_1$ 出现在 $\mathcal{M}$ 的某个完整构型的纸带上，则 Un($\mathcal{M}$) 可证。

我们需展示如何证明 Un($\mathcal{M}$)。设第 n 个完整构型中，纸带上的符号序列为 $S_{r_0}, S_{r_1}, ...., S_{r_n}$，其后为空白，被扫描的是第 $l$ 个符号，m-构型为 $q_k$。则可形成命题

$$R_{S_{r_0}}(u^{(0)}, u) \& R_{S_{r_1}}(u^{(0)}, u') \& ... \& R_{S_{r_n}}(u^{(0)}, u^{(n)})$$

$$\& I(u^{(0)}, u^{(l)}) \& K_{q_k}(u^{(0)}) \& (y) [ F(y, u) \lor F(y, u') \lor ... \lor F(y, u^{(n)}) \lor R_{S_0}(u^{(0)}, y) ]$$

将其缩写为 $CC_n$。

如前，$F(u, y) \& F(y, u') \& ... \& F(u^{(n-1)}, u^{(n)})$ 缩写为 $F^{(n)}$。

我将证明所有形如 $A(\mathcal{M}) \& F^{(n)} \to CC_n$（缩写为 $CF_n$）的公式均可证。$CF_n$ 意为“$\mathcal{M}$ 的第 n 个完整构型如此这般”，其中“如此这般”指 $\mathcal{M}$ 的实际第 n 个完整构型。故 $CF_n$ 应可证。

$CF_0$ 显然可证，因初始完整构型中所有符号皆为空白，m-构型为 $q_1$，扫描方格为 $u$，即 $CC_0$ 为 $$R_{S_0}(u^{(0)}, u) \& I(u^{(0)}, u) \& K_{q_1}(u^{(0)}) \& (y) R_{S_0}(u^{(0)}, y)$$

于是 $A(\mathcal{M}) \to CC_0$ 显然成立。

下一步证明对每个 $n$，$CF_n \to CF_{n+1}$ 可证。需考虑三种情形：从第 n 个到第 $(n+1)$ 个构型，机器左移、右移或静止。设第一种情形成立，即机器左移。其余情形论证类似。

若 $r(l, n) = i$，$r(l+1, n) = a$，$k(n) = m$，且 $\delta(m, i) = q_k S_k L q_l$，则 Des($\mathcal{M}$) 必含 $Inst{q_m S_i S_k L q_l}$ 作为一项，即 $$\text{Des}(\mathcal{M}) \to Inst{q_m S_i S_k L q_l}$$

故 $$A(\mathcal{M}) \& F^{(n+1)} \to Inst{q_m S_i S_k L q_l} \& F(u^{(l)}, u^{(l+1)}) \& CC_n$$

且 $$(A(\mathcal{M}) \& F^{(n+1)} \& CC_n) \to CC_{n+1}$$

即 $$CF_n \to CF_{n+1}$$

故对每个 $n$，$CF_n$ 均可证。现据引理假设，$S_1$ 在某个完整构型中出现在 $\mathcal{M}$ 打印的符号序列中；即存在整数 $N, K$，使 $CC_N$ 含 $R_{S_1}(u^{(N)}, u^{(K)})$ 作为一项，故 $CC_N \to R_{S_1}(u^{(N)}, u^{(K)})$ 可证。于是 $$A(\mathcal{M}) \& F^{(N+K)} \to CC_N$$ 且 $$A(\mathcal{M}) \& F^{(N+K)} \to R_{S_1}(u^{(N)}, u^{(K)})$$ 且 $$(\exists u) A(\mathcal{M}) \to (\exists u)(\exists u') ... (\exists u^{(N+K)}) (A(\mathcal{M}) \& F^{(N+K)})$$ 其中 $N' = \max(N, K)$。故 $$(\exists u) A(\mathcal{M}) \to (\exists u)(\exists u') ... (\exists u^{(N')}) R_{S_1}(u^{(N)}, u^{(K)})$$ 即 Un($\mathcal{M}$) 可证。

引理 2. 若 Un($\mathcal{M}$) 可证，则 $S_1$ 出现在 $\mathcal{M}$ 的某个完整构型的纸带上。

若将可证公式中的函数变量代以任意命题函数，所得公式为真。特别地，将上述列表中的含义代入 Un($\mathcal{M}$)，所得真命题意为“$S_1$ 在 $\mathcal{M}$ 的某个完整构型中出现在纸带上”。

现在可以证明判定问题不可解。假设相反，则存在通用（机械）过程判定 Un($\mathcal{M}$) 是否可证。据引理1和2，这意味着存在过程判定 $\mathcal{M}$ 是否会打印0，而据第8节，此为不可能。故判定问题不可解。

在对于量词系统受限的公式方面，判定问题已有大量特例场景得到了解决，将 Un($\mathcal{M}$) 表达成所有量词置于开头的形式是有意义的。实际上，可以将 Un($\mathcal{M}$) 表达成下面的形式：

$$ (u)(\exists x)(w)(\exists u_1)\ldots(\exists u_n)\mathfrak{B}, \tag{I} $$

其中 $\mathfrak{B}$ 不含量词，且 $n = 6$。通过一些非本质性的修改，可以得到一个具有 Un($\mathcal{M}$) 全部本质特征的公式，其形式为 (I) 且 $n = 5$。

逐段解析

判定问题的来龙去脉

要理解图灵这篇文章的历史意义，必须回到二十世纪初数学界的一场宏大梦想。

十九世纪末，数学经历了一场深刻的基础危机。集合论悖论、非欧几何的发现、分析学的严格化，都迫使数学家们重新审视数学的根基。德国数学家大卫·希尔伯特提出了一个雄心勃勃的计划：将全部数学建立在一套完备、一致的公理系统之上。所谓完备，是指任何数学命题，在这个系统里要么能被证明为真，要么能被证明为假；所谓一致，是指这个系统不会自相矛盾，不会同时证明一个命题既真又假。

希尔伯特计划的核心是判定问题（德语叫 Entscheidungsproblem，英语叫 Decision Problem）。这个问题问的是：是否存在一种机械的、有限步骤的方法，能够判定任意数学命题的真假？换句话说，能否造出一台"数学真理机器"，输入任意命题，输出"可证"或"不可证"？

如果答案是肯定的，数学将变成一项完全机械化的事业。数学家不再需要灵感、直觉、创造力，只需要按部就班地运行算法即可。这在当时的许多人看来并非天方夜谭——毕竟，代数方程有求根公式，几何证明有作图法，为什么整个数学不能有一套通用的判定程序呢？

然而，这个梦想在1930年代被彻底了否定。

哥德尔的工作

1931年，年仅25岁的奥地利逻辑学家库尔特·哥德尔发表了两条不完备性定理，震惊了整个数学界。

第一不完备性定理说：在任何足够强的一致形式系统中，必然存在一些命题，它们是真的，但在这个系统内无法被证明。哥德尔的证明极其巧妙——他构造了一个自指的命题，大意是"本命题在系统中不可证"。如果这个命题可证，系统就矛盾了；如果不可证，那它说的就是真话，但真话却无法被证明。这揭示了形式系统的内在局限：完备性与一致性不可兼得。

第二不完备性定理更加致命：任何足够强的一致形式系统，都无法在内部证明自身的一致性。这直接宣判了希尔伯特计划的核心目标无法实现——你永远不能用数学自己证明数学没有矛盾。

哥德尔的工作告诉我们：存在特定的命题，系统对它无能为力。

但注意，这并不直接回答判定问题。

哥德尔证明的是「存在不可判定的命题」，但这些命题是特别构造出来的，也许普通的数学命题仍然可以被判定？换句话说，也许存在某种更聪明的方法，虽然不能判定所有命题，但能判定我们关心的绝大多数命题？

图灵的工作正是要证明：连这种希望也是虚幻的。

一致性与可证性的关系

在图灵的论述中，有一个关键逻辑需要解释清楚。他说：判定一个公式是否可证，等价于判定一个新系统是否一致。这到底是怎么回事？

首先，什么叫「一致」？一个形式系统是「一致的」，就是它不会自相矛盾——不会同时证明某个命题和它的否定。举个例子，如果系统能够证明「所有天鹅都是白的」，又能够证明「存在一只黑天鹅」，那这两个结论就冲突了，系统就不一致了。一致的系统只说真话，不会自己打自己的脸。

现在来看图灵说的等价关系。给定一个公式𝔘，我们问：𝔘在系统K中是否可证？这个问题可以转化成另一个问题：如果把-𝔘（即𝔘的否定）作为一条新公理加入K，得到的新系统是否一致？

为什么这两个问题等价？推理如下。

第一种情况：假设𝔘在K中可证。这意味着K里面已经有𝔘的证明了。现在我们把-𝔘加进去作为公理，新系统里就同时存在两样东西：一是𝔘的证明（从原来的K继承来的），二是-𝔘作为公理（直接假定它成立）。一个命题和它的否定同时被系统接受，系统就自相矛盾了。所以：𝔘可证，则新系统不一致。

第二种情况：假设𝔘在K中不可证。这意味着K里面没有𝔘的证明。现在把-𝔘加进去作为公理。由于K本身是一致的（不会同时证明𝔘和-𝔘），而𝔘又不可证，所以K和-𝔘之间不会产生冲突。新系统依然一致。所以：𝔘不可证，则新系统一致。

把这两种情况合起来：𝔘可证当且仅当新系统不一致。两边取个否定，就得到：𝔘不可证当且仅当新系统一致。这就是图灵所说的等价关系。

还有一个相关的问题：为什么如果𝔘或-𝔘有一个可证，另一个就一定不可证？这背后的原理是系统的一致性。假设𝔘可证，又假设-𝔘也可证，那么系统同时证明了𝔘和-𝔘，这意味着系统自相矛盾。但K是一个一致的系统，它不会自相矛盾。所以如果𝔘可证，-𝔘一定不可证；反过来，如果-𝔘可证，𝔘一定不可证。两者不可能同时可证。

但是，两者能不能同时不可证呢？这正是哥德尔发现的情况！在某些系统中，存在这样的𝔘，使得𝔘和-𝔘都不可证。这种命题叫「不可判定命题」——系统既不能证明它对，也不能证明它错。哥德尔构造出了这种命题，从而打破了「完备性」的幻想。

逻辑系统K与编码方案

图灵的证明中涉及一个叫K的逻辑系统，还有一些命题函数。这些都是什么？为什么它们能把图灵机的行为翻译成逻辑公式？

首先，K是什么？K是一个「谓词演算」系统，也叫「一阶逻辑」。它是现代逻辑学的基础形式系统，包含命题连接词（如「并且」「或者」「并非」「如果...那么...」）、量词（「所有」「存在」）以及谓词和个体变量。你可以把它理解成一个形式化的推理框架，规定了什么样的推理是合法的。希尔伯特和阿克曼在他们的书中详细描述了这个系统。

为什么图灵说「K中没有整数」？这是一个关键的技术细节。在一阶逻辑的标准表述中，自然数并不是内置的原始对象。你无法直接说「x是一个自然数」，也无法直接进行算术运算。K只提供抽象的个体变量和谓词，不预设任何特定的数学结构。这和皮亚诺算术或《数学原理》的系统不同——后两者明确包含自然数和算术公理。

正因如此，图灵必须「从零开始」构造出一套语言来描述图灵机。他不能直接说「第n个时刻」或「第k个方格」，而必须用谓词和量词间接地表达这些概念。这就是为什么证明显得「有些冗长」——他要用纯逻辑的语言重建整套计算框架。

那么，图灵是如何把图灵机翻译成逻辑公式的？核心思想是用四类谓词来刻画机器在任意时刻的完整状态。

第一类谓词描述「纸带内容」。它表达的是：在某个时刻，某个方格上写的是什么符号。这就像给纸带拍一张快照，记录每个位置的字符。

第二类谓词描述「读写头位置」。它表达的是：在某个时刻，读写头正停在哪个方格上。这告诉我们机器「正在看哪里」。

第三类谓词描述「机器的内部状态」。它表达的是：在某个时刻，机器处于哪个状态。图灵机有多种状态，不同状态下机器的行为不同，这个谓词就是为了标记当前状态。

第四类谓词描述「时刻的先后顺序」。它表达的是：某个时刻是另一个时刻的直接后继，即紧挨着的下一时刻。这建立了时间的链条，让我们能说「这一步之后是那一步」。

有了这四类基本词汇，每一条机器指令就可以翻译成一个逻辑公式。比如，一条指令说：「如果在状态A扫描到符号B，就打印符号C，左移，进入状态D。」翻译成逻辑语言，大意就是：如果在某个时刻机器处于状态A且扫描符号B，那么在下一时刻，原来的符号B位置变成了符号C，读写头左移了一格，机器状态变成了D。这就是一个「如果...那么...」形式的蕴涵式。

把所有指令对应的蕴涵式合并起来，就得到机器的「完整描述」——一个刻画机器全部行为规则的大公式。最后，图灵定义了一个核心公式Un($\mathcal{M}$)，它的意思是：「如果机器M从空白纸带开始运行，那么在某个时刻，纸带上会出现某个特定符号。」这个特定符号就是图灵用来标记「打印了0」的记号。

现在关键问题来了：为什么「判定Un($\mathcal{M}$)是否可证」等价于「判定M是否会打印0」？

这涉及到两个方向的推理。第一个方向：如果机器确实打印了那个符号，为什么Un($\mathcal{M}$)可证？答案在于，打印符号是一个有限过程——机器运行了有限步之后，在某个方格上写下了这个符号。既然是有限步，每一步的状态转移都可以被逻辑公式精确描述。把这些描述串起来，就像记录一段旅程的每一步脚印，最终构成一个完整的证明链。

第二个方向：如果Un($\mathcal{M}$)可证，为什么机器确实会打印那个符号？这依赖于逻辑系统的「可靠性」——一个可靠的系统不会证明假命题。如果Un($\mathcal{M}$)说「机器会打印这个符号」而且它被证明了，那么机器就真的会打印。证明不会凭空产生，它必须基于公理和推理规则，而这些公理和规则正确地反映了机器的行为逻辑。

两个方向合起来，就建立了等价关系：问机器会不会打印符号，等价于问Un($\mathcal{M}$)能不能被证明。这个等价关系是图灵整个证明的枢纽——它把一个关于计算的问题，转化成了一个关于逻辑证明的问题。

图灵的贡献

图灵1936年的贡献比哥德尔更加彻底。他证明的是：不存在任何通用的机械方法，能够判定任意命题是否可证。注意措辞的区别——哥德尔说"存在特定的例外"，图灵说"整个任务本身就不可能完成"。

打个比方：哥德尔指出有些案件永远审不完；图灵指出根本不可能建造一个能审理所有案件的万能法庭。前者是局部问题，后者是根本限制。

图灵还特别指出了他的结果与哥德尔的关系。如果哥德尔的结论反过来成立——即每个命题要么可证，要么其否定可证——那么判定问题反而有解了。因为我们可以设计一台机器，按顺序枚举所有可能的证明，迟早会碰到目标命题或其否定的证明。但哥德尔已经证明这种完备性不成立，所以枚举法注定失败。然而，枚举法的失败并不意味着判定问题必然无解——也许存在某种不依赖枚举的巧妙方法？图灵的工作正是要堵死这条路。

归约证明的逻辑

图灵采用的是「归约法」——这是不可解性证明中的经典策略。其核心思想是：把一个已知的不可解问题，转化为待证明的问题。如果转化成功，那么待证明的问题也不可能解决——否则我们就可以用后者来解决前者，产生矛盾。

图灵的证明可以分解为四个步骤，每一步都清晰可验证。

第一步：找一个已知的不可解问题。

第8节已经证明了一个关键结果：不存在通用方法判定任意图灵机是否会打印符号0。这个问题的不可解性，与著名的「停机问题」本质相同。停机问题问的是：给定任意程序和输入，能否判定程序最终会停止还是永远运行下去？答案是：不可能。这个结论直观上可以理解——程序的行为千变万化，我们无法预见所有可能性。

现在，图灵手上有了一个「锚点」：打印0的问题是不可解的。

第二步：把图灵机编码为逻辑公式。

这是整个证明中最精巧的部分。图灵设计了一套系统化的编码方案，把任意一台图灵机的结构和行为，完整地翻译成一阶逻辑公式。具体来说，他用四类谓词来刻画机器的完整构型：

• $R_{S_l}(x, y)$ 表示「在时刻 $x$，方格 $y$ 上的符号是 $S_l$」——这刻画了纸带内容。
• $I(x, y)$ 表示「在时刻 $x$，读写头正扫描方格 $y$」——这刻画了读写头位置。
• $K_{q_m}(x)$ 表示「在时刻 $x$，机器处于状态 $q_m$」——这刻画了机器的内部状态。
• $F(x, y)$ 表示「$y$ 是 $x$ 的直接后继」——这刻画了时刻的先后顺序。

有了这些基本词汇，每一条机器指令都可以翻译成一个逻辑蕴涵式。例如，指令「若在状态 $q_i$ 扫描到符号 $S_j$，则打印 $S_k$，左移，转入状态 $q_l$」就翻译成 $Inst{q_i S_j S_k L q_l}$，它表达的是：如果在某时刻机器处于状态 $q_i$ 且扫描符号 $S_j$，那么下一时刻纸带、读写头和状态会如何变化。

把所有指令对应的公式合取起来，就得到机器的完整描述 Des($\mathcal{M}$)。最后，图灵定义了一个核心公式 Un($\mathcal{M}$)，它的直观含义是：「如果机器 $\mathcal{M}$ 从空白纸带开始运行，那么在某个时刻，纸带上会出现符号 $S_1$」。这里 $S_1$ 就是图灵用作标记的那个符号（在第8节中，他用的是打印0来标记）。为了证明判定问题不可解，这里的「打印0」和「打印 $S_1$」是等价的设定。

第三步：建立等价关系。

这是整个证明的核心。图灵证明了两个引理，建立起「机器行为」与「公式可证性」之间的精确对应。这两个引理分别处理两个方向，合起来就建立了完整的等价关系。

引理一：如果机器确实在运行过程中打印了符号S1，那么公式Un($\mathcal{M}$)可证。

为什么这个方向成立？关键在于：打印符号是一个有限过程。

想象一下，机器从空白纸带开始，一步一步运行。每一步，它根据当前状态和扫描到的符号，决定打印什么、移动方向、转入什么状态。假设机器在第N步打印了S1。那么从第0步到第N步，机器一共走了N+1个完整构型——每个构型都完整记录了纸带内容、读写头位置和机器状态。

图灵的编码方案正是为这每一拍「快照」服务的。对于第k个构型，逻辑公式可以精确描述：此时纸带上每个方格是什么符号、读写头在哪个位置、机器处于什么状态。更重要的是，从第k个构型到第k+1个构型的转移，也可以被一条「如果...那么...」的蕴涵式刻画——这条蕴涵式正是机器指令的翻译。

现在，把所有这些刻画串起来：初始构型的描述、每一步转移的蕴涵式、最终构型中S1出现在纸带上的事实。这就构成了一条完整的推理链——从「机器开始运行」推出「机器打印了S1」。这条推理链，就是Un($\mathcal{M}$)的证明。

所以，只要机器确实打印了S1，就一定能在逻辑系统里构造出Un($\mathcal{M}$)的证明。这不是魔法，而是因为机器的每一步操作都可以被逻辑语言忠实记录。

引理二：如果公式Un($\mathcal{M}$)可证，那么机器确实会打印符号S1。

这个方向涉及逻辑系统的一个根本性质：可靠性。

什么叫可靠性？一个逻辑系统是「可靠的」，意思是：如果某个公式在这个系统里可证，那么这个公式陈述的内容就是真的。可靠系统不会证明假命题——它不会凭空捏造不存在的事实。

为什么K系统是可靠的？因为它的推理规则都是保真的。比如，从「A并且B」推出「A」，这个推理规则永远不会把真命题变成假命题。从「如果A那么B」和「A」推出「B」，这个规则也是保真的。K系统的每一条推理规则都经过严格审视，确保不会引入错误。

现在，Un($\mathcal{M}$)说的是什么？它说的是「如果机器M从空白纸带开始运行，那么在某个时刻，纸带上会出现S1」。如果Un($\mathcal{M}$)可证，而K又是可靠的，那么Un($\mathcal{M}$)陈述的内容就必须是真的。换句话说，机器M从空白纸带开始运行后，真的会在某时刻打印S1。

这里有一个微妙之处：Un($\mathcal{M}$)的证明依赖于机器描述Des(M)作为「前提」。Des(M)是机器所有指令的逻辑翻译，它正确地反映了机器的行为规则。所以，基于Des(M)推出的结论，必然符合机器的真实行为。

两个引理合起来的威力。

引理一说：打印S1 → Un($\mathcal{M}$)可证。 引理二说：Un($\mathcal{M}$)可证 → 打印S1。

两个方向合起来，就是完整的等价关系：机器是否打印S1，当且仅当Un($\mathcal{M}$)是否可证。

这个等价关系意味着什么？它意味着「机器行为问题」和「逻辑可证问题」本质上是同一个问题，只是换了两套语言来描述。问「机器会不会打印S1」，等价于问「Un($\mathcal{M}$)能不能被证明」。这就把一个关于计算的问题，完美转化成了一个关于逻辑的问题。

第四步：反证完成。

现在万事俱备。假设判定问题有解，即存在通用算法能判定任意公式是否可证。我们来推导矛盾：

取任意图灵机 $\mathcal{M}$，用第二步的方法构造公式 Un($\mathcal{M}$)。然后用判定算法检验 Un($\mathcal{M}$) 是否可证。根据第三步的等价关系，检验结果直接告诉我们 $\mathcal{M}$ 是否会打印 $S_1$。

但这意味着我们找到了判定「机器是否打印 $S_1$」的通用方法——而第8节已经证明，这种方法不可能存在。矛盾。

因此，假设错误。判定问题无解。

这就是图灵证明的完整逻辑链条。四个步骤环环相扣：从已知的不可解问题出发，构造编码方案，建立等价关系，最后反证收尾。整个过程干净利落，展示了图灵深邃的洞察力——他看到了「计算」与「证明」之间的内在联系，并用这种联系证明了逻辑学的根本界限。

本章总结：图灵证明判定问题不可解，终结了希尔伯特的机械化数学之梦。其核心创新在于将图灵机行为编码为逻辑公式，建立计算与证明的等价桥梁，揭示了算法能力的根本边界。