数学联邦政治世界观
超小超大

数理逻辑-余俊伟(三) (4-3)

(一阶)算术语言 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),接着再看更方便。

相关小说

随缘观影 连载中
随缘观影
言岁安
练笔文,ooc预警,文内视频若有侵权必删,一切随缘。
0.2万字1个月前
沉:降 连载中
沉:降
shadowohyeah
自设的故事。自娱自乐用。总之就是血族和血猎的老套故事。
5.1万字1个月前
枇杷树荫 连载中
枇杷树荫
piW_riW
本不拘泥于情爱的明媚少女因为他无法自拔,本有光明未来却因拯救男主而意外去世。“庭有枇杷树,吾妻死之年所手植也。”而我将永远沉浸于它的树荫下。
4.4万字1个月前
米露的无限重生 连载中
米露的无限重生
琦柒七
你如果能回到18岁,你想做什么?你如果一直能回到18岁你又想做什么?是痛快地来一场诗与远方地说走就走地旅行,还是努力学习奋发向上,考一个好的......
20.8万字1个月前
STAR——star 连载中
STAR——star
希会你
(2021.7.11签约成功୧⍢⃝୨)“我还记得,你的笑容……”“它就像一束光,伴随着温暖,给我希望……”“因为有你,我不再孤独了呢!”“我......
29.3万字1个月前
死神是我哥哥 连载中
死神是我哥哥
雾槿
别人的外挂是死神,这有什么?我的哥哥是死神,惹过我的人要么都被哥哥杀了,要么都被折磨疯了
4.2万字4周前