哥德尔不完全性定理表明，任何一个形式系统，只要包括了简单的初等数论描述，而且是自洽的，它必定包含某些系统内所允许的方法既不能证明真也不能证伪的命题。
- 没有证明
有没有证明只有有限多的质数？当然没有! 毕竟，欧几里德在他的《几何原理》中告诉我们，有无限多的质数。由于任何定理都不可能既是真的又是假的，所以我们不能给出只有有限多个质数的证明。
因此，证明某个定理没有证明的方法之一就是为它的否定找一个证明。我们知道，没有证据表明数字π是有理的，因为数学家已经找到了几个证明，表明它是无理的。我们知道自然数和实数之间不可能有1比1的对应关系，因为康托尔证明了实数比自然数多。
但是，当你可以直接证明否！的时候，为什么要关心某些证明的不存在？因为哥德尔的第一个不完备性定理。
数学通过证明从公理发展到定理。哥德尔表明，如果我们从足以进行一些基本算术的公理出发，那么一定有一个独立于我们公理的陈述。这意味着，无论是陈述本身还是其否定都无法从公理中得到证明。
这种现象最显著的例子之一是康托尔的连续统假说。集合论的标准Zermelo-Fraenkel公理既不能证明连续体假说，也不能证明其否定。
但我们怎么知道我们不能证明连续统假设呢？就是说。我们如何证明没有证明？
几何学中的平行公设
让我们来看看一个有2000多年历史的例子。欧几里德在他的《几何原理》中为几何学提出了五条公理。
- 首先，你可以从任何一个点到任何一个点画一条直线。
- 第二，你可以在每个方向上无限延伸任何一条直线。
- 第三，给定一个点和一个半径，你可以画一个圆。
- 第四，所有的直角都是相互相等的。
然而，欧几里德的公理中最有趣的是第五条。这就是所谓的平行公设。
- 如果一条直线落在两条直线上，使同一侧的内角小于直角，那么这两条直线就会在那一侧相交。
本质上，平行公设指出，两条不平行的直线最终必须相交。
几千年来，数学家们一直试图证明前四条公理能推导出平行公设。为什么呢？无穷大使问题变得复杂。欧几里德对平行直线的定义是这样的。
平行的直线是指在同一平面内，在两个方向上都能无限延伸，但在任何一个方向上都不相交的直线。(《欧几里德元素》，第一册，定义23）
因此，对于古代数学家来说，声称两条线是平行的，就意味着它们甚至不会在无限远处相交。然而，这些数学家也意识到，有一些线确实在无限远处相交：所谓的渐近线。
平行公设对直线在无限远处的行为提出了规定，因此，它不被认为是不言而喻的。如果一个数学定理不是不证自明的，那么它就需要一个证明。然而，从欧几里德的前四条几何公理中证明平行公设的每一次尝试都注定要失败。
非欧几里得几何学在19世纪被发展，极大地改变了我们对平行公设的理解。
数学家们发现了一些几何学，在这些几何学中，欧几里德的前四条公理是真实的，但平行公设却失败了。尤金尼奥-贝尔特拉米（Eugenio Beltrami）是第一个研究的数学家，尽管他的同时代人没有意识到他工作的重要性。贝尔特拉米是非欧几里得几何学的先驱者。
这些非欧几里得几何学如何意味着没有平行公设的证明？如果有这样的证明，那么前四个公设的每个模型都将是平行公设的模型。但事实并非如此。所以不可能有一个证明。
证明与模型：逻辑学中的一个案例研究
但这一切在形式上是如何运作的呢？我们怎样才能给出一个完整的数学证明？这就是数理逻辑发挥作用的地方。经典的命题逻辑可以通过三个公理和一个规则对所有命题p和q进行公理化。
- 公理1.p→（q→p）。
- 公理2.（p→（q→r））→（（p→q）→（p→r））。
- 公理3.¬¬p→p。
- 推演规则：肯定前件（Modus Ponens）。从'p'和'p → q'，推导出'q'。
- 如果上述符号显示有问题
第三条公理也被称为双重否定消去律，它等同于更著名的排中律'p∨¬p'。
这几个公理和规则就是我们证明所有经典逻辑的命题重言式所需要的全部。无论多么复杂的重言式，总会有证明的。假设你想证明重言式‘(q→p)→(q→p)’ 是这样的：
- 公理1的实例。P→(q→P)。
- 公理2的实例。(p→(q→p))→((p→q))
- 第1,2行的 "模式"。(p → q) → (p → q)。
我们只用了三步就证明了重言式。
虽然这样的形式化证明看起来很繁琐，但形式化证明系统对于数理逻辑来说是不可或缺的，因为它们提供了一种将证明作为数学对象的方法。
现在，你可能会想知道。我们真的需要古典逻辑的所有这三个公理吗？难道我们不能从前两个公理和推演法则中证明双重否定的消去律吗？
就像欧几里德的平行公设一样，这是不可能的。但我们如何才能证明这一点呢？诀窍是找到一个命题逻辑的模型，满足前两个公理和演绎规则，但不满足第三个。
- 3值逻辑的真值表。
所以我们来发明这样一个模型。我们将考虑三个真值：真T、假F和中间I。在我们的模型中，每个命题都将有这三个真值之一。然后，更复杂的命题的真值可以用上图中的真值表来计算。
¬p的真值被定义为'p→F'的真值。
例如，如果p的真值是I，那么¬p的真值一定是'I→F'。根据真值表，就是F。所以如果p是中间值，那么¬p就为假。
我们能否证明这个模型满足前两条公理和演绎规则，但不满足第三条？
为了说明演绎规则在我们的模型中是真的，假设'p'和'p→q'都有真值T。我们必须证明'q'也有真值T。设想'q'没有真值T，而是有真值I或F。因此，'q'也必须有真值T。
这表明演绎规则在我们的模型中是真的。只要'p → q'和'p'是真的，那么'q'也一定是真的。
那公理呢？第一个公理，'p → (q → p)'，可以在模型中显示为真，具体如下。
- 如果'p'有真值T，那么'q→p'也有真值T，但这时'p→（q→p）'将是真T。
- 如果'p'有真值I，那么'q → p'就有真值I或T（真值表的第二列）。但接下来，'p→（q→p）'将是真T，因为这只是'I→I'或'I→T'。
- 最后，如果'p'有真值F，那么'p→（q→p）'的形式就是'F→（q→p）'。根据真值表，这永远是真的。
第二条公理也可以用类似的方式证明为真。
然而，有趣的是，双重否定消去律在这个模型中失效。为什么呢？只要'p'有真值I，那么'¬p'就是F，'¬¬p'一定是T。所以'¬¬p → p'是'T → I'，但那只是I。
所以'¬¬p → p'在这个模型中不是一个重言式：有一些情况下它不是真的。由于这个原因，排中律也必须在我们的模型中失效。
那么我们得到了什么？我们已经证明了双重否定消去律或排中律是经典命题逻辑的必要公理。
结论
逻辑学家使用模型和形式证明来推理一些句子是否能从其他句子中得到证明。我只是在上面给大家介绍了一个很小的例子，但本质上同样的想法，被用来证明连续体假说的独立性和数理逻辑中其他迷人的结果。