《哥德尔证明》阅读笔记——一致性问题的绝对证明

2023-12-17 08:12

本文主要是介绍《哥德尔证明》阅读笔记——一致性问题的绝对证明,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

前言

追问一个公理系统的一致性,我们知道一个模型法,即从现实经验中找到一个模型,能将所有公理映射成此模型的真陈述,但很多系统模型是无穷的,比如想检验“空间中两点能确定一条直线”这个欧氏几何公理在空间模型中的陈述,需要检验所有无穷多的点,这显然不可能做到,这是模型法的固有缺陷。数学家也在尝试建立公理一致性的其他方法。

希尔伯特的方法:一致性的绝对证明

模型法可以视为一种相对证明方法,它将公理体系进行映射到别的体系中。希尔伯特尝试建造的证明方法不依赖任何其他系统的一致性。

完全形式化的系统

上章已经提到过“形式化”这个词,它表示抽离意义,只考虑逻辑上的模式的演绎系统。完全形式化(complete formalization) 是更进一步的操作,它意味着将系统内表达式的所有意义都抽离掉,将系统中的陈述作为空洞的“指号”,可以理解为字符串。这些指号的组合由一套精确陈述的规则说明。

这样的系统中公理和定理是什么样的呢?它们是没有任何意义的“串”,或称为有穷长符号序列。这样的系统中公理是一组串定理也是一组串,推导只是根据规则将一组串转换为另一组串而已。

必须做出说明的是,这样的完全形式化系统中,“串”本身可以看起来有意义,它们所用的符号也可能强烈暗示它有意义,比如 1 + 1 = 2 1+1=2 1+1=2就是一个串,但就形式系统而言,它并不关注串的意义,它们只是按照规则允许组合而已。

两个层次的陈述

建立一个完全形式化的系统,一个相当重要的目的是让我们区分两种不同层次的陈述,形式系统的元数学的(meta-mathematics)。以书上的例子说明:

2+3=5这是一个算术形式系统中的指号串
"2+3=5"是一个算术公式这不属于算术形式系统中的串,它属于元数学
如果指号"="用于算数公式中,这个指号两边应是数字表达式属于元数学
用数字"0"代替变元"x",那么可以从公式"x=x"推出"0=0"属于元数学
形式系统X是一致的属于元数学

由此可见,元数学是用于描述形式系统中的串的,严格来说元数学的陈述中,不包含形式系统中的任何指号,上表中,用引号引起来的"2+3=5",并不是串本身,而是代表这个串的名称。

如果说形式系统是我们研究对象本身,那么元数学就是对这个研究对象的讨论,它处于一个更超脱的视角。一个更明晰的例子是这样的,老鹰是由雄性孵蛋,这个陈述串属于动物学;但如果我们说:“老鹰是由雄性孵蛋”这个断言是扯淡,那么我们讨论的对象不是老鹰,而是动物学中的串,这就属于“元动物学”了。

希尔伯特的尝试

希尔伯特看到了形式系统和元数学的区分,他试图建立一致性的绝对证明,他的设想是:发展一种方法,对于一个完全形式化的演算中表达式有穷多结构特征进行分析,证明一致性。如何分析证明呢?记录形式化盐酸中出现的各种指号,说明如何将它们组合成公式,描述公式如何从其他公式得到,最终目的是检验形式上互相矛盾的公式不能从所给公理中得到。

这个方法有一定的要求,公式不能有无穷多的结构属性,也不能涉及对公示的无穷次运算,总结下来就是要给出一套有限的元数学步骤。

一个形象的例子

上述描述依旧比较晦涩,书中给出了一个形象的国际象棋例子。现在让我们想象国际象棋只有棋盘,棋子,忘掉国际象棋的所有规则。那么我们可以把棋子与棋盘视为基本指号;棋子在棋盘上合法排列视为公式或叫做串(良构串);棋子初始排列对应系统的公理;游戏规则就是元数学陈述(此时应当叫做“元象棋”)。我们可以给出元象棋的定理,比如白方只有两个马和王,黑方只有王时,白方不可能将死黑方。总而言之,可以通过有限的元象棋步骤,检验所有初始布局的每一种情况。希尔伯特的目的就是通过这种有穷的方法证明一个给定的形式演算中不可能出现形式上矛盾的串。

