(一阶)算术语言 L1 的图册 sigL1 = {0, S, +, × },其中 0 是常量符号,S 是一元 函数符号,+, × 是二元函数符号。特殊地,分别称此时的 L1-项、L1-公式、L1-语句、 L1-结构、L1-模型、L1-理论为算术项、算术公式、算术语句、算术结构、算术模型、算 术理论。如无特殊说明,第 5.3 节和第 5.4 节所谈及的项、公式、语句、结构、模型、理 论默认都是算术的。另外,称基于算术语言的一阶公理系统为一阶算术公理系统。 罗宾森算术最早由塔斯基、莫斯托夫斯基1 、罗宾森2 在 1953 年提出3 。
5.3.2 可表示性
本节主要任务是证明所有的可计算关系都是可表示的。
5.3.3 算术化
首先用哥德尔编码的方式把算术语言的初始符号进行算术化。 本子节所关注的语法概念都有可以借助哥德尔编码转换为自然数的某个原始递归子 集(除证明转化为可计算子集、可证性转化为可计算枚举子集外),从而都是可表示的。
哥德尔编码的实质是在标准算术模型 N 中创建变元的镜像,比如,21 是 x0 的镜像。
5.3.4 不完全性
此节证不完全性。
5.3.5 相关推论:不可表示性、不可判定性、希尔伯特第 10 问题
丘奇于 1935 年、图灵于 1936 年分别独立地证明了一阶逻辑的不可判定性1 ,所以 如下推论也称丘奇–图灵不可判定性定理。1931 年,哥德尔没有证明2 丘奇–图灵不可判 定性定理,原因应该是如本书第 256 页所说,当时关于算法的概念还不是十分清楚。但 是后来人们发现该定理可以作为哥德尔所证明的不动点引理 5.3.77 的推论。为方便起见, 先证明 RA 的强不可判定性定理。
5.4 第二不完全性
冯·诺伊曼去信向哥德尔说明,用相同思路可以证明哥德尔第二不完全性定理。哥德尔、伯内斯和泡利同乘一条船前往美国,在旅途中和抵达普林斯顿高等研究院的几周里,哥德尔向伯内斯讲解了哥德尔第二不完全性定理的证明细节4 。 后来,伯内斯从哥德尔的证明中提取出可证性条件,然后推出了哥德尔第二不完全性定理。
哥德尔第二不完全性定理:设 T 是足够强的可计算公理化的理论。如果 T,比如皮亚诺算术,是一 致的,那么它不能证明自身一致性。
5.4.1 皮亚诺算术
由于本书所证哥德尔第二不完全性定理的最小典型实例是皮亚诺算术,所以先介绍皮亚诺算术。
5.4.2 可证性条件
可证性条件最早是由伯内斯于 1939 年从哥德尔的证明中提取出的,由于著作也署名希尔伯特,所以也称希尔伯特–伯内斯可证性条件。
3(可证性条件). 设 φ, ψ 是公式。三个可证性条件为: D1 : 如果 `T φ, 那么 `T ✷Tφ; D2 : `T ✷T(φ → ψ) → ✷Tφ → ✷Tψ; D3 : `T ✷Tφ → ✷T✷Tφ。
5.4.3 T满足D1
本子节关注可证性条件 D1,并且证明满足一定条件的理论 T 满足 D1。 引理 5.4.19. 设 T 是包含 PA 的、可计算公理化的理论。
5.4.4 T满足D2
首先引入可证计算的概念以形式化部分函数和关系,然后形式化部分算术定理,继而形式化有穷序列的概念和有穷序列的串接运算,从而形式化原始递归和语法概念,最后利用形式化的有穷序列概念、串接运算、证明概念证明 T 满足 D2。
5.4.5 T满足D3
该节引入了新符号释放了自由变元。
5.4.6 不完全性
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。