AI 中文总结
本文解决了阿克曼式Goodstein原理的两个问题，证明基于阿克曼函数的任何Goodstein过程都终止，得到了不依赖范式的等价原理，为终止性证明提供了新方法。
AI 中文摘要
Goodstein定理指出，基于自然数指数表示的特定序列总是有限的。该结果独立于皮亚诺算术（Peano arithmetic），是通过超限归纳法证明终止性的典型例子。Arai等人最近提出了基于阿克曼函数（Ackermann function）的变体，该变体独立于更强大的理论$\sf ATR_0$。然而，这一结果依赖于基于“夹逼”过程的相当复杂的自然数范式。这留下了两个问题：一是在保留阿克曼式Goodstein原理全部强度的同时，能否消除夹逼过程；二是其他范式是否会导致非终止。在本文中，我们通过证明基于阿克曼函数的**任何**Goodstein过程都是终止的，且夹逼过程会产生具有最大长度的Goodstein原理，解决了这些问题。我们因此得到了一个完全不涉及范式的等价原理，它直接蕴含了所有已研究的阿克曼式Goodstein原理。我们的技术提供了一种新的终止性证明方法，其中序列中的项不一定在复杂性上递减，而是被某些已知终止的“主”过程所控制。
英文摘要
Goodstein's theorem states that a certain sequences based on exponential notation for the natural numbers are always finite. The result is independent of Peano arithmetic and is a prototypical example of a proof of termination by transfinite induction. A variant based instead on the Ackermann function has more recently been proposed by Arai et al., and instead is independent of the more powerful theory ${\sf ATR}_0$. However, this result is contingent on rather elaborate normal forms for natural numbers based on a `sandwiching' procedure. This leaves open both the question of whether the sandwiching procedure can be eliminated while retaining the full strength of the Ackermannian Goodstein principle, and whether other normal forms can lead to non-termination. In this article we settle these questions by showing that {\em any} Goodstein process based on the Ackermann function is terminating, and indeed the sandwiching procedure gives rise to Goodstein principles of maximal length. We thus obtain an equivalent principle which does not involve normal forms at all and immediately implies all Ackermannian Goodstein principles that have been considered. Our techniques provide a new approach to termination proofs, where terms in a sequence do not necessarily decrease in complexity, but instead are majorized by some ``master'' process, already known to be terminating.
