Beklemishev 自主体可证性演算中的可推导性与独立性
逻辑
2020-09-01 v1
摘要
Beklemishev 基于可证性代数的自主扩张引入了 Feferman-Schütte 序数 的序数记号系统。在本文中我们给出逻辑 （括号演算）。 的语言将上述序数记号系统扩展为一种严格正模态语言。因此，与其他可证性逻辑不同， 基于一个自包含的签名，该签名产生一个序数记号系统，而非由先验给定的某个序数所索引的模态。我们证明了所给出的逻辑等价于 ，即 的严格正片段。随后我们基于 定义了一个组合陈述，并证明其在算术超限递归理论 （一种远比皮亚诺算术更强的二阶算术理论）中独立。
引用
@article{arxiv.2008.13445,
title = {Deducibility and Independence in Beklemishev's Autonomous Provability Calculus},
author = {David Fernández-Duque and Eduardo Hermo Reyes},
journal= {arXiv preprint arXiv:2008.13445},
year = {2020}
}