2019 Fiscal Year Research-status Report
Proof-Theoretic Study of Doxastic and Epistemic Updates via Questions
| Project/Area Number |
19K12113
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
佐野 勝彦 北海道大学, 文学研究院, 准教授 (20456809)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Keywords | 分散的知識 / 証明論 / カット除去定理 / 認識論理 / Inquisitive logic |
|---|
| Outline of Annual Research Achievements |
疑問文と平叙文を同一設定で扱う inquisitive logic は直観主義論理の拡張ともみなされる。Inquisitive logic への集団知識概念を加える前段階として、(1) Artemov らによる直観主義認識論理の証明論研究、(2) 分散知識概念をもつ認識論理の証明論研究、の二つの研究を行った。また、(3) 直観主義論理へ疑問文の構成を可能とする inquisitive disjunction を加えた intuitionistic inquisitive logic についてのモデル論的研究も行い、国際会議AiML2020へ論文投稿を行った。以下では(1)と(2)の研究実績について説明する。(1) Artemovらは、知識演算子KAの証明とは、Aの証明の存在の決定的検証である、という証明による解釈を提案し、直観主義命題論理について研究を行ったが、その証明論は望ましい性質（部分論理式特性）と満たさない欠点があった。この欠点を取り除いた式計算体系を考案し、さらに、述語論理への拡張も可能であることを明らかにした。この実績は北海道大学文学研究科の大学院生、蘇有安との共同研究として、国際会議LORI-VIIのプロシーディングに採録された。(2) 集団Gの分散的知識（distributed knowledge）とはG中の各エージェントの知識を第三者視点で組み合わせることで得られる知識のことである。分散的知識の研究はこれまで意味論的研究が主であり、式計算による証明論研究は手薄であった。分散的知識概念をもつ認識論理のいくつかの族に対して、式計算体系を与え、カット除去定理、および、クレイグの補間定理が成立することを明らかにした。これは、北海道大学文学研究科の大学院生、村井涼との共同研究として、国際会議FoiKSのプロシーディングに採録された。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究には、(A) 質疑を伴う推論、質疑応答による知識・信念の更新を扱う証明体系の構築、(B) Why 疑問文、How疑問文の形式化、(C) ギャップやグラットを許す矛盾許容論理による疑問文の形式化、の三つの課題が存在した。平成31年度は(A)と(C)の両方に取り組むことを予定していたが、課題(A)についての大きな進展が予想されたため、(A)について集中的に取り組み、質疑を伴う推論を適切に扱う証明体系の構築の前段階として、直観主義認識論理や集団知識概念をもつ認識論理の証明論の整備を行うことができた。
|
| Strategy for Future Research Activity |
令和2年度の研究では、前年度の成果に基づき、さらに課題(A)を進めると同時に平成31年度に予定していた課題(C)Belnap-Dunn による四値論理のinquisitive logic の拡張について取り組む予定である。特に課題(A)については、inquisitive logic の述語論理の拡張（妥当な式全体が公理化できるかは未解決問題である）とその証明論の整備に取り組む予定である。課題(A)の達成を加速させるために、述語論理版 inquisitive logic について準備的議論を行っているTadeusz Litak氏(FAU Erlangen-Nuernberg)を一定期間招へいし、共同研究を行う予定である。
|
| Causes of Carryover |
コロナウイルス感染拡大のため、年度末の国外出張、および、研究打ち合わせの予定がキャンセルとなったため。次年度以降に同じ目的のために使用する予定である。
|
