| Project/Area Number |
20K03712
|
|---|
| 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 | Tokyo Institute of Technology |
|---|
Principal Investigator |
鹿島 亮 東京工業大学, 情報理工学院, 准教授 (10240756)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2024: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2020: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 様相論理 / 証明可能性論理 / ２階型付けラムダ計算 / 完全性 / 中間論理 / ２階論理 / 命題論理 / 非古典論理 |
|---|
| Outline of Research at the Start |
中間論理とは直観主義論理よりも強く古典論理よりも弱い論理体系の総称である。それらは使用する論理記号によって (1) 中間命題論理、(2) 中間１階述語論理、(3) 中間２階命題論理、(4) 中間２階述語および中間高階述語論理に分類される。(1,2)はすでに多く研究されているが(3)や(4)の研究は今までほとんどなされていなかった。その研究を立ち上げ、博士課程学生や学外の研究協力者とともに推進していく。
|
| Outline of Annual Research Achievements |
本研究課題である中間2階命題論理はクリプキモデルに様々な条件を加えることで得られる論理であるが、クリプキモデルを用いる論理の研究の一般論が様相論理の研究である。すなわち中間2階命題論理の研究は様相論理の研究の特殊例とみなすことができる。現在、中間2階命題論理の当初計画していた研究はやや行き詰まっているので、より広い視点で様相論理の研究に重点を置いて研究を進めている。具体的には次の2つである。
(1)証明可能性論理(算術の証明可能性述語に対応する様相記号を持つ論理)について。これについては次の2つの成果を得た。(1-1) 証明可能性論理Dのシンプルなシークエント計算体系を2つ作り上げそれらのカット除去定理を証明した。この結果は2023年10月に開催された国際会議 17th Asian Logic Conference で発表するとともに、論文誌に投稿中である。(1-2) 証明可能性論理GLの入れ子シークエント計算の構文論的カット除去をシンプルに示した。GLは証明可能性論理の基本中の基本でありカット除去についても今までの多くの研究があるが、それに対して新しい成果を示した。この結果は2024年秋に開催される国際会議に投稿中である。
(2)様相ミュー計算の完全性について。様相ミュー計算は様相論理に不動点演算子を加えたもので、幅広い応用を持つ重要な論理である。この論理の証明体系の完全性はWalukiewicz(2000)によって示されているが、その証明は難解であり改良が期待されている。本研究でもこれに取り組みんでいるが、残念ながら2023年度には外部に発表できる実績は得られなかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
計画策定時の見込み違いにより中間2階命題論理の性質が当初想定したものとやや異なることがわかり、当初やろうと思っていたことがあまりうまくできないことがわかってきた。これをどう回避するかは検討中である。
一方、より幅広い視点で様相論理の研究に取り組み、特に証明可能性論理のシークエント計算について良い成果を複数得ている。
|
| Strategy for Future Research Activity |
以下の3つのテーマについて研究を進める。
(1)証明可能性論理のカット除去の研究。証明可能性論理の従来の研究は算術の証明可能性に紐づいているが、その縛りから離れて純粋に「クリプキモデルのクラスで特徴付けられる論理」として研究を発展させる。また証明可能性論理のカット除去はカリーハワード対応によって計算の再帰呼び出しに対応すると考えることもできるので、その視点での研究を発展させる。
(2)様相ミュー計算の研究。2024年秋から受け入れ予定の学振外国人特別研究員との共同研究によって様相ミュー計算の証明体系の完全性の簡潔な証明を目指す。
(3)中間2階命題論理について、当初の見込みを適切に修正し研究を軌道に乗せる。
|
