研究課題/領域番号 |
20K03716
|
研究機関 | 静岡大学 |
研究代表者 |
鈴木 信行 静岡大学, 理学部, 教授 (60216421)
|
研究期間 (年度) |
2020-04-01 – 2025-03-31
|
キーワード | 非古典論理 / 述語論理 / 直観主義的算術 / disjunction property / existence property |
研究実績の概要 |
数理論理学において黎明期からの重要なテーマとして、構成性(constructivity)の研究がある。これを特徴的に表現している性質が、存在特性(existence property, EPと略記)と選言特性(disjunction property, DPと略記)である。これらふたつの特性の研究は、数理論理学のいくつかの分野でほぼ独立に深めらていた。しかし、数年前に、中間述語論理と直観主義的(構成的) 数学の2分野で重なり合う部分が見いだされ、一方で、一見すると整合的でない結果も現れた。そこで、この一見不整合に見える点をテコとして、直観主義述語論理上でEPとDPを互いに独立な状態で制御する手法を開発し、中間述語論理の研究を進歩させることを目的とする。 本年度は、直観主義的算術(Heyting arithmetic)とその周辺について、研究協力者と議論して、基本的な概念(特に直観主義的算術のモデルに関するもの)について整理することに集中した。分野横断的な研究において、基本概念の分野間での様々な「ねじれ」をすり合わせることは、大変重要であることから、今後の研究には欠かせない部分が進展したと考える。これにより、直観主義的(構成的) 算術をベースとするのEPとDPについて、一定の理解が得られた。また、意味論的道具立て(クリプキ層 Kripke sheavs)を利用する手法について考察した。 本研究の中心的な概念であるEPとDPに関する内容について、日本数学会 秋季総合分科会(数学基礎論および歴史分科会)で特別講演を行った。
|
現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
当初の計画に従い、研究協力者と膝づめで討論することを予定していたが、新型コロナウイルス感染症の流行により、実際に会合することが不可能であった。そのため、インターネットを活用したリモートのディスカッションに終始し、もうすこし進歩したいところであったが、残念ながらかなわなかった。 外国出張することができず、国際会議での成果発表やできなかった。また、H. Wansing教授のグループ(Ruhr大学Bochum、ドイツ)との研究レビューを予定していたができなかった。
|
今後の研究の推進方策 |
存在特性(existence property)を述語論理の言語で書く場合、中間述語論理の文脈での公理型と構成的数学における公理型とは、その「代入例(instance)」の姿が異なることがある。これを自由に議論し制御できる概念として、新しい理論的枠組みが必要であり、その構築を目指す。 そのため、研究協力者を含むディスカッションを行う予定である。新型コロナウイルス感染症の流行により、膝詰めのディスカッションが難しい状況なので、インターネットをより活用して補う予定である。
|
次年度使用額が生じた理由 |
新型コロナウイルス感染症による出張困難な事態により、研究協力者との連絡がリモートに限られてしまい、特に外国における国際会議出席と討論に支障をきたした。外国出張ができなかったため、研究レビューが不可能であった。 インターネットをより活用して、ディスカッションの不足を補う予定である。そのために、コンピュータやリモート会議用機器を購入する。 また、数理論理学の文献資料を収集する。
|