本文主要是介绍《哥德尔证明》阅读笔记——一致性问题，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！
前言
从第一次了解到哥德尔不确定性原理时，我就被此定理的内涵和意义所吸引，也对这个定理的证明过程充满兴趣，最近闲暇时，买了这本《哥德尔证明》的书，希望理解这个意义重大的数学定理的核心，在此做一个阅读笔记。
背景
提哥德尔不确定性原理就不得不追溯到一个古老且优美的数学思想“公理化方法”，公理化方法最早来自于古希腊的欧氏几何，欧几里得通过五条公理或公设，再加上对点线面这些概念的定义，运用逻辑推理，导出了几何学的众多定理。
高斯，波尔约，罗巴切夫斯基和黎曼等人通过更改欧几里得第五公设，得到了另一套完全不同的几何学公理，这剧烈动摇了数学家对公理的看法，公理的显然性，自明性不再是纯数学家关注的重点，纯数学家的任务应当时从公理推导出定理，而不需要关心公理是否为真。
数学不应当被视为数量的科学，更恰当的说法应当是对任意给定一组公理，得出其逻辑上蕴涵的结论的学科，它不必和任何实物有对应关系。此时我们对公理化几何学有了进一步的认识，我们甚至可以去掉定义，“点”，“线”，“面”这些概念是无需定义的，因为在公理化体系中它们没有任何意义，它们只是用于承载公理，也可以理解为，它们被公理隐式定义。总而言之，不要关注我们所讨论的“陈述”，只需要关注“陈述”之间的逻辑依赖。用罗素的话总结，纯数学是一门我们不知道自己在说什么，也不知道我们说的是否为真的学科。
一片完全抽象的土地，完全没有任何实际世界的信标，一个很精妙的词语形容是“形式化”的，我们可以建立各种各样的形式化的系统，这些系统可能可以往现实世界进行映射，比如几何学，也可能只有形式的推理过程，这不是什么大问题，一个真正的核心问题是，一个形式化的系统，他的根基——一组公理，是否是一致的，即公理导出的定理是否无矛盾。
公理是否一致的模型法
对欧几里得几何来说，有一条可靠的原则能保证其一致性，即逻辑上不相容的陈述不可能同时为真。这里我们说真，是指欧几里得五大公理在我们的经验中都是真命题，此时说的是形式系统的现实映射。
对于非欧几何或者其他抽象的形式系统来说，想通过和欧氏几何一样的方法说明公理的一致性，只有通过建立一种解释或模型，如果可以将公理转换为这种解释下的真陈述，就可以确定抽象公理的一致性。
这套方法的原理是什么，我的理解是，这相当于将公理的一致性依托在一个我们现实世界的模型中，在模型和抽象的公理体系中做了一个同构，这个模型可以存在，就说明了公理体系的结构也无矛盾。
一个形式系统示例
假设我们有类的概念，表示可区分成分的组合，其中每个成分成为类的元素，有 K K K和 L L L两个集合，那么可以建立一套公理：
- K K K任意两个元素恰好包含在 L L L的一个元素之中
- 没有 K K K的元素被包含在 L L L的两个以上元素之中
- K K K的所有元素并不都包含在 L L L的单个元素之中
- L L L的任意两个元素恰好包含 K K K的一个元素
- 没有 L L L的元素包含 K K K的两个以上的元素
这一套公理体系足够抽象，无法按直观理解，我们即不知道元素是什么，也不知道包含是什么意思，虽然如此，这套公理体系仍然可以导出一些定理。例如通过第一条公理和第三条公理，我们可以知道 K K K的元素数目必然大于 2 2 2，甚至可以证明出 K K K元素数目一定为 3 3 3。
事实上，我们可以找到一个常见的模型，把所有公理映射为关于此模型的真陈述，此映射为： K K K的元素是三角形的三个顶点， L L L的元素是三角形的三个边，包含的含义视为 L L L的元素代表的边是否连着 K K K代表的顶点。那么这套公理映射到这套模型中就是：
- 三角形任意两个顶点在三角形一个边上。
- 三角形任何顶点都不会连两个以上的边。
- 三角形任何一个边，都不可能连所有顶点。
- 三角形任意两个边，恰好会连同一个顶点。
- 三角形任意一个边都不可能连三个顶点。
这些都是真陈述，因此这个形式系统的公理是一致的。
关于一致性的再次追问
使用最严格的态度追问，即便我们所说的模型论是能证明公理系统的一致性的，欧几里得几何学的公理转换为日常经验描述，在我们所属的模型，即日常的平直空间中是正确的吗？我们可以在有穷的事实中确定其“可能正确”，但空间是无限的，我们怎么能确信日常经验能推到无穷的空间呢？三角形那个形式系统是确信无疑的，因为他的模型是可数的，我们可以尽情检验所有边和点。两者有根本区别。
希尔伯特借助笛卡尔坐标系，将欧几里得几何映射为代数学，但这仍然无法回避那个核心的问题，我们没有一个无穷的可信的模型作为源头。遗憾的是，大部分公理系统都只能映射到非无穷模型。
这篇关于《哥德尔证明》阅读笔记——一致性问题的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！
