2019 Fiscal Year Research-status Report
| Project/Area Number |
18K00036
|
|---|
| Research Institution | Kanazawa University |
|---|
Principal Investigator |
黒川 英徳 金沢大学, GS教育系, 准教授 (30710230)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Keywords | 証明論的意味論 / 論理定項 / ラベル付きシークエント計算 / モデル論的帰結関係 / informal rigour / 非可述的 |
|---|
| Outline of Annual Research Achievements |
１）論理定項の証明論的意味論の観点からの特徴づけという目標への準備作業として、証明論的意味論における基本概念であるダメットの「stability」という概念について解明を行った。これは昨年度からアルベルト・ナイボ、マティア・ペトローロの二人と共同で継続している研究である。この研究では元来自然演繹という枠組みで考えられたstabiltiyという概念をシークエント計算という枠組みの中で特徴付けることを目指している。昨年度ドイツの学会で発表した内容を論文にする際、そこからのスピンオフとしてもう一本論文になるほどの内容が議論の結果として得られたため、現在その新しい論文を作成中である。
２）申請書で述べた関連研究であるサラ・ネグリとの共同研究である、ラベル付きシークエント計算によるrelevant logic の研究を進め、論文として仕上げた。現在投稿中である。
３）本研究は証明論的意味論に基づくが、申請書にもある通り、モデル論的帰結関係との対比も取り扱う。2019年度は当初想定していたよりも積極的に、モデル論的な帰結関係と証明論的なそれの関係がどのようなものかということを考察した。これら２つは通常、完全性定理により結び付けられる。ではその完全性定理のもつ哲学的な意義とは何か？ これをを証明論の大家であったクライゼルによる「informal rigour」という概念に関する議論を中心に探究した。これは日本数学会の秋季大会、人工知能学会の大会におけるLENLSというワークショップで口頭発表され、論文はそれぞれの学会のproceedingsの中で出版された。
４）申請書にも言及した二階論理の証明論的意味論に関する研究として、竹内外史の証明論（あるいは証明の概念）による非可述的集合概念の解明というテーマについて昨年度発表した内容を１ヶ月以上の時間をかけて改訂し、論文として出版した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
以下の理由より、昨年度の研究の進捗は概ね満足すべきものであったと思われる。１）2019年度中に本研究に関連する幾つかの発表を行い、また幾つかの論文を出版することができた。
２）証明論的意味論の観点からの論理定項の特徴付けという大きなテーマについては長足の進歩があったとは言い難い。とりわけネステッド・シークエントを使った証明論的研究はすでに成果は上がっているとはいえ、まだ論文にする時間がない。しかしながら、それでも「stabiltiy」のような証明論的意味論において重要な概念に関する解明を確実に進めることができている。「stability」の概念に関するシークエント計算によるアプローチに関しても研究は進んでいるが、そもそもその「stability」という概念についてどのような理解をすればよいかということに関し、ある程度概念的な解明をすることができたことは進歩である。
３）やはり当初の関心からすれば副次的な関心であったものの、モデル論的な意味での論理的帰結関係、そして完全性定理の意義について証明論的意味論ともリンクする形で概念的な考察を加えることができた。このことは論理学の根本概念への考察を進めたことになっていると考えられる。
４）竹内外史は日本の数理論理学の歴史において最も偉大な論理学者といってよい。その竹内外史が日本語で残した、「集合概念」と「証明概念によるその解明」という重要な「哲学的」考察の意義について英文で出版することができた。このことはこの分野における重要な貢献であると思われる。
|
| Strategy for Future Research Activity |
１）「stability」に関して現在行っている研究をさらに進め、「stability」の概念的解明に関するものと、シークエント計算の観点からの「stability」概念の分析の少なくとも二本の論文にする。
２）ネステッド・シークエントを使った、多くの非古典論理体系の定式化とカット除去定理の証明を含む論文を執筆する。証明はできているため、執筆時間を十分にとることができれば十分実現可能である。
３）２）に関連し、ネステッド・シークエントの歴史的な起源がローレンツェンと彼の学派にあることが明らかになったため、ネステッド・シークエントとローレンツェン風の論理規則のadmissibilityという概念との間の関係について考察を深める。
４）クライゼルの「informal rigour」の概念についてのワルター・ディーンとの共同研究をさらに進める。完全性定理、論理的帰結についてさらに考察を深めるだけでなく、申請書でも言及した「構成の理論」とも深く関係する直観主義論理における「選列（choice sequence）」の理論について、直観主義論理の論理定項の意図された意味との関係も含めて考察する。
４）竹内外史の論理思想についてさらに研究を進める。特に、集合概念とその証明論的解明という思想が竹内の基本予想とどのように関係しているのか、また竹内の後期の思想における独自の集合概念の展開などについてさらに研究する。
|
| Causes of Carryover |
次年度使用額が生じたのは、コロナウィルスの蔓延のため、３月に予定していた、共同研究及び、コンファレンス参加を目的とするヨーロッパへの出張をキャンセルせざるを得ないこととなったためである。
翌年度分として請求した金額と合わせ、海外出張が可能になった時点で共同研究を目的として、ヨーロッパへの出張を行う予定である。また必要に応じて書籍、コンピュータなどの物品を買う費用に充てることにする。
|
