在本文的6.2节中，我们看到了数学逻辑的简要介绍以及计算理论对该主题的影响。
为了开始我们的讨论，让我们看看数学逻辑的基本组成部分。
公式由变量、关系、逻辑运算符和量词组成。
在公式中，变量从指定的范围中获取值。宇宙的一些例子包括正整数和实数。
关系是一个或多个参数的布尔函数。一个典型的例子是关系+(x,y,z)，当且仅当x + y = z，其计算结果为真。
公式中允许的量词包括存在量词∃和全称量词∀。
这里有一些公式的例子。第一个例子是关于0存在的语句：
∃z∀x +（x,z,x）
第二个例子是关于可加逆的存在性的陈述。
∃z(∀x +(x,z,x))∧（∀s∃t +(s,t,z)）
公式中未量化的变量称为自由变量。没有自由变量的公式称为句子。
一种比较抽象的公式是没有明确规定关系的公式。例如，我们可以通过将具体关系+替换为占位符关系R1来更通用地重写最后一个例子：
∃z(∀x R1(x,z,x))∧（∀s∃t R1(s,t,z)）
为了全面评估一个句子，我们必须指定所使用的精确关系和变量的范围。我们通过指定一个模型来做到这一点。给定的句子可能在一个模型中为真，而在另一个模型中为假。例如，最后一句话在模型（0,+）中为真，但在模型（0,+）中为假。
在特定模型中为真的赢博体育句子的集合就是该模型的理论。
给定某个模型中的一个句子，一个重要的问题是这个句子是否为真。如果存在某种计算过程，可以在有限时间内确定给定的句子是否为真，那么一个理论就是可判定的。
在6.2节中，作者证明了模型M = (n,+)的理论是可判定的。
Alonzo Church证明了模型M = (M,+, x)的理论是不可判定的。显示此结果的一种方法是使用ATM中的缩减。假设这个理论有一个决定因素。给定任意图灵机M和输入w，我们可以构造这个句子
∃x φM,w
其中φM，w是一个精细的公式，它表示x编码了M接受w的计算轨迹。然后我们就可以在这个句子上运行我们模型的决策器：如果这个句子是真的，我们就有了M接受w的证明，我们可以用这个知识来决定ATM。
驱动公式φM，w构造的一个关键思想是观察到，如果我们能够使用加法和乘法运算，我们可以将大整数x分解成它的组成数。通过这样做，我们可以将计算跟踪分解为其组成符号，然后检查结果符号序列是否表示w在M上运行的有效接受计算。
一旦我们了解到某些理论是不可确定的，我们就可以退回到另一种策略。相反，我们建立了一个证明系统，并用它来制造一系列可证明为真的陈述。
证明是数学的中心概念之一。在我们正在建立的框架中，证明制度有几个关键组成部分。
证明系统有两个关键属性。如果每一个可以被证明的陈述都是正确的，那么证明体系就是可靠的。如果每一个真命题都能被证明，那么这个证明体系就是完备的。
不幸的是，Kurt Gödel表明任何证明系统要么是健全的要么是完整的，但没有一个证明系统可以两者兼而有之。在他著名的不完备性定理中，他表明任何健全的证明体系都是不完备的。
下面是一些证明不完备定理的结果。第一步是想象一个检验证据的机械过程。
语言PROVABLE = {φ | φ有证明}是图灵可识别的。
这是一个可证明的识别器。识别器使用枚举器E来枚举赢博体育可能字符串的语言。
关于输入φ：
由于我们先前证明了模型M = (n,+, x)的理论是不可判定的，我们现在可以用矛盾的方法证明这个理论的任何证明系统都是不完整的。我们通过为理论构造一个决策器来做到这一点：
关于输入φ：
我们已经知道模型M = (M,+, x)的理论是不可确定的，所以这个决策不可能起作用。走出这一困境的唯一途径是考虑举证制度不完备的可能性；也就是说，在我们的证明体系中存在不能被证明的真命题。允许不完整性将允许上面的步骤1永远运行，这将导致我们的机器不是一个决策器。
最后，这里是另一种利用递归定理的不完备性证明。
证明使用了以下图灵机S：
输入x：
这里有两种可能性。第一个是我们构造的句子ψ有一个证明。如果有证据，它一定是真的。如果这个句子为真，我们就有一个矛盾，因为这个句子说S不接受0，这与S本身的行为相矛盾。第二种可能性是ψ没有证明。如果是这样，S不可能接受0，那么句子ψ一定是真的。这证明了一个不能证明的真命题的存在性。