| 研究課題/領域番号 |
25330013
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2019-03-31
|
| キーワード | 部分構造論理 / 代数的証明論 / MacNeille完備化 / 抽象代数論理 / 橋渡し定理 |
|---|
| 研究実績の概要 |
これまで取り組んできた証明論への代数的アプローチが、単に部分構造論理をはじめとする非古典論理だけでなく、普通の論理（高階古典論理、高階直観主義論理）や二階算術における伝統的証明論の問題に適用できることを見出した。具体的には、パラメータを含まない二階算術のカット除去を示すために伝統的に用いられてきたBuchholzのオメガ規則が、代数的証明論の核心にあるMacNeille完備化により基礎づけられることを示した。リンデンバウム代数上に限っていえば、オメガ規則が直観主義論理の代数的意味論において健全なのは、MacNeille完備化の場合に限られることを示し、またオメガ規則が一般には偽になることを示す反例を与えた。これらの結果により前原・岡田の代数的カット除去証明法がパラメータを含まない場合にスケールダウンできて、帰納的定義の有限回の繰り返しのみを許す算術の体系で形式化可能なことを示した。これらの洞察は、膨大な歴史と文献により裏付けられた伝統的証明論に対して、新しく代数的アプローチを提示するものとして重要である。成果は国際学会MLA 2018で発表し、論文を投稿済である。
その他の成果として、抽象代数論理における一連の「橋渡し」定理の分析を行った（たとえば論理が局所演繹性を持つことと、対応する代数のクラスが合同拡張性を持つことの一致など）。橋渡しの本質は、論理のtheoryからなる圏とそれに対応する代数がなす圏の間にある関手の存在に集約される。この洞察に基づいて一連の橋渡し現象に見通しのよい説明を与え、論理におけるRobinson性や局所演繹性、性質のよいメタ選言を持つための条件に対して新しい特徴づけを与えた。成果は現在投稿準備中である。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
4: 遅れている
理由
健康問題が最大の理由である。健康問題ゆえに多くの時間をとられ、また予定していた学会出張や研究訪問を中止せざるをえなかった。また代数的証明論はよいとして、本研究のもう１つの眼目であるラムダ計算の共通型については、ほとんど進展がみられなかった。その理由は、問題自体の難しさにある。これまで高階マッチングの決定問題に集中して研究を進めてきたが、方針転換してもう少し研究範囲を拡げたほうがよいのかもしれない。
|
| 今後の研究の推進方策 |
筆者が推進してきた証明論への代数的アプローチが実は伝統的証明論の問題意識と通底しているというのは、大きな発見であった。今後は（膨大な先行研究をもつ）伝統的証明論への関与を深め、代数的アプローチにより既存の結果がどこまで説明可能なのか、新しい結果を得ることは可能なのかを探っていきたい。もう1つの発見として、矛盾許容論理で取り扱われるKleeneの3値意味論が、実は意味論的カット除去の背後にあるSchutteの3値意味論と同一だということが挙げられる。この知見により、矛盾許容論理と代数的証明論を結びつける方向性が自然に開かれる。今後は矛盾許容論理の研究者とも対話を深め、代数的証明論のアプローチを多方面に展開していきたいと思っている。
|
| 次年度使用額が生じた理由 |
健康上の理由により、予定していた国外出張をいくつかキャンセルせざるを得なかった。研究期間を1年間延長したうえで、研究成果発表のための出張旅費として用いる予定である（2018年9月に英国で開催される国際会議Computer Science Logic 2018に参加予定）。
|
