Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic
Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic
复制标题
形式化二阶算术子系统中的强制论证
DOI：
10.1016/0168-0072(96)00003-6
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
J. Avigad
中科院分区：
文献类型：
--
作者：
J. Avigad
我们证明，涉及二阶算术子系统的某些模型理论强制论证可以在基础理论中形式化，从而将它们转换为有效的证明理论论证。我们使用这种方法来锐化Harrington和Brown-Simpson的守恒定理，有效证明WKL+0相对于RCA0是保守的，并且证明长度没有显着增加。
We show that certain model-theoretic forcing arguments involving subsystems of second-order arithmetic can be formalized in the base theory, thereby converting them to effective proof-theoretic arguments. We use this method to sharpen the conservation theorems of Harrington and Brown-Simpson, giving an effective proof that WKL+0is conservative over RCA0with no significant increase in the lengths of proofs.