Solovay 关于 FIM 与 BI 的相对一致性证明
逻辑
2021-01-18 v1 历史与综述
摘要
2002 年，Robert Solovay 证明了经典二阶算术的一个子系统 BI（带杆归纳与算术可数选择）可以利用马尔可夫原理 MP，在 Kleene 直觉主义分析 FIM 的中性子系统 BSK 中作否定解释。将此结果与 Kleene 形式化递归实现相结合，他在原始递归算术 PRA 中确立了 FIM + MP 与 BI 具有相同的相容性强度。本历史注记经其许可收录了 Solovay 的原始证明，并补充了一个观察：马尔可夫原理可弱化为与 Brouwer 创造主体反例相容的双重否定移位公理。
引用
@article{arxiv.2101.05878,
title = {Solovay's Relative Consistency Proof for FIM and BI},
author = {Joan Rand Moschovakis},
journal= {arXiv preprint arXiv:2101.05878},
year = {2021}
}