GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN?P?TER FUNCTION
GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN?P?TER FUNCTION
复制标题
基于参数化 ACKERMANN?P?TER 函数的古斯坦序列
DOI：
10.1017/bsl.2021.30
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
WEIERMANN ANDREAS
中科院分区：
文献类型：
--
作者：
ARAI TOSHIYASU;WAINER STANLEY S.;WEIERMANN ANDREAS
在我们的[6]之后，虽然这里的方法有些不同，但Goodstein序列的进一步变体是根据参数化的Ackermann-Péter函数引入的。每个序列的终止，并校准这些事实的证明理论的强度通过序数分配，产生一系列的理论：PRA，PA，-DC，ATR，ID的独立结果。关键是所谓的“哈代层次”的证明理论的边界函数，提供了一个统一的方法，将古德斯坦型序列与参数化的正规形式表示的正整数。
Following our [6], though with somewhat different methods here, further variants of Goodstein sequences are introduced in terms of parameterized Ackermann–Péter functions. Each of the sequences is shown to terminate, and the proof-theoretic strengths of these facts are calibrated by means of ordinal assignments, yielding independence results for a range of theories: PRA, PA, -DC , ATR , up to ID . The key is the so-called “Hardy hierarchy” of proof-theoretic bounding finctions, providing a uniform method for associating Goodstein-type sequences with parameterized normal form representations of positive integers.