分类:证明论:修订间差异
外观
无编辑摘要 |
无编辑摘要 |
||
| 第1行: | 第1行: | ||
在数理逻辑的研究中,将问题形式化、公理化成公式, | 在数理逻辑的研究中,将问题形式化、公理化成公式, | ||
并通过公式结构本身(形式、语法,而非内容、语义)的变形规则,对任意一个[[命题]],即语法上的一个公式,寻求一个[[证明]]序列。 | |||
相关理论称为'''证明论'''('''proof theory''')。 | 相关理论称为'''证明论'''('''proof theory''')。 | ||
| 第6行: | 第6行: | ||
试图将数学形式化, | 试图将数学形式化, | ||
通过列举出概念、基本公理、基本推理规则, | 通过列举出概念、基本公理、基本推理规则, | ||
确认数学体系的[[完备性]]、[[一致性]],理论上即等价于一切的命题都可以在这个形式化系统中以有穷序列可证为真或假。 | 确认数学体系的[[完备性(逻辑)|完备性]]、[[一致性]],理论上即等价于一切的命题都可以在这个形式化系统中以有穷序列可证为真或假。 | ||
后被证明,任意一个包含一阶谓词逻辑与初等数论的形式系统,都存在不能在这一系统中证明真假的命题; | 后被证明,任意一个包含一阶谓词逻辑与初等数论的形式系统,都存在不能在这一系统中证明真假的命题; | ||
一个包含初等数论且一致的系统,不能从系统本身中证明其一致性。 | 一个包含初等数论且一致的系统,不能从系统本身中证明其一致性。 | ||
2025年12月11日 (四) 08:39的版本
在数理逻辑的研究中,将问题形式化、公理化成公式, 并通过公式结构本身(形式、语法,而非内容、语义)的变形规则,对任意一个命题,即语法上的一个公式,寻求一个证明序列。 相关理论称为证明论(proof theory)。
其中代表性、知名度高的是希尔伯特纲领(Hilbert's program)。 试图将数学形式化, 通过列举出概念、基本公理、基本推理规则, 确认数学体系的完备性、一致性,理论上即等价于一切的命题都可以在这个形式化系统中以有穷序列可证为真或假。 后被证明,任意一个包含一阶谓词逻辑与初等数论的形式系统,都存在不能在这一系统中证明真假的命题; 一个包含初等数论且一致的系统,不能从系统本身中证明其一致性。 这被称为哥德尔不完备定理(Gödel's incompleteness theorems)。