书名：皇帝新脑（第一推动丛书·综合系列）
作者：罗杰·彭罗斯
译者：许明贤,吴忠超
出版社：湖南科学技术出版社
出版时间：2018-01-01
ISBN：9787535794444
第4章 真理、证明和洞察
- 数学的希尔伯特计划
- 形式数学系统
- 哥德尔定理
- 数学洞察
- 柏拉图主义或直觉主义
- 从图灵结果到类哥德尔定理
- 递归可列集
- 芒德布罗集是递归的吗
- 一些非递归数学的例子
- 芒德布罗集像非递归数学吗
- 复杂性理论
- 物理事物中的复杂性和可计算性
二、形式数学系统
1、形式系统
- 形式系统（Formal System），包含字母、字的集合及由关系组成的有限集合。
例如：集合论、布林代数、欧几里得平面几何及贝克式正规形式（Backus Normal Form）都是形式系统。
2、常用的形式系统
- 有：语言、数理规则和逻辑。其中由于数学的研究对象是形式系统中唯一天生的逻辑自洽系统，因此数学也被一些人称为：形式科学。而语言大类中，部分为逻辑自洽的形式系统，如计算编程用的各类程序语言等。
3、形式证明
- 在数学领域里，形式证明是形式系统的产物，由一些公理与演绎规则组成。定理便是形式证明可能的最后一行结论。这几个步骤总和起来便是数学界通称的形式主义。
- 大卫·希尔伯特创立元数学以作为讨论形式系统的学科。
任何用于讨论形式系统的语言称为元语言。
元语言也许像普通语言一样自然，或它可能部分形式化，但它通常比起受检验系统的形式语言来得较不正规化。
此形式语言称为对象语言，意指问题议论的对象。
4、费马大定理的形式化
5、形式系统的组成
命题函数
系统的公理
系统的公理是由一般命题的有限罗列所构成，假定在符号的意义已给定的情形下，这些命题的真理性是不证自明的。
例如，对于任何命题或命题函数P, Q, R（），在我们公理之中有:
（P&Q）⇒P，
～（～P）⇔ P，
～∃x[R（x）]⇔ ∀x[～R（x）]，
其“自明的真理性”清楚地可由其意义所确定基本的算术公理
∀x, y[x+y=y+x]∀x, y,
z[（x+y）×z=（x×z）+（y×z）]，步骤法则
步骤法则是诸如这样（自明）的东西：
“从P和P⇒Q我们可推出Q”，
“从∀x[R（x）]我们可推出把一特殊的自然数代入到R（x）中的x而得出的任何命题”。
这些是告诉我们如何从已成立的命题引出新命题的方针。现在从公理开始，然后不断重复应用步骤法则，就可以建立起一长串的命题。
6、希尔伯特计划的思想
希尔伯特计划的思想是，对于任何定义好的数学领域，去找一足够广泛的公理和步骤法则的表，使得所有适合于该领域的正确的数学推理的形式都可以编入。
希尔伯特的希望是，对于任何一串代表一个数学命题的符号，譬如讲P，人们应能证明P或者～P，依P是真的还是假的而定。
P仅仅为一语法正确的符号串。
如果P为一道定理（也就是可在系统内证明P），则符号串P的真值就可被赋予真。另一方面，如果能证明～P为定理的话，则可被赋予假。
为了使这些有意义，我们除了完备性外还需要一致性。也就是说，不应有P和～P都为定理的符号串P。否则P会同时是真的和假的！把数学陈述中的意义抽走，只把它们当成某种形式数学系统的符号串是形式主义的数学观点。
有些人喜欢这种观点，而数学就变成一种“无意义的游戏”。然而是“意义”而非盲目的算法计算才赋予数学以实质。幸好哥德尔给了形式主义以毁灭性的打击，没让形式主义得逞！
