| 研究課題/領域番号 |
20K03716
|
|---|
| 研究機関 | 静岡大学 |
|---|
研究代表者 |
鈴木 信行 静岡大学, 理学部, 教授 (60216421)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| キーワード | 非古典論理 / 述語論理 / 直観主義的算術 / disjunction property / existence property |
|---|
| 研究実績の概要 |
数理論理学の伝統的に重要なテーマとして、構成性(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)を付加的公理とするものも、無限個含まれる。
この結果について、ふたつの研究集会で発表を行った。また、関連する論文(査読付き)がひとつ出版された。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
新型コロナウイルス感染症の流行により、当初の計画であったところの研究協力者との議論を深めることが困難であった。そのため、インターネットを活用したリモートのディスカッションに終始し、もうすこし進歩したいところであったが、残念ながらかなわなかった。
外国出張することができず、国際会議での成果発表やできなかった。また、H. Wansing教授のグループ(Ruhr大学Bochum、ドイツ)との研究レビューを予定していたができなかった。
|
| 今後の研究の推進方策 |
本年度にフォーカスしたprenex normal formもそうであるが、述語論理の言語での構成性・非構成性を記述する場合、述語論理の文脈での公理型と構成的数学における公理型とは、その「代入例(instance)」の姿が異なることがある。これを自由に議論し制御するべく考察を進め、理論的枠組みの構築を目指す。
そのため、国内外の研究協力者を含むディスカッションを行う予定である。可能であれば、直接にあって議論したい。新型コロナウイルス感染症の流行により、膝詰めのディスカッションが難しい状況が続くならば、インターネットをより活用して補う予定である。
|
| 次年度使用額が生じた理由 |
研究進捗に不可欠なディスカッションが、新型コロナウイルス感染症による出張困難な事態により、リモートに限られてしまった。特に外国における国際会議出席とディスカッションに支障をきたした。（研究レビューが不可能であったことが大きい。）
次年度は、ある程度のスペックのンピュータやリモート会議用機器を買い整え、インターネットをより活用して、ディスカッションの不足を補う予定である。また、数理論理学の文献資料を収集する。
|
