我们现在要讨论能否用机器完成证明的问题。在这里，我们所说的机器就是指图灵机。但为了讨论的方便，我们在这里使用一个图灵机的等价模型寄存器机。它有\(m\)个用来存放符号串的内存，能够写入某个内存末尾加字符、减字符、跳转、打印和停机五种指令。一个寄存器机程序（简称程序）就是有限条寄存器机上的指令（且最后一条为停机）的集合。程序的输入是指程序开始时第一个内存上的符号串。程序的输出是指程序打印出来的符号串。
我们称一个字符串集合\(W\)是可判定的，当且仅当存在一个程序在输入某个字符串时，如果这个字符串属于\(W\)就输出空串，否则输出非空串；称一个字符串集合\(W\)是可枚举的，当且仅当存在一个程序在输入空串时，能恰好输出所有\(W\)内的字符串。对于函数\(F:\mathcal{A}^* \to \mathcal{B}^*\)，如果存在一个程序输入\(w \in \mathcal{A}^*\)总能恰好输出\(F(w)\)，就称\(F\)是可计算的。
是否存在一个不可判定的集合？反例就是自指，小明说“我在说谎”时就会自动走向不可判定小明是否在说谎的悖论。这里的关键在于，我们将会看到一个程序与一个字符串本身是没有界限的，因此程序自身可以作为输入被输入进一个程序，由此我们仿照说谎的小明来导出矛盾。下面就来严格地说明这件事。首先任何一个程序拼接成某个有限字符集下的一个有限字符串，取这个字符串在这个字符集下的字典序，这样我们就可以把任何一个程序都与一个自然数对应起来，这称为程序的哥德尔编码。这个字符集下的程序就可以用程序本身来作为输入了，也即把程序本身的哥德尔编码作为这个程序的输入是完全合法的。对于这个字符集上的所有程序我们都可以这么做。对于所有这些程序，有一些会运行终止有一些不会。现在我们把这里面所有不停机的程序（的哥德尔编码）收集进集合\(\Pi_{\text{halt}}\)，我们证明这个集合就是不可判定的！假如存在判定这个集合的程序\(P_0\)，那么\(P_0\)会在输入程序停机时输出空串，不停机时输出非空串。现在我们对\(P_0\)做一点修改，每当\(P_0\)要输出时就强制停机，而当\(P_0\)要正常停机时就让它死循环。这样得到了一个程序\(P_1\)，那么现在让\(P_1\)输入自身，假如它要停机那么它就不停机，如果它不停机他就会停机。这样我们就得到了一个说谎的小明一样不可能存在的程序，这就导出了矛盾。
下面我们要说明一阶逻辑中恒真命题的集合是不可判定的，也即集合\(\{\varphi \in L_0^{S_{\infty}}\mid\ \models \varphi\}\)是不可判定的。我们将会把这个问题规约为停机问题。 没写完，待会儿再写。