重访 Goodstein

受 Gentzen 1936 年一致性证明的启发，Goodstein 发现了序数 $\epsilon_0$ 的递减序列与整数序列（现称为 Goodstein 序列）之间的紧密对应关系。本文重访了 Goodstein 1944 年的论文。结合在 Bernays 与 Goodstein 的通信中发现的新历史细节，我们探讨了 Goodstein 距离证明 PA 的独立性结果有多近。我们还给出了一个初等证明，表明所有特殊 Goodstein 序列（即由移位函数诱导的序列）的终止性在 PA 中不可证。这一事实最早由 Kirby 和 Paris 于 1982 年利用算术模型论技术证明。此处提出的证明仅使用了可能在 1940 年代或 1950 年代就已具备的工具。因此我们思考：显著的独立性结果是否本可以更早被证明？同样，我们也怀疑在 1970 年代末之前，寻找 PA 中不完全性的严格数学实例是否真的达到了其“圣杯”地位。文章几乎未给出直接的道德结论；相反，它致力于罗列证据供读者考量，让读者形成自己的结论。然而，就独立性结果而言，我们认为 Goodstein 和 Gentzen 都值得获得更多的赞誉。