Propositional Logic（PL）的有效性（Validity）是可判定的，这意味着存在一个算法，给定任意一个PL中的语句，回答该语句是否是有效的，也就是所有的该语句在所有的truth assignment下都为真。这个算法很简单，只需要粗暴地对每一个proposition尝试不同的真值组合即可。（题外话：虽然提到的这个PL和有效性问题相关的另一个问题：可满足性问题（又叫SAT问题）是一个NP完全问题，也就是说它的解的正确性可以在多项式时间内被验证，但是目前还没有发现多项式时间内的算法——“NP完全”意味着NP复杂度类中的所有问题至多和SAT问题一样复杂，也就是NP类中的所有问题都可以被reduce到SAT问题，这意味着你如果能找到一个适用于SAT问题的多项式时间算法，那么你就解决了P=NP问题）。当这个问题被扩展到一阶逻辑中时被称为判定问题（Decision Problem/Entscheidungsproblem），它最早在Hilbert's Program中被提出——当时的希尔伯特认为数学是完备，自洽，且可判定的，其中的可判定指的就是判定问题，在论文On Computable Numbers, With an Application to the Entscheidungsproblem（中文一般译作《论可计算数及其在判定问题中的应用》）中，图灵证明了判定问题的答案是否。在讨论这个问题之前，需要先明确一下有效性和可满足性的区别：

1. 可满足性指的是一个是否存在一个结构 \mathfrak{M} 使得对于语句 \varphi 有 \mathfrak{M}\vDash \varphi
2. 有效性指的是是否对于所有的结构 \mathfrak{M}，都有 \mathfrak{M}\vDash \varphi，写作 \vDash \varphi

因此，FOL的有效性问题就是指是否存在一个图灵机，初始状态输入是任意一个一阶逻辑的语句 \varphi，判定 \vDash \varphi。这个问题的答案是否定的，也即不存在这样的图灵机，在证明之前，我们首先给出图灵机的定义：

图灵机
一个图灵机是一个四元组\langle Q,\Sigma, q_0, \delta\rangle，其中包含:

1. 一个有限的状态集合 Q
2. 一个字母表，包含 \rhd 与 0 ，其中 \rhd 用来指示图灵机纸带的左侧边界，0 指代空符号，在机器开始运行前，读写头将位于 \rhd 右侧一格的位置，同时我们假设 \rhd 永远不能被覆写
3. 初始状态 q_0\in Q
4. 状态转移函数 \delta: Q\times\Sigma \rightharpoonup Q\times\Sigma\times\lbrace L,R,N\rbrace。其中 \delta(q_i, \sigma_i)=\langle q_j,\sigma_j, R\rangle 意味着图灵机在 q_i 状态读到字符 \sigma_i 时，状态转移到 q_j，将字符替换为 \sigma_j，读写头往右侧移动一格，如果是 L 则向左移动，N 则不移动

接着，我们会将停机问题reduce到该问题来对其进行证明，也就是假设存在一个能够判定FOL的有效性的Oracle Machine O，那么就可以利用这个O来解决停机问题。既然停机问题是不可判定的，那么该问题也同样是不可判定的。这意味着我们需要构造一个语句 \tau(M,w) 来表达“输入为 w 的图灵机 M”，用另一个语句 \alpha(M,w) 表示“输入为 w 的图灵机 M 会停机”；此时，“输入为 w 的图灵机 M 会停机”就可以被表示为 \vDash \tau(M,w)\rightarrow \alpha(M,w)。这样，O 就能够判定这个语句，从而判定停机问题，也就是说，我们成功地将停机问题reduce到了FOL的有效性问题。
  下一步，我们需要构造这样的一个能够用来表示 “输入为 w 的图灵机 M ”的语句 \tau(M,w)，这个语句应当能够完整的描述一个图灵机的所有属性，也就是图灵机的初始状态，状态转移函数 \delta 中所有的状态转移，以及足够完备的自然数公理用于描述图灵机执行的步骤和当前读取的方格数。这可以通过构造一个描述图灵机 M 的一阶理论实现。

