2023 Fiscal Year Annual Research Report
Project/Area Number |
19K03599
|
Research Institution | The University of Tokyo |
Principal Investigator |
新井 敏康 東京大学, 大学院数理科学研究科, 教授 (40193049)
|
Project Period (FY) |
2019-04-01 – 2024-03-31
|
Keywords | 証明論 |
Outline of Annual Research Achievements |
最終年度には冪集合公理無しの集合論の順序数解析を主に研究していた.研究課題は順序数上の正則関数 g による整列性原理 WOP(g) は「任意の整列集合 X に対してg(X) も整列」という主張であり, 正則関数 g の取り方によりその証明論的強さが異なることが知られていたが, それらの結果は, 既に証明論的強さが既知であったComprehension Axiomなどと WOP(g) が同等であることを通じて得られていた.そこで 一般に, WOP(g) の証明論的順序数は正則関数 g の最小不動点と等しいことを示した.証明の鍵は, 整礎性の証明から埋め込みを抽出すること(これはGentzen-Takeutiの証明から可能であることを示した)及びその埋め込みの, g(X) における g-項の識別不可能性を用いた拡張にある.さらに集合に関する量化子が存在-任意に続く論理式を用いてしか定義できない maximal distinguished setを用いて, 順序数体系の整礎性を証明した. この証明は集合に関する量化子が存在-任意に続く論理式を用いてパラメタ無しで定義できるクラスを集合と認めれば形式化され, また順序数体系はstable ordinalを一つ持つ集合論の順序数解析のためのものである. また2階論理計算の一部 SBLでのカット消去を, 有限の証明図をGentzen-Takeuti流に解析して示した. SBLのカット消去は, 再帰的到達不可能順序数の集合論の1-consistencyと同等である.
|