| Project/Area Number |
23K10991
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
藤田 憲悦 群馬大学, 情報学部, 准教授 (30228994)
|
|---|
| Project Period (FY) |
2023-04-01 – 2027-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2026: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2023: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | 直観主義論理 / 代数的意味論 / Kripkeモデル / 決定可能性 / 領域理論 / 代数的モデル / Curry-Howard同型 / Stone双対性 |
|---|
| Outline of Research at the Start |
本研究は，直観主義論理のモデル理論に関するものであり，位相構造に基づくモデルと厳密に対応する代数的モデルの構成を基本的な目標としている．それによって，論理の形式的体系に関する多彩な拡張を統一的かつシンプルに説明できるモデル理論の実現が期待され，そのようにして得られる新たな代数的視点の下で，直観主義論理の証明（更にそこから抽出される計算）に関連する基本概念の分析を試みる．
|
| Outline of Annual Research Achievements |
本研究は，過去に行った「2階直観主義命題論理IPC2の代数的モデルに関する考察」を進展させて，「より強い表現を含む直観主義論理の解釈を可能にする代数的モデルを構築すること」や「新たに得られた意味論の視点から，直観主義論理（更にその証明から抽出される計算）の基本的な特徴を分析すること」を主な目的としている．そして，このような研究全体の目的の中で，2023年度は，①IPC2の決定可能性に関する分析，更には②高階直観主義命題論理IPCωの基本体系に対する近傍モデルの構築を試みた．
①について，IPC2の既存研究の中で広く考察されている形式的体系やKripke意味論に注目すると，殆どの枠組において「その下で定義される証明可能性・恒真性を判定するアルゴリズムは存在しない」といった否定的な特徴が知られている．これに対して，2023年度の考察では，Kripkeモデルの基礎となる可能世界集合や各可能世界に付随するドメインに対して，その濃度と表現可能性に一種の制限を施すと，「制限されたKripke意味論の下では，恒真性を判定するアルゴリズムが存在する」といった肯定的な特徴が得られることが分かった．
②について，IPCωではIPC2に「命題コンストラクタとその量化」に関する推論が追加され，そのように拡張された体系に機能する近傍意味論の枠組は知られていない．その一方で，「IPC2の代数的モデルは代数的領域上に定義される近傍モデルと同等であること」や「命題コンストラクタはカルテシアン閉圏の構造があれば解釈できること」など個々の演算については独立したモデルの枠組が存在する．そこで，これらの事実を踏まえて，新たに「代数的領域を特殊化して得られるカルテシアン閉圏」によってIPCωの近傍モデルの枠組を構築することに着手した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究計画に従って，2023年度は，①2階直観主義命題論理IPC2の決定可能性に関する分析②高階直観主義命題論理IPCωに対する近傍モデルの構築を試みた．
①については，具体的に，IPC2のKripke意味論に基づく恒真性に注目し，「恒真性を判定するアルゴリズムが存在するような論理を規定するKripkeモデルのクラス」を特徴付ける試みを行なった．結果として，そのようなクラスに関する十分条件の一つを（既存研究にはない視点から）与えることができた．このことは，当初期待していた通りの結果であり，研究の進捗状況も概ね順調であると考えている．（得られた結果自体も論文に纏めている段階にある．）
②について，IPCωの体系には「命題に関する演算」と「命題コンストラクタに関する演算」に関連した推論が含まれている．これらに対して，IPC2の近傍モデルにカルテシアン閉圏の構造を付加した枠組を用いて，「前者の演算はIPC2の近傍モデルの構造に従った解釈」「後者の演算はカルテシアン閉圏の構造に従った解釈」を行う意味論の構築に着手している．その結果として，個々の演算に対しては従来の手法に従って解釈の定義を与えることは可能であるが，「両者が共存した際に，2つの解釈の手法の整合性を保つために一定の工夫が必要となる」ことが分かってきた．この点を克服するために，現状では，近傍モデルの定義に幾つかの付加的な構造を要請している．そのような条件の必然性については確認中であるが，考察の初期段階としては十分な知見が得られていると考えている．
|
| Strategy for Future Research Activity |
2024年度は，上記①の結果を纏めて成果発表を行うことと共に，その過程から派生した課題についても考察を進める予定である．具体的には，IPC2の中で扱われる命題演算の組合せの違いが（標準的な形式的体系の下で）証明できる命題の決定可能性に複雑な影響を与えることが知られるようになってきていて，「そのような命題演算の組合せに依存した特徴の差異を意味論の視点から説明すること」や「今回の考察で得られた決定可能な論理を形式的体系の規則として特徴付けること」などが課題となる．これらについて，研究分担者・研究協力者と共に更に考察を進めることを計画をしている．
また，これと並行して，令和2024-25年度にかけては，上記②の考察を進める予定である．現時点では，（カルテシアン閉圏の構造を持つように）代数的領域を特殊化することによって新たな近傍モデルの枠組を与え，その下でIPCωの体系が持つ推論を矛盾なく解釈することができるか有効性を確認している段階である．この確認にある程度の見通しが立った時点で，更に「特殊化の基準を満たす具体的な構造」を領域理論の既存研究の中から見出すことを予定している．その際には，完全性定理を保証することが重要な課題であり，「IPC2の意味論を拡張して，IPCωのカノニカルモデルの構成を行うこと」や「そのようなカノニカルモデルを含むような構造としてモデルを与えること」が具体的な問題となる．
更に，その先にある課題としては，③完全分配代数的束の代数構造を2階型付ラムダ計算の表示的意味論に活用する試みを予定している．
|
Report
(1 results)
Research Products
(6 results)
