2023 Fiscal Year Research-status Report
Revisiting ordinal notation systems in proof theory: from the viewpoint of linear logic
| Project/Area Number |
21K12822
|
|---|
| Research Institution | Ochanomizu University |
|---|
Principal Investigator |
高橋 優太 お茶の水女子大学, 文理融合 AI・データサイエンスセンター, 特任助教 (70826990)
|
|---|
| Project Period (FY) |
2021-04-01 – 2026-03-31
|
| Keywords | 型理論 / 証明論 / 順序数 / 構成的集合論 |
|---|
| Outline of Annual Research Achievements |
19世紀末に創始された数理論理学は、閉じて完成している集まりとして無限を扱う実在論と、際限なく続く開いたプロセスとして無限を扱う反実在論という二つの立場に厳密な数学的定式化を与えた。特に、数理論理学の一分野である証明論は、順序数表記系と呼ばれる数体系を導入し、公理系の中の形式的証明をこの表記系の中の数に対応付けることで、当の公理系を反実在論的立場から解釈する方法を与えた。一方で、同じく数理論理学の一分野である線形論理は、形式的証明をゲームの観点から捉える数学的・概念的枠組みを証明論にもたらした。この枠組みにおいては、ゲームにおけるエージェントどうしの相互作用に焦点が当てられ、ここでの相互作用は言語行為を介するものとみなすこともできる。
本研究の目的は、線形論理がもつこのゲーム的・言語行為的観点から、形式的証明を順序数に対応づける従来の証明論的反実在論を反省し分析することである。
本年度は、前年度に引き続き、順序数とゲームを共存させることのできる枠組みとして型理論に着目し、特にマーティン・レーフ型理論(MLTT)に関する研究を行なった。前年度に従事した、ユニバース型と呼ばれるデータ型の構成についての研究を発展させ、構成的集合論(constructive set theory)をMLTTへと埋め込む試みに着手した。構成的集合論は反実在論の立場に基づく集合論であり、順序数を集合の一種として捉える点は古典的集合論と変わらないが、構成的集合論においては、集合から成る無限領域は際限なく構成されるプロセスとして捉えられる。こうした構成的集合論にさらに巨大集合に関する公理を加えることで得られる集合領域を、対応するユニバース型の構成をさらに強力にすることでMLTTに埋め込む方法を精査し、新たな方法につながる部分的な成果を得ることができた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度は、線形論理がもたらすゲーム的観点についての研究は行なえなかったものの、構成的集合論とMLTTとの関係性を精査することで集合一般の反実在論的な理解を深められたことが主な理由である。前述の通り集合論において順序数は集合の一種となるため、本年度の成果は、証明論における順序数表記系をMLTTの中で構成する際に新たな知見を提供しうる。
また、MLTTの中で順序数表記系をゲーム的観点から構成している先行研究の手法は、MLTTを代数的に定式化する枠組みに基づくものであるが、この枠組みについてのサーベイも進めることができた。
|
| Strategy for Future Research Activity |
次年度からは、本年度までに蓄積した線形論理に関する研究および型理論に関する研究に基づき、MLTTの中で順序数表記系を線形論理的方法でもって構成する研究に着手する。そのためにまず、MLTTの中で順序数表記系をゲーム的観点から構成している前述の先行研究の成果を線形論理的方法により分析する。特に、この先行研究におけるゲームの概念と線形論理におけるゲームの概念とを比較し、前者を後者によって捉えることができるかどうか精査する。
以上に加え、線形論理分野での最先端の研究もサーベイし、本研究課題の構想時にはなかったアイデアおよび観点を加えることを試みる。
|
