我们知道哥德尔完全性定理需要至少在二阶算术语言中陈述,并且可以在二阶算术公理系统WKL0 中被证明。
另一方面,我们不能无限扩大对这部分“元数学”的解释。
一般被认为,下 行的勒文海姆-斯寇伦定理是哥德尔完全性定理证明的推论。
但其证明中使用了某种形式的选择公理。准确地说,在ZF基础之上,针对可数语言的下行的勒文海姆-斯寇伦定理与依赖选择公理(dependent choice,DC)是等价的;而针对任意基数语言的下行的勒文海姆-斯寇伦定理与选择公理等价[11]。
显然, 科里不会承认选择公理是否为真也是他所谓的关于形式系统“元数学”的问题。
二、形式主义对数学实践的影响
笔者在《结构主义是一种有效的数学哲学吗?》中质疑结构主义是有效的数学哲学[12]。
在同样的意义上,形式主义无疑是有效的数学哲学。
希尔伯特的形式主义纲领直面数学工作者的困惑。
无论是希尔伯特本人关于几何的公理化工作,还是一阶谓词逻辑和集合论的公理化,抑或前文提到的根岑和哥德尔关于皮亚诺算术的一致性和相对一致性证明,都是在希尔伯特形式主义纲领启发下的数学工作。
在这个意义上,形式主义的确对数学实践有着积极的影响。
裘江杰在《集合论多宇宙观与形式主义》中认为,元数学“作为对数学的反思性研究”是“形式主义的 重要组成部分”,并且形式主义,尤其是被纳入形式主义框架的集合论多宇宙观有助于为集合论搜寻新公理。
本节中,笔者则试图说明:形式主义者尤其关注的元数学研究恰恰非常依赖超出形式主义的思想和直观;而形式主义对探究集合论新公理的作用是有限的。
的确,当代集合论研究中大量使用力迫法得到的结果都可以写成Con(T)→Con(T+φ)这样的形式。
这种相对一致性结果可以被看作是典型的元数学命题,并且本质上可以在弱如PRA这样的算术公理系统中得到证明。
但实际上,几乎没有集合论工作者是在算术公理系统中工作来发现这些证明的。
一般关于力迫法的直观是构造一个已有集合论宇宙中不存在的泛型(泛型,generic)对象,例如ℵ2 个实数,来 得到满足某个命题的“更大的”集合论宇宙,并称之为力迫扩张(forcingextension)。
按照朴素的单一宇宙观,把集合论宇宙理解成所有集合组成的宇宙,就无法解释何以能够再造出一个在集合论宇宙中不存在的泛型对象。
对此,一般可以借助可数传递模型或力迫语言来解释。
用可数传递模型来解释 Con(T)→Con(T+φ)的力迫法证明,首先假设存在T的可数传递的玩具模型M,由于可数模型上的泛型对象总存在,我们可以证明存在M的力迫扩张M[G]满足T+φ。
在这个解释下,我们处理的只是玩具模型, 无论玩具模型M、泛型对象G还是M的力迫扩张M[G]都真实地存在于我们的宇宙中。
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。