Revisiting ordinal notation systems in proof theory: from the viewpoint of linear logic
| Project/Area Number |
21K12822
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 01010:Philosophy and ethics-related
|
|---|
| Research Institution | Ochanomizu University |
|---|
Principal Investigator |
高橋 優太 お茶の水女子大学, 文理融合 AI・データサイエンスセンター, 特任助教 (70826990)
|
|---|
| Project Period (FY) |
2021-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2025: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2024: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2023: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2022: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 型理論 / 項書換え / 証明論 / 順序数 / 論理学の哲学 / 数学の哲学 / 数学基礎論 |
|---|
| Outline of Research at the Start |
数理論理学の一分野である証明論は、数学における証明を抽象化した上で「証明の大きさ」の概念を数学的に定義し、小さいものから順に際限なく構成されるものとして証明を捉える。そして、この観点のもとで数学における無限を解明しようとする。しかし、ここでいう「構成」とは何なのかという問いは数学の中だけで扱えるものではなく、この問いを探究するためには哲学的研究も必要になる。本研究は、同じく数理論理学の一分野である線形論理がもたらす相互作用という観点を援用し、この問いに取り組む。以上の探究を通して、数学における無限およびそれを捉える人間の論理的思考を解明し、その成果を情報科学などの他分野へ応用することを目指す。
|
| Outline of Annual Research Achievements |
19世紀末に創始された数理論理学は、完成した集まりとして無限を扱う実在論と、際限なく続くプロセスとして無限を扱う反実在論という二つの立場に厳密な数学的定式化を与えた。特に、数理論理学の一分野である証明論は、順序数表記系と呼ばれる数体系を導入し、公理系の中の形式的証明を順序数に対応付けることで、その公理系がどの程度の反実在論を表現しているのかについての尺度を与えた。一方で、同じく数理論理学の一分野である線形論理は、形式的証明をゲームの枠組みの中で捉える観点をもたらした。本研究の目的は、線形論理がもつゲーム的・言語行為的観点から、形式的証明を順序数に対応づける従来の証明論的反実在論を反省し分析することである。
本年度は、順序数とゲームを共存させることのできる枠組みとして型理論に着目し、それについて研究することで次年度以降の研究の準備を行なった。まず、項書換え系と呼ばれる計算規則を単純型付きラムダ計算に加えたときに計算の停止性が保存される条件について研究した。このことを通して、プログラミング言語の一種でもある型理論の計算的側面を探究した。
次に、マーティン・レーフ型理論の中で、ユニバース型と呼ばれるデータ型の構成を際限なく繰り返すことのできる演算子を定式化した。ユニバース型からは順序数と類似した構造をもつデータを構成できるため、この演算子の定義を通して、型理論の中で順序数を際限なく構成するアプローチを模索した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
前年度は線形論理におけるゲームの研究を進めることができたのに対し、本年度は、順序数表記系とゲームを共存させることのできる枠組みである型理論の研究に進捗があったことが主な理由である。特に、項書換え系を単純型付きラムダ計算に加える研究を、1本の査読付き英語論文にまとめることができた。また、マーティン・レーフ型理論についての研究を手がかりに、順序数表記系と線形論理の研究の統合に関してもアイデアを得ることができた。
|
| Strategy for Future Research Activity |
次年度は、前年度と同様に、順序数表記系の研究と線形論理の研究を並行して進展させるという課題を主軸とする。さらに、本年度に得られた着想をもとに、これらの研究の統合を視野に入れて研究活動に従事する。
|
Report
(2 results)
Research Products
(8 results)