这篇关于《哥德尔证明》阅读笔记——一致性问题的绝对证明的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/503698

相关文章

关于MongoDB图片URL存储异常问题以及解决

《关于MongoDB图片URL存储异常问题以及解决》:本文主要介绍关于MongoDB图片URL存储异常问题以及解决方案,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐... 目录MongoDB图片URL存储异常问题项目场景问题描述原因分析解决方案预防措施js总结MongoDB图

SpringBoot项目中报错The field screenShot exceeds its maximum permitted size of 1048576 bytes.的问题及解决

《SpringBoot项目中报错ThefieldscreenShotexceedsitsmaximumpermittedsizeof1048576bytes.的问题及解决》这篇文章... 目录项目场景问题描述原因分析解决方案总结项目场景javascript提示:项目相关背景:项目场景:基于Spring

解决Maven项目idea找不到本地仓库jar包问题以及使用mvn install:install-file

《解决Maven项目idea找不到本地仓库jar包问题以及使用mvninstall:install-file》:本文主要介绍解决Maven项目idea找不到本地仓库jar包问题以及使用mvnin... 目录Maven项目idea找不到本地仓库jar包以及使用mvn install:install-file基

usb接口驱动异常问题常用解决方案

《usb接口驱动异常问题常用解决方案》当遇到USB接口驱动异常时,可以通过多种方法来解决,其中主要就包括重装USB控制器、禁用USB选择性暂停设置、更新或安装新的主板驱动等... usb接口驱动异常怎么办,USB接口驱动异常是常见问题,通常由驱动损坏、系统更新冲突、硬件故障或电源管理设置导致。以下是常用解决

Mysql如何解决死锁问题

《Mysql如何解决死锁问题》:本文主要介绍Mysql如何解决死锁问题,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录【一】mysql中锁分类和加锁情况【1】按锁的粒度分类全局锁表级锁行级锁【2】按锁的模式分类【二】加锁方式的影响因素【三】Mysql的死锁情况【1

SpringBoot内嵌Tomcat临时目录问题及解决

《SpringBoot内嵌Tomcat临时目录问题及解决》:本文主要介绍SpringBoot内嵌Tomcat临时目录问题及解决,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,... 目录SprinjavascriptgBoot内嵌Tomcat临时目录问题1.背景2.方案3.代码中配置t

SpringBoot使用GZIP压缩反回数据问题

《SpringBoot使用GZIP压缩反回数据问题》:本文主要介绍SpringBoot使用GZIP压缩反回数据问题,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录SpringBoot使用GZIP压缩反回数据1、初识gzip2、gzip是什么,可以干什么?3、Spr

如何解决idea的Module:‘:app‘platform‘android-32‘not found.问题

《如何解决idea的Module:‘:app‘platform‘android-32‘notfound.问题》:本文主要介绍如何解决idea的Module:‘:app‘platform‘andr... 目录idea的Module:‘:app‘pwww.chinasem.cnlatform‘android-32

kali linux 无法登录root的问题及解决方法

《kalilinux无法登录root的问题及解决方法》:本文主要介绍kalilinux无法登录root的问题及解决方法,本文给大家介绍的非常详细,对大家的学习或工作具有一定的参考借鉴价值,... 目录kali linux 无法登录root1、问题描述1.1、本地登录root1.2、ssh远程登录root2、

SpringBoot应用中出现的Full GC问题的场景与解决

《SpringBoot应用中出现的FullGC问题的场景与解决》这篇文章主要为大家详细介绍了SpringBoot应用中出现的FullGC问题的场景与解决方法,文中的示例代码讲解详细,感兴趣的小伙伴可... 目录Full GC的原理与触发条件原理触发条件对Spring Boot应用的影响示例代码优化建议结论F