2021 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世紀末に創始された数理論理学はこれら二つの立場に厳密な数学的定式化を与えた。数理論理学の一分野である証明論は、順序数表記系と呼ばれる順序数の記号体系を構成し、公理体系内の形式的証明をこうした記号体系に対応づけることで、公理体系がどの程度の反実在論を表現しているのかについての尺度を導入した。一方で、同じく数理論理学の一分野である線形論理は、形式的証明をゲームの枠組みの中で捉える観点をもたらした。本研究の目的は、線形論理がもつゲーム的・言語行為的観点から、形式的証明を順序数に対応づける従来の証明論的観点を反省し、反実在論に対する証明論的定式化を分析することである。
本年度の主要な研究実績としては、形式的証明をゲームの枠組みの中で捉えるという線形論理のアイデアについての研究が挙げられる。このアイデアを具体化する体系である計算ルディクス(Computational Ludics)に着目し、証明論的意味論と呼ばれる論理哲学の理論との関係を調べた。証明論的意味論とは、推論実践に基づいて言語表現の意味を説明する理論である。特に、計算ルディクスの中に見られるゲームの概念と証明論的意味論の調和概念とを接続し、線形論理がもつゲームの概念を推論実践の観点から理解することを試みた。このことを通して、線形論理がもつ言語行為的観点の分析に取り組んだ。
|
| 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 |
次年度も、順序数表記系の研究と線形論理の研究を並行して進展させるという課題を主軸としつつ、これらの研究の統合を視野に入れて研究活動に従事する。
|
| Causes of Carryover |
当初計画していた海外研究出張を取りやめたため、次年度使用額が生じた。次年度分の助成金は当初の予定通り使用する。次年度使用額は、本研究を計算機科学分野と接続するためのプログラミング用PCの購入に用いる予定である。
|
