2015 Fiscal Year Annual Research Report
| Project/Area Number |
15J05414
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
黒川 英徳 神戸大学, システム情報学研究科, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2015-04-24 – 2018-03-31
|
| Keywords | 構成の理論 / 直観主義 / 証明論 / 下部構造論理 / 様相論理 / 証明論理 / 証明論的意味論 |
|---|
| Outline of Annual Research Achievements |
本研究では，「構成の理論」という，直観主義数学の中で使用される証明概念を理論化しようとした理論を研究することにより，直観主義における証明概念についての理解を深めることを目的としている．また様々な非古典論理の証明体系，証明論理と呼ばれる論理体系を研究し，それらにおいて扱われる証明概念と，この構成的証明の概念を比較することを通じて，構成的証明の概念と形式的証明概念の関係について考察することも目的としている．
この目的に照らした場合の成果としては，構成の理論に関しては，平成２７年以前に得られていた成果が，論文集の中の１冊として平成２７年度中に刊行された．直観主義における構成的証明概念の意図された解釈を理論化する目的で作られた構成の理論は，ある種の自然な前提の下で矛盾することがかつて示された（クライゼルーグッドマンのパラドックス）．この論文では，この矛盾を回避するため既存の方法よりも自然な手法によってこの矛盾を回避することが可能であるということを哲学的な議論によって示した．これにより，構成的証明の概念に関する認識について一定の進歩が得られたと考えられる．また，非古典論理の証明論については，それらの証明体系の望ましい性質の幾つかを証明することに成功した．この点では研究目的に直接関係する，これから行う哲学的な考察の材料について一定の成果が得られたと言える．
具体的な研究実施計画に照らした成果については，平成２７年度中この研究の成果を受け，この理論について実際に無矛盾性証明を与えることを目指したが，現在のところその証明の基本方針を得るという成果を得るにとどまっている．構成の理論に関する直観主義論理の健全性，完全性についても状況は同じである．
他の証明体系の研究では，下部構造論理と呼ばれる論理の幾つかの性質を証明した．それらの成果は平成２７年度中にすでに幾つかの研究集会で発表された．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
現在までの進捗状況は以下の通りである．まず全般的な状況としては，当初予定していたよりも本研究の目標を達成すること自体は遅れている．これには幾つかの理由がある．まず，研究全体に関わることとして，当初研究計画の予定に必ずしも入っていなかったが，本研究の課題と密接に関係した課題に平成２７年中に関わったということがある．このため，当初予定していたよりも本研究に使える時間が少なかったということが挙げられる．こうした研究には，真理論に関するサーヴェイ論文を書くという課題，ダメットの「無際限拡張可能性」に関する研究，不動点演算子をもつ様相論理の研究，等がある．しかし，これらの研究は将来，本研究の課題と密接に関わってくる可能性が高いため，必ずしも時間を無駄にした訳ではない．
また「構成の理論」においては，その無矛盾性を証明するために，当初想定していたよりも多くの予備知識が必要であるということが判明し，現在その必要な知識を身につけている最中である．Nested sequents を使った，「論理定項とは何か」という問題についての研究でも，やはり当初の予定になかった理論を視野に入れる必要が出て来たという点ではこの場合と同様である．「下部構造論理」の研究においては，研究途中で得られたと思われる証明に誤りを発見したことにより，誤った証明を修正しなければならなかった．こうした事情が若干研究の進捗を遅らせることとなった．しかしながら，現在のところ，当初の想定を完全に覆すような数学的事実が得られているわけではなく，最終的には当初の目標とそれほど違わない成果を得るのは不可能ではないと思われる．
|
| Strategy for Future Research Activity |
今後の研究においては，次の点に特に強調点をおいて研究を推進する予定である．まず「構成の理論」については，上で述べた，当初予期していなかった予備知識の必要性に鑑み，必要な最低限の知識（型なしラムダ計算の特殊なリダクションについての知識，算術化された完全性定理についての知識）を早急に身につけ，その上で構成の理論の無矛盾性，直観主義論理の構成の理論に関する健全性，完全性を証明する．つまり，当面は技術的な成果を得ることに集中する．
また本研究の目標とする主定理の一つである「グッドマンの定理」を証明するための準備を今年度中に行う．具体的にはこの定理の既存の証明について学説史的な研究を終える．
下部構造論理のラベル付き証明体系の研究については，これまで得られた証明について修正が必要な部分を早急に修正する．その上で，この研究について一本目の論文を準備する．下部構造様相論理とその証明論理による「現実化定理」に関する研究については，現在，他の場合よりもやや大規模な証明の修正が必要であることが分かっているため，それをできるだけ早く仕上げることを目標とする．この修正が完了すれば，この研究は直ちに論文として発表できる段階にある．
Nested sequents を使った，「論理定項とは何か」という問題についての研究では，技術的な成果と，哲学的な議論の両方について研究を推進する．技術的な成果については，一本目の論文にするには十分な程の成果が得られているのだが，分量が多いために時間がかかっている．これを論文にすることを当面の目標とする．さらに哲学的な部分についてはパリ在住の共著者の議論と筆者の議論の関係について細部にわたり同意を得る必要があるため，その部分に強調点をおいて研究をすすめる予定である．
|
Research Products
(13 results)
