Proof-theoretic analysis of KPM
Proof-theoretic analysis of KPM
复制标题
KPM的证明理论分析
DOI：
--
复制
发表时间：
1991
影响因子：
0.3
通讯作者：
M. Rathjen
中科院分区：
文献类型：
--
作者：
M. Rathjen
摘要kpm是集合论的一个子系统，用于形式化递归Mahlo集合。在本文中，我们证明了一定的序数符号系统足以度量kpm的证明理论强度。这涉及到通过无穷微积分RS(M)的迂回，为此我们证明了几个消除定理。的推导可完全消除切割
$$Sigma (L_{omega _1^c } )$$
句子，其中ω1c表示最小非递归序数。这篇论文是独立的，至少从技术的角度来看是这样。
AbstractKPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of
$$Sigma (L_{omega _1^c } )$$
sentences, whereω1c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a technical point of view.