2021 Fiscal Year Research-status Report
| Project/Area Number |
20K03716
|
|---|
| Research Institution | Shizuoka University |
|---|
Principal Investigator |
鈴木 信行 静岡大学, 理学部, 教授 (60216421)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | 非古典論理 / 述語論理 / 直観主義的算術 / disjunction property / existence property |
|---|
| Outline of Annual Research Achievements |
数理論理学の伝統的に重要なテーマとして、構成性(constructivity)の研究がある。これを特徴的に表現すると考えられる性質が、存在特性(existence property, EPと略記)と選言特性(disjunction property, DPと略記)である。これらふたつの特性の研究は、数理論理学のいくつかの分野でほぼ独立に深めらていた。しかし、数年前に、中間述語論理と直観主義的(構成的) 数学の2分野で重なり合う部分が見いだされ、一方で、一見すると整合的でない結果も現れた。そこで、この一見不整合に見える点をテコとして、直観主義述語論理上でEPとDPを互いに独立な状態で制御する手法を開発し、中間述語論理の研究を進歩させることを本研究の目的としている。
本年度は、構成性が古典論理において壊れていることを典型的に示すprenex normal form theorem(冠頭標準形定理)を超直観主義述語論理の枠組みで考察することを試み、構成性の考察を裏側から見る、という着想で研究を進めた。構成性に「裏側」からアプローチすることを試みたことになる。ここまで研究してきた意味論的道具立て(クリプキ層 Kripke sheavs)を利用することで、超直観主義述語論理においてprenex normal form theoremが成立する実例を無限個生成することができた。それらの中には、直観主義的算術(Heyting arithmetic)において重要な原理(omniscience priciplesと呼ばれる)に対応するような述語論理での公理型(axiom schemata)を付加的公理とするものも、無限個含まれる。
この結果について、ふたつの研究集会で発表を行った。また、関連する論文(査読付き)がひとつ出版された。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
新型コロナウイルス感染症の流行により、当初の計画であったところの研究協力者との議論を深めることが困難であった。そのため、インターネットを活用したリモートのディスカッションに終始し、もうすこし進歩したいところであったが、残念ながらかなわなかった。
外国出張することができず、国際会議での成果発表やできなかった。また、H. Wansing教授のグループ(Ruhr大学Bochum、ドイツ)との研究レビューを予定していたができなかった。
|
| Strategy for Future Research Activity |
本年度にフォーカスしたprenex normal formもそうであるが、述語論理の言語での構成性・非構成性を記述する場合、述語論理の文脈での公理型と構成的数学における公理型とは、その「代入例(instance)」の姿が異なることがある。これを自由に議論し制御するべく考察を進め、理論的枠組みの構築を目指す。
そのため、国内外の研究協力者を含むディスカッションを行う予定である。可能であれば、直接にあって議論したい。新型コロナウイルス感染症の流行により、膝詰めのディスカッションが難しい状況が続くならば、インターネットをより活用して補う予定である。
|
| Causes of Carryover |
研究進捗に不可欠なディスカッションが、新型コロナウイルス感染症による出張困難な事態により、リモートに限られてしまった。特に外国における国際会議出席とディスカッションに支障をきたした。（研究レビューが不可能であったことが大きい。）
次年度は、ある程度のスペックのンピュータやリモート会議用機器を買い整え、インターネットをより活用して、ディスカッションの不足を補う予定である。また、数理論理学の文献資料を収集する。
|
