Ω-规则的分析与扩展
逻辑
2011-03-15 v2
摘要
W. Buchholz 引入了 Ω-规则，以给出一个包含 Π¹₁-概括的分析子系统的无序数切割消除证明。他的证明仅对算术序列提供了通过熟悉规则的无切割推导。当存在二阶量词时，它们由 Ω-规则引入，并且一些残余切割未被消除。使用 Ω-规则的扩展，我们（通过与 W. Buchholz 相同的方法）获得了完全的切割消除：任意序列的任何推导都被转化为其通过标准规则（用 ω-规则替代归纳）的无切割推导。W. Buchholz 使用 Ω-规则来解释有限推导的归约（由 G. Takeuti 用于分析子系统）是如何通过应用于带有 Ω-规则的推导的切割消除步骤生成的。我们表明，相同的步骤生成了带有二阶量词熟悉标准规则的无穷推导的标准切割归约步骤。这提供了用标准规则对 Ω-规则的分析，以及带有二阶量词标准规则系统的无序数切割消除证明。事实上，我们处理了 W. Buchholz 用于解释有限归约的 Π¹₁-CA 子系统（与 ID₁ 强度相同）。扩展到完整的 Π¹₁-CA 将在另一篇论文中给出。
引用
@article{arxiv.0904.4742,
title = {Analysis and Extension of Omega-Rule},
author = {R. Akiyoshi and G. Mints},
journal= {arXiv preprint arXiv:0904.4742},
year = {2011}
}