描述图灵机 M 的语言 \mathcal{L}_M
给定一个图灵机 M=\langle Q, \Sigma, q_0, \delta \rangle，我们可以构造一个用来描述该图灵机的一阶语言 \mathcal{L_M}，包含:

1. 对每一个状态 q\in Q，一个二元谓词 Q_q(x, y) 代表“在运行 y 步后，图灵机 m 位于状态 q，正在读取第 x 格”
2. 对字母表中的每一个符号 \sigma \in \Sigma，一个二元谓词 S_\sigma(x, y) 代表“在运行 y 步后，纸带的第 x 个方格上的字符是 \sigma ”
3. 一个常量符号 \sf o 代表自然数 0
4. 一个一元函数 ' 代表后继函数，例如 \mathsf{o'} = \overline{1}，在这里，为了方便起见，我们用 \overline{0} 代表 \sf o，\overline{1} 代表 \sf o'，\overline{2} 代表 \sf o''，\overline{n+1}=\overline{n}' 以此类推
5. 一个二元谓词 \lt，用于表示自然数之间的大小关系

在定义该理论的语言后，我们需要定义之前提到的三条以及自然数相关的公理：

描述自然数的公理

1. 用于描述每个自然数都小于其后继的公理
   \forall x. x< x' \tag{AN-Succ}
2. 用于描述 < 的传递性的公理
   \forall x.\forall y.\forall z. (x < y\land y < z\rightarrow x < z) \tag{AN-Trans}

描述图灵机初始状态的公理

1. 描述初始状态的公理：在机器开始运行前，也即第0步时，M 位于初始状态 q_0，正在读取第1个方格
   Q_{q_0}(\overline{1}, \overline{0})\tag{AT-Init}
2. 描述图灵机输入的公理：在机器开始运行前，纸带的前k+1个方格包含符号\rhd,\sigma_1,\sigma_2,...,\sigma_k，其中 \rhd 代表纸带左侧边界
   S_\rhd(\overline{0}, \overline{0})\land S_{\sigma_1}(\overline{1}, \overline{0})\land S_{\sigma_2}(\overline{2}, \overline{0})\land ... \land S_{\sigma_k}(\overline{k}, \overline{0}) \tag{AT-Input}
3. 描述初始状态时纸带的公理：在机器开始运行前，除了前 k+1 个方格外，纸带上的剩余方格都只包含空符号 0
   \forall x. (\overline{k} < x \rightarrow S_0(x, \overline{0}))\tag{AT-Tape}

描述图灵机状态转移的公理
由于图灵机一次至多修改一个方格，因此在描述图灵机的状态转移时，首先我们需要一个语句来描述“除了第 x 格以外，其余所有方格在 y+1 步之后和第 y 步时保持一致”，令 \Phi(x, y) 为:

其含义为“除了第 x 格外，其余所有在第 y 步时包含字符 \sigma 的第 z 个方格，在第 y+1 步后依然包含字符 \sigma”

