2016 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 |
本研究における主要な研究目標は，直観主義論理の基礎理論となる「構成の理論」の再構成である．本年度は，その再構成のプロセスにおいて最も重要な意味を持つ「構成の理論」の或る定式化における無矛盾性を証明することを課題とした．この大きな目標は現在のところまだ達成されていないものの，その証明の手法について，いくつかの洞察を得ることができた．具体的には，無矛盾性証明の手法について具体的な候補をいくつかに絞り込むことができた．
また本研究では，本研究の概念的な目標である，構成的な証明概念の解明ということに関して，必ずしも「構成の理論」そのものには直接関わらない，本研究における言わば下位目標をいくつか定めている．こうしたものとしては，様々な非古典論理に関する証明論的研究を行うこと，また（数学的真理，また構成的証明などを含む）ある種の数学的概念の無際限拡張可能性という概念を解明することなどを挙げてきた．これらの主題については，幾つかの非古典論理の証明体系（何らかの形で拡張されたシークエント計算）に関する証明論的研究について，具体的にはカット除去定理の証明に関し，研究の進展があった．また，無際限拡張可能性に関しても，哲学者ダメットによる不完全性定理の意義に関する論文の解釈について，以前よりも見通しのよい解釈を得るに至った．「論理定項とは何か」についての証明論的意味論の観点からの研究については，stabilityという概念について以前よりも認識が多少深めることができるに留まった．
また本研究で扱う構成的な証明概念の解明を２階あるいは高階のそれへと拡張するというさらなる問題を得た．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
本研究の最大目標である「構成の理論」の再構成に関して言えば，その「構成の理論」そのものの無矛盾性証明が我々が当初想定していたよりも困難であるということが分かったということが，研究が思っていたよりも遅れている最大の要因である．ニコラス・グッドマンの博士論文が「構成の理論」における最も詳細な内容を含む文献なのだが，この中の無矛盾性証明をまず理解するために，１９６０年代によく読まれていたラムダ計算に関する文献を参照せねばならず，さらにその証明を現代的に再構成するためには，そこで使われている手法をもう一度現代的に（ただし必ずしも標準的とは言えない仕方で）再構成する必要がある．現在，我々はこの課題を実行している途上であり，この課題に成功するまでは，この研究にはまだ相当な困難が存在すると予想される．
その他の課題に関して言えば，証明を得ること，あるいは議論を進めること自体にはそれなりに進展をみている．とはいえ，出版戦略の上からできるだけ多くの成果を統一的に発表しようとする意図から，あるいは共著者との時間のすり合わせが難しいということから，成果の発表が遅れている．
|
| Strategy for Future Research Activity |
本研究の今後の推進方策に関して言うと，これまでの方針を大幅に変更する必要は認められない．初期の目標を達成するためには，とにかく「構成の理論」において，その無矛盾性証明を与えることが現時点において最重要課題であるため，そこに重点を置くことになる．その際，我々が現在直面している困難を考慮し，歴史的な文献中で使われている無矛盾性証明の再構成以外に，これまでになかった点として，より洗練された手段によっても無矛盾性を証明することによって，結果の正しさをさらに説得的にするという手法を付け加える．矛盾性を証明した後，タイプ付き算術の体系に選択公理を付け加えることは，元の体系の保存的拡張であるということを証明する．
本研究で扱っているその他の小さな課題については，現在行っている研究を継続する．つまり，非古典論理の証明論については，現在取り扱い中の体系についてカット除去定理を証明し，無際限拡張可能性については，「不完全性定理」についてのダメットの論文の解釈を確定し，論理定項の証明論意味論的観点からの特徴づけについては，特にstabilityという概念がそこでどのような役割を果たすかを考える．
一旦，これらの課題に成功したのちには，２階ないし高階の理論への「構成の理論」の適用，あるいは他の課題の２階論理，高階論理への拡張というさらなる課題に取り組む.
|
Research Products
(4 results)
