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

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

相关文章

SpringBoot启动报错的11个高频问题排查与解决终极指南

《SpringBoot启动报错的11个高频问题排查与解决终极指南》这篇文章主要为大家详细介绍了SpringBoot启动报错的11个高频问题的排查与解决,文中的示例代码讲解详细,感兴趣的小伙伴可以了解一... 目录1. 依赖冲突:NoSuchMethodError 的终极解法2. Bean注入失败:No qu

MySQL新增字段后Java实体未更新的潜在问题与解决方案

《MySQL新增字段后Java实体未更新的潜在问题与解决方案》在Java+MySQL的开发中,我们通常使用ORM框架来映射数据库表与Java对象,但有时候,数据库表结构变更(如新增字段)后,开发人员可... 目录引言1. 问题背景:数据库与 Java 实体不同步1.1 常见场景1.2 示例代码2. 不同操作

如何解决mysql出现Incorrect string value for column ‘表项‘ at row 1错误问题

《如何解决mysql出现Incorrectstringvalueforcolumn‘表项‘atrow1错误问题》:本文主要介绍如何解决mysql出现Incorrectstringv... 目录mysql出现Incorrect string value for column ‘表项‘ at row 1错误报错

如何解决Spring MVC中响应乱码问题

《如何解决SpringMVC中响应乱码问题》:本文主要介绍如何解决SpringMVC中响应乱码问题,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录Spring MVC最新响应中乱码解决方式以前的解决办法这是比较通用的一种方法总结Spring MVC最新响应中乱码解

pip无法安装osgeo失败的问题解决

《pip无法安装osgeo失败的问题解决》本文主要介绍了pip无法安装osgeo失败的问题解决,文中通过示例代码介绍的非常详细,对大家的学习或者工作具有一定的参考学习价值,需要的朋友们下面随着小编来一... 进入官方提供的扩展包下载网站寻找版本适配的whl文件注意:要选择cp(python版本)和你py

解决Java中基于GeoTools的Shapefile读取乱码的问题

《解决Java中基于GeoTools的Shapefile读取乱码的问题》本文主要讨论了在使用Java编程语言进行地理信息数据解析时遇到的Shapefile属性信息乱码问题,以及根据不同的编码设置进行属... 目录前言1、Shapefile属性字段编码的情况:一、Shp文件常见的字符集编码1、System编码

Spring MVC使用视图解析的问题解读

《SpringMVC使用视图解析的问题解读》:本文主要介绍SpringMVC使用视图解析的问题解读,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录Spring MVC使用视图解析1. 会使用视图解析的情况2. 不会使用视图解析的情况总结Spring MVC使用视图

Redis解决缓存击穿问题的两种方法

《Redis解决缓存击穿问题的两种方法》缓存击穿问题也叫热点Key问题,就是⼀个被高并发访问并且缓存重建业务较复杂的key突然失效了,无数的请求访问会在瞬间给数据库带来巨大的冲击,本文给大家介绍了Re... 目录引言解决办法互斥锁(强一致,性能差)逻辑过期(高可用,性能优)设计逻辑过期时间引言缓存击穿:给

Java程序运行时出现乱码问题的排查与解决方法

《Java程序运行时出现乱码问题的排查与解决方法》本文主要介绍了Java程序运行时出现乱码问题的排查与解决方法,包括检查Java源文件编码、检查编译时的编码设置、检查运行时的编码设置、检查命令提示符的... 目录一、检查 Java 源文件编码二、检查编译时的编码设置三、检查运行时的编码设置四、检查命令提示符

Jackson库进行JSON 序列化时遇到了无限递归(Infinite Recursion)的问题及解决方案

《Jackson库进行JSON序列化时遇到了无限递归(InfiniteRecursion)的问题及解决方案》使用Jackson库进行JSON序列化时遇到了无限递归(InfiniteRecursi... 目录解决方案‌1. 使用 @jsonIgnore 忽略一个方向的引用2. 使用 @JsonManagedR