Proof-theoretic investigations on wellfoundedness

2023 Fiscal Year Final Research Report

• Project/Area Number: 19K03599
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 12030:Basic mathematics-related
• Research Institution: The University of Tokyo
• Principal Investigator: Arai Toshiyasu 東京大学, 大学院数理科学研究科, 教授 (40193049)
• Project Period (FY): 2019-04-01 – 2024-03-31
• Keywords: proof theory

Outline of Final Research Achievements

The well ordering principle WOP(g) for a normal function g on ordinals states that whenever a well order X is given, g(X) is also a well order. Its proof-theoretic strength is known to depend on the normal functions g. Proofs of these facts were obtained by showing that WOP(g) is equivalent to a Comprehension Axiom, whose strength has been determined.
We show in general that the proof-theoretic ordinal of WOP(g) is equal to the least fixed point of the normal function g. The key in our proof lies in an extraction of an embedding from derivations of the well-foundedness, and of an extendability of embeddings through an indiscernibility of g-terms in g(X).

Free Research Field

数学基礎論

Academic Significance and Societal Importance of the Research Achievements

整列性原理WOP(g)は証明論において考察するのが極めて自然な原理である. その証明論的強さを正則関数gによらずに一様に与えた学術的意義は小さくない. さらにgの微分g'による整列性原理WOP(g')が「任意に大きいWOP(g)のオメガモデルの存在」と同等であるという事実も示したが, これも逆数学の文脈で意義のある結果である. それらの定理の証明に用いた事実は二つあった.一つは整礎性の証明から埋め込みを抽出すること, 二つ目にその埋め込みのg(X)におけるg-項の識別不可能性を用いた拡張にある. 前者はGentzen-Takeutiの結果から得られるが, 後者は全く新しい観点に基づいている.