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
|
Project Status |
Completed (Fiscal Year 2023)
|
Budget Amount *help |
¥2,730,000 (Direct Cost: ¥2,100,000、Indirect Cost: ¥630,000)
Fiscal Year 2022: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2020: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2019: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
Keywords | proof theory / 証明論 / 順序数解析 / 整列性 |
Outline of Research at the Start |
整列性というのは、再帰的定義の基本となる原理である。最も簡単なのが自然数の順序だがそれをより大きい順序へ拡張したのが整列順序である。 この整列順序の型が順序数と呼ばれる。順序数解析はこの順序数を通じて、公理系に潜む原理を摘出することをしている。今回の研究は、この順序数解析の道具である順序数そのものに焦点を当てて、それを公理系として捉えて、順序数によりこの公理系を分析する。
|
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).
|
Academic Significance and Societal Importance of the Research Achievements |
整列性原理WOP(g)は証明論において考察するのが極めて自然な原理である. その証明論的強さを正則関数gによらずに一様に与えた学術的意義は小さくない. さらにgの微分g'による整列性原理WOP(g')が「任意に大きいWOP(g)のオメガモデルの存在」と同等であるという事実も示したが, これも逆数学の文脈で意義のある結果である. それらの定理の証明に用いた事実は二つあった.一つは整礎性の証明から埋め込みを抽出すること, 二つ目にその埋め込みのg(X)におけるg-項の識別不可能性を用いた拡張にある. 前者はGentzen-Takeutiの結果から得られるが, 後者は全く新しい観点に基づいている.
|