順序数解析

順序数解析は、理論が整列順序であることを証明できない最小の順序数によって形式理論の強度を測定し、各理論に正確な証明論的順序数を割り当てる。

Definition

理論の証明論的順序数とは、その理論が整礎性を証明できる再帰的整列順序の順序型の最小上界である。順序数解析とは、この不変量を計算し、それを用いて理論を比較・較正するプログラムである。

Scope

このトピックでは、順序数イプシロン・ゼロまでの超限帰納法を用いたゲンツェンの算術の無矛盾性証明、順序数表記体系、理論の不変量としての証明論的順序数、無限導出に対するカット除去法、算術の部分体系および述語論理的理論の解析について扱う。

Core questions

• 順序数は算術理論の強度をどのように測定するのか？
• なぜイプシロン・ゼロまでの超限帰納法が算術の無矛盾性を証明するのか？
• 順序数表記は、有限的に推論できるようにどのように定義されるのか？
• 二次算術の標準的な部分体系に対応する順序数は何か？

Key theories

ゲンツェンの無矛盾性証明

ゲンツェンは、イプシロン・ゼロ未満の順序数を証明に割り当て、カット除去がそれらを減少させることを示すことで、一階算術の無矛盾性を証明した。これにより、イプシロン・ゼロまでの超限帰納法が無矛盾性を保証する。

証明論的順序数

十分に強力な各理論は、それが正当化できる超限帰納法を捉える特徴的な順序数を持ち、論理的強度のきめ細かく、ほぼ線形な尺度を提供する。

順序数表記体系

大きな順序数は、ヴェブレン関数や崩壊関数などの有限な構文表記によって表現され、無限の順序数を有限または算術的理論内で操作することを可能にする。

Clinical relevance

順序数解析は、数学的理論の強度を測定する上で最も洗練された手段を提供する。これにより、理論が必要とする超限帰納法を正確に特定し、理論の証明可能な再帰関数を分類し、巨大基数から得られる情報とは相補的な相対的無矛盾性情報を提供する。

History

ゲンツェンによる1936年および1938年の算術の無矛盾性証明は、イプシロン・ゼロまでの超限帰納法を通じて順序数解析を導入した。シュッテ、フェファーマンらはこの方法を述語論理的理論や分岐解析に拡張し、後に崩壊関数の発展により、順序数解析は強力な非述語論理的体系へと進展した。

Key figures

• Gerhard Gentzen
• Kurt Schuette
• Solomon Feferman
• Wolfram Pohlers

Seminal works

• pohlers2009
• takeuti1987
• schutte1977

Frequently asked questions

一階算術の証明論的順序数とは何か？

それはイプシロン・ゼロであり、オメガ指数関数の塔の極限である。一階算術はイプシロン・ゼロ未満の任意の順序数までの超限帰納法を証明できるが、イプシロン・ゼロ自体までは証明できない。これはゲンツェンがその無矛盾性を証明するために用いた原理と全く同じである。

順序数解析は不完全性定理とどのように関連しているか？

ゲーデルの第二不完全性定理は、算術が自身の無矛盾性を証明できないことを示している。順序数解析は、それを証明する追加の原理、すなわちイプシロン・ゼロまでの超限帰納法を特定し、それによって理論の無矛盾性を確立するために、理論をどれだけ超える必要があるかを正確に測定する。