1. 描述图灵机状态转移的公理1：对于每个向右移动读写头的状态转移规则 \delta(q_i, \sigma_j)=\langle q_j, \sigma_j, R\rangle，有：
   \begin{aligned}
   &\forall x.\forall y.((Q_{q_i}(x,y)\land S_{\sigma_i}(x,y))\rightarrow \\ &\qquad(Q_{q_j}(x',y')\land S_{\sigma_j}(x,y')\land\Phi(x,y)))\tag{AT-TransR}
   \end{aligned}

   注意在该语句中，Q_{q_i}(x,y)\land S_{\sigma_i}(x,y) 代表“图灵机在第 y 步时位于状态 q_i 并且正在读取第 x 格的字符 \sigma_i”，而 Q_{q_j}(x',y')\land S_{\sigma_j}(x,y')\land\Phi(x,y) 代表“图灵机在第 y+1 步时位于状态 q_j，此时第 x 格的字符被读写头覆写成了 \sigma_j，且除了第 x 格以外的所有方格都保持和第 y 步时一样”，将这两句联系起来意味着 “如果图灵机在第 y 步时位于状态 q_i 并且正在读取第 x 格的字符 \sigma_i，那么在第 y+1 步时其位于状态 q_j，此时第 x 格的字符被读写头覆写成了 \sigma_j，且除了第 x 格以外的所有方格都保持和第 y 步时一样”，因此，该公理描述了一个将读写头向纸带右侧移动的状态转移规则。注意由于这样的状态转移规则可能有多个，所以上述的公理不止一条，而是对于每条这样的规则都有一份实例。同理，我们也需要另外两条公理分别对应读写头向左移动的规则以及读写头不移动的规则。

2. 描述图灵机状态转移的公理2：对于每个向左移动读写头的状态转移规则 \delta(q_i, \sigma_j)=\langle q_j, \sigma_j, L\rangle，有：

   \begin{aligned}
   &\forall x.\forall y.((Q_{q_i}(x',y)\land S_{\sigma_i}(x',y))\rightarrow \\ &\qquad(Q_{q_j}(x,y')\land S_{\sigma_j}(x',y')\land\Phi(x',y)))\ \land\\
   &\forall y.((Q_{q_i}(\mathsf{o}, y)\land S_{\sigma_i}(\mathsf{o}, y))\rightarrow \\&\qquad(Q_{q_j}(\mathsf{o}, y')\land S_{\sigma_j}(\mathsf{o}, y')\land\Phi(\mathsf{o}, y)) \tag{AT-TransL}
   \end{aligned}

   注意在该语句中，额外多了一条 \forall y.((Q_{q_i}(\mathsf{o}, y)\land S_{\sigma_i}(\mathsf{o}, y))\rightarrow (Q_{q_j}(\mathsf{o}, y')\land S_{\sigma_j}(\mathsf{o}, y')\land\Phi(\mathsf{o}, y))，其中 \sf o 代表纸带上的第一个方格，该语句声明如果在读写头读取纸带的最左侧方格时遇到了一个要求将读写头向左移动的状态转移规则，则应该忽视读写头的移动要求，将其保留在原地不动，而符号的替换和覆写则正常进行，同时除了 \sf o 外的所有方格照例保持不变。这相当于要求读写头不能够越界，也即超过最左侧的方块。

3. 描述图灵机状态转移的公理3：对于每个不移动读写头的状态转移规则 \delta(q_i, \sigma_j)=\langle q_j, \sigma_j, N\rangle，有：

   \begin{aligned}
   &\forall x.\forall y.((Q_{q_i}(x,y)\land S_{\sigma_i}(x,y))\rightarrow \\ &\qquad(Q_{q_j}(x,y')\land S_{\sigma_j}(x,y')\land\Phi(x,y)))\tag{AT-TransN}
   \end{aligned}

在完成对该理论的公理的定义后，我们就可以用这些公理来描述一个图灵机 M 了——包括 M 的初始状态和每条状态转移规则，令 \tau(M, w) 是上述所有公理的合取，可以被形象的理解为：

（注意其中 \text{AT-TransR}， \text{AT-TransL}，与 \text{AT-TransN} 实际上分别各是一组公理的集合）

通过以上的几条公理，我们已经能够成功的使用一阶语言描述任意图灵机。接着，我们还需要使用同样的一阶语言来描述任意图灵机 M 的停机，在某些图灵机的定义中，停机状态是被显示标注的，而在我们对图灵机的定义里则并没有，因此我们需要利用状态转移函数是偏函数的特性来实现这一点：如果图灵机抵达了停机状态，则此时状态转移函数是未定义的。令 X 是所有使得 \delta(q,\sigma) 是未定义的序偶 \langle q,\sigma\rangle 的集合，令：

则 \alpha(M,w) 就表示了 “存在 x, y，使得图灵机 M 在执行第 y 步时的状态是 q，并且正在读取第 x 个方格上的符号 \sigma，同时状态转移函数在 \delta(q,\sigma) 上未定义”。也就是说等价于表示了图灵机 M 已经运行至停机状态。

  至此，我们已经完整的给出了能够用来定义 \tau(M,w) 以及 \alpha(M,w) 的语言和理论，也就是说，我们有了使用一阶语言描述图灵机及其停机的能力。接下来，我们需要证明 \tau(M,w)\rightarrow\alpha(M,w) 这样一个语句对图灵机和其停机的描述的正确性，使该语句的有效性和图灵机 M 的停机吻合，也即

图灵机 M 停机当且仅当 \vDash \tau(M,w)\rightarrow\alpha(M,w)

  在证明之前，我们需要有一个办法来使用一阶语言描述在执行每一步时的图灵机，也就是任意时刻图灵机的格局（configuration），包含其状态，纸带上的信息以及读写头的位置。定义 \mathcal{X}(M,w,n) 为

其中 k 在 n=0 也就是第一步时代表的是纸带上最右侧的非空方格，而在 n\ne 0 时代表读写头曾经读写到的最右端（最远端）的方格，因此 k 右侧的所有方格都没有被读写过，因此都应该是空白字符 0。上面的语句中，Q_q(\overline{m}, \overline{n}) 代表图灵机此时在第 n 步，状态为 q，正在读取第 m 个方格。S_{\sigma_0}(\overline{0}, \overline{n})\land...\land S_{\sigma_k}(\overline{k},\overline{n}) 代表此时纸带上的内容，一直到读写头读写的最远端第 k 个方格为止。而 \forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}) 代表从第 k+1 个方格开始都没有被读写过，因此内容符号都是 0。注意虽然看上去这其中的 \overline{k} 和 \overline{m} 看上去像是未绑定的自由变量，但是他们其实不是自由变量，而是常量符号 \sf o 或者函数符号 \sf o'，\sf o''...等等，因此这依然是一个不包含自由变量的一阶语句。上述这几条合在一起，我们就有了一个能够描述每一步时图灵机的格局的语句。

引理1：如果 m\lt k，则 \tau(M,w)\vDash \overline{m}\lt \overline{k}

证明： 对 k-m 进行归纳：

1. 当 k-m=0 时，m \lt k 不成立，因此该引理hold vacuously
2. 当 k-m=n+1\ (n\ge 0) 时，有 k-(m+1)=n ，根据归纳假设，\tau(M,w)\vDash \overline{m}'\lt \overline{k}，根据后继公理 \text{AN-Succ} 有 \overline{m}\lt\overline{m}'，根据传递公理 \text{AN-Trans} 有 \overline{m}\lt \overline{k}，因此 \tau(M,w)\vDash \overline{m}\lt \overline{k}

□

引理2：如果输入为 w 的图灵机 M 在执行 n 步后处于停机状态，则 \mathcal{X}(M,w,n)\vDash\alpha(M,w)

证明： 假设输入为 w 的图灵机 M 在执行 n 步后停机，则意味着存在一个状态 q\in Q，方格 x，以及符号 \sigma 使得:

1. 在执行 n 步后，M 处于 q 状态，并且正在读取第 m 个方格上的符号 \sigma
2. 状态转移函数 \delta(q,\sigma) 是未定义的

根据 \mathcal{X} 的定义可以得知，\mathcal{X}(M,w,n) 描述了此时图灵机 M 的格局，同样又定义可知 \mathcal{X}(M,w,n) 包含了子句 Q_q(\overline{m},\overline{n}) 以及 S_\sigma(\overline{m},\overline{n})（此时的 m 就是读写头正在读取的方格，其一定满足 0\le m\le k，因为 k 被保证是读写头曾经到达过的最右端位置），而这两个子句在一起满足了 \alpha(M,w)。 □

  为了证明 \vDash \tau(M,w)\rightarrow \alpha(M,w)，我们还需要证明如果图灵机没有停机，则 \mathcal{X}(M,w,n) 对于每一步 n 都描述了当时图灵机的格局。

引理3：对于所有 n，如果图灵机 M 在执行 n 步后尚未停机，则 \tau(M,w) \vDash \mathcal{X}(M,w,n)

证明： 对 n 进行归纳。当 n 等于0时，\mathcal{X}(M,w,0)=Q_q(\overline{1}, \overline{0})\land S_\rhd(\overline{0}, \overline{0}) \land ... \land S_{\sigma_k}(\overline{k}, \overline{0}) \land\forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}))，其子句恰好都被包含在 \tau(M,w) 中，因此 \tau(M,w)\vDash \mathcal{X}(M,w,0)。
   当 n > 0 时，假设 M 在 n 步后还没有停机，因为此时不处于停机状态，因此一定有对应的状态转移规则，对具体的三种状态转移规则分类讨论，证明当 \tau(M,w) \vDash \mathcal{X}(M,w,n) 时有 \tau(M,w) \vDash \mathcal{X}(M,w,n+1)

1. 当前的状态转移规则是 \delta(q_i,\sigma_i)=\langle q_j, \sigma_j, R\rangle 时。根据状态转移公理，\tau(M,w) 包含子句
   \begin{aligned}
   &\forall x.\forall y.((Q_{q_i}(x,y)\land S_{\sigma_i}(x,y))\rightarrow \\ &\qquad(Q_{q_j}(x',y')\land S_{\sigma_j}(x,y')\land\Phi(x,y)))\tag{1.1}
   \end{aligned}

   使用 m 和 n 去实例化该子句中的量词绑定的 x 和 y，可以得到

   \begin{aligned}
   &Q_{q_i}(\overline{m},\overline{n})\land S_{\sigma_i}(\overline{m}, \overline{n}) \rightarrow \\ &\qquad Q_{q_j}(\overline{m}',\overline{n}')\land S_{\sigma_j}(\overline{m},\overline{n}')\land\Phi(\overline{m},\overline{n})\tag{1.2}
   \end{aligned}

   由归纳假设 \tau(M,w) \vDash \mathcal{X}(M,w,n) 可得

   Q_{q_i}(\overline{m}, \overline{n})\land S_{\sigma_0}(\overline{0}, \overline{n})\land...\land S_{\sigma_k}(\overline{k},\overline{n})\land\forall x. (\overline{k} < x \rightarrow S_0(x, \overline{n})) \tag{1.3}

   由于在运行 n 步之后，图灵机在 m 方格读取 \sigma 符号（m 和 \sigma 究竟是什么不重要，我们只需要知道一定存在一个 m 和 \sigma 满足这些条件，这是图灵机的定义规定的——读写头总是在读取某个方格，而每个方格里都有一个字符），因此，(1.3) 蕴含了

   Q_{q_i}(\overline{m}, \overline{n})\land S_{\sigma_i}(\overline{m}, \overline{n})\tag{1.4}

   将 (1.4) 应用到 (1.2)，可以得到

   Q_{q_j}(\overline{m}',\overline{n}')\land S_{\sigma_j}(\overline{m},\overline{n}')\land \Phi(\overline{m},\overline{n})\tag{1.5}

   其中谓词 \Phi(\overline{m},\overline{n}) 告诉我们除了第 m 个方格以外，其余所有方格在第 n+1 步后都和第 n 步时保持一致，因此我们可以将 (1.3) 中描述每个方格状态的除了 S_\sigma(\overline{m},\overline{n}) 以外的（因为 S_\sigma(\overline{m},\overline{n}) 是图灵机正在读取和操作的方格，不能保证 n+1 步后还和第 n 步一致，也就是说他不在 \Phi(\overline{m},\overline{n}) 谓词中） S 子句提取出来并将 \overline{n} 修改为 \overline{n}'，得到

   \underbrace{S_{\sigma_0}(\overline{0},\overline{n}')\land...\land S_{\sigma_k}(\overline{k},\overline{n}')}_{\text{不包含 } S_{\sigma_m}(\overline{m},\overline{n}')}\tag{1.6}

   注意，谓词 \mathcal{X}(M,w,n) 包含三部分，第一部分是描述状态的 Q 谓词，第二部分是一组描述纸带状态的 S 谓词，最后一部分断言纸带在 k 个方格之后的所有方格都是空白。如果要证明 \tau(M,w)\vDash \mathcal{X}(M,w,n) 时有 \tau(M,w)\vDash \mathcal{X}(M,w,n+1)，那么我们就要证明构成 \mathcal{X}(M,w,n+1) 的这三部分。现在

   1. 由 (1.5)，我们已经证明其中的 Q 谓词部分（(1.5) 中的 Q_{q_j}(\overline{m}', \overline{n}') 子句）
   2. 由 (1.5) 和 (1.6)，对于所有的 0 \le x\le k（包括 x=m，此情形位于 (1.5) 中），我们都证明了 S_{\sigma_x}(\overline{x},\overline{n}')

   接下来我们还需要证明断言空白方格的子句 \forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}'))（注意 S_0(x,\overline{n}) 变成了 S_0(x,\overline{n}')，因为此时要证明的是 \mathcal{X}(M,w,n+1)，因此对应子句中的 \overline{n} 也需要改为其后继 \overline{n}'）。此时需要分析 m\lt k 或 m = k

   1. 如果 m \lt k，由归纳假设 (1.3)，有 \forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}))；根据引理1有 \tau(M,w)\vDash \overline{m}\lt\overline{k}，因此，根据传递公理 \text{AN-Trans} 可得 \forall x. \overline{k}\lt x\rightarrow \overline{m}\lt x。因此由谓词 \Phi(\overline{m},\overline{n})，可知 \forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}')) 成立。
   2. 如果 m = k，则当执行 n+1 步后，由于状态转移规则要求读写头向右移动，因此图灵机 M 必然同样读取了 k+1 方格的符号，此时 k+1 变成了读写头曾途径的最右侧的方格。因此此时 \mathcal{X}(M,w,n+1) 应当包含 S_0(\overline{k}',\overline{n}')（因为 \overline{k}' 是 k+1 方格，而由于在第 n+1 步以前 k+1 方格都从未被读取过，因此一定是空的）。同理，由于此时新的最右侧边界变成了 k+1 而不是 k，因此 \mathcal{X}(M,w,n+1) 的最后一个子句同样应当改为 \forall x.(\overline{k}'\lt x\rightarrow S_0(x,\overline{n}'))。此时我们需要证明这两个新子句的正确性。
        根据归纳假设 (1.3)，有 \forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}))，同时由于 m=k，因此由谓词 \Phi(\overline{m},\overline{n}) 有 \forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}'))。特别的，由后继公理可知 \overline{k}\lt\overline{k}'，因此有 S_0(\overline{k}',\overline{n}')。
        由 \forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}')) ，\overline{k}\lt \overline{k}' 以及传递公理 \text{AN-Trans}，可得 \forall x. (\overline{k}' \lt x \rightarrow S_0(x, \overline{n}'))。

   此时，我们已经证明了 \mathcal{X}(M,w,n+1) 的 Q 谓词子句（由 (1.5)），S 谓词子句（由 (1.5) 和 (1.6)），以及在 m=k 和 m\lt k 两种情况下用于断言空白方格的子句，将这三者结合起来，我们得到了

   1. 当 m\lt k时
   \begin{aligned}
   &Q_{q_j}(\overline{m}',\overline{n}')\land S_{\sigma_j}(\overline{m},\overline{n}')\land \\ &\qquad S_{\sigma_0}(\overline{0},\overline{n}')\land...\land S_{\sigma_k}(\overline{k},\overline{n}')\ \land \\ &\qquad
   \forall x. (\overline{k} \lt x \rightarrow S_0(x, \overline{n}'))
   \end{aligned}
   2. 当 m=k 时
   \begin{aligned}
   &Q_{q_j}(\overline{m}',\overline{n}')\land S_{\sigma_j}(\overline{m},\overline{n}')\land \\ &\qquad S_{\sigma_0}(\overline{0},\overline{n}')\land...\land S_{\sigma_k}(\overline{k},\overline{n}')\land S_0(\overline{k}',\overline{n}')\ \land \\ &\qquad \forall x. (\overline{k}' \lt x \rightarrow S_0(x, \overline{n}'))
   \end{aligned}

   合在一起，我们证明了当 \delta(q_i,\sigma_i)=\langle q_j,\sigma_j,R\rangle 时，对所有 n，有\tau(M,w)\vDash\mathcal{X}(M,w,n)。

2. 当 \delta(q_i,\sigma_i)=\langle q_j,\sigma_j,L\rangle 时，只有 m=0 时的情况需要特别说明，其余部分的证明策略均与1相同，此时可以直接从 ((Q_{q_i}(\mathsf{o}, \overline{n})\land S_{\sigma_i}(\mathsf{o}, \overline{n}))\rightarrow (Q_{q_j}(\mathsf{o}, \overline{n}')\land S_{\sigma_j}(\mathsf{o}, \overline{n}')\land\Phi(\mathsf{o}, \overline{n})) 得到证明。

3. 当 \delta(q_i,\sigma_i)=\langle q_j,\sigma_j,N\rangle 时，证明策略与1相同。

  至此，我们已经证明了对于所有的 n，有\tau(M,w)\vDash\mathcal{X}(M,w,n)。□

引理4：如果图灵机 M 在 w 上停机，则 \vDash\tau(M,w)\rightarrow\alpha(M,w)

证明： 由引理3，我们知道对任意 n，\mathcal{X}(M,w,n) 都准确描述了此时图灵机的格局，因此 \tau(M,w)\vDash \mathcal{X}(M,w,n)。假设 m 在执行 k 步之后停机，则此时 M 一定在扫描某个方格 m\in \N。此时 \mathcal{X}(M,w,k) 就描述了 M 的停机格局，因此由引理2，\mathcal{X}(M,w,k)\vDash \alpha(M,w)，根据 \vDash 的传递性以及 Semantic Deduction Theorem，有 \vDash\tau(M,w)\rightarrow\alpha(M,w)。□

引理5：如果 \vDash\tau(M,w)\rightarrow\alpha(M,w)，则图灵机 M 在 w 上停机

证明： 令 \mathfrak{M} 是一个 \mathcal{L}_M-结构，其域为 \N，解释常量符号 \mathsf{o}^{\mathfrak{M}}=0，解释一元函数 '^{\mathfrak M} 为后继函数， 解释二元谓词 <^{\mathfrak{M}} 为自然数之间的小于关系，解释二元谓词 Q_q^{\mathfrak{M}} 为

解释二元谓词 S_\sigma^{\mathfrak{M}} 为

也就是说我们将一个图灵机 M 的所有信息以及其每一步的格局“编码”进了 \mathfrak{M} 里。显然，有 \mathfrak{M}\vDash\tau(M,w)（我们可以进一步推广：对任何满足这样一个图灵机 N 的“编码”的 \mathcal{L}_N-结构 \mathfrak{N}，都有 N\vDash\tau(N,w)）；如果 \vDash\tau(M,w)\rightarrow \alpha(M,w)，则 \mathfrak{M}\vDash\alpha(M,w)。由 \mathfrak{M} 的定义以及 \alpha(M,w) 的定义可知图灵机 M 处于状态转移函数未定义的格局上，也即 M 已停机。□

定理1：判定问题是不可判定的：不存在一个接受任意一阶语句 w 图灵机 M，使得当 w 有效时 M 输出 1，反之输出 0

证明： 我们将会将停机问题reduce到该问题。假设这样的图灵机 M 是存在的，那么针对任意图灵机 N，我们可以构造对应的一阶语句 \tau(N,w)\rightarrow\alpha(N,w)，并让 M 计算该语句，如果 M 停机，则说明该语句成立，否则不成立；又因为该语句对应了图灵机 N 的停机，我们成功的将停机问题reduce到了判定问题：图灵机 N 在 w 上停机当且仅当 M 计算 \tau(N,w)\rightarrow\alpha(N,w) 的结果是 1。由于停机问题是不可判定的，因此判定问题本身同样是不可判定的。□

定理2：一阶逻辑的可满足性问题是不可判定的：不存在一个接受任意一阶语句 w 图灵机 M，使得当 w 可满足时 M 输出 1，反之输出 0

证明： 我们将会将判定问题reduce到可满足性问题，假设这样的图灵机 M 是存在的，假设其输入为一阶语句 w，我们可以构造一个图灵机 S，将其输入 w 的每个符号都向右移动一格，接着回到最左侧并写入对应逻辑否的符号 \neg。同时构造另一个图灵机 N，当它的输入是 1 时就抹去并输出 0，输出是 0 时就抹去病输出 1，此时将这三台图灵机结合之后得到的图灵机 S\smallfrown M\smallfrown N就是一个解决判定问题的图灵机，过程如下：首先，对于任意输入的一阶语句 w，S 将 w 修改为 \neg w 并输入给 M，M 判定 \neg w 是否可满足并输出 1 或 0，最后 N 逆转 M 的输出结果并停机。也即 M 判定 \neg w 是否是可满足的，因为已知 w 是有效的当且仅当 \neg w 是不可满足的，所以 M 输出 1 时说明 w 不可满足，反之说明 w 可满足，因此 N 逆转 M 的输出并停机。综上，我们成功将判定问题reduce到了可满足性问题，由于判定问题是不可判定的，因此可满足性问题同样是不可判定的。□

定理3：判定问题是半可判定的（Semi-Decidable），换言之，判定问题的值域是递归可枚举集合：存在一个接受任意一阶语句 w 的图灵机 M，使得当 w 有效时 M 输出 1，反之则不停机

证明： 由于一阶逻辑的推导是可枚举的，因此可以构造一个图灵机 M 从公理触发枚举所有一阶语句的推导，每当其找到一个一阶语句的推导，就判断是否是 w 的推导，也即是否 \vdash w，如果是就停机并输出 1，由一阶逻辑的soundness定理可知，\vdash w 蕴含 \vDash w。因此我们成功的构造了一个判定问题的semi-decider。□

定理4：一阶逻辑的不可满足性问题是半可判定的，换言之，不可满足问题的值域是递归可枚举集合：存在一个接受任意一阶语句 w 图灵机 M，使得当 w 不可满足时 M 输出 1，反之输出则不停机

证明： 由于哥德尔完备性定理，一阶逻辑的可满足性等价于一阶逻辑的自洽性(见Henkin's Model Existence Theorem）。因此一个一阶语句 w 是不可满足的当且仅当 \neg \text{Con}(\lbrace w\rbrace)，也即 \lbrace w\rbrace \vdash \bot。我们可以构造一个图灵机搜索所有 w 的推导，一旦搜索到等价于 w\vdash \bot 的推导就输出 1，否则不停机。这样，我们成功构造了一个不可满足性问题的semi-decider。□

推论1：一阶逻辑的可满足性问题不是半可判定的，换言之，可满足性问题的值域不是递归可枚举集合

证明： 如果可满足性问题是半可判定的，那么由于不可满足性问题也是半可判定的，这意味着可满足性问题同时是semi-decidable与co-semi-decidable的，这意味着可满足性问题应当是可判定的（如果一个集合和他的补集都是递归可枚举的，那么这个集合是一个递归集合），然而我们已经证明了可满足性问题是不可判定的，因此可满足性问题也不是半可判定的。实际上，可满足性问题的复杂度是co-RE的。□