序数分析
序数分析通过理论无法证明为良序的最小序数来衡量形式理论的强度，为每个理论分配一个精确的证明论序数。
用 PaperMind 寻找选题即将推出Find papers & topics
Tools & resources
Learn & explore
视频即将推出
Definition
一个理论的证明论序数是该理论可以证明其良基性的递归良序的序类型的上确界；序数分析是计算此不变量并用其比较和校准理论的程序。
Scope
本主题涵盖了根岑（Gentzen）使用直到ε₀序数的超限归纳法对算术进行的一致性证明、序数表示系统、作为理论不变量的证明论序数、无穷推导的切消方法，以及算术子系统和可预测理论的分析。
Core questions
- 序数如何衡量算术理论的强度？
- 为什么直到ε₀的超限归纳法能证明算术的一致性？
- 序数表示法是如何定义的，以便能够对其进行有限推理？
- 哪些序数对应于二阶算术的标准子系统？
Key theories
- 根岑一致性证明
- 根岑通过将小于ε₀的序数分配给证明并证明切消会减少这些序数，从而证明了一阶算术的一致性，因此直到ε₀的超限归纳法证明了一致性。
- 证明论序数
- 每个足够强的理论都有一个特征序数，它捕捉了该理论可以证明的超限归纳，提供了一个精细且大致线性的逻辑强度尺度。
- 序数表示系统
- 大序数通过有限的句法表示法来表示，例如维布伦函数（Veblen functions）和折叠函数（collapsing functions），这使得无限序数可以在有限或算术理论中进行操作。
Clinical relevance
序数分析提供了衡量数学理论强度的最精细可用方法：它精确地确定了一个理论需要哪些超限归纳，对一个理论的可证明递归函数进行分类，并提供了与大基数获得的相对一致性信息互补的信息。
History
根岑（Gentzen）在1936年和1938年对算术的一致性证明通过直到ε₀的超限归纳法引入了序数分析。舒特（Schuette）、费弗曼（Feferman）等人将该方法扩展到可预测理论和分层分析，随后折叠函数（collapsing functions）的发展将序数分析推向了强大的非可预测系统。
Key figures
- Gerhard Gentzen
- Kurt Schuette
- Solomon Feferman
- Wolfram Pohlers
Related topics
Seminal works
- pohlers2009
- takeuti1987
- schutte1977
Frequently asked questions
- 一阶算术的证明论序数是多少？
- 它是ε₀，即ω指数塔的极限。一阶算术可以证明直到任何小于ε₀的序数的超限归纳，但不能证明直到ε₀本身的超限归纳，这正是根岑用来证明其一致性的原理。
- 序数分析与不完备性有何关系？
- 哥德尔第二定理指出算术不能证明自身的一致性。序数分析确定了额外的原理，即直到ε₀的超限归纳，它确实证明了这一点，从而精确地衡量了要建立其一致性，必须超越该理论多